chandrasekhar_limit
plain-language theorem explainer
The declaration defines the Chandrasekhar limit as 1.44 solar masses to mark the white dwarf stability threshold in the Recognition Science stellar evolution model. Astrophysicists classifying stellar remnants or modeling the white dwarf to neutron star transition reference this constant. The definition is a direct numerical assignment with no computation or lemmas applied.
Claim. The Chandrasekhar limit is defined as $M_{Ch} = 1.44 M_⊙$.
background
The Stellar Evolution module derives main sequence relations such as luminosity scaling from nuclear burning equilibrium using the RS Gamow factor together with radiative transport and hydrostatic equilibrium. It introduces virial temperature $T_c ∝ M/R$, nuclear efficiency $ε_H = 0.007 c^2$, and the stellar endpoints distinction among white dwarfs at the Chandrasekhar limit, neutron stars at the TOV limit, and black holes. Upstream the NeutronStarTOV module states the same limit as the mass where electron degeneracy pressure balances gravity, while the Recognition module and Cycle3 supply the base structure M.
proof idea
The definition is a direct one-line assignment of the constant 1.44 with no lemmas or tactics invoked. It replicates the identical definition from the NeutronStarTOV module to maintain consistency across modules.
why it matters
This definition supplies the mass threshold that endpoint_classification applies to separate white dwarf outcomes from neutron star or black hole formation. It supports the downstream NeutronStarTOV theorems tov_exceeds_chandrasekhar and neutron_star_requires_stronger_eos, which establish that the TOV limit exceeds this value and therefore requires a stronger equation of state. In the Recognition Science framework it implements the stellar_endpoints boundary listed in the module documentation and the paper RS_Stellar_Evolution_HR_Diagram.tex.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.