`endpoint_classification`

proved

show as: view math explainer →

module: IndisputableMonolith.Physics.StellarEvolution
domain: Physics
line: 146 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.StellarEvolution on GitHub at line 146.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 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
 166  · exact luminosity_increases s₁.mass s₂.mass s₁.h_pos h
 167  · unfold ms_temperature
 168    exact Real.rpow_lt_rpow (le_of_lt s₁.h_pos) h (by norm_num)
 169
 170end StellarEvolution
 171end Physics
 172end IndisputableMonolith

papers checked against this theorem

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