3.8. Zero-Axiom Policy🔗

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

This means the formal guarantees are as strong as the Lean kernel itself: if the kernel accepts the proofs, the properties hold.