acoustic_peak
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.