modular_interpret_periodic
plain-language theorem explainer
The theorem states that the modular interpretation map into a finite cyclic carrier is periodic with period given by the modulus. Researchers constructing finite models of the forcing chain cite it to confirm that the carrier wraps without altering the interpretation. The proof reduces the claim to an equality of underlying naturals via Fin.ext and then simplifies using the toNat_fromNat inversion lemma.
Claim. Let $I_k$ map the free orbit to the cyclic carrier $Fin(m(k))$ with $m(k)=k+2$. For any element $n$ of the free orbit, $I_k(fromNat(toNat(n)+m(k)))=I_k(n)$.
background
LogicNat is the inductive type whose constructors identity and step generate the free orbit under the generator, mirroring the smallest subset of positive reals closed under multiplication by γ and containing 1. The functions toNat and fromNat are the forward and inverse maps between this orbit and ℕ, with toNat_fromNat establishing that they are mutual inverses. modularInterpret(k,n) is defined by reducing toNat(n) modulo modulus(k) inside Fin(modulus(k)), where modulus(k):=k+2. The module provides a periodic finite-cyclic realization of Universal Forcing while keeping the internal orbit free, showing that not every realization must embed arithmetic faithfully into the carrier.
proof idea
The proof is a one-line wrapper that applies Fin.ext to equate the Fin elements by their underlying naturals. Simplification then unfolds modularInterpret and invokes toNat_fromNat to cancel the added modulus term.
why it matters
The result belongs to the ModularLogicRealization module, which supplies periodic finite-cyclic models for Universal Forcing. It verifies correct wrapping of the carrier interpretation even though the LogicNat orbit remains free. No downstream theorems are recorded, yet the lemma supports the broader claim that forcing admits non-faithful finite embeddings. It operates at the foundational level of the T0-T8 chain without invoking physical constants such as the alpha band or D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.