`modularRealization`

definition

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

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

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

  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
  57  orbit_no_confusion := by
  58    intro k h
  59    exact LogicNat.zero_ne_succ k h
  60  orbit_step_injective := LogicNat.succ_injective
  61  orbit_induction := by
  62    intro P h0 hs k
  63    exact LogicNat.induction (motive := P) h0 hs k
  64  orbitEquivLogicNat := Equiv.refl LogicNat
  65  orbitEquiv_zero := rfl
  66  orbitEquiv_step := by intro k; rfl
  67  identity := zmodCost_self

papers checked against this theorem

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