  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.