IndisputableMonolith.Foundation.UniversalForcing.ModularRealization

   1import Mathlib
   2import IndisputableMonolith.Foundation.UniversalForcing
   3
   4/-!
   5  ModularRealization.lean
   6
   7  Modular/cyclic realization. The carrier is `ZMod n`, with equality cost.
   8  The semantic orbit in the finite carrier may close; the forced arithmetic is
   9  the universal iteration object certified by the internal orbit.
  10-/
  11
  12namespace IndisputableMonolith
  13namespace Foundation
  14namespace UniversalForcing
  15namespace ModularRealization
  16
  17open ArithmeticFromLogic
  18
  19/-- Equality cost on a cyclic carrier. -/
  20def zmodCost {n : ℕ} (a b : ZMod n) : Nat :=
  21  if a = b then 0 else 1
  22
  23@[simp] theorem zmodCost_self {n : ℕ} (a : ZMod n) : zmodCost a a = 0 := by
  24  simp [zmodCost]
  25
  26theorem zmodCost_symm {n : ℕ} (a b : ZMod n) : zmodCost a b = zmodCost b a := by
  27  by_cases h : a = b
  28  · subst h; simp [zmodCost]
  29  · have h' : b ≠ a := by intro hb; exact h hb.symm
  30    simp [zmodCost, h, h']
  31
  32/-- Interpret `LogicNat` in `ZMod n` by the usual coercion of its index. -/
  33def zmodOrbitInterpret (n : ℕ) (k : LogicNat) : ZMod n :=
  34  (LogicNat.toNat k : ZMod n)
  35
  36/-- Modular realization for any nontrivial modulus. -/
  37def modularRealization (n : ℕ) [Fact (1 < n)] : LogicRealization where
  38  Carrier := ZMod n
  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. -/
  82noncomputable def modular_arithmetic_invariant (n : ℕ) [Fact (1 < n)]
  83    (R : LogicRealization.{0, 0}) :
  84    (arithmeticOf (modularRealization n)).peano.carrier
  85      ≃ (arithmeticOf R).peano.carrier :=
  86  ArithmeticOf.equivOfInitial (arithmeticOf (modularRealization n)) (arithmeticOf R)
  87
  88end ModularRealization
  89end UniversalForcing
  90end Foundation
  91end IndisputableMonolith
  92