modularRealization
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not claim the orbit remains infinite inside the finite carrier.
- Does not assert that the cost function coincides with any physical distance.
- Does not extend to the case n=1 where the carrier collapses.
- Does not guarantee that every property of the infinite LogicNat lifts verbatim.
formal statement (Lean)
37def modularRealization (n : ℕ) [Fact (1 < n)] : LogicRealization where
38 Carrier := ZMod n
proof body
Definition body.
39 Cost := Nat
40 zeroCost := inferInstance
41 compare := zmodCost
42 zero := 0
43 step := fun z => z + 1
44 Orbit := LogicNat
45 orbitZero := LogicNat.zero
46 orbitStep := LogicNat.succ
47 interpret := zmodOrbitInterpret n
48 interpret_zero := by
49 show ((0 : ℕ) : ZMod n) = 0
50 norm_num
51 interpret_step := by
52 intro k
53 show ((LogicNat.toNat (LogicNat.succ k) : ZMod n) =
54 (LogicNat.toNat k : ZMod n) + 1)
55 rw [LogicNat.toNat_succ]
56 norm_num
57 orbit_no_confusion := by
58 intro k h
59 exact LogicNat.zero_ne_succ k h
60 orbit_step_injective := LogicNat.succ_injective
61 orbit_induction := by
62 intro P h0 hs k
63 exact LogicNat.induction (motive := P) h0 hs k
64 orbitEquivLogicNat := Equiv.refl LogicNat
65 orbitEquiv_zero := rfl
66 orbitEquiv_step := by intro k; rfl
67 identity := zmodCost_self
68 nonContradiction := zmodCost_symm
69 excludedMiddle := True
70 composition := True
71 actionInvariant := True
72 nontrivial := by
73 refine ⟨(1 : ZMod n), ?_⟩
74 have hne : (1 : ZMod n) ≠ 0 := by
75 intro h
76 have hval := congrArg ZMod.val h
77 rw [ZMod.val_one n, ZMod.val_zero] at hval
78 norm_num at hval
79 simp [zmodCost, hne]
80
81/-- Modular realization carries the universal forced arithmetic. -/