rs_drag_redshift
plain-language theorem explainer
The RS drag redshift fixes the baryon-photon decoupling epoch at 1060. Researchers computing the BAO sound horizon integral cite this constant to set the lower integration bound. The declaration is a direct numerical assignment with no reduction steps or lemmas invoked.
Claim. The drag redshift at baryon-photon decoupling is defined by $z_{drag} = 1060$.
background
The BAO module derives the sound horizon $r_s$ from the integral of sound speed $c_s = c / √(3(1+R))$ over redshift, using RS-predicted baryon and matter densities. The drag redshift marks the Saha-equation decoupling point that terminates the tight-coupling regime. Module documentation states that $r_s ≈ 147$ Mpc follows from these RS parameters together with the spectral index $n_s ≈ 0.967$.
proof idea
The declaration is a direct constant definition that assigns the real number 1060. No lemmas from the upstream depends_on list are applied; the value is supplied explicitly to match the standard decoupling redshift.
why it matters
This constant supplies the integration cutoff for the sound-horizon formula that yields $r_s ≈ 147$ Mpc, anchoring the BAO predictions in the RS framework. It completes the parameter set referenced in RS_Baryon_Acoustic_Oscillations.tex and supports downstream calculations of baryon loading and spectral tilt. The value is consistent with the eight-tick octave and D = 3 spatial structure of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.