modularRealization
plain-language theorem explainer
modularRealization constructs a finite cyclic LogicRealization whose carrier is Fin(modulus k) while the internal orbit remains the free inductive LogicNat. Researchers on Universal Forcing cite it to exhibit invariant extracted arithmetic under periodic carrier interpretation. The definition assembles the record by wiring finCost, cycStep, modularInterpret and the LogicNat induction theorems into the required fields.
Claim. For each natural number $k$, let $m=$ modulus$(k)$. The modular realization is the LogicRealization whose carrier is the finite set Fin$(m)$, whose cost function is finCost, whose zero element is $0$ with proof modulus_pos$(k)$, whose successor is cycStep$(k)$, whose orbit is the inductive type LogicNat, whose interpretation map is modularInterpret$(k)$, and whose remaining axioms hold by the properties of finCost and the Peano theorems on LogicNat.
background
ModularLogicRealization supplies periodic finite-cyclic realizations inside Universal Forcing. The carrier is the finite cyclic group Fin(modulus k) while the orbit stays the free inductive type LogicNat whose constructors identity and step generate the orbit {1, γ, γ², …} closed under multiplication by the generator. This separation shows that the forced arithmetic need not be faithfully embedded in the carrier itself. The module imports DiscreteLogicRealization and depends on ArithmeticFromLogic, where LogicNat is introduced as the natural numbers forced by the Law of Logic and succ_injective, zero_ne_succ and induction are proved as theorems of that inductive structure.
proof idea
The definition is a direct record construction. Carrier, Cost, zero, step, Orbit, interpret and the interpret_zero/interpret_step fields are set by direct reference to modulus, finCost, cycStep and modularInterpret. orbit_no_confusion applies zero_ne_succ, orbit_step_injective applies succ_injective, orbit_induction applies LogicNat.induction, and nontrivial applies one_lt_modulus together with finCost. The remaining fields are filled with rfl, True or finCost_self/finCost_symm.
why it matters
The definition supplies the modular case required by modular_arithmetic_invariant, which proves that the arithmetic extracted via UniversalForcing.arithmeticOf is equivalent for any two realizations. It therefore demonstrates that Universal Forcing forces arithmetic invariantly even when the carrier interpretation is made periodic rather than faithful. In the broader framework this supports the claim that the Law of Logic yields the same Peano structure regardless of the concrete realization chosen.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.