solar_calibration
plain-language theorem explainer
The solar calibration theorem states that the luminosity scaling function returns exactly one when evaluated at unit solar mass. Stellar modelers anchoring mass-luminosity relations to solar observations would cite this result to fix the zero point of the L(M) curve. The proof is a one-line wrapper that unfolds the definition of luminosity scaling and applies simplification to the resulting power.
Claim. Let $L(M) = M^{3.9}$ denote the luminosity scaling for main-sequence stars. Then $L(1) = 1$.
background
The module derives main-sequence relations from Recognition Science by combining nuclear burning equilibrium with radiative transport and hydrostatic equilibrium. The key definition is luminosity scaling, given explicitly as the power law $L(M) = M^{3.9}$ that follows from Kramers opacity scaling as density times temperature to the minus 3.5 together with the pp-chain burning rate scaling as density times temperature to the fourth. The module document states that this yields the observed main-sequence $L$ proportional to $M^{3.9}$ relation and lists related results such as virial temperature scaling and main-sequence lifetime scaling as $M$ to the minus 2.9.
proof idea
The proof is a one-line wrapper. It unfolds the definition of luminosity scaling to obtain the expression $1^{3.9}$ and then applies simplification to reduce the power to the constant 1.
why it matters
This theorem supplies the normalization point for the luminosity-mass scaling used throughout the stellar-evolution development. It directly implements the solar calibration step required by the paper RS_Stellar_Evolution_HR_Diagram.tex so that the derived $L$ proportional to $M^{3.9}$ relation passes through the observed solar values. The result sits inside the broader Recognition Science chain that obtains stellar properties from the J-cost functional and the eight-tick octave structure, though no downstream theorems in the current module depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.