eqCost_self
plain-language theorem explainer
The two-valued equality cost vanishes on any element paired with itself inside a decidable carrier. Researchers constructing LogicRealizations from bare distinctions cite this identity as the zero-cost base case. The proof is a one-line simp wrapper that unfolds the definition of eqCost.
Claim. For any type $K$ equipped with decidable equality and any element $a$ of $K$, the two-valued equality cost satisfies $eqCost(a,a)=0$.
background
The module constructs a LogicRealization on an arbitrary carrier $K$ once a distinction $x≠y$ is given. The cost function is the two-valued equality cost, defined to return zero on equal inputs and one on distinct inputs. This supplies the minimal interface needed for the Law-of-Logic realization so that Universal Forcing applies directly to $K$.
proof idea
The proof is a one-line wrapper that applies the simp tactic to the definition of eqCost, which immediately reduces the equal case to zero.
why it matters
eqCost_self supplies the zero-cost identity required by logicRealizationOfDistinction, the universal instantiation theorem that turns any non-singleton carrier into a LogicRealization. The module doc states that this step lets Universal Forcing reach the same forced arithmetic object on every such carrier, without assuming a native smooth J-cost. It therefore closes the first link in the chain from distinction to the Recognition Science arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.