eqCost_ne_one
plain-language theorem explainer
In any type K with decidable equality, the two-valued equality cost between distinct elements a and b equals exactly one. Researchers building LogicRealization instances on arbitrary carriers cite this to confirm the binary distinction metric before invoking universal forcing. The proof is a one-line simplification that unfolds the cost definition and applies the inequality hypothesis directly.
Claim. Let $K$ be a type equipped with decidable equality. For distinct elements $a, b$ in $K$, the two-valued equality cost satisfies $eqCost(a, b) = 1$.
background
The module shows that any carrier with at least one distinction instantiates the Law-of-Logic realization interface on its own carrier. The two-valued equality cost serves as the comparison function, the identity point is a fixed base, and the step map is constant on the distinct point; the internal orbit is the free LogicNat structure. Upstream, LogicNat from ArithmeticFromLogic supplies the inductive orbit with identity as the zero-cost element and step as the generator iteration, mirroring the multiplicative orbit closed under the recognition step.
proof idea
The proof is a one-line wrapper that applies simplification to the eqCost definition together with the distinctness hypothesis.
why it matters
This result supplies the cost property needed to construct a LogicRealization on an arbitrary non-singleton carrier K, allowing the universal forcing chain to apply and yield the same forced arithmetic object as the canonical realization. It fills the initial universal step described in the module documentation before the lift to continuous J-cost via realization invariance. No downstream parents are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.