zmodCost_self
plain-language theorem explainer
The cost function on the cyclic group ZMod n returns zero on equal arguments. Researchers building modular realizations for the UniversalForcing chain cite this to confirm the zero element of the cost. The proof is a one-line simp wrapper on the definition.
Claim. For any natural number $n$ and any $a$ in the cyclic group $Z/nZ$, the equality cost satisfies $cost(a,a)=0$, where $cost(x,y)$ equals 0 if $x=y$ and 1 otherwise.
background
The Strict.Modular module treats strict modular realizations on the periodic carrier ZMod n. The function zmodCost is defined by cases: if the two arguments are equal then 0, else 1. This definition appears both in the sibling module ModularRealization and locally in Strict.Modular.
proof idea
One-line wrapper that applies simp to the definition of zmodCost.
why it matters
The result is used by modularRealization and strictModularRealization to equip ZMod n with a LogicRealization and StrictLogicRealization. It supplies the required zero-cost property inside the UniversalForcing construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.