pith. machine review for the scientific record. sign in
theorem proved term proof

massive_star_more_luminous

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  95theorem massive_star_more_luminous (M : ℝ) (hM : 1 < M) :
  96    1 < luminosity_scaling M := by

proof body

Term-mode proof.

  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
 102/-! ## Main Sequence Lifetime -/
 103
 104/-- **MAIN SEQUENCE LIFETIME**: t_MS = ε_H X M / L ∝ M^(1-3.9) = M^(-2.9)
 105    where X ≈ 0.7 is hydrogen mass fraction, ε_H = 0.007 c². -/

depends on (9)

Lean names referenced from this declaration's body.