cascadeStep
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not compute the fixed-point closure of the full cascade.
- Does not incorporate explicit time evolution or recovery rates.
- Assumes finite species count and non-negative support values.
- Does not depend on the concrete numerical value of the life threshold beyond its use in the bankruptcy test.
- Does not address spatial embedding or higher-dimensional geometry of the species graph.
Lean usage
let L' : Finset (Fin n) := cascadeStep E Lformal statement (Lean)
137def cascadeStep {n : ℕ} (E : Ecosystem n) (L : Finset (Fin n)) :
138 Finset (Fin n) :=
proof body
Definition body.
139 L.filter (fun j => ¬ IsBankrupt E L j)
140