lifetime_decreases
plain-language theorem explainer
Massive stars above one solar mass have shorter main-sequence lifetimes than lower-mass stars. Astrophysicists modeling stellar populations or the HR diagram would cite this monotonicity. The proof unfolds the lifetime definition, rewrites it as a positive constant over M to the 2.9, and applies real-number power and reciprocal inequalities to establish the strict decrease.
Claim. For real numbers $M_1, M_2$ satisfying $1 < M_1 < M_2$, the main-sequence lifetime $t_{MS}(M) = 0.0070.7 M / M^{3.9}$ obeys $t_{MS}(M_2) < t_{MS}(M_1)$.
background
The module derives main-sequence relations from Recognition Science via nuclear burning equilibrium and radiative transport. Luminosity scaling is the definition $L(M) = M^{3.9}$, which follows from Kramers opacity and the pp-chain rate. Main-sequence lifetime is the definition $t_{MS}(M) = 0.0070.7 M / L(M)$, yielding the $M^{-2.9}$ scaling. Nuclear efficiency is the constant 0.007 from the helium binding energy fraction. The local setting is the paper RS_Stellar_Evolution_HR_Diagram.tex, which lists virial temperature, luminosity-mass scaling, and stellar endpoints as companion results.
proof idea
The tactic proof unfolds ms_lifetime, luminosity_scaling, and nuclear_efficiency. It obtains positivity of $M_1$, $M_2$ and their 2.9-powers via linarith and rpow_pos_of_pos. It invokes rpow_lt_rpow to get the power inequality, then one_div_lt_one_div_of_lt for the reciprocal. Two rewrite lemmas isolate the 2.9 exponent in the denominator using rpow_add and field_simp. The final step applies mul_lt_mul_of_pos_left to the scaled reciprocals.
why it matters
This theorem supplies the monotonicity half of the main-sequence lifetime scaling $t_{MS} ∝ M^{-2.9}$ inside the stellar-evolution module. It directly supports the paper derivation of the HR diagram and the statement that massive stars burn out faster. Within Recognition Science it is consistent with the self-similar phi-ladder scalings, though it does not invoke the J-function or the T0-T8 forcing chain. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.