massive_star_more_luminous
plain-language theorem explainer
Stars exceeding one solar mass in mass exhibit luminosity exceeding unity under the adopted scaling. Stellar population modelers and HR-diagram analysts cite the result to justify the steep upper-main-sequence branch. The argument reduces to unfolding the power-law definition and invoking the strict monotonicity of real exponentiation for positive exponent.
Claim. Let $M$ be stellar mass in solar units. If $M > 1$, then the luminosity scaling $L(M) = M^{3.9}$ satisfies $L(M) > 1$.
background
The StellarEvolution module derives main-sequence relations from Recognition Science by combining hydrostatic equilibrium, radiative transport with Kramers opacity, and nuclear burning rates. Luminosity_scaling is introduced as the explicit power $M^{3.9}$ that encodes the combined dependence of energy generation and opacity on central temperature and density. The module also records the companion relations virial_temperature scaling as $T_c$ proportional to $M/R$ and main-sequence lifetime scaling as $M^{-2.9}$.
proof idea
The term proof unfolds luminosity_scaling to expose the real power $M^{3.9}$, rewrites the constant 1 as $1^{3.9}$, and closes by the lemma Real.rpow_lt_rpow that preserves strict inequality under positive exponentiation when the base is increased.
why it matters
The declaration supplies the monotonicity step required for the main-sequence lifetime formula recorded in the same module. It thereby connects the nuclear-efficiency and Gamow-energy results to the overall HR-diagram construction that the module presents as following from the Recognition Science forcing chain and the recognition composition law. No downstream theorems are yet attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.