def
definition
def or abbrev
extinctionCascadeCert
show as:
view Lean formalization →
formal statement (Lean)
241def extinctionCascadeCert : ExtinctionCascadeCert where
242 Z_life_pos := Z_life_pos
proof body
Definition body.
243 Z_life_gt_one := Z_life_gt_one
244 totalRung_pos := fun _ E L j => totalRung_pos E L j
245 isBankrupt_antimono := fun _ E L₁ L₂ h j => isBankrupt_antimono E L₁ L₂ h j
246 cascadeStep_subset := fun _ E L => cascadeStep_subset E L
247 cascadeStep_card_le := fun _ E L => cascadeStep_card_le E L
248 cascadeIterate_subset := fun _ E L k => cascadeIterate_subset E L k
249 cascadeIterate_card_monotone :=
250 fun _ E L k => cascadeIterate_card_monotone E L k
251 recoveryTime_pos := recoveryTime_pos
252 recoveryTime_strict_mono := recoveryTime_strict_mono
253 deep_cascade_recovery_lower := deep_cascade_recovery_lower
254
255/-- **EXTINCTION CASCADE ONE-STATEMENT.** A species goes extinct when
256its total rung falls below `Z_life = φ^19`. The cascade closure on a
257finite species ecosystem is monotone (each step weakly shrinks the
258live set, and bankruptcy is preserved under support-removal). The
259cascade terminates in at most `n` steps on a finite ecosystem of `n`
260species. Post-cascade recovery time scales as `φ^k` in cascade depth,
261unbounded above. -/
depends on (38)
-
of -
rung -
step -
cascadeIterate_card_monotone -
cascadeIterate_subset -
cascadeStep_card_le -
cascadeStep_subset -
deep_cascade_recovery_lower -
ExtinctionCascadeCert -
isBankrupt_antimono -
recoveryTime_pos -
recoveryTime_strict_mono -
totalRung_pos -
Z_life -
Z_life_gt_one -
Z_life_pos -
rung -
of -
A -
is -
of -
as -
is -
E -
of -
is -
of -
A -
rung -
rung