baryon_loading
plain-language theorem explainer
Baryon loading ratio at redshift z is defined as R(z) = R0 / (1 + z), where R0 equals 3Ω_b / (4Ω_γ) at z = 0. Cosmologists modeling baryon acoustic oscillations cite the expression to track the falling baryon-to-photon density ratio during expansion. The definition is a direct algebraic assignment with no auxiliary computation or lemmas.
Claim. The baryon loading ratio at redshift $z$ is $R(z) = R_0 / (1 + z)$, where $R_0 = 3Ω_b / (4Ω_γ)$ denotes the present-day value.
background
In the Recognition Science derivation of baryon acoustic oscillations the baryon loading ratio enters the sound-speed formula for the baryon-photon fluid. The module documentation states that the ratio is given by R(z) = 3ρ_b/(4ρ_γ) from the RS baryon-to-photon ratio, and that the sound horizon r_s is obtained from the integral of c_s / H(z). Photon number density scales as (1 + z)^4 while baryon density scales as (1 + z)^3, producing the explicit 1/(1 + z) redshift dependence.
proof idea
The definition is the direct algebraic assignment R(z) := R0 / (1 + z). No lemmas are invoked; the expression is introduced as a primitive in the BAO module.
why it matters
This definition supplies the redshift dependence required by the downstream theorem baryon_loading_decreasing, which establishes that the ratio falls as redshift increases. It fills the baryon_loading_ratio slot in the BAO derivation from the RS primordial spectrum, as referenced in the module documentation to the paper RS_Baryon_Acoustic_Oscillations.tex. The construction links the RS-predicted baryon density to the observable acoustic scale of approximately 147 Mpc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.