cascadeIterate_subset_initial
The k-fold iteration of the cascade step on an ecosystem remains contained within the initial seed set L for every natural number k. Modelers of recognition-driven species extinctions cite this to guarantee that cascades cannot grow beyond the starting extinction set. The proof is by induction on k, reducing the successor case to the single-step inclusion via transitivity.
claimFor any natural number $n$, ecosystem $E$ on $n$ species, finite set $L$ of species indices, and natural number $k$, the set obtained by iterating the cascade step $k$ times starting from $L$ is a subset of $L$.
background
An Ecosystem is a finite collection of $n$ species, each with a positive baseline rung and non-negative support values from other species representing recognition bonds. The cascade process models extinction propagation: a species goes extinct if its rung drops below the life threshold after removing supports from extinct neighbors. The cascadeIterate function applies the single-step removal repeatedly $k$ times. This result relies on the definition of cascadeIterate as recursive application of cascadeStep and the prior theorem that each single step produces a subset of the previous set.
proof idea
Proof by induction on $k$. The base case $k=0$ follows immediately by simplification from the definition of cascadeIterate. In the successor case, the subset relation for $k+1$ follows by transitivity from the single-step inclusion cascadeIterate_subset applied to the iterate at $k$, together with the induction hypothesis.
why it matters in Recognition Science
This inclusion bound is a key structural property of the cascade closure operator in the Recognition Science ecology model, ensuring the iterated extinction set stays within the initial ledger bankruptcy seed. It supports the module's claim that the cascade is a monotone fixed-point iteration bounded above by the seed set. The result closes part of the structural analysis needed before proving convergence or domino criteria in finite graphs.
scope and limits
- Does not establish convergence of the iteration to a fixed point.
- Does not apply to infinite species graphs.
- Does not incorporate the explicit rung threshold Z_life = phi^19.
- Does not compute the final extinct set size or rung values.
formal statement (Lean)
170theorem cascadeIterate_subset_initial {n : ℕ} (E : Ecosystem n)
171 (L : Finset (Fin n)) (k : ℕ) :
172 cascadeIterate E L k ⊆ L := by
proof body
Term-mode proof.
173 induction k with
174 | zero => simp [cascadeIterate]
175 | succ k ih =>
176 apply Finset.Subset.trans (cascadeIterate_subset E L k) ih
177