The invariant handles duplicates, NOT, and CNOT
On this page · Permalink · Source line 193
Suppose a gate toggles target \(u\) by a product of \(c\) controls. In a product list \(L\) that contains \(u\), remove all occurrences of \(u\) to obtain \(R\). Boolean idempotence leaves one updated target factor, and
The old invariant bounds these terms by \(t+1+|R|\) and \(t+c+|R|\). Since \(|R|+1\le |L|\), the budget rises by at most \(\max\{c-1,0\}\).
| Gate | \(c\) | toggle expression | extra budget |
|---|---|---|---|
| NOT | 0 | 1 | 0 |
| CNOT | 1 | one control | 0 |
| Toffoli | 2 | two controls | 1 |
If the target is absent from \(L\), the product is unchanged. An empty list is the constant-one product. Repeated target indices are removed using idempotence; repeated other indices can only reduce multilinear degree. Controls already appearing in \(R\) also cause no difficulty.
For general XOR–AND computations, the written proof introduces a Boolean variable for each AND output. Every wire is affine in inputs and preceding gate variables. Substitute those variables in reverse topological order. A squarefree monomial contains each substituted variable at most once, so replacing it by a quadratic raises degree by at most one. After \(t\) substitutions, the affine output has degree at most \(t+1\).
These are two precise proof routes. The general syntax argument is written; the maintained NCT register argument is in Lean. The formalization does not assert a separate arbitrary XOR–AND compiler or a canonical ANF algorithm.