LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-30

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.

Boolean circuits become quadratic systems with a fixed input prefix

Statement

Let $C$ be an explicit topologically ordered Boolean circuit with $s$ input wires, a designated prefix of $n$ inputs where $0 \leq n \leq s$ , and $m$ non-input nodes. Each non-input node is a constant $0$ or $1$ , a NOT gate, or a two-input AND or OR gate; represented constant nodes count among the $m$ nodes. Its output is one of the resulting $s + m$ wires. There is a deterministic polynomial-time construction of a QUADEQ instance over $F_{2}$ with $N = s + m$ wire variables and $m + 1$ equations, each with at most four monomials. The variables are ordered with the $s$ input wires first and the non-input nodes next in topological order, so the named inputs are the first $n$ variables. For every $x \in F_{2}^{n}$ , fixing those first $n$ variables to $x$ extends to a solution of the QUADEQ instance if and only if there is a completion $y \in F_{2}^{s - n}$ such that $C (x, y) = 1$ .

Facts & Assumptions

Given: A valid circuit as in the statement and the fixed named-prefix assignment $x$ .

[F1]

In the canonical QUADEQ encoding, constants are moved to the right-hand side, repeated monomials cancel in $F_{2}$ , and a linear term $w_{i}$ is represented by the diagonal monomial $w_{i}^{2}$ . (Quadratic equations and tensor-code oracle tables)

[F2]

A Boolean circuit is a finite directed acyclic graph with input wires, constants, NOT/AND/OR gates, a designated output, and evaluation in topological order. (Boolean circuits: basis, fan-in, size, and depth)

[F3]

Circuit satisfiability asks whether some input assignment makes the designated output one. (Circuit satisfiability)

Proof

1.1F2givenconstruct

Number the $s$ primary input wires first, then number the $m$ remaining nodes in topological order, and associate a variable $w_{i}$ to each wire. Thus $N = s + m$ , and fixing $w_{1}, \dots, w_{n}$ to $x$ fixes exactly the named prefix; the other primary input variables remain available for the completion.

2.1F1F2step 1.1algebra

For a constant node with variable $z$ and value $c$ , impose $z = c$ ; for a NOT node with input $a$ impose $z + a = 1$ ; for an AND node with inputs $a, b$ impose $z + a b = 0$ ; and for an OR node impose $z + a + b + a b = 0$ . These equations force exactly the indicated Boolean operation: in particular $a \lor b = a + b + a b$ for bits. They remain valid when the two input wires coincide, after reducing repeated monomials using $a^{2} = a$ in $F_{2}$ . Append the output equation $w_{o u t} = 1$ . There are $m + 1$ equations, each with at most four monomials. Using [F1], place each linear term on its diagonal tensor coordinate, each quadratic term on its upper-triangular coordinate, and each constant on the right-hand side; this gives a canonical QUADEQ instance.

3.1F2F3step 2.1algebra

Suppose a solution extends the prefix $x$ . Its next $s - n$ coordinates define a completion $y$ . The gate equations in step 2.1, read in topological order, force every non-input wire to equal its evaluated circuit value, and the output equation forces $C (x, y) = 1$ .

3.2F2F3step 2.1constructalgebra

Conversely, suppose some completion $y$ makes $C (x, y) = 1$ . Set the first $s$ variables to $(x, y)$ and set every remaining variable to the value of its node under the circuit evaluation. Each constant or gate equation in step 2.1 then holds by its defining Boolean operation, and the output equation holds because the output is one. This constructs a QUADEQ solution extending $x$ , proving the reverse implication.

4.1F1F2step 2.1discharge-constructalgebra∎

The construction lists one constant-size equation per node and one output equation. Writing each of the $m + 1$ coefficient matrices with $N^{2}$ entries takes $O ((m + 1) N^{2})$ time; since the explicit description lists all $s + m = N$ wires, this is polynomial in its length. The equations themselves have the claimed bound from step 2.1. The construction uses only the topological order and fixed gate formulas, so it is deterministic.

Depends on

Used by

Two-piece PCP of proximity and concatenation check Definition
A two-piece constant-query PCP of proximity Theorem

Dependency tree · two levels

5 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, §18.4.3, proof of Corollary 18.25, printed p. 368; §18.4.2, QUADEQ encoding, printed pp. 365–366 (standard reference, not scraped)