virial_temperature

formal source

  53
  54/-- **VIRIAL TEMPERATURE**: T_c ∝ GM m_p / (k_B R)
  55    From the virial theorem applied to a stellar interior. -/
  56noncomputable def virial_temperature (M R : ℝ) : ℝ :=
  57  M / R  -- in natural units where G m_p / k_B = 1
  58
  59/-- Central temperature increases with mass for fixed radius. -/
  60theorem temp_increases_with_mass (M₁ M₂ R : ℝ)
  61    (hM₁ : 0 < M₁) (hM₂ : 0 < M₂) (hR : 0 < R) (h : M₁ < M₂) :
  62    virial_temperature M₁ R < virial_temperature M₂ R := by
  63  unfold virial_temperature
  64  exact div_lt_div_of_pos_right h hR
  65
  66/-- **MAIN SEQUENCE RADIUS SCALING**: R ∝ M^0.8 (from homology relations).
  67    This scaling gives L ∝ M^3.9 when combined with luminosity transport. -/
  68noncomputable def main_sequence_radius (M : ℝ) : ℝ := M ^ (0.8 : ℝ)
  69
  70/-- Radius scales sub-linearly with mass. -/
  71theorem radius_sublinear (M₁ M₂ : ℝ) (hM₁ : 0 < M₁) (h : M₁ < M₂) :
  72    main_sequence_radius M₁ < main_sequence_radius M₂ := by
  73  unfold main_sequence_radius
  74  exact Real.rpow_lt_rpow (le_of_lt hM₁) h (by norm_num)
  75
  76/-! ## Luminosity-Mass Relation -/
  77
  78/-- **LUMINOSITY**: L ∝ M^3.9 for main-sequence stars.
  79    This follows from radiative transport with Kramers opacity κ ∝ ρ T^{-3.5}
  80    and nuclear burning rate ε ∝ ρ T^4 (pp chain). -/
  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