intCost_symm
plain-language theorem explainer
The equality cost on integers, returning zero exactly when arguments coincide and one otherwise, is symmetric under swap. Researchers constructing order realizations of the forced arithmetic cite this to confirm the compare operation is undirected on the integer carrier. The proof proceeds by case analysis on equality, with substitution and simplification discharging both branches.
Claim. For all integers $a$ and $b$, the equality cost of $a$ and $b$ equals the equality cost of $b$ and $a$, where equality cost is zero if the arguments coincide and one otherwise.
background
The OrderRealization module supplies a lightweight order-theoretic realization of the forced natural numbers on the integers. LogicNat is the inductive type with constructors identity (zero-cost element) and step (one iteration of the generator), mirroring the orbit closed under multiplication by the generator and containing the multiplicative identity. The intCost function supplies the compare operation by returning zero on equality and one on inequality, embedding LogicNat into ℤ while preserving the certified arithmetic structure.
proof idea
The tactic proof opens with by_cases on whether a equals b. The equal branch substitutes and simplifies using the intCost definition. The unequal branch constructs the symmetric inequality b ≠ a and simplifies the goal with both inequalities.
why it matters
This lemma is invoked by orderRealization to equip the integer carrier with a symmetric cost and by strictOrderedRealization in the Strict.Ordered submodule. It supplies a basic consistency requirement for the compare field in the LogicRealization structure, supporting the arithmetic realization step in the forcing chain. No open scaffolding questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.