modularInterpret_step
plain-language theorem explainer
The theorem shows that modular interpretation of a logic natural commutes with successor by reducing to a cyclic increment on the finite carrier Fin(modulus k). Researchers constructing periodic realizations of the Law of Logic cite it when building finite models that separate the internal orbit from the carrier. The term proof reduces the claim via Fin.ext to an identity on Nat, then applies toNat_succ together with add_mod and the bound one_lt_modulus.
Claim. For any natural number $k$ and logic natural $n$, the modular interpretation of the successor of $n$ equals the cyclic step of $k$ applied to the modular interpretation of $n$.
background
The module develops periodic finite-cyclic realizations of Universal Forcing. LogicNat is the inductive type whose constructors identity and step generate the free orbit under the generator, with toNat counting iterations so that toNat(succ n) equals toNat(n) plus one. modularInterpret sends each logic natural to an element of Fin(modulus k) by reducing the iteration count modulo the period, while cycStep implements the corresponding cyclic successor on that finite set.
proof idea
The term proof begins with Fin.ext to equate the underlying naturals. It rewrites the left-hand side via toNat_succ and succ_eq_add_one, then invokes the symmetry of add_mod to match the right-hand side. The final simpa uses one_lt_modulus to confirm the representative stays inside the modulus.
why it matters
This result is invoked inside the definition of modularRealization, which equips the finite carrier Fin(modulus k) with the required LogicRealization structure. It illustrates the module's central point that Universal Forcing permits periodic carrier interpretations without faithful arithmetic embedding. The construction sits downstream of the ArithmeticFromLogic development of LogicNat and feeds the broader exploration of distinct realizations along the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.