module module

`IndisputableMonolith.Geology.EruptionRecurrenceLadder`

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 (10)

def vei_step_ratio L52
theorem vei_step_ratio_pos L54
theorem vei_step_ratio_band L59
def cumulative_ratio L77
theorem cumulative_ratio_pos L79
theorem cumulative_ratio_one_step L83
theorem cumulative_ratio_factors L88
structure EruptionRecurrenceCert L95
def eruptionRecurrenceCert L103
theorem eruption_recurrence_one_statement L113