ratio_2_1
plain-language theorem explainer
ratio_2_1 establishes that for any positive real base wavenumber k_0 the ratio of the second CMB acoustic peak wavenumber to the first equals the golden ratio phi. Cosmologists working inside the Recognition Science lattice would cite this result when fixing the bare k-space peak ratios before any projection to angular multipoles. The argument is a direct one-line application of the adjacent-peak theorem already proved in StructureFormationFromBIT.
Claim. For any positive real number $k_0$, the ratio of the wavenumber at the second CMB acoustic peak to the wavenumber at the first peak equals the golden ratio: $k_2 / k_1 = phi$, where $k_n = k_0 phi^n$.
background
The module deepens StructureFormationFromBIT (Plan v5 Track E1) by supplying explicit phi-rational predictions for the first three CMB acoustic peaks together with a falsifiable comparison to Planck 2018 data at the wavenumber level. The central definition is k_peak(k_0, n) := k_0 * phi^n, which places every peak on the phi-ladder starting from an arbitrary positive base wavenumber k_0. Upstream, the theorem peak_2_1_ratio already records that consecutive peaks differ by exactly phi via reduction to k_peak_adjacent_ratio; the present declaration simply re-exports that fact under the local naming convention of the cosmology module.
proof idea
The proof is a one-line wrapper that applies the peak_2_1_ratio theorem imported from StructureFormationFromBIT, which itself reduces directly to k_peak_adjacent_ratio at n = 1.
why it matters
This supplies the first structural fact inside the CMBAcousticPeakRatiosCert certificate and is invoked by both cmb_acoustic_peak_ratios_one_statement and ratio_2_1_band. It realizes the theorem portion of the module claim that the bare wavenumber ratios are phi-rational, derived without new axioms from the 8-tick lattice results of StructureFormationFromBIT. The open question it leaves is the projection-geometry factor that maps these k-ratios onto the observed angular-multipole ratios at Planck 2018.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.