sound_speed
plain-language theorem explainer
The sound speed in the baryon-photon fluid is defined as 1 over the square root of 3 times (1 plus the baryon loading ratio R). Cosmologists deriving the BAO sound horizon from RS-predicted densities would cite this when evaluating the integral for r_s. The definition is a direct algebraic expression with no lemmas or tactics applied.
Claim. The sound speed of the baryon-photon fluid is given by $c_s(R) = 1 / √[3(1 + R)]$, where $R$ is the baryon loading ratio $R = 3ρ_b/(4ρ_γ)$.
background
The BAO module derives the sound horizon r_s ≈ 147 Mpc from RS-predicted parameters including baryon density, matter density, and spectral index n_s ≈ 0.967. The sound speed enters the integral r_s = ∫ c_s dz/H(z) and follows the standard expression for a relativistic fluid with baryon loading. The module documentation lists this as the key formula c_s = c/√[3(1+R)] in units where c = 1.
proof idea
This is a one-line definition that directly encodes the standard sound speed formula using Real.sqrt from Mathlib. No upstream lemmas are invoked and no tactics are applied beyond the algebraic expression itself.
why it matters
This definition is used directly by the sibling theorems sound_speed_positive, sound_speed_decreasing, and sound_speed_radiation_limit. It supplies the core expression listed under Key Results in the module documentation for computing the BAO sound horizon from RS parameters. It sits inside the broader Recognition Science derivation of cosmological scales via the phi-ladder and eight-tick octave, though the formula itself is the conventional one.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.