ov_limit_solar_masses
plain-language theorem explainer
The declaration defines the Oppenheimer-Volkoff limit for a free neutron gas at 0.71 solar masses as the baseline maximum mass in the Recognition Science TOV derivation. Neutron-star modelers cite this value when separating the non-interacting case from interaction-enhanced bounds. The definition is a direct numerical assignment with no lemmas or computation.
Claim. The Oppenheimer-Volkoff limit for non-interacting neutrons is $M_{OV} = 0.71 M_⊙$.
background
The module derives the Tolman-Oppenheimer-Volkoff equation from the Recognition Science framework as the J-cost-minimization condition for neutron-star hydrostatic equilibrium. Key results include the reduction to Newtonian hydrostatics at low density and the existence of a maximum stable mass where dM/dP_c = 0. The OV limit treats the free neutron gas without interactions and supplies the lower bound on the true maximum mass once nuclear repulsion is restored.
proof idea
Direct numerical definition assigning the constant 0.71 to the real number ov_limit_solar_masses. No lemmas or tactics are applied.
why it matters
This definition anchors the lower bound on neutron-star maximum mass within the RS TOV analysis. It is used by ov_limit_positive to establish positivity and by true_max_exceeds_ov to show that nuclear interactions raise the limit above 0.71 solar masses. The value matches the classical Oppenheimer-Volkoff result for free neutrons and connects to the module's statement that the TOV equation arises as J-cost minimization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.