TOVSolution

formal source

  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
  66  M_of_Pc : ℝ → ℝ  -- mass as function of central pressure
  67  R_of_Pc : ℝ → ℝ  -- radius as function of central pressure
  68
  69/-- The maximum mass is where the M(P_c) curve turns over. -/
  70def IsMaximumMass (sol : TOVSolution) (P_c_max M_max : ℝ) : Prop :=
  71  sol.M_of_Pc P_c_max = M_max ∧
  72  -- At P_c_max, the mass has a local maximum:
  73  ∀ P_c : ℝ, P_c ≠ P_c_max → sol.M_of_Pc P_c ≤ M_max
  74
  75/-- **STABILITY CRITERION**: The TOV stability condition for a NS.
  76    Configuration is stable iff dM/dρ_c > 0 (mass increases with central density).
  77    Above M_max, this condition fails. -/
  78def IsDynamicallyStable (sol : TOVSolution) (P_c : ℝ) : Prop :=
  79  StrictMonoOn sol.M_of_Pc (Set.Iio P_c)
  80
  81/-! ## Oppenheimer-Volkoff Limit -/
  82
  83/-- **THE OPPENHEIMER-VOLKOFF LIMIT** (free neutron gas, no interactions):
  84    M_OV ≈ 0.71 M_sun.
  85
  86    This is a lower bound on the true M_TOV since nuclear interactions
  87    provide additional repulsive pressure. -/
  88noncomputable def ov_limit_solar_masses : ℝ := 0.71
  89
  90/-- The OV limit is positive. -/
  91theorem ov_limit_positive : 0 < ov_limit_solar_masses := by
  92  unfold ov_limit_solar_masses; norm_num
  93
  94/-- The true M_TOV exceeds the OV limit due to nuclear interactions. -/
  95theorem true_max_exceeds_ov (M_TOV : ℝ) (h_interactions : 0 < M_TOV - ov_limit_solar_masses) :