MainSequenceStar
plain-language theorem explainer
MainSequenceStar defines a main-sequence star as a positive real mass M. Astrophysicists deriving HR-diagram scalings from nuclear equilibrium and hydrostatic balance cite this structure to index the main-sequence locus. The definition is a bare structure carrying only the mass field and its strict positivity hypothesis.
Claim. A main-sequence star is a real number $M$ satisfying $M > 0$.
background
The module models stellar evolution via Recognition Science, deriving the main-sequence relation $L ∝ M^{3.9}$ from nuclear burning equilibrium (Gamow factor), radiative transport, and hydrostatic equilibrium. The main sequence appears as a one-dimensional curve in $(T_ eff, L)$ space parameterized by mass. Key supporting results listed in the module include virial temperature $T_c ∝ M/R$, luminosity-mass scaling, main-sequence lifetime $t_MS ∝ M^{-2.9}$, and nuclear efficiency $ε_H = 0.007 c^2$.
proof idea
This is a structure definition with an empty proof body. It directly introduces the mass field together with the positivity hypothesis 0 < mass.
why it matters
The structure supplies the base object for downstream results such as hr_diagram_direction (more massive stars are hotter and more luminous) and the derived functions ms_luminosity and ms_temperature. It fills the parameterization step required by the Recognition Science derivation of the HR diagram from nuclear burning and hydrostatic equilibrium, as stated in the module paper RS_Stellar_Evolution_HR_Diagram.tex.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.