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.

A false field claim becomes true in one round with bounded probability

Statement

Let $Φ$ be a closed prenex quantified Boolean formula, with $n$ variables and the parameters $D$ and $p$ of its Shamir protocol, and let an arbitrary prover run against the verifier of The Shamir interactive protocol for TQBF. Fix a round $t \in {1, \dots, T}$ and condition on a reached prefix of positive probability whose current point $σ_{t}$ assigns a value to every variable of the stage polynomial $G_{t}$ and whose current claim satisfies $c_{t} \neq G_{t} (σ_{t})$ . Suppose the round- $t$ message $s$ is a legal list of degree at most $D$ that passes the round's check. Then the probability, over the fresh challenge $r_{t}$ that the verifier draws after the message is fixed, that the updated claim equals the true predecessor value is at most $2 D / p$ ; here the true predecessor value at the challenge $r$ is $q^{*} (r)$ , where $q^{*}$ is the restriction of $G_{t - 1}$ to $σ_{t}$ in the active variable of the round.

Facts & Assumptions

Given: A closed prenex quantified Boolean formula $Φ$ , its Shamir protocol, an arbitrary prover, a round index $t$ , a reached prefix with $c_{t} \neq G_{t} (σ_{t})$ , and a legal message $s$ passing the round's check.

[A1]

In the round with node $M = N_{t}$ and active variable $x_{i}$ the verifier tests $c = s (0) s (1)$ for a universal node, $c = s (0) + s (1) - s (0) s (1)$ for an existential node, and $c = (1 - a) s (0) + a s (1)$ with $a = σ_{t} (i)$ for a reduction; then it reads a fresh challenge block, sets $σ_{t - 1} (i) = r_{t}$ , $σ_{t - 1} (k) = σ_{t} (k)$ for $k \neq i$ and $c_{t - 1} = s (r_{t})$ , and the challenge is drawn only after the message is fixed. The honest (true) round polynomial is the restriction of $G_{t - 1}$ to the current point in the active variable (The Shamir interactive protocol for TQBF).

[A2]

Every node polynomial of the operator list, after substituting arbitrary field elements for all variables other than its active variable, has degree at most $D = \max {L, 2}$ in that active variable; in particular $q^{*}$ has degree at most $D$ (Multilinearization preserves Boolean values and bounds individual degree).

[A3]

The verifier's challenge is the integer value of a block of $2 ⌈ \log_{2} p ⌉$ uniform bits reduced modulo $p$ , and this sampler gives every residue of $F$ probability at most $2 / p$ (A polynomial-size prime field meets the soundness budget).

[A4]

The operators of the arithmetization are $A_{X_{i}} P = (P ∣_{X_{i} = 0}) (P ∣_{X_{i} = 1})$ , $E_{X_{i}} P = 1 - (1 - P ∣_{X_{i} = 0}) (1 - P ∣_{X_{i} = 1})$ (Field arithmetization of QBF quantifiers) and $R_{X_{i}} P = (1 - X_{i}) (P ∣_{X_{i} = 0}) + X_{i} (P ∣_{X_{i} = 1})$ (Multilinearization in one variable).

[A5]

At a reached round in block $j$ , the reverse schedule has already sampled every variable in the input polynomial's block prefix except the active variable: before $O_{j}$ these are $x_{1}, \dots, x_{j - 1}$ , and before a reduction $R_{X_{i}}$ the preceding quantifier and reduction rounds have assigned the other variables among $x_{1}, \dots, x_{j}$ (Multilinearization in one variable, The Shamir interactive protocol for TQBF).

[L1]

A nonzero polynomial of degree at most $D$ over a field has at most $D$ distinct roots in that field (A nonzero polynomial of degree $n$ over an integral domain has at most $n$ distinct roots).

Proof

technique · direct calculation

1.1

By [A5], the restriction $q^{*}$ of $G_{t - 1}$ to the current point in the active variable is well defined. Let $M = N_{t}$ be the round's node. By [A4] the true value of the current stage at $σ_{t}$ is $q^{*} (0) q^{*} (1)$ when $M$ is a universal node and $1 - (1 - q^{*} (0)) (1 - q^{*} (1))$ , equivalently $q^{*} (0) + q^{*} (1) - q^{*} (0) q^{*} (1)$ , when $M$ is an existential node. If $M$ is the reduction $R_{X_{i}}$ , put $a = σ_{t} (i)$ ; this value is defined in that case because the protocol rejects a reduction round with undefined $σ_{t} (i)$ , and the stage value is $(1 - a) q^{*} (0) + a q^{*} (1)$ . In each case the round's check is the same expression evaluated at $s (0), s (1)$ , using $a$ only in the reduction case.

A1A4A5givenalgebra

1.2

The polynomial $q^{*}$ has degree at most $D$ by [A2], and the received message $s$ has degree at most $D$ by hypothesis; both are univariate polynomials over $F$ .

A2given

2.1

If $s = q^{*}$ as polynomials, then the value the check computed, namely $c_{t}$ , would equal the expression of step 1.1 with $q^{*}$ in place of $s$ , which is $G_{t} (σ_{t})$ ; this contradicts the hypothesis $c_{t} \neq G_{t} (σ_{t})$ . Hence $s \neq q^{*}$ .

step 1.1given

2.2

By step 1.2 the difference $s - q^{*}$ is a nonzero polynomial of degree at most $D$ ; by [L1] it has at most $D$ distinct roots in $F$ .

step 1.2L1

2.3

The updated claim is $s (r_{t})$ and the true value of the updated stage is $q^{*} (r_{t})$ , because $G_{t - 1}$ agrees with $q^{*}$ in the active variable and $σ_{t - 1}$ differs from $σ_{t}$ only there. So the updated claim equals the true value exactly when $r_{t}$ is a root of $s - q^{*}$ .

A1step 1.1algebra

3.1

The challenge $r_{t}$ is drawn after the message is fixed and puts probability at most $2 / p$ on each residue by [A3], so the probability that it lies in the root set of $s - q^{*}$ , a set of at most $D$ residues, is at most $2 D / p$ . Averaging over any randomization of the prover's message preserves the bound, since the verifier's fresh bits are independent of the message; when $2 D / p \geq 1$ the bound is trivially true.

step 2.2step 2.3A3algebra∎

Depends on

Used by

Total TQBF soundness by the first repaired claim Lemma

Dependency tree · two levels

21 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

A. Shen, IP = PSPACE: Simplified Proof, JACM 39(4) 1992, pp. 878–880 (standard reference, not scraped)
Arora and Barak, Computational Complexity: A Modern Approach, §8.5.3 and Remark 8.19, author-hosted draft (standard reference, not scraped)