LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 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.

The ordered arithmetization evaluates to the quantified Boolean truth value

Statement

Let $F$ be a field, let $Φ = Q_{1} x_{1} \dots Q_{n} x_{n} ψ$ be a closed prenex quantified Boolean formula with quantifier-free matrix $ψ$ (Quantified Boolean formulas and the language TQBF), let $b = P_{ψ}$ be its matrix arithmetization (Arithmetization of Boolean formulas), and let $P^{(n)} = b, P^{(n - 1)}, \dots, P^{(0)}$ be the multilinearized ordered arithmetization of $Φ$ (Multilinearization in one variable). For $0 \leq j \leq n$ put $Ψ_{j} : = Q_{j + 1} x_{j + 1} \dots Q_{n} x_{n} ψ,$ so that $Ψ_{n} = ψ$ and $Ψ_{0} = Φ$ , and $Ψ_{j}$ has free variables $x_{1}, \dots, x_{j}$ . Then for every $j$ and every Boolean assignment $a \in {0, 1}^{j}$ , $P^{(j)} (a) = the Boolean value of Ψ_{j} at a,$ the truth values being embedded in $F$ as $0$ and $1$ . In particular $P^{(0)}$ , a constant, is the truth value of $Φ$ .

Facts & Assumptions

Given: A field $F$ and a closed prenex quantified Boolean formula $Φ = Q_{1} x_{1} \dots Q_{n} x_{n} ψ$ .

[A1]

The polynomials $P^{(j)}$ and $M_{j}$ are the stages of the multilinearized ordered arithmetization: $P^{(n)} = b$ , $M_{j}$ is obtained from $P^{(j)}$ by the reductions $R_{X_{1}}, \dots, R_{X_{j}}$ , and $P^{(j - 1)} = O_{j} (M_{j})$ (Multilinearization in one variable).

[A2]

The subformulas $Ψ_{j}$ are given by $Ψ_{n} = ψ$ and $Ψ_{j - 1} = Q_{j} x_{j} Ψ_{j}$ ; their Boolean values are defined by the usual recursive semantics (Quantified Boolean formulas and the language TQBF).

[L1]

$R_{X_{i}} P$ agrees with $P$ at $X_{i} = 0$ and $X_{i} = 1$ , and leaves the other variables' degrees no larger; in particular, if $P$ agrees with a function at all Boolean points of the cube, then so does $R_{X_{i}} P$ (Multilinearization preserves Boolean values and bounds individual degree).

[L2]

The matrix arithmetization agrees with the Boolean value of $ψ$ at every Boolean assignment (Arithmetization preserves Boolean values).

[L3]

For every polynomial $P$ , 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})$ (Field arithmetization of QBF quantifiers).

Proof

technique · induction

1.1

Base case $j = n$ : by [A1] and [A2], $P^{(n)} = b = P_{ψ}$ and $Ψ_{n} = ψ$ ; by [L2] the two agree at every Boolean assignment to $x_{1}, \dots, x_{n}$ , including the assignment-free case $n = 0$ .

L2A1A2givenbase

1.2

Induction hypothesis: suppose $1 \leq j \leq n$ and $P^{(j)}$ agrees with $Ψ_{j}$ at every point of the cube ${0, 1}^{j}$ .

2.1

Under the hypothesis of step 1.2, $M_{j}$ is obtained from $P^{(j)}$ by the reductions $R_{X_{1}}, \dots, R_{X_{j}}$ , each of which preserves agreement on Boolean points by [L1]; hence $M_{j}$ also agrees with $Ψ_{j}$ on ${0, 1}^{j}$ . In particular, for every $a \in {0, 1}^{j - 1}$ and each $b \in {0, 1}$ , the specialized value $M_{j} ∣_{X_{j} = b} (a)$ is the Boolean value of $Ψ_{j} (a, b)$ , and the two values are the two bits whose universal and existential quantification define the truth values of $Ψ_{j - 1} (a) = Q_{j} x_{j} Ψ_{j}$ .

step 1.2L1A1A2

3.1

Fix a Boolean assignment $a$ to the remaining variables and put $u = M_{j} ∣_{X_{j} = 0} (a)$ and $v = M_{j} ∣_{X_{j} = 1} (a)$ . Both are bits by step 2.1. By [L3], the universal operator returns $u v$ and the existential operator returns $1 - (1 - u) (1 - v)$ . On the four pairs $(u, v) = (0, 0), (0, 1), (1, 0), (1, 1)$ these expressions give, respectively, $(0, 0, 0, 1)$ and $(0, 1, 1, 1)$ in every field. Thus they compute conjunction and disjunction, precisely the semantics of $Q_{j}$ in [A2]. Since $P^{(j - 1)} = O_{j} (M_{j})$ by [A1], it agrees with $Ψ_{j - 1}$ at every Boolean $a$ .

step 2.1L3A1A2algebra

4.1

Step 1.1 supplies the base case and step 3.1 the induction step, so agreement holds at every index $j = n, n - 1, \dots, 0$ . For $j = 0$ the cube ${0, 1}^{0}$ has the single empty assignment and $Ψ_{0} = Φ$ , so the constant $P^{(0)}$ is the truth value of $Φ$ ; the case $n = 0$ is the base case itself.

step 1.1step 1.2step 3.1discharge-induction∎

Depends on

Used by

Dependency tree · two levels

11 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)