acoustic_peak_positions
plain-language theorem explainer
Recognition Science fixes the first three CMB acoustic peaks at multipoles 220, 440 and 660. Modelers comparing RS predictions to Planck spectra would cite this when testing exact harmonic scaling against observed anisotropy. The proof is a direct simplification that unfolds the acoustic peak definition as an integer multiple of the base value 220 and evaluates the arithmetic.
Claim. The acoustic peak positions satisfy $ℓ_1 = 220$, $ℓ_2 = 440$, $ℓ_3 = 660$.
background
The CMB Temperature module derives the present-day blackbody temperature from recombination at redshift z* ≈ 1100 and temperature T* ≈ 3000 K, with the acoustic peaks supplying the angular scale. The acoustic peak function is defined as n times the first peak multipole, which is set to 220. This implements the module's statement that peak positions scale as n × 220 and aligns with the listed result cmb_anisotropy_peaks: First peak at ℓ ≈ 220.
proof idea
The term proof applies simp to unfold the definitions of acoustic_peak and first_acoustic_peak_ell, then invokes norm_num to confirm the three numerical identities.
why it matters
The declaration populates the cmb_anisotropy_peaks entry in the CMB Temperature module and supplies the angular information needed for the temperature scaling T0 = T*/(1 + z*). It connects the Recognition Science phi-ladder scaling to an observable CMB feature while leaving open the integration with full power-spectrum calculations or higher peaks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.