temp_increases_with_mass
plain-language theorem explainer
Central temperature scales linearly with mass at fixed radius under the virial approximation. Stellar modelers working in Recognition Science cite this when building the main-sequence temperature-mass relation ahead of luminosity scalings. The proof reduces to monotonicity of division by a positive constant after the definition is unfolded.
Claim. Let $M_1, M_2, R > 0$ with $M_1 < M_2$. The central temperature satisfies $T_c(M_1, R) < T_c(M_2, R)$, where $T_c(M, R) = M/R$ in units with $G m_p / k_B = 1$.
background
The StellarEvolution module derives main-sequence relations from Recognition Science by combining nuclear burning equilibrium with radiative transport and hydrostatic equilibrium. The upstream definition sets the central temperature to $T_c(M, R) := M/R$ in natural units, with the explicit note that it follows from the virial theorem applied to a stellar interior. This places the result inside the broader chain that produces $L ∝ M^{3.9}$ and main-sequence lifetimes.
proof idea
The term proof unfolds the definition of virial_temperature to expose the ratio form, then applies the lemma div_lt_div_of_pos_right directly to the hypotheses $M_1 < M_2$ and $R > 0$.
why it matters
The result supplies the temperature-mass increase needed to reach the luminosity-mass scaling $L ∝ M^{3.9}$ described in the module documentation for RS_Stellar_Evolution_HR_Diagram.tex. It sits between the virial theorem and the nuclear-efficiency step in the Recognition Science treatment of the HR diagram. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.