Physics Neutron Star Tov

Neutron Star TOV Limit

The Tolman-Oppenheimer-Volkoff (TOV) equation is the general-relativistic condition for hydrostatic equilibrium in a static, spherically symmetric perfect fluid. In Recognition Science, this equation is derived as a cost-minimization condition: the structure of a neutron star minimizes the same recognition cost function that forces other physical laws. The module establishes that this TOV equation reduces to Newtonian hydrostatics in the low-density, weak-gravity limit, and that a maximum stable mass exists where the mass as a function of central pressure turns over.

The TOV equation itself is a differential relation: dP/dr = -(ε + P)(M + 4πr³P/c²) / (r²(1 - 2GM/c²r)). The three general-relativistic corrections are explicit: pressure gravitates (ε + P replaces ε), pressure contributes to the source mass (M + 4πr³P/c² replaces M), and the metric redshift factor (1 - 2M/r)⁻¹ appears. The theorem tov_newtonian_limit proves that when P → 0, the TOV right-hand side equals the Newtonian expression divided by (1 - 2M/r). This is a formal limit, not an approximation: the Lean proof is axiom-clean.

The module defines stability and the maximum mass. A configuration is dynamically stable exactly when the mass increases with central pressure, formalized as strict monotonicity of M(P_c). The maximum mass is the point where the M(P_c) curve turns over; configurations beyond that are unstable. For a free neutron gas, the Oppenheimer-Volkoff limit is 0.71 solar masses, established positive. The module also proves that the true maximum mass exceeds this lower bound when nuclear interactions add repulsive pressure.

The Recognition Science prediction for the maximum neutron star mass is the interval [2.0, 2.5] solar masses. This interval is consistent with the measured masses of PSR J0740+6620 (2.08 M_sun) and PSR J0952-0607 (2.35 M_sun), both of which are established to lie within the range. The TOV limit also exceeds the Chandrasekhar limit for white dwarfs (1.44 M_sun), reflecting that neutron stars require a stronger equation of state.

MODEL tov_rhs · IndisputableMonolith/Physics/NeutronStarTOV.lean

THEOREM tov_newtonian_limit · IndisputableMonolith/Physics/NeutronStarTOV.lean

MODEL ov_limit_solar_masses · IndisputableMonolith/Physics/NeutronStarTOV.lean

THEOREM true_max_exceeds_ov · IndisputableMonolith/Physics/NeutronStarTOV.lean

MODEL rs_mass_range_low · IndisputableMonolith/Physics/NeutronStarTOV.lean

THEOREM psr_j0740_in_range · psr_j0952_in_range · IndisputableMonolith/Physics/NeutronStarTOV.lean

What this page does not claim

No claim that the TOV equation is derived from first principles in the pack; it is given as a structure and the limit theorem is established. No claim that the [2.0, 2.5] solar mass range is a theorem; it is a model prediction. No claim that the measured masses are exact; they are stated as fixed numbers in the pack.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Physics/NeutronStarTOV.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: