ofTwoDistinct_exprReflexive
plain-language theorem explainer
Any formal system built from two distinct tokens has a reflexive expression order: every finite-trace length extends itself under ordinary length comparison. Cited when placing the two-token inevitability instance on the non-degenerate side of the PRC distinction dichotomy. The proof is a one-line term applying reflexivity of natural-number order.
Claim. For any type $\alpha$ and distinct $a_0,a_1\in\alpha$, the formal system with tokens $\alpha$, expressions $\mathbb{N}$ (finite-trace lengths), and expression extension $m\preceq n\iff m\le n$ is expression-reflexive: $\forall e,\, e\preceq e$.
background
In the Primitive Recognition Calculus (PRC) distinction module, a formal system packages tokens, expressions, a distinguishability relation, and an expression-extension preorder. Expression-reflexivity means every expression extends itself; the module notes this holds for any "is-derivable-from", "$\subseteq$", or "extends" relation.
The two-distinct construction builds a minimal formal system from any type with two unequal primitives: tokens are the type's elements, expressions are natural numbers (trace lengths), extension is the usual order $\le$ on $\mathbb{N}$, and endpoints pick one or the other primitive by side. Distinguishability is plain inequality of tokens.
The local setting is the distinction dichotomy: foundations are either degenerate or discriminating (hence realize the $\delta$ core via a PRC embedding). Reflexivity of the expression order is a basic structural fact needed before non-degeneracy and $\delta$-realization arguments for concrete instances.
proof idea
Term-mode proof. Unfold expression-reflexivity on the two-distinct instance: one must show $\forall n:\mathbb{N},, n\le n$ under the instance's exprExtends. Supply the witness fun n => Nat.le_refl n. No case split, induction, or PRC-specific lemma is required; the claim reduces exactly to reflexivity of $\le$ on natural numbers.
why it matters
Places the canonical two-token inevitability instance on the structural side needed for the distinction dichotomy: once expression order is reflexive, the instance can be checked for non-degeneracy and $\delta$-realization alongside the named foundations (logic, arithmetic, set theory, type theory), which the module records as all falling on the $\delta$ side.
No downstream uses are wired yet in the graph, so this is a leaf lemma in the present build. It still closes a required interface obligation for ofTwoDistinct before distinction_not_optional and named_foundations_not_degenerate style results can treat that instance uniformly with other foundations. In the broader RS forcing chain this is pure foundation scaffolding (pre-T5), not a physics constant claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.