`modulus`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.ModularLogicRealization
domain: Foundation
line: 32 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.ModularLogicRealization on GitHub at line 32.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

used by

formal source

  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
  52  apply Fin.ext
  53  change 0 % modulus k = 0
  54  exact Nat.zero_mod (modulus k)
  55
  56theorem modularInterpret_step (k : ℕ) (n : ArithmeticFromLogic.LogicNat) :
  57    modularInterpret k (ArithmeticFromLogic.LogicNat.succ n)
  58      = cycStep k (modularInterpret k n) := by
  59  apply Fin.ext
  60  change ArithmeticFromLogic.LogicNat.toNat (ArithmeticFromLogic.LogicNat.succ n) % modulus k =
  61    (ArithmeticFromLogic.LogicNat.toNat n % modulus k + 1) % modulus k
  62  rw [ArithmeticFromLogic.LogicNat.toNat_succ, Nat.succ_eq_add_one]

papers checked against this theorem

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