peak_2_1_ratio
plain-language theorem explainer
The theorem establishes that the ratio of the second to first characteristic wavenumber equals the golden ratio φ for any positive base scale k_0. Cosmologists deriving the matter power spectrum from the BIT kernel cite this when obtaining scale-invariant acoustic peak ratios. The proof is a direct one-line application of the adjacent-ratio lemma at the first step.
Claim. For any real number $k_0 > 0$, let $k_n = k_0 φ^n$ be the wavenumber of the n-th acoustic peak. Then $k_2 / k_1 = φ$.
background
The Structure Formation from BIT module shows that the matter power spectrum inherits the φ-ladder of the BIT kernel, so adjacent peak wavenumbers stand in the fixed ratio φ. The definition k_peak sets the n-th peak wavenumber to k_n = k_0 · φ^n. The upstream theorem k_peak_adjacent_ratio proves that k_{n+1}/k_n = φ holds exactly whenever k_0 is positive, by direct expansion of the powers and cancellation of the common factors.
proof idea
The proof is a one-line wrapper that applies the adjacent peak ratio theorem k_peak_adjacent_ratio at n=1 with the supplied positivity hypothesis on k_0.
why it matters
This supplies the second-to-first ratio used by the downstream theorem ratio_2_1 in the CMBAcousticPeakRatios module. It completes the φ-rational ratio structure step in the module's proof of parameter-free peak ratios, as stated in the module documentation. The module falsifier is any observed CMB peak ratio more than 5% off the predicted φ values.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.