cascadeIterate_zero
plain-language theorem explainer
The base case of the cascade iteration states that zero applications of the extinction operator to an initial seed set L in a finite ecosystem E returns L unchanged. Modelers of recognition-bonded extinction chains on finite species graphs cite this when initializing the monotone closure computation for ledger-bankruptcy cascades. The proof reduces directly to the recursive definition of the iterate via reflexivity.
Claim. Let $E$ be an ecosystem on $n$ species with baseline rungs and non-negative bond supports, and let $L$ be a finite set of species indices. Then the zero-fold iteration of the cascade operator satisfies $cascadeIterate(E, L, 0) = L$.
background
An ecosystem is a structure on $n$ species whose baseline rung map and support matrix satisfy positivity and non-negativity, respectively. The cascade iteration is defined recursively: at step zero it returns the seed set $L$, and at step $k+1$ it applies the single-step cascade operator to the result of step $k$. This supplies the base case of that recursion, ensuring the iteration begins from the initial extinct species as described in the module's account of ledger bankruptcy driving rung drops below the life threshold.
proof idea
This is a one-line wrapper that applies reflexivity to the base clause of the recursive definition of cascadeIterate.
why it matters
This base case anchors the structural cascade theorem on finite recognition graphs. It supports the proof that the cascade closure is monotone and contains the seed set, as described in the module's account of ledger bankruptcy driving rung drops below the life threshold. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.