cmb_acoustic_peak_ratios_one_statement
plain-language theorem explainer
The declaration states that the bare wavenumber ratios of the second and third CMB acoustic peaks to the first are exactly the golden ratio φ and φ², while the observed Planck angular multipole ratio ℓ₂/ℓ₁ is not equal to φ. Cosmologists modeling structure formation on the Recognition Science lattice would cite it for its exact φ-rational predictions at the k-space level, distinct from projected angular data. The proof is a one-line term that packages the ratio theorems ratio_2_1 and ratio_3_1 together with the non-equality result planck_ratio_
Claim. Let $k_n = k_0 · φ^n$ be the wavenumber of the n-th acoustic peak for positive base wavenumber $k_0$. Then $k_2/k_1 = φ$, $k_3/k_1 = φ^2$, and the Planck angular ratio $ℓ_2/ℓ_1 ≠ φ$.
background
The module derives CMB acoustic peak ratios from the 8-tick lattice in StructureFormationFromBIT. The definition k_peak(k_0, n) := k_0 * phi^n gives the wavenumber at the n-th peak. Upstream theorems ratio_2_1 and ratio_3_1 establish the exact equalities k_peak(k_0,2)/k_peak(k_0,1) = phi and k_peak(k_0,3)/k_peak(k_0,1) = phi^2. The definition planck_ratio_2_1 := planck_l_2 / planck_l_1 records the observed angular multipole ratio ≈2.456. The theorem planck_ratio_not_directly_phi shows this observed ratio differs from phi because projection from k-space to ℓ-space introduces a geometry factor depending on angular diameter distance.
proof idea
The proof is a one-line term wrapper that applies ratio_2_1 k_0 h, ratio_3_1 k_0 h, and planck_ratio_not_directly_phi to assemble the conjunction.
why it matters
This one-statement theorem collects the φ-rational k-space predictions from the 8-tick octave (T7) and phi fixed point (T6) into a single falsifiable claim for cosmology. It feeds the broader StructureFormationFromBIT track by separating bare wavenumber ratios (testable via BAO) from projected ℓ ratios. The module docstring notes that full projection matching to Planck 2018 remains a hypothesis pending transfer-function work; the present result closes the structural part of the E1 track.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.