cascadeIterate_subset
plain-language theorem explainer
The cascade iteration operator on a finite ecosystem is non-increasing in the live-species set. Ecologists modeling recognition-driven extinction cascades cite this to guarantee monotonicity of the closure process. The proof is a one-line term that unfolds the successor definition of the iterate and invokes the single-step inclusion lemma.
Claim. Let $E$ be an ecosystem on $n$ species, $L$ a finite set of species indices, and $k$ a natural number. Let $I_m$ denote the live set obtained by applying the cascade step operator $m$ times to the initial set $L$. Then $I_{k+1}subseteq I_k$.
background
An ecosystem is a structure on $n$ species consisting of a baseline rung function (positive for each species) and a support function (non-negative between every pair). The cascade iterate starts from an initial live set $L$ at step zero and repeatedly applies the cascade step, which removes species whose total rung falls below the life threshold after support removal from extinct neighbors.
proof idea
The term proof rewrites the left side via the successor equation for the iterate definition, reducing it to the cascade step applied to the $k$-th iterate. It then applies the single-step subset theorem directly to that iterate.
why it matters
This monotonicity result is invoked to obtain the cardinality comparison of successive iterates and the inclusion from the initial set. It contributes to the extinction cascade certificate and the one-statement theorem asserting that the cascade closure is monotone and terminates in at most $n$ steps on a finite ecosystem. In the Recognition Science framework it supplies the structural monotonicity property of ledger-bankruptcy dynamics on finite graphs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.