massive_star_more_luminous
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the numerical exponent 3.9 from Recognition primitives.
- Does not treat post-main-sequence evolution or mass loss.
- Does not incorporate metallicity or rotation corrections.
- Does not supply absolute luminosity values in physical units.
formal statement (Lean)
95theorem massive_star_more_luminous (M : ℝ) (hM : 1 < M) :
96 1 < luminosity_scaling M := by
proof body
Term-mode proof.
97 unfold luminosity_scaling
98 have h1 : (1 : ℝ) = 1 ^ (3.9 : ℝ) := (Real.one_rpow _).symm
99 rw [h1]
100 exact Real.rpow_lt_rpow (by norm_num) hM (by norm_num)
101
102/-! ## Main Sequence Lifetime -/
103
104/-- **MAIN SEQUENCE LIFETIME**: t_MS = ε_H X M / L ∝ M^(1-3.9) = M^(-2.9)
105 where X ≈ 0.7 is hydrogen mass fraction, ε_H = 0.007 c². -/