theorem proved term proof

`rs_sound_horizon_consistent`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 114theorem rs_sound_horizon_consistent :
 115    |sound_horizon_approx - 147.18| < 0.5 := by

proof body

Term-mode proof.

 116  norm_num [sound_horizon_approx]
 117
 118/-! ## BAO Peak Positions -/
 119
 120/-- BAO peaks in the matter power spectrum occur at k_n = nπ/r_s. -/

depends on (2)

Lean names referenced from this declaration's body.

power in IndisputableMonolith.Cosmology.PrimordialSpectrum decl_use
sound_horizon_approx in IndisputableMonolith.Physics.BAO decl_use