luminosity_increases

formal source

  81noncomputable def luminosity_scaling (M : ℝ) : ℝ := M ^ (3.9 : ℝ)
  82
  83/-- Luminosity increases steeply with mass. -/
  84theorem luminosity_increases (M₁ M₂ : ℝ) (hM₁ : 0 < M₁) (h : M₁ < M₂) :
  85    luminosity_scaling M₁ < luminosity_scaling M₂ := by
  86  unfold luminosity_scaling
  87  exact Real.rpow_lt_rpow (le_of_lt hM₁) h (by norm_num)
  88
  89/-- **SOLAR CALIBRATION**: L_sun corresponds to M = 1 M_sun. -/
  90theorem solar_calibration : luminosity_scaling 1 = 1 := by
  91  unfold luminosity_scaling
  92  simp
  93
  94/-- More massive stars are much more luminous. -/
  95theorem massive_star_more_luminous (M : ℝ) (hM : 1 < M) :
  96    1 < luminosity_scaling M := by
  97  unfold luminosity_scaling
  98  have h1 : (1 : ℝ) = 1 ^ (3.9 : ℝ) := (Real.one_rpow _).symm
  99  rw [h1]
 100  exact Real.rpow_lt_rpow (by norm_num) hM (by norm_num)
 101
 102/-! ## Main Sequence Lifetime -/
 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