baryon_loading_decreasing
plain-language theorem explainer
Baryon loading R(z) = R0/(1+z) is strictly decreasing in redshift z for fixed R0 > 0 and z > -1. Cosmologists deriving the BAO sound horizon from the RS primordial spectrum cite this monotonicity to control the redshift dependence of the baryon-photon fluid. The proof is a one-line term application of div_lt_div_of_pos_left after unfolding the definition of baryon_loading.
Claim. Let $R_0 > 0$. For redshifts $z_1, z_2 > -1$ with $z_1 < z_2$, the baryon loading ratio satisfies $R(z_2) < R(z_1)$, where $R(z) := R_0/(1+z)$.
background
The BAO module derives the sound horizon from RS-predicted cosmological parameters. The upstream definition states that the baryon loading ratio at redshift z is R(z) = 3ρ_b/(4ρ_γ) = R0/(1+z), where R0 = 3Ω_b/(4Ω_γ) at z=0. This ratio enters the sound speed formula c_s = 1/√(3(1+R)) for the baryon-photon fluid. The module setting assumes the RS baryon-to-photon ratio and connects to the sound horizon integral r_s = ∫ c_s dz/H(z).
proof idea
The term proof first unfolds baryon_loading to replace the left-hand side with R0/(1+z2) and the right-hand side with R0/(1+z1). It then applies div_lt_div_of_pos_left, using the three positivity hypotheses (R0 > 0, 1+z1 > 0, 1+z2 > 0) together with the ordering z1 < z2 to obtain the strict inequality.
why it matters
The result establishes the redshift dependence required for the sound speed to decrease as photons dominate at high z, feeding the sound horizon calculation in the RS BAO framework. It directly supports the module's key results on c_s and r_s ≈ 147 Mpc. The declaration sits inside the chain from RS baryon density to observable BAO scales, consistent with the eight-tick octave and phi-ladder mass formulas that fix Ω_b and Ω_γ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.