`cascadeIterate_subset_initial`

proved

show as: view math explainer →

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

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

formal source

 167  rw [cascadeIterate_succ]
 168  exact cascadeStep_subset E (cascadeIterate E L k)
 169
 170theorem cascadeIterate_subset_initial {n : ℕ} (E : Ecosystem n)
 171    (L : Finset (Fin n)) (k : ℕ) :
 172    cascadeIterate E L k ⊆ L := by
 173  induction k with
 174  | zero => simp [cascadeIterate]
 175  | succ k ih =>
 176      apply Finset.Subset.trans (cascadeIterate_subset E L k) ih
 177
 178theorem cascadeIterate_card_monotone {n : ℕ} (E : Ecosystem n)
 179    (L : Finset (Fin n)) (k : ℕ) :
 180    (cascadeIterate E L (k + 1)).card ≤ (cascadeIterate E L k).card :=
 181  Finset.card_le_card (cascadeIterate_subset E L k)
 182
 183/-! ## §6. Cascade-recovery time on the φ-ladder -/
 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

papers checked against this theorem

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