zmodCost_symm
plain-language theorem explainer
The equality cost on the cyclic group Z/nZ is symmetric for any natural number n. Researchers constructing modular realizations of logic cite this when verifying that the compare operation is invariant under argument swap. The proof proceeds by case analysis on whether the inputs coincide, followed by direct simplification from the definition.
Claim. For any natural number $n$ and elements $a,b$ in the cyclic group $Z/nZ$, the cost $c(a,b)$ equals $c(b,a)$, where $c(x,y)$ equals 0 if $x=y$ and 1 otherwise.
background
The Strict.Modular module realizes logic on the cyclic carrier ZMod n for n>1, with periodic interpretation and free-orbit arithmetic. The cost function zmodCost is defined to return 0 precisely when its arguments are equal and 1 otherwise; this supplies the compare field of both LogicRealization and StrictLogicRealization. The upstream definition of zmodCost in ModularRealization supplies the same indicator function on the cyclic group.
proof idea
Case analysis on whether a equals b. The equal case substitutes the hypothesis and simplifies the definition. The unequal case derives the symmetric inequality b ≠ a and simplifies the definition under both hypotheses.
why it matters
The result is invoked by modularRealization and strictModularRealization, which furnish the carrier and cost for logic realizations inside UniversalForcing. It supplies the symmetry axiom required by the meta-realization certificate and by the self-reference structure for. In the Recognition framework this is a prerequisite for the forcing chain before lifting to the phi-ladder or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.