luminosity_increases
plain-language theorem explainer
For positive real masses M1 < M2 the luminosity scaling function at M1 is strictly less than at M2. Stellar modelers cite this to anchor the main-sequence mass-luminosity relation. The proof is a one-line wrapper that unfolds the scaling definition and applies the real-power monotonicity lemma.
Claim. If $0 < M_1 < M_2$ are real numbers then $M_1^{3.9} < M_2^{3.9}$.
background
The StellarEvolution module derives observable stellar properties from Recognition Science. luminosity_scaling is the noncomputable definition sending mass M to M raised to the power 3.9, obtained from radiative transport under Kramers opacity combined with nuclear burning rate scaling. The module imports the core Recognition structure M and the Cycle3 variant of M, which supply the underlying algebraic recognition framework. The local setting is the derivation of the HR diagram and main-sequence lifetime from virial equilibrium and the Gamow factor, as stated in the module documentation.
proof idea
The proof unfolds luminosity_scaling to obtain the claim M1 ^ 3.9 < M2 ^ 3.9. It then applies the lemma Real.rpow_lt_rpow, feeding the non-negativity of the base from the positivity hypothesis on M1, the given strict mass inequality, and the positivity of the exponent 3.9 via norm_num.
why it matters
This result is invoked directly by hr_diagram_direction to prove that more massive main-sequence stars are both more luminous and hotter, tracing the observed main-sequence slope in the HR diagram. It supplies the concrete L ∝ M^{3.9} step inside the Recognition Science stellar-evolution chain described in the module documentation and the paper RS_Stellar_Evolution_HR_Diagram.tex. The declaration closes a short algebraic link between the luminosity_scaling definition and the global HR-diagram ordering.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.