true_max_exceeds_ov
plain-language theorem explainer
The declaration shows that the true maximum neutron star mass exceeds the Oppenheimer-Volkoff limit once nuclear interactions are included. Modelers of compact objects cite it to align RS mass predictions in the 2.0-2.5 solar mass interval with pulsar observations such as PSR J0740+6620. The proof reduces directly to linear arithmetic on the supplied strict inequality hypothesis.
Claim. If $0 < M_{TOV} - M_{OV}$, then $M_{OV} < M_{TOV}$, where $M_{TOV}$ is the true maximum mass of a neutron star and $M_{OV}$ is the Oppenheimer-Volkoff limit for a free neutron gas.
background
The module derives the Tolman-Oppenheimer-Volkoff equation from the Recognition Science framework as a J-cost minimization condition under ledger factorization. It recovers Newtonian hydrostatics at low density and establishes that the maximum stable mass satisfies dM/dP_c = 0, with the free-gas OV lower bound at 0.71 solar masses. Upstream results supply nuclear density tiers via phi-ladder scaling and the consistency predicate for backpropagation states.
proof idea
The proof is a one-line wrapper applying the linarith tactic to the hypothesis that M_TOV exceeds the OV limit by a positive amount, yielding the strict inequality directly.
why it matters
This result closes the gap between the free-gas OV bound and the RS-predicted mass range of 2.0-2.5 solar masses arising from nuclear interaction pressure. It supports the parent claims that a maximum mass exists and remains dynamically stable, consistent with phi-forcing and the eight-tick octave. The module references the paper RS_Neutron_Star_TOV_Limit.tex for the full structural bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.