Verification and proof boundaries
On this page · Permalink · Source line 184
UNIVERSAL PROOFS AND FINITE CONTROLS REMAIN DISTINCT
| Module | Count | Formal role |
|---|---|---|
| Gates | 16 | Inherited legal primitives and reversal |
| CutComparison | 13 | Inherited complete cut cover |
| Examples | 11 | Inherited dirty and output-active controls |
| Degree | 19 | Polynomial certificates and closure |
| MultiplicativeDegree | 12 | Degree invariant with sharing |
| SafeDegree | 22 | Least complete degree and balanced cuts |
| AffineOutput | 14 | Affine compiler and optimized bound |
| DegreeChecks | 8 | AND2 exclusion and exact parameters |
| Total | 115 | 75 new declarations, 40 inherited |
The current audit rebuilt all source in a fresh project directory, treated warnings as errors, printed each declaration's type and axiom dependencies, and replayed all eight modules through the bundled checker. Its eight deliberately invalid or forbidden controls were rejected.
Only propext, Classical.choice, and Quot.sound occur in the archived audited dependencies. No custom axiom, admitted proof, native-decision oracle, or kernel bypass is used. Lean 4.34.0-rc2 and its bundled Std are pinned. This checker shares the toolchain's trust boundary and is not an independent implementation or human review.
The separate Python checker, freshly reproduced in this edition, uses exact truth tables and integer Möbius transforms. It covers all 278 functions on zero through three inputs; all words over the documented 12-gate three-wire alphabet through length three and the 28-gate four-wire alphabet through length two (2,698 words); 28,088 register-product checks; and 251 restored words. The universal theorems do not follow by extrapolation from those finite tests.
What remains outside the formal block
On this page · Permalink · Source line 204
C02's evaluation-span dual, affine input invariance, and general monotone ideal are not formalized. C03–C08 retain their previous written and finite-check status. The original classical/reversible circuit-size comparison and general exact monomial-cost theorem are not newly formalized. The active claim register controls interpretation.