modularInterpret_zero
plain-language theorem explainer
The theorem shows that the modular interpretation of the base element of LogicNat (the identity) lands exactly at the zero element of the finite cyclic carrier Fin(modulus k) for any natural number k. Researchers constructing periodic models of the Law of Logic would cite this base case when verifying that the zero of the realization matches the interpreted identity. The proof reduces the claim via Fin.ext and applies the arithmetic fact that zero modulo any positive integer is zero.
Claim. For every natural number $k$, let $m = k+2$. The modular interpretation of the identity element of LogicNat equals the zero element of the finite set of size $m$, written as the pair whose first component is $0$ and whose second component is the proof that $0 < m$.
background
The module constructs periodic finite-cyclic realizations of Universal Forcing. The internal orbit stays free as LogicNat (the inductive type whose identity constructor is the zero-cost multiplicative identity and whose step constructor generates the orbit {1, γ, γ², …}), while the carrier is folded into a cycle of length modulus(k) = k + 2. The function modularInterpret(k, n) returns the value toNat(n) mod modulus(k) packaged inside Fin(modulus k), and modulus_pos supplies the positivity witness 0 < modulus k. The module doc states that this setup demonstrates Universal Forcing does not require every realization to embed arithmetic faithfully into the carrier.
proof idea
The proof applies Fin.ext to reduce the equality of Fin elements to an equality of their underlying natural numbers. It rewrites the left-hand side to 0 % modulus k by the definition of modularInterpret on the base element, then invokes Nat.zero_mod to obtain the required identity.
why it matters
The result supplies the base-case equality needed inside the definition of modularRealization, which builds a LogicRealization whose Carrier is Fin(modulus k) and whose zero element is exactly the pair ⟨0, modulus_pos k⟩. It thereby completes the periodic-interpretation construction in the ModularLogicRealization module and illustrates that the forcing chain permits non-faithful carrier embeddings while preserving the free LogicNat orbit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.