ms_lifetime
plain-language theorem explainer
Main sequence lifetime for a star of mass M equals nuclear efficiency times 0.7 times M divided by luminosity scaling. Stellar evolution models cite this scaling to obtain t_MS proportional to M to the power of negative 2.9. The definition composes the fixed nuclear efficiency constant directly with the M to the 3.9 luminosity law.
Claim. $t_{MS}(M) = 0.007 · 0.7 · M / L(M)$ where $L(M) = M^{3.9}$ and the constant 0.007 is the fraction of rest mass converted to energy in hydrogen fusion.
background
The Stellar Evolution module derives main-sequence relations from nuclear burning equilibrium, radiative transport with Kramers opacity, and hydrostatic equilibrium. Nuclear efficiency is the fraction of rest mass converted to energy in 4p to He-4 fusion, fixed at 0.007. Luminosity scaling states L proportional to M to the 3.9 from the pp-chain burning rate combined with opacity scaling.
proof idea
One-line definition that multiplies the nuclear efficiency constant by 0.7 and M then divides by the luminosity scaling function.
why it matters
This definition supplies the main sequence lifetime used by lifetime_decreases to prove massive stars burn out faster and by solar_lifetime_approx to recover the 10 Gyr solar value. It fills the main_sequence_lifetime step in RS_Stellar_Evolution_HR_Diagram.tex, linking nuclear efficiency to the overall mass-luminosity relation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.