distinction_not_optional
plain-language theorem explainer
For any formal foundation whose expression order is reflexive, realizing the δ core is equivalent to distinguishing at least one pair of tokens; the foundation is either fully degenerate or realizes δ; and realizing δ excludes degeneracy. Cited by the δ-program shrunk certificate as the δ4 headline. The proof packages the dichotomy with the two directions of the realizes-δ / discriminating equivalence via existing local lemmas.
Claim. Let $F$ be a formal system whose expression-extension relation is reflexive. Then: (i) $F$ admits a PRC embedding into its own interface if and only if $F$ distinguishes at least one pair of tokens; (ii) either $F$ distinguishes nothing, or $F$ admits such an embedding; (iii) if $F$ admits the embedding, then $F$ is not degenerate.
background
The Primitive Recognition Calculus (PRC) studies when an arbitrary formal foundation is forced to host the δ core (a minimal recognition structure). The carrier is FormalSystem: types of tokens and expressions, a discrimination relation on tokens, an expression-extension order, and endpoint tokens. Degeneracy means the discrimination relation is empty; discrimination means some pair of tokens is told apart. Realizing δ means there is a nonempty PRC embedding into the system's own interface.
Expression reflexivity (every expression extends itself) is the mild structural hypothesis; it holds for any "derivable-from" or "extends" order. Upstream, the dichotomy theorem already shows that under reflexivity a foundation is either degenerate or realizes δ, by case-splitting on whether it discriminates and routing through the embedding construction from a discriminating pair.
This module packages those facts into the δ4 headline: distinction is not optional except for the empty-discrimination foundation, which cannot state a nontrivial proposition.
proof idea
Term-mode refine builds a triple. The second and third conjuncts are direct applications of distinction_dichotomy (under reflexivity) and not_degenerate_of_realizesDelta.
The first conjunct is the biconditional RealizesDelta ↔ Discriminating. Forward: from a realization, not_degenerate_of_realizesDelta gives non-degeneracy, then not_degenerate_iff_discriminating converts that to Discriminating. Backward: realizesDelta_of_discriminating builds the PRC embedding from a discriminating pair, using reflexivity of expression extension.
No new case analysis; the work is already in the local lemmas.
why it matters
This is the δ4 headline of the PRC inevitability program: the only foundation that escapes δ is the one that distinguishes nothing at all. Downstream it feeds prc_shrunk_certificate and the PRCShrunkCertificate structure, which packages seven proved headlines with no axioms and no sorry ("The δ program certificate holds").
In the broader Recognition Science forcing chain, δ is the primitive recognition act that later feeds cost, the J-functional uniqueness (T5), and the self-similar fixed point φ (T6). Establishing that any non-vacuous reflexive foundation must realize δ closes the "distinction is optional" escape hatch before those later steps. The companion facts that named foundations (set theory, type theory, etc.) are non-degenerate sit in the same module and make the hypothesis mild in practice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.