pith. sign in
module module moderate

IndisputableMonolith.Physics.NeutronStarTOV

show as:
view Lean formalization →

This module encodes the Tolman-Oppenheimer-Volkoff hydrostatic equilibrium equation for neutron stars inside the Recognition Science framework. Compact-object astrophysicists cite the system definitions when deriving mass-radius relations and stability bounds. The module supplies the governing ODE, its Newtonian reduction, and auxiliary declarations for the right-hand side and mass limits.

claimThe hydrostatic equilibrium equation is $\frac{dP}{dr} = -(\varepsilon + P)(M + 4\pi r^3 P) / [r^2 (1 - 2M/r)]$ in units with $G = c = 1$, together with the coupled system for enclosed mass $M(r)$ and the Newtonian limit obtained by dropping the $2M/r$ term.

background

Recognition Science derives physics from the J-cost functional equation and forces the constants of nature via the T0-T8 chain. The module imports JcostCore to supply the energy-density terms that enter the fluid equations. The supplied DOC_COMMENT states that the TOV equation governs hydrostatic equilibrium for a static, spherically symmetric perfect fluid and records the natural-unit form used throughout the declarations.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The declarations supply the general-relativistic structure equations that later results on neutron-star mass ranges and dynamical stability will invoke. The module advances the Recognition Science program by embedding the standard TOV system as a prerequisite for observable predictions such as the OV limit. No parent theorems are recorded in the dependency graph.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (18)