chandrasekhar_limit
plain-language theorem explainer
The definition fixes the Chandrasekhar limit at 1.44 solar masses as the maximum white-dwarf mass set by electron degeneracy pressure. Astrophysicists classifying stellar endpoints and comparing white-dwarf versus neutron-star formation cite this constant. The implementation is a direct numerical assignment with no reduction steps or lemmas.
Claim. The Chandrasekhar limit is the constant $M_{Ch} = 1.44 M_⊙$, the maximum mass of a white dwarf supported by electron degeneracy pressure against gravitational collapse.
background
In the Neutron Star TOV module the Chandrasekhar limit supplies the reference mass separating white-dwarf and neutron-star endpoints. The module derives the Tolman-Oppenheimer-Volkoff equation from J-cost minimization and recovers the Newtonian hydrostatic limit at low density. The upstream StellarEvolution result states that massive stars end as neutron stars when final mass exceeds this limit.
proof idea
The definition is a direct numerical assignment of the real number 1.44. No lemmas or tactics are invoked; the value is imported as a standard astrophysical constant for later comparison with RS mass ranges.
why it matters
The constant is used by the theorems neutron_star_requires_stronger_eos and tov_exceeds_chandrasekhar to show that neutron-star structure demands a stronger equation of state than white-dwarf structure. It anchors the RS derivation of the Oppenheimer-Volkoff lower bound (0.71 solar masses) in the paper RS_Neutron_Star_TOV_Limit.tex and connects to the framework's comparison of standard limits with phi-ladder mass predictions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.