rs_mass_range_valid
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.