module module

`IndisputableMonolith.Ecology.ExtinctionCascadeFromLedgerBankruptcy`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (24)

def Z_life L71
theorem Z_life_pos L73
theorem Z_life_gt_one L77
structure Ecosystem L85
def totalRung L97
theorem totalRung_pos L100
def IsBankrupt L112
theorem isBankrupt_antimono L121
def cascadeStep L137
theorem cascadeStep_subset L141
theorem cascadeStep_card_le L147
def cascadeIterate L154
theorem cascadeIterate_zero L159
theorem cascadeIterate_succ L162
theorem cascadeIterate_subset L165
theorem cascadeIterate_subset_initial L170
theorem cascadeIterate_card_monotone L178
def recoveryTime L187
theorem recoveryTime_pos L189
theorem recoveryTime_strict_mono L193
theorem deep_cascade_recovery_lower L204
structure ExtinctionCascadeCert L214
def extinctionCascadeCert L241
theorem extinction_cascade_one_statement L262