`one_lt_modulus`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.ModularLogicRealization
domain: Foundation
line: 38 · 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 38.

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

depends on

used by

formal source

  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]
  63  have h := (Nat.add_mod (ArithmeticFromLogic.LogicNat.toNat n) 1 (modulus k)).symm
  64  simpa [Nat.mod_eq_of_lt (one_lt_modulus k)] using h
  65
  66/-- Finite cyclic Law-of-Logic realization with periodic interpretation. -/
  67def modularRealization (k : ℕ) : LogicRealization where
  68  Carrier := Fin (modulus k)

papers checked against this theorem

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