`rsPredictions`

definition

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Cosmology.Inflation on GitHub at line 201.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 198  f_NL : ℝ -- Non-Gaussianity parameter
 199
 200/-- RS predictions for N = 60 e-foldings. -/
 201noncomputable def rsPredictions : InflationPredictions := {
 202  n_s := 1 - 2/60,  -- ≈ 0.967
 203  r := 8/60^2,      -- ≈ 0.002
 204  f_NL := 0         -- Negligible
 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

papers checked against this theorem

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