intCost
plain-language theorem explainer
Equality cost on integers returns zero for identical arguments and one otherwise. Researchers constructing ordered realizations for logic embeddings in Recognition Science cite this when building integer carriers with unit translation. The definition is given by a direct conditional on equality.
Claim. Let $c: ℤ × ℤ → ℕ$ satisfy $c(a,b) = 0$ whenever $a = b$ and $c(a,b) = 1$ otherwise.
background
The module defines a strict ordered realization on the integers that uses equality cost together with unit translation. The cost function serves as the compare operation inside the LogicRealization structure, returning zero precisely on equality. This mirrors the equality cost definition supplied by the upstream OrderRealization module, which states the same integer cost function.
proof idea
The definition is supplied directly by a conditional expression that branches on whether the two integer arguments are equal.
why it matters
The definition supplies the compare function for the ordered integer realization. It is invoked to establish the self-cost and symmetry theorems and to assemble the full LogicRealization instance. These results feed the strictOrderedRealization construction and support the embedding of logical structures into arithmetic carriers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.