modularRealization
plain-language theorem explainer
Modular realization supplies a cyclic carrier ZMod n for the forced logic structure whenever n exceeds 1. It is cited by work on finite models of universal arithmetic to embed the LogicNat orbit into a finite ring. The construction directly assembles the record by setting the carrier to ZMod n, the orbit to LogicNat, and verifying the interpretation commutes with successor via toNat_succ and norm_num.
Claim. For any natural number $n>1$, the modular realization is the structure with carrier the cyclic group $Z/nZ$, cost function the natural numbers under equality, zero element $0$, successor map $zmapsto z+1$, and orbit identified with the forced naturals via the canonical projection $LogicNat to Z/nZ$.
background
The module defines modular realizations of the forced arithmetic. The carrier is the finite ring of integers modulo $n$ for $n>1$, equipped with the natural-number cost function. The semantic orbit is the inductive type LogicNat whose constructors are the zero-cost identity and the successor step; this type encodes the smallest subset of positive reals closed under multiplication by the generator and containing 1. The interpretation map sends each LogicNat element to its residue class in ZMod n, and the required axioms (zero preservation, successor commutation, injectivity, induction) are discharged by direct computation on the toNat projection and the ring operations.
proof idea
The definition populates every field of the LogicRealization record. Carrier and zero are set to ZMod n and 0. The orbit is taken to be LogicNat with its zero and succ constructors. The interpret field uses the sibling zmodOrbitInterpret. Commutation of interpret with step is proved by rewriting toNat_succ followed by norm_num. Injectivity of the orbit step reuses LogicNat.succ_injective. Induction reuses LogicNat.induction. Nontriviality is shown by exhibiting the class of 1 and verifying its positive cost via zmodCost.
why it matters
This definition supplies the finite cyclic model required by the modular arithmetic invariant, which in turn shows that the extracted Peano arithmetic is independent of the choice of realization. It therefore closes the loop from the universal forcing chain to concrete finite carriers while preserving the forced successor and induction. The construction sits inside the foundation layer that precedes any appeal to the eight-tick octave or spatial dimension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.