CMBAcousticPeakRatiosCert
plain-language theorem explainer
The CMBAcousticPeakRatiosCert structure certifies that CMB acoustic-peak wavenumbers form a geometric sequence with common ratio phi: k2/k1 equals phi, k3/k2 equals phi, and k3/k1 equals phi squared, together with the numerical bands (1.61,1.62) and (2.59,2.63). Cosmologists testing Recognition Science against BAO surveys would cite the certificate for its direct k-space prediction. It is realized as a structure definition that bundles the five ratio properties obtained by cancellation from the upstream k_peak formula.
Claim. Let $k_n = k_0 phi^n$ for positive real $k_0$ and natural $n$. The certificate asserts that $k_2/k_1 = phi$, $k_3/k_2 = phi$, $k_3/k_1 = phi^2$, together with the bounds $1.61 < k_2/k_1 < 1.62$ and $2.59 < k_3/k_1 < 2.63$.
background
In Recognition Science the wavenumber at the n-th acoustic peak is given by the upstream definition k_peak(k_0, n) := k_0 * phi^n. This module sits inside the eight-tick lattice setting of StructureFormationFromBIT and isolates the bare wavenumber ratios that follow immediately from that formula. The module document states that the phi-rational k-space ratios are theorems while the comparison to observed angular multipoles remains a hypothesis pending full projection geometry.
proof idea
The declaration is a structure definition. Its first three fields are obtained by algebraic cancellation: k_peak(k_0,2)/k_peak(k_0,1) simplifies directly to phi, and likewise for the other two ratios. The two band fields are instantiated from the numerical inequalities on phi supplied by the Constants module.
why it matters
This certificate supplies the precise phi-rational statement required by StructureFormationFromBIT and is instantiated by the downstream cmbAcousticPeakRatiosCert. It realizes the T7 eight-tick octave prediction for the acoustic scale at the wavenumber level and isolates the claim recoverable from direct k-space BAO measurements. The open question it leaves is whether the projected ell ratios can be reconciled once the full Boltzmann transfer function is computed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.