module module

`IndisputableMonolith.Climate.AtmosphericLayeringFromPhiLadder`

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

def tropopause_rung L104
def stratopause_rung L107
def mesopause_rung_lower L110
def mesopause_rung_upper L113
def thermosphere_rung L116
theorem tropopause_rung_eq L118
theorem stratopause_rung_eq L119
theorem thermosphere_rung_eq L120
theorem rung_strict_ordering L123
def altitude_at_rung L135
theorem altitude_at_rung_pos L137
theorem altitude_geometric L143
def stratopause_tropopause_ratio L150
theorem phi_cubed_eq L153
theorem stratopause_tropopause_ratio_gt_4 L162
theorem stratopause_tropopause_ratio_band L171
def thermosphere_tropopause_ratio L181
theorem thermosphere_tropopause_ratio_pos L183
theorem thermosphere_above_stratopause_ratio L189
structure AtmosphericLayeringFromPhiLadderCert L213
def atmosphericLayeringFromPhiLadderCert L231
theorem atmospheric_layering_one_statement L252