The proof dependency route
On this page · Permalink · Source line 293
A SOURCE MAP RATHER THAN A NEW AXIOM
| Stage | Source role and conclusion |
|---|---|
| Legal gates and reversal | Distinct-wire constructor proofs; each gate is self-inverse; reverse gate lists invert the run |
| Separated boundary | The two initial target branches remain distinct after every prefix |
| Cut transport | Inverse suffix meets the appropriate forward target branch; \(H_i=fD_i\) gives safety and pointwise completeness |
| Polynomial certificates | Monomial evaluation and XOR/product closure connect concrete lists to degree bounds |
| Shared register products | Products of \(r\) current registers have budget \(t+r\) after \(t\) Toffolis; repeats and feedback are allowed |
| Balanced cut | An attainable prefix cost gives both sides cost at most \(\lceil T/2\rceil\); the complete family gives the beta bound |
| Affine-output circuit | Degree-one certificates compile to restored NOT/CNOT lists, giving zero extra Toffolis for every mask |
| Joint endpoint | The forward target at initial zero supplies \(f\); degree and optimized-cover conclusions are conjoined |
The strongest degree invariant concerns products of actual current registers. It does not duplicate the histories of shared controls. This is why its coordinate consequence applies to DAG reuse, temporary input modification and target feedback in this gate model. The general XOR–AND syntax argument in the main paper remains a separate written proof.
The general run theorem needs degree-one certificates for the initial register functions. The canonical boundary supplies these certificates; restoration is used later to identify the final target with \(f\). The affine existence theorem constructs gate lists inside its proof. It does not expose a separate executable compiler function or assert minimum total gate count.
The balanced cut and least-degree facts are established dependencies. They are not extra assumptions added to restored_degree_and_cover_bound. That endpoint assumes a legal gate list and restoration in the canonical boundary model. The register prints its full type as L107.