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

LogicRealization

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)

  32structure LogicRealization where
  33  Carrier : Type u
  34  Cost : Type v
  35  zeroCost : Zero Cost
  36  compare : Carrier → Carrier → Cost
  37  zero : Carrier
  38  step : Carrier → Carrier
  39  Orbit : Type u
  40  orbitZero : Orbit
  41  orbitStep : Orbit → Orbit
  42  interpret : Orbit → Carrier
  43  interpret_zero : interpret orbitZero = zero
  44  interpret_step : ∀ n : Orbit, interpret (orbitStep n) = step (interpret n)
  45  orbit_no_confusion : ∀ n : Orbit, orbitZero ≠ orbitStep n
  46  orbit_step_injective : Function.Injective orbitStep
  47  orbit_induction :
  48    ∀ P : Orbit → Prop,
  49      P orbitZero →
  50      (∀ n, P n → P (orbitStep n)) →
  51      ∀ n, P n
  52  orbitEquivLogicNat : Orbit ≃ LogicNat
  53  orbitEquiv_zero : orbitEquivLogicNat orbitZero = LogicNat.zero
  54  orbitEquiv_step : ∀ n : Orbit,
  55    orbitEquivLogicNat (orbitStep n) = LogicNat.succ (orbitEquivLogicNat n)
  56  identity : ∀ x : Carrier, compare x x = 0
  57  nonContradiction : ∀ x y : Carrier, compare x y = compare y x
  58  excludedMiddle : Prop
  59  composition : Prop
  60  actionInvariant : Prop
  61  nontrivial : ∃ x : Carrier, compare x zero ≠ 0
  62
  63attribute [instance] LogicRealization.zeroCost
  64
  65namespace LogicRealization
  66
  67/-- The identity-step shadow of a realization. This is the data from which
  68`ArithmeticOf` extracts arithmetic. -/

used by (40)

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

… and 10 more

depends on (22)

Lean names referenced from this declaration's body.