rs_mass_range_low
plain-language theorem explainer
Recognition Science sets the lower edge of the maximum stable neutron-star mass at 2.0 solar masses on the basis of nuclear interaction pressure. Modelers of the Tolman-Oppenheimer-Volkoff equation and observers comparing PSR J0740+6620 or PSR J0952-0607 would cite this constant. The declaration is introduced as a direct numeric abbreviation carrying no proof obligations.
Claim. The Recognition Science lower bound on the maximum neutron-star mass is $2.0 M_⊙$, forming the interval $[2.0, 2.5] M_⊙$ that follows from RS nuclear pressure.
background
The NeutronStarTOV module treats the Tolman-Oppenheimer-Volkoff equation as the J-cost-minimization condition for hydrostatic equilibrium in the Recognition Science framework. Upstream results recalled in the module include the reduction of TOV to Newtonian hydrostatics at low density and the existence of a maximum stable mass satisfying dM/dP_c = 0; the module also states the Oppenheimer-Volkoff limit of 0.71 solar masses for a free neutron gas. The local setting is the derivation of structural bounds on neutron-star mass from RS nuclear interaction pressure, as described in the module documentation.
proof idea
Numeric constant introduced by direct assignment; no lemmas or tactics are applied.
why it matters
This constant supplies the lower edge of the RS mass interval checked against pulsar observations in psr_j0740_in_range and psr_j0952_in_range. It is invoked to establish that the TOV limit exceeds the Chandrasekhar limit in tov_exceeds_chandrasekhar, thereby requiring a stronger equation of state for neutron stars. Within the Recognition Science framework the value encodes the effect of nuclear interaction pressure on the maximum stable mass and is consistent with the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.