Circuit satisfiability becomes linear-quadratic consistency

List the wires of $C$ in a topological order, starting with the $n$ named inputs $x_1,\dots ,x_n$, then the $s-n$ remaining inputs, and then the $m$ non-input gates, and create one variable $w_{\mathrm{\ell }}\in {\mathbb{F}}_2$ for each wire, so that the first $n$ variables are exactly the named input coordinates and $N=s+m$. Record the index of the designated output wire from the circuit description; it need not be the last wire in this order. This is a construction on the explicit gate list, and it uses no choices.

For every gate, in the topological order of the wire list of step 1.1, write one equation in the variables of its input wires and its output wire, and write one further equation for the designated output; all arithmetic is in ${\mathbb{F}}_2$:

Suppose $C$ accepts $x$, choose an assignment to the other $s-n$ inputs witnessing acceptance and assign to every wire variable its value in the resulting full-input evaluation of $C$. Then $w_1\cdots w_n=x$, and each equation of step 2.1 holds: for NOT, AND, OR and the constants this is exactly the evaluation rule in the identities of [F4], and the output equation holds because the designated output evaluates to $1$. Hence the system has a solution extending $x$; it is the evaluation assignment of the circuit.

Conversely, suppose $w$ satisfies all $m+1$ equations and $w_1\cdots w_n=x$. We show by induction along the topological order that every wire variable equals the evaluation of its wire on the full input assignment encoded by $w_1,\dots ,w_s$. The input variables do by the definition of that assignment. For a gate whose input wires are already correct, its equation determines the output variable: the NOT equation gives $z=1+x$, the AND equation $z=xy$, the OR equation $z=x+y+xy$, and the constant equations give $z=1$, $z=0$, all of which are the evaluation rules of [F4]. Thus every wire variable has its evaluated value, including the designated output wire; the additional output equation forces that value to be $1$. Hence $C$ accepts $x$ by [F1], and once all $s$ input coordinates are fixed, the extension to the gate wires is unique: two solutions with the same full input assignment agree wire by wire in the same induction.

For the random subsum, fix any $w\in {\mathbb{F}}_2^N$ and put $v_k:=q_k(w)+b_k\in {\mathbb{F}}_2$, so that $v_k=0$ says the $k$-th equation is satisfied, and let $U:=w\otimes w$; by [F2] each $q_k(w)=A_k\odot U$, so $v_k=A_k\odot U+b_k$ and the combined equation of the statement holds exactly when $z\cdot v=0$. If $w$ fails at least one equation then $v\mathrm{\ne }0$, and [F3] makes $z\cdot v=1$ with probability exactly $1\mathrm{/}2$ over the uniform $z$; this is the claimed rejection probability, and the combined left side is $A(z)\odot U=g(A(z))$ for the Hadamard table of $U$, so the whole test costs the single table query $g(A(z))$ plus the computation of $A(z)$ and $b(z)$ from the gate list.

Steps 3.1, 3.2 and 3.3 are the three clauses of the statement: the construction of steps 1.1 and 2.1 gives the input prefix and the size bound, the pair of inductions gives the exact extension equivalence and uniqueness conditional on the full input assignment, and the subsum argument gives the constant rejection probability of a single tensor query; the circuit-to-system translation is deterministic and polynomial time in the gate list.