rs_mass_range_valid
The declaration verifies that the lower edge of the Recognition Science neutron star mass interval lies below the upper edge. Compact object modelers cite it when confirming that the predicted window contains observed pulsar masses such as PSR J0740+6620. The proof reduces to a single numerical normalization step on the defining constants.
claimThe lower bound of the Recognition Science neutron star mass range is strictly less than the upper bound: $2.0 < 2.5$ in solar masses.
background
This module derives the Tolman-Oppenheimer-Volkoff equation from the Recognition Science framework by casting it as a J-cost minimization condition on the spacetime interval. Supporting results include the low-density reduction to Newtonian hydrostatics and the existence of a maximum stable mass at vanishing dM/dP_c. The mass bounds are introduced as real constants 2.0 and 2.5 solar masses, documented as consistent with PSR J0740+6620 (2.08 M_sun) and PSR J0952-0607 (2.35 M_sun).
proof idea
The proof is a one-line wrapper that applies the norm_num tactic to compare the two real constants directly.
why it matters in Recognition Science
This result anchors the internal consistency of the [2.0, 2.5] solar mass window predicted for neutron stars under Recognition Science nuclear pressure. It supports the structural bounds derived from the TOV equation in the module and the paper RS_Neutron_Star_TOV_Limit.tex. Within the framework the interval aligns with the phi-ladder mass formula, though the specific edges here are set by the RS interaction pressure rather than the full eight-tick scaling.
scope and limits
- Does not derive the numerical values of the bounds from the J-cost functional.
- Does not establish dynamical stability inside the interval.
- Does not incorporate rotation or magnetic fields into the TOV solution.
formal statement (Lean)
107theorem rs_mass_range_valid : rs_mass_range_low < rs_mass_range_high := by norm_num
proof body
Term-mode proof.
108
109/-- Observed masses are within the RS prediction interval. -/