gamow_energy_increases_with_T
plain-language theorem explainer
Gamow energy for nuclear fusion increases monotonically with temperature as T to the power 2/3. Stellar modelers cite this monotonicity when deriving main-sequence luminosity from core temperature and fusion rates. The term-mode proof unfolds the explicit formula then applies mul_lt_mul_of_pos_left followed by Real.rpow_lt_rpow on the temperature ratio.
Claim. Let $Z_1 Z_2 > 0$, $μ > 0$, $T_1 > 0$ and $T_1 < T_2$. Then the Gamow energy satisfies $E_G(T_1, Z_1 Z_2, μ) < E_G(T_2, Z_1 Z_2, μ)$, where $E_G(T, Z_1 Z_2, μ) = 1.22 (Z_1 Z_2)^2 μ (T / 10^7)^{2/3}$ (keV) is the peak energy for Coulomb-barrier tunneling.
background
In the Recognition Science treatment of stellar evolution the Gamow energy is the temperature-dependent peak of the nuclear reaction window, defined explicitly as 1.22 Z₁Z₂² μ (T/10⁷)^{2/3} keV. The module derives main-sequence relations (L ∝ M^{3.9}, t_MS ∝ M^{-2.9}) from nuclear-burning equilibrium together with the virial theorem and radiative transport. Upstream results supply the energy-conservation theorem (applied to time-translation symmetry) and the Boltzmann constant k_B, though the present proof uses only the algebraic form of gamow_energy.
proof idea
The term-mode proof unfolds gamow_energy to expose the product 1.22 Z₁Z₂² μ ⋅ (T/10⁷)^{2/3}. It applies mul_lt_mul_of_pos_left to the positive prefactor, reducing the claim to strict increase of the real power. Real.rpow_lt_rpow is then invoked with the hypothesis T₁ < T₂, positivity of the base, and exponent 2/3.
why it matters
The result supplies the temperature dependence required by the RS Gamow factor inside the nuclear-burning equilibrium that yields the observed main-sequence scaling. It directly supports the module's luminosity-mass relation and the paper proposition RS_Stellar_Evolution_HR_Diagram.tex. No downstream uses are recorded; the lemma closes the monotonicity step needed for equilibrium models.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.