IndisputableMonolith.Physics.NeutronStarTOV
The NeutronStarTOV module encodes the Tolman-Oppenheimer-Volkoff hydrostatic equilibrium equation for static spherically symmetric neutron stars in general relativity. Recognition Science researchers modeling compact objects via the phi-ladder would cite it to anchor mass formulas in the J-cost framework. The module proceeds through definitions of the TOV system and right-hand sides, followed by lemmas on the Newtonian limit and stability bounds.
claimThe TOV equation in units with $G=c=1$ reads $dP/dr = -[ε + P][M + 4π r³ P] / [r² (1 - 2M/r)]$, where ε is energy density, P is pressure, and M(r) is the enclosed mass; the module also defines the Newtonian limit and stability predicates for solutions.
background
Recognition Science starts from the J-functional obeying the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). This module imports JcostCore to supply the cost-based definitions of energy and pressure that enter the fluid stress-energy tensor. It presents the TOV equation as the GR condition for hydrostatic equilibrium of a static, spherically symmetric perfect fluid, exactly as stated in the module documentation.
proof idea
The module is organized as a sequence of definitions followed by limit and stability lemmas. It defines TOVSystem, tov_rhs, and newtonian_rhs, then establishes the Newtonian reduction via tov_newtonian_limit. Further definitions introduce TOVSolution together with the predicates IsMaximumMass and IsDynamicallyStable, plus explicit numerical bounds such as ov_limit_solar_masses and the rs_mass_range pair.
why it matters in Recognition Science
The module supplies the general-relativistic structure equations needed to embed neutron-star models inside the Recognition Science phi-ladder and eight-tick octave. It directly implements the TOV equation quoted in the module documentation and prepares the ground for mass-range results that connect to the T8 forcing step and the alpha inverse band. No downstream theorems are yet recorded.
scope and limits
- Does not solve the TOV equation for any specific equation of state.
- Does not treat rotating or time-dependent configurations.
- Does not derive the TOV equation from the J-functional.
- Does not incorporate finite-temperature or composition effects.
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