acoustic_peaks_positive
plain-language theorem explainer
The theorem shows that the n-th CMB acoustic peak multipole remains strictly positive for every positive integer n. Researchers modeling the CMB power spectrum or acoustic oscillations would cite it to guarantee that peak locations stay in the observable multipole range. The proof is a one-line wrapper that unfolds acoustic_peak n to n times the constant 220 and invokes the positivity tactic.
Claim. For every positive integer $n$, the n-th acoustic peak position satisfies $0 < n times 220$.
background
The CMB Temperature module derives T₀ = 2.725 K from the recombination epoch at redshift z* ≈ 1100 and recombination temperature T* ≈ 3000 K. Within this setting the first acoustic peak is fixed at first_acoustic_peak_ell := 220, matching the standard value ℓ₁ ≈ π/θ_s from the sound horizon at recombination. Acoustic peak positions are then defined by scaling: acoustic_peak n := n * first_acoustic_peak_ell, so that ℓ_n ≈ n × 220.
proof idea
The term-mode proof unfolds acoustic_peak and first_acoustic_peak_ell, reducing the goal to 0 < n * 220, then applies the positivity tactic which discharges the inequality for positive n and positive constant 220.
why it matters
The result supplies a basic positivity guarantee for the acoustic peak locations used in the CMB anisotropy analysis of RS_CMB_Temperature.tex. It rests on the scaling relation ℓ_n ≈ n × 220 stated in the module and on the upstream definition of first_acoustic_peak_ell. No downstream theorems currently depend on it, but it closes a foundational check required before any further spectral modeling in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.