zmodOrbitInterpret
zmodOrbitInterpret maps each LogicNat element to its residue in ZMod n by extracting the iteration count via toNat. Workers constructing finite cyclic carriers for the universal forcing would invoke this map inside modularRealization. The definition is a direct one-line coercion from the inductive orbit counter into the modular integers.
claimFor modulus parameter $n$ and element $k$ of the inductive type generated by identity and step, the map sends $k$ to the class of toNat$(k)$ in $ZMod n$.
background
LogicNat is the inductive type whose constructors identity and step generate the smallest orbit closed under multiplication by the generator, with toNat reading off the step count (identity maps to 0). ZMod n supplies the finite cyclic carrier whose elements are residue classes modulo n. The module document states that the carrier is ZMod n equipped with equality cost, so that the semantic orbit may close after finitely many iterations while still realizing the universal iteration object.
proof idea
One-line definition that applies LogicNat.toNat to obtain a natural number and coerces the result into ZMod n.
why it matters in Recognition Science
The map is invoked by modularRealization to equip ZMod n with a LogicRealization instance. It therefore supplies the concrete interpretation of the forced arithmetic inside any nontrivial cyclic carrier, supporting the modular arithmetic invariant that appears downstream in the same file. The construction aligns with the Recognition Science requirement that the universal iteration object be realizable in both infinite and finite settings.
scope and limits
- Does not verify that the induced structure satisfies the full LogicRealization axioms.
- Does not define or compute any cost function on the carrier.
- Does not extend the map to non-cyclic groups or infinite carriers.
- Does not address the case of modulus 1.
formal statement (Lean)
33def zmodOrbitInterpret (n : ℕ) (k : LogicNat) : ZMod n :=
proof body
Definition body.
34 (LogicNat.toNat k : ZMod n)
35
36/-- Modular realization for any nontrivial modulus. -/