IndisputableMonolith.Physics.SupernovaClassificationFromRS

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Supernova Classification from RS — Astrophysics Depth
   6
   7Five canonical supernova classes (= configDim D = 5):
   8  Type Ia (thermonuclear), Type Ib, Type Ic, Type II-P, Type II-L.
   9
  10Light-curve decline timescales on φ-ladder.
  11
  12Lean status: 0 sorry, 0 axiom.
  13-/
  14
  15namespace IndisputableMonolith.Physics.SupernovaClassificationFromRS
  16
  17inductive SupernovaType where
  18  | typeIa
  19  | typeIb
  20  | typeIc
  21  | typeIIP
  22  | typeIIL
  23  deriving DecidableEq, Repr, BEq, Fintype
  24
  25theorem supernovaType_count : Fintype.card SupernovaType = 5 := by decide
  26
  27structure SupernovaCert where
  28  five_types : Fintype.card SupernovaType = 5
  29
  30def supernovaCert : SupernovaCert where
  31  five_types := supernovaType_count
  32
  33end IndisputableMonolith.Physics.SupernovaClassificationFromRS
  34