intCost_self
plain-language theorem explainer
The equality cost on integers vanishes on the diagonal. Workers on order realizations in the Recognition Science foundation would invoke this to simplify zero-cost identities. The proof is a one-line simp wrapper that unfolds the definition of the cost function.
Claim. For every integer $a$, the cost function satisfies $cost(a,a)=0$, where the cost between two integers is defined to be zero precisely when they are equal and one otherwise.
background
The module develops order-theoretic realizations on the integers, using an equality-based cost function with unit steps. The cost function is defined by cases: it returns zero when the two arguments coincide and one otherwise. This lightweight carrier embeds the logic natural numbers into the integers while the arithmetic is handled by the internal orbit.
proof idea
The proof is a one-line wrapper that applies the simp tactic with the definition of the cost function.
why it matters
This basic identity is used to construct the ordered integer realization and its strict variant. It supports the zero-cost property required by the LogicRealization structure in the UniversalForcing module. In the Recognition framework it anchors the integer model before lifting to the phi-ladder and forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.