`CMBObservable`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.CosmicMicrowaveBackgroundTemperatureFromRS
domain: Physics
line: 26 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Physics.CosmicMicrowaveBackgroundTemperatureFromRS on GitHub at line 26.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  23namespace IndisputableMonolith.Physics.CosmicMicrowaveBackgroundTemperatureFromRS
  24open Constants
  25
  26inductive CMBObservable where
  27  | temperature | spectralIndex | tensorScalar | baryonDensity | darkEnergy
  28  deriving DecidableEq, Repr, BEq, Fintype
  29
  30theorem cmbObservableCount : Fintype.card CMBObservable = 5 := by decide
  31
  32/-- CMB temperature ∈ (2.7, 2.8) K (structural band). -/
  33def cmbTempLow : ℝ := 2.7
  34def cmbTempHigh : ℝ := 2.8
  35
  36/-- The 5 CMB observables span the 5-dimensional recognition parameter space. -/
  37theorem cmb_span_configDim : Fintype.card CMBObservable = 5 := cmbObservableCount
  38
  39structure CMBTempCert where
  40  five_observables : Fintype.card CMBObservable = 5
  41
  42def cmbTempCert : CMBTempCert where
  43  five_observables := cmbObservableCount
  44
  45end IndisputableMonolith.Physics.CosmicMicrowaveBackgroundTemperatureFromRS

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.