solar_lifetime_approx
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 in Recognition Science
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.
scope and limits
- Does not compute the numerical lifetime in gigayears or seconds.
- Does not derive the 3.9 luminosity-mass exponent.
- Does not address post-main-sequence phases or mass loss.
- Does not incorporate metallicity or rotation effects.
formal statement (Lean)
135theorem solar_lifetime_approx :
136 ms_lifetime 1 = nuclear_efficiency * 0.7 := by
proof body
Term-mode proof.
137 unfold ms_lifetime luminosity_scaling
138 simp [nuclear_efficiency]
139
140/-! ## Stellar Endpoints -/
141
142/-- Massive stars end as neutron stars when M_final > M_Chandrasekhar. -/