ov_limit_positive
plain-language theorem explainer
The declaration proves that the Oppenheimer-Volkoff mass limit for a free neutron gas is strictly positive. Compact-object physicists would cite it when anchoring lower bounds on neutron-star masses within general-relativistic hydrostatic equilibrium. The proof is a direct term-mode reduction that unfolds the constant definition and applies numerical normalization.
Claim. $0 < M_{OV}$ where $M_{OV} = 0.71 M_⊙$ is the Oppenheimer-Volkoff limit for a free neutron gas.
background
The module derives the Tolman-Oppenheimer-Volkoff equation from the Recognition Science framework by casting hydrostatic equilibrium as a J-cost minimization condition. Key upstream definitions include the TOV structure as the stationarity condition on the J-cost functional and the reduction to Newtonian hydrostatics at low density. The constant ov_limit_solar_masses supplies the concrete lower bound M_OV ≈ 0.71 M_⊙ for non-interacting neutrons; its documentation states that this value is a lower bound on the true M_TOV because nuclear interactions supply additional repulsive pressure.
proof idea
The proof is a one-line term wrapper. It unfolds the definition of ov_limit_solar_masses to the literal constant 0.71 and invokes norm_num to discharge the inequality 0 < 0.71.
why it matters
The result supplies the positivity needed for the module's structural bounds on maximum neutron-star mass and for the downstream claim that the true M_TOV exceeds the OV limit. It fills the concrete numerical anchor in the Recognition Science derivation of the TOV equation, connecting the general mass-ladder construction to the specific scale of compact objects. The module documentation positions it as the starting point for stability arguments that incorporate nuclear repulsion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.