`recoveryTime`

definition

show as: view math explainer →

module: IndisputableMonolith.Ecology.ExtinctionCascadeFromLedgerBankruptcy
domain: Ecology
line: 187 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Ecology.ExtinctionCascadeFromLedgerBankruptcy on GitHub at line 187.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

used by

formal source

 184
 185/-- Recovery time after a cascade of depth `k` (in φ-ladder units of
 186the natural recovery scale `τ_0`). -/
 187def recoveryTime (k : ℕ) : ℝ := phi ^ k
 188
 189theorem recoveryTime_pos (k : ℕ) : 0 < recoveryTime k := by
 190  unfold recoveryTime
 191  exact pow_pos phi_pos k
 192
 193theorem recoveryTime_strict_mono (k : ℕ) :
 194    recoveryTime k < recoveryTime (k + 1) := by
 195  unfold recoveryTime
 196  rw [pow_succ]
 197  have hk : 0 < phi ^ k := pow_pos phi_pos k
 198  have hphi : 1 < phi := one_lt_phi
 199  nlinarith
 200
 201/-- Recovery time at deep cascade (`k = 17`, mammal Z-rung)
 202exceeds φ^16 (`≈ 2207`), consistent with `10⁴–10⁵` years for the
 203K-Pg mammal radiation under canonical biological τ_0 calibration. -/
 204theorem deep_cascade_recovery_lower :
 205    phi ^ 16 < recoveryTime 17 := by
 206  unfold recoveryTime
 207  rw [pow_succ]
 208  have h16 : 0 < phi ^ 16 := pow_pos phi_pos 16
 209  have hphi : 1 < phi := one_lt_phi
 210  nlinarith
 211
 212/-! ## §7. Master certificate -/
 213
 214structure ExtinctionCascadeCert where
 215  Z_life_pos : 0 < Z_life
 216  Z_life_gt_one : 1 < Z_life
 217  totalRung_pos :

papers checked against this theorem

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