modularInterpret_zero
plain-language theorem explainer
The modular interpretation of LogicNat's identity element equals the zero of the finite cyclic carrier Fin(k+2) for any k. Researchers building periodic realizations of Universal Forcing cite this base case. The proof is a term-mode wrapper that applies Fin.ext followed by the arithmetic identity zero modulo any positive integer.
Claim. For every natural number $k$, the periodic map sending the identity element of the free orbit to the cyclic carrier of size $k+2$ yields the zero element of that carrier: modularInterpret$(k,0)=0$ in Fin$(k+2)$.
background
The module supplies periodic finite-cyclic carriers for Universal Forcing while the internal orbit remains the free LogicNat type. LogicNat is the inductive type whose identity constructor is the zero-cost element and whose step constructor generates the orbit under multiplication by the generator; its doc-comment states it is 'the natural numbers as forced by the Law of Logic.' modularInterpret$(k,n)$ reduces the natural-number value of $n$ modulo modulus$(k)=k+2$ inside Fin$(k+2)$, with modulus_pos supplying the positivity witness. The local setting is given by the module doc: 'Periodic finite-cyclic realization for Universal Forcing. The internal orbit is still free (LogicNat), while the carrier interpretation is periodic.'
proof idea
Term-mode proof applies Fin.ext to equate the underlying naturals, rewrites the definition of modularInterpret to obtain the goal 0 % modulus k = 0, then closes with the lemma Nat.zero_mod.
why it matters
The result supplies the zero case for modularRealization, the finite cyclic Law-of-Logic realization whose doc-comment describes it as 'Finite cyclic Law-of-Logic realization with periodic interpretation.' It directly illustrates the module claim that Universal Forcing does not require every realization to embed arithmetic faithfully into the carrier, closing the base case inside the Foundation layer before the eight-tick octave and D=3 steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.