lifetime_decreases
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not apply for stellar masses at or below one solar mass.
- Does not incorporate metallicity or convective-core corrections.
- Does not address post-main-sequence evolution or endpoints.
- Does not supply absolute numerical lifetimes, only the inequality direction.
formal statement (Lean)
110theorem lifetime_decreases (M₁ M₂ : ℝ) (hM₁ : 1 < M₁) (h : M₁ < M₂) :
111 ms_lifetime M₂ < ms_lifetime M₁ := by
proof body
Tactic-mode proof.
112 unfold ms_lifetime luminosity_scaling nuclear_efficiency
113 have hM₁pos : 0 < M₁ := by linarith
114 have hM₂pos : 0 < M₂ := by linarith
115 have hpow : M₁ ^ (2.9 : ℝ) < M₂ ^ (2.9 : ℝ) :=
116 Real.rpow_lt_rpow (le_of_lt hM₁pos) h (by norm_num)
117 have hpow₁_pos : 0 < M₁ ^ (2.9 : ℝ) := Real.rpow_pos_of_pos hM₁pos _
118 have hpow₂_pos : 0 < M₂ ^ (2.9 : ℝ) := Real.rpow_pos_of_pos hM₂pos _
119 have hrecip : 1 / M₂ ^ (2.9 : ℝ) < 1 / M₁ ^ (2.9 : ℝ) :=
120 one_div_lt_one_div_of_lt hpow₁_pos hpow
121 have hconst : 0 < (7e-3 : ℝ) * 0.7 := by
122 norm_num
123 have hrewrite₁ : (7e-3 : ℝ) * 0.7 * M₁ / M₁ ^ (3.9 : ℝ) =
124 (7e-3 : ℝ) * 0.7 / M₁ ^ (2.9 : ℝ) := by
125 rw [show (3.9 : ℝ) = 1 + 2.9 by norm_num, Real.rpow_add hM₁pos, Real.rpow_one]
126 field_simp [hM₁pos.ne', ne_of_gt (Real.rpow_pos_of_pos hM₁pos _)]
127 have hrewrite₂ : (7e-3 : ℝ) * 0.7 * M₂ / M₂ ^ (3.9 : ℝ) =
128 (7e-3 : ℝ) * 0.7 / M₂ ^ (2.9 : ℝ) := by
129 rw [show (3.9 : ℝ) = 1 + 2.9 by norm_num, Real.rpow_add hM₂pos, Real.rpow_one]
130 field_simp [hM₂pos.ne', ne_of_gt (Real.rpow_pos_of_pos hM₂pos _)]
131 rw [hrewrite₂, hrewrite₁]
132 simpa [one_div] using mul_lt_mul_of_pos_left hrecip hconst
133
134/-- **SOLAR LIFETIME**: t_MS(M_sun) ≈ 10 Gyr. -/