zmodCost
plain-language theorem explainer
zmodCost supplies the equality indicator as the compare operation on the cyclic carrier Z/nZ. Researchers building modular realizations of logic or forcing chains cite it to equip periodic carriers with a discrete cost. The definition is a direct conditional that returns zero precisely on equality and one otherwise.
Claim. For any natural number $n$, the function $c: (Z/nZ) × (Z/nZ) → ℕ$ is given by $c(a,b) = 0$ if $a = b$ and $c(a,b) = 1$ otherwise.
background
The module Strict/Modular.lean constructs strict modular realizations whose carrier is the cyclic group Z/nZ with periodic interpretation. The cost function serves as the compare field inside LogicRealization and StrictLogicRealization. The upstream definition in ModularRealization carries the identical doc-comment 'Equality cost on a cyclic carrier' and the same implementation.
proof idea
Direct definition via conditional expression on equality of the two ZMod elements.
why it matters
The definition populates the compare slot of modularRealization and strictModularRealization, which in turn supply the carrier and cost for strict modular realizations when n > 1. It therefore sits at the base of the periodic-carrier constructions inside the universal forcing development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.