rs_mass_range_high
plain-language theorem explainer
The upper endpoint of the Recognition Science neutron star mass interval is fixed at 2.5 solar masses. Observers comparing measured pulsar masses to theoretical TOV bounds cite this constant to close the predicted range. The declaration is a direct numerical abbreviation with no internal computation or lemma application.
Claim. The upper limit of the RS-predicted neutron star mass range is given by $M_{RS,high}=2.5M_⊙$.
background
The module derives the Tolman-Oppenheimer-Volkoff equation from the Recognition Science J-cost minimization condition and establishes bounds on maximum stable neutron star mass. Key results include the reduction to Newtonian hydrostatics at low density and the existence of a maximum mass where dM/dP_c vanishes. The declaration supplies the concrete upper numerical endpoint of the RS mass interval used to test against observations.
proof idea
The declaration is a direct abbreviation that assigns the real number 2.5 with no tactics or lemmas applied.
why it matters
It is invoked by the theorems psr_j0740_in_range and psr_j0952_in_range to verify that observed masses 2.08 M_⊙ and 2.35 M_⊙ lie inside the RS interval, and by rs_mass_range_valid to confirm the interval is nonempty. The bound completes the mass-range definition that supports the module's claim of consistency between RS predictions and measured neutron star masses, aligning with the TOV maximum-mass existence result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.