LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-27

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.

Quantifier polynomials agree with QBF semantics on Boolean assignments

Statement

Let $F$ be a field, let $φ (x, y_{1}, \dots, y_{m})$ be a quantifier-free Boolean formula on the variables $x, y_{1}, \dots, y_{m}$ with $m \geq 0$ , and let $P : = P_{φ} \in F [X, Y_{1}, \dots, Y_{m}]$ be its arithmetization. Then for every Boolean assignment $a \in {0, 1}^{m}$ to $y_{1}, \dots, y_{m}$ the two operators of Field arithmetization of QBF quantifiers satisfy $(A_{X} P) (a) = the truth value of \forall x φ (x, a), (E_{X} P) (a) = the truth value of \exists x φ (x, a),$ where Boolean truth values are embedded in $F$ as $0$ and $1$ .

Facts & Assumptions

Given: A field $F$ , a quantifier-free Boolean formula $φ (x, y_{1}, \dots, y_{m})$ with $m \geq 0$ , its arithmetization $P = P_{φ}$ , and a Boolean assignment $a$ to $y_{1}, \dots, y_{m}$ .

[A1]

Arithmetization replaces $\neg$ by $1 - P_{ψ}$ , $\land$ by $P_{ψ} P_{θ}$ , and $\lor$ by $P_{ψ} + P_{θ} - P_{ψ} P_{θ}$ , and the Boolean value of a formula is obtained from the usual truth tables, with false and true identified with the field elements $0$ and $1$ (Arithmetization of Boolean formulas).

[L1]

For every Boolean assignment $z$ to $x, y_{1}, \dots, y_{m}$ , the arithmetization $P_{φ} (z)$ equals the Boolean value of $φ$ at $z$ , embedded as $0$ or $1$ in $F$ (Arithmetization preserves Boolean values).

[L2]

The operators are $A_{X} P = (P ∣_{X = 0}) (P ∣_{X = 1})$ and $E_{X} P = 1 - (1 - P ∣_{X = 0}) (1 - P ∣_{X = 1})$ , evaluated at the remaining variables (Field arithmetization of QBF quantifiers).

Proof

technique · direct

1.1

On the four bit pairs $(u, v) = (0, 0), (0, 1), (1, 0), (1, 1)$ the product $u v$ takes the values $0, 0, 0, 1$ , and the expression $u + v - u v$ takes the values $0, 1, 1, 1$ . These are exactly the truth tables of the conjunction and the disjunction of two bits, and the computations are polynomial identities valid in every field, including fields of characteristic two.

A1algebra

1.2

Let $b$ denote $0$ or $1$ . By [L1] the value $P ∣_{X = b} (a) = P_{φ} (b, a)$ is the Boolean value of the formula $φ (b, a)$ at the assignment $a$ , hence an element of ${0, 1} \subset F$ . This includes the case $m = 0$ , where $a$ is the empty assignment and $φ$ has no free variable besides $x$ , and the case in which $φ$ is a constant formula.

L1given

2.1

Put $u : = P ∣_{X = 0} (a)$ and $v : = P ∣_{X = 1} (a)$ . By step 1.2 both are bits. Hence by [L2] $(A_{X} P) (a) = u v, (E_{X} P) (a) = u + v - u v .$ By step 1.1 the first value is $1$ exactly when both $φ (0, a)$ and $φ (1, a)$ are true, which is the truth value of $\forall x φ (x, a)$ , and the second is $1$ exactly when at least one of the two is true, which is the truth value of $\exists x φ (x, a)$ . Both operator values are therefore themselves bits.

step 1.1step 1.2L2algebra

3.1

Consequently $A_{X}$ and $E_{X}$ , evaluated at any Boolean assignment to the remaining variables, return the truth values of the corresponding quantifications of the arithmetized subformula.

step 2.1∎

Depends on

Used by

Dependency tree · two levels

6 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: A Modern Approach, §8.5, author-hosted draft (standard reference, not scraped)
A. Shen, IP = PSPACE: Simplified Proof, JACM 39(4) 1992, pp. 878–880 (standard reference, not scraped)