LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-09-12

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 reuse keeps the reachability formulas polynomial in size

Statement

Fix the configuration length $m$ and assume that the one-step predicate $Next (U, V)$ from The quantified formula expressing reachability between two configurations has size $O (m)$ . Then there is a constant $c > 0$ such that the formula $Θ_{i} (U, V)$ has size at most $c m (i + 1)$ for every $i \in N$ . In particular, if $m$ itself is polynomial in the input length and $i = O (m)$ , then $Θ_{i}$ has polynomial size.

Facts & Assumptions

Given: the recursive formulas $Θ_{i} (U, V)$ for a fixed bit-length $m$ , with $Next (U, V)$ of size $O (m)$ .

[L1]

By definition, $Θ_{0} (U, V) = {Eq}_{m} (U, V) \lor Next (U, V)$ , where both summands have size $O (m)$ , while $Θ_{i}$ for $i \geq 1$ adds one midpoint block, one selector bit, two comparison blocks, and a single recursive copy of $Θ_{i - 1}$ (The quantified formula expressing reachability between two configurations).

Proof

technique · induction

1.1

By [L1], the base formula $Θ_{0} (U, V)$ has size $O (m)$ .

L1base

1.2

For $i \geq 1$ , [L1] shows that $Θ_{i}$ contains exactly one copy of $Θ_{i - 1}$ plus only $O (m)$ new symbols coming from the variables $W, b, Y, Z$ , the two equality tests, and the Boolean guards for $b = 0$ and $b = 1$ . So if $s_{i}$ denotes the size of $Θ_{i}$ , then $s_{i} \leq s_{i - 1} + c m$ for some constant $c$ .

L1ihalgebra

2.1

Starting from the $O (m)$ base bound in step 1.1 and iterating the recurrence from step 1.2 gives $s_{i} \leq c m (i + 1)$ for a suitable constant $c$ . If $m$ is polynomial in the input length and $i = O (m)$ , this bound is polynomial.

step 1.1step 1.2discharge-induction∎

Depends on

The quantified formula expressing reachability between two configurations

Used by

TQBF is PSPACE-complete Theorem

Dependency tree · two levels

2 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

Sanjeev Arora and Boaz Barak, Computational Complexity: A Modern Approach (standard reference, not scraped)