extinction_cascade_one_statement
plain-language theorem explainer
The declaration establishes four core properties of the extinction cascade in a finite recognition ecosystem: the life threshold exceeds zero, bankruptcy is anti-monotone in the live set, iterated cascade sets are nested and decreasing, and recovery time grows strictly with depth k. An ecologist modeling species collapse under bond removal would cite this to guarantee monotonicity and phi-scaled recovery. The proof is a direct term assembly of four prior results on positivity, anti-monotonicity, subset iteration, and strict increase.
Claim. Let $Z_ {rm life}=phi^{19}$. In any finite ecosystem $E$ of $n$ species, if species $j$ is bankrupt (total rung below $Z_{rm life}$) under live set $L_2$, then it remains bankrupt under any $L_1subseteq L_2$. The iterated cascade satisfies $C_{k+1}(L)subseteq C_k(L)$ for all $k$. Recovery time after depth $k$ obeys $tau(k)<tau(k+1)$ where $tau(k)=phi^k$.
background
The module models a finite species graph where each species carries a positive baseline rung and receives non-negative support from neighbors. Ecosystem is the structure recording these baselines and supports. IsBankrupt declares a species bankrupt under live set L precisely when its total rung (baseline plus summed supports from L) drops below Z_life = phi^19. CascadeIterate applies the single-step removal of bankrupt species iteratively, beginning from an initial live set. RecoveryTime(k) = phi^k supplies the post-cascade recovery scale.
proof idea
The proof is a term-mode constructor that directly supplies the four conjuncts from upstream results: Z_life_pos for positivity, isBankrupt_antimono for anti-monotonicity of bankruptcy, cascadeIterate_subset for the nested inclusion of iterates, and recoveryTime_strict_mono for the strict increase of recovery times.
why it matters
This packages the structural properties of the cascade closure on finite ecosystems, serving as the central reference for extinction dynamics in Recognition Science ecology. It implements the monotone fixed-point iteration with Z_life = phi^19 linking to the abiogenesis threshold and recovery scaling as phi^k reflecting the phi-ladder. No downstream uses appear yet, but it closes the basic monotonicity and scaling claims for cascade depth.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.