Strong co-nondeterministic lower bounds for NP cannot be proved feasibly

We show unconditionally that Cook’s theory PV formalizing poly-time reasoning cannot prove, for any non-deterministic poly-time machine M defining a language L(M), that L(M) is inapproximable by co-nondeterministic circuits of sub-exponential size. In fact, our unprovability result holds also for a theory which supports a fragment of Jeřábek’s theory of approximate counting APC1. We also show similar unconditional unprovability results for the conjecture of Rudich about the existence of super-bits.