`configDim`

definition

show as: view math explainer →

module: IndisputableMonolith.Cosmology.CosmicMicrowaveBackgroundFromRS
domain: Cosmology
line: 28 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Cosmology.CosmicMicrowaveBackgroundFromRS on GitHub at line 28.

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

  25namespace IndisputableMonolith.Cosmology.CosmicMicrowaveBackgroundFromRS
  26
  27def baryonRung : ℕ := 44
  28def configDim : ℕ := 5
  29
  30/-- ℓ₁ = baryonRung × configDim = 220. -/
  31def firstPeak : ℕ := baryonRung * configDim
  32theorem firstPeak_eq : firstPeak = 220 := by decide
  33
  34/-- Planck measured value 220 ± 0.5. -/
  35def firstPeakPlanck : ℕ := 220
  36theorem firstPeak_matches_planck : firstPeak = firstPeakPlanck := by decide
  37
  38/-- Second peak ratio ∈ (2.3, 2.4). -/
  39def secondPeakRatio : ℚ := 507 / 220  -- approximate ℓ₂/ℓ₁ ≈ 2.305
  40theorem secondPeakRatio_band : (2.3 : ℝ) < (secondPeakRatio : ℝ) ∧ (secondPeakRatio : ℝ) < 2.4 := by
  41  unfold secondPeakRatio
  42  constructor <;> norm_num
  43
  44structure CMBCert where
  45  first_peak : firstPeak = 220
  46  matches_planck : firstPeak = firstPeakPlanck
  47  second_ratio_band : (2.3 : ℝ) < (secondPeakRatio : ℝ) ∧ (secondPeakRatio : ℝ) < 2.4
  48  decomposition : firstPeak = baryonRung * configDim
  49
  50def cmbCert : CMBCert where
  51  first_peak := firstPeak_eq
  52  matches_planck := firstPeak_matches_planck
  53  second_ratio_band := secondPeakRatio_band
  54  decomposition := rfl
  55
  56end IndisputableMonolith.Cosmology.CosmicMicrowaveBackgroundFromRS

papers checked against this theorem

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