hr_diagram_direction
plain-language theorem explainer
More massive main-sequence stars are both more luminous and hotter. Stellar astrophysicists would cite this when tracing the main sequence on the Hertzsprung-Russell diagram. The proof splits the conjunction, applies the luminosity-increases theorem directly, and reduces the temperature part to a power inequality.
Claim. Let $s_1$ and $s_2$ be main-sequence stars with $M_1 < M_2$. Then the luminosity of $s_1$ is less than the luminosity of $s_2$ and the effective temperature of $s_1$ is less than that of $s_2$, where luminosity is given by the scaling function and temperature by $M^{0.55}$.
background
The StellarEvolution module derives main-sequence relations from Recognition Science nuclear burning equilibrium combined with radiative transport and hydrostatic equilibrium. MainSequenceStar is the structure consisting of a positive real mass that parameterizes the one-dimensional curve in (T_eff, L) space. ms_luminosity extracts luminosity via the scaling function; ms_temperature is the explicit power M^{0.55}. The upstream luminosity_increases theorem states that luminosity_scaling is strictly increasing on positive reals.
proof idea
Term-mode proof. Constructor splits the conjunction. The first conjunct is discharged by direct application of the luminosity_increases theorem to the two masses and the positivity hypothesis. The second conjunct unfolds the temperature definition and invokes Real.rpow_lt_rpow on the positivity, the mass inequality, and the exponent supplied by norm_num.
why it matters
The result fixes the direction of the main sequence on the HR diagram, confirming that higher mass corresponds to upper-left movement. It directly supports the module's listed key results (L ∝ M^3.9, virial temperature, main-sequence lifetime) and the paper RS_Stellar_Evolution_HR_Diagram.tex. No downstream theorems are recorded, leaving the relation available for later lifetime or endpoint calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.