no_confusion
plain-language theorem explainer
In the two-element type of Martin-Löf type theory (parsed as Bool), the constructors are disjoint: false is not equal to true. Anyone packaging type theory as a FormalSystem that realizes the δ core cites this. The proof is a one-line decidability check on Bool equality.
Claim. Writing $2$ for the canonical two-element type of Martin-Löf type theory (with closed terms $\mathsf{false}$ and $\mathsf{true}$), one has $\mathsf{false} \neq \mathsf{true}$.
background
The module parses Martin-Löf type theory into the minimal FormalSystem interface used by the Primitive Recognition Calculus (PRC) inevitability theorem. Tokens are closed terms of the two-element type; discrimination is term inequality; endpoints are the two constructors; expression order is derivation length.
Here the two-element type is abbreviated as Lean's Bool, whose closed terms are exactly false and true. A sibling canonicity result states that every closed term is one of those two constructors. The FormalSystem structure records carriers Token and Expr, a distinction relation, an expression-extension order, and endpoint tokens, so that δ becomes visible inside an arbitrary formal system.
No-confusion is the dual half of canonicity: not only are there at most two closed terms, they are actually distinct. That is the type theory's own discrimination verdict, not an external stipulation.
proof idea
One-line tactic proof: by decide. Equality on Bool is decidable, so the kernel discharges false ≠ true by computation. No lemmas are invoked; the recursor (or Boolean decision procedure) supplies the disjointness of constructors directly.
why it matters
This is the constructor-disjointness half of the faithful parse of type theory into PRC. The parent theorem type_theory_realizes_delta packages three facts: canonicity (every closed term of the two-element type is false or true), no-confusion (they are distinct), and a nonempty PRC embedding of the δ core into the type-theory formal system. Its doc-comment states: type theory's two-element type satisfies canonicity and no-confusion, and the foundation realizes the δ core.
In the Recognition framework this anchors the claim that ordinary constructive type theory already carries the minimal distinction structure PRC needs, before any physics-facing forcing (T5 J-uniqueness, T6 φ, T7 eight-tick, T8 D = 3) is applied. It is a small but load-bearing brick in the foundation layer that lets later inevitability arguments treat MLTT as a concrete FormalSystem rather than an informal metaphor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.