rs_sound_horizon_consistent
plain-language theorem explainer
The theorem verifies that the Recognition Science sound horizon approximation of 147 Mpc satisfies an absolute difference below 0.5 Mpc from the BOSS value 147.18 Mpc. Cosmologists comparing BAO scales to RS primordial spectrum outputs would cite this numerical match to confirm parameter consistency. The proof is a direct one-line numerical normalization that evaluates the bound from the sound horizon definition.
Claim. The Recognition Science sound horizon approximation satisfies $|r_s - 147.18| < 0.5$ in megaparsecs, where $r_s = 147$ Mpc.
background
The BAO module derives baryon acoustic oscillation scales from the Recognition Science primordial spectrum. The sound horizon approximation is defined as the constant 147 Mpc, obtained from RS values of baryon density, matter density, and spectral index. The upstream power definition supplies the spectrum shape as amplitude scaled by wavenumber to the power of (spectral index minus one). Module context includes the sound speed formula $c_s = c / √(3(1+R))$ for the baryon-photon fluid and the horizon as the integral of sound speed over the expansion history, approximated here for the matter-radiation era.
proof idea
One-line wrapper that applies norm_num to unfold the sound horizon approximation definition and confirm the numerical inequality holds.
why it matters
This result supplies a direct consistency check between the RS-predicted sound horizon and BOSS data, supporting BAO peak position derivations in the module. It closes the numerical link from the primordial spectrum power to observable scales without introducing new hypotheses. The agreement sits inside the RS framework landmarks of phi-ladder mass formulas and the eight-tick octave that fix the underlying constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.