logicRealizationOfDistinction_excludedMiddle
plain-language theorem explainer
On any carrier with two distinguishable points, the minimal distinction realization of the Law-of-Logic interface satisfies excluded middle: every pair of elements is either equal or unequal. Anyone citing universal instantiation from a bare distinction needs this field of the realization record. The proof is a one-line appeal to decidable equality via eq_or_ne.
Claim. For any type $K$ with decidable equality and any $x,y\in K$ with $x\neq y$, the Law-of-Logic realization built from the bare distinction $(x,y)$ satisfies excluded middle: for all $a,b\in K$, either $a=b$ or $a\neq b$.
background
The module Universal Instantiation from One Distinction repairs a skeptical gap in RealityFromDistinction. A bare distinction $x\neq y$ on a carrier $K$ should itself instantiate the Law-of-Logic realization interface, rather than sit beside a pre-existing canonical reality certificate.
The minimal construction equips $K$ with the two-valued equality cost as comparator, identity point $x$, and constant step map to $y$. The internal orbit is the free LogicNat orbit. It is intentionally thin: it does not claim a native smooth real-valued $J$-cost on arbitrary $K$. Excluded middle is one structural field of that interface (every pair is same-or-different).
The module's thesis is that every non-singleton carrier instantiates the Law-of-Logic interface, so Universal Forcing applies and forces the same arithmetic object as the canonical recognition realization. Continuous $J$/spacetime content arrives later via realization-invariance, not by treating $K$ as $\mathbb{R}_{>0}$.
proof idea
Unpack the excluded-middle field of the constructed realization to the goal $\forall a,b:K,\ a=b\lor a\neq b$. The carrier carries a DecidableEq instance, so Mathlib's eq_or_ne supplies the disjunction for every pair. The body is a pure term after a show: fun a b => eq_or_ne a b. No cost algebra or forcing lemmas are invoked.
why it matters
This lemma discharges one of the three structural obligations of the minimal distinction realization (with the composition and action-invariance siblings). It underwrites the claim that every non-singleton carrier instantiates the Law-of-Logic interface, the first universal step before Universal Forcing and realization-invariance reach the continuous $J$/spacetime layer.
Without excluded middle holding on the constructed object, the skeptical objection would stand: a bare distinction would not genuinely carry the logical content the interface demands. The result is local to the foundation layer. It does not itself force $\varphi$, the eight-tick octave (T7), or $D=3$ (T8), but it licenses applying those forcing theorems to any carrier that admits at least one distinction. The companion composition field deliberately carries only the additive triangle law; multiplicative L4 is known to fail for equality cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.