On the Unprovability of Circuit Size Bounds in Intuitionistic 𝖲^1_2

We show that there is a constant k such that Buss's intuitionistic theory 𝖨𝖲^1_2 does not prove that SAT requires co-nondeterministic circuits of size at least n^k. To our knowledge, this is the first unconditional unprovability result in bounded arithmetic in the context of worst-case fixed-polynomial size circuit lower bounds. We complement this result by showing that the upper bound 𝖭𝖯⊆𝖼𝗈𝖭𝖲𝖨𝖹𝖤[n^k] is unprovable in 𝖨𝖲^1_2.