IndisputableMonolith.Foundation.UniversalForcing.BiologyRealization

   1import IndisputableMonolith.Foundation.UniversalForcing.EthicsRealization
   2
   3/-!
   4  BiologyRealization.lean
   5
   6  Lightweight biological realization: the carrier is generation count, with
   7  the reproductive step as generator.
   8-/
   9
  10namespace IndisputableMonolith
  11namespace Foundation
  12namespace UniversalForcing
  13namespace BiologyRealization
  14
  15open ArithmeticFromLogic
  16open Invariance.Universal
  17
  18abbrev Generation := Nat
  19
  20def biologyCost (a b : Generation) : Nat :=
  21  if a = b then 0 else 1
  22
  23@[simp] theorem biologyCost_self (a : Generation) : biologyCost a a = 0 := by
  24  simp [biologyCost]
  25
  26theorem biologyCost_symm (a b : Generation) : biologyCost a b = biologyCost b a := by
  27  by_cases h : a = b
  28  · subst h; simp [biologyCost]
  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
  63  composition := True
  64  actionInvariant := True
  65  nontrivial := by
  66    refine ⟨1, ?_⟩
  67    simp [biologyCost]
  68
  69noncomputable def biology_arith_equiv_nat :
  70    (arithmeticOf biologyRealization).peano.carrier ≃ LogicNat :=
  71  biologyRealization.orbitEquivLogicNat
  72
  73end BiologyRealization
  74end UniversalForcing
  75end Foundation
  76end IndisputableMonolith
  77