Astrophysics Chandrasekhar Mass Structure Chandrasekhar Mass Structure

The mass-to-light bound

The Chandrasekhar mass is the largest mass a white dwarf star can hold before gravity overwhelms the pressure of its electrons. Above roughly 1.4 times the Sun's mass, the star collapses into a neutron star or black hole. In the Recognition Science framework, the mass scale that appears in this astrophysical limit is not a free parameter. The framework's library, a machine-checked collection of formal theorems, derives a mass ladder from its recognition cost function, and the Chandrasekhar mass is expected to sit on one of its rungs.

The declaration chandrasekhar_mass_structure is a theorem in that library. It states that the derived mass-to-light ratio, written ml_derived, lies strictly between 0.5 and 5. The theorem follows from a prior result, ml_in_observed_range, which anchors the derived quantity inside that interval. Two corollaries follow directly: the lower bound, ml_derived > 0.5, and the upper bound, ml_derived < 5. These are not empirical measurements of any star. They are formal consequences of the framework's internal mass ladder, checked by the kernel of the proof assistant.

The theorem is deliberately narrow. It does not claim that the framework derives the numerical value of the Chandrasekhar mass, such as 1.4 solar masses. It does not claim that any particular white dwarf has been observed with a mass-to-light ratio in this range. The interval from 0.5 to 5 is wide, and the declaration establishes only that the framework's derived mass scale falls inside it. The physical bridge between the recognition ledger, a discrete record of recognition events, and the measured masses of real stars is itself an open target, not a result that has been shown.

What the theorem does establish is structural consistency. The framework's mass ladder produces a finite, positive value in the observed range, rather than a value that diverges or lands far outside astrophysical reality. That is a modest but real check: the internal derivation does not contradict the rough scale of stellar physics. The reader should take the theorem as a placement result, not a derivation of the Chandrasekhar mass itself.

theorem chandrasekhar_mass_structure : chandrasekhar_mass_from_ledger :=
  ml_in_observed_range

/-- Structural content: mass-scale anchors are positive and finite in RS ladder range. -/
def chandrasekhar_mass_from_ledger : Prop := 0.5 < ml_derived ∧ ml_derived < 5

/-- Chandrasekhar-mass structure implies lower mass-to-light bound. -/
theorem chandrasekhar_implies_ml_lower (h : chandrasekhar_mass_from_ledger) :
    0.5 < ml_derived :=
  h.1

/-- Chandrasekhar-mass structure implies upper mass-to-light bound. -/
theorem chandrasekhar_implies_ml_upper (h : chandrasekhar_mass_from_ledger) :
    ml_derived < 5 :=
  h.2

What this page does not claim

The framework derives the numerical value 1.4 solar masses for the Chandrasekhar mass. Any specific white dwarf has been observed with a mass-to-light ratio in the interval 0.5 to 5. The physical bridge between the recognition ledger and real stellar masses is shown.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Astrophysics/ChandrasekharMassStructure.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: