`planckMeasurements`

definition

show as: view math explainer →

module: IndisputableMonolith.Cosmology.Inflation
domain: Cosmology
line: 208 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Cosmology.Inflation on GitHub at line 208.

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

 205}
 206
 207/-- Planck satellite measurements (2018). -/
 208def planckMeasurements : String :=
 209  "n_s = 0.9649 ± 0.0042, r < 0.06 (95% CL), f_NL = 0.9 ± 5.1"
 210
 211/-! ## Falsification Criteria -/
 212
 213/-- RS inflation would be falsified by:
 214    1. n_s significantly different from 0.96-0.97
 215    2. Detection of large r (> 0.01)
 216    3. Detection of significant non-Gaussianity
 217    4. Evidence for non-slow-roll dynamics -/
 218structure InflationFalsifier where
 219  /-- Type of potential falsification. -/
 220  falsifier : String
 221  /-- Current experimental status. -/
 222  status : String
 223
 224/-- Current observations are consistent with RS inflation. -/
 225def experimentalStatus : List InflationFalsifier := [
 226  ⟨"Spectral index", "n_s = 0.965 ± 0.004 matches prediction"⟩,
 227  ⟨"Tensor modes", "r < 0.06, consistent with small r prediction"⟩,
 228  ⟨"Non-Gaussianity", "f_NL consistent with zero"⟩
 229]
 230
 231end Inflation
 232end Cosmology
 233end IndisputableMonolith

papers checked against this theorem

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