intCost_symm
plain-language theorem explainer
Symmetry of the integer equality cost function holds for the strict ordered realization on ℤ. Researchers constructing logic realizations cite this result to confirm that swapping arguments leaves the cost unchanged. The proof splits into cases on whether the arguments coincide and simplifies directly from the definition.
Claim. For all integers $a,b$, the equality cost satisfies $C(a,b)=C(b,a)$, where $C(a,b)=0$ if $a=b$ and $C(a,b)=1$ otherwise.
background
The module defines a strict ordered realization on the carrier ℤ equipped with Nat-valued costs. The cost function returns zero precisely on equal arguments and one otherwise. This construction sits inside the UniversalForcing layer and re-uses the same intCost definition appearing in the sibling OrderRealization module.
proof idea
Case analysis on a = b. The equal case substitutes and rewrites by the definition. The unequal case derives the symmetric inequality b ≠ a and rewrites by the definition in both branches.
why it matters
The symmetry is invoked by strictOrderedRealization to satisfy the StrictLogicRealization interface and by orderRealization to satisfy the LogicRealization interface. It supplies the required symmetry axiom for the ordered integer model used in the forcing-chain foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.