The arithmetic bridge and restored-circuit model have executable Lean companions. Their coverage is explicit: the arithmetic package formalizes the fixed twelve-dimensional realization, while the circuit package formalizes legal reversible gates, cut coverage, the degree invariant with sharing, and the numerical complete-cover bound.
| Component | Formal scope | Current replay |
|---|---|---|
| Arithmetic bridge | 96 named theorems in five modules | PASS: fresh build, axiom inspection, five kernel replays. |
| Circuit obstructions | 115 indexed theorems in eight modules | PASS: fresh build, axiom inspection, eight kernel replays, eight rejected controls. |
A compiler pass checks elaboration of the source. Axiom inspection records its logical dependencies. Kernel replay rechecks the emitted declarations with Lean's kernel. Rejected controls test that the checking procedure detects specified invalid conclusions. These operations do not formalize the remaining prose merely because it appears in the same volume.
The general-modulus arithmetic theory, symmetry simulation theorems, catalytic gate theory, and the remaining circuit claims retain their stated written or finite computational evidence. The open research programs remain listed in their own chapters and appendices. This volume does not assert unrestricted quantum advantage, a general circuit lower bound, or complete Lean coverage of all its results.
The symmetry treatment also supplies an adaptive discarded-state certificate. Its written proof bounds the error by the sum of discarded norms on the computed trajectory. That result does not itself prove that the required packets or norm calculations remain polynomial in size.