zmodCost_self
plain-language theorem explainer
Equality cost on the cyclic carrier ZMod n returns zero on the diagonal. Constructions of modular realizations cite the result to confirm the zero element of the cost structure. The proof is a one-line simp reduction on the definition of the cost.
Claim. For any natural number $n$ and any element $a$ of the cyclic group of integers modulo $n$, the equality cost satisfies $cost(a,a)=0$, where $cost$ is the indicator that returns zero precisely on equal arguments.
background
The module supplies a modular realization of logic whose carrier is the cyclic group ZMod n equipped with an equality cost. The cost function is defined to return zero when its two arguments coincide and one otherwise. This supplies the compare operation inside the LogicRealization structure and permits the semantic orbit to close inside the finite carrier.
proof idea
One-line wrapper that applies simp to the definition of the cost function.
why it matters
The lemma is invoked inside the definitions of modularRealization and strictModularRealization, which instantiate LogicRealization and StrictLogicRealization on cyclic carriers. It supplies the self-cost property required for the zeroCost field in those structures and thereby supports the modular arithmetic invariant used in the universal forcing construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.