acoustic_peak
Acoustic peak positions in the CMB power spectrum scale as integer multiples of the base multipole 220. Cosmologists analyzing anisotropy spectra cite this linear relation to locate higher harmonics. The definition is a direct multiplication of the input natural number by the fixed base value from the sound horizon angular scale.
claimThe multipole of the nth acoustic peak is given by $ℓ_n = n × 220$.
background
The CMB module derives the present temperature T₀ = 2.725 K from the recombination temperature T* ≈ 3000 K at redshift z* ≈ 1100. It fixes the first acoustic peak via the angular scale of the sound horizon at last scattering. The upstream definition states: First CMB acoustic peak position: ℓ₁ ≈ π/θ_s ≈ π/r_s × D_A(z*). For standard ΛCDM: ℓ₁ ≈ 220.
proof idea
This is a one-line definition that multiplies the natural number n by first_acoustic_peak_ell.
why it matters in Recognition Science
The definition supports acoustic_peak_positions, which verifies peaks at 220, 440 and 660, and acoustic_peaks_positive, which proves positivity for positive n. It implements the cmb_anisotropy_peaks result in the module documentation, where the first peak at ℓ ≈ 220 follows from the angular diameter distance to recombination in the Recognition Science framework.
scope and limits
- Does not derive the base value 220 from the sound horizon radius or angular diameter distance.
- Does not incorporate baryon loading, Silk damping or higher-order spectrum corrections.
- Does not address polarization spectra or tensor mode contributions.
formal statement (Lean)
125noncomputable def acoustic_peak (n : ℕ) : ℝ := n * first_acoustic_peak_ell
proof body
Definition body.
126