zmodCost_self
The equality cost on the cyclic carrier ZMod n vanishes on the diagonal. Researchers constructing modular realizations in the Recognition Science foundation cite this to anchor the zero element of the cost function. It follows by direct simplification from the piecewise definition of zmodCost.
claimFor any natural number $n$ and element $a$ in the cyclic group $ZMod n$, the equality cost function $c$ satisfies $c(a,a)=0$, where $c(a,b)$ equals 0 if $a=b$ and 1 otherwise.
background
The Strict.Modular module equips the cyclic group ZMod n with a cost function for strict modular realizations. The function zmodCost is defined by cases: it returns 0 precisely when the two arguments coincide and 1 otherwise. This realizes the universal forcing on a periodic carrier whose arithmetic is the free orbit under addition, consistent with the module's description of forced arithmetic remaining the derived free orbit.
proof idea
The proof is a one-line wrapper that applies simp to the definition of zmodCost, which immediately reduces the diagonal case to zero.
why it matters in Recognition Science
This result supports the definitions of modularRealization and strictModularRealization, which instantiate LogicRealization and StrictLogicRealization on cyclic groups. It supplies the zero-cost property required for these concrete models in the Recognition Science foundation, aligning with the periodic carrier interpretation used in the universal forcing chain.
scope and limits
- Does not compute the cost between distinct elements of ZMod n.
- Does not extend the zero-cost property to non-cyclic carriers.
- Does not establish symmetry or triangle inequality for the cost function.
- Does not link the cost to J-cost, phi-ladder, or spatial dimension forcing.
Lean usage
example {n : ℕ} (a : ZMod n) : zmodCost a a = 0 := by simp [zmodCost_self]formal statement (Lean)
20@[simp] theorem zmodCost_self {n : ℕ} (a : ZMod n) : zmodCost a a = 0 := by
proof body
One-line wrapper that applies simp.
21 simp [zmodCost]
22