neutron_star_requires_stronger_eos
plain-language theorem explainer
Neutron stars require a stiffer equation of state than white dwarfs because their RS-derived lower mass bound of 2.0 solar masses exceeds the Chandrasekhar limit of 1.44 solar masses. Astrophysicists modeling the transition from semi-relativistic white dwarfs to fully relativistic neutron stars would cite this when bounding compact-object stability. The proof is a direct one-line term application of the tov_exceeds_chandrasekhar theorem.
Claim. The Chandrasekhar limit $M_{Ch} = 1.44 M_⊙$ for white dwarfs is strictly less than the RS neutron-star mass-range lower bound $M_{RS,low} = 2.0 M_⊙$.
background
The module derives the Tolman-Oppenheimer-Volkoff equation from the Recognition Science J-cost framework and establishes structural bounds on neutron-star maximum mass. Key upstream definitions are chandrasekhar_limit (1.44 solar masses, electron degeneracy pressure versus gravity) and rs_mass_range_low (2.0 solar masses, the lower end of the RS neutron-star mass interval consistent with PSR J0740+6620 and PSR J0952-0607). The immediate predecessor is the theorem tov_exceeds_chandrasekhar, whose doc-comment states: “The TOV limit exceeds the Chandrasekhar limit.” The sibling structure required supplies the minimal hypotheses needed to state these mass comparisons.
proof idea
This is a one-line term proof that directly applies the tov_exceeds_chandrasekhar theorem.
why it matters
The result sharpens the distinction between white-dwarf and neutron-star regimes inside the RS TOV derivation, confirming that the same mass budget demands stronger nuclear pressure support once general-relativistic effects dominate. It sits downstream of the module’s core claims (tov_equation_structure, maximum_mass_exists, ov_lower_bound) and the paper RS_Neutron_Star_TOV_Limit.tex. No downstream uses are recorded yet, leaving open the question of how this bound propagates into explicit TOV solutions or stability criteria.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.