eqCost
plain-language theorem explainer
eqCost defines the two-valued equality cost on any decidably equal type K, returning zero for identical elements and one for distinct ones. Constructions that build LogicRealization from a single named distinction on an arbitrary carrier cite this as the comparison operator. The definition is a direct conditional on the equality test.
Claim. For any type $K$ equipped with decidable equality, the cost function $c:K×K→ℕ$ is defined by $c(a,b)=0$ if $a=b$ and $c(a,b)=1$ otherwise.
background
The module shows that any non-singleton carrier $K$ with a distinction $x≠y$ instantiates the Law-of-Logic realization interface directly on $K$. The two-valued equality cost serves as the comparison in this minimal LogicRealization, with the identity point and constant step map taken from the distinguishing pair. The module doc states that the construction is intentionally minimal and does not assert that every carrier has a native smooth real-valued J-cost; it proves only that Universal Forcing applies to the carrier and yields the same forced arithmetic object as the canonical realization.
proof idea
The definition is a direct if-then-else on the decidable equality test between the inputs, returning the natural number 0 or 1.
why it matters
eqCost supplies the comparison operator for logicRealizationOfDistinction, the universal instantiation theorem that equips any distinguished carrier with a LogicRealization. It supports the lemmas eqCost_self, eqCost_symm and eqCost_ne_one that establish the cost properties. In the Recognition framework this supplies the first universal step that every non-singleton carrier has the forced arithmetic object, reaching the continuous J/spacetime layer through realization-invariance rather than by assuming smoothness on arbitrary $K$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.