chandrasekharLimit
plain-language theorem explainer
The definition supplies the Chandrasekhar limit as the rational constant 14/10 in solar masses. Modelers of white dwarf degeneracy pressure cite this fixed value when bounding stellar masses from Pauli-derived exclusion. The body is a direct assignment with no lemma calls or reductions.
Claim. The Chandrasekhar mass limit equals $14/10$ solar masses.
background
The QFT.PauliExclusion module derives the Pauli exclusion principle from ledger single-occupancy for odd-phase fermion entries under the 8-tick cycle. Antisymmetry forces identical states to satisfy ψ(a,a) = 0, which produces the observed shell capacities and the degeneracy pressure scaling P ∝ n^{5/3}. This pressure in turn determines the Chandrasekhar limit for white dwarf stability in three spatial dimensions.
proof idea
The declaration is a direct definition that binds the rational 14/10 to the identifier. No upstream lemmas are applied and no tactics are executed.
why it matters
It supplies the numerical value required by the chandrasekhar field inside the PauliProofSummary structure that collects all exclusion results. The same constant is unfolded in chandrasekhar_approx to prove the bound 1 < limit < 2 and in tov_gt_chandrasekhar to compare against the TOV limit. Within Recognition Science the definition instantiates the stellar consequence of ledger antisymmetry, connecting the eight-tick octave to the observed 1.4 solar mass scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.