cascadeIterate_subset
The cascade iteration operator on a finite ecosystem is non-increasing in the live-species set. Ecologists modeling recognition-driven extinction cascades cite this to guarantee monotonicity of the closure process. The proof is a one-line term that unfolds the successor definition of the iterate and invokes the single-step inclusion lemma.
claimLet $E$ be an ecosystem on $n$ species, $L$ a finite set of species indices, and $k$ a natural number. Let $I_m$ denote the live set obtained by applying the cascade step operator $m$ times to the initial set $L$. Then $I_{k+1}subseteq I_k$.
background
An ecosystem is a structure on $n$ species consisting of a baseline rung function (positive for each species) and a support function (non-negative between every pair). The cascade iterate starts from an initial live set $L$ at step zero and repeatedly applies the cascade step, which removes species whose total rung falls below the life threshold after support removal from extinct neighbors.
proof idea
The term proof rewrites the left side via the successor equation for the iterate definition, reducing it to the cascade step applied to the $k$-th iterate. It then applies the single-step subset theorem directly to that iterate.
why it matters in Recognition Science
This monotonicity result is invoked to obtain the cardinality comparison of successive iterates and the inclusion from the initial set. It contributes to the extinction cascade certificate and the one-statement theorem asserting that the cascade closure is monotone and terminates in at most $n$ steps on a finite ecosystem. In the Recognition Science framework it supplies the structural monotonicity property of ledger-bankruptcy dynamics on finite graphs.
scope and limits
- Does not prove that the iteration reaches a fixed point in finitely many steps.
- Does not supply bounds on the number of steps to termination.
- Does not extend to infinite or continuous species sets.
- Does not compute explicit rung values or bankruptcy predicates.
formal statement (Lean)
165theorem cascadeIterate_subset {n : ℕ} (E : Ecosystem n) (L : Finset (Fin n)) (k : ℕ) :
166 cascadeIterate E L (k + 1) ⊆ cascadeIterate E L k := by
proof body
Term-mode proof.
167 rw [cascadeIterate_succ]
168 exact cascadeStep_subset E (cascadeIterate E L k)
169