A major goal of proof complexity is to show limits on the types of reasoning formalizable with concepts of small computational complexity, usually formalized as circuits from small circuit classes. This makes results in proof complexity analogous to (and often building on) results in circuit complexity. However, despite having strong lower bounds for the class AC 0 [p] since the 1980's, ( [18,19] ) it is still an open problem in proof complexity to establish superpolynomial (or even quadratic) lower bounds for the corresponding proof system AC 0 [p]-Frege.
Motivated by the lack of progress towards proving AC 0 [p]-Frege lower bounds, [4] defined the Nullstellensatz (Nullsatz) proof system for refuting systems of unsolvable polynomial equations. Given a system of polynomial equations P = {P 1 = 0, . . . , P m = 0} in Boolean variables x 1 , . . . , x n (where we enforce the Boolean condition by adding the equations x 2 i -x i = 0 to P), a Nullsatz refutation of P over a field F is a set of polynomials Q = {Q 1 , . . . , Q m } such that i P i Q i = 1. The degree of the refutation is the maximum degree of the P i Q i 's, and the size is the sum of the sizes of the polynomials in P, Q. A dynamic version of Nullsatz, called the Polynomial Calculus (PC) was later defined in [10].
While these and later papers showed strong lower bounds for these proof systems, often these lower bounds were brittle in that the tautologies where lower bounds were proved also had small upper bounds under changes of variables. Our work is intended to address the issue of proving algebraic proof lower bounds that are more robust under changes of variables. This can be viewed as a small but significant step towards proving lower bounds for AC 0 [p]-Frege, since the latter can simulate such changes of variables.
One reason for the brittleness of many of the earlier lower bounds is that these lower bounds were highly sensitive to the initial encoding. The known PC lower bounds hold for unsatisfiable CNF formulas which are converted to a corresponding system of unsolvable polynomial equations. Previous works established exponential PC lower bounds assuming a Boolean encoding, where the variables are Boolean, enforced by the initial equations x 2 i -x i = 0. Another natural encoding is the "Fourier" encoding which represents the constraints by polynomials over {-1, 1}-valued variables (by applying the linear transformation x i = 1 -2x i to the Boolean encoding). However under this second encoding, the size lower bounds all break down. This is due to the proof method, where size lower bounds were obtained from degree lower bounds. Over {0, 1}-valued variables, this can be accomplished by applying known size-degree tradeoffs for PC or by a random restriction argument to kill off all large monomials. But over {-1, 1}-valued variables, these methods no longer work: a generic sizedegree tradeoff no longer holds (there are polynomial sized proofs of the Tseitin tautologies, although they require linear degree [8]), and since the monomials now correspond to parity equations, they are resilient to random restrictions.
However, recently, Sokolov [20] broke this barrier, and managed to prove exponential size lower bounds for PC refutations over the {-1, 1} encoding. We note that while this may seem like a minor improvement over the known lower bounds which held for the {0, 1}-encoding, Sokolov had to invent a new and ingenious technique for proving size lower bounds. In this work, we generalize the methods of Sokolov to prove exponential PC lower bounds with up to M = N 2-ϵ extension variables which can depend on up to κ = O(log N ) original variables (where N is the number of variables in the tautology). This shows that the Sokolov method can be used to prove highly robust lower bounds, that are not sensitive to local changes of variables. We state our result more precisely for two different choices of parameters, one that maximizes the size lower bound, and the other that maximizes the number of allowable extension variables.
▶ Theorem 1 (high-end). For n sufficiently large, there is a family of CNF tautologies F SEL on O(n log n) variables with poly(n) clauses of width O(log n) such that for any M = npolylog(n) and κ = O(log log n), any PC refutation over F p of F SEL , together with M κ-local extension axioms, requires size 2 Ω(n/polylog(n)) .
▶ Theorem 2 (low-end). For the same family of tautologies as above, there are 0 < α, β, γ < 1 so that, for M = n 1+α , κ = βlogn, any PC refutation of F SEL together with any M κ-local extensions over F p requires size 2 Ω(n γ ) .
We remark that our extension variables are only allowed to depend on the original variables, and not on previously defined extension variables. (In the more general case where extension variables are defined recursively, the proof system corresponds to AC 0 [p]-Frege, where the level of recursion corresponds to the AC 0 [p] circuit depth.) Thus our lower bound can be (roughly) seen as proving exponential lower bounds for the following restricted class of depth-2.5 PC refutations. First, the refutation is given a new set of M variables, z 1 , . . . , z M , and is allowed to define a corresponding set of M κ-local polynomials Q 1 , . . . , Q M (where each Q i can only depend on κ original variables). Lines in the refutation are polynomials over the original variables, plus the new extension variables (which are placeholders for the Q i 's). Substituting the Q i 's for the new variables gives a set of depth 2.5 algebraic circuits using a pre-specified set of κ-local functions at the bottom layer of the circuit.
The work that inspired us and that is most related to our result is the recent paper by Sokolov [20], proving exponential lower bounds on the size of PC refutations of CNF formulas, where the variables take on values in {1, -1}. We generalize Sokolov's result to hold over any finite field, even with the addition of superlinear many extension variables, each depending arbitrarily on a small number of original variables. Thus our result can be alternatively viewed as making progress towards proving exponential lower bounds for depth-3 AC 0 [p]-Frege, for a family of CNF formulas.
We note that for systems of polynomial equations over the rationals, a body of recent work establishes much stronger lower bounds. First, [13] proved lower bounds for subsystems of IPS over the rationals by restricted classes of circuits, including low-depth formulas, multilinear formulas and read-once oblivious branching programs. Secondly, Alekseev [2] proved exponential lower bounds on the bit complexity of PC proofs with an arbitrary number of extension variables of unbounded depth over the rationals. Andrews and Forbes [3] prove quasipolynomial lower bounds on the circuit size of constant-depth IPS proofs for a different family of polynomials over the rationals; however, their hard instances do not have small-size constant-depth circuits. Finally, [14] establish a similar lower bound as [3], but for hard instances that have small constant-depth circuits.
We remark that these lower bounds are incomparable to ours for several reasons. First, they do not hold for finite fields, and secondly, the choice of hard polynomials are inherently nonboolean: [13,2,14] use the subset sum principle which when translated to a propositional statement is no longer hard, and the hard polynomials in [3] have logarithmic depth. Thus on the one hand they establish superpolynomial lower bounds for much stronger subsystems of IPS, but on the other hand, they do not translate to lower bounds for propositional proofs in the sense of Cook-Reckhow [11]. In particular, they don't imply lower bounds for proof systems dealing with Boolean formulae.
The standard way of proving size lower bounds for PC for an unsatisfiable formula F for Boolean-valued variables dates back to the celebrated superpolynomial lower bounds for Resolution [15,7], where the basic tool is to reduce size lower bounds to degree lower bounds (or in the case of Resolution, size to clause-width) by way of either a general size-depth tradeoff, or by a more general random restriction argument. At a high level, both methods iteratively select a variable that occurs in a lot of high-degree terms, set this variable to zero (to kill off all high-degree terms containing it), while also ensuring (possibly by setting additional variables) that F remains hard to refute after applying the partial restriction. After applying this size-to-degree reduction, the main technical part is to prove degree lower bounds for the restricted version of F .
As mentioned in the Introduction, over the {-1, 1} basis, the size to degree reduction breaks down. In fact, no generic reduction to degree can exist since random XOR instances over this basis require linear degree but have polynomial size PC refutations. Moreover, we lacked any method for proving PC lower bounds for unsatisfiable CNFs over the basis {-1, 1}, and more generally over an arbitrary linear transformation of the variables. In [16], we highlighted this as an open problem, noting that it is a necessary step toward proving superpolynomial AC 0
Recently, Sokolov [20] made significant progress by proving exponential lower bounds for PC (as well as for SOS) for random CNF formulas over the domain {-1, 1}, by developing new formula-specific techniques to reduce size to degree over this domain. As this is the starting point for our work, we begin by describing the main method in [20] for reducing size to degree for certain families of formulas over {-1, 1}.
Let Π be an alleged PC refutation of F of small size which includes the axioms w 2 = 1 for all variables w. The first step in Sokolov's argument is to show how to remove all high degree terms containing a particular variable w, provided that w is irrelevant -meaning that it does not occur in any of the initial polynomials other than the equation w 2 = 1. Intuitively, we want to show that if our unsatisfiable system of polynomial equations doesn't contain w, then we should be able to eliminate high degree terms containing w altogether from the refutation. To show this, Sokolov introduced a new operation termed Split where he writes each line q in the refutation as q 0 + q 1 w, and proves by induction that if we replace each line q by the pair of lines q 0 , q 1 , then it is still a valid refutation of F (and no longer contains w). While the Split operation removes w from the proof, it doesn't kill off high degree terms. The crucial insight is that although this doesn't directly kill off high degree terms, a slightly different measure of degree (called Quadratic degree) can be used instead, since removing w via the Split operation removes all high Quadratic degree terms that w contributed to, and secondly low Quadratic degree implies low ordinary degree. The second and easier step in Sokolov's argument uses specific expansion properties of F to show that for any variable w, there exists a small restriction ρ (to some of the other variables) such that w becomes irrelevant under ρ.
Our main theorem significantly generalizes Sokolov's lower bound by proving exponential lower bounds for an unsatisfiable CNF formulas F , even when we allow the axioms P to contain superlinear many extension axioms, provided that each extension axiom depends on a small number of original variables. Note that the variables of F are Boolean, but the extension variables are not restricted to being Boolean. In particular, it may be the case that zero is not in the support of an extension variable (i.e. the set of all possible values that can be assigned to it without violating any Boolean axioms), for example if extension variable z is defined by the equation z = x -2, then z cannot be set to zero without falsifying the Boolean axiom x 2 -x = 0 for x. Intuitively we will handle extension variables z that cannot be set to zero in a similar manner to Sokolov, by first isolating z, and then generalizing the Split operation in order to kill off all large Quadratic degree terms that contain z. However, dealing with a general set of extension axioms presents new technical challenges that we address next.
Our first idea is to design the unsatisfiable formula F carefully so that we can force variables to be irrelevant in a more modular way. Specifically, let F (x 1 , . . . , x n ) be an expanding unsatisfiable k-CSP formula with m = O(n) constraints, such that any subset of m ′ = ϵm constraints is unsatisfiable and requires proofs of large PC degree. We define an unsatisfiable formula F SEL (based on F ) that intuitively states that there is a subset S of m ′ = ϵm constraints of F (as chosen by new selector variables y) that is satisfiable. We will prove lower bounds on the set of constraints F SEL even with the addition of an arbitrary set of extension axioms satisfying the conditions mentioned earlier. In order to make a variable of F SEL irrelevant, we will simply make sure that our eventual assignment to the selector variables (y) avoids constraints of F that contain this variable (we can also make a selector variable irrelevant in a slightly more complicated way, details are left to the relevant section).
A second challenge that we face (that doesn't come up in Sokolov's proof) is that extension variables may be defined so that originally they can be consistently set to zero, but can change status after applying a restriction. For example, suppose the proof uses the extension axiom z = x 1 x 2 + x 1 . Then zero is in the support of z (since we can set x 1 = x 2 = 0), but if we set x 1 = 1, then zero is no longer in the support of z. In order to deal with this dynamically changing status of variables, our notion of Quadratic degree must pay attention to which category each of the extension variables is in at any particular time, and make sure that we do not lose progress that was made earlier due to variables changing from initially containing zero to disallowing zero in their support. Fortunately we observe that variables can only change unidirectionally, (since the support of a variable cannot increase under a restriction) and this is crucial for arguing that our measure of Quadratic degree always decreases so that we continually make progress.
Finally, we also have to generalize Sokolov's Split operation, which was previously defined only for {-1, 1} variables. We give a generalization of how to do the Split for arbitrary valued variables.
2 Preliminaries ▶ Definition 3 (Polynomial Calculus/Polynomial Calculus Resolution). Let Γ = {P 1 . . . P m } be an unsolvable system of polynomials in variables {x 1 . . . x n } over F. A PC (Polynomial Calculus) refutation of Γ is a sequence of polynomials {R 1 . . . R s } such that R s = 1 and for every ℓ ∈ [s], R ℓ ∈ Γ, R ℓ is either a polynomial from Γ, or is obtained from two previous polynomials R j , R k , j, k < ℓ by one of the following derivation rules: R ℓ
The size of the refutation is
where |R ℓ | is the number of monomials in the polynomial R ℓ . The degree of the refutation is max ℓ deg(R ℓ ). A PCR (Polynomial Calculus Resolution) refutation is a PC refutation over the set of Boolean variables {x 1 . . . x n , x1 . . . xn } where {x 1 . . . xn } are twin variables of {x 1 . . . x n } i.e. the equations x 2 i -x i = 0, xi 2 -xi = 0 and x i xi = 0 are treated as axioms. ▶ Definition 4 (PC plus Extension Axioms). Let Γ = {P 1 . . . P m } be a set of polynomials in variables {x 1 . . . x n } over a field F. We will refer to the polynomials in Γ as (initial) axioms. Let z = z 1 . . . z M be new extension variables with corresponding extension axioms z j -Q j (x 1 . . . x n ). A PC + Ext (PC plus extension) refutation of Γ with M extension axioms Ext
at most κ of the x-variables. We say that Π is a (M, κ) -PC + Ext refutation of Γ if it is a PC + Ext refutation of Γ with M extension axioms, each of which are κ-local. The size of the refutation is total size of all lines in the refutation, including the polynomials in Γ plus the extension axioms (where the size of a line P ∈ Π is the number of monomials in P ).
We note that our definition of extension axioms is more limited than the general notion of extension axioms. Here we only allow the extension variables to depend on the original variables from Γ; the more general definition allows the extension variables to depend on the original x-variables, and also on other extension variables.
▶ Definition 5 (k-local CSPs). A constraint C i over Boolean variables {x 1 , . . . , x n } is simply a Boolean formula over these variables.
We translate a k-CSP formula into a system of polynomial equations using the standard PCR translation which we define next.
▶ Definition 6 (Converting k-CSPs into Polynomial Equations). Let C be a k-local constraint over variables x i1 , . . . , x i k . We convert C to a polynomial equation, p(C), using the translations p(
It is easy to check that for any Boolean assignment α to the underlying variables, C(α) = 1 ↔ p(α) = 0, and
} where E j is the polynomial equation p(C j ) In addition, we add the Boolean axioms
to be zero-one valued, and force exactly one of x i , xi to be one.
The Hard Formulas
We distinguish between the case p = 2 and the case p > 2, and concentrate on the latter. This is because the case p = 2 does not require any new technical ideas, and we can pick from a large number of known hard tautologies for this case, such as random CN F 's. Over F 2 , every extension variable is zero-one valued, and so standard size-degree tradeoffs pertain even with respect to extension variables. Also, κ-local extension variables can change the degree by at most a factor of κ, therefore a degree lower bound of Ω(n) for the original tautology over n variables implies a degree lower bound of Ω(n/κ) after adding κ-local extension variables. Known size-degree tradeoffs imply that the degree must be at least square root of the number of variables in order to obtain exponential size lower bounds, this immediately gives a lower bound tolerating close to n 2 /κ 2 many κ-local extension variables [10,6,17]. Over any field, there are unsatisfiable families of k-CNF formulas (e.g. the Tseitin tautologies as well as random parity equations) that require linear degree but have polynomial sized proofs with a linear number of extension variables [8,6]. Therefore formulas that require high PC degree are not sufficient. Instead we will create our hard examples by taking a hard instance and then using selector variables to pick out a subset of the constraints. Similar ideas were used earlier (e.g., [12]). In more detail, our underlying hard unsatisfiable formulas, {F SEL n,k }, will be constructed from a family of k-CSP formulas, F n,k , that have the property that any sufficiently large subset of the constraints of F n,k is unsatisfiable and still requires large PC degree.
consists of the polynomial equations E SEL together with the Boolean axioms
Intuitively we think of the y variables as a mapping from m ′ pigeons to m holes, where the holes correspond to the m axioms/constraints from E. For i ∈ [m ′ ], the i th "pigeon" y i selects a hole (an equation from E).
The first set of polynomial equations in E SEL states that if pigeon y i selects the equation E b1...b log m , then this equation must be satisfied; the second set of equations in E SEL states that the mapping is one-to-one and thus altogether the y selector variables choose a subset E ′ of exactly m ′ equations from E. Thus F SEL n,k asserts that there exists a subset of m ′ constraints of F n,k (chosen by the y-variables) that are satisfiable.
Throughout this paper, the x-variables are the variables that underly F n,k ; the y-variables are the selector/pigeon variables described above that choose a subset of m ′ constraints from F n,k , and the extension variables used in the PC + Ext refutation will be the z-variables.
Our hard instances will be
▶ Property 8. Every subset of (1 -ϵ)m ′ constraints is unsatisfiable and requires linear PC degree.
The following Theorem shows that for sufficiently large n, such formulas exist. Similar proofs have appeared in several papers (e.g., [5]) but we give a proof in the Appendix for completeness.
▶ Theorem 9. Let m = 10n. Then there exists constants k > 0, 0 < ϵ < 1 such that for sufficiently large n, there exists k-CSP formulas {F n,k } with m constraints such that Property 8 holds with m ′ = (1 -ϵ)m.
The Lower Bound
Conventionally, proof size lower bounds are reduced to degree lower bounds, a single step of which involves finding a heavy variable that occurs in a large fraction of high degree terms of the proof and setting it to zero. In our setting, if the heavy variable turns out to be an extension variable, z with extension axiom z = Q(x, y), it may be Nonsingular meaning that we cannot set z = 0 (without falsifying the extension axiom or a Boolean axiom), as opposed to Singular variables which can be set to zero in a consistent way 1 . In this case, we cannot simply eliminate the high degree terms containing z by setting z = 0. Sokolov [20] focused on the case where variables are over the ±1 basis instead of the usual Boolean one, which is the simplest case where all variables are Nonsingular. Sokolov introduced Quadratic degree as a measure to be used instead of degree. Quadratic degree essentially measures the maximal degree of the square of each polynomial P occurring in the proof. For a ±1 variable z, z 2 = 1, so squaring a polynomial P on ±1 variables removes the contribution of a term t ∈ P as it gets squared out, and what remain are the terms t 1 t 2 for t 1 , t 2 ∈ P . Since any variable that appears in both terms gets squared out, the degree of these terms measures the symmetric difference between such terms, and this turns out to be a key complexity measure while dealing with Nonsingular variables. Sokolov showed that a refutation of low Quadratic degree can be turned into one of low degree. Thus the presence of Nonsingular variables 1 This terminology is taken from singular and nonsingular matrices, since the key property we use is that a variable z is Nonsingular if and only if z p-2 is a "multiplicative inverse" of z, i.e. z p-1 = 1 C C C 2 0 2 3
Lower Bounds for Polynomial Calculus with Extension Variables over Finite Fields is not necessarily a problem as long as the Quadratic degree of each line is low. Sokolov also introduced an operation Split that acts on a proof line by line in order to remove the contribution to Quadratic degree of any particularly heavy Nonsingular variable z, in the special case where they always take on values in ±1, by replacing a line P = P 1 z + P 0 in the refutation with the lines P 1 and P 0 . Sokolov managed to show that for some well chosen tautologies, the new Split lines still form a valid refutation of a hard subset of axioms. The crucial observation here is that this splitting of lines has eliminated from the square of the proof all pairs of terms whose product contained z. Thus, repeated application of Split would lead to contradiction of known degree lower bounds.
The first step for us was to generalize the notions of Quadratic degree and Split to any finite field. Motivated by the above definition of Quadratic degree, we generalize it as follows. Given two terms t 1 and t 2 , a Nonsingular variable z contributes to the Quadratic degree between t 1 and t 2 if and only if it appears with different exponents in them, i.e. z i ∈ t 1 and z j ∈ t 2 , for i ̸ = j. A Singular variable z contributes if and only if it appears in one of the terms with a nonzero exponent. The Quadratic degree of t 1 and t 2 is the total number of such variables z that contribute. Generalizing the Split operation proved a bit more difficult. We first focus on the case over F p analogous to Sokolov's, where we have a variable z such that the identity (z -a)(z -b) = 0 holds for some constants a, b ̸ = 0 in the field. Note that a line P (z) of the proof is of the form P p-2 z p-2 + • • • + P 1 z + P 0 . In the case of ±1 variables, p = 3 and thus the contribution by z to Quadratic degree comes just from the interaction between two polynomials P 1 and P 0 . Therefore separating P 1 and P 0 into different lines removes this contribution entirely. In the general case, however, the contribution by z to Quadratic degree is the sum total of interactions between polynomials P i and P j for every pair i, j < p -1 such that i and j are distinct. We show how to separate P into two lines R 1 , R 0 such that the interaction between P i and P j is completely removed, for any i, j satisfying a i-j ̸ = b i-j , or in other words, z i and z j are linearly independent over the two values that z takes. Let R(z) = R 1 z i + R 0 z j be a polynomial such that R agrees with P for each possible value of z, i.e. R(a) = P (a) and R(b) = P (b). Since z i and z j are linearly independent over values {a, b}, these two equations can be solved for their coefficients R 1 , R 0 , expressed in terms of P p-2 . . . P 0 . On closer observation, we find that P i does not occur in the expression for R 1 and similarly P j does not occur in R 0 , and therefore we have successfully broken P into lines R 1 and R 0 while separating P i and P j . It is straightforward to show that this new set of lines forms a valid refutation, but an essential assumption we make here is that the initial axioms are free of z, except for (z -a)(z -b) = 0.
We now move to dealing with the case of a more general extension variable z with the extension axiom z -Q, where Q(x, y) is a polynomial that can depend on at most κ variables. Let H be the set of all pairs of terms (t 1 , t 2 ) in a line of a given refutation that have high Quadratic degree between them. We would like to emulate Sokolov's strategy of eliminating this set of pairs from the refutation to drop its Quadratic degree. If an extension variable z which is Singular appears heavily in H, we apply the restriction that sets it to zero (which exists by the definition of Singular). In the case that z is Nonsingular, our goal is to reduce it to the above case in order to apply Split. But first, we will have to choose a "good" pair of indices ℓ 1 , ℓ 0 such that Splitting them is effective in reducing H. We observe that for any pair of indices i, j, the set of pairs (t 1 , t 2 ) in H such z i ∈ t 1 and z j ∈ t 2 is disjoint from the similar set defined for a distinct pair i ′ , j ′ . Therefore by averaging we can pick a good pair ℓ 1 , ℓ 0 that covers at least a 1/p 2 fraction of z's appearances in H. We now have to reduce z to take on two distinct values a, b in order to apply Split, but these values need to be such that a ℓ1-ℓ0 ̸ = b ℓ1-ℓ0 . We show that there is a decision tree process (Lemma 22) that queries the variables underlying Q such that it is always possible to reduce z to the form (b -a)w * + a, where a, b are useful to separate the indices ℓ 1 , ℓ 0 . It is fairly easy to see as a result of the discussion so far that if we are able to apply Split on z with indices ℓ 1 , ℓ 0 at this stage, it causes a sizable reduction in H.
We are now almost ready to apply Split, but we still have to meet the requirement that the axioms are free of z. Since z is an extension variable it appears only in the extension axiom which has now been reduced to the form (b -a)w * + a, and so the only way to remove this axiom is to make a substitution for w * = (z -a)/(b -a) in terms of z. This would get rid of this extension axiom and take the Boolean axiom for w * to (z -a)(z -b) = 0 just like we need, but if w * appears in any of the other axioms this substitution just creates new copies of z. Therefore we need to remove w * from all the other axioms before we try to make this substitution. Here is where we make use of the structure of our tautology F SEL n,k by defining an operation Cleanup which can remove any Boolean variable w * from the axioms without actually setting it to a constant value. Cleanup also restores the structure of our tautology so that we are always working with a subset of equations and pigeons from F SEL n,k that are untouched by previous restrictions. We describe this operation in detail in Section 4.5.1.
Once we perform the above cleanup operations we are ready to make the substitution for w * = (z -a)/(b -a) in terms of z to satisfy the requirements for Split. We are met with a final hurdle here: this substitution can potentially increase the number of pairs of terms in H. Fortunately it can be resolved by a simple case analysis: if the blowup is too large it must have been the case that w * appeared frequently in H, and so setting it to zero will reduce H without the need for Split. Otherwise, Split is able to offset this blowup.
Therefore we have demonstrated above how to reduce the size of the high Quadratic degree set H by a constant fraction. Performing this for sufficiently many iterations would remove H entirely and lower the Quadratic degree of any refutation. We then use a generalized version of Sokolov's argument that low Quadratic degree implies low degree in order to switch to a low degree refutation. For a small sized refutation, the number of iterations needed is bounded and thus we are able to keep most of the pigeons and equations alive at the end. We then select a hard subset of equations by assigning all remaining pigeons, and expand any remaining extension variables in order to obtain a low degree refutation of these equations, towards a contradiction.
Let us fix the finite field F p , p > 2 for the rest of the article. We also fix a set of unsatisfiable polynomials F over Boolean variables x ∪ y, and a set of extension axioms Ext of the form z -Q over variables z. Whenever we refer to a refutation Π, we assume that it is a PC + Ext refutation of F ∪ Ext.
▶ Definition 10 (Support of a variable). Let z -Q(w i1 , . . . , w iκ ) = 0 be a κ-local extension axiom associated with z. We define the set vars(Q) = {w i1 , . . . , w iκ } and sometimes write vars(z) to denote vars(Q), the set of variables that z depends on. The support of z, supp(z) ⊆ [0, p -1], is equal to the set of all values a ∈ [0, p -1] such that there exists a Boolean assignment α to the variables of Q such that Q(α) = a. Sometimes we also indicate this by supp(Q).
We extend the definition of support also to Boolean variables. For a Boolean variable w, supp(w) = {0, 1} as enforced by the Boolean axiom w 2 = w.
Definition 11 (Singular and Nonsingular variables w.r.t. Ext). Let Ext be a set of extension axioms and let z be an extension variable with an axiom in Ext. We say that z is Singular C C C 2 0 2 3 7:10 Lower Bounds for Polynomial Calculus with Extension Variables over Finite Fields w.r.t. Ext iff 0 ∈ supp(z); otherwise we say that z is N onsingular w.r.t. Ext. Any Boolean variable is considered Singular by default, independent of the set Ext, since zero always belongs to its support. For a term t, let sing(t) be the subterm of t containing the Singular variables in t, and let nsing(t) be the subterm of t containing the Nonsingular variables.
Note that for a Singular extension variable z, it is possible to set z to zero, However, we note that this may falsify other polynomial equations in F . For example, if xy = 0 is a polynomial equation in F , and the extension axiom for z is z -1 + xy = 0, then setting x = y = 1 forces z = 0, but this falsifies xy = 0.
▶ Lemma 13. Let z be a Nonsingular extension variable with extension axiom z -Q = 0. Then the following polynomial equations are implied by (and therefore derivable from) the extension axiom for z plus the Boolean axioms for all variables in vars(Q), in degree at most
In particular, if z is Nonsingular, then the polynomial equation z p-1 -1 = 0 is implied by z -Q = 0 together with the Boolean axioms for vars(Q).
Proof. Let z -Q(w i1 , . . . , w iκ ) = 0 be the extension axiom for z, and let supp(z
. First, we can derive the multilinear version of Q, Q ′ , from Q together with the Boolean axoms w 2 -w = 0 for all w ∈ vars(Q). Secondly, by definition, supp(z) = A means that the allowable values for z over Boolean assignments to vars(Q) are the values in A. Therefore, z -Q = 0 together with the Boolean axioms w 2 -w = 0 for all w ∈ vars(Q) implies Π a∈A (z -a) = 0. Furthermore, this polynomial has a PC derivation, by the derivational completeness of PC. Since A ⊆ A ′ , Π a∈A ′ (z -a) = 0 is a weakening of Π a∈A (z -a) = 0 and is therefore derivable from Π a∈A (z = a) = 0. Lastly, we will argue that there exists some constant c ∈ F * p such that z ℓ(A) -c = 0 is semantically implied by z -Q = 0 plus the Boolean axioms for vars(z) and therefore is derivable from these axioms. Since the only allowable values for z under the Boolean axioms are the values in A, and since by definition of ℓ(A), for every a ∈ A, a ℓ(A) = c for some c ∈ F * p , it follows that z ℓ(A) -c = 0.
◀ ▶ Definition 14. For a term t and a variable w, deg(t, w) is equal to the degree of w in t. If w is N onsingular, then w p-1 = 1 mod p, so deg(t, w) < p -1. On the other hand if w is Singular then we have w p = w mod p and therefore deg(t, w) < p. For a term t the degree of t, deg(t), equals w∈vars(t) deg(t, w).
The next definition is a generalization/modification of Sokolov's definition of Quadratic degree for the more general scenario where the proof contains extension variables that are Singular as well as ones that are N onsingular.
▶ Definition 15 (Quadratic degree). Let V be a set of variables and let S be a subset of V . For a pair of terms t 1 , t 2 over V , and a variable w ∈ V , we define Qdeg S (t
1 , t 2 , w) as follows. If w ∈ S, then Qdeg S (t 1 , t 2 , w) = 1 if w occurs in at least one of t 1 or t 2 ; if w ̸ ∈ S, then Qdeg S (t 1 , t 2 , w) = 1 if and only if deg(t 1 , w) ̸ = deg(t 2 , w). The overall quadratic degree of the pair t 1 , t 2 , Qdeg S (t 1 , t 2 ), is equal to w∈V Qdeg S (t 1 , t 2 , w). The quadratic degree of a polynomial P is equal to the maximum quadratic degree over all pairs (t 1 , t 2 ) such that t 1 , t 2 ∈ P . For a proof Π, the quadratic degree of Π is the maximum quadratic degree over all polynomials P ∈ Π.
We usually instantiate the above definition with V = x ∪ y ∪ z and with S being the set of Singular variables as defined by the extension axioms corresponding to z. However since Qdeg S is a different measure for every S, and our set of Singular variables can change under the application of a restriction ρ to the variables in V , we must make sure that our measure of Quadratic degree does not change significantly under a restriction 2 . Fortunately, we can show that for any two sets S and T such that T ⊆ S, Qdeg T ≤ Qdeg S . Along with the simple observation that the set of Singular extension variables can only shrink under a restriction, this implies that our measure of Quadratic degree can only decrease under a restriction. We make this formal below.
▶ Lemma 16. Let V be a set of variables and let S and T be subsets of V such that T ⊆ S. Then for any two terms t 1 , t 2 over V , Qdeg T (t 1 , t 2 ) ≤ Qdeg S (t 1 , t 2 ).
Proof. Note that for a variable w ∈ S -T , Qdeg S (t 1 , t 2 , w) = 1 when w has a nonzero exponent in one of t 1 or t 2 , otherwise zero. However, Qdeg T (t 1 , t 2 , w) = 1 if and only if the previous condition is satisfied and the exponents of w in t 1 and t 2 are not equal. Thus the claim follows.
◀
Henceforth, when we refer to Quadratic degree, we always fix the set S to be the set of Singular variables w.r.t. the underlying extension axioms. We have the following important corollary that this measure always decreases under a restriction to the underlying variables.
▶ Corollary 17. Let F be a set of unsatisfiable polynomials over variables x ∪ y and let Ext be a set of extension axioms of the form z -Q(w i1 , . . . , w iκ ) for variables z ∈ z and w i1 , . . . , w iκ ∈ x ∪ y. Let ρ be a restriction to x ∪ y and let Ext| ρ be the axioms given by z -Q| ρ for each axiom z -Q ∈ Ext. The Quadratic degree w.r.
t. Ext| ρ is at most the Quadratic degree w.r.t. Ext. Proof. Since supp(Q| ρ ) ⊆ supp(Q) for any polynomial Q, we have that the set of Singular variables under Ext| ρ is a subset of those under Ext. Therefore our claim follows from the previous lemma. ◀ ▶ Lemma 18 (Quadratic degree upper bounds degree of Singular variables). For any term t, deg(sing(t)) ≤ pQdeg(t, t) Proof. For any Singular variable w, Qdeg(t, t, w) = 1 if and only if w occurs in t. Since w can occur in t with degree at most p -1, the claim follows. ◀ ▶ Definition 19 (High quadratic degree terms). For a proof Π and d ≥ 0, let H d (Π) denote the set of unordered pairs (t 1 , t 2 ) of quadratic degree at least d. That is, H d (Π) is the set of unordered pairs of terms (t 1 , t 2 ) such that t 1 , t 2 both occur in P for some polynomial P ∈ Π, and Qdeg(t 1 , t 2 ) ≥ d. Proof. Consider a polynomial P ∈ Π and a pair of terms (t 1 , t 2 ) that occur in P . For any variable w distinct from z, Qdeg(t 1 , t 2 , w) is unaltered when P is reduced by z ℓ(z) = c. On the other hand, if z does not contribute to the Quadratic degree of (t 1 , t 2 ) i.e. Qdeg(t 1 , t 2 , z) = 0, then it will still be 0 after reducing by z ℓ(z) = c. Therefore Qdeg(t 1 , t 2 ) never increases for any pair (t 1 , t 2 ) and thus
The following is a generalized version of the argument from [20] that shows how to convert a proof with low Quadratic degree to one with low degree.
▶ Lemma 21. Let F be a set of unsatisfiable polynomials of degree d 0 with a PC refutation of Quadratic degree at most d ≥ d 0 over F p . Then F has a PC refutation of degree at most 3pd.
Proof. The proof of this lemma is largely based on (a slightly cleaner version of) Sokolov's argument ( [20], Lemma 3.6) that low Quadratic degree over {±1} variables implies low degree. Our first observation is that Sokolov's argument can be applied to any refutation of low Quadratic degree over F p such that every term contains only Nonsingular variables. In particular if {P j } is a refutation that only contains Nonsingular terms, then we can use his argument to show that {t p-2 j P j } is also a valid refutation for some carefully chosen term t j ∈ P j . Moreover, the degree of the latter refutation is bounded by a constant times the Quadratic degree of the former one. To see this, first note that for two Nonsingular terms t 1 and t 2 , we have that deg(t
because of the following. For a variable z that is Nonsingular such that z occurs in t 1 and t 2 with deg(t 1 , z) = deg(t 2 , z), we have deg(t 1 t p-2 2
, z) = Qdeg(t 1 , t 2 , z) = 0 since it would appear in t 1 t p-2 2 with an exponent that is a multiple of p -1, and z p-1 = 1 holds for Nonsingular variables. Any other Nonsingular z that occurs in at least one of t 1 and t 2 has deg(t 1 t p-2 2 , z) < p -1 and Qdeg(t 1 , t 2 , z) = 1. Therefore the degree of t 1 t p-2 2 is at most p • Qdeg(t 1 , t 2 ) when t 1 and t 2 contain only Nonsingular variables. This implies that the lines in the new refutation {t p-2 j P j } have degree at most p times the Quadratic degree of the original refutation {P j }. Sokolov additionally showed that each line in the new refutation can be derived from previous lines without exceeding degree equal to 2p times the Quadratic degree of the original refutation, completing the argument.
In our case we deal with terms containing both Singular and Nonsingular variables. The above argument cannot be applied directly to our case, since it crucially depends on the fact that Nonsingular variables can be raised to the power p -1 to make them vanish. Fortunately by Lemma 18, the degree of Singular variables in any term is at most p times the Quadratic degree with itself. Given this bound, we can ignore for each term the part that contains Singular variables, and apply the above argument only with respect to the Nonsingular part of each term, to reduce the degree of Nonsingular variables in each term of the refutation. Since we now have a bound on the degree of both Singular and Nonsingular variables in each term, we have bounded its degree. We describe this in full technical detail below.
Let {P j } be a refutation of F with Quadratic degree bounded by d. For any term t recall that nsing(t) denotes the subterm of t containing only Nonsingular variables. Note that nsing(t) p-1 = 1 for any t. For every line P j in the refutation, we pick a term t j ∈ P j and define P ′ j = nsing(t j ) p-2 P j . Note that by the arguments outlined above, for any two terms t 1 and t 2 in P j , we have deg(nsing(t 1 ) p-2 nsing(t 2 )) ≤ pd and thus the degree of Nonsingular variables in any term of P ′ j is bounded by pd. Since the Singular variables in any term remain unchanged under multiplication by nsing(t j ) p-2 , the Singular degree of P ′ j the same as that of P j and is bounded by pd (Lemma 18) and therefore deg(P ′ j ) ≤ pd + pd = 2pd. We now show that the set {P ′ j } forms a valid refutation of F and each P ′ j can be derived from previous lines in degree 3pd. If P j is one of the axioms, we multiply by nsing(t j ) p-2 to get P ′ j for an arbitrary t j ∈ P j , and this takes degree pd 0 ≤ pd. If P j = wP j1 for j 1 < j and some variable w, we choose t j ∈ P j such that t j = wt j1 where t j1 ∈ P j1 was chosen earlier. If w is Singular, we have nsing(t j ) = nsing(t j1 ) and therefore P ′ j = nsing(t j ) p-2 P j = w • nsing(t j1 ) p-2 P j1 = wP ′ j1 . On the other hand, if w is Nonsingular, we have nsing(t j ) = w • nsing(t j1 ) and therefore P ′ j = nsing(t j ) p-2 P j = w p-1 • nsing(t j1 ) p-2 P j1 = P ′ j1 . Finally, let P j = P j1 + P j2 for j 1 , j 2 < j. We pick an arbitrary term t j ∈ P j . Note that since nsing(t) p-1 = 1 for any term t, P j1 = nsing(t j1 )P ′ j1 and P j2 = nsing(t j2 )P ′ j2 and thus we have
2 nsing(t j1 )P ′ j1 + nsing(t j ) p-2 nsing(t j2 )P ′ j2 for t j1 ∈ P j1 and t j2 ∈ P j2 chosen earlier. We now show that deg(nsing(t j ) p-2 nsing(t j1 )) ≤ pd and deg(nsing(t j ) p-2 nsing(t j2 )) ≤ pd to conclude the proof. Since every term in P j appears in one of P j1 , P j2 , let t j ∈ P j1 without loss of generality. Then we have that t j , t j1 both appear in P j1 and thus deg(nsing(t j ) p-2 nsing(t j1 )) ≤ pd. If t j2 ∈ P j i.e. it is not cancelled in the sum P j1 + P j2 , then we have t j , t j2 both appear in P j and hence deg(nsing(t j ) p-2 nsing(t j2 )) ≤ pd. If t j2 ̸ ∈ P j , this implies that it was cancelled in the sum P j1 + P j2 and therefore t j2 ∈ P j1 and deg(nsing(t j ) p-2 nsing(t j2 )) ≤ pd. ◀
In this section we will show how to apply a restriction and then use an operation Split (motivated by [20]) in order to eliminate high quadratic degree terms. Our main focus will be to handle the case where the variable to be set is an extension variable with extension axiom z -Q = 0 where z is N onsingular, since in the other case we can potentially just set z = 0 to eliminate terms. We start by showing how to apply a small Boolean restriction ρ such that Q| ρ is a simple linear function of just one variable. Proof. We will create a decision tree that will query vars(Q) one-by-one. Associated with the root r is the set of values S r = {a l | a ∈ supp(Q)}. That is, we label the root with the set of all possible values that z l can take on. Since l < ℓ(supp(z)), it follows that |S r | ≥ 2 (since otherwise we would have l = ℓ(supp(z))). At the root we query the first variable w 1 , with left edge labelled by w 1 = 0 and right edge labelled by w 1 = 1. Now we label the left vertex with the set {a l | a ∈ supp(Q| w1=0 )}, of all values that z l can take on under the restriction w 1 = 0. Similarly we label the right vertex with the set {a l | a ∈ supp(Q| w1=1 )}. We continue recursively, querying the next variable at each vertex v of the decision tree, as long as the set of allowable values for z l under the partial restriction ρ v associated with v is greater than one. Now consider the longest path, ξ in T . The partial restriction ρ associated with ξ sets the first k ′ variables, where k ′ ≥ 1 since initially z l takes on at least two values. Also since ξ is a complete path, the associated set {a l | a ∈ supp(Q| ρ )} contains exactly one element, call it q. C C C 2 0 2 3
Now consider the twin path ξ ′ with associated restriction ρ ′ , where ρ ′ is obtained from ρ by toggling the value of the last variable, w k ′ , queried. Again since ξ ′ is a complete path, the associated set {a l | a ∈ supp(Q| ρ ′ )} contains exactly one element, call it q ′ . Note that q, q ′ must be distinct.
Let δ be the following assignment to vars(Q) -w k ′ : for 1 ≤ j < k ′ , we set δ(w j ) = ρ(w j ) = ρ ′ (w j ), and for k ′ < j ≤ k, we set δ(w j ) = 0. Setting w * = w k ′ , Q| δ is a linear equation of the form (b -a)w * + a, where b, a ∈ supp(Q). Finally, by construction, a l ̸ = b l (since otherwise the two paths corresponding to ρ, ρ ′ would be the same). ◀
In the remainder of this subsection, we will be interested in the case where we want to eliminate some Nonsingular extension variable z from the refutation, and we have already applied the above Lemma so that the extension axiom for z is of the form z -((b-a)w+a) = 0, where w is some variable in x ∪ y. Thus, supp(z) = {a, b}. The next two Lemmas generalizes a similar argument due to Sokolov, and show how to remove Quadratic degree pairs of the form (t 1 z i , t 2 z j ) for a carefully chosen pair i, j from the refutation via the Split operation.
▶ Lemma 23. Let z be an extension variable such that supp(z) = {a, b}, where a ̸ = b and a, b ∈ F * p and let P be any polynomial. Then, for any two distinct numbers ℓ 0 , ℓ 1 where ℓ 0 < ℓ 1 and a ℓ1-ℓ0 ̸ = b ℓ1-ℓ0 , there exists a unique polynomial Proof. Let z -Q = 0 be the extension axiom for z, where supp(z) = {a, b}. Then by Lemma 13 the polynomial (z -a)(z -b) = 0 is implied by (and derivable from) the extension axiom for z plus the Boolean axioms. We can assume without loss of generality that P has the form P 0 + zP 1 + . . . + z p-2 P p-2 . Now we want to argue that there exists a polynomial R = z ℓ0 R 0 + z ℓ1 R 1 , where R 0 , R 1 are polynomials over vars(P ) -z, and such that R(a) = P (a), and R(b) = P (b). We can find R 0 and R 1 by solving the following system of equations, where we view R 0 , R 1 as the underlying variables, and treating P (a), P (b) as constants:
This has a (unique) solution since the determinant of the associated matrix is a ℓ0 a ℓ1 b ℓ0 b ℓ1 = a ℓ0 b ℓ0 (b ℓ1-ℓ0 -a ℓ1-ℓ0 ). By our assumption, this matrix is non-singular over F p and therefore the above system of equations has a unique solution over F p , given by:
Abbreviating a ℓ0 , a ℓ1 , b ℓ0 , b ℓ1 by a 0 , a 1 , b 0 , b 1 respectively, we have by definition of the inverse:
Solving for R 0 we have: R. Impagliazzo, S. Mouli, and T. Pitassi 7:15
for some constants c 0i ∈ F p . And similarly solving for R 1 , it has the following form:
for some constants c 1i ∈ F p . ◀ ▶ Definition 24 (Split). Let z be an extension variable with extension axiom z -
. For any polynomial P and for every ℓ 0 < ℓ 1 such that a ℓ1-ℓ0 ̸ = b ℓ1-ℓ0 , let R = R 0 z ℓ0 + R 1 z ℓ1 be the unique polynomial given by Lemma 23 such that R = P mod (z -a)(z -b). Then Split z,ℓ1,ℓ0 (P ) is defined to be the pair of polynomials {R 0 , R 1 }. For a proof Π, and an extension variable z such that supp(z) = {a, b}, we define Split z,ℓ0,ℓ1 (Π) to be the sequence of lines Split z,ℓ0,ℓ1 (P ), over all P ∈ Π.
▶ Lemma 25. Let Π be a refutation of a set of unsatisfiable polynomials F . Let z be a variable that occurs in Π such that the polynomials in F do not contain z except for the axiom (z -a)(z -b) = 0 for some a, b ∈ F * p . Then for any ℓ 0 , ℓ 1 such that ℓ 0 < ℓ 1 and a ℓ1-ℓ0 ̸ = b ℓ1-ℓ0 , Π ′ = Split z,ℓ0,ℓ1 (Π) forms a valid refutation of F modulo (z -a)(z -b) Proof. Fix an extension variable z in Π such that it does not occur in any axioms except (z -a)(z -b) = 0, and let ℓ 0 , ℓ 1 be such that ℓ 0 < ℓ 1 and a ℓ1-ℓ0 ̸ = b ℓ1-ℓ0 . We will show by induction on the number of lines in Π that Split z,ℓ0,ℓ1 (Π) is a valid derivation that meets the conditions of the lemma. For the base case, note that all of the axioms are either free of z or eliminated as a result of reducing by (z -a)(z -b), and hence their Split versions are derivable. Now suppose that the Lemma holds for the first j -1 lines of Π; that is, Split z,ℓ0,ℓ1 (Π j-1 ) is a valid derivation, where Π j-1 denotes the first j -1 lines of Π.
The first case is where P j is a linear combination of two previously derived lines, so P j = αP j1 +βP j2 for some j 1 and j 2 less than j and α, β ∈ F p . Using the inductive hypothesis, we have:
By the uniqueness of the polynomial R j = z ℓ0 R j0 + z ℓ1 R j1 that is equivalent to P j mod (z -a)(z -b) (by Lemma 23), this implies that R j0 = αR j10 + βR j20 and similarly R j1 = αR j11 + βR j21 , and thus R j0 can be derived from a linear combination of R j10 and R j20 and similarly for R j1 .
C C C 2 0 2 3
The second case is when P j is derived from a previously derived line P j ′ by multiplying P j ′ by a variable w. That is, P j = wP j ′ for some j ′ < j. If w ̸ = z, then we have that R j1 = wR j ′ 1 (similarly for R j0 ). If w = z then we have:
from which we need to derive
Thus, R j1 can be derived as a linear combination of R j ′ 1 and R j ′ 0 , and similarly for R j0 . ◀
The proof of our lower bound for the tautology
with extension axioms Ext proceeds by choosing a variable in the given refutation Π that contributes to a lot of high quadratic degree pairs of terms in Π. If this variable is Singular, we apply the restriction that sets it to zero. On the other hand, if it is Nonsingular and therefore an extension variable z, we first reduce it to depend on a single variable w * by applying a restriction chosen from Lemma 22, and then use a more complicated case analysis (see Lemma 30) in order to apply the Split operation from Lemmas 23 and 25 on z. In both of these cases we are able to remove a small fraction of high Quadratic degree terms, and thus after sufficiently many iterations we obtain a refutation of low Quadratic degree. We convert this to a refutation of low (usual) degree using Lemma 21, and then substitute for the pigeon variables y to select a subset of equations from F n,k that require high degree, obtaining a contradiction.
In order to get the contradiction at the end of the above argument, we need to ensure that our process above is always working with a subset of equations of F n,k that are untouched, i.e. unaffected by earlier restrictions to variables. We also need to eliminate any partially assigned pigeons so that we have full choice over the equations we are able to pick at the end. Additionally, a key requirement of the Split lemmas (Lemmas 23 and 25) is that the variable z we Split on must not appear in any axioms except for one of the form (z -a)(z -b) = 0, which indicates that it takes two distinct values. In particular, we cannot set z or the underlying variable w * described above in order to eliminate them from the refutation. This presents us with a unique requirement: for any choice of a variable w * ∈ x ∪ y, we need to be able to eliminate all axioms containing w * without actually setting it. We show how to perform these operations by making use of the structure of our tautology F SEL n,k . We first show how to "ban" an equation E b1...b log m from F n,k by switching to a set of axioms that prevent any pigeon from being assigned to b 1 . . . b log m . ▶ Lemma 26. Let Π be a refutation of F SEL n,k | ρ for some restriction ρ and let
0 be one of its axioms. Then there exists another valid refutation Π ′ with the latter axiom replaced by the axiom (y i ̸ = b 1 . . . b log m ) ≡ bj =1 y i,j bj =0 y i,j , such that the quadratic degree of Π ′ is at most that of Π.
..b log m = 0 can be derived from the axiom (y i ̸ = b 1 . . . b log m ) ≡ bj =1 y i,j bj =0 y i,j by multiplying by the polynomial E b1...b log m . Since this derivation involves only singular variables, the degree can never drop and therefore the quadratic degree of this derivation is at most that of the final polynomial. We construct Π ′ as follows. We first derive the former axiom from the latter in Π ′ . Besides this derivation, Π ′ involves the same steps as Π. ◀ ▶ Definition 27. An equation E b1...b log m is said to be banned when the previous lemma is applied repeatedly to eliminate all occurrences of it from the axioms.
along with axioms that ban some subset of equations of the form E b1...b log m .
We now describe how to perform the cleanup operations, which we collectively call Cleanup(ρ), that takes as input an "unclean" version of F SEL n,k derived by applying a restriction ρ to a clean version, and outputs another clean version that is in some sense a subset of the input. Suppose that we are given a restriction ρ that has been applied to a clean version of F SEL n,k , with a variable w * ∈ ρ possibly set to ⋆, indicating that it must remain unset. To eliminate an axiom that has been affected by a x variable in ρ not set to ⋆, we simply obtain the refutation that bans the corresponding equation E b1...b log m as described in the above lemma. Note that since we are eliminating the axiom without setting any variables in it, we can also do this in case our variable w * ∈ x. Suppose that y ij is a y variable in ρ not set to ⋆. We first note that any axiom that contained y ij before the application of ρ contains all the variables y i1 . . . y i log m corresponding to the i th pigeon y i . We first make sure that this i th pigeon does not contain our variable w * that must remain unset. If it doesn't, we proceed as follows. We set all the other variables in this pigeon to select some equation E b1...b log m that has not been banned. Such an equation exists provided that the number of banned equations so far is bounded, and the size of the restriction ρ is also bounded (we formalize this in the lemma below). We then apply an additional restriction to the x variables that satisfies this equation E b1...b log m picked above. We then ban all the equations affected by this additional restriction, like we did above for the part of ρ containing x variables. This eliminates the pigeon y i . We are left with the case where our variable w * belongs to some pigeon y j . We set all the variables in the pigeon y j except for w * , such that neither of the two equations E b1...b log m and E b ′ 1 ...b ′ log m that would be selected if w * is set to zero or one are banned (again, these exist under the same conditions as above). We then proceed as before, i.e. apply an additional restriction to satisfy both these equations, and then ban any other equations that have been affected by this additional restriction. With this we have eliminated the axioms of pigeon y j which select an equation, but we are still left with the axioms that prevent y j from colliding with any other pigeon, which are now of the form w * • (y
We note that the above cleanup operations over y variables terminate successfully only when there are enough equations that have not been banned by prior calls to cleanup, and also the size of the restriction ρ is bounded. We make this formal by the below lemma.
▶ Lemma 29 (Correctness of Cleanup(ρ)). Let ρ be a restriction of size κ. If the number of banned equations (from previous calls to Cleanup) is ≪ m/2 κ , then Cleanup(ρ) terminates correctly. Moreover, it bans at most O(κ) additional equations and removes at most O(κ) pigeons in its run.
Proof. In Cleanup(ρ), note that we can remove the axioms that contain x variables unconditionally. When we remove a pigeon y i = y i1 . . . y i log m , we rely on having an equation it can be set to that is not already banned. Since the size of ρ is bounded by κ, note that at most κ variables from y i1 . . . y i log m can be set by ρ. Therefore there are at least log m -κ of them unset, corresponding to selecting m/2 κ many equations. Since we assume that the number of banned equations is much less than this, we can always find one that is not banned to assign this pigeon to.
We now count the number of new equations banned and the number of pigeons removed by this call to Cleanup(ρ). Since each x variable appears in a constant number of equations, the number of equations we ban while processing it is a constant. When we process a y variable, we pick and satisfy an equation, and ban all other equations affected in the process. Since every equation also contains a constant number of variables, satisfying it affects only a constant number of other equations. Therefore, for every variable we process we ban only a constant number of equations, and thus the total number of equations banned is O(κ). We remove only those pigeons with a variable in ρ, so this is also bounded by O(κ). ◀
We need first the following key lemma that shows how to apply the Split operation to reduce high quadratic degree terms.
▶ Lemma 30. Let F be a system of unsatisfiable polynomials and let z be a nonsingular extension variable with the extension axiom z -Q. Let ℓ = ℓ(supp(Q)) so that z ℓ = c holds for some c ∈ F p . Let Π be a refutation of F ∪ {z -Q} modulo z ℓ = c such that for at least an ϵ fraction of pairs (t 1 , t 2 ) in H d (Π), Qdeg(t 1 , t 2 , z) = 1, for some d ≥ 0. Then there exists a refutation
Proof. We will apply a procedure as described by Algorithm 1 in order to modify the proof to satisfy the post-conditions of the Lemma. Here we give a detailed description of the algorithm, together with its correctness. Let H d (Π, z) be the set of all unordered pairs (t
1 , t 2 ) ∈ H d (Π) that z contributes to. That is, H d (Π, z) is the set of all unordered pairs (t 1 , t 2 ) ∈ H d (Π) such that Qdeg(t 1 , t 2 , z) = 1. There are many different ways that z can contribute to H d (Π, z): namely, for all i, j such that i < j < ℓ, let H d (Π, z, i, j) be the set of all unordered pairs (t 1 , t 2 ) ∈ H d (Π, z)
, such that the degree of z in t 1 is i and the degree of z in t 2 is j. Note that for any two pairs (i, j) and (i ′ , j ′ ) such that i ̸ = i ′ or j ̸ = j ′ , H d (Π, z, i, j) and H d (Π, z, i ′ , j ′ ) are disjoint. Therefore, there exists a "good" pair ℓ 0 < ℓ 1 < ℓ such that removing H d (Π, z, ℓ 1 , ℓ 0 ) from H d (Π, z) will remove at least a 1/p 2 fraction of H d (Π, z) and therefore a ϵ/p 2 fraction of pairs in
We want to apply the Split operation Split z,ℓ0,ℓ1 to remove all such pairs. But in order to do this we have to satisfy the preconditions of Lemmas 23 and 25: we need two values a, b such that a ℓ1-ℓ0 ̸ = b ℓ1-ℓ0 and all the axioms should be free of z except for (z -a)(z -b) = 0. The first step (Line 2 of 1) is to apply Lemma 22 with l = ℓ 1 -ℓ 0 . This gives us w * ∈ vars(Q), a, b ∈ supp(Q) and a partial restriction
where a ℓ1-ℓ0 ̸ = b ℓ1-ℓ0 mod p. Next, we apply the restriction δ to Π (Line 3). Now we have a simpler linear extension axiom for z of the form z -(b -a)w * -a = 0. Next we would like to make the substitution w * = (z -a)/(b -a) in Π in order to satisfy this extension axiom, towards the goal of eliminating z from the axioms so that we have the preconditions of Lemma 25 and therefore are able to apply Split z,ℓ1,ℓ0 . However, if w * appears in any of the axioms in F , this would create additional occurrences of z and we would not make any progress. Therefore, we have to make sure that none of the axioms of F contain w * . But we also cannot set w * to zero or one in an attempt to get rid of it, since this would set z to either a or b through the above extension axiom, and Split requires that z take on two distinct values. We thus have to get rid of all axioms mentioning w * either by setting other variables or by replacing these axioms with stronger versions, such that the former can be derived from the latter. This is what the subroutine Cleanup does, in addition to removing the axioms in F that were affected by our earlier restriction δ, so that we have a clean version of F SEL n,k as defined in the previous section. We are now ready to make the substitution w * = (z -a)/(b -a). Under this substitution, the Boolean axiom w * 2 -w = 0 reduces to (z -a)(z -b) = 0, and the original extension axiom for z disappears (since under this substitution it becomes 0 = 0.) Thus this substitution would satisfy all of the preconditions of Lemmas 23, 25. However, this substitution can create a new problem: it can cause a blow up in the size of H d (Π) since for every pair of terms (t 1 , t 2 ) such that one of them contains w * , we could have up to four new terms after the substitution. In order to deal with this potential blow up we do a simple case analysis: If w * contributes to at least an ϵ/4p 2 fraction of pairs (t 1 , t 2 ) in H d (Π), then we set w * = 0 (Lines 4-5). This gives us the required reduction in the size of H d (Π) (z is also set to a constant by setting w * = 0, but we don't care about that since we have obtained a reduction in high Quadratic degree terms without needing to use Split). Otherwise, the blowup caused by the substitution w * = (z -a)/(b -a) adds at most 3ϵ/4p 2 fraction of pairs to H d (Π), and C C C 2 0 2 3
Lower Bounds for Polynomial Calculus with Extension Variables over Finite Fields thus if we remove all pairs in H d (Π, z, ℓ 0 , ℓ 1 ) (after this blowup) then overall we will will have reduced the size of H d (Π) to (1 -ϵ/4p 2 )|H d (Π)|. So in this latter case, we apply the substitution mentioned above (Line 8) which simultaneously removes w * from all axioms, and replaces the linear axiom for z by (z -a)(z -b) = 0. Now all preconditions for Lemma 8 hold so we can apply Split z,ℓ0,ℓ1 (Line 9) to get a valid refutation. It is left to argue that this indeed removes the set H d (Π, z, ℓ 1 , ℓ 0 ). More precisely, we argue that high Quadratic degree pairs of terms in the refutation obtained after applying Split have a one to one mapping to the set H d (Π) -H d (Π, z, ℓ 1 , ℓ 0 ). Fix a line P ∈ Π. Since we are working modulo z ℓ = c, we can assume that P = P 0 + zP 1 + . . . z ℓ-1 P ℓ-1 . Let R = z ℓ0 R 0 + z ℓ1 R 1 be the unique polynomial equivalent to P mod (z -a)(z -b). Split z,ℓ0,ℓ1 (Π) is the refutation with lines R 1 , R 0 for all P ∈ Π. By the proof of Lemma 23 R 0 , R 1 have the form:
For a pair of terms (t i , t j ) in R 1 such that t i ∈ P i and t j ∈ P j and Qdeg(t i , t j ) ≥ d, we map it to the pair (t i z i , t j z j ) ∈ P , and similarly for R 0 . Clearly this is a one-one mapping, and since P ℓ0 does not occur in R 1 and P ℓ1 does not occur in R 0 , it is a mapping to H d (Π) -H d (Π, z, ℓ 1 , ℓ 0 ). Therefore we have that for the refutation with logarithm of its size less than γn 2 /(10 κ (M + n log n)), for a small enough constant γ. Given Π, Algorithm 2 (defined below) will apply a sequence of restrictions and cleanup steps in order to produce a refutation Π ′ of a clean version of F SEL n,k (see Definition 29) with the property that the Quadratic degree of Π ′ is at most d = νn/κ for a small enough constant ν > 0. The algorithm contains a while loop which iteratively removes all pairs of terms of high Quadratic degree. From Π ′ , we will apply a further restriction to all of the remaining unset y-variables (i.e. pigeons that select equations from F n,k ), to extract a refutation of a subset of m ′ equations from F n,k of low degree, contradicting the degree lower bound given in Lemma 35. Recall that F n,k is defined over variables x and we pick a subset of these equations by matching pigeons y i to equations in F n,k through a complete bipartite graph.
The algorithm first initializes a few things. Set d = νn/κ for a small enough constant ν > 0. Let M ′ = M + n log n, which upper bounds the total number of variables occurring in the refutation. Let S be the set of all variables that are Singular w.r.t. the current set of extension axioms. We initialize S to be the set of all variables x ∪ y ∪ z since this is the largest possible set we will be dealing with; this will be updated at every iteration of the while loop, although we note that it can only reduce as we apply restrictions. Henceforth when we refer to Quadratic degree, we mean Qdeg S . Finally, we initialize H to be the set of all pairs of terms in Π with Quadratic degree greater than d.
In the while loop, we first update the set S by checking which of the extension variables z have zero in their support according to their current extension axioms, and deleting those that don't. For each extension variable z that we delete from S, we reduce the refutation Π
Algorithm 2 Eliminating high Quadratic degree terms from the proof. Input: A refutation Π of F SEL n,k with extension axioms Ext Output: A refutation Π ′ with Quadratic degree less than d 1 d ← νn/κ, where ν is a sufficiently small constant. 2 M ′ ← M + n log(n). (M ′ upper bounds |x ∪ y ∪ z|, the total number of variables) 3 S ← x ∪ y ∪ z (the current set of singular variables: all Boolean variables are singular by default and we initialize all extension variables to also be singular. This could possibly reduce in each iteration.) 4 H ← {(t 1 , t 2 ) | t 1 , t 2 ∈ Π and Qdeg S (t 1 , t 2 ) ≥ d} (the set of all pairs of terms of large Quadratic degree according to S) 5 while H is non empty do 6 for every extension axiom z -Q ∈ Ext do 7 if 0 ̸ ∈ supp(Q) then 8 S ← S -{z} 9 Compute c such that z ℓ(z) = c and reduce Π by the latter identity 10 end 11 end 12 H ← {(t 1 , t 2 ) | t 1 , t 2 ∈ Π and Qdeg S (t 1 , t 2 ) ≥ d} (update H to reflect changes due to the above for loop) 13 Pick a variable w that, by an averaging argument, occurs in at least an ϵ fraction of terms in H, where we choose ϵ = d/M ′ . 14 if w ∈ S then 15 Let σ be a restriction on x ∪ y such that w| σ = 0 16 Π ← Π| σ 17 Cleanup(σ) 18 end 19 else 20 Apply Algorithm 1, which by Lemma 30 satisfies the post-conditions of Lemma 30 21 end 22 end by z ℓ(z) = c. Such an identity exists and is derivable by Lemma 13, and does not increase the size of H by Lemma 20. Once we have updated S, we recompute the set of high Quadratic degree pairs H with respect to the updated set S. This also does not increase the size of H, by Lemma 16. We then pick a variable w that contributes to the Quadratic degree of at least a d/M ′ fraction of pairs in H by averaging.
There are two cases depending on whether w ∈ S or not. In the first case (lines 14-18), w is Singular so we apply the restriction σ such that w| σ = 0 and call Cleanup(σ) to restore to a clean version of our tautology. This eliminates the contribution to high Quadratic degree from terms containing w, and hence obtains a (1 -d/M ′ )-factor reduction in the size of H. In the second case (lines 19-34), w is Nonsingular so we apply Algorithm 1, which uses the Split operation non-trivially to reduce the size of H. Lemma 30 proves correctness of the algorithm, and thus upon termination of one call to Algorithm 1, we have obtained a (1 -d/(4p 2 M ′ ))-factor reduction in the number of high Quadratic degree terms.
Repeating the above forlog |H|/ log(1 -d/4p 2 M ′ ) ≈ 4p 2 M ′ log |H|/d ≤ O(γ)κn/10 κ iterations, we eliminate all terms in H from the proof and thus obtain a refutation of Quadratic degree less than d. Since we call Cleanup once per iteration, and in each call it C C C 2 0 2 3 bans at most O(κ) many equations and removes at most O(κ) many pigeons (by Lemma 29), we have banned at most O(γ)κ 2 n/10 κ equations and removed at most those many pigeons in total. Therefore, we always satisfy the invariant that the number of banned equations is much less than m/2 κ (where m = 10n), satisfying the required conditions for correctness of Cleanup from Lemma 29.
Let Π ′ denote the modified proof upon termination of Algorithm 2. Note that out of the m ′ = (1 -ϵ)m pigeons, there are at least a 1 -O(γ) fraction of pigeons still alive (i.e. not removed by Cleanup) and a 1 -O(γ) fraction of the m equations not banned. We now substitute for the remaining pigeons y so that we select a subset of at least (1 -2ϵ)m unsatisfiable equations from F n,k that are not banned and obtain a refutation of them of Quadratic degree at most d (assuming γ is small enough). By Lemma 21, we can obtain a refutation of these equations of degree at most 3pd. Now, for all surviving extension variables we substitute them with their definitions in terms of the variables x. Note that since each extension variable is a degree κ polynomial this raises the degree to at most 3κpd. Since d = νn/κ, for sufficiently small ν we end up with a refutation of (1 -2ϵ) equations from F n,k of degree less than c 2 n, contradicting Lemma 35. ◀
We will prove Theorem 9, which we state again here for convenience.
▶ Theorem 32 (Theorem 9). Let m = 10n. Then there exists constants k > 0, 0 < ϵ < 1 such that for sufficiently large n, there exists k-CSP formulas {F n,k } with m k-local constraints such that for m ′ = (1 -ϵ)m, every subset of m ′ constraints is unsatisfiable and requires linear degree PC refutations.
First we'll show that a random regular bipartite graph has good boundary expansion. This has been used implicitly in other works ([9], [5]), but for completeness we state and prove it here. Let G = (L, R, E) be a bipartite graph, and let A ⊆ R. The boundary for A, ∂(A), is the set of vertices x in L so that |N (x) ∩ A| = 1, i.e., vertices with a unique neighbor in A. If not, there are sets A ⊂ R and B ⊂ L so that N (A) ⊆ B and |B| = 3k|A|/4. We will bound the probability that this is true for fixed sets A, B and then take a union bound. We can view picking a random (d, k) bipartite graph as picking a random matching between d half-edges adjacent to each x ∈ L and k such half-edges adjacent to each y ∈ R; if a half edge for x is matched to a half-edge for y, it forms an edge between x and y.
We can form this matching by going through the half edges for nodes in R and for each randomly selecting an unmatched half-edge for some node in L. We start with the edges for A in an arbitrary order. If we condition on all previous neighbors for A being in B, the number of half-edges left still available for B is less than d|B|, whereas the number for B stays at exactly d(n -|B|). Thus, the conditional probability that the next edge formed is also in B is at most |B|/n, and we do this for each of k|A| edges, meaning the probability that all neighbors are in B is at most (|B|/n) k|A| . Now, for a fixed |A| and setting |B| = 3k|A|/4, we take the union bound over all subsets A and B. This gives a total probability of failure for some set A of size a as : m a n 3ka/4 (3ka/4n) ka ≤ (em/a) a (4en/3ka) 3ka/4 (3ka/4n) ka ≤ (em/a) a (e 3 ka/n) ka/4 = (ekn/da) a (e 3 ka/n) ka/4 = (e 3k/4+1 a k/4-1 k k/4+1 /dn k/4-1 ) a
Since we are assuming a < n/(e 6 k 2 ), the base in the above expression is at most
The probability that a set of (1 -ϵ)10n random parities (i.e. for a random choice of b) is satisfiable is at most 2 -9n for a small enough ϵ. The probability that any such subset of F n,k is satisfiable is therefore at most 2 (-n(9-10H(ϵ))) , which is exponentially small for a small enough ϵ (where H(ϵ) is the binary entropy function). b) This follows directly from [1], Theorem 3.8 and Theorem 4.4, since by Theorem 33 the bipartite graph underlying the system of parity equations A has good boundary expansion with high probability. ◀