ms_temperature
plain-language theorem explainer
The definition supplies the temperature scaling T = M^{0.55} for any main sequence star of mass M. Astrophysicists working on Recognition Science models of the HR diagram cite it when establishing the direction of the main sequence. The implementation is a direct power-law assignment on the mass field.
Claim. Let $s$ be a main sequence star with mass $M > 0$. The temperature of $s$ is $T(s) = M^{0.55}$.
background
MainSequenceStar is a structure with a single positive real field mass, representing the main sequence as a 1D curve in (T_eff, L) space. The StellarEvolution module derives stellar relations from Recognition Science by combining nuclear burning equilibrium (RS Gamow factor), radiative transport, and hydrostatic equilibrium, yielding L ∝ M^{3.9} together with virial temperature T_c ∝ M/R. This temperature definition extends the MainSequenceStar structure to support HR diagram analysis.
proof idea
The definition is a direct one-line assignment that raises the mass field of the input MainSequenceStar to the real power 0.55.
why it matters
It supplies the temperature component invoked by the hr_diagram_direction theorem, which proves that higher mass yields both higher luminosity and higher temperature, tracing the main sequence upper-left to lower-right in the HR diagram. The result sits inside the Recognition Science stellar evolution framework that obtains the L ∝ M^{3.9} relation from nuclear efficiency and the RS Gamow factor, as stated in the module documentation. It closes one link in the chain from MainSequenceStar to observable HR properties.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.