zmodOrbitInterpret
plain-language theorem explainer
zmodOrbitInterpret embeds each element of LogicNat into ZMod n by sending it to the residue of its iteration count. It is invoked when building finite cyclic carriers for the modular realization of the forced arithmetic. The definition is a direct one-line coercion via the toNat map on LogicNat.
Claim. The map sending each $k$ in LogicNat to the class of toNat$(k)$ in $ZMod n$, where toNat extracts the iteration depth starting from identity at zero.
background
LogicNat is the inductive type with constructors identity (zero-cost element) and step (one further iteration of the generator), mirroring the orbit closed under multiplication by the generator. The toNat function reads off the iteration count as a natural number. In this module the carrier is ZMod n with n given by modulus (k+2), and the orbit is realized inside the finite cyclic group where it may close.
proof idea
One-line wrapper that applies LogicNat.toNat to obtain the natural-number index and coerces the result into ZMod n.
why it matters
modularRealization applies this definition to equip ZMod n with a LogicRealization structure. It supplies the concrete interpretation of the universal iteration object inside a finite carrier, consistent with the orbit/step coherence axioms recorded in UniversalForcingSelfReference. The construction sits inside the modular arithmetic invariant that supports the broader forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.