tov_rhs
plain-language theorem explainer
The tov_rhs definition supplies the right-hand side of the Tolman-Oppenheimer-Volkoff hydrostatic equation as obtained from the Recognition Science framework. Neutron star structure modelers cite it when imposing J-cost equilibrium under general-relativistic corrections. The definition is a direct algebraic transcription of the three correction factors to Newtonian balance.
Claim. The right-hand side of the TOV pressure gradient is given by $ - (ε + P) (M + 4π r^3 P) / (r^2 (1 - 2M/r)) $, where ε is energy density, P is pressure, M is enclosed mass, and r is radial coordinate.
background
The NeutronStarTOV module obtains the TOV equation by imposing J-cost minimization at equilibrium inside a neutron star. The upstream equilibrium theorem states that J = 0 at equilibrium. The module imports JcostCore for the cost function and uses the RecognitionStructure M defined in both the main Recognition module and the Cycle3 variant.
proof idea
The definition is a one-line algebraic transcription of the three GR correction factors to Newtonian hydrostatic equilibrium. It directly encodes the replacements (ε + P) for ε, (M + 4πr³P) for M, and the redshift factor (1 - 2M/r)^{-1}.
why it matters
This definition underpins the tov_newtonian_limit theorem that recovers Newtonian hydrostatics when P ≪ ε and 2M/r ≪ 1. It fills the step from J-cost equilibrium to the structural equation for neutron stars and supports the OV lower bound of 0.71 solar masses. In the framework it implements the TOV structure as a consequence of the Recognition Composition Law applied to the phi-ladder in three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.