New Bounds for the Ideal Proof System in Positive Characteristic

Amik Raj Behera; Nutan Limaye; Srikanth Srinivasan; Varun Ramanathan

REVIEW 1 major objections 5 minor 2 references

New Bounds for the Ideal Proof System in Positive Characteristic

T0 review · 1 major / 5 minor · reviewed 2026-08-15 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read For large fields of any positive characteristic, several restricted algebraic proof systems remain exponentially weak on simple sparse polynomials, while constant-depth IPS refutes those same instances efficiently.

desk verdict Solid large-field positive-characteristic transfer of known IPS lower bounds, with a new degree lemma and useful upper bounds; the constant-depth transfer is the one part I'd want checked. read the letter →

arxiv 2506.16397 v1 pith:H2L3JYDW submitted 2025-06-19 cs.CC cs.LOmath.LO

Amik Raj Behera , Nutan Limaye , Varun Ramanathan , Srikanth Srinivasan This is my paper · ORCID

classification cs.CCcs.LOmath.LO

keywords idealproofsystemalgebraiccomplexitypositivecharacteristicfunctionallowerboundsconstant-depthcircuitsmultilinearformulasread-onceobliviousbranchingprogramsNullstellensatzcertificate

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper tries to show that lower bounds previously known for restricted fragments of the Ideal Proof System (IPS) over characteristic zero survive for fields of any positive characteristic, provided the field is large: size $n^{\omega(1)}$. It claims that sparse-IPSLIN1, read-once oblivious branching program IPSLIN1, multilinear-formula IPSLIN1, and multilinear constant-depth IPSLIN1 all require exponential or superpolynomial refutation size for explicit sparse polynomials that are themselves easy to compute. The same hard instances admit polynomial-size constant-depth IPSLIN refutations, and every unsatisfiable multilinear symmetric system is refutable in constant depth with polynomial size. This matters because restricted IPS systems are the main current route toward lower bounds for $AC^0[p]$-Frege, and the paper removes the characteristic-zero restriction that previously blocked that route.

What carries the argument

The load-bearing mechanism is Lemma 2.2, a tight degree lower bound for the multilinear inverse of a random linear form; it replaces the characteristic-zero component in the functional lower bound framework of the prior papers. The framework reduces every restricted IPS refutation to computing $1/f$ on the Boolean cube. On the upper-bound side, the mechanism is the Freshman's Dream identity $(a+b)^p = a^p + b^p$: repeatedly raising the linear constraint $\sum \alpha_i x_i - \beta$ to $p$-th powers expresses the $p^k$-powered version as a multiple of the original modulo the Boolean axioms, and choosing $\beta$ outside the coefficient field makes the difference between the $p^k$-powered and original linear forms a nonzero constant. That difference directly writes $1$ as a polynomial combination with constant-depth coefficient circuits.

What would settle it

For $n=3$, set $S = \mathbb{F}_8$ and $F' = \mathbb{F}_{64}$, fix any $\beta \in \mathbb{F}_{64} \setminus \mathbb{F}_8$, and enumerate all $8^3 = 512$ coefficient vectors $\alpha \in S^3$. For each, compute the unique multilinear polynomial agreeing with $1/(\sum_{i=1}^3 \alpha_i x_i - \beta)$ on the Boolean cube. If fewer than 64 of the 512 polynomials have full degree 3, Lemma 2.2's probability bound is violated and the lower-bound arguments collapse.

Watch

Extended reading notes

Core claim

The central discovery is a degree lower bound for the reciprocal of a random linear form over a large field. Let $F$ be a strict subfield of $F'$, fix $\beta \in F' \setminus F$, and choose $\alpha = (\alpha_1,\dots,\alpha_n) \in F^n$ uniformly from a finite set $S \subseteq F$. With probability at least $1 - (2^n-1)/|S|$, the unique multilinear polynomial that agrees with $1/(\sum_{i=1}^n \alpha_i x_i - \beta)$ on the Boolean cube has full degree $n$. The proof exhibits a numerator monomial with coefficient $1$, so the bound cannot be killed by the characteristic. Substituting this lemma for the older characteristic-zero degree bound, the paper feeds the functional lower bound method of the earlier work: a $C$-IPSLIN1 refutation forces the coefficient polynomial to compute the reciprocal on the Boolean cube, so any lower bound on computing that function becomes a refutation-size lower bound. The same degree lemma also supplies the constant-depth multilinear case, where the field needs only $2^{O((\log n)^2)}$ size.

Load-bearing premise

The lower-bound proofs require the coefficient field to be at least $2^{2n}$ (or $2^{O((\log n)^2)}$ for the constant-depth case) so the union bound over all restrictions succeeds; for small finite fields the same argument guarantees no hard coefficient vector.

Editorial extensions

If this is right

Sparse-IPSLIN1 refutations of $\sum_{i=1}^n \alpha_i x_i - \beta$ require size $2^{\Omega(n)}$ when the coefficient field has size $2^{\Omega(n)}$.
Fixed-order roABP-IPSLIN1 refutations of $\sum_{i=1}^n \alpha_i x_i y_i - \beta$ require width $2^{\Omega(n)}$.
Any-order roABP-IPSLIN1 and multilinear-formula-IPSLIN1 refutations of $\sum_{i<j} \alpha_{i,j} z_{i,j} x_i x_j - \beta$ require size $2^{\Omega(n)}$ and $n^{\Omega(\log n)}$ respectively.
Multilinear constant-depth IPSLIN1 refutations of the degree-four subset-sum instance $\sum_{i<j<k<\ell} \alpha_{i,j,k,\ell} z_{i,j,k,\ell} x_i x_j x_k x_\ell - \beta$ require size $n^{\omega(1)}$.
The same instances have $\mathrm{poly}(n,p)$-size constant-depth IPSLIN refutations of degree $O(k p D)$, so the multilinearity and the restricted models are both doing essential work.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

If Lemma 2.2 were extended to fields of size $O(n)$ instead of $2^{\Omega(n)}$, every lower bound in this paper would transfer to small finite fields; the field-size condition is the explicit bottleneck in the paper.
The constant-depth refutation of all symmetric multilinear systems suggests symmetry is a structural source of short algebraic proofs in every characteristic; a natural test is whether the $O(m^2 n^5 \log n)$ bound can be improved to near-linear in the number of terms.
Because the lower bounds target IPSLIN1 while the upper bounds are non-multilinear IPSLIN, the gap isolates multilinearity as the source of hardness; a next step would be to prove lower bounds against multilinear constant-depth IPS without the linear-in-$y$ restriction.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Colleague,

Here's my read on Behera et al. The paper does what it says: it takes the FSTW21/GHT22 IPS lower-bound framework and extends it to positive characteristic, at the price of requiring large fields (|F| = n^{ω(1)}). The core new ingredient is Lemma 2.2, a degree lower bound for the multilinear inverse of a random linear form over any characteristic. The proof via the numerator polynomial and Claim 2.3 is explicit and I checked the key step: the top monomial coefficient is 1, so it survives p-torsion. The accompanying union-bound Lemma 2.4 is straightforward and correct.

Given that lemma, the sparse, roABP, and multilinear-formula lower bounds go through by plugging into the known machinery. Those sections are solid, and the fact that the hard instances are easy to compute (sparse, roABP-computable, multilinear-formula-computable) is a genuine improvement over HLT24. The upper bounds — constant-depth IPSLIN refutations for sparse polynomials with β outside the field, the degree O(kp) Nullstellensatz certificate for linear forms, and the symmetric-instance refutation — are new and nicely complement the lower bounds. Theorem 1.11 looks like the most self-contained result.

The soft spot is Theorem 1.6, the constant-depth multilinear IPSLIN1 lower bound. Section 2.5 says that after swapping in Forbes' theorem and Lemma 2.14, 'the rest of the proof of [GHT22] works out verbatim.' That is an assertion, not a demonstration. GHT22's rank lemma (Lemma 2.13) uses the degree lower bound in a way that the paper sketches, but I cannot fully verify from this text that every step in that proof is characteristic-free. The paper's own summary says the only char-0 uses were [LST21] and the degree lower bound; if that is accurate, the transfer works. But because the proof is not reproduced, a hidden p-torsion issue in the rank lemma cannot be ruled out. If one exists, the constant-depth result would be unproven rather than false; the other lower bounds stand on their own.

The field-size requirement is explicit and honest. It is a real limitation, not a flaw: the authors acknowledge small finite fields need different hard instances, and concurrent work covers that case. The citation pattern is proper — Forbes, FSTW21, GHT22 are given credit, and the relation to EGLT25 is stated.

Bottom line: this deserves a serious referee. I would accept it with the request that Section 2.5 be expanded or that the authors provide a fuller proof of the constant-depth transfer. The rest of the paper is in good shape. I'd bring it to reading group and would cite it if I worked on algebraic proof complexity.

Referee Report

1 major / 5 minor

Summary. The paper studies the Ideal Proof System (IPS) over fields of positive characteristic, extending earlier characteristic-0 results of Forbes--Shpilka--Tzameret--Wigderson (FSTW21) and Govindasamy--Hakonomi--Tzameret (GHT22). The main lower bounds state that, for fields of size n^{ω(1)} (or larger), several restricted IPS fragments—sparse-IPSLIN1, roABP-IPSLIN1, multilinear-formula-IPSLIN1, and multilinear constant-depth IPSLIN1—require exponential or superpolynomial refutation size for explicitly given sparse polynomials that are easy to compute. The central technical lemma, Lemma 2.2, proves that for a random linear form Σ α_i x_i with coefficients in a proper subfield F and β outside F, the unique multilinear polynomial that agrees with 1/(Σ α_i x_i - β) on the Boolean cube has full degree n with high probability, with no restriction on the characteristic. The lower-bound proofs plug this degree lower bound into the functional lower-bound machinery of FSTW21 and GHT22, replacing characteristic-0-dependent steps. The paper also proves upper bounds: every sparse polynomial f - β with β outside the coefficient field has a constant-depth IPSLIN refutation of degree O(kpD); every unsatisfiable degree-1 polynomial over F_{p^k} has an IPSLIN refutation of degree O(kp); and every multilinear symmetric system has a constant-depth IPSLIN refutation of size O(m^2 n^5 log n). The large-field requirement is explicitly stated and discussed.

Significance. If the results hold, they extend a substantial body of algebraic proof-complexity lower bounds from characteristic 0 to arbitrary characteristic, providing a further step toward the long-standing open problem of AC0[p]-Frege lower bounds, which is a stated motivation. The hard instances are themselves easy to compute—sparse and of low degree—which is a strength relative to some prior constructions whose hard instances were not efficiently computable. The paper gives a self-contained proof of the central degree lower bound (Lemma 2.2 with Claim 2.3) and provides explicit, detailed constructions for the upper bounds. The bounded-depth symmetric-system upper bound and the non-multilinear upper bounds also shed light on the role of multilinearity in IPS. The main caveat is that the constant-depth lower bound (Theorem 1.6) is obtained by asserting that a published characteristic-0 proof adapts verbatim, rather than by reproducing the adaptation; this is the softest spot in the paper.

major comments (1)

[Section 2.5, Theorem 2.15] Section 2.5: The transfer of the constant-depth lower bound from [GHT22] is the least self-contained part of the paper. The authors claim the proof works verbatim after replacing the degree lower bound and the [LST21] result by [For24], but they do not demonstrate that Lemma 2.13's proof has no hidden characteristic-0 assumption. This is a significant gap in a main theorem.

minor comments (5)

[Section 2.1, Claim 2.3] Claim 2.3 is the crux of the main degree lower bound but is proved only via a proof sketch. Please expand it into a complete, self-contained proof, since the uniqueness of the monomial selection is essential for the lemma.
[Section 4, Claim 4.4] In the proof of Claim 4.4, the statement that the system of Q_t constraints implies "for each coordinate i, b_i ≤ n_i" is false. For example, with p=2, n=4, b=3 (so b_1=1 > n_1=0) the Q_t constraints are still satisfied. The intended conclusion k≤n can be obtained directly by taking t=k when k>n; please correct this step.
[Section 4, Claim 4.2] In the proof of Claim 4.2, the product expressing e_d(a) as a function of e_{p^i}(a) should run over i=0,...,ℓ (including e_1), not i=1,...,ℓ as written. The current indexing omits the p^0 digit.
[Theorem 1.8] The stated size bound "poly(s,p)" in Theorem 1.8 is not supported by the proof, which yields circuits of size O(k(s+p)+sD). Please restate the theorem with the correct bound, or explicitly restrict to instances of constant degree, since the size of the refutation may legitimately depend on the degree of the sparse polynomial.
[Section 1.3.2, Remark 1.10] Remark 1.10 refers to "polypn,pq-sized" refutations from Theorem 1.8, while the theorem statement says "size polyps,pq"; please align the two statements.

Circularity Check

0 steps flagged · score 2.0 of 10

No circular derivation: the degree lower bound is proved in-paper, hard instances are unsat by construction rather than by fit, and the external lower bounds used are independent; only an asserted char-p transfer in Section 2.5 is a correctness caveat, not a circularity.

full rationale

I find no circular step in the derivation chain. The central new ingredient, Lemma 2.2, is proved from first principles: Claim 2.3 exhibits a monomial with coefficient 1 in the numerator of the reciprocal's top Fourier coefficient, so the full-degree conclusion holds over any characteristic. The hard instances' unsatisfiability is baked in by choosing beta outside the coefficient field (e.g. Theorems 1.3-1.6 and Remark 1.7); this is an input design choice, not a fitted parameter renamed as a prediction. The lifting arguments rely on external, independently published results: FSTW21's sparsity lemma (Prop 2.5), Nisan's roABP characterization and Raz-Yehudayoff's multilinear-formula rank theorem (Thm 2.9), Forbes's Corollary 27 (Thm 2.12), and GHT22's rank lemma (Lemma 2.13). None of these are derived from the present paper's conclusions. The only self-citation with author overlap is [LST21] (Limaye and Srinivasan), but it is not load-bearing: the characteristic-independent replacement is Forbes's [For24], whose authors do not overlap with this paper, and the new degree bound supplies the remaining ingredient. Section 2.5's statement 'the rest of the proof of [GHT22] works out verbatim' is asserted rather than demonstrated; any hidden char-p obstruction in GHT22's Lemma 2.13 would be a correctness gap in Theorem 1.6, not a circular reduction. Theorems 1.3-1.5 are self-contained modulo external lower bounds and are not circular. Score 2 reflects the one minor self-citation and the unverified transfer assertion; neither makes the central claim circular.

Assumptions & free parameters 0 free parameters · 9 assumptions · 0 invented entities

The paper's proofs rely on standard algebraic facts and on previously published circuit lower bounds. No new free parameters are fit to data, and no new mathematical entities are introduced. The main new ingredient is a degree lower bound for inverses of linear forms over arbitrary characteristics.

assumptions (9)

standard math Hilbert's Nullstellensatz over arbitrary fields
Used in Section 4 to produce low-variate Nullstellensatz certificates for unsatisfiable systems over algebraically closed fields; the paper notes certificates can be solved via linear systems over F.
standard math Polynomial Identity Lemma (Schwartz-Zippel over arbitrary fields)
Used in Lemma 2.2 to bound the probability that the rational function numerator N(α) vanishes for random α from S^n.
standard math Freshman's Dream in characteristic p
Used in Claim 3.2 and in Theorem 1.9 to raise linear forms to p-th powers termwise.
standard math Ben-Or's polynomial-size constant-depth circuits for elementary symmetric polynomials
Used in Lemma 4.11 and Theorem 1.11 to construct depth-5 circuits for products of elementary symmetric polynomials; requires |F| > n.
standard math Raz-Yehudayoff multilinear formula size lower bound
Used in Theorem 2.10 to turn coefficient dimension lower bounds into size lower bounds for multilinear formulas.
standard math Forbes's constant-depth set-multilinear projection theorem [For24, Corollary 27]
Used in Section 2.5 to extend LST21/GHT22 lower bounds from characteristic zero to arbitrary fields.
standard math Nisan's coefficient dimension characterization of roABP width
Used in Appendix A.1 to equate roABP width with maximum coefficient dimension.
standard math Lucas's Theorem for binomial coefficients modulo p
Used in Claim 4.2 to show symmetric functions over the Boolean cube in positive characteristic depend only on O(log n) elementary symmetric polynomials.
standard math Fundamental Theorem of Symmetric Polynomials
Used in Section 4 to represent symmetric polynomials as polynomials in elementary symmetric polynomials.

how reviews work

0 comments

Cite this review

Pith. "Pith review of New Bounds for the Ideal Proof System in Positive Characteristic." pith.science (2026). https://pith.science/paper/H2L3JYDW

@misc{pith2026250616397,
  author       = {Pith},
  title        = {Pith review of: New Bounds for the Ideal Proof System in Positive Characteristic},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/H2L3JYDW}},
  note         = {Machine review of arXiv:2506.16397}
}

abstract

In this work, we prove upper and lower bounds over fields of positive characteristics for several fragments of the Ideal Proof System (IPS), an algebraic proof system introduced by Grochow and Pitassi (J. ACM 2018). Our results extend the works of Forbes, Shpilka, Tzameret, and Wigderson (Theory of Computing 2021) and also of Govindasamy, Hakoniemi, and Tzameret (FOCS 2022). These works primarily focused on proof systems over fields of characteristic $0$, and we are able to extend these results to positive characteristic. The question of proving general IPS lower bounds over positive characteristic is motivated by the important question of proving $AC^{0}[p]$-Frege lower bounds. This connection was observed by Grochow and Pitassi (J. ACM 2018). Additional motivation comes from recent developments in algebraic complexity theory due to Forbes (CCC 2024) who showed how to extend previous lower bounds over characteristic $0$ to positive characteristic. In our work, we adapt the functional lower bound method of Forbes et al. (Theory of Computing 2021) to prove exponential-size lower bounds for various subsystems of IPS. Additionally, we derive upper bounds for the instances presented above. We show that they have efficient constant-depth IPS refutations. We also show that constant-depth IPS can efficiently refute a general class of instances, namely all symmetric instances, thereby further uncovering the strength of these algebraic proofs in positive characteristic. Notably, our lower bounds hold for fields of arbitrary characteristic but require the field size to be $n^{\omega(1)}$. In a concurrent work, Elbaz, Govindasamy, Lu, and Tzameret have shown lower bounds against restricted classes of IPS over finite fields of any size by considering different hard instances.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

2 extracted references · 1 canonical work pages

[207]

Lower bounds on the size of bounded depth circuits over a complete basis with logical addition

issn: 1016-3328. doi: 10.1007/s00037-009-0270-8 (cit. on p. 20). [Raz87] Alexander A. Razborov. “Lower bounds on the size of bounded depth circuits over a complete basis with logical addition”. In:Mathematical notes of the Academy of Sciences of the USSR41 (1987), pp. 333–338.url: https://api.semanticscholar. org/CorpusID:121744639 (cit. on p. 5). [Raz98]...

doi:10.1007/s00037-009-0270-8 1987
[3454]

Linear Gaps between Degrees for the Polynomial Calculus Modulo Distinct Primes

doi: 10.1145/3689957 . url: https://doi.org/10.1145/3689957 (cit. on p. 6). [BGIP01] Sam Buss, Dima Grigoriev, Russell Impagliazzo, and Toniann Pitassi. “Linear Gaps between Degrees for the Polynomial Calculus Modulo Distinct Primes”. In:Journal of Computer and System Sciences62.2 (2001), pp. 267–289. issn: 0022-0000. doi: https://doi.org/10.1006/jcss.200...

work page arXiv 2001

Pith tools

Reviewed August 15, 2026 · model on record in the stance chip above.

[1] [207]

Lower bounds on the size of bounded depth circuits over a complete basis with logical addition

issn: 1016-3328. doi: 10.1007/s00037-009-0270-8 (cit. on p. 20). [Raz87] Alexander A. Razborov. “Lower bounds on the size of bounded depth circuits over a complete basis with logical addition”. In:Mathematical notes of the Academy of Sciences of the USSR41 (1987), pp. 333–338.url: https://api.semanticscholar. org/CorpusID:121744639 (cit. on p. 5). [Raz98]...

doi:10.1007/s00037-009-0270-8 1987

[2] [3454]

Linear Gaps between Degrees for the Polynomial Calculus Modulo Distinct Primes

doi: 10.1145/3689957 . url: https://doi.org/10.1145/3689957 (cit. on p. 6). [BGIP01] Sam Buss, Dima Grigoriev, Russell Impagliazzo, and Toniann Pitassi. “Linear Gaps between Degrees for the Polynomial Calculus Modulo Distinct Primes”. In:Journal of Computer and System Sciences62.2 (2001), pp. 267–289. issn: 0022-0000. doi: https://doi.org/10.1006/jcss.200...

work page arXiv 2001