intCost_self
plain-language theorem explainer
The equality cost function on integers returns zero for any self-comparison. Researchers building discrete realizations in the Recognition Science foundation cite this as the base case establishing zero cost on the diagonal. The proof is a one-line wrapper that reduces directly via simplification to the cost definition.
Claim. For every integer $a$, if $c$ denotes the equality cost function on $ℤ$ defined by $c(a,b)=0$ when $a=b$ and $1$ otherwise, then $c(a,a)=0$.
background
The module constructs a strict ordered realization on the integers equipped with an equality cost and unit translation. The cost function returns 0 precisely on equal arguments and 1 otherwise, supplying the compare operation for the realization. Upstream, the definition of the equality cost on integers provides the concrete implementation that this theorem invokes.
proof idea
This is a one-line wrapper that applies the definition of the integer equality cost function via the simp tactic.
why it matters
This supplies the zero-cost self-comparison property required by the ordered integer realization and the strict ordered realization. It closes the diagonal case for the discrete setting, feeding the construction of LogicRealization and StrictLogicRealization on $ℤ$ with unit step. In the framework it supports the ordered structure used in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.