`cmb_span_configDim`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Physics.CosmicMicrowaveBackgroundTemperatureFromRS on GitHub at line 37.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  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.