On the consistency of circuit lower bounds for non-deterministic time

We prove the first unconditional consistency result for superpolynomial circuit lower bounds with a relatively strong theory of bounded arithmetic. Namely, we show that the theory [Formula: see text] is consistent with the conjecture that [Formula: see text], i.e. some problem that is solvable in non-deterministic exponential time does not have polynomial size circuits. We suggest this is the best currently available evidence for the truth of the conjecture. The same techniques establish the same results with [Formula: see text] replaced by the class of problems decidable in non-deterministic barely superpolynomial time such as [Formula: see text]. Additionally, we establish a magnification result on the hardness of proving circuit lower bounds.