IndisputableMonolith.Foundation.ModularLogicRealization

   1import IndisputableMonolith.Foundation.DiscreteLogicRealization
   2
   3/-!
   4  ModularLogicRealization.lean
   5
   6  Periodic finite-cyclic realization for Universal Forcing.
   7
   8  The internal orbit is still free (`LogicNat`), while the carrier
   9  interpretation is periodic. This demonstrates that Universal Forcing does
  10  not require every realization to embed arithmetic faithfully into the carrier.
  11-/
  12
  13namespace IndisputableMonolith
  14namespace Foundation
  15namespace ModularLogicRealization
  16
  17/-- Equality cost on a finite carrier. -/
  18def finCost {m : ℕ} (x y : Fin m) : Nat :=
  19  if x = y then 0 else 1
  20
  21@[simp] theorem finCost_self {m : ℕ} (x : Fin m) : finCost x x = 0 := by
  22  simp [finCost]
  23
  24theorem finCost_symm {m : ℕ} (x y : Fin m) : finCost x y = finCost y x := by
  25  by_cases h : x = y
  26  · subst h
  27    simp [finCost]
  28  · have h' : y ≠ x := by intro hyx; exact h hyx.symm
  29    simp [finCost, h, h']
  30
  31/-- The cyclic carrier size for the `k`th modular realization. -/
  32def modulus (k : ℕ) : ℕ := k + 2
  33
  34theorem modulus_pos (k : ℕ) : 0 < modulus k := by
  35  unfold modulus
  36  omega
  37
  38theorem one_lt_modulus (k : ℕ) : 1 < modulus k := by
  39  unfold modulus
  40  omega
  41
  42/-- Successor on the finite cyclic carrier. -/
  43def cycStep (k : ℕ) (x : Fin (modulus k)) : Fin (modulus k) :=
  44  ⟨(x.val + 1) % modulus k, Nat.mod_lt _ (modulus_pos k)⟩
  45
  46/-- Interpret the free orbit periodically in a finite cyclic carrier. -/
  47def modularInterpret (k : ℕ) (n : ArithmeticFromLogic.LogicNat) : Fin (modulus k) :=
  48  ⟨ArithmeticFromLogic.LogicNat.toNat n % modulus k, Nat.mod_lt _ (modulus_pos k)⟩
  49
  50@[simp] theorem modularInterpret_zero (k : ℕ) :
  51    modularInterpret k ArithmeticFromLogic.LogicNat.zero = ⟨0, modulus_pos k⟩ := by
  52  apply Fin.ext
  53  change 0 % modulus k = 0
  54  exact Nat.zero_mod (modulus k)
  55
  56theorem modularInterpret_step (k : ℕ) (n : ArithmeticFromLogic.LogicNat) :
  57    modularInterpret k (ArithmeticFromLogic.LogicNat.succ n)
  58      = cycStep k (modularInterpret k n) := by
  59  apply Fin.ext
  60  change ArithmeticFromLogic.LogicNat.toNat (ArithmeticFromLogic.LogicNat.succ n) % modulus k =
  61    (ArithmeticFromLogic.LogicNat.toNat n % modulus k + 1) % modulus k
  62  rw [ArithmeticFromLogic.LogicNat.toNat_succ, Nat.succ_eq_add_one]
  63  have h := (Nat.add_mod (ArithmeticFromLogic.LogicNat.toNat n) 1 (modulus k)).symm
  64  simpa [Nat.mod_eq_of_lt (one_lt_modulus k)] using h
  65
  66/-- Finite cyclic Law-of-Logic realization with periodic interpretation. -/
  67def modularRealization (k : ℕ) : LogicRealization where
  68  Carrier := Fin (modulus k)
  69  Cost := Nat
  70  zeroCost := inferInstance
  71  compare := finCost
  72  zero := ⟨0, modulus_pos k⟩
  73  step := cycStep k
  74  Orbit := ArithmeticFromLogic.LogicNat
  75  orbitZero := ArithmeticFromLogic.LogicNat.zero
  76  orbitStep := ArithmeticFromLogic.LogicNat.succ
  77  interpret := modularInterpret k
  78  interpret_zero := modularInterpret_zero k
  79  interpret_step := modularInterpret_step k
  80  orbit_no_confusion := by
  81    intro n h
  82    exact ArithmeticFromLogic.LogicNat.zero_ne_succ n h
  83  orbit_step_injective := ArithmeticFromLogic.LogicNat.succ_injective
  84  orbit_induction := by
  85    intro P h0 hs n
  86    exact ArithmeticFromLogic.LogicNat.induction (motive := P) h0 hs n
  87  orbitEquivLogicNat := Equiv.refl ArithmeticFromLogic.LogicNat
  88  orbitEquiv_zero := rfl
  89  orbitEquiv_step := by intro n; rfl
  90  identity := finCost_self
  91  nonContradiction := finCost_symm
  92  excludedMiddle := True
  93  composition := True
  94  actionInvariant := True
  95  nontrivial := by
  96    refine ⟨⟨1, one_lt_modulus k⟩, ?_⟩
  97    simp [finCost]
  98
  99/-- Modular realization has invariant extracted arithmetic. -/
 100noncomputable def modular_arithmetic_invariant (k : ℕ) (R : LogicRealization.{0, 0}) :
 101    (UniversalForcing.arithmeticOf (modularRealization k)).peano.carrier
 102      ≃ (UniversalForcing.arithmeticOf R).peano.carrier :=
 103  ArithmeticOf.equivOfInitial
 104    (UniversalForcing.arithmeticOf (modularRealization k))
 105    (UniversalForcing.arithmeticOf R)
 106
 107/-- The modular interpretation is periodic on the carrier. -/
 108theorem modular_interpret_periodic (k : ℕ) (n : ArithmeticFromLogic.LogicNat) :
 109    modularInterpret k
 110        (ArithmeticFromLogic.LogicNat.fromNat
 111          (ArithmeticFromLogic.LogicNat.toNat n + modulus k))
 112      = modularInterpret k n := by
 113  apply Fin.ext
 114  simp [modularInterpret, ArithmeticFromLogic.LogicNat.toNat_fromNat]
 115
 116end ModularLogicRealization
 117end Foundation
 118end IndisputableMonolith
 119