TOVSystem
plain-language theorem explainer
The TOVSystem structure supplies the three radial profiles needed to express hydrostatic equilibrium for a static spherical neutron star in general relativity. Modelers working inside the Recognition Science framework cite it when they convert J-cost minimization into the Tolman-Oppenheimer-Volkoff equation and its Newtonian limit. The declaration is introduced as a bare structure definition whose fields are later constrained by the module's subsequent theorems.
Claim. A TOVSystem consists of three functions $ε, P, M : ℝ → ℝ$ giving the energy-density profile, pressure profile, and enclosed-mass function $M(r) = ∫_0^r 4π r'^2 ε(r') dr'$, obeying the Tolman-Oppenheimer-Volkoff hydrostatic balance $dP/dr = -(ε + P)(M + 4π r^3 P)/(r^2 (1 - 2M/r))$ in units where $G = c = 1$.
background
The module derives neutron-star structure from the Recognition Science framework by treating the Tolman-Oppenheimer-Volkoff equation as the stationarity condition for J-cost. It imports the pressure definition from ILG.PressureForm, which supplies an effective source term 4π G a² p, and the density definition from NeutronStarCrustalRegimesFromRS, which sets density(k) = phi^k on the recognition ladder. The two Recognition.M structures supply the underlying three-cycle and recognition map used to close the forcing chain.
proof idea
The declaration is a structure definition that simply names the three fields ε, P, M; no lemmas are applied and no tactics are executed.
why it matters
TOVSystem is the data type on which the module builds its key results: tov_equation_structure (TOV as J-cost minimization), tov_reduces_to_newtonian, and the Oppenheimer-Volkoff lower bound M_OV = 0.71 M_⊙. It therefore supplies the concrete interface between the Recognition Science phi-ladder and classical general-relativistic stellar structure, as stated in the module documentation and the accompanying paper RS_Neutron_Star_TOV_Limit.tex.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.