3.8. Zero-Axiom Policy🔗

The project uses zero axioms beyond Lean's built-in foundations (propext, Quot.sound, Classical.choice). No partial def is used — every function has a kernel-checked termination proof.

The released scanner, parser, and soundness layers are entirely sorry-free. One frontier remains in progress: the emitter round-trip property (§Round-Trip Properties, headline 6.1 universal_roundtrip) currently carries 4 sorry markers — two base content-equality steps and two flow-subrange structure obligations — which feed the in-progress universal_roundtrip capstone. These are tracked explicitly and surfaced with a 🚧 marker wherever a headline depends on them; no other theorem in the catalogue is sorry-reachable.

This means the formal guarantees are as strong as the Lean kernel itself: for every theorem not flagged 🚧, if the kernel accepts the proof, the property holds with no escape hatch.