sound_horizon_approx
plain-language theorem explainer
The declaration supplies the numerical value of the sound horizon scale at 147 Mpc for baryon acoustic oscillation calculations in the Recognition Science model. Cosmologists working with BAO peak positions would cite this constant when comparing RS predictions to BOSS data. The definition is a direct numerical assignment drawn from the integrated sound speed formula under RS cosmological parameters.
Claim. $r_s = 147$ Mpc, where $r_s$ is the sound horizon at recombination obtained from the RS-predicted baryon density, matter density, and spectral index via the integral of the baryon-photon sound speed.
background
The module derives BAO observables from the RS primordial spectrum. Key definitions include the sound speed $c_s = c / √(3(1+R))$ for the baryon-photon fluid with baryon loading ratio $R(z) = 3ρ_b/(4ρ_γ)$, the sound horizon integral $r_s = ∫ c_s dz/H(z)$, and the spectral index $n_s ≈ 0.967$. The local setting states that the BAO sound horizon $r_s ≈ 147$ Mpc follows directly from these RS parameters. Upstream results supply the collision-free and edge-length structures used to ground the underlying cosmological quantities.
proof idea
One-line definition that assigns the constant 147 Mpc obtained from the RS sound horizon integral under the module's cosmological parameters.
why it matters
This constant anchors the downstream theorems bao_peak_approximately_150, first_peak_wavenumber, rs_sound_horizon_consistent, and sound_horizon_positive. The parent result rs_sound_horizon_consistent states that the RS value agrees with the BOSS measurement $r_s = 147.18 ± 0.29$ Mpc to within 0.5 Mpc. It fills the numerical slot required by the BAO peak positions in the Recognition framework and connects to the RS baryon-to-photon ratio.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.