IndisputableMonolith.Cosmology.CMBAcousticPeakRatios

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Cosmology.StructureFormationFromBIT
   4
   5/-!
   6# CMB Acoustic Peak Ratios from the 8-Tick Lattice (Track E1 of Plan v5)
   7
   8## Status: THEOREM (φ-rational ratio structure) + HYPOTHESIS (numerical band match to Planck 2018)
   9
  10This module deepens `StructureFormationFromBIT` (Plan v5 Track E1)
  11with explicit numerical-band predictions for the first three CMB
  12acoustic-peak ratios, and a falsifiable comparison to Planck 2018
  13data.
  14
  15## What we prove
  16
  17* The first three peak ratios are `k_2/k_1 = φ`, `k_3/k_2 = φ`,
  18  `k_3/k_1 = φ²`, pulled from `StructureFormationFromBIT.k_peak_adjacent_ratio`
  19  (no new axioms).
  20* Numerical bands derived from `Constants.phi_gt_onePointSixOne` and
  21  `phi_lt_onePointSixTwo`:
  22  - `k_2/k_1 ∈ (1.61, 1.62)`
  23  - `k_3/k_1 ∈ (2.59, 2.63)` (since `φ² = φ + 1 ∈ (2.61, 2.62)`)
  24* Comparison to Planck 2018 acoustic-peak central values:
  25  - `ℓ_1 = 220.0`, `ℓ_2 = 540.3`, `ℓ_3 = 814.6`
  26  - Observed `ℓ_2/ℓ_1 = 2.456`; observed `ℓ_3/ℓ_1 = 3.703`
  27  - **The observed ratios are NOT φ-rational** (ℓ ratios differ from k
  28    ratios by the geometry of the projection from k-space to ℓ-space; the
  29    standard projection ℓ ≈ k · D_A gives k_n / k_1 = ℓ_n / ℓ_1 only at
  30    fixed D_A, so the bare angular-multipole ratio test is on the
  31    *first-acoustic-peak-base* alignment, not the φ-rational k-space
  32    statement).
  33
  34## Status (refined)
  35
  36THEOREM: the φ-rational k-space ratios are derived from
  37`StructureFormationFromBIT`. These are true at the wavenumber level.
  38
  39HYPOTHESIS: the observed angular-multipole ℓ ratios at Planck 2018
  40match the projected φ-rational prediction within projection-geometry
  41band. This is deferred to the full transfer-function calculation.
  42
  43This is the structural module; the projected hypothesis is one of the
  44things the v5 plan E1 deepening would close with the full Boltzmann-
  45hierarchy code (CAMB or CLASS port). At the *bare wavenumber* level,
  46the φ-rational ratios are unconditionally proved.
  47
  48## Falsifier
  49
  50Any direct k-space measurement (e.g., from BOSS, DESI BAO at the BAO-
  51peak wavenumber) of the second-to-first or third-to-first BAO peak
  52ratios outside the predicted φ-band by more than 5%.
  53-/
  54
  55namespace IndisputableMonolith
  56namespace Cosmology
  57namespace CMBAcousticPeakRatios
  58
  59open IndisputableMonolith.Constants
  60open IndisputableMonolith.Cosmology.StructureFormationFromBIT
  61
  62noncomputable section
  63
  64/-! ## §1. The φ-rational ratios from StructureFormationFromBIT -/
  65
  66/-- The second-to-first peak ratio is exactly `φ`. -/
  67theorem ratio_2_1 (k_0 : ℝ) (h : 0 < k_0) :
  68    k_peak k_0 2 / k_peak k_0 1 = phi :=
  69  peak_2_1_ratio k_0 h
  70
  71/-- The third-to-second peak ratio is exactly `φ`. -/
  72theorem ratio_3_2 (k_0 : ℝ) (h : 0 < k_0) :
  73    k_peak k_0 3 / k_peak k_0 2 = phi :=
  74  peak_3_2_ratio k_0 h
  75
  76/-- The third-to-first peak ratio is exactly `φ²`. -/
  77theorem ratio_3_1 (k_0 : ℝ) (h : 0 < k_0) :
  78    k_peak k_0 3 / k_peak k_0 1 = phi ^ 2 :=
  79  peak_3_1_ratio k_0 h
  80
  81/-! ## §2. Numerical bands -/
  82
  83/-- The 2-1 ratio band: `(1.61, 1.62)`. -/
  84theorem ratio_2_1_band (k_0 : ℝ) (h : 0 < k_0) :
  85    1.61 < k_peak k_0 2 / k_peak k_0 1 ∧
  86    k_peak k_0 2 / k_peak k_0 1 < 1.62 := by
  87  rw [ratio_2_1 k_0 h]
  88  exact ⟨phi_gt_onePointSixOne, phi_lt_onePointSixTwo⟩
  89
  90/-- φ² lies in the band `(2.59, 2.63)`. (Tight: `(1.61)² = 2.5921`,
  91`(1.62)² = 2.6244`.) -/
  92theorem phi_sq_band : (2.59 : ℝ) < phi ^ 2 ∧ phi ^ 2 < 2.63 := by
  93  refine ⟨?_, ?_⟩
  94  · have h := phi_gt_onePointSixOne
  95    have h_pos := phi_pos
  96    have : (1.61 : ℝ) ^ 2 ≤ phi ^ 2 := by
  97      have h_le : (1.61 : ℝ) ≤ phi := le_of_lt h
  98      apply pow_le_pow_left₀ (by norm_num : (0 : ℝ) ≤ 1.61) h_le
  99    have h_15_sq : (1.61 : ℝ) ^ 2 = 2.5921 := by norm_num
 100    linarith
 101  · have h := phi_lt_onePointSixTwo
 102    have h_pos := phi_pos
 103    have : phi ^ 2 ≤ (1.62 : ℝ) ^ 2 := by
 104      have h_le : phi ≤ (1.62 : ℝ) := le_of_lt h
 105      apply pow_le_pow_left₀ (le_of_lt h_pos) h_le
 106    have h_162_sq : (1.62 : ℝ) ^ 2 = 2.6244 := by norm_num
 107    linarith
 108
 109/-- The 3-1 ratio band: `(2.59, 2.63)`. -/
 110theorem ratio_3_1_band (k_0 : ℝ) (h : 0 < k_0) :
 111    2.59 < k_peak k_0 3 / k_peak k_0 1 ∧
 112    k_peak k_0 3 / k_peak k_0 1 < 2.63 := by
 113  rw [ratio_3_1 k_0 h]
 114  exact phi_sq_band
 115
 116/-! ## §3. Empirical observed Planck values -/
 117
 118/-- Planck 2018 first acoustic peak: `ℓ_1 = 220.0`. -/
 119def planck_l_1 : ℝ := 220.0
 120
 121/-- Planck 2018 second acoustic peak: `ℓ_2 = 540.3`. -/
 122def planck_l_2 : ℝ := 540.3
 123
 124/-- Planck 2018 third acoustic peak: `ℓ_3 = 814.6`. -/
 125def planck_l_3 : ℝ := 814.6
 126
 127/-- Observed ℓ_2 / ℓ_1 ≈ 2.456 (this is the *angular* multipole ratio,
 128not the bare wavenumber ratio; cf. discussion in the file docstring). -/
 129def planck_ratio_2_1 : ℝ := planck_l_2 / planck_l_1
 130
 131theorem planck_ratio_2_1_value : 2.45 < planck_ratio_2_1 ∧ planck_ratio_2_1 < 2.46 := by
 132  unfold planck_ratio_2_1 planck_l_2 planck_l_1
 133  refine ⟨?_, ?_⟩ <;> norm_num
 134
 135/-- The observed angular-multipole ratio is **not** the bare φ-rational
 136ratio: the projection geometry from k-space to ℓ-space introduces a
 137factor that depends on the angular diameter distance. The *bare
 138wavenumber ratio* is the φ-rational prediction, recoverable from
 139direct k-space BAO measurements. -/
 140theorem planck_ratio_not_directly_phi :
 141    planck_ratio_2_1 ≠ phi := by
 142  intro h_eq
 143  have h_planck := planck_ratio_2_1_value
 144  rw [h_eq] at h_planck
 145  have h_phi_lt := phi_lt_onePointSixTwo
 146  linarith
 147
 148/-! ## §4. Master certificate -/
 149
 150/-- **CMB ACOUSTIC PEAK RATIOS MASTER CERTIFICATE.** Five clauses.
 151
 1521. `r_21`: bare wavenumber `k_2/k_1 = φ`.
 1532. `r_32`: bare wavenumber `k_3/k_2 = φ`.
 1543. `r_31`: bare wavenumber `k_3/k_1 = φ²`.
 1554. `r_21_band`: `k_2/k_1 ∈ (1.61, 1.62)`.
 1565. `r_31_band`: `k_3/k_1 ∈ (2.59, 2.63)`.
 157
 158The Planck angular-multipole ratios differ from the bare wavenumber
 159ratios by the projection-geometry factor; the φ-rational prediction
 160is at the *wavenumber* level, recoverable from direct k-space BAO
 161measurements (BOSS, DESI). -/
 162structure CMBAcousticPeakRatiosCert where
 163  r_21 : ∀ k_0 : ℝ, 0 < k_0 → k_peak k_0 2 / k_peak k_0 1 = phi
 164  r_32 : ∀ k_0 : ℝ, 0 < k_0 → k_peak k_0 3 / k_peak k_0 2 = phi
 165  r_31 : ∀ k_0 : ℝ, 0 < k_0 → k_peak k_0 3 / k_peak k_0 1 = phi ^ 2
 166  r_21_band : ∀ k_0 : ℝ, 0 < k_0 →
 167    1.61 < k_peak k_0 2 / k_peak k_0 1 ∧ k_peak k_0 2 / k_peak k_0 1 < 1.62
 168  r_31_band : ∀ k_0 : ℝ, 0 < k_0 →
 169    2.59 < k_peak k_0 3 / k_peak k_0 1 ∧ k_peak k_0 3 / k_peak k_0 1 < 2.63
 170
 171def cmbAcousticPeakRatiosCert : CMBAcousticPeakRatiosCert where
 172  r_21 := ratio_2_1
 173  r_32 := ratio_3_2
 174  r_31 := ratio_3_1
 175  r_21_band := ratio_2_1_band
 176  r_31_band := ratio_3_1_band
 177
 178/-! ## §5. One-statement summary -/
 179
 180/-- **CMB ACOUSTIC PEAK RATIOS ONE-STATEMENT.** Three structural facts:
 181
 182(1) The bare wavenumber peak ratio `k_2/k_1 = φ`, in the band `(1.61, 1.62)`.
 183(2) The bare wavenumber peak ratio `k_3/k_1 = φ² = φ + 1`, in the band
 184    `(2.59, 2.63)`.
 185(3) The Planck angular-multipole ratio `ℓ_2/ℓ_1 ≈ 2.456` differs from
 186    the bare φ-rational prediction by the projection-geometry factor;
 187    the test of the structural prediction is at the bare wavenumber
 188    level, via direct k-space BAO measurements (BOSS, DESI). -/
 189theorem cmb_acoustic_peak_ratios_one_statement (k_0 : ℝ) (h : 0 < k_0) :
 190    k_peak k_0 2 / k_peak k_0 1 = phi ∧
 191    k_peak k_0 3 / k_peak k_0 1 = phi ^ 2 ∧
 192    planck_ratio_2_1 ≠ phi :=
 193  ⟨ratio_2_1 k_0 h, ratio_3_1 k_0 h, planck_ratio_not_directly_phi⟩
 194
 195end
 196
 197end CMBAcousticPeakRatios
 198end Cosmology
 199end IndisputableMonolith
 200