cascadeStep_card_le
plain-language theorem explainer
The theorem establishes that each application of the cascade operator on a finite ecosystem produces a live set whose cardinality is at most that of the input set. Ecologists modeling extinction dynamics on recognition graphs cite it to bound successive waves of species loss. The proof is a one-line wrapper that applies the subset relation between output and input live sets to the standard cardinality monotonicity lemma for finite sets.
Claim. Let $E$ be a finite ecosystem on $n$ species and let $L$ be any subset of species indices. Then the cardinality of the live set after one cascade step satisfies $|$cascadeStep$(E, L)|$ $≤$ $|L|$.
background
An ecosystem is a finite recognition graph with $n$ species, each carrying a positive baseline rung and non-negative support values contributed by neighbors, per the Ecosystem structure. The cascade step removes from the current live set $L$ every species whose total rung (baseline plus supports from remaining live neighbors) drops below the ignition threshold $Z_ life = φ^{19}$. The module treats the cascade as the monotone fixed-point iteration of this removal rule on the finite species set.
proof idea
The proof is a one-line wrapper that applies Finset.card_le_card to the subset relation cascadeStep_subset E L.
why it matters
The result feeds directly into the ExtinctionCascadeCert structure that assembles the full set of certified cascade properties. It supplies the cardinality bound needed for the module's proof that the cascade closure operator is inclusion-monotone and bounded above by the full species set. Within Recognition Science it closes one structural step of the ecological track on rung thresholds and bond removal, consistent with the phi-ladder and the Recognition Composition Law, while leaving open the explicit calibration of recovery times against biological data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.