k_peak
plain-language theorem explainer
k_peak defines the wavenumber of the n-th CMB acoustic peak as the base scale k_0 scaled by the golden ratio to the power n. Researchers deriving acoustic peak ratios in the Recognition Science cosmology track cite it to establish the phi-ladder in the matter power spectrum. The definition is a direct algebraic scaling expression with no lemmas or proof steps beyond real arithmetic.
Claim. The wavenumber of the n-th acoustic peak is $k_n = k_0 ϕ^n$ for base wavenumber $k_0 > 0$ and natural number $n$.
background
This definition sits in the Structure Formation Power Spectrum from BIT module, which shows that the matter power spectrum inherits the phi-ladder structure of the BIT kernel so that adjacent peak wavenumbers stand in the fixed ratio phi. The module states that the first three CMB acoustic-peak wavenumber ratios are k_2/k_1 = phi and k_3/k_2 = phi, hence k_3/k_1 = phi^2, and that these ratios are independent of the base scale k_0. Upstream, the construction rests on the self-similar fixed point phi forced in the unified forcing chain and on the collision-free and edge-length properties imported from OptionAEmpiricalProgram and SimplicialLedger.
proof idea
The declaration is a definition, not a theorem. It directly encodes the phi-ladder scaling via the expression k_0 * phi ^ n using real multiplication and natural-number exponentiation.
why it matters
k_peak supplies the primitive object for the CMBAcousticPeakRatiosCert structure, which certifies the bare ratios r_21 = phi, r_32 = phi, r_31 = phi^2 together with their numerical bands (1.61,1.62) and (2.59,2.63). It fills the phi-rational ratio step in the cosmology track, connecting to the Recognition Composition Law and the eight-tick octave that forces D=3. The module lists the open hypothesis of numerical match to Planck/DESI data and gives the explicit falsifier of any first-three-peak ratio deviating more than 5 percent from the predicted phi values.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.