`rs_mass_range_valid`

proved

show as: view math explainer →

module: IndisputableMonolith.Physics.NeutronStarTOV
domain: Physics
line: 107 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Physics.NeutronStarTOV on GitHub at line 107.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 104abbrev rs_mass_range_low : ℝ := 2.0
 105abbrev rs_mass_range_high : ℝ := 2.5
 106
 107theorem rs_mass_range_valid : rs_mass_range_low < rs_mass_range_high := by norm_num
 108
 109/-- Observed masses are within the RS prediction interval. -/
 110theorem psr_j0740_in_range : rs_mass_range_low ≤ 2.08 ∧ (2.08 : ℝ) ≤ rs_mass_range_high := by
 111  constructor <;> norm_num [rs_mass_range_low, rs_mass_range_high]
 112
 113theorem psr_j0952_in_range : rs_mass_range_low ≤ 2.35 ∧ (2.35 : ℝ) ≤ rs_mass_range_high := by
 114  constructor <;> norm_num [rs_mass_range_low, rs_mass_range_high]
 115
 116/-! ## Chandrasekhar vs. TOV -/
 117
 118/-- The Chandrasekhar limit for white dwarfs:
 119    M_Ch = 1.44 M_sun (electron degeneracy pressure vs. gravity). -/
 120def chandrasekhar_limit : ℝ := 1.44
 121
 122/-- The TOV limit exceeds the Chandrasekhar limit. -/
 123theorem tov_exceeds_chandrasekhar :
 124    chandrasekhar_limit < rs_mass_range_low := by
 125  norm_num [chandrasekhar_limit, rs_mass_range_low]
 126
 127/-- NS are more compact than WDs: same mass budget requires stronger EOS. -/
 128theorem neutron_star_requires_stronger_eos :
 129    -- NS: fully relativistic (GR required), P_central ≫ P_WD
 130    -- WD: semi-relativistic (SR + Newtonian gravity)
 131    chandrasekhar_limit < rs_mass_range_low := tov_exceeds_chandrasekhar
 132
 133end TOV
 134end Physics
 135end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.