IndisputableMonolith.Astrophysics.StellarEvolutionPhasesFromConfigDim

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Stellar Evolution Phases from configDim — Astrophysics Depth
   6
   7Five canonical stellar-evolution phases (= configDim D = 5) for a
   8sun-like star:
   9  protostar, main sequence, red giant branch, asymptotic giant branch,
  10  white dwarf (or supernova remnant for high-mass).
  11
  12Lean status: 0 sorry, 0 axiom.
  13-/
  14
  15namespace IndisputableMonolith.Astrophysics.StellarEvolutionPhasesFromConfigDim
  16
  17inductive StellarPhase where
  18  | protostar
  19  | mainSequence
  20  | redGiantBranch
  21  | asymptoticGiantBranch
  22  | whiteDwarfOrRemnant
  23  deriving DecidableEq, Repr, BEq, Fintype
  24
  25theorem stellarPhase_count : Fintype.card StellarPhase = 5 := by decide
  26
  27structure StellarEvolutionCert where
  28  five_phases : Fintype.card StellarPhase = 5
  29
  30def stellarEvolutionCert : StellarEvolutionCert where
  31  five_phases := stellarPhase_count
  32
  33end IndisputableMonolith.Astrophysics.StellarEvolutionPhasesFromConfigDim
  34