main_sequence_radius
plain-language theorem explainer
The main sequence radius scaling defines stellar radius as R(M) = M to the power 0.8. Stellar modelers cite it to recover the luminosity-mass relation L proportional to M to the 3.9 when combined with nuclear burning and transport. The definition is introduced as a direct power-law assignment drawn from homology relations with no lemmas or computation required.
Claim. The main-sequence stellar radius scales with mass according to $R(M) = M^{0.8}$.
background
The StellarEvolution module derives the Hertzsprung-Russell diagram from Recognition Science by combining nuclear burning equilibrium (RS Gamow factor) with radiative transport and hydrostatic equilibrium. Key supporting definitions include virial_temperature giving central temperature proportional to M/R, nuclear_efficiency as epsilon_H = 0.007 c squared from helium-4 binding energy, and luminosity_mass_scaling yielding L proportional to M to the 3.9. The module documentation states that the main sequence L proportional to M to the 3.9 relation follows from these elements.
proof idea
The declaration is a direct noncomputable definition assigning the power-law expression M raised to the real number 0.8. No lemmas from upstream results such as interval subtraction or RecognitionStructure are applied; it functions as the base assignment for the radius_sublinear theorem.
why it matters
This radius scaling supplies the relation invoked by the radius_sublinear theorem to establish sub-linear growth with mass. It fills the homology relations step in the module documentation, enabling the L proportional to M to the 3.9 result. In the Recognition Science framework it supports the stellar evolution chain connected to the phi-ladder mass formula and eight-tick octave, though the specific 0.8 exponent is taken from standard homology rather than derived from the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.