cascadeStep_subset
The theorem shows that applying one step of the cascade operator to a live species set L in a finite ecosystem always returns a subset of L. Modelers of recognition-driven extinctions cite this monotonicity when proving that iterated cascades remain nested and bounded. The proof is a one-line wrapper that unfolds the filter definition of cascadeStep and invokes the standard Finset filter subset fact.
claimFor any natural number $n$, ecosystem $E$ on $n$ species, and live set $L$ of species indices, the set of non-bankrupt species remaining after one cascade step satisfies $cascadeStep(E,L)subseteq L$.
background
An Ecosystem is a finite recognition graph whose species carry baseline rungs (all positive) and non-negative bond supports; total rung for a species is baseline plus summed supports from currently live neighbors. The module models ledger bankruptcy: a species is removed when its total rung drops below the ignition threshold $Z_life=phi^{19}$. cascadeStep is the operator that filters the current live set $L$ to retain only those species that remain non-bankrupt under the supports induced by $L$.
proof idea
Unfold the definition of cascadeStep, which is the filter of $L$ by the predicate of not being IsBankrupt under $E$ and $L$. The library lemma Finset.filter_subset then directly supplies the inclusion.
why it matters in Recognition Science
cascadeStep_subset is invoked by cascadeIterate_subset to establish that the iterated cascade is a decreasing sequence of sets, and by cascadeStep_card_le to obtain the cardinality bound. It supplies the single-step monotonicity required for the monotone fixed-point construction of the full extinction cascade closure, closing the structural part of the finite-graph iteration described in the module header.
scope and limits
- Does not prove termination of the iterated cascade.
- Does not bound the number of steps needed for a given seed.
- Does not treat infinite species graphs or continuous dynamics.
- Does not incorporate stochastic bond fluctuations.
Lean usage
rw [cascadeIterate_succ]; exact cascadeStep_subset E (cascadeIterate E L k)formal statement (Lean)
141theorem cascadeStep_subset {n : ℕ} (E : Ecosystem n) (L : Finset (Fin n)) :
142 cascadeStep E L ⊆ L := by
proof body
Term-mode proof.
143 unfold cascadeStep
144 exact Finset.filter_subset _ _
145
146/-- Each cascade step weakly shrinks the live set. -/