Theory of Computing
-------------------
Title     : A Lower Bound for Polynomial Calculus with Extension Rule
Authors   : Yaroslav Alekseev
Volume    : 22
Number    : 4
Pages     : 1-29
URL       : https://theoryofcomputing.org/articles/v022a004

Abstract
--------

A major proof complexity problem is to prove a superpolynomial lower
bound on the length of Frege proofs of arbitrary depth. A more
difficult question is to prove an Extended Frege lower bound.
Surprisingly, proving such bounds turns out to be much easier in the
algebraic setting. In this paper, we study a proof system that can
efficiently simulate Extended Frege: an extension of the Polynomial
Calculus proof system where we can take a square root and introduce
new variables that are equivalent to algebraic circuits of arbitrary
depth. We prove that an instance of the subset-sum principle, the
binary value principle $1 + x_1 + 2 x_2 + \ldots + 2^{n - 1} x_n = 0$
($BVP_n$), requires refutations of exponential bit size over
$\Q$ in this system.

Part and Tzameret (ITCS'20) proved an exponential lower bound on the
size of Res-Lin (Resolution over linear equations) refutations of
$BVP_n.$ We show that our system p-simulates Res-Lin and
thus we get an alternative exponential lower bound for the size of
Res-Lin refutations of $BVP_n.$


---------------

A preliminary version of this paper appeared in the Proceedings of
the 36th Conference on Computational Complexity (CCC'21).