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

orderRealization

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 orderRealization : LogicRealization where
  38  Carrier := ℤ

proof body

Definition body.

  39  Cost := Nat
  40  zeroCost := inferInstance
  41  compare := intCost
  42  zero := 0
  43  step := fun z => z + 1
  44  Orbit := LogicNat
  45  orbitZero := LogicNat.zero
  46  orbitStep := LogicNat.succ
  47  interpret := intOrbitInterpret
  48  interpret_zero := by simp [intOrbitInterpret]
  49  interpret_step := by
  50    intro n
  51    show ((LogicNat.toNat (LogicNat.succ n) : ℤ) = (LogicNat.toNat n : ℤ) + 1)
  52    rw [LogicNat.toNat_succ]
  53    norm_num
  54  orbit_no_confusion := by
  55    intro n h
  56    exact LogicNat.zero_ne_succ n h
  57  orbit_step_injective := LogicNat.succ_injective
  58  orbit_induction := by
  59    intro P h0 hs n
  60    exact LogicNat.induction (motive := P) h0 hs n
  61  orbitEquivLogicNat := Equiv.refl LogicNat
  62  orbitEquiv_zero := rfl
  63  orbitEquiv_step := by intro n; rfl
  64  identity := intCost_self
  65  nonContradiction := intCost_symm
  66  excludedMiddle := True
  67  composition := True
  68  actionInvariant := True
  69  nontrivial := by
  70    refine ⟨1, ?_⟩
  71    simp [intCost]
  72
  73/-- Ordered realization carries the universal forced arithmetic. -/

used by (1)

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

depends on (23)

Lean names referenced from this declaration's body.