ExtinctionCascadeCert
plain-language theorem explainer
ExtinctionCascadeCert bundles the positivity of the life-ignition threshold, antimonotonicity of bankruptcy, monotonicity of cascade iterations on finite species graphs, and the recovery-time lower bound at depth 17. Ecologists calibrating post-extinction recovery on the phi-ladder cite the packaged inequalities when mapping to geological timescales such as the K-Pg mammal radiation. The declaration is a record type assembled directly from the module's component lemmas on cascade steps and rung thresholds.
Claim. Let $Z_{\text{life}} = \phi^{19}$. An ecosystem consists of $n$ species with positive baseline rungs and nonnegative support values. A species $j$ is bankrupt under live set $L$ when its total rung falls below $Z_{\text{life}}$. The certificate asserts $0 < Z_{\text{life}}$, $1 < Z_{\text{life}}$, positivity of every total rung, that bankruptcy is antimonotone in the live set, that each cascade step is a subset of the live set with cardinality at most that of the live set, that iterated cascades are nested with nonincreasing cardinality, that recovery time is positive and strictly increasing, and $\phi^{16} < $ recovery time at step 17.
background
In this module an ecosystem is a finite recognition graph whose vertices carry baseline rungs and whose directed edges carry nonnegative support values; total rung of species $j$ under live set $L$ is the baseline plus the sum of supports from species still in $L$. The life-ignition threshold is defined by $Z_{\text{life}} := \phi^{19}$. IsBankrupt holds precisely when total rung drops below this threshold. Cascade step removes every bankrupt species from the current live set; cascade iterate applies the step repeatedly.
The module states: "A species goes extinct when its recognition rung Z falls below the life-ignition threshold Z_life = φ^19". The cascade is the monotone closure of this removal process on a finite set. Recovery time is an auxiliary function on the phi-ladder that counts the number of steps needed to reach a given cascade depth; the structure records that this count at depth 17 exceeds $\phi^{16}$.
proof idea
The structure is a record whose fields are supplied verbatim by prior results in the same module: Z_life_pos and Z_life_gt_one unfold the definition of Z_life; totalRung_pos, isBankrupt_antimono, cascadeStep_subset, cascadeStep_card_le, cascadeIterate_subset and cascadeIterate_card_monotone are the corresponding named theorems; recoveryTime_pos, recoveryTime_strict_mono and deep_cascade_recovery_lower are the listed recovery-time facts. No additional reasoning is performed inside the structure itself.
why it matters
The record is instantiated by extinctionCascadeCert to produce the master certificate for the entire extinction-cascade development. It supplies the structural invariants required by the finite-graph cascade theorem in §7 of the module. The recovery-time field at k=17 directly links the phi-ladder to biological recovery timescales after the K-Pg event, consistent with the phi-based mass formula and the eight-tick octave of the broader Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.