Meta-Mathematics of Algebraic Complexity

We initiate the study of the meta-mathematics of algebraic circuit lower bounds, aiming both to gain insight into the methods sufficient and necessary to prove algebraic circuit lower bounds, and to contribute to the study of bounded arithmetic as a logical foundation for complexity lower bounds. We demonstrate that while algebraic circuit lower bounds are hard for somewhat weak proof systems such as polynomial calculus resolution (PCR), contemporary lower bounds are efficiently provable in proof systems and bounded arithmetic theories corresponding to NC 2 , such as VNC 2 and the corresponding class of propositional Frege proofs of quasipolynomial-size. Moreover, going below VNC 2 into algebraic constant-depth reasoning is likely insufficient to efficiently prove already constant-depth algebraic circuit lower bounds. Specifically, we show the following. NC 2 -reasoning and rank method. Algebraic circuit lower bounds are often proved via the "rank method", with recent prominent applications including the constant-depth lower bounds of Limaye, Srinivasan and Tavenas [27] and Forbes [10]. We show that these rank-based arguments can be formalized in the bounded arithmetic theory VNC 2 , which captures reasoning with NC 2 concepts. This complements the work of Tzameret and Cook [47], who formalized structural upper bounds in this theory, and provides a unified framework for studying barriers to current algebraic complexity methods, complementing barriers studied by Efremenko, Garg, Makam, Oliveira, and Wigderson [9, 13]. Sparsity algebraic reasoning. We show that Polynomial Calculus Resolution (PCR) cannot efficiently prove superpolynomial algebraic circuit lower bounds for any family of polynomials. Moreover, PCR cannot efficiently prove exponential constant-depth circuit lower bounds for any family of polynomials. Constant-depth algebraic reasoning. We introduce the Tensor Rank Principle and demonstrate it is hard for PCR. We show that if this principle is hard against constant-depth Ideal Proof System (IPS) then constant-depth IPS cannot efficiently prove constant-depth algebraic circuit lower bounds.