rs_omega_m_h2

formal source

  70def rs_omega_b_h2 : ℝ := 0.022
  71
  72/-- **RS MATTER DENSITY**: Ω_m h² ≈ 0.143 from RS dark matter + baryons. -/
  73def rs_omega_m_h2 : ℝ := 0.143
  74
  75/-- Matter density exceeds baryon density (dark matter component). -/
  76theorem matter_exceeds_baryons : rs_omega_b_h2 < rs_omega_m_h2 := by
  77  norm_num [rs_omega_b_h2, rs_omega_m_h2]
  78
  79/-- **RS SPECTRAL INDEX**: n_s ≈ 0.967 from slow-roll inflation.
  80    n_s = 1 - 2/N_e where N_e ≈ 60 e-foldings. -/
  81noncomputable def rs_spectral_index (N_e : ℝ) : ℝ := 1 - 2 / N_e
  82
  83/-- For N_e = 60 e-foldings: n_s ≈ 0.967. -/
  84theorem spectral_index_60efolds :
  85    rs_spectral_index 60 = 1 - 1/30 := by
  86  unfold rs_spectral_index
  87  norm_num
  88
  89/-- Spectral index is less than 1 (red-tilted spectrum). -/
  90theorem spectral_index_red_tilt (N_e : ℝ) (hN : 0 < N_e) :
  91    rs_spectral_index N_e < 1 := by
  92  unfold rs_spectral_index
  93  linarith [div_pos two_pos hN]
  94
  95/-! ## Sound Horizon -/
  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.