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. Under an algebraic analogue of the Krajicek--Razborov conjecture, our results suggest that proving superpolynomial lower bounds for general algebraic circuits will require stronger reasoning than that used in the rank-based proofs studied here. Specifically, we show the following.

$\mathbf{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 [LST25] and Forbes [For24]. We show that these rank-based arguments can be formalised in the bounded arithmetic theory $VNC^2$, which captures reasoning with $NC^2$ concepts. This complements the work of Tzameret and Cook [TC21], who formalised structural $\mathit{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 [EGdOW18, GMdOW19].

$\mathbf{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.

$\mathbf{Constant}$-$\mathbf{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.