`deep_cascade_recovery_lower`

proved

show as: view math explainer →

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

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

 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
 224  cascadeStep_subset :
 225    ∀ n (E : Ecosystem n) (L : Finset (Fin n)),
 226      cascadeStep E L ⊆ L
 227  cascadeStep_card_le :
 228    ∀ n (E : Ecosystem n) (L : Finset (Fin n)),
 229      (cascadeStep E L).card ≤ L.card
 230  cascadeIterate_subset :
 231    ∀ n (E : Ecosystem n) (L : Finset (Fin n)) (k : ℕ),
 232      cascadeIterate E L (k + 1) ⊆ cascadeIterate E L k
 233  cascadeIterate_card_monotone :
 234    ∀ n (E : Ecosystem n) (L : Finset (Fin n)) (k : ℕ),

papers checked against this theorem

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