intCost_self
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not address costs between distinct integers.
- Does not generalize the carrier set beyond the integers.
- Does not incorporate the composition operation of the realization.
- Does not derive further arithmetic properties of the cost function.
Lean usage
example (a : ℤ) : intCost a a = 0 := intCost_self aformal statement (Lean)
18@[simp] theorem intCost_self (a : ℤ) : intCost a a = 0 := by
proof body
One-line wrapper that applies simp.
19 simp [intCost]
20