module module

`IndisputableMonolith.Engineering.MarsAtmosphereJCostSchedule`

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

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (14)

def r_0 L38
def releaseRate L41
theorem releaseRate_zero L43
theorem releaseRate_pos L46
theorem releaseRate_strict_mono L50
theorem releaseRate_succ L56
def cumulativeRelease L64
theorem cumulativeRelease_zero L67
theorem cumulativeRelease_succ L70
theorem cumulativeRelease_nonneg L75
theorem cumulativeRelease_strict_mono L82
structure MarsAtmosphereJCostScheduleCert L95
def marsAtmosphereJCostScheduleCert L105
theorem mars_terraform_one_statement L118