LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07

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.

Ph circuit matrix final block encoding

Statement

For a fixed polynomial-time Boolean predicate $R (x, y)$ , and a polynomial bound on $∣ y ∣$ in $∣ x ∣$ , one can construct in time polynomial in $∣ x ∣$ formulas $F_{\exists} (x; y, z)$ in 3CNF and $F_{\forall} (x; y, z)$ in 3DNF such that, for every allowed $y$ , $R (x, y) ⟺ \exists z F_{\exists} (x; y, z) ⟺ \forall z F_{\forall} (x; y, z) .$ Here clauses or terms have at most three literals. Both formula length and $∣ z ∣$ are polynomially bounded.

When the allowed strings have varying lengths at most a fixed bound $p (∣ x ∣)$ , the formula's $y$ -block is a fixed-width encoding: a $⌈ \log_{2} (p (∣ x ∣) + 1) ⌉$ -bit length field followed by $p (∣ x ∣)$ payload bits. A length field outside ${0, \dots, p (∣ x ∣)}$ decodes to the empty string, and otherwise the decoder returns the indicated initial payload segment. Thus every fixed-width string decodes to an allowed $y$ , every allowed $y$ has an encoding, and $R (x, y)$ in the display means $R$ applied to that decoded string. For a prescribed exact length, use the identity encoding.

Facts & Assumptions

Given: the objects and hypotheses in the statement above.

[F1]

For every fixed deterministic Turing machine $M$ that halts in polynomial time, there is a polynomial-size logspace-uniform Boolean circuit family $(C_{n})$ such that $C_{n} (x) = 1$ exactly when $M$ accepts $x \in {0, 1}^{n}$ . (Polynomial-time computations have logspace-uniform circuit families).

[F2]

A Boolean circuit on $n$ inputs is a finite directed acyclic graph with inputs $x_{1}, \dots, x_{n}$ , constants $0$ and $1$ , and NOT, AND, and OR gates; AND and OR have fan-in two, while NOT has fan-in one. One node is designated as the output. The circuit's value is the value at that node after evaluating the graph in topological order. Its size is its number of non-input gates, and its depth is the largest number of non-input gates on a directed path ending at the output (a path may begin at an input or a constant). If two fixed finite bounded-arity bases can simulate every gate (and every constant) of one another by fixed finite circuits, then changing between them costs only constant factors in size and depth. In particular this holds for any two such functionally complete bases with simulable constants. No such claim is made for an arbitrary finite basis that may fail to express one of the Boolean operations. (Boolean circuits: basis, fan-in, size, and depth).

Proof

1.1

Compile the fixed machine that first applies the stated total decoder and then evaluates $R$ at the exact encoded-pair length determined by $∣ x ∣$ and the fixed bound; then fix the bits of $x$ . The decoder is polynomial-time and never changes $R$ by silently padding its argument. A halting logspace uniformity procedure on polynomial-length gate indices has polynomially many configurations and hence runs in polynomial time; enumerating the polynomially many gates therefore takes polynomial time. Use the NOT, binary AND/OR and constant basis.

F1F2

2.1

Introduce a variable for every gate output. For $z = a \land b$ , use $(\neg z \lor a) \land (\neg z \lor b) \land (z \lor \neg a \lor \neg b)$ ; for $z = a \lor b$ , use $(z \lor \neg a) \land (z \lor \neg b) \land (\neg z \lor a \lor b)$ ; for $z = \neg a$ , use $(z \lor a) \land (\neg z \lor \neg a)$ . Constants use unit clauses. If necessary add an output gate copying the designated input via two negations. Let $C$ be the conjunction. Each assignment to the inputs extends uniquely to one assignment satisfying $C$ , by gate order.

step 1.1algebra

3.1

With output variable $o$ , set $F_{\exists} = C \land o$ and $F_{\forall} = \neg (C \land \neg o)$ . If $R$ is true, the unique consistent extension witnesses the first formula and every extension satisfies the second. If $R$ is false, no extension satisfies the first and the consistent extension falsifies the second. Negating the 3CNF $C \land \neg o$ gives a 3DNF of the same linear size. Constant predicates and zero input bits obey the same construction.

step 2.1algebra∎

Depends on

Used by

Bounded alternation qbf is level complete Theorem

Dependency tree · two levels

4 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–Barak, Computational Complexity, 2007 draft; §5.2.2 Example5.9, pp93–94; constructive circuit prerequisite on disk. (standard reference, not scraped)