TOVSystem

formal source

  32
  33    In natural units (G = c = 1):
  34    dP/dr = -(ε + P)(M + 4πr³P) / (r²(1 - 2M/r)) -/
  35structure TOVSystem where
  36  ε : ℝ → ℝ  -- energy density profile ε(r)
  37  P : ℝ → ℝ  -- pressure profile P(r)
  38  M : ℝ → ℝ  -- mass function M(r) = ∫₀ʳ 4πr'²ε(r')dr'
  39
  40/-- GR corrections to Newtonian hydrostatics:
  41    Factor 1: (ε + P) replaces ε — pressure gravitates in GR
  42    Factor 2: (M + 4πr³P) replaces M — pressure contributes to source
  43    Factor 3: (1 - 2M/r)⁻¹ — metric redshift factor -/
  44noncomputable def tov_rhs (ε P M r : ℝ) : ℝ :=
  45  -(ε + P) * (M + 4 * Real.pi * r^3 * P) / (r^2 * (1 - 2 * M / r))
  46
  47/-- Newtonian hydrostatic equilibrium: dP/dr = -ε M / r² -/
  48noncomputable def newtonian_rhs (ε M r : ℝ) : ℝ := -ε * M / r^2
  49
  50/-- **TOV REDUCES TO NEWTONIAN at low density**:
  51    When P ≪ ε (non-relativistic) and 2M/r ≪ 1 (weak gravity),
  52    TOV → Newtonian hydrostatics. -/
  53theorem tov_newtonian_limit (ε M r : ℝ) (hε : 0 < ε) (hM : 0 < M) (hr : 0 < r) :
  54    -- In the limit P → 0: tov_rhs ε 0 M r = newtonian_rhs ε M r / (1 - 2M/r)
  55    tov_rhs ε 0 M r = newtonian_rhs ε M r / (1 - 2 * M / r) := by
  56  unfold tov_rhs newtonian_rhs
  57  simp only [mul_zero, add_zero, zero_add, ne_eq]
  58  field_simp
  59
  60/-! ## Maximum Mass Criterion -/
  61
  62/-- The maximum neutron star mass occurs at the saddle point of M(P_c):
  63    dM/dP_c = 0 at M = M_max.
  64    Configurations with M > M_max are dynamically unstable. -/
  65structure TOVSolution where