logicRealizationOfDistinction_composition
plain-language theorem explainer
On any carrier with two distinct points, the minimal distinction realization satisfies the triangle inequality for its two-valued equality cost. Anyone assembling a Law-of-Logic interface from a bare distinction needs this field discharged. The proof is a short case split: equal endpoints give cost zero; unequal endpoints force a unit cost on at least one leg of the path.
Claim. Let $K$ be a type with decidable equality and let $x,y\in K$ with $x\neq y$. Write $d(a,b)=0$ if $a=b$ and $d(a,b)=1$ otherwise. The logic realization built from the distinction $(x,y)$ satisfies additive composition: for all $a,b,c\in K$, $d(a,c)\le d(a,b)+d(b,c)$.
background
The module answers a skeptical gap in RealityFromDistinction: a bare distinction should instantiate the Law-of-Logic interface on its own carrier, not sit beside a pre-existing certificate. Given any $K$ and $x\neq y$, one builds a LogicRealization whose carrier is $K$, identity point $x$, step the constant map to $y$, and comparison the two-valued equality cost.
That cost, eqCost, is the discrete metric $d(a,b)\in{0,1}$ with $d=0$ iff $a=b$. The composition field of a logic realization is precisely the triangle inequality for this cost (additive path composition), not the multiplicative Recognition Composition Law used later for continuous $J$.
Upstream, eqCost_ne_one records that distinct inputs cost exactly one, and logicRealizationOfDistinction packages the whole interface. The continuous $J$/spacetime layer is reached only later by realization-invariance, not by treating arbitrary $K$ as $\mathbb{R}_{>0}$.
proof idea
Unfold the composition field to $\forall a,b,c,; d(a,c)\le d(a,b)+d(b,c)$ with $d=$ eqCost. Fix $a,b,c$ and case on $a=c$.
If $a=c$, then $d(a,c)=0$ by simplification of eqCost, and $0\le d(a,b)+d(b,c)$ is Nat.zero_le.
If $a\neq c$, then $d(a,c)=1$ by eqCost_ne_one. The intermediate point must split: $a\neq b$ or $b\neq c$, else $a=c$ by transitivity, contradiction. In the first subcase $d(a,b)=1$ and the other summand is nonnegative, so the sum is at least $1$; symmetrically in the second. Close both with omega.
why it matters
This discharges the additive composition slot of the minimal distinction realization, so every non-singleton carrier truly instantiates the Law-of-Logic interface and Universal Forcing can run on it. The module doc states the intended chain: instantiate the interface, apply Universal Forcing, obtain the same forced arithmetic object as the canonical recognition realization.
The doc-comment is explicit that this is not multiplicative composition consistency (L4). Equality cost provably fails L4 (equality_cost_insufficient_for_recognition); the slot is deliberately only the additive law that holds. That separation keeps the foundation honest: discrete distinction gives logic and arithmetic forcing, while continuous $J$ (T5 uniqueness, RCL) arrives through canonical realization-invariance, not by overclaiming on arbitrary carriers.
No downstream consumers are wired yet in the graph; the lemma exists to complete the LogicRealization record for the distinction construction and its sibling fields (excluded middle, action invariance).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.