bao_correlation_peak
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the sound horizon from redshift integrals.
- Does not incorporate damping or nonlinear corrections to the peak.
- Does not convert between comoving and observed scales.
Lean usage
theorem bao_peak_approximately_150 : |bao_correlation_peak sound_horizon_approx - 294| < 1 := by norm_num [bao_correlation_peak, sound_horizon_approx]formal statement (Lean)
139noncomputable def bao_correlation_peak (r_s : ℝ) : ℝ := 2 * r_s
proof body
Definition body.
140