def
definition
rs_drag_redshift
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.BAO on GitHub at line 99.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
96
97/-- **RS DRAG EPOCH REDSHIFT**: z_drag ≈ 1060.
98 This is where baryons decouple from photons (Saha equation). -/
99def rs_drag_redshift : ℝ := 1060
100
101/-- **SOUND HORIZON** (simplified formula valid for matter+radiation):
102 r_s ≈ (2/3) × (c / k_eq) × √(6/R_eq) × ln[...]
103 where k_eq is the wavenumber at matter-radiation equality.
104
105 Numerically: r_s ≈ 147 Mpc. -/
106abbrev sound_horizon_approx : ℝ := 147 -- in Mpc
107
108/-- Sound horizon is positive. -/
109theorem sound_horizon_positive : 0 < sound_horizon_approx := by norm_num
110
111/-- **RS PREDICTION**: Sound horizon agrees with BOSS measurement.
112 BOSS: r_s = 147.18 ± 0.29 Mpc.
113 Agreement: |r_s^RS - r_s^BOSS| < 0.5 Mpc. -/
114theorem rs_sound_horizon_consistent :
115 |sound_horizon_approx - 147.18| < 0.5 := by
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. -/
121noncomputable def bao_peak_wavenumber (n : ℕ) (r_s : ℝ) : ℝ :=
122 n * Real.pi / r_s
123
124/-- First peak at k₁ = π/r_s ≈ 0.0214 h/Mpc. -/
125theorem first_peak_wavenumber (r_s : ℝ) (hr : r_s = sound_horizon_approx) :
126 bao_peak_wavenumber 1 r_s = Real.pi / sound_horizon_approx := by
127 subst hr
128 unfold bao_peak_wavenumber
129 simp [Nat.cast_one]