`phi_cubed_eq`

proved

show as: view math explainer →

module: IndisputableMonolith.Climate.AtmosphericLayeringFromPhiLadder
domain: Climate
line: 153 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Climate.AtmosphericLayeringFromPhiLadder on GitHub at line 153.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 150def stratopause_tropopause_ratio : ℝ := phi ^ 3
 151
 152/-- `phi^3 = phi^2 · phi`, expanded via `phi^2 = phi + 1`. -/
 153theorem phi_cubed_eq : phi ^ 3 = 2 * phi + 1 := by
 154  have h : phi ^ 2 = phi + 1 := phi_sq_eq
 155  have h_step : phi ^ 3 = phi ^ 2 * phi := by ring
 156  rw [h_step, h]
 157  ring_nf
 158  rw [h]
 159  ring
 160
 161/-- The ratio is strictly above 4. -/
 162theorem stratopause_tropopause_ratio_gt_4 :
 163    4 < stratopause_tropopause_ratio := by
 164  unfold stratopause_tropopause_ratio
 165  rw [phi_cubed_eq]
 166  have h := phi_gt_onePointSixOne
 167  linarith
 168
 169/-- Numerical band: `φ³ ∈ (4.22, 4.24)`, inside empirical layer-ratio
 170band `(3.5, 4.5)`. -/
 171theorem stratopause_tropopause_ratio_band :
 172    4.22 < stratopause_tropopause_ratio ∧
 173    stratopause_tropopause_ratio < 4.24 := by
 174  unfold stratopause_tropopause_ratio
 175  rw [phi_cubed_eq]
 176  have h1 := phi_gt_onePointSixOne
 177  have h2 := phi_lt_onePointSixTwo
 178  refine ⟨?_, ?_⟩ <;> linarith
 179
 180/-- The thermosphere / tropopause ratio: `φ⁷`. -/
 181def thermosphere_tropopause_ratio : ℝ := phi ^ 7
 182
 183theorem thermosphere_tropopause_ratio_pos :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.