radius_sublinear
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the specific numerical exponent from Recognition Science axioms.
- Does not address the validity of the main-sequence approximation outside a limited mass range.
- Does not incorporate effects such as rotation or magnetic fields.
formal statement (Lean)
71theorem radius_sublinear (M₁ M₂ : ℝ) (hM₁ : 0 < M₁) (h : M₁ < M₂) :
72 main_sequence_radius M₁ < main_sequence_radius M₂ := by
proof body
Term-mode proof.
73 unfold main_sequence_radius
74 exact Real.rpow_lt_rpow (le_of_lt hM₁) h (by norm_num)
75
76/-! ## Luminosity-Mass Relation -/
77
78/-- **LUMINOSITY**: L ∝ M^3.9 for main-sequence stars.
79 This follows from radiative transport with Kramers opacity κ ∝ ρ T^{-3.5}
80 and nuclear burning rate ε ∝ ρ T^4 (pp chain). -/