strictModularRealization

formal source

  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