psr_j0740_in_range
plain-language theorem explainer
The theorem confirms that the measured mass of pulsar PSR J0740+6620 lies inside the Recognition Science interval for the maximum neutron star mass. Researchers in relativistic astrophysics would cite it when comparing RS predictions against timing observations of massive pulsars. The proof proceeds as a direct one-line wrapper applying the constructor tactic and numerical normalization to the pre-defined range bounds.
Claim. $2.0 M_⊙ ≤ 2.08 M_⊙ ≤ 2.5 M_⊙$, where the bounds are the Recognition Science predictions for the Tolman-Oppenheimer-Volkoff maximum mass derived from nuclear interaction pressure.
background
This declaration sits in the Neutron Star TOV module, which derives the Tolman-Oppenheimer-Volkoff equation from the Recognition Science framework as a J-cost minimization condition. The module establishes structural bounds such as the existence of a maximum stable mass and the Oppenheimer-Volkoff limit for free neutron gas. The upstream definitions supply the concrete interval: rs_mass_range_low := 2.0 and rs_mass_range_high := 2.5, with the explicit statement that M_TOV ∈ [2.0, 2.5] M_sun from RS nuclear interaction pressure, consistent with observations of 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 constructor tactic to split the conjunction into two inequalities, followed by norm_num which normalizes the numerical comparisons using the definitions of rs_mass_range_low and rs_mass_range_high.
why it matters
This result places the observed mass of PSR J0740+6620 inside the RS-predicted interval, supporting consistency of the Recognition Science mass formula with astrophysical data. It builds on the TOV equation structure and maximum mass existence theorems in the same module. The declaration closes a verification step for the RS neutron star bounds in the paper RS_Neutron_Star_TOV_Limit.tex without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.