zmodCost
plain-language theorem explainer
zmodCost equips each cyclic group ZMod n with a binary cost that vanishes exactly when its arguments coincide. Researchers constructing finite models of logic cite it to supply the compare operator inside LogicRealization. The definition is introduced by a direct conditional on equality of the two elements.
Claim. The function $c_n : (Z/nZ) × (Z/nZ) → ℕ$ is given by $c_n(a,b) = 0$ if $a = b$ and $c_n(a,b) = 1$ otherwise.
background
The module treats the cyclic group ZMod n as carrier together with an equality-based cost. This produces a finite realization in which the semantic orbit may close while still certifying the universal iteration object. The identical case distinction appears upstream in the Strict.Modular module to support the strict variant of the same construction.
proof idea
Direct definition by case distinction on equality of the arguments in ZMod n.
why it matters
The definition supplies the compare field for modularRealization and strictModularRealization, thereby instantiating both LogicRealization and StrictLogicRealization on cyclic carriers. It therefore supports the modular arithmetic invariant required by the Recognition framework for finite models. The construction touches the open question of how such finite carriers embed into the infinite forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.