`zmodCost_symm`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.UniversalForcing.ModularRealization
domain: Foundation
line: 26 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.UniversalForcing.ModularRealization on GitHub at line 26.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  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

papers checked against this theorem

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