first_peak_wavenumber
plain-language theorem explainer
The declaration shows that the wavenumber of the first baryon acoustic oscillation peak equals π over the approximate sound horizon when the supplied radius matches the standard value of 147 Mpc. Researchers modeling the matter power spectrum in cosmology would reference this to fix the location of the fundamental BAO mode. The proof is a direct algebraic reduction obtained by substituting the hypothesis into the peak definition and simplifying.
Claim. If $r_s$ equals the approximate sound horizon value of 147 Mpc, then the first baryon acoustic oscillation peak wavenumber satisfies $k_1 = 1 · π / r_s$.
background
In the Recognition Science treatment of baryon acoustic oscillations the sound horizon is given by the constant approximation 147 Mpc. The peak locations are defined by the function that places BAO peaks at $k_n = n π / r_s$ for positive integers n. The module derives these features from the RS-predicted primordial spectrum together with the baryon-photon fluid parameters (sound speed $c_s = c / √(3(1+R))$, baryon loading ratio R, and spectral index $n_s ≈ 0.967$).
proof idea
The proof substitutes the equality hypothesis into the goal, unfolds the definition of the peak wavenumber function, and applies simplification to the cast of the natural number one.
why it matters
This result pins the position of the primary BAO peak in the matter power spectrum at approximately 0.0214 h/Mpc, consistent with the RS framework's derivation of the sound horizon from baryon-photon fluid dynamics. It supports the broader analysis of large-scale structure oscillations predicted by the Recognition Science primordial spectrum as described in the module documentation for RS_Baryon_Acoustic_Oscillations.tex.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.