cascadeStep_subset
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.