ttSystem_not_degenerate
plain-language theorem explainer
The MLTT formal system built on the two-element type is non-degenerate: its discrimination relation is nonempty. Anyone citing the three-foundations dichotomy (set theory, type theory, topos theory all on the δ side) needs this fact. The proof is a one-line application of the lemma that realizing the δ core forces discrimination.
Claim. The type-theory formal system (tokens $=$ closed terms of the two-element type $\mathbb{2}$, discrimination $=$ term inequality) is not degenerate: it is not the case that every pair of tokens fails to be distinguished.
background
In the Primitive Recognition Calculus, a formal system is a token set with a discrimination relation, an expression order, and designated endpoints. Degeneracy means the discrimination relation is empty: the foundation cannot tell any two objects apart.
The type-theory parse takes tokens to be closed terms of the two-element type $\mathbb{2}$, with discrimination as term inequality and endpoints the two canonical constructors. Canonicity says every closed term is one of those two constructors; no-confusion says they are distinct. The δ core is the minimal distinction structure (two endpoints that are distinguished); realizing δ means there is a structure-preserving embedding of that core into the formal system.
Upstream, realizing δ already entails non-degeneracy: the two cases are mutually exclusive, because the embedding preserves a distinguished pair.
proof idea
One-line wrapper. Apply not_degenerate_of_realizesDelta to ttSystem, feeding the already-proved fact that the type-theory system embeds (hence realizes) the δ core. That lemma unpacks the embedding witness and shows that degeneracy would contradict preservation of the distinguished pair.
why it matters
Feeds directly into three_foundations_not_degenerate, which packages the claim that the three named foundations (hereditarily finite set theory, this type-theory parse, and the elementary topos parse) all land on the δ side of the distinction dichotomy: none is degenerate.
In the Recognition Science foundation layer this is bookkeeping for the forcing chain: before J-uniqueness (T5), φ (T6), the eight-tick octave (T7), or D = 3 (T8) can be forced, the ambient formal systems must be shown capable of discrimination at all. Closing non-degeneracy for the type-theory parse removes the trivial counter-model in which MLTT distinguishes nothing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.