TheoremStatement: 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.

TQBF has a polynomial-round interactive proof

Statement

$T Q B F \in I P$ : the language of true closed prenex quantified Boolean formulas has a public-coin interactive proof with perfect completeness and soundness error at most $1 / 3$ , in which the verifier is a probabilistic polynomial-time machine and the number of rounds and the communicated bits are bounded by polynomials in the input length. Concretely, on input $Φ$ the verifier runs the Shamir protocol of The Shamir interactive protocol for TQBF for $Φ$ with the following public-coin message convention: after a passed round check it sends the full fresh block $U_{t} \in {0, 1}^{2 ⌈ \log_{2} p ⌉}$ instead of just its residue $r_{t}$ , and both parties compute $r_{t} = U_{t} m o d p$ ; the honest prover is accepted with probability $1$ when $Φ \in T Q B F$ , and no prover is accepted with probability more than $1 / 3$ when $Φ \notin T Q B F$ , including malformed inputs.

Facts & Assumptions

Given: The language TQBF of true closed prenex quantified Boolean formulas under a fixed effective encoding.

[A1]

The class $I P$ consists of the languages having an interactive protocol with a probabilistic polynomial-time verifier, polynomially bounded rounds and communication, completeness at least $2 / 3$ and soundness at most $1 / 3$ (The class IP).

[A2]

On every true input the honest prover of the Shamir protocol is accepted with probability one (Shamir protocol has perfect completeness).

[A3]

On every false input the acceptance probability of every prover is at most $2 T D / p < 1 / 6 < 1 / 3$ (Total TQBF soundness by the first repaired claim).

[A4]

The verifier is a probabilistic polynomial-time machine; it rejects malformed inputs immediately, parses it otherwise, and its running time, randomness consumption and communication are polynomial in the input length (Shamir verifier runs in polynomial time).

[A5]

The protocol has at most $T = O (n^{2})$ rounds with one message per round, each message of at most $D + 1$ field elements of $O (\log (T D + 2))$ bits, and its verifier state updates and tests use each sampled block only through its residue (Explicit communication, round, and evaluation bounds, The Shamir interactive protocol for TQBF).

Proof technique: direct.

Proof

1.1

By [A4] the verifier runs in polynomial time and, by [A5], the interaction has polynomially many rounds and messages of polynomial total length; in the variant specified in the statement each verifier message is its full fresh random block, and these blocks are all its coins. Thus this variant is public-coin. It sends at most $2 T ⌈ \log_{2} p ⌉$ verifier bits and at most $T (D + 1) ⌈ \log_{2} p ⌉$ prover bits; computing the same residues leaves the verifier time polynomial.

A4A5given

1.2

If $Φ \in T Q B F$ then $Φ$ is true and the honest prover computes each residue from the revealed block and otherwise uses the original strategy. On every random tape the messages and verifier state coincide with the original run, so [A2] gives acceptance with probability one, so completeness is $1 \geq 2 / 3$ .

A2given

1.3

For any prover in the public-coin variant, construct a randomized prover in the residue-message protocol as follows. Upon receiving $r_{t}$ , independently sample a uniformly distributed block from the nonempty finite set ${U \in {0, 1}^{k} : U m o d p = r_{t}}$ , and give this block to the simulated prover. Conditional on $r_{t}$ , this is exactly the distribution of the verifier's real block; the verifier uses no other information from that block. Induction over reached rounds therefore gives the same joint law of prover messages, residues and acceptance in the two protocols. The simulation uses no future verifier coins, so it is an allowed randomized strategy in [A3]. Thus on a well-formed false input [A3] gives acceptance probability at most $2 T D / p < 1 / 3$ also in the public-coin variant. Malformed inputs reject immediately by [A4].

A3A4A5given

2.1

Steps 1.1, 1.2 and 1.3 verify every clause of the definition of $I P$ in [A1] for the language TQBF: a probabilistic polynomial-time verifier, polynomially bounded interaction, completeness at least $2 / 3$ and soundness at most $1 / 3$ ; hence $T Q B F \in I P$ , which is the statement.

step 1.1step 1.2step 1.3A1∎

Depends on

Used by

Perfect completeness through a TQBF reduction Example
PSPACE is contained in IP Theorem

Dependency tree · two levels

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