modular_interpret_periodic
The modular interpretation of the free LogicNat orbit is periodic with period equal to the carrier size modulus k. Researchers building finite cyclic models for the forcing chain cite this to confirm that adding multiples of the modulus leaves the interpreted value unchanged. The proof is a direct term-mode application of Fin.ext followed by simplification using the definition of modularInterpret and the toNat_fromNat round-trip lemma.
claimFor any natural number $k$ and any element $n$ in the free orbit LogicNat, modularInterpret$(k, $fromNat$(toNat$(n) + modulus$(k))) = modularInterpret$(k, n)$, where modulus$(k) = k + 2$ and modularInterpret$(k, n)$ extracts the remainder of toNat$(n)$ modulo modulus$(k)$.
background
The module constructs periodic finite-cyclic realizations of Universal Forcing. The internal structure remains the free orbit LogicNat, built by iterated step constructors from identity and mirroring the multiplicative orbit generated by a fixed element greater than one. The carrier is the finite set Fin(modulus k) with modulus k defined as k + 2. The function modularInterpret maps each LogicNat element to its iteration count modulo the carrier size using the toNat projection.
proof idea
The proof applies the extensionality principle Fin.ext to reduce equality of Fin elements to equality of their underlying naturals. It then simplifies the left-hand side using the definition of modularInterpret and invokes the upstream round-trip lemma toNat_fromNat to cancel fromNat and toNat, reducing the claim to the standard modular arithmetic identity (m + modulus k) mod modulus k = m mod modulus k.
why it matters in Recognition Science
This result sits inside the construction of modular realizations and confirms the periodicity property required for the finite carrier. It supports the module claim that periodic interpretations suffice for Universal Forcing without faithful arithmetic embedding into the carrier. No downstream theorems currently depend on it, leaving open whether it will be invoked in proofs of invariance for the eight-tick octave structure.
scope and limits
- Does not establish injectivity of the modular interpretation.
- Does not extend to non-periodic or infinite carriers.
- Does not address compatibility with the Recognition Composition Law.
- Does not derive the specific value of modulus from the forcing chain steps.
formal statement (Lean)
108theorem modular_interpret_periodic (k : ℕ) (n : ArithmeticFromLogic.LogicNat) :
109 modularInterpret k
110 (ArithmeticFromLogic.LogicNat.fromNat
111 (ArithmeticFromLogic.LogicNat.toNat n + modulus k))
112 = modularInterpret k n := by
proof body
Term-mode proof.
113 apply Fin.ext
114 simp [modularInterpret, ArithmeticFromLogic.LogicNat.toNat_fromNat]
115
116end ModularLogicRealization
117end Foundation
118end IndisputableMonolith