luminosity_scaling
plain-language theorem explainer
Luminosity of main-sequence stars scales as L = M^{3.9} in Recognition Science units. Stellar evolution and population synthesis models cite this power law to link nuclear burning rates with radiative transport and the HR diagram. The definition implements the scaling directly via real exponentiation calibrated to Kramers opacity and pp-chain temperature dependence.
Claim. The luminosity $L$ of a main-sequence star of mass $M$ satisfies $L = M^{3.9}$ in RS-native units.
background
Stellar evolution in Recognition Science starts from the RecognitionStructure M that supplies the monoid for composition laws, then combines it with the Gamow energy threshold and virial theorem to fix central temperature. The module derives the main-sequence luminosity-mass relation from equilibrium between nuclear generation (ε ∝ ρ T^4) and radiative diffusion under Kramers opacity (κ ∝ ρ T^{-3.5}). Sibling definitions such as nuclear_efficiency and virial_temperature close the hydrostatic and energy-balance loop.
proof idea
The declaration is a one-line definition that directly assigns luminosity_scaling M := M^{3.9}. No lemmas or tactics are applied; the body is the explicit real power.
why it matters
This definition supplies the mass-luminosity relation used by lifetime_decreases, luminosity_increases, massive_star_more_luminous, ms_lifetime, ms_luminosity, solar_calibration, and solar_lifetime_approx. It realizes the module proposition that L ∝ M^{3.9} follows from Kramers opacity and pp-chain burning, thereby connecting the Recognition Composition Law to observable stellar lifetimes t_MS ∝ M^{-2.9}. The result sits at the interface between the eight-tick recognition cycle and astrophysical scaling relations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.