IndisputableMonolith.Astrophysics.ChandrasekharMassStructure

   1import Mathlib
   2import IndisputableMonolith.Astrophysics.MassToLight
   3
   4namespace IndisputableMonolith
   5namespace Astrophysics
   6namespace ChandrasekharMassStructure
   7
   8open MassToLight
   9
  10/-- Structural content: mass-scale anchors are positive and finite in RS ladder range. -/
  11def chandrasekhar_mass_from_ledger : Prop := 0.5 < ml_derived ∧ ml_derived < 5
  12
  13theorem chandrasekhar_mass_structure : chandrasekhar_mass_from_ledger :=
  14  ml_in_observed_range
  15
  16/-- Chandrasekhar-mass structure implies lower mass-to-light bound. -/
  17theorem chandrasekhar_implies_ml_lower (h : chandrasekhar_mass_from_ledger) :
  18    0.5 < ml_derived :=
  19  h.1
  20
  21/-- Chandrasekhar-mass structure implies upper mass-to-light bound. -/
  22theorem chandrasekhar_implies_ml_upper (h : chandrasekhar_mass_from_ledger) :
  23    ml_derived < 5 :=
  24  h.2
  25
  26end ChandrasekharMassStructure
  27end Astrophysics
  28end IndisputableMonolith
  29