zmodCost
This definition supplies the binary cost on the cyclic group Z/nZ that vanishes exactly when two residues coincide and equals one otherwise. Constructions of modular and strict modular logic realizations cite it as the compare operation. It is realized by a direct conditional on equality of the arguments.
claimFor any natural number $n$, the equality cost on the cyclic group $Z/nZ$ is the function $c(a,b) = 0$ if $a=b$ and $c(a,b)=1$ otherwise.
background
The Strict.Modular module introduces strict modular realizations on the cyclic carrier ZMod n, where the carrier interpretation remains periodic and forced arithmetic is the derived free orbit. The upstream ModularRealization module defines the same object as the equality cost on a cyclic carrier. This cost is installed as the compare field in the LogicRealization structure.
proof idea
The definition is a direct case split on whether the two ZMod elements are equal, returning zero on equality and one otherwise. No lemmas or tactics are invoked; it is a primitive definition by cases.
why it matters in Recognition Science
It supplies the compare operation for modularRealization and strictModularRealization, which embed cyclic carriers into the LogicRealization and StrictLogicRealization framework. The definition supports the universal forcing chain by furnishing a minimal periodic carrier. Downstream results such as zmodCost_self and zmodCost_symm establish its reflexivity and symmetry.
scope and limits
- Does not define a metric or continuous distance.
- Does not reference the J-function or phi-ladder.
- Does not depend on forcing-chain steps T5-T8.
- Does not incorporate Recognition Composition Law directly.
formal statement (Lean)
17def zmodCost {n : ℕ} (a b : ZMod n) : Nat :=
proof body
Definition body.
18 if a = b then 0 else 1
19