`cascadeIterate_zero`

proved

show as: view math explainer →

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

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

 156  | 0     => L
 157  | k + 1 => cascadeStep E (cascadeIterate E L k)
 158
 159theorem cascadeIterate_zero {n : ℕ} (E : Ecosystem n) (L : Finset (Fin n)) :
 160    cascadeIterate E L 0 = L := rfl
 161
 162theorem cascadeIterate_succ {n : ℕ} (E : Ecosystem n) (L : Finset (Fin n)) (k : ℕ) :
 163    cascadeIterate E L (k + 1) = cascadeStep E (cascadeIterate E L k) := rfl
 164
 165theorem cascadeIterate_subset {n : ℕ} (E : Ecosystem n) (L : Finset (Fin n)) (k : ℕ) :
 166    cascadeIterate E L (k + 1) ⊆ cascadeIterate E L k := by
 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

papers checked against this theorem

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