pith. machine review for the scientific record. sign in
structure definition def or abbrev high

ExtinctionCascadeCert

show as:
view Lean formalization →

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.

claimA 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 214structure ExtinctionCascadeCert where
 215  Z_life_pos : 0 < Z_life
 216  Z_life_gt_one : 1 < Z_life
 217  totalRung_pos :
 218    ∀ n (E : Ecosystem n) (L : Finset (Fin n)) (j : Fin n),
 219      0 < totalRung E L j
 220  isBankrupt_antimono :
 221    ∀ n (E : Ecosystem n) (L₁ L₂ : Finset (Fin n)),
 222      L₁ ⊆ L₂ → ∀ j : Fin n,
 223        IsBankrupt E L₂ j → IsBankrupt E L₁ j
 224  cascadeStep_subset :
 225    ∀ n (E : Ecosystem n) (L : Finset (Fin n)),
 226      cascadeStep E L ⊆ L
 227  cascadeStep_card_le :
 228    ∀ n (E : Ecosystem n) (L : Finset (Fin n)),
 229      (cascadeStep E L).card ≤ L.card
 230  cascadeIterate_subset :
 231    ∀ n (E : Ecosystem n) (L : Finset (Fin n)) (k : ℕ),
 232      cascadeIterate E L (k + 1) ⊆ cascadeIterate E L k
 233  cascadeIterate_card_monotone :
 234    ∀ n (E : Ecosystem n) (L : Finset (Fin n)) (k : ℕ),
 235      (cascadeIterate E L (k + 1)).card ≤ (cascadeIterate E L k).card
 236  recoveryTime_pos : ∀ k : ℕ, 0 < recoveryTime k
 237  recoveryTime_strict_mono :
 238    ∀ k : ℕ, recoveryTime k < recoveryTime (k + 1)
 239  deep_cascade_recovery_lower : phi ^ 16 < recoveryTime 17
 240

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (21)

Lean names referenced from this declaration's body.