The Propositional Proof System of APX₁: Formalizing Razborov-Smolensky Below APC₁

We study the proof complexity of constant-depth circuit lower bounds with modularcounting gates in bounded arithmetic. While it is known that the theory PV1 proves AC0 lowerbounds and APC1 proves lower bounds for AC0[p] circuits, the exact proof-theoretic strengthrequired for the Razborov–Smolensky lower bound has remained an open question. We showthat APX1, a theory introduced by Chen, Li, Oliveira, and Williams [ CLOW26 ] capturingapproximate counting, is sufficient. Specifically, we prove that APX1 ⊢ MODq /∈ AC0[p]d byproviding a sharp decomposition of the proof: the algebraic dimension-counting argumentformalizes in PV1, while the probabilistic approximation step requires only the first-momentmethod available in APX1, avoiding full Chernoff bounds. Furthermore, we introduceEF(P)—Extended Frege augmented with approximate counting oracle axioms—as the naturalpropositional translation of APX1, a system which, to the best of our knowledge, is absentfrom existing proof complexity literature. We conclude with motivated conjectures regardingthe Additivity Gap, the Proof Analysis Problem for EF(P), and model-theoretic obstructionsto propositional reflection.