IndisputableMonolith.Physics.GravitationalWaveSourcesFromConfigDim

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Gravitational Wave Source Classes from configDim — B12 Depth
   6
   7Five canonical GW source classes (= configDim D = 5):
   8  compact binary inspiral-merger-ringdown, core-collapse supernova,
   9  continuous (rotating neutron star), stochastic background, memory.
  10
  11Each spans a distinct frequency band from mHz (LISA) to kHz (LIGO).
  12
  13Lean status: 0 sorry, 0 axiom.
  14-/
  15
  16namespace IndisputableMonolith.Physics.GravitationalWaveSourcesFromConfigDim
  17
  18inductive GWSourceClass where
  19  | compactBinary
  20  | coreCollapse
  21  | continuous
  22  | stochasticBackground
  23  | memory
  24  deriving DecidableEq, Repr, BEq, Fintype
  25
  26theorem gwSourceClass_count : Fintype.card GWSourceClass = 5 := by decide
  27
  28structure GWSourcesCert where
  29  five_classes : Fintype.card GWSourceClass = 5
  30
  31def gwSourcesCert : GWSourcesCert where
  32  five_classes := gwSourceClass_count
  33
  34end IndisputableMonolith.Physics.GravitationalWaveSourcesFromConfigDim
  35