`gap45`

definition

show as: view math explainer →

module: IndisputableMonolith.Cosmology.InflationSpectralIndexFromJCost
domain: Cosmology
line: 32 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Cosmology.InflationSpectralIndexFromJCost on GitHub at line 32.

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

formal source

  29namespace IndisputableMonolith.Cosmology.InflationSpectralIndexFromJCost
  30
  31/-- Gap-45 = body-plan ceiling = 45. -/
  32def gap45 : ℕ := 45
  33
  34/-- RS spectral index: n_s = 1 - 2/gap45. -/
  35noncomputable def nsRS : ℝ := 1 - 2 / (gap45 : ℝ)
  36
  37theorem nsRS_val : nsRS = 1 - 2 / 45 := by
  38  unfold nsRS gap45; norm_cast
  39
  40theorem nsRS_lt_one : nsRS < 1 := by
  41  unfold nsRS gap45; norm_num
  42
  43theorem nsRS_gt_zero : nsRS > 0 := by
  44  unfold nsRS gap45; norm_num
  45
  46/-- n_s_RS ∈ (0.955, 0.957). -/
  47theorem nsRS_band : (0.955 : ℝ) < nsRS ∧ nsRS < 0.957 := by
  48  rw [nsRS_val]; norm_num
  49
  50/-- Planck observed value 0.965 is close to RS prediction within 0.01. -/
  51def nsPlanck : ℝ := 0.965
  52theorem nsRS_near_planck : |nsRS - nsPlanck| < 0.015 := by
  53  rw [nsRS_val]
  54  unfold nsPlanck
  55  rw [abs_lt]
  56  constructor <;> norm_num
  57
  58structure SpectralIndexCert where
  59  nsRS_band : (0.955 : ℝ) < nsRS ∧ nsRS < 0.957
  60  nsRS_near_planck : |nsRS - nsPlanck| < 0.015
  61
  62def spectralIndexCert : SpectralIndexCert where

papers checked against this theorem

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