The formal endpoint
On this page · Permalink · Source line 28
Let \(c\) be a finite legal classical NOT/CNOT/Toffoli circuit. For \(n\) input bits and \(a\) zero-initialized ancillas, assume for every \(x\) and both initial target values \(b\) that
Write \(T={\operatorname{tc}}(c)\) for its number of Toffoli gates. The Block 02 joint endpoint is
Degree and complete-cover bound
CircuitObstructions.restored_degree_and_cover_bound
The first conclusion is an explicit certificate that \(f\) has a Boolean polynomial representation of degree at most \(T+1\). The second is the affine-optimized complete safe-cover lower bound, equivalently \(T\ge\max\{0,2\beta^*(f)-3\}\).
This applies even when the output controls intermediate gates, the inputs are modified temporarily, and workspace is dirty internally. It requires restoration only at the boundary. It makes no restriction to clean intermediate representations.
What changed
On this page · Permalink · Source line 45
Block 01 proved that discrepancies between a prefix and an inverse suffix form a complete safe cover. Block 02 supplies the missing degree dependency, proves that the cover parameters exist, constructs the balanced cut, and implements affine-output adjustment using legal zero-Toffoli circuits.
What did not change
On this page · Permalink · Source line 48
The mathematical scope remains the eight maintained claim groups. C02 is still partial as a group: its dual-certificate theorem is not included. The formal source also proves
This ceiling prevents the degree parameter alone from producing a superpolynomial lower bound. No new best-known bound or publication-novelty claim is made.
Where the proof lives
On this page · Permalink · Source line 55
Every proof term is in formalization/lean/CircuitObstructions/. The source inventory, archived 21 September elaboration log, and archived axiom report identify the exact statements. The register in this document lists all 115 maintained theorem declarations, including the 40 inherited declarations. Imported standard-library theorems are not counted.