ms_luminosity
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not derive the 3.9 exponent from the Recognition Science forcing chain.
- Does not incorporate metallicity, rotation, or other real-star parameters.
- Applies only to objects satisfying the MainSequenceStar structure.
- Provides no conversion to physical units such as solar luminosities.
Lean usage
theorem luminosity_order (s1 s2 : MainSequenceStar) (h : s1.mass < s2.mass) : ms_luminosity s1 < ms_luminosity s2 := by exact luminosity_increases s1.mass s2.mass s1.h_pos hformal statement (Lean)
158noncomputable def ms_luminosity (s : MainSequenceStar) : ℝ := luminosity_scaling s.mass