radius_sublinear

formal source

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