`finCost`

definition

show as: view math explainer →

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

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

  15namespace ModularLogicRealization
  16
  17/-- Equality cost on a finite carrier. -/
  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)⟩

papers checked against this theorem

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