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 AC0p 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 /∈ AC0pd 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.