k_peak_adjacent_ratio
plain-language theorem explainer
The theorem shows that adjacent wavenumbers in the CMB acoustic peak ladder satisfy k_{n+1}/k_n = φ exactly, for any positive base scale k_0. Modelers of structure formation from the BIT kernel cite it to obtain parameter-free ratios that match the first three observed peaks. The proof reduces the claim by unfolding the geometric definition of the peak sequence, canceling the common k_0 factor, and simplifying the resulting power ratio with field arithmetic.
Claim. Let $k_n = k_0 φ^n$ for real $k_0 > 0$ and natural number $n$. Then $k_{n+1}/k_n = φ$.
background
The module derives the matter power spectrum from the BIT kernel, which imposes a φ-ladder on characteristic wavenumbers. The upstream definition states that the wavenumber at the n-th CMB acoustic peak is k_n = k_0 · φ^n. All peaks remain positive when k_0 is positive. The local setting is the φ-rational ratio structure of the first three acoustic peaks, with ratios independent of the base scale k_0.
proof idea
The term proof unfolds the peak definition to expose the ratio (k_0 φ^{n+1}) / (k_0 φ^n). It asserts φ ≠ 0 and k_0 ≠ 0 from the positivity hypotheses, rewrites the successor exponent, and cancels via field_simp to obtain φ.
why it matters
This result supplies the adjacent-ratio axiom for the master certificate structureFormationFromBITCert and for the explicit statements of the second-to-first and third-to-second ratios. It realizes the self-similar fixed point φ in the cosmological power spectrum, consistent with the forcing chain that selects φ as the unique solution to the Recognition Composition Law. The module falsifier is any observed peak ratio deviating more than 5% from φ or φ².
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.