Physics Bao Rs Sound Horizon Consistent

The sound horizon check

The sound horizon is the greatest distance a pressure wave could have traveled through the hot, dense plasma of the early universe before the plasma cooled into neutral gas. That distance left a permanent imprint: a preferred separation between galaxies, visible in surveys as a slight excess of pairs at a particular scale. Astronomers call this excess the baryon acoustic oscillation (BAO) peak, and its measured scale is about 147 megaparsecs.

The Recognition Science (RS) framework starts from a different premise: reality keeps a ledger, a discrete record of recognition events, and the cost of each recognition is forced by a proved theorem. From that starting point the framework derives a chain of results, including the cosmological parameters that feed the sound horizon calculation. The relevant definitions are concrete: a baryon density parameter of 0.022, a matter density parameter of 0.143, and a spectral index of about 0.967, all in the standard units cosmologists use.

Given those parameters, the framework computes the sound horizon by integrating the sound speed over the expansion history. The sound speed follows the standard formula c_s = c/√(3(1+R)), where R is the baryon-to-photon ratio. The integral yields a value of 147 Mpc. The theorem rs_sound_horizon_consistent proves that this value is within 0.5 Mpc of 147.18 Mpc, the measured value. The proof is a direct numerical check, not a derivation of the measurement itself.

The framework's library of formal theorems also proves supporting facts: the sound speed is positive and decreases as the baryon loading increases, the baryon loading itself decreases with redshift, and the BAO peaks are evenly spaced in wavenumber. The first peak falls at π divided by the sound horizon, and the correlation peak sits at twice the sound horizon. These are all consequences of the same definitions.

What the theorem does not claim is as important as what it proves. It does not derive the measured value from first principles; it takes the framework's predicted parameters as given and checks that the resulting sound horizon is consistent with observation. The agreement is a sanity check on the framework's parameters, not a proof that those parameters are correct. The theorem also does not claim that the framework's derivation of the parameters is complete or that the measurement itself is exact.

/-- **RS PREDICTION**: Sound horizon agrees with BOSS measurement.
    BOSS: r_s = 147.18 ± 0.29 Mpc.
    Agreement: |r_s^RS - r_s^BOSS| < 0.5 Mpc. -/
theorem rs_sound_horizon_consistent :
    |sound_horizon_approx - 147.18| < 0.5 := by
  norm_num [sound_horizon_approx]

/-- **SOUND SPEED**: c_s = c/√(3(1+R))
    In units c=1: c_s = 1/√(3(1+R)). -/
noncomputable def sound_speed (R : ℝ) : ℝ := 1 / Real.sqrt (3 * (1 + R))

/-- **RS BARYON DENSITY**: Ω_b h² ≈ 0.022 from RS baryogenesis. -/
def rs_omega_b_h2 : ℝ := 0.022

/-- **RS MATTER DENSITY**: Ω_m h² ≈ 0.143 from RS dark matter + baryons. -/
def rs_omega_m_h2 : ℝ := 0.143

/-- The correlation function peak in real space: r = 2π/k₁ ≈ 150 h⁻¹ Mpc. -/
noncomputable def bao_correlation_peak (r_s : ℝ) : ℝ := 2 * r_s

What this page does not claim

The theorem does not derive the sound horizon value from first principles; it checks consistency of given parameters. The framework's cosmological parameters are not proved correct by this agreement; they are definitions. The measured value of 147.18 Mpc is not exact; it carries its own observational uncertainty.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Physics/BAO.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: