extinctionCascadeCert
plain-language theorem explainer
The declaration defines ExtinctionCascadeCert by direct field assignment of pre-established lemmas on positivity, antimonotonicity, and iteration properties. Modelers of recognition graphs in finite ecosystems cite this certificate to invoke the full cascade closure theorem without re-proving each component. Construction is a one-line structure literal that references sibling theorems for each field.
Claim. The extinction cascade certificate is the structure whose fields are the statements $0 < Z_ {life}$, $1 < Z_{life}$, positivity of total rung on any ecosystem and live set, antimonotonicity of bankruptcy under live-set inclusion, subset and cardinality monotonicity of cascade iteration, and the lower bound on recovery time at depth 17.
background
An ecosystem is a finite recognition graph whose vertices carry rungs and whose edges supply rung support; total rung of a species is its baseline plus summed supports from live neighbors. Bankruptcy occurs when total rung drops below the life threshold $Z_{life} = phi^{19}$. The module proves the cascade is the monotone fixed-point iteration of single-step extinctions on this graph. Upstream, Z_life_pos establishes $0 < Z_{life}$ by unfolding the definition and applying pow_pos; cascadeIterate_subset and cascadeIterate_card_monotone establish the inclusion and cardinality decrease at each iteration step.
proof idea
One-line wrapper that populates each field of the ExtinctionCascadeCert structure by direct reference to the corresponding sibling theorem or function: Z_life_pos, Z_life_gt_one, totalRung_pos, isBankrupt_antimono, cascadeStep_subset, cascadeStep_card_le, cascadeIterate_subset, cascadeIterate_card_monotone, recoveryTime_pos, recoveryTime_strict_mono, and deep_cascade_recovery_lower.
why it matters
This certificate supplies the single object referenced by the module's one-statement summary of the extinction cascade theorem. It closes the structural results on monotone cascade closure for finite species graphs and supplies the recovery-time scaling that links to the phi-ladder (T5 J-uniqueness, T6 phi fixed point). The declaration touches the open question of calibrating biological tau_0 against observed K-Pg recovery intervals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.