intCost
plain-language theorem explainer
The equality cost function on integers returns zero precisely when its arguments coincide and one otherwise. Researchers on order realizations in the UniversalForcing foundation cite it as the compare operation for the integer carrier. The definition is introduced by a direct conditional on equality.
Claim. Let $c : ℤ × ℤ → ℕ$ satisfy $c(a,b) = 0$ if $a = b$ and $c(a,b) = 1$ otherwise.
background
The OrderRealization module supplies an order-theoretic realization on the integers with equality cost and unit step. This is a lightweight realization: forced arithmetic is carried by the certified internal orbit while the carrier uses the standard embedding of LogicNat into ℤ.
proof idea
The definition is given directly by cases on whether the two integers are equal.
why it matters
It supplies the compare operation for the ordered integer realization. This feeds the self-cost and symmetry theorems together with the main realization definition, supporting the lightweight integer case in the UniversalForcing construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.