temp_increases_with_mass

formal source

  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
  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