  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

papers checked against this theorem

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