ratio_3_1
plain-language theorem explainer
The wavenumber ratio between the third and first CMB acoustic peaks equals exactly φ². Cosmologists building Recognition Science models cite this for the exact φ-rational k-space structure of acoustic peaks. The proof is a one-line wrapper that invokes the peak_3_1_ratio lemma from StructureFormationFromBIT.
Claim. For positive real $k_0$, let $k_n = k_0 φ^n$ be the wavenumber of the n-th acoustic peak. Then $k_3 / k_1 = φ^2$.
background
The module derives CMB acoustic peak ratios from the 8-tick lattice of StructureFormationFromBIT (Track E1). The upstream definition k_peak(k_0, n) := k_0 * φ^n supplies the peak locations. The sibling theorem peak_3_1_ratio states the same equality and proves it by unfolding k_peak, noting φ ≠ 0 and k_0 ≠ 0, then applying field_simp. The local setting is the bare-wavenumber level before any projection to angular multipoles ℓ; the module distinguishes this structural theorem from the separate hypothesis on observed ℓ ratios.
proof idea
The proof is a one-line wrapper that applies peak_3_1_ratio k_0 h.
why it matters
This supplies the 3-1 ratio to cmbAcousticPeakRatiosCert and to the one-statement theorem cmb_acoustic_peak_ratios_one_statement, completing the set of φ-rational k-space ratios (k2/k1 = φ, k3/k1 = φ²). It fills the structural claim in the module doc-comment for Track E1. The module records that observed Planck ℓ ratios differ from these k-ratios by projection geometry, leaving the full Boltzmann transfer match as an open hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.