chandrasekhar_approx
plain-language theorem explainer
The result shows the Chandrasekhar mass limit lies between one and two solar masses. Modelers of white dwarf degeneracy pressure cite this interval when linking ledger single-occupancy to stellar stability. The argument unfolds the explicit rational definition and normalizes the bounds numerically.
Claim. $1 < 14/10 < 2$, where the central term is the Chandrasekhar mass limit in solar masses.
background
The module derives the Pauli exclusion principle from ledger single-occupancy. Fermions are odd-phase ledger entries that accumulate a minus sign through the eight-tick cycle, forcing antisymmetry and therefore single occupancy per quantum state. This yields atomic shell structure and degeneracy pressure in white dwarfs and neutron stars. The upstream definition fixes the Chandrasekhar limit at the rational 14/10.
proof idea
Unfold the definition of the limit to expose the fraction 14/10. Split the conjunction with the constructor tactic. Apply norm_num to discharge both inequalities by direct computation.
why it matters
The bound supplies the Chandrasekhar component inside the pauliProofs summary. It connects ledger single-occupancy to degeneracy pressure, consistent with the eight-tick cycle and the module's target of first-principles shell structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.