radius_sublinear
plain-language theorem explainer
The main-sequence radius function is strictly increasing for positive masses. Stellar modelers working within Recognition Science would cite this when establishing the sublinear mass-radius relation on the main sequence. The proof is a one-line term that unfolds the radius definition and invokes the monotonicity of the real exponentiation function with a fixed positive exponent less than one.
Claim. Let $R(M)$ denote the main-sequence radius for mass $M > 0$. Then for all positive reals $M_1 < M_2$, $R(M_1) < R(M_2)$.
background
In the Recognition Science treatment of stellar evolution the main sequence arises from nuclear burning equilibrium combined with radiative transport and hydrostatic equilibrium. The radius-mass relation takes the form of a power law whose exponent is fixed and lies strictly between zero and one, yielding sublinear growth. This module builds on the virial temperature result $T_c$ proportional to $M/R$ and the Gamow energy considerations imported from upstream modules.
proof idea
The proof unfolds the definition of main_sequence_radius to expose a constant times $M$ raised to a fixed real power. It then applies Real.rpow_lt_rpow together with the hypothesis $M_1 < M_2$ and the norm_num tactic to confirm the exponent satisfies the required bounds for strict increase.
why it matters
This theorem supports the derivation of the Hertzsprung-Russell diagram within Recognition Science by establishing sublinear radius growth with mass. It feeds into the luminosity scaling and main-sequence lifetime results listed as siblings in the same module. The result aligns with the framework's self-similar structures and closes a concrete step in the paper RS_Stellar_Evolution_HR_Diagram.tex.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.