  29  · have h' : b ≠ a := by intro hb; exact h hb.symm
  30    simp [biologyCost, h, h']
  31
  32def biologyInterpret (n : LogicNat) : Generation :=
  33  LogicNat.toNat n
  34
  35/-- Biological realization as generation-count comparison. -/
  36def biologyRealization : LogicRealization where
  37  Carrier := Generation
  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

papers checked against this theorem

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