`recoveryTime_strict_mono`

proved

show as: view math explainer →

module: IndisputableMonolith.Ecology.ExtinctionCascadeFromLedgerBankruptcy
domain: Ecology
line: 193 · 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 193.

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

depends on

used by

formal source

 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 :
 218    ∀ n (E : Ecosystem n) (L : Finset (Fin n)) (j : Fin n),
 219      0 < totalRung E L j
 220  isBankrupt_antimono :
 221    ∀ n (E : Ecosystem n) (L₁ L₂ : Finset (Fin n)),
 222      L₁ ⊆ L₂ → ∀ j : Fin n,
 223        IsBankrupt E L₂ j → IsBankrupt E L₁ j

papers checked against this theorem

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