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

biologyRealization

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)

  36def biologyRealization : LogicRealization where
  37  Carrier := Generation

proof body

Definition body.

  38  Cost := Nat
  39  zeroCost := inferInstance
  40  compare := biologyCost
  41  zero := 0
  42  step := Nat.succ
  43  Orbit := LogicNat
  44  orbitZero := LogicNat.zero
  45  orbitStep := LogicNat.succ
  46  interpret := biologyInterpret
  47  interpret_zero := by rfl
  48  interpret_step := by
  49    intro n
  50    show LogicNat.toNat (LogicNat.succ n) = Nat.succ (LogicNat.toNat n)
  51    rfl
  52  orbit_no_confusion := by intro n h; exact LogicNat.zero_ne_succ n h
  53  orbit_step_injective := LogicNat.succ_injective
  54  orbit_induction := by
  55    intro P h0 hs n
  56    exact LogicNat.induction (motive := P) h0 hs n
  57  orbitEquivLogicNat := Equiv.refl LogicNat
  58  orbitEquiv_zero := rfl
  59  orbitEquiv_step := by intro n; rfl
  60  identity := biologyCost_self
  61  nonContradiction := biologyCost_symm
  62  excludedMiddle := True
  63  composition := True
  64  actionInvariant := True
  65  nontrivial := by
  66    refine ⟨1, ?_⟩
  67    simp [biologyCost]
  68

used by (1)

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

depends on (24)

Lean names referenced from this declaration's body.