distinction_dichotomy
plain-language theorem explainer
Any formal foundation whose expression order is reflexive is either degenerate (distinguishes no tokens) or realizes the δ core via a PRC embedding. Cited by the δ4 headline that distinction is not optional, and by the shrunk PRC certificate. Proof is a two-branch case split on whether the foundation discriminates at least one pair, using the discriminating-to-embedding lemma on one side and the empty-discrimination definition on the other.
Claim. Let $F$ be a formal system whose expression-extension relation is reflexive. Then either $F$ is degenerate (its discrimination relation on tokens is empty) or $F$ realizes $\delta$ (there exists a PRC embedding into $F$'s interface).
background
The Primitive Recognition Calculus (PRC) studies when an arbitrary formal foundation is forced to host the δ core. A FormalSystem is a minimal interface: carriers Token and Expr, a discrimination relation on tokens, an expression-extension order, and a map from endpoints to tokens. Degeneracy means the discrimination relation is empty: no two tokens are told apart. Discrimination is the existential dual: at least one distinguished pair. Realizing δ means there is a nonempty PRC embedding into that interface.
Expression reflexivity is the mild structural hypothesis that every expression extends itself. It holds for any "derivable-from", subset, or extends-style order, and is the only extra assumption beyond the formal-system signature.
Locally this module packages the dichotomy that feeds the δ4 headline: distinction is not optional except for the fully degenerate foundation, which cannot express a nontrivial proposition.
proof idea
Tactic proof by cases on whether $F$ is discriminating.
If it is, apply realizesDelta_of_discriminating (which needs expression reflexivity) to obtain a PRC embedding, hence RealizesDelta, and take the right disjunct.
If it is not, the negation of "exists a distinguished pair" is exactly "for all tokens $a,b$, not distinguished", which is the definition of Degenerate; take the left disjunct.
No further algebraic work: the split is exhaustive because discrimination and its negation partition the possibilities, and degeneracy is definitionally that negation.
why it matters
This is the middle clause of the δ4 headline assembled in distinction_not_optional: for reflexive foundations, realizing δ is equivalent to discriminating, the foundation is degenerate or realizes δ, and realizing δ rules out degeneracy. The only escape from δ is total nondiscrimination, which cannot host a nontrivial proposition.
Downstream it is also consumed by prc_shrunk_certificate, the seven-headline certificate that the δ program holds with no axioms and no sorry. In the Recognition forcing picture this sits under the foundation layer that feeds the chain (T0–T8): once a nondegenerate foundation is forced to realize δ, the cost and ladder structure that produce $J$, $\varphi$, the eight-tick octave, and $D=3$ can attach.
It does not itself construct the embedding or force physics constants; it only locks the dichotomy that makes distinction mandatory for any usable foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.