solar_lifetime_approx
plain-language theorem explainer
The main-sequence lifetime for unit solar mass equals nuclear efficiency times the hydrogen mass fraction 0.7 in normalized units. Stellar evolution modelers cite this normalization to fix the solar calibration point before scaling to other masses. The proof is a one-line wrapper that unfolds the lifetime definition, substitutes the luminosity scaling at unit mass, and simplifies the constant factor.
Claim. $t_{MS}(M_⊙) = ε_H × 0.7$, where $ε_H$ is the nuclear efficiency (rest-mass fraction converted in hydrogen fusion) and the mass is normalized so that $M_⊙ = 1$.
background
The StellarEvolution module derives main-sequence relations from Recognition Science nuclear burning equilibrium combined with radiative transport and hydrostatic equilibrium. Key definitions are luminosity_scaling(M) := M^{3.9} (from Kramers opacity and pp-chain burning rate), ms_lifetime(M) := nuclear_efficiency * 0.7 * M / luminosity_scaling(M), and nuclear_efficiency := 0.007 (from the 4p → He-4 binding-energy defect). The module_doc states that the L ∝ M^{3.9} relation follows from the RS Gamow factor together with radiative transport, yielding the lifetime scaling t_MS ∝ M^{-2.9}.
proof idea
The proof is a one-line wrapper. It unfolds ms_lifetime and luminosity_scaling, then applies simp on the nuclear_efficiency constant; at M = 1 the luminosity term cancels to 1, leaving the stated product.
why it matters
This result anchors the solar calibration inside the Recognition Science stellar-evolution chain (T5–T8 forcing and RCL structure). It supplies the M = 1 base case for the main-sequence lifetime scaling that feeds downstream stellar-endpoint statements (white-dwarf, neutron-star, black-hole branches). The module_doc links it directly to the paper proposition on the HR diagram from nuclear-burning equilibrium.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.