ratio_2_1_band
plain-language theorem explainer
The theorem establishes the strict numerical band (1.61, 1.62) for the ratio of the second to first CMB acoustic peak wavenumbers. Modelers of cosmic microwave background structure in the Recognition Science approach cite this for its direct tie to the golden ratio bounds. The proof applies a rewrite to the exact phi equality followed by the bounding lemmas on phi.
Claim. For any $k_0 > 0$, with peak wavenumbers $k_n = k_0 phi^n$, the ratio satisfies $1.61 < k_2 / k_1 < 1.62$.
background
The module derives CMB acoustic peak ratios from the 8-tick lattice in StructureFormationFromBIT. There the wavenumber at the n-th peak is defined as k_peak k_0 n = k_0 * phi^n. The exact ratio k_2 / k_1 = phi follows from the adjacent ratio result in the same module. The band uses the lemmas establishing 1.61 < phi and phi < 1.62 from Constants.
proof idea
The proof rewrites the target ratio via the theorem that equates it to phi. It then supplies the pair of inequalities from the phi bounding lemmas to close the conjunction.
why it matters
It populates the band field in the certificate cmbAcousticPeakRatiosCert that aggregates all three peak ratios. The result fills the numerical prediction step in the module's theorem on phi-rational structure, connecting to the self-similar fixed point phi and the eight-tick period in the foundational forcing chain. The remaining open question is the geometry-adjusted comparison to observed angular multipoles.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.