zmodCost_symm
plain-language theorem explainer
The equality cost on the cyclic carrier ZMod n is symmetric in its arguments. Researchers building finite models of the LogicNat orbit cite this when confirming that the compare operation satisfies the axioms of a LogicRealization. The proof applies case analysis on whether the two elements coincide and reduces both sides to the same constant by simplification.
Claim. For every natural number $n$ and all $a,b$ in the cyclic group $Z/nZ$, the equality cost $c(a,b)$ equals $c(b,a)$, where $c(x,y)$ returns $0$ if $x=y$ and $1$ otherwise.
background
The module constructs modular realizations of the universal forcing on the finite cyclic carrier ZMod n. The cost function returns zero precisely when its arguments are identical and one otherwise, furnishing a discrete model in which the semantic orbit generated by LogicNat may close. LogicNat itself is the inductive type whose constructors identity and step encode the zero-cost element and successive iterations of the generator, mirroring the orbit closed under multiplication by the golden ratio.
proof idea
The proof uses case distinction on whether a equals b. When the elements coincide, substitution followed by simplification of the definition reduces both sides to zero. When they differ, the symmetric inequality is introduced and both sides simplify to one.
why it matters
Symmetry of the cost is required by the compare field of modularRealization, which assembles a LogicRealization with carrier ZMod n and cost type Nat. The same fact is invoked by strictModularRealization. In the Recognition framework this lemma closes the symmetry requirement for the modular step of the forcing chain, ensuring the finite carrier supports the orbit interpretation without directional bias.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.