IndisputableMonolith.Physics.NeutronStarTOV
Formalizes the Tolman–Oppenheimer–Volkoff hydrostatic equilibrium ODE for static spherical perfect fluids, plus its Newtonian limit, solution/maximum-mass/stability predicates, the classical OV solar-mass bound, and RS neutron-star mass-range constants. Relativists and RS auditors cite it when linking GR stellar structure to the phi-ladder mass window. The module is mostly definitions and comparison lemmas, not a single closed existence theorem.
claimIn natural units $G=c=1$, hydrostatic equilibrium for a static spherically symmetric perfect fluid is $\frac{dP}{dr}=-\frac{(\varepsilon+P)(M+4\pi r^3 P)}{r^2(1-2M/r)}$. The module packages this RHS, the Newtonian RHS, the Newtonian-limit identity, solution and maximum-mass/stability predicates, the Oppenheimer–Volkoff solar-mass limit (positive), a true-max-exceeds-OV comparison, and RS low/high mass-range constants.
background
The Tolman–Oppenheimer–Volkoff (TOV) equation is the GR replacement for Newtonian hydrostatic balance in a static, spherically symmetric star modeled as a perfect fluid. Pressure gradient is sourced by the enclosed mass-energy and stiffened by relativistic redshift and curvature factors; the denominator $1-2M/r$ encodes the Schwarzschild factor.
In natural units the classical form collapses to $dP/dr=-(\varepsilon+P)(M+4\pi r^3 P)/(r^2(1-2M/r))$. The Newtonian counterpart drops the relativistic corrections and recovers $dP/dr\approx-\varepsilon M/r^2$ (or the usual $GM\rho/r^2$ form when $G$ is restored).
This module sits in the Physics domain and imports the J-cost compatibility surface only as a shared cost primitive; the stellar-structure content itself is classical GR plus named RS mass-window constants (rs_mass_range_low / rs_mass_range_high) for later comparison with the phi-ladder mass formula.
proof idea
Definition-and-predicate module rather than a single deep proof. It introduces the TOV system record and the two right-hand sides (tov_rhs, newtonian_rhs), then a limit lemma equating TOV to Newtonian structure when relativistic corrections vanish. Solution, maximum-mass, and dynamical-stability are Prop-level predicates on those data. Numeric/comparison facts pin the classical OV solar-mass scale (positivity and that a true maximum exceeds OV) and expose the RS low/high mass-range constants as named bounds. No global existence/uniqueness theorem for the ODE is claimed here.
why it matters in Recognition Science
Neutron-star maximum mass is a sharp GR+EOS observable; the classical OV limit sits near $0.7,M_\odot$ for free neutrons, while modern EOS and observations push the true ceiling above $2,M_\odot$. Packaging TOV, the OV benchmark, and RS mass-range endpoints in one place lets later RS physics modules test whether phi-ladder baryon masses and the eight-tick/D=3 forcing chain land inside the astrophysically allowed window.
No downstream Lean consumers are wired yet (used_by empty), so the module is an upstream physics interface: it supplies the ODE language and the OV-versus-true-max comparison that a mass-formula or stability argument would cite. It does not itself invoke T5–T8 or the Recognition Composition Law; those enter only when RS mass rungs are compared to rs_mass_range_low/high.
scope and limits
- Does not prove global existence or uniqueness of TOV solutions for a given EOS.
- Does not encode a realistic nuclear EOS or integrate the ODE numerically.
- Does not derive the OV solar-mass number from RS first principles.
- Does not claim dynamical stability criteria beyond a named predicate.
- Does not connect mass ranges to the phi-ladder formula inside this module.
depends on (1)
declarations in this module (18)
-
structure
TOVSystem -
def
tov_rhs -
def
newtonian_rhs -
theorem
tov_newtonian_limit -
structure
TOVSolution -
def
IsMaximumMass -
def
IsDynamicallyStable -
def
ov_limit_solar_masses -
theorem
ov_limit_positive -
theorem
true_max_exceeds_ov -
abbrev
rs_mass_range_low -
abbrev
rs_mass_range_high -
theorem
rs_mass_range_valid -
theorem
psr_j0740_in_range -
theorem
psr_j0952_in_range -
def
chandrasekhar_limit -
theorem
tov_exceeds_chandrasekhar -
theorem
neutron_star_requires_stronger_eos