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.

Shamir verifier runs in polynomial time

Statement

Let an input $Φ$ be a closed prenex quantified Boolean formula on $n$ variables whose matrix has $L$ syntax nodes, let $ℓ$ be the input length, and let $T = n (n + 3) / 2$ , $D = \max {L, 2}$ , $N = \max {2, 12 T D + 1}$ and $p < 2 N$ be the parameters of the Shamir protocol of The Shamir interactive protocol for TQBF. Then the verifier of that protocol:

uses $p = 3$ when $T = 0$ and otherwise performs the deterministic prime search of A polynomial-size prime field meets the soundness budget in $O (N^{2} \log^{2} N)$ bit operations; it rejects a malformed input immediately;
runs at most $T$ rounds, in each of which it performs $O (D)$ field operations on the received message and, only if that round passes, reads one block of $2 ⌈ \log_{2} p ⌉$ fresh random bits; if all round checks pass, it then evaluates the matrix arithmetization at one point in $O (L)$ field operations;
consequently runs in worst-case time $O ⁣ (N^{2} \log^{2} N + (T D + L) \log^{2} p)$ bit operations, which is polynomial in $ℓ$ , and uses at most $2 T ⌈ \log_{2} p ⌉$ random bits.

The verifier is therefore a probabilistic polynomial-time machine in the sense of Interactive-proof transcripts, rounds, and prover strategies: a fixed deterministic procedure whose running time on every input and every random tape is bounded by a polynomial in the input length.

Facts & Assumptions

Given: A closed prenex quantified Boolean formula $Φ$ with $n$ variables and a matrix of $L$ syntax nodes, and the protocol of The Shamir interactive protocol for TQBF.

[A1]

On input that is not a well-formed closed prenex formula the verifier rejects immediately; otherwise it runs at most $T$ rounds, checks the format and the identity of each received list, draws one challenge block of $k = 2 ⌈ \log_{2} p ⌉$ bits per passed round, and, if no round rejects, finishes with the evaluation of $b$ at the current point; the prime $p$ depends on the input alone, being $3$ for $T = 0$ and otherwise found by the deterministic search of A polynomial-size prime field meets the soundness budget (The Shamir interactive protocol for TQBF).

[A2]

The protocol has at most $T$ messages, each with at most $D + 1$ entries; the verifier reads at most $2 T ⌈ \log_{2} p ⌉$ random bits; per round it performs $O (D)$ field operations, and the terminal evaluation costs $O (L)$ field operations (Explicit communication, round, and evaluation bounds).

[A3]

For $T \geq 1$ , the deterministic search for $p$ performs at most $N^{2}$ trial divisions and $O (N^{2} \log^{2} N)$ bit operations, and $p = O (T D)$ with $⌈ \log_{2} p ⌉ = O (\log (T D))$ (A polynomial-size prime field meets the soundness budget). For $T = 0$ the protocol sets $N = 2$ and $p = 3$ directly. In both cases $⌈ \log_{2} p ⌉ = O (\log (T D + 2))$ , and every field operation on residues of $Z / p$ costs $O (\log^{2} p)$ bit operations.

[L1]

A probabilistic polynomial-time verifier is a deterministic machine with a read-only random tape whose computation time is bounded by a polynomial in the input length on every input and every random tape (Interactive-proof transcripts, rounds, and prover strategies).

Proof technique: direct calculation.

Proof

1.1

The verifier first parses the input and, if the input is malformed, rejects; otherwise it uses $p = 3$ when $T = 0$ , and when $T \geq 1$ it runs the deterministic search for $p$ , which by [A3] uses at most $N^{2}$ trial divisions and $O (N^{2} \log^{2} N)$ bit operations. The direct $T = 0$ choice also fits this bound.

A1A3given

1.2

Fix a round and a received message. Format checking inspects at most $D + 1$ coefficients; evaluating the message at $0$ and at $1$ costs $O (D)$ field operations, and the identity test then costs a constant number of field operations. If the check passes, drawing the challenge block costs one read of $k = 2 ⌈ \log_{2} p ⌉$ bits and one reduction modulo $p$ , and the update evaluates $s$ at the challenge, again $O (D)$ field operations. So each round costs $O (D)$ field operations and at most $k$ random bits.

A1A2A3algebra

2.1

There are at most $T$ rounds, so the rounds cost $O (T D)$ field operations and at most $T k = 2 T ⌈ \log_{2} p ⌉$ random bits in total; no step of the verifier loops unboundedly, since the round count and the message-length caps are fixed functions of the input.

step 1.2A1A2algebra

3.1

If the terminal step is reached, the verifier evaluates $b$ at one point of $F^{n}$ , which costs $O (L)$ field operations by [A2]; together with step 2.1 the field-operation count of the whole run is $O (T D + L)$ , which by [A3] is $O ((T D + L) \log^{2} p)$ bit operations.

step 2.1A2A3algebra

4.1

Adding the search cost of step 1.1 gives the bound $O (N^{2} \log^{2} N + (T D + L) \log^{2} p)$ claimed in item 3; here $T = n (n + 3) / 2$ , $n \leq ℓ$ , $L \leq ℓ$ , $D = \max {L, 2}$ and $p < 2 N$ . When $T \geq 1$ , $N = 12 T D + 1$ and hence $2 N = 24 T D + 2$ ; when $T = 0$ , $N = 2$ and the protocol directly sets $p = 3 < 4 = 2 N$ . Thus $N$ and $p$ are polynomially bounded in $ℓ$ , so the displayed bit bound is polynomial in $ℓ$ . The verifier is a deterministic machine with an explicit polynomial bound on its steps for every input and every random tape, so by [L1] it is a probabilistic polynomial-time machine, as claimed.

step 1.1step 3.1A1A3L1algebra∎

Depends on

Used by

TQBF has a polynomial-round interactive proof Theorem

Dependency tree · two levels

15 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.3 and Remark 8.19, author-hosted draft (standard reference, not scraped)
A. Shen, IP = PSPACE: Simplified Proof, JACM 39(4) 1992, pp. 878–880 (standard reference, not scraped)