ExtinctionCascadeCert
plain-language theorem explainer
The ExtinctionCascadeCert structure assembles the positivity, monotonicity, and recovery bounds required by the ledger-bankruptcy cascade on finite species graphs. Modelers of post-extinction recovery on the phi-ladder would cite it to guarantee that iterated removal of bankrupt species produces nested live sets whose cardinalities decrease while recovery times increase strictly. The structure is assembled by direct reference to the already-proved sibling lemmas on cascade steps, iteration, and the explicit phi^16 lower bound at depth 17.
Claim. A structure certifying that the life-ignition threshold satisfies $0 < Z_ {life} = phi^{19}$ and $1 < Z_ {life}$, that total rung is positive for every ecosystem $E$ and live set $L$, that bankruptcy is antimonotone in the live set, that each cascade step yields a subset of the current live set with cardinality at most that of the live set, that iterated cascades are nested decreasing subsets with non-increasing cardinality, and that recovery time $tau(k)$ is strictly increasing with $phi^{16} < tau(17)$.
background
An ecosystem is a finite recognition graph whose vertices carry positive baseline rungs and whose directed edges carry non-negative support values. The life-ignition threshold is the constant $Z_ {life} := phi^{19}$. A species $j$ is bankrupt under live set $L$ precisely when its total rung (baseline plus summed supports from live neighbors) lies strictly below this threshold. The cascade step removes every bankrupt species from the current live set; iteration of this operator produces a monotone decreasing sequence of subsets whose cardinalities are non-increasing. Recovery time is a strictly increasing function of iteration depth whose value at depth 17 exceeds $phi^{16}$.
proof idea
The structure is populated by direct references to the sibling results: Z_life_pos and Z_life_gt_one supply the threshold bounds, totalRung_pos supplies rung positivity, isBankrupt_antimono supplies antimonotonicity, cascadeStep_subset and cascadeStep_card_le supply the single-step inclusion and cardinality bounds, cascadeIterate_subset and cascadeIterate_card_monotone supply the iterated inclusion and cardinality bounds, and the explicit inequality deep_cascade_recovery_lower supplies the recovery-time lower bound at depth 17. No additional tactics are applied.
why it matters
The certificate supplies the structural invariants required by the master definition extinctionCascadeCert, which packages them for use in downstream ecology results on the Q2 track. It confirms that recovery times at mammal-relevant rung depths exceed $phi^{16}$, aligning with geological timescales for the K-Pg boundary under canonical biological calibration. The construction inherits the phi-ladder and Recognition Composition Law from the constants module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.