13.5 A degree invariant that retains sharing
On this page · Permalink · Source line 68
The preceding Boolean substitution proof applies to general XOR–AND straight-line computations. The later formal development proves the classical reversible specialization directly on the evolving register state. This route makes the resource accounting visible without unfolding reused registers into duplicated formulas.
Theorem 13.3: Register-product degree invariant
Let \(s_i(x)\) be the contents of a finite register after \(t\) Toffoli gates, with arbitrary intervening NOT and CNOT gates. Initial register contents are affine functions of \(x\). For every finite list \(L\) of \(r\) register indices, including repeated indices,
The zero-function convention is as above. In the formal source the conclusion is the concrete representation certificate DegreeLE.
Proof
Initially a product of \(r\) affine functions has degree at most \(r\). Suppose a gate toggles register \(u\) by a product of \(q\) controls, with \(q=0,1,2\) for NOT, CNOT, and Toffoli respectively. If \(u\) does not occur in \(L\), the product is unchanged. If it occurs, Boolean idempotence removes all its repetitions. Let \(R\) be the remaining list, so \(|R|+1\le r\). The updated product is
By the old invariant, these two summands have degrees at most \(t+1+|R|\) and \(t+q+|R|\). The latter is at most \(t+r+\max\{q-1,0\}\). NOT and CNOT therefore consume no degree budget; a Toffoli consumes at most one. Induction along the actual gate list proves the claim. The empty list is the constant-one product and is also covered.
For \(r=1\) this recovers the coordinate bound. The initial target can be fixed to either boundary bit while the inputs vary. Temporary input disturbance, dirty intermediate workspace, output controls, and repeated use of earlier products are all allowed. The formal locators are workspaceDegree_run and canonical_run_coordinate_degree.
The representation is part of the theorem
DegreeLE(d,f) is tied by proved equivalences to an explicit finite XOR of monomials with length at most \(d\). It is not an assumed degree oracle. Canonical algebraic-normal-form extraction and a separate generic XOR–AND simulation compiler are outside this formal block.