Claim 1 · formal composition
0 hidden imports
Source inclusions are explicit hypotheses. Lean checks extensional equivalence and exact preservation of every old residual coordinate under width padding.
Theorem 4.2: kernel-checked repair
Lean 4.32 reproduction audit · nBuL6HywFX · two universal circuit-class equalities
Claim 2 · universal repair
3 exact theorems
For arbitrary positions and scores: layer 1 selects source, layer 2 collects destination, and the printed source route is rejected whenever source ≠ gate.
Fail-closed kernel gate
no sorryAx
The checker rejects proof escapes, pins Lean 4.32, hashes the source, and parses every #print axioms report.
Constant-width repair
6 coordinates
Self, source, and gate use exactly six pointer coordinates independent of input length; threshold arithmetic and induction close universally.