zmodCost_symm
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not extend symmetry to non-cyclic or infinite carriers.
- Does not compute numerical values of the cost beyond the 0-1 indicator.
- Does not address composition, addition, or other operations on the cost.
- Does not prove that this cost is the unique or minimal symmetric function on ZMod n.
formal statement (Lean)
23theorem zmodCost_symm {n : ℕ} (a b : ZMod n) : zmodCost a b = zmodCost b a := by
proof body
Tactic-mode proof.
24 by_cases h : a = b
25 · subst h
26 simp [zmodCost]
27 · have h' : b ≠ a := by intro hb; exact h hb.symm
28 simp [zmodCost, h, h']
29
30/-- Strict modular realization for moduli `n > 1`. -/