zmodOrbitInterpret
plain-language theorem explainer
zmodOrbitInterpret maps each LogicNat element to its iteration count inside ZMod n. Researchers constructing finite cyclic carriers for universal forcing cite this map when realizing arithmetic orbits modulo a nontrivial modulus. The definition is a direct coercion of the toNat count into the cyclic group.
Claim. The function sending natural number $n$ and LogicNat element $k$ to the residue class of toNat$(k)$ in $Z/nZ$.
background
LogicNat is the inductive type with constructors identity (the zero-cost multiplicative identity) and step (one iteration of the generator), forming the smallest orbit closed under multiplication by the generator and containing 1. toNat reads off the iteration count by recursion on this structure. The module sets the carrier to ZMod n with equality cost, allowing the semantic orbit to close inside the finite group while the forced arithmetic remains the universal iteration object.
proof idea
One-line definition that applies toNat to the LogicNat argument and coerces the resulting natural number into ZMod n.
why it matters
This supplies the orbit map required by modularRealization to build a LogicRealization instance on ZMod n for any n > 1. It completes the modular side of the self-reference structure in UniversalForcing, linking the LogicNat orbit to the cyclic carrier used in the forcing chain (T5 J-uniqueness through T8 D=3). It addresses the closure of orbits inside finite carriers without altering the underlying arithmetic axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.