cascadeIterate_succ
plain-language theorem explainer
The successor clause for the cascade iteration states that advancing one more step applies the single-step bankruptcy filter to the current live set. Modelers of recognition-based extinction dynamics cite this identity when establishing inclusion-monotonicity of the cascade closure. The equality holds immediately by the recursive clause in the definition of the iteration operator.
Claim. Let $E$ be a finite ecosystem on $n$ species with positive baseline rungs and non-negative bond supports, let $L$ be an initial set of live species, and let $k$ be a natural number. Then the result of iterating the cascade $k+1$ times equals the single cascade step applied to the result of iterating $k$ times.
background
An ecosystem on $n$ species is a structure carrying a positive baseline rung for each species and a non-negative support value from every species to every other. The cascade step removes from the current live set every species whose total rung (baseline plus supports from remaining live neighbors) falls below the life-ignition threshold. The iteration operator is defined recursively: it returns the seed set at step 0 and applies the cascade step to the previous iterate at each successor step. This module develops the monotone closure of extinction cascades on finite recognition graphs, where extinction of one species removes its support contributions and may drive downstream species below threshold.
proof idea
The proof is a one-line wrapper that unfolds the recursive definition of cascadeIterate at successor arguments, which directly matches the right-hand side by reflexivity.
why it matters
This identity supplies the unfolding step used to prove that the cascade iterate is inclusion-monotone, as applied in the downstream result cascadeIterate_subset. It supports the structural theorem that the cascade closure is a monotone fixed-point operator on the power set of species. In the Recognition Science framework it formalizes the domino effect in extinction chains driven by rung-support removal, consistent with the phi-ladder thresholds and the finite-graph fixed-point iteration described in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.