ms_lifetime

formal source

 103
 104/-- **MAIN SEQUENCE LIFETIME**: t_MS = ε_H X M / L ∝ M^(1-3.9) = M^(-2.9)
 105    where X ≈ 0.7 is hydrogen mass fraction, ε_H = 0.007 c². -/
 106noncomputable def ms_lifetime (M : ℝ) : ℝ :=
 107  nuclear_efficiency * 0.7 * M / luminosity_scaling M
 108
 109/-- Lifetime decreases with mass (massive stars burn out faster). -/
 110theorem lifetime_decreases (M₁ M₂ : ℝ) (hM₁ : 1 < M₁) (h : M₁ < M₂) :
 111    ms_lifetime M₂ < ms_lifetime M₁ := by
 112  unfold ms_lifetime luminosity_scaling nuclear_efficiency
 113  have hM₁pos : 0 < M₁ := by linarith
 114  have hM₂pos : 0 < M₂ := by linarith
 115  have hpow : M₁ ^ (2.9 : ℝ) < M₂ ^ (2.9 : ℝ) :=
 116    Real.rpow_lt_rpow (le_of_lt hM₁pos) h (by norm_num)
 117  have hpow₁_pos : 0 < M₁ ^ (2.9 : ℝ) := Real.rpow_pos_of_pos hM₁pos _
 118  have hpow₂_pos : 0 < M₂ ^ (2.9 : ℝ) := Real.rpow_pos_of_pos hM₂pos _
 119  have hrecip : 1 / M₂ ^ (2.9 : ℝ) < 1 / M₁ ^ (2.9 : ℝ) :=
 120    one_div_lt_one_div_of_lt hpow₁_pos hpow
 121  have hconst : 0 < (7e-3 : ℝ) * 0.7 := by
 122    norm_num
 123  have hrewrite₁ : (7e-3 : ℝ) * 0.7 * M₁ / M₁ ^ (3.9 : ℝ) =
 124      (7e-3 : ℝ) * 0.7 / M₁ ^ (2.9 : ℝ) := by
 125    rw [show (3.9 : ℝ) = 1 + 2.9 by norm_num, Real.rpow_add hM₁pos, Real.rpow_one]
 126    field_simp [hM₁pos.ne', ne_of_gt (Real.rpow_pos_of_pos hM₁pos _)]
 127  have hrewrite₂ : (7e-3 : ℝ) * 0.7 * M₂ / M₂ ^ (3.9 : ℝ) =
 128      (7e-3 : ℝ) * 0.7 / M₂ ^ (2.9 : ℝ) := by
 129    rw [show (3.9 : ℝ) = 1 + 2.9 by norm_num, Real.rpow_add hM₂pos, Real.rpow_one]
 130    field_simp [hM₂pos.ne', ne_of_gt (Real.rpow_pos_of_pos hM₂pos _)]
 131  rw [hrewrite₂, hrewrite₁]
 132  simpa [one_div] using mul_lt_mul_of_pos_left hrecip hconst
 133
 134/-- **SOLAR LIFETIME**: t_MS(M_sun) ≈ 10 Gyr. -/
 135theorem solar_lifetime_approx :
 136    ms_lifetime 1 = nuclear_efficiency * 0.7 := by