newtonian_rhs
plain-language theorem explainer
The Newtonian right-hand side function supplies the classical hydrostatic force term negative energy density times enclosed mass over radius squared. Astrophysicists recovering the non-relativistic limit of neutron star structure equations cite this expression when pressure is negligible and gravity is weak. The definition is a direct algebraic assignment with no lemmas or reductions applied.
Claim. The Newtonian hydrostatic equilibrium term is given by $dP/dr = -ε M / r^2$, where $ε$ is energy density, $M$ the enclosed mass, and $r$ the radial coordinate.
background
The module derives the Tolman-Oppenheimer-Volkoff equation from the Recognition Science framework and proves bounds on maximum neutron star mass. It recovers Newtonian hydrostatics when pressure is much less than energy density and $2M/r$ is much less than 1. Upstream results include the density definition $phi^k$ on the recognition ladder and the core RecognitionStructure $M$ encoding the recognition relation.
proof idea
The definition is introduced as a direct one-line algebraic expression for the Newtonian term without applying any lemmas or tactics.
why it matters
This definition supplies the target expression for the reduction theorem tov_newtonian_limit, which shows the TOV right-hand side equals the Newtonian term divided by $(1 - 2M/r)$ when pressure vanishes. It completes the low-density recovery step in the RS_Neutron_Star_TOV_Limit paper and anchors the link between J-cost minimization in the TOV equation and classical hydrostatic equilibrium.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.