ms_luminosity
plain-language theorem explainer
ms_luminosity equips each main-sequence star with a luminosity value drawn from the established M to the 3.9 power scaling. Stellar population modelers and HR-diagram theorists cite it when assigning luminosities from mass alone. The definition is realized as a direct one-line wrapper around the luminosity_scaling function applied to the star's mass field.
Claim. For a main-sequence star $s$ with mass $M > 0$, the luminosity satisfies $L(s) = M^{3.9}$ (in RS-native units).
background
The StellarEvolution module derives main-sequence properties from Recognition Science, with the luminosity-mass relation L ∝ M^{3.9} obtained from nuclear burning equilibrium (RS Gamow factor), radiative transport under Kramers opacity κ ∝ ρ T^{-3.5}, and hydrostatic equilibrium via the virial theorem. MainSequenceStar is the structure consisting of a positive real mass that parameterizes the one-dimensional curve of stars in (T_eff, L) space. The upstream luminosity_scaling supplies the explicit form L(M) := M^{3.9}, justified by the nuclear burning rate ε ∝ ρ T^4 for the proton-proton chain.
proof idea
This definition is a one-line wrapper that applies luminosity_scaling directly to the mass component of the MainSequenceStar structure.
why it matters
This definition supplies the luminosity values required by the downstream theorem hr_diagram_direction, which establishes that higher-mass main-sequence stars are both more luminous and hotter, tracing the main-sequence direction on the HR diagram. It implements the luminosity-mass scaling from the RS stellar evolution paper, consistent with the framework's derivation of stellar properties from the J-cost and forcing chain. No open questions attach directly to this definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.