psr_j0952_in_range
plain-language theorem explainer
The theorem verifies that the pulsar mass 2.35 solar masses lies inside the Recognition Science interval [2.0, 2.5] solar masses for the TOV maximum. Observational astrophysicists comparing RS nuclear-pressure bounds to timing data for PSR J0952-0607 would cite it. The proof is a one-line term-mode check that splits the conjunction and normalizes the numerical inequalities against the two range abbreviations.
Claim. $M_{RS,low} ≤ 2.35 M_⊙ ≤ M_{RS,high}$ with $M_{RS,low} = 2.0 M_⊙$ and $M_{RS,high} = 2.5 M_⊙$, where the bounds are the RS neutron-star mass range obtained from J-cost minimization in the TOV structure equation.
background
The module derives the Tolman-Oppenheimer-Volkoff equation as the J-cost-minimization condition for neutron-star hydrostatic equilibrium and extracts structural bounds on the maximum stable mass. Key supporting definitions are the pressure term (effective source 4π G a² p) and the two abbreviations that encode the RS mass interval. The low-end abbreviation carries the explicit statement that M_TOV lies in [2.0, 2.5] M_⊙ from RS nuclear interaction pressure and is consistent with PSR J0740+6620 (2.08 M_⊙) and PSR J0952-0607 (2.35 M_⊙). Upstream lemmas supply the universal forcing self-reference structure and the pressure display used to close the TOV derivation.
proof idea
The proof is a one-line wrapper. Constructor splits the conjunction into two separate inequalities; norm_num then evaluates both sides by unfolding the abbreviations rs_mass_range_low and rs_mass_range_high and reducing the resulting numerical comparisons.
why it matters
The declaration supplies the direct numerical link between the RS-derived TOV mass interval and the observed mass of PSR J0952-0607, closing the consistency check stated in the module documentation. It sits inside the broader TOV derivation that begins from J-cost minimization and recovers the Newtonian limit at low density. The result supports the paper claim that RS nuclear pressure yields a maximum mass compatible with the heaviest known pulsars; no open scaffolding remains for this particular numerical check.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.