  23def lineageCost (a b : LineageState) : Nat :=
  24  if a = b then 0 else 1
  25
  26@[simp] theorem lineageCost_self (a : LineageState) : lineageCost a a = 0 := by
  27  simp [lineageCost]
  28
  29theorem lineageCost_symm (a b : LineageState) : lineageCost a b = lineageCost b a := by
  30  by_cases h : a = b
  31  · subst h
  32    simp [lineageCost]
  33  · have h' : b ≠ a := by intro hb; exact h hb.symm
  34    simp [lineageCost, h, h']
  35
  36def reproduce (a b : LineageState) : LineageState :=
  37  { lineage := a.lineage, generationDepth := a.generationDepth + b.generationDepth }
  38
  39def lineageZero : LineageState := ⟨0, 0⟩
  40def reproductiveStep : LineageState := ⟨0, 1⟩
  41
  42/-- Strict biological realization using reproduction as the generator. -/
  43def strictBiologyRealization : StrictLogicRealization where
  44  Carrier := LineageState
  45  Cost := Nat
  46  zeroCost := inferInstance
  47  compare := lineageCost
  48  compose := reproduce
  49  one := lineageZero
  50  generator := reproductiveStep
  51  identity_law := lineageCost_self
  52  non_contradiction_law := lineageCost_symm
  53  excluded_middle_law := True
  54  composition_law := True
  55  invariance_law := True
  56  nontrivial_law := by

papers checked against this theorem

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