IndisputableMonolith.Foundation.UniversalForcing.Strict.Biology

   1import IndisputableMonolith.Foundation.UniversalForcing.Strict.Music
   2
   3/-!
   4  Strict/Biology.lean
   5
   6  Domain-rich biological realization over a simple lineage-state structure.
   7-/
   8
   9namespace IndisputableMonolith
  10namespace Foundation
  11namespace UniversalForcing
  12namespace Strict
  13namespace Biology
  14
  15/-- A lineage state is a generation-depth coordinate together with a lineage
  16label.  The label keeps this from being a bare `Nat` alias; arithmetic is
  17forced by repeated reproductive step, not assumed by the carrier name. -/
  18structure LineageState where
  19  lineage : Nat
  20  generationDepth : Nat
  21  deriving DecidableEq, Repr
  22
  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
  57    simp [lineageCost, reproductiveStep, lineageZero]
  58
  59def biology_arith_equiv_logicNat :
  60    (StrictLogicRealization.arith strictBiologyRealization).peano.carrier
  61      ≃ ArithmeticFromLogic.LogicNat :=
  62  (StrictLogicRealization.toLightweight strictBiologyRealization).orbitEquivLogicNat
  63
  64end Biology
  65end Strict
  66end UniversalForcing
  67end Foundation
  68end IndisputableMonolith
  69