tov_newtonian_limit
plain-language theorem explainer
The theorem establishes that the Tolman-Oppenheimer-Volkoff right-hand side at vanishing pressure equals the Newtonian hydrostatic right-hand side divided by (1 - 2M/r). Astrophysicists using the Recognition Science framework for neutron star models would cite this reduction when validating the low-density regime against classical gravity. The proof is a direct algebraic simplification obtained by unfolding the two right-hand side definitions and applying field simplification after canceling zero terms.
Claim. For positive real numbers density parameter ε, mass M, and radius r, the Tolman-Oppenheimer-Volkoff right-hand side at zero pressure equals the Newtonian hydrostatic right-hand side divided by (1 - 2M/r): $tov_rhs(ε, 0, M, r) = newtonian_rhs(ε, M, r) / (1 - 2M/r)$.
background
In the Recognition Science framework the Tolman-Oppenheimer-Volkoff equation arises as the J-cost minimization condition for hydrostatic equilibrium inside a neutron star. The module derives this equation from RS-native units and proves structural bounds including the maximum stable mass at the saddle point dM/dP_c = 0. Upstream results supply the maximum-mass definition from coherent assembly over N cycles and the phi-tier structure of nuclear densities.
proof idea
The term proof unfolds the definitions of tov_rhs and newtonian_rhs, then applies simp using mul_zero, add_zero, zero_add and ne_eq to clear additive and multiplicative zeros, followed by field_simp to obtain the stated identity.
why it matters
This reduction confirms consistency between the RS-derived TOV equation and Newtonian gravity at low density, supporting the maximum-mass criterion M_max and the Oppenheimer-Volkoff lower bound of 0.71 solar masses. It fills the low-density limit step in the neutron-star TOV paper and aligns with the phi-ladder mass formula and eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.