cascadeStep
plain-language theorem explainer
The single-step cascade operator removes from the current live set every species whose total rung falls below the life-ignition threshold under that set. Ecologists modeling recognition-driven extinctions cite it as the atomic update rule for simulating domino effects on finite species graphs. It is realized as a direct Finset filter that retains only non-bankrupt indices according to the total-rung comparison.
Claim. Let $E$ be an ecosystem on $n$ species equipped with positive baseline rungs and a non-negative support matrix. For a live set $L$ of species indices, the next live set consists of those $j$ in $L$ for which the total rung of $j$ (baseline plus summed supports received from members of $L$) satisfies total rung at least $Z_mathrm{life}$.
background
An ecosystem is a finite collection of species, each carrying a positive baseline rung together with a matrix of non-negative support values contributed by one species to another. The bankruptcy predicate holds for index $j$ under live set $L$ precisely when the total rung of $j$ (baseline plus supports from live neighbors) lies strictly below the life-ignition threshold $Z_mathrm{life} = phi^{19}$. The module document states that a cascade occurs when the extinction of one species removes recognition bonds whose absence drives another species below the same threshold. Upstream results establish the positivity of $Z_mathrm{life}$ and the decidability of the bankruptcy test.
proof idea
One-line definition that applies the Finset filter operation to $L$, retaining only those indices $j$ for which the bankruptcy predicate fails.
why it matters
This operator generates the sequence of live sets inside the iterated cascade closure and supplies the inclusion and cardinality lemmas used to certify termination. It fills the atomic dynamics slot in the structural cascade theorem for finite recognition graphs, linking directly to the phi-ladder rung calculations. Downstream certificates such as ExtinctionCascadeCert rely on repeated application to bound recovery times after deep cascades.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.