bao_peak_approximately_150
plain-language theorem explainer
The declaration verifies that the BAO correlation peak, defined as twice the sound horizon, lies within 1 Mpc of 294 when the horizon is set to the RS numerical approximation of 147 Mpc. Cosmologists using Recognition Science parameters for the primordial spectrum would cite this to fix the acoustic scale near the observed 150 h^{-1} Mpc. The proof reduces directly to arithmetic by unfolding the two explicit definitions.
Claim. $|2 r_s - 294| < 1$ where the approximate sound horizon $r_s$ equals 147 Mpc.
background
The BAO module derives acoustic features from the RS primordial spectrum, with the sound horizon given by the simplified numerical value 147 Mpc valid for matter plus radiation. The correlation peak position is defined as twice this horizon value, producing the scale 294 Mpc that matches the expected real-space peak at roughly 150 h^{-1} Mpc. The module documentation states that this horizon follows from the integral of sound speed over the expansion history, with baryon loading and spectral index supplied by upstream RS results.
proof idea
The proof is a one-line wrapper that applies norm_num to the definitions of the correlation peak as twice its argument and the horizon approximation as the constant 147, reducing the absolute-value inequality to the trivial 0 < 1.
why it matters
This result supplies a concrete numerical anchor for the BAO peak inside the Physics.BAO module, confirming the RS-derived sound horizon scale listed among the module's key results. It supports the broader Recognition Science derivation of cosmological parameters from the phi-ladder and eight-tick octave without introducing new hypotheses. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.