bao_correlation_peak
plain-language theorem explainer
BAO correlation peak is defined as twice the sound horizon r_s. Galaxy survey analysts would cite this when matching RS-derived sound horizons to the observed baryon acoustic scale. The definition performs direct scaling of the input parameter with no further computation.
Claim. The BAO correlation peak position is given by $r = 2 r_s$, where $r_s$ is the sound horizon scale from the RS baryon-photon fluid.
background
The BAO module computes the sound horizon via the integral of sound speed $c_s = 1/√(3(1+R))$ over redshift, with R the baryon loading ratio drawn from RS baryon-to-photon parameters. Module results also fix the spectral index near 0.967 and baryon density constraints. This definition converts the sound horizon into the real-space peak of the two-point correlation function at the scale stated in the module documentation.
proof idea
The declaration is a one-line definition that directly multiplies the input sound horizon by two.
why it matters
It supplies the peak location used by the downstream theorem bao_peak_approximately_150 to verify the RS sound horizon approximation against the 294 Mpc scale. This connects Recognition Science predictions for the primordial spectrum to the BAO feature observed in large-scale structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.