IndisputableMonolith.Foundation.UniversalForcing.Strict.Modular

   1import Mathlib
   2import IndisputableMonolith.Foundation.UniversalForcing.Strict.Ordered
   3
   4/-!
   5  Strict/Modular.lean
   6
   7  Strict modular realization on `ZMod n`. Carrier interpretation is periodic;
   8  forced arithmetic remains the derived free orbit.
   9-/
  10
  11namespace IndisputableMonolith
  12namespace Foundation
  13namespace UniversalForcing
  14namespace Strict
  15namespace Modular
  16
  17def zmodCost {n : ℕ} (a b : ZMod n) : Nat :=
  18  if a = b then 0 else 1
  19
  20@[simp] theorem zmodCost_self {n : ℕ} (a : ZMod n) : zmodCost a a = 0 := by
  21  simp [zmodCost]
  22
  23theorem zmodCost_symm {n : ℕ} (a b : ZMod n) : zmodCost a b = zmodCost b a := by
  24  by_cases h : a = b
  25  · subst h
  26    simp [zmodCost]
  27  · have h' : b ≠ a := by intro hb; exact h hb.symm
  28    simp [zmodCost, h, h']
  29
  30/-- Strict modular realization for moduli `n > 1`. -/
  31def strictModularRealization (n : ℕ) [Fact (1 < n)] : StrictLogicRealization where
  32  Carrier := ZMod n
  33  Cost := Nat
  34  zeroCost := inferInstance
  35  compare := zmodCost
  36  compose := fun a b => a + b
  37  one := 0
  38  generator := 1
  39  identity_law := zmodCost_self
  40  non_contradiction_law := zmodCost_symm
  41  excluded_middle_law := True
  42  composition_law := True
  43  invariance_law := True
  44  nontrivial_law := by
  45    have hne : (1 : ZMod n) ≠ 0 := by
  46      intro h
  47      have hval := congrArg ZMod.val h
  48      rw [ZMod.val_one n, ZMod.val_zero] at hval
  49      norm_num at hval
  50    simp [zmodCost, hne]
  51
  52def strictModular_arith_equiv_logicNat (n : ℕ) [Fact (1 < n)] :
  53    (StrictLogicRealization.arith (strictModularRealization n)).peano.carrier
  54      ≃ ArithmeticFromLogic.LogicNat :=
  55  (StrictLogicRealization.toLightweight (strictModularRealization n)).orbitEquivLogicNat
  56
  57end Modular
  58end Strict
  59end UniversalForcing
  60end Foundation
  61end IndisputableMonolith
  62