LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Degree under Boolean elimination operators

Statement

Let $p \in F [X_{1}, \dots, X_{n}]$ , with $n \geq 1$ , and eliminate variable $X_{i}$ . Write $p_{b} = p ∣_{X_{i} = b}$ for $b = 0, 1$ . If $\deg_{X_{j}} p \leq d_{j}$ for $j \neq i$ , with nonnegative upper bounds including zero polynomials, then $p_{0} + p_{1}$ has bound $d_{j}$ , while $p_{0} p_{1}$ and $p_{0} + p_{1} - p_{0} p_{1}$ have bound $2 d_{j}$ .

If $p$ is Boolean-valued on the Boolean cube, the latter two operators represent universal and existential quantification there, respectively. The sum operator adds the two field values; it is not a Boolean OR operator over arbitrary fields. Repeated product elimination can produce exponentially growing degrees.

Facts & Assumptions

Given: The objects and hypotheses in the statement above.

[F1]

The Boolean AND and OR arithmetizations are uv and u+v-uv (Arithmetization of Boolean formulas).

Proof

1.1

Substituting $0$ or $1$ for $X_{i}$ does not increase any exponent in another variable. Addition preserves the maximum of the remaining bounds and multiplication adds them. Thus the sum has bound $d_{j}$ and both expressions containing a product have bound $2 d_{j}$ , including when a restriction vanishes or $d_{j} = 0$ .

givenalgebra

1.2

At any remaining Boolean assignment, put $u = p_{0}$ and $v = p_{1}$ ; by hypothesis $u, v \in {0, 1}$ . The AND and OR gate formulas give $u v$ and $u + v - u v$ as the universal and existential truth values. The sum instead gives $2$ when both inputs are one: in characteristic two this is zero, and in other characteristics it is not one. When $n = 1$ , these are simply operations on two constants.

F1algebra

2.1

Actual exponential growth is possible: start with $p = Y$ and eliminate $k$ other variables absent from $p$ using the product operator. Each elimination squares the current polynomial, leaving the formal polynomial $Y^{2^{k}}$ . Hence degree growth is not merely a loose bound.

step 1.1algebra∎

Depends on

Arithmetization of Boolean formulas

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

3 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Arora and Barak, Computational Complexity, January 2007 web draft, §8.5.1 p.158 and §8.5.3 opening degree-growth paragraph p.160 (standard reference, not scraped)