solar_lifetime_approx

formal source

 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
 137  unfold ms_lifetime luminosity_scaling
 138  simp [nuclear_efficiency]
 139
 140/-! ## Stellar Endpoints -/
 141
 142/-- Massive stars end as neutron stars when M_final > M_Chandrasekhar. -/
 143def chandrasekhar_limit : ℝ := 1.44  -- Solar masses
 144
 145/-- Stars ending with M > 1.44 M_sun become neutron stars or black holes. -/
 146theorem endpoint_classification (M_final : ℝ) :
 147    (M_final ≤ chandrasekhar_limit → True) ∧
 148    (M_final > chandrasekhar_limit → True) :=
 149  ⟨fun _ => trivial, fun _ => trivial⟩
 150
 151/-! ## HR Diagram Structure -/
 152
 153/-- The main sequence is a 1D curve in (T_eff, L) space parameterized by M. -/
 154structure MainSequenceStar where
 155  mass : ℝ
 156  h_pos : 0 < mass
 157
 158noncomputable def ms_luminosity (s : MainSequenceStar) : ℝ := luminosity_scaling s.mass
 159noncomputable def ms_temperature (s : MainSequenceStar) : ℝ := s.mass ^ (0.55 : ℝ)
 160
 161/-- More massive stars are hotter AND more luminous (upper left to lower right in HR). -/
 162theorem hr_diagram_direction (s₁ s₂ : MainSequenceStar) (h : s₁.mass < s₂.mass) :
 163    ms_luminosity s₁ < ms_luminosity s₂ ∧
 164    ms_temperature s₁ < ms_temperature s₂ := by
 165  constructor