Quantum and Circuits

Download original file

This is the original TeX manuscript source. Use the paper’s PDF for typeset equations.

Read the typeset paper

Read this chapter with formatted equations

1 \guidepage{The model: boundary restoration and Boolean degree}
2 A state has logical input wires $x$, zero-initialized ancillary wires, and a
3 target bit $y$. A restored oracle is a legal classical circuit satisfying
4 \[
5  C(x,0^a,y)=(x,0^a,y+f(x))
6  \qquad\text{for every }x\text{ and both }y.
7 \]
8 The input and scratch restoration conditions hold at the boundary. Wires may
9 change internally, and the target may control an intermediate gate. Each
10 primitive gate is an involution:
11 \[
12  y\leftarrow y+1,\quad y\leftarrow y+x_i,\quad
13  y\leftarrow y+x_i x_j.
14 \]
15 In a CNOT the control differs from the target. In a Toffoli all three wires
16 are distinct. These are construction rules, not informal assumptions.
17 
18 All polynomial arithmetic in the Boolean state model is over $\F_2$, with
19 $x_i^2=x_i$. Every function has a unique multilinear algebraic normal form.
20 Its degree is the largest support size with a nonzero coefficient; the zero
21 function has mathematical degree $-1$ in the Python helpers. A formal degree
22 bound uses a natural number, so zero has a degree-zero certificate.
23 
24 \begin{tabularx}{\textwidth}{@{}p{1.15in}X@{}}\toprule
25 Quantity & Meaning\\\midrule
26 $T$ & Number of Toffoli gates; NOT and CNOT have zero cost in this quantity\\
27 $L$ & Total number of NOT, CNOT, and Toffoli gates\\
28 $M$ & Number of binary AND operations in an XOR--AND computation\\
29 $n$ & Actual number of input bits, including all variables in a displayed family\\
30 $\dim_K A$ & Dimension of a specified linear summary algebra over $K$\\\bottomrule
31 \end{tabularx}
32 
33 A bound on one row of this table cannot silently be substituted for a bound
34 on another row. In particular, a computation can have few Toffolis and many
35 CNOTs. An exponentially large ambient algebra can have succinct expressions.
36 Those distinctions explain the projection and gluing examples later.
37 
38 \sourcepath{docs/FOUNDATIONS.md, Conventions; formalization/lean/CircuitObstructions/Gates.lean}
39 
40 \guidepage{An arbitrary cut compares two reversible computations}
41 Write the circuit as $C=Q\circ P$. The prefix $P$ runs forward; the inverse
42 suffix $Q^{-1}$ starts from the same zero-target boundary state. Define
43 \[
44  A(x)=P(x,0),\qquad B(x)=Q^{-1}(x,0),\qquad
45  D(x)=P(x,1)+P(x,0).
46 \]
47 The zero ancillas are suppressed here. The two executions generally arrive
48 at different interior states, even though they start at matching boundaries.
49 
50 \visualfigure{cut_transport}{The exact C01 objects. Both arrows remain inside the legal reversible state space.}
51 
52 Correctness on both target branches gives
53 \[
54  Q^{-1}(x,b)=P(x,b+f(x)).
55 \]
56 To derive it, apply $C$ to $(x,b+f(x))$ and then apply $Q^{-1}$ to the result.
57 For $b=0$, $B=A$ when $f(x)=0$, while $B=P(x,1)$ when $f(x)=1$. Thus
58 \[
59  H(x):=A(x)+B(x)=f(x)D(x).
60 \]
61 The two original states differ in their target. Since $P$ is injective,
62 $D(x)\ne0$. Each coordinate discrepancy is supported on positives, and
63 some coordinate discrepancy detects every positive input.
64 
65 \evidence{General written identity; archived formal declarations
66 \code{cut_transport_identity}, \code{direction_nonzero}, and \code{complete_safe_cover}.}
67 
68 \guidepage{Why completeness is pointwise, and why no decoder is needed}
69 For a coordinate $i$, let $H_i=A_i+B_i$. The cut identity says
70 \[
71  H_i(x)=f(x)D_i(x),\qquad H_i\le f,\qquad \bigvee_i H_i=f.
72 \]
73 The last equation is pointwise. For every fixed accepted $x$, at least one
74 coordinate has $D_i(x)=1$. The detecting coordinate may depend on $x$ and
75 may be an input, scratch, or target wire. The argument does not require a
76 single fixed coordinate to detect all positives.
77 
78 At an empty prefix, the direction is simply the target unit vector. At a
79 full prefix, all non-target wires have restored and the target discrepancy
80 is $f$. Interior cuts can spread the direction through the workspace.
81 These minimum cases verify the composition order and the role of the two
82 target branches.
83 
84 The zero-input cases are also valid. With only a target wire, the empty
85 circuit realizes the constant-zero oracle and one NOT realizes the
86 constant-one oracle. At every cut, the direction is nonzero and the
87 discrepancy cover has the correct accepting set.
88 
89 \begin{quote}\small
90 \textbf{Essential hypothesis.} The endpoint condition holds for both initial
91 target values. The inverse-suffix derivation uses the branch $b+f(x)$.
92 Correctness only for initial target zero is not the stated model.
93 \end{quote}
94 
95 The theorem also does not require scratch to remain zero at the cut. Imposing
96 that extra condition would exclude admitted restored circuits. Conversely,
97 dropping target separation from the boundary encoding permits a vacuous
98 endpoint equation: an encoding that ignores $y$ can make the empty circuit
99 appear to compute a nonzero function. The formal \code{Boundary.target_eq}
100 property prevents precisely this degeneracy.
101 
102 \sourcepath{CutComparison.lean: inverse_suffix_boundary, every_index_cut, canonical_complete_safe_cover}
103 
104 \guidepage{A dirty scratch wire can be fully restored}
105 Consider the four-wire oracle in the Lean examples. First compute $ab$ into
106 scratch $s$, copy $s$ into the target, and uncompute $s$:
107 \[
108  (a,b,s,y)\xrightarrow{T(a,b;s)}(a,b,s+ab,y)
109  \xrightarrow{C(s;y)}(a,b,s+ab,y+s+ab)
110  \xrightarrow{T(a,b;s)}(a,b,s,y+s+ab).
111 \]
112 The displayed final expression specializes to the required oracle when
113 the boundary scratch is zero. On the positive input $a=b=1$, the scratch
114 is dirty between the first and last gates.
115 
116 \visualfigure{dirty_and_trace}{Exact states for the accepting input, in wire order $(a,b,s,y)$. White cells are zero; teal cells are one.}
117 
118 The two panels check both initial targets. The final target is toggled,
119 the logical inputs are unchanged, and scratch returns to zero. A proof that
120 used an intermediate clean-workspace assumption would fail to cover this
121 explicit legal fixture.
122 
123 This circuit uses two Toffolis. It is a useful restoration witness, not the
124 optimal two-input AND oracle: the direct gate $T(a,b;y)$ computes that oracle
125 with one Toffoli and no scratch. The guide distinguishes an exact example
126 from an optimization claim.
127 
128 \evidence{Exact new trace assertion imported from the source gate semantics;
129 the same fixture is formalized by \code{Examples.andOracle_restores}.}
130 
131 \guidepage{The output direction can move away from the target}
132 Two data/target wires already suffice. A SWAP is implemented by three legal
133 CNOTs. Let $P$ be that SWAP, and let $Q$ be NOT on the data wire followed
134 by another SWAP. Then
135 \[
136  (x,y)\xrightarrow{P}(y,x)
137  \xrightarrow{Q}(x,1+y).
138 \]
139 The whole circuit is a restored constant-one oracle with zero Toffolis.
140 At the cut after the first SWAP,
141 \[
142  A=P(x,0)=(0,x),\qquad B=Q^{-1}(x,0)=(1,x),
143  \qquad H=(1,0).
144 \]
145 The target discrepancy is zero on every input, while the data discrepancy
146 is one on every input. Reading only the target at this cut would reject
147 the constant-one function.
148 
149 \begin{center}
150 \begin{tabular}{@{}ccccc@{}}\toprule
151 $x$ & $A$ & $B$ & $H$ & named target discrepancy\\\midrule
152 0 & $(0,0)$ & $(1,0)$ & $(1,0)$ & 0\\
153 1 & $(0,1)$ & $(1,1)$ & $(1,0)$ & 0\\\bottomrule
154 \end{tabular}
155 \end{center}
156 
157 This example uses the target as a control during each SWAP. That behavior
158 is expressly allowed by the model. Its relevance is logical: completeness
159 belongs to the full register comparison, not to an arbitrarily chosen wire.
160 The coordinate packets remain perfectly safe even though the detection
161 direction has moved.
162 
163 \evidence{Constructive formal counterexample to target-only reconstruction:
164 \code{outputActiveOracle_restores}, \code{moved_discrepancy_data},
165 \code{moved_discrepancy_target}.}
166 
167 \guidepage{Degree bounds must retain shared register products}
168 Take four independent input bits. Compute
169 \[
170  q_1=x_1x_2,\qquad q_2=x_3x_4,\qquad q_3=q_1q_2.
171 \]
172 After two ANDs, each nonlinear register has degree two, but their product
173 has degree four. After the third AND, a coordinate of degree four appears.
174 
175 \visualfigure{sharing_degree}{Exact degrees from the complete four-input truth tables. The square marker is a two-register product, not a coordinate.}
176 
177 The correct invariant tracks a product of $r$ current registers after $t$
178 Toffolis:
179 \[
180  \deg\!\left(\prod_{i\in L}s_i(x)\right)\le t+|L|=t+r.
181 \]
182 At $t=2$, the product $q_1q_2$ has $r=2$ and saturates $t+r=4$. At $t=3$,
183 the resulting coordinate has $r=1$ and saturates $t+1=4$.
184 
185 This explains why tracking only individual register degrees and then
186 adding their separate histories can lose the shared accounting. The
187 invariant applies to the actual evolving state. It does not unfold a
188 reused register into a new copy of the entire computation.
189 
190 \evidence{Exact finite fixture plus the general register-product invariant;
191 the source proves \code{workspaceDegree_run} for arbitrary gate lists.}
192 
193 \guidepage{The invariant handles duplicates, NOT, and CNOT}
194 Suppose a gate toggles target $u$ by a product of $c$ controls. In a product
195 list $L$ that contains $u$, remove all occurrences of $u$ to obtain $R$.
196 Boolean idempotence leaves one updated target factor, and
197 \[
198  \prod_{i\in L}s_i'=
199  s_u\prod_{i\in R}s_i+
200  \left(\prod_{j\in\mathrm{controls}}s_j\right)\prod_{i\in R}s_i.
201 \]
202 The old invariant bounds these terms by $t+1+|R|$ and $t+c+|R|$.
203 Since $|R|+1\le |L|$, the budget rises by at most $\max\{c-1,0\}$.
204 
205 \begin{center}
206 \begin{tabular}{@{}lccc@{}}\toprule
207 Gate & $c$ & toggle expression & extra budget\\\midrule
208 NOT & 0 & 1 & 0\\
209 CNOT & 1 & one control & 0\\
210 Toffoli & 2 & two controls & 1\\\bottomrule
211 \end{tabular}
212 \end{center}
213 
214 If the target is absent from $L$, the product is unchanged. An empty list
215 is the constant-one product. Repeated target indices are removed using
216 idempotence; repeated other indices can only reduce multilinear degree.
217 Controls already appearing in $R$ also cause no difficulty.
218 
219 For general XOR--AND computations, the written proof introduces a Boolean
220 variable for each AND output. Every wire is affine in inputs and preceding
221 gate variables. Substitute those variables in reverse topological order.
222 A squarefree monomial contains each substituted variable at most once,
223 so replacing it by a quadratic raises degree by at most one. After $t$
224 substitutions, the affine output has degree at most $t+1$.
225 
226 These are two precise proof routes. The general syntax argument is written;
227 the maintained NCT register argument is in Lean. The formalization does not
228 assert a separate arbitrary XOR--AND compiler or a canonical ANF algorithm.
229 
230 \sourcepath{MultiplicativeDegree.lean; docs/FOUNDATIONS.md, F3}
231 
232 \guidepage{One safe packet need not cover every accepting point}
233 For $k=3$ consider
234 \[
235  F_3(a,b,z_1,z_2,z_3)=ab\ \mathrm{OR}\ z_1z_2z_3.
236 \]
237 The packet $ab$ is safe and has degree two. It detects every teal point
238 below. It misses three additional positives, which require the other
239 packet $z_1z_2z_3$.
240 
241 \visualfigure{packet_coverage}{All 32 assignments. There are 11 positives: 8 in the teal row and 3 additional gold points. The coordinate labels use $(z_1,z_2,z_3)$ order.}
242 
243 The one-packet parameter $\alpha_1$ asks for any nonzero safe polynomial.
244 The complete parameter $\beta$ asks for safe detection of every positive:
245 \[
246  \beta_v(f)=\min\{\deg h:h\le f,\ h(v)=1\},\qquad
247  \beta(f)=\max_{v:f(v)=1}\beta_v(f).
248 \]
249 For this monotone function, its minimal positive supports have sizes two
250 and three. Thus $\alpha_1(F_3)=2$ while $\beta(F_3)=3$. Selecting one
251 easy accepting region loses the pointwise obstruction at the other region.
252 
253 \evidence{All 32 points and the two parameter values were freshly recomputed;
254 the general monotone minterm characterization is a written proof for nonzero functions.}
255 
256 \guidepage{Balanced cuts turn coverage into a Toffoli bound}
257 Choose a cut after $\lfloor T/2\rfloor$ Toffolis. Both sides have at most
258 $\lceil T/2\rceil$ Toffolis. Reversing the suffix preserves its count because
259 every gate is self-inverse. Each forward or inverse-suffix coordinate has
260 degree at most $\lceil T/2\rceil+1$, and their XOR has the same upper bound.
261 
262 For every positive $v$, completeness chooses a discrepancy $H_i$ that
263 detects $v$. Its safety and degree bound imply
264 \[
265  \beta(f)\le\left\lceil\frac T2\right\rceil+1,
266  \qquad 2\beta(f)\le T+3.
267 \]
268 The integer rounding matters. If $T=2r$, the first bound gives
269 $2\beta\le T+2$. If $T=2r+1$, it gives $2\beta\le T+3$.
270 The uniform bound uses the latter constant.
271 
272 An affine output mask $\ell(x)$ costs zero additional Toffolis: append
273 CNOTs from restored inputs and, if needed, a target NOT. This constructs
274 a restored oracle for $f+\ell$, so the bound applies to every affine mask.
275 Define
276 \[
277  \beta^*(f)=\max_{\ell\text{ affine}}\beta(f+\ell).
278 \]
279 Together with the output degree bound,
280 \[
281  \boxed{T\ge\max\{0,\deg f-1,2\beta^*(f)-3\}.}
282 \]
283 
284 There are finitely many affine masks. The Lean definition uses the least
285 upper bound of their beta values, which equals this finite maximum. Its
286 affine-output theorem constructs legal gates rather than assuming masks
287 are free transformations of an arbitrary interior computation.
288 
289 \evidence{Written theorem and archived endpoint
290 \code{restored_degree_and_cover_bound}; the dual is a separate written result.}
291 
292 \guidepage{An affine shift reveals a harder accepting point}
293 For $k\ge2$, let $B=z_1\cdots z_k$ and $F_k=ab\ \mathrm{OR}\ B$ on
294 $n=k+2$ inputs. Add the affine mask $a$ to obtain $G_k=F_k+a$.
295 On the face $b=1$,
296 \[
297  G_k|_{b=1}=(1+a)B.
298 \]
299 This is a singleton indicator on the $k+1$ variables $(a,z)$.
300 At $v=(a=0,b=1,z=1^k)$, every safe detecting polynomial must restrict to
301 that singleton indicator, so its degree is at least $k+1$.
302 
303 The general two-positive indicator construction gives the matching upper
304 bound $\beta(G_k)\le n-1=k+1$. The maintained family proves
305 \[
306  \max_\ell\alpha_1(F_k+\ell)=3,\qquad \beta^*(F_k)=k+1.
307 \]
308 The gap between one-packet and complete degree therefore grows with $k$.
309 
310 \begin{center}
311 \begin{tabular}{@{}rrrrr@{}}\toprule
312 $k$ & $n$ & $\beta^*$ & complete bound $2k-1$ & combined degree/one-packet bound\\\midrule
313 2 & 4 & 3 & 3 & 3\\
314 3 & 5 & 4 & 5 & 4\\
315 4 & 6 & 5 & 7 & 5\\
316 6 & 8 & 7 & 11 & 7\\\bottomrule
317 \end{tabular}
318 \end{center}
319 
320 For $k=3$, all 64 affine masks were freshly checked and the optimized
321 parameters are exactly $(3,4)$. The all-size family proof is not inferred
322 from those 64 cases. Its restored construction has $T\le2n-3$, so this
323 remains a linear-size easy family. The exact optimum between the lower and
324 upper constructions is not asserted when they differ.
325 
326 \sourcepath{docs/THEORY.md, section 2; reviews/visual_examples.json, unbalanced_or}
327 
328 \guidepage{A degree-one dual certificate for two-input AND}
329 Let $f(a,b)=ab$, with unique positive point $(1,1)$. For degree at most one,
330 the evaluation vector is $v_1(a,b)=(1,a,b)$. The three negative points
331 already span the positive vector.
332 
333 \visualfigure{evaluation_dual}{The first three rows are negative inputs. Their XOR equals the last evaluation row.}
334 
335 Any affine polynomial is a coefficient covector $c=(c_0,c_a,c_b)$.
336 Safety means that it pairs to zero with each negative row. The displayed
337 dependence therefore forces its value at $(1,1)$ to be zero. No safe affine
338 packet detects the positive point.
339 
340 The degree-two polynomial $ab$ does detect it, so
341 $\beta_{11}(f)=\beta(f)=2$. Since $\beta^*\le n=2$ and $\beta^*\ge\beta$,
342 $\beta^*=2$. The complete bound gives $T\ge1$, attained by one direct
343 Toffoli to the target.
344 
345 The constant coordinate also checks parity: this dependence uses three
346 negative rows, an odd number. Without the constant coordinate, that parity
347 conclusion would not follow.
348 
349 \evidence{Exact finite dependence plus written duality. Lean proves the
350 corresponding AND2 degree and beta exclusions by four-corner parity,
351 without formalizing the general evaluation-span dual.}
352 
353 \guidepage{The finite evaluation-span dual in full}
354 Fix a positive $v$ and integer $d\ge0$. Let
355 \[
356  v_d(x)=(x^S)_{S\subseteq[n],\ |S|\le d},\qquad
357  U=f^{-1}(0),\qquad N=\Span_{\F_2}\{v_d(u):u\in U\}.
358 \]
359 The constant monomial $S=\varnothing$ is included. Degree-$d$ coefficient
360 covectors form the finite dual of this evaluation space. A covector is safe
361 exactly when it annihilates $N$.
362 
363 If $v_d(v)\in N$, every safe covector vanishes at $v$. If $v_d(v)\notin N$,
364 extend a basis of $N$ by $v_d(v)$ and then to a basis of the full space.
365 Assign zero to the $N$ basis and one to $v_d(v)$. The resulting covector is
366 a safe detector. Hence
367 \[
368  \boxed{\beta_v(f)>d\quad\Longleftrightarrow\quad v_d(v)\in N.}
369 \]
370 Choose a basis of $N$ from negative evaluation rows. A span representation
371 of the positive row gives a subset $W\subseteq U$ with
372 \[
373  v_d(v)=\sum_{u\in W}v_d(u),\quad |W|\text{ odd},\quad
374  |W|\le\sum_{j=0}^{\min(d,n)}\binom nj.
375 \]
376 It is a replayable finite obstruction to every safe degree-$d$ detector.
377 
378 At $d=0$, a negative exists exactly when the constant-one detector is unsafe.
379 At $d\ge n$, the full evaluation rows are independent and no positive row
380 lies in the negative span. This matches $\beta_v\le n$ from point indicators.
381 For $f=0$, there is no positive $v$ and the separate convention is $\beta(0)=0$.
382 
383 Fresh enumeration checked all 278 functions on zero through three inputs,
384 all positives, and every $d=0,\ldots,n$: 4,201 primal/dual checks agree.
385 Those bounded checks support the independently supplied universal proof.
386 
387 \sourcepath{scripts/core_dual_checks.py; reviews/core_dual_checks.json}
388 
389 \guidepage{Every function through three inputs has a matching oracle}
390 The small calibration concerns every truth table on one, two, or three
391 inputs. It is not a search through all reversible circuit words. A theorem
392 lower bound and an explicit construction coincide.
393 
394 \visualfigure{small_oracle_counts}{Reconstructed source constructions for all 276 functions. Totals are 28 with $T=0$, 120 with $T=1$, and 128 with $T=3$.}
395 
396 Affine functions use target CNOTs and possibly NOT. A nonaffine quadratic
397 through three bits has alternating quadratic rank two, so it is a product
398 of two independent linear forms plus an affine residual. Compute those
399 forms on clean wires, apply one Toffoli, uncompute, and append the residual.
400 
401 Every three-bit cubic is a translated three-variable monomial plus an
402 affine residual. The singleton monomial needs three Toffolis by complete
403 coverage, and compute/toggle/uncompute attains that number.
404 
405 The new figure script rebuilds and validates all 276 circuits and both target
406 branches, covering 4,240 scalar input/target cases via exact truth tables.
407 Its totals match the frozen baseline. Zero-input constants were checked in
408 the separate dual suite, rather than being added to this 276-function count.
409 
410 \evidence{Matching written lower bounds and exact constructed implementations;
411 not exhaustive optimal-circuit synthesis. The generic monomial cost theorem
412 is not newly Lean-certified by this edition.}
413 
414 \guidepage{Projection is defined in the original coordinates}
415 For $m\ge2$, put $a=(1,\ldots,1)$ and
416 \[
417  V=\F_2^m\setminus\{0,a\},\qquad n=2^m-2.
418 \]
419 There is one input bit $x_v$ for each $v\in V$. Define
420 \[
421  L_j(x)=\sum_{v:v_j=1}x_v,\qquad
422  P_m(x)=\prod_{j=1}^m L_j(x).
423 \]
424 The linear map $x\mapsto L(x)$ has rank $m$, because the standard basis
425 columns are present. In the $L$ coordinates, $P_m$ is a monomial in $m$
426 independent bits. Its restored nonlinear cost is $2m-3$.
427 
428 Now extract the quadratic homogeneous ANF component $Q_m$ in the
429 \emph{original} $x_v$ coordinates. Since $P_m(0)=P_m(e_v)=0$, for distinct
430 $u,v$ its quadratic coefficient is
431 \[
432  [x_ux_v]P_m=P_m(e_u+e_v)=[u+v=a].
433 \]
434 The involution $v\mapsto v+a$ pairs every variable with one other variable:
435 \[
436  Q_m=\sum_{\{v,v+a\}}x_vx_{v+a}.
437 \]
438 It is a quadratic inner product on $n/2$ disjoint pairs. Its alternating
439 polar matrix has full rank $n$.
440 
441 The coordinate choice is essential. Homogeneous grade is not invariant
442 under arbitrary affine changes of variables. A cheap representation in
443 the $L$ coordinates does not imply cheap independent generation of the
444 quadratic grade in the original coordinates. The comparison keeps the
445 definition of projection fixed throughout.
446 
447 \sourcepath{docs/THEORY.md, section 3; checks/verify_projection.py}
448 
449 \guidepage{Exact nonlinear projection costs versus actual input length}
450 The source proves the all-size formulas
451 \[
452  M(P_m)=m-1,\quad T_{\mathrm{rest}}(P_m)=2m-3,\qquad
453  M(Q_m)=T_{\mathrm{rest}}(Q_m)=n/2.
454 \]
455 The chart uses actual input length $n=2^m-2$ on its horizontal axis.
456 
457 \visualfigure{projection_costs}{Exact formulas for $m=2,\ldots,10$. Both axes are logarithmic; the plotted points are not optimal-circuit search results.}
458 
459 For $Q_m$, each disjoint quadratic pair is accumulated directly into the
460 target with one Toffoli. The lower bound allows nonlinear intermediates:
461 any computation with $t$ multiplications is affine on an affine subspace
462 of codimension at most $t$. A nondegenerate quadratic can be affine only
463 on a subspace with isotropic direction space, whose dimension is at most
464 $n/2$. Thus $t\ge n/2$.
465 
466 The separation grows exponentially in $m$, but $n$ itself grows
467 exponentially in $m$. The quadratic cost is linear in actual input length.
468 The conclusion is about nonlinear generation and a specified grade
469 extraction operation, not a superpolynomial unrestricted circuit bound.
470 
471 \evidence{All-size written cost proofs; constructor gate counts freshly
472 asserted through $m=10$. No full truth-table enumeration at $m>4$ is claimed.}
473 
474 \guidepage{At $m=10$, the total-gate accounting points the other way}
475 Here $n=1,022$. The full function uses 17 Toffolis; its quadratic grade
476 needs 511. However, computing and uncomputing the $m$ parities also uses
477 \[
478  2m(2^{m-1}-1)=20\cdot511=10,220\quad\text{CNOTs}.
479 \]
480 The explicit full construction has $10,237$ total gates. The quadratic
481 accumulation uses only 511 total gates.
482 
483 \visualfigure{projection_m10}{Two different resource comparisons at the same input length. The right panel reports the totals of the stated constructions, not an asserted optimal total for $P_{10}$.}
484 
485 The left panel is a valid nonlinear-cost separation. The right panel
486 prevents interpreting it as an exponential ordinary total-gate separation.
487 The total full construction is $O(n\log n)$, whereas the quadratic
488 construction is $n/2$ gates.
489 
490 A proposed invariant that charges an original computation for every
491 separately extracted grade would have to justify that extraction's cost.
492 These formulas refute an overhead bounded only by a polynomial in the
493 original nonlinear count, independently of input and linear resources.
494 They do not exclude an overhead polynomial in $n+T$ or a different
495 precisely defined invariant.
496 
497 \evidence{Exact counts obtained from the source constructors; optimal
498 Toffoli formulas have written proofs. The full total-gate count is an upper
499 construction count.}
500 
501 \guidepage{Quadratic projection can destroy safety}
502 At $m=3$, variables are ordered by source labels $v=1,2,3,4,5,6$.
503 Assignment index $13$ is read least-significant-bit first:
504 \[
505  (x_1,x_2,x_3,x_4,x_5,x_6)=(1,0,1,1,0,0).
506 \]
507 The active labels have syndrome $1+3+4=6$, not $a=7$.
508 
509 \visualfigure{unsafe_projection}{A concrete accepted point for $Q_3$ that is rejected by $P_3$. The variable ordering matches the source checker.}
510 
511 The three linear forms evaluate to $L=(0,1,1)$, so $P_3=L_1L_2L_3=0$.
512 The quadratic grade has pairs $(1,6)$, $(2,5)$, $(3,4)$, so
513 \[
514  Q_3=x_1x_6+x_2x_5+x_3x_4=0+0+1=1.
515 \]
516 Thus $Q_3\notin I_{P_3}$: homogeneous extraction does not preserve the
517 positive-support ideal. The whole polynomial is supported on its own
518 accepting set, but its isolated homogeneous components need not be.
519 
520 The new script checks all 64 inputs here, finds 24 false positives, and
521 confirms that 13 is the first in the stated integer ordering. The frozen
522 $m=4$ control similarly has 7,616 false positives among its $2^{14}$
523 assignments. These are separate finite statements with exact ranges.
524 
525 \evidence{Fresh complete $m=3$ truth-table check; baseline $m=4$ check was
526 reproduced by the full source verifier. Safety failure is already established
527 by the single valid assignment above.}
528 
529 \guidepage{Witness indicators are orthogonal idempotents}
530 Let $K$ be a field and $W=\{0,1\}^m$. The full witness algebra is
531 $B=K^W$ with pointwise addition and multiplication. For each witness $v$,
532 the indicator $\delta_v$ is one at $v$ and zero elsewhere. Then
533 \[
534  \delta_v^2=\delta_v,\qquad \delta_u\delta_v=0\ (u\ne v),
535  \qquad \sum_v\delta_v=1.
536 \]
537 
538 \visualfigure{orthogonal_gluing}{The four-witness multiplication table at $m=2$. Each nonzero diagonal entry is its own point indicator.}
539 
540 The four indicator functions form a basis of $K^4$. General $m$ has $2^m$
541 such basis elements. A verifier is the sum of the indicators of its accepted
542 witnesses, and pointwise multiplication models intersection of accepting
543 sets.
544 
545 This algebra retains exact witness compatibility: disjoint singleton
546 predicates multiply to zero. A summary that preserves that product operation
547 while retaining every singleton must preserve the same orthogonal structure.
548 The following dimension theorem says exactly how much fixed linear space
549 that requires.
550 
551 \evidence{Exact $m=2$ multiplication table; general product-algebra identities
552 hold over any field. No characteristic-two assumption is needed for the
553 dimension proof.}
554 
555 \guidepage{Faithful linear multiplicative summaries need $2^m$ dimensions}
556 Suppose $\Phi:K^W\to A$ is $K$-linear and multiplicative, and
557 $\Phi(\delta_v)\ne0$ for every $v\in W$. Put $e_v=\Phi(\delta_v)$.
558 The images are nonzero orthogonal idempotents.
559 
560 If $\sum_v c_v e_v=0$, multiply by $e_u$. Orthogonality removes every other
561 term and idempotence gives $c_u e_u=0$. Since $K$ is a field and $e_u\ne0$,
562 $c_u=0$. Hence all $e_v$ are linearly independent and
563 \[
564  \boxed{\dim_K A\ge |W|=2^m.}
565 \]
566 No unital hypothesis is needed. At $m=0$, there is one empty witness and
567 the bound is simply $\dim_K A\ge1$.
568 
569 For a unital scalar map to $K$, scalar idempotents are zero or one.
570 Orthogonality permits at most one nonzero image, and preservation of one
571 requires exactly one. Such a map is evaluation at one witness. For $m\ge1$
572 it loses at least one other singleton verifier. For $m=0$, there is no other
573 witness to lose.
574 
575 \begin{quote}\small
576 \textbf{Model boundary.} The theorem quantifies a fixed summary serving all
577 predicates at a witness length, preserving linear combinations and exact
578 pointwise multiplication. An unrestricted algorithm need not use such a
579 summary. Syntax, nonlinear encodings, changing spaces, context-dependent
580 operations, and succinct expressions are outside these hypotheses.
581 \end{quote}
582 
583 An exponentially large algebra can still contain short circuit expressions.
584 Therefore exponential dimension does not imply exponential expression length
585 or a lower bound for every algorithm on one explicit decision family.
586 
587 \sourcepath{docs/THEORY.md, Theorem 4.1; reviews/extended_audit.md}
588 
589 \guidepage{Distinct witness monomials prevent formal cancellation}
590 Over a characteristic-two field, define
591 \[
592  P_R(z)=\sum_{w\in\{0,1\}^m}R(w)\prod_i z_i^{w_i}.
593 \]
594 The $z_i$ are formal indeterminates, not Boolean variables. Different
595 witnesses produce different monomials, so $P_R=0$ exactly when there is
596 no accepting witness.
597 
598 \visualfigure{witness_fingerprint}{An exact three-bit verifier accepts witness indices $1,2,5,6$ in least-significant-bit order. Four accepts have parity zero, but their monomials are distinct.}
599 
600 Here
601 \[
602  P_R=z_1+z_2+z_1z_3+z_2z_3=(z_1+z_2)(1+z_3)\ne0.
603 \]
604 The ordinary unweighted characteristic-two sum of the four accepts is
605 zero. The formal polynomial avoids this cancellation by retaining witness
606 labels as monomial supports.
607 
608 Nonzero as a formal polynomial does not mean nonzero at every field point.
609 For instance, this example vanishes whenever $z_1=z_2$ or $z_3=1$.
610 Random evaluation is governed by a root bound, not by the formal identity
611 alone. Evaluating the polynomial efficiently remains a separate task.
612 
613 \evidence{Exact support fixture; general no-cancellation argument is written.
614 The source finite evaluator retains $2^m$ coefficients.}
615 
616 \guidepage{A short expression inside a trace is not a computed trace}
617 Let $\tau_w$ extract the top multilinear coefficient in the Boolean witness
618 ring. For any $G(w)$ over a characteristic-two field,
619 \[
620  \tau_w(G)=\sum_{v\in\{0,1\}^m}G(v).
621 \]
622 A proper-support monomial evaluates to one an even number of times; the
623 full-support monomial does so once. This proves the identity directly.
624 
625 Applying it to a weighted expression gives
626 \[
627  P_R(z)=\tau_w\!\left[
628  R(w)\prod_{i=1}^m\bigl(1+(1+z_i)w_i\bigr)\right].
629 \]
630 At $w_i=0$, a multiplier equals one. At $w_i=1$, it equals $z_i$.
631 Summing evaluations therefore produces exactly the witness monomials.
632 For the preceding verifier, the four surviving products are
633 $z_1,z_2,z_1z_3,z_2z_3$.
634 
635 The circuit expression \emph{inside} the trace adds only $O(m)$ operations
636 to the verifier. That observation bounds the expression's construction,
637 not the cost of applying $\tau_w$. The finite checker computes with a
638 complete table of $2^m$ witness coefficients.
639 
640 \begin{center}
641 \begin{tabularx}{\textwidth}{@{}p{1.8in}X@{}}\toprule
642 Established & Not supplied by the expression\\\midrule
643 Small weighted circuit inside $\tau$ & A polynomial-time evaluator for the trace\\
644 Formal polynomial detects nonemptiness & A deterministic identity test from one evaluation\\
645 Exact finite table algorithm & Polynomial storage in the witness length\\\bottomrule
646 \end{tabularx}
647 \end{center}
648 
649 At $m=0$, the empty product is one, the top coefficient is the constant
650 itself, and there is a single empty witness. The definitions remain valid.
651 
652 \sourcepath{docs/THEORY.md, equations (10)--(11); checks/verify_fingerprint.py}
653 
654 \guidepage{Disjoint-variable factorization uses each predicate's own block}
655 Suppose $A$ depends on witness variables in block $S$ and $B$ on a disjoint
656 block $T$. Write $\tau_{z_S}(A)=\sum_s A(s)z_S^s$ for the weighted trace
657 on $S$, distinct from the unweighted top-coefficient notation $\tau_w$.
658 Weighted sum over the union factors as
659 \[
660  \sum_{s,t} A(s)B(t)z_S^s z_T^t
661  =\left(\sum_s A(s)z_S^s\right)
662   \left(\sum_t B(t)z_T^t\right).
663 \]
664 Each factor is traced on its own variable block. The union trace is then
665 their product. This is an ordinary factorization of a finite double sum.
666 
667 For $A=w_1$ and $B=w_2$,
668 \[
669  \tau_{z_1}(A)=z_1,\qquad \tau_{z_2}(B)=z_2,\qquad
670  \tau_{z_1,z_2}(AB)=z_1z_2.
671 \]
672 Tracing both factors over the full two-bit ambient domain introduces unused
673 variable sums:
674 \[
675  \tau_{z_1,z_2}(A)=z_1(1+z_2),\qquad
676  \tau_{z_1,z_2}(B)=z_2(1+z_1).
677 \]
678 Their product generally differs from the union trace. At $z_1=z_2=1$, each
679 full ambient factor is zero, while the trace of $AB$ is one. Disjoint
680 dependence alone does not justify multiplying traces with mismatched domains.
681 
682 The source checker tests all four one-bit predicates per block and every
683 pair of GF(16) weights: $4\cdot4\cdot16^2=4,096$ own-block factorization
684 cases. It does not claim an ambient-domain product identity.
685 
686 \evidence{General written factorization under the own-block convention;
687 exact finite source check and an explicit ambient-domain counterexample.}
688 
689 \guidepage{Overlap breaks the attempted context-free product rule}
690 One shared witness bit already defeats multiplicativity. With
691 $\tau_z(P)=P(0)+zP(1)$,
692 \[
693  \tau_z(w)=z,\qquad \tau_z(1+w)=1,
694  \qquad \tau_z(w(1+w))=0.
695 \]
696 The product of the separate summaries is $z$. Also $w^2=w$ in the Boolean
697 ring, so $\tau_z(w^2)=z$, whereas $\tau_z(w)^2=z^2$.
698 
699 \visualfigure{overlap_gf16}{A concrete field point $z=\theta$ with $\theta\ne0,1$. The two columns are unequal in both rows.}
700 
701 The field is $\F_{16}=\F_2[\theta]/(\theta^4+\theta+1)$. The checker stores
702 field elements as four-bit coefficient vectors: $\theta$ is integer 2 and
703 $\theta^2$ is integer 4. These integers encode field elements; they are not
704 ordinary integer multiplication. Exact field multiplication gives the
705 reported mismatch.
706 
707 The first row loses witness compatibility: $w$ and $1+w$ have no common
708 accepting witness, yet their separate weighted summaries multiply to a
709 nonzero value. The second row loses Boolean idempotence. This is a genuine
710 counterexample to a context-free multiplicative trace compiler, not a
711 floating-point effect or an implementation anomaly.
712 
713 \evidence{Exact GF(16) fixture imported from the source field routines. The
714 general overlap failure is symbolic and does not depend on the selected field.}
715 
716 \guidepage{Randomized detection is conditional on efficient evaluation}
717 The witness polynomial has total degree at most $m$. Over a finite field
718 $K$, a nonzero polynomial of total degree at most $m$ vanishes on at most
719 an $m/|K|$ fraction of independent uniform field points. The standard
720 inductive proof separates the leading coefficient in the last variable
721 and applies the univariate root bound.
722 
723 If a uniform polynomial-time exact evaluator for the weighted trace were
724 available, with efficient field representation and arithmetic and
725 $|K|\ge4m$, one evaluation would accept a satisfiable verifier with
726 probability at least $3/4$. An unsatisfiable verifier has the zero polynomial,
727 so it never produces a false acceptance. Repetition with independent samples
728 reduces the false-rejection probability to at most $4^{-r}$ after $r$ trials.
729 
730 \begin{center}
731 \begin{tabular}{@{}rrrr@{}}\toprule
732 Witness bits & GF(16) points & maximum zeros in source tests & degree-bound zeros\\\midrule
733 1 & 16 & 1 & 1\\
734 2 & 256 & 31 & 32\\
735 3 & 4,096 & 721 & 768\\\bottomrule
736 \end{tabular}
737 \end{center}
738 
739 These source tests enumerate every verifier at each displayed witness length
740 and all field points for the polynomial evaluations. The independent
741 coefficient-extraction comparison has a narrower three-variable grid:
742 coordinates $0,1,2,3$, rather than all GF(16) points. Both scopes are recorded.
743 
744 This is a conditional randomized algorithmic implication. The required
745 efficient trace evaluator is not supplied. The existing exact evaluator is
746 exponential in witness length, and no deterministic $P=NP$ conclusion is
747 drawn. Random bits and polynomial output description alone do not account
748 for the evaluation operation.
749 
750 \sourcepath{docs/THEORY.md, section 5; evidence/baseline/fingerprint.json}
751 
752 \guidepage{Reproduce the figures and inspect their exact evidence}
753 All 12 figure pairs are vector PDFs plus raster PNG previews. Their single
754 generation command, from the publication-set root, is
755 \begin{lstlisting}
756 python scripts/make_figures.py
757 \end{lstlisting}
758 The script imports the original gate, profile, construction, and GF(16)
759 functions without invoking their release-writing entry points. It writes
760 only new figures and \code{reviews/visual_examples.json}. That record contains
761 fixture truth-table integers, ordered bits, exact gate lists, scalar counts,
762 the source hashes, and the distinction between finite assertions and
763 plotted all-size formulas.
764 
765 The separate dual sanity suite runs as
766 \begin{lstlisting}
767 python scripts/core_dual_checks.py \
768   --output reviews/core_dual_checks.json
769 \end{lstlisting}
770 It compares exhaustive degree-bounded safe truth tables with a separate
771 Gaussian-elimination calculation of the negative evaluation span. Its
772 range is all truth tables at $n=0,1,2,3$, not an extrapolation.
773 
774 \begin{tabularx}{\textwidth}{@{}p{1.4in}X@{}}\toprule
775 Evidence layer & Publication treatment\\\midrule
776 General mathematics & Main paper written proofs with explicit model boundaries\\
777 Formal subset & C01, maintained NCT degree, and numerical C02; fresh compiler and kernel replay passed\\
778 New figures & 12 exact generated examples/formula plots, each with fixture provenance\\
779 Fresh source checks & Complete source \code{--all} verification and preserved historical outputs passed in the current replay\\
780 Rendering & This guide is compiled and visually checked separately from mathematical and kernel verification\\\bottomrule
781 \end{tabularx}
782 
783 The source release, earlier companions, and archived evidence remain
784 unchanged. Publication corrections clarify evidence labels, the nonzero
785 monotone minterm domain, the $m=0$ scalar-summary boundary, and trace-variable
786 domains. No new conjecture or extension to unrestricted hardness is added.
787 
788 \evidence{Figure and manuscript sources are included for review and reproduction.}
789 

Back to source controls

Back to Quantum and Circuits