The purpose and evidence contract
On this page · Permalink · Source line 1
This companion explains the actual Lean source behind the Circuit Obstructions main paper. It supplies the computational model, the meaning of its predicates, the route from legal gates to the joint lower bound, and all 115 indexed theorem types with exact source locations. The written arguments are explained for a mathematical reader; the source proof terms remain authoritative.
The formal source has 115 indexed theorem declarations across eight modules.
Current formal verification
Fresh source compilation, axiom inspection, and replay of all eight modules passed. All eight deliberately invalid or forbidden controls were rejected. The source package preserves the complete current receipt and logs alongside historical evidence.
The formal subset consists of C01, the maintained NCT sharing-degree dependency from F3, and the numerical lower-bound part of C02. C02's evaluation-span dual, affine-input invariance and general monotone ideal, together with C03–C08, remain outside this block. A theorem-name count is not a count of independent discoveries. Forty declarations were inherited and 75 added in Block 02.
| Part | Reader's task |
|---|---|
| Explanatory body | Check the hypotheses and how the predicates represent Boolean mathematics |
| Proof dependencies | Follow legal reversibility, cut coverage, shared degree, balancing and affine compilation |
| Evidence chapters | Distinguish written reasoning, exact finite checks, text scans and archived kernel checking |
| Declaration register | Inspect each complete elaborated type, file, line, block and axiom set |
The guide does not supply a new toolchain, an independent checker or independent human review. It preserves the original rights record and the original release files. There is no new publication-novelty or unrestricted hardness claim.