sound_speed_positive
plain-language theorem explainer
The theorem shows that the baryon-photon sound speed stays positive for all baryon loading parameters R greater than -1. Researchers computing the BAO sound horizon integral would invoke it to keep the propagation speed real and the horizon length well-defined. The argument unfolds the explicit formula, applies positivity of division and square root, then closes with linear arithmetic on the hypothesis.
Claim. For every real number $R$ satisfying $R > -1$, the sound speed $c_s(R) = 1/√(3(1+R))$ obeys $c_s(R) > 0$.
background
In the BAO module the sound speed of the baryon-photon fluid is given by the explicit formula $c_s = 1/√(3(1+R))$ (units $c=1$), where $R = 3ρ_b/(4ρ_γ)$ is the baryon loading ratio. The module derives the sound horizon $r_s ≈ 147$ Mpc by integrating this speed over redshift, using RS-predicted values for baryon density and spectral index. The upstream definition supplies the closed-form expression whose positivity must be verified before the integral is formed.
proof idea
The term proof first unfolds the definition of sound_speed. It then applies the lemma that a positive numerator divided by a positive denominator remains positive, invokes the fact that the square root is positive when its argument is positive, and finishes with linarith to confirm that $3(1+R) > 0$ follows immediately from the hypothesis $R > -1$.
why it matters
The result guarantees a physically admissible domain for the sound-speed formula that enters the BAO sound-horizon calculation inside the RS framework. It supports the downstream integral for $r_s$ and the extraction of the spectral index $n_s ≈ 0.967$ from the same primordial spectrum. The claim aligns with the T5 J-uniqueness step that fixes the underlying scale factor and with the module's derivation of RS baryon-to-photon ratios.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.