pith. machine review for the scientific record. sign in
def definition def or abbrev

modularRealization

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  37def modularRealization (n : ℕ) [Fact (1 < n)] : LogicRealization where
  38  Carrier := ZMod n

proof body

Definition body.

  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
  68  nonContradiction := zmodCost_symm
  69  excludedMiddle := True
  70  composition := True
  71  actionInvariant := True
  72  nontrivial := by
  73    refine ⟨(1 : ZMod n), ?_⟩
  74    have hne : (1 : ZMod n) ≠ 0 := by
  75      intro h
  76      have hval := congrArg ZMod.val h
  77      rw [ZMod.val_one n, ZMod.val_zero] at hval
  78      norm_num at hval
  79    simp [zmodCost, hne]
  80
  81/-- Modular realization carries the universal forced arithmetic. -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (25)

Lean names referenced from this declaration's body.