sound_speed_decreasing
plain-language theorem explainer
Sound speed in the baryon-photon fluid decreases monotonically with rising baryon loading ratio R. BAO modelers cite the result to bound the sound horizon integral when baryon density increases. The proof unfolds the explicit formula then applies positivity and square-root comparison lemmas with linarith.
Claim. For real numbers $R_1,R_2$ with $-1<R_1<R_2$, the sound speed satisfies $1/√[3(1+R_2)] < 1/√[3(1+R_1)]$.
background
The BAO module derives the sound horizon from the RS primordial spectrum using the baryon loading ratio R = 3ρ_b/(4ρ_γ). Sound speed is defined explicitly as 1/√[3(1+R)] in units where c=1. The upstream sound_speed declaration supplies this formula while PrimitiveDistinction.from encodes the seven axioms that underwrite the structural conditions for the fluid description.
proof idea
Unfold sound_speed to expose the two explicit expressions. Apply div_lt_div_of_pos_left with one_pos. Establish positivity of the square-root denominators via sqrt_pos_of_pos and linarith. Finish with sqrt_lt_sqrt on the arguments inside the roots, again using linarith.
why it matters
The monotonicity guarantees that higher baryon density lowers the sound speed and therefore shrinks the sound horizon integral, supporting the RS prediction Ω_b h² ≈ 0.022 and the spectral index n_s ≈ 0.967. It fills the step between the sound_speed definition and the sound_horizon_integral in the RS_Baryon_Acoustic_Oscillations derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.