Ecosystem

formal source

  82/-! ## §2. Species network and rung-support -/
  83
  84/-- A finite species ecosystem with current rungs and bond supports. -/
  85structure Ecosystem (n : ℕ) where
  86  /-- Baseline rung of each species (intrinsic, before bond support). -/
  87  baseline : Fin n → ℝ
  88  /-- Support `i → j` from each species i to each species j. -/
  89  support : Fin n → Fin n → ℝ
  90  /-- All baselines positive. -/
  91  baseline_pos : ∀ i : Fin n, 0 < baseline i
  92  /-- All supports non-negative. -/
  93  support_nonneg : ∀ i j : Fin n, 0 ≤ support i j
  94
  95/-- Total rung of species `j` under a "live" set `L` (only live
  96species contribute support). -/
  97def totalRung {n : ℕ} (E : Ecosystem n) (L : Finset (Fin n)) (j : Fin n) : ℝ :=
  98  E.baseline j + (L.sum fun i => E.support i j)
  99
 100theorem totalRung_pos {n : ℕ} (E : Ecosystem n) (L : Finset (Fin n)) (j : Fin n) :
 101    0 < totalRung E L j := by
 102  unfold totalRung
 103  have hb := E.baseline_pos j
 104  have hs : 0 ≤ L.sum (fun i => E.support i j) :=
 105    Finset.sum_nonneg (fun i _ => E.support_nonneg i j)
 106  linarith
 107
 108/-! ## §3. The bankruptcy step -/
 109
 110/-- Species `j` is **bankrupt** under live set `L` iff its total rung
 111falls below the life-ignition threshold. -/
 112def IsBankrupt {n : ℕ} (E : Ecosystem n) (L : Finset (Fin n)) (j : Fin n) : Prop :=
 113  totalRung E L j < Z_life
 114
 115instance {n : ℕ} (E : Ecosystem n) (L : Finset (Fin n)) (j : Fin n) :