intCost
The intCost definition supplies the equality-based cost function on the integers for order realizations in the Recognition Science framework. Researchers modeling discrete order structures with unit-step costs reference this when building LogicRealization instances on ℤ. It is realized as a direct conditional expression that returns zero on equality and one otherwise, serving as the base for symmetry and self-cost lemmas.
claimDefine the function $intCost : ℤ × ℤ → ℕ$ by $intCost(a,b) = 0$ if $a = b$ and $intCost(a,b) = 1$ otherwise.
background
The OrderRealization module supplies a lightweight order-theoretic realization on the carrier ℤ. The module doc states that forced arithmetic is carried by the certified internal orbit while the carrier interpretation is the usual embedding of LogicNat into ℤ. This definition provides the compare operation with equality cost and unit step, matching the identical construction in the Strict.Ordered submodule to ensure consistency across order variants.
proof idea
This is a direct definition via conditional expression: zero when the arguments are equal, one otherwise. No lemmas or tactics are invoked; the expression itself is the complete body and immediately supports the simp lemmas intCost_self and intCost_symm that follow.
why it matters in Recognition Science
This definition is the compare field inside the orderRealization instance, which realizes ordered integer structures for UniversalForcing. It supplies the concrete cost needed for downstream symmetry and self-cost theorems, anchoring the integer case in the forcing chain before applications of the Recognition Composition Law. The construction directly supports the T5 J-uniqueness step by furnishing a minimal discrete cost compatible with the phi-ladder.
scope and limits
- Does not extend the cost function to real numbers or other carriers.
- Does not incorporate any distance measure beyond strict equality.
- Does not define the full LogicRealization record or its zeroCost instance.
- Does not handle non-integer inputs or continuous orderings.
Lean usage
example (a b : ℤ) : intCost a b = 0 ∨ intCost a b = 1 := by cases a == b <;> simp [intCost]formal statement (Lean)
20def intCost (a b : ℤ) : Nat :=
proof body
Definition body.
21 if a = b then 0 else 1
22