modularInterpret
plain-language theorem explainer
modularInterpret projects each element of the free LogicNat orbit onto a residue in the cyclic carrier of size k+2. Researchers building periodic realizations of Universal Forcing cite the map to keep the internal orbit free while rendering the carrier finite and periodic. The definition is a one-line construction that extracts the iteration count via toNat, reduces modulo the carrier size, and attaches the positivity witness.
Claim. For each natural number $k$, the periodic interpretation map sends an element $n$ of the free orbit to the residue of its iteration count modulo $k+2$ inside the finite set of size $k+2$.
background
LogicNat is the inductive type with constructors identity (the zero-cost element) and step, generating the free multiplicative orbit; toNat extracts the iteration depth as a natural number. The modulus function returns $k+2$ as carrier size, and modulus_pos proves this size is positive for every natural $k$ (via unfolding and omega).
proof idea
This is a one-line wrapper that applies toNat to obtain the iteration count, reduces the result modulo modulus k, and packages the outcome with the witness from modulus_pos that the modulus is positive.
why it matters
The map supplies the interpretation used to build modularRealization, the finite cyclic Law-of-Logic realization. It directly enables the periodicity theorem, the step case, and the zero case. The construction shows that Universal Forcing permits periodic carriers without faithful arithmetic embedding into the carrier, as stated in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.