module module

`IndisputableMonolith.Climate.GeoengineeringApproachesFromConfigDim`

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

inductive GeoengineeringApproach L24
theorem geoengineeringApproach_count L32
def safeBandLower L36
def safeBandUpper L37
theorem safeBand_nondegenerate L39
theorem safeBand_contains_phi_point L42
structure GeoengineeringCert L47
def geoengineeringCert L52