cascadeIterate_card_monotone
plain-language theorem explainer
The theorem establishes that the cardinality of the iterated cascade set on a finite ecosystem is non-increasing at each step. Ecologists analyzing extinction propagation in recognition graphs cite it to confirm that the process cannot expand the affected set in size during iteration. The argument is a direct one-line reduction from the inclusion of consecutive iterates to the standard cardinality comparison for subsets.
Claim. Let $E$ be an ecosystem on $n$ species with baseline rungs and non-negative bond supports, let $L$ be a finite set of species indices, and let $k$ be a natural number. The cardinality of the $(k+1)$-fold iterate of the cascade operator applied to $E$ and $L$ satisfies $|$iterated cascade at step $k+1| |$ ≤ $|$iterated cascade at step $k| |$.
background
An Ecosystem is a finite structure on $n$ species whose baseline rung vector is strictly positive and whose support matrix is entrywise non-negative; each species total rung is the sum of its baseline plus incoming supports. The cascade iterate begins at an initial set $L$ and applies the cascade step recursively, where the step removes species whose post-removal total rung drops below the life threshold. The module develops these dynamics as the closure of ledger bankruptcy on a recognition graph, with upstream results supplying the recursive definition of the iterate and the inclusion relation between successive values.
proof idea
The proof is a one-line wrapper that applies Finset.card_le_card directly to the inclusion cascadeIterate E L (k + 1) ⊆ cascadeIterate E L k supplied by the cascadeIterate_subset lemma.
why it matters
The result is assembled into the ExtinctionCascadeCert record that collects monotonicity and positivity facts for the full cascade certification. It supports the structural theorem on monotone fixed-point iteration for extinction cascades in the ecology track, consistent with the Recognition Science derivation of dynamics from the J-cost equation and the phi-ladder recovery scale. The module documentation ties it to recovery times exceeding phi^16 for deep cascades at rung 17.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.