sound_speed_positive

formal source

  41noncomputable def sound_speed (R : ℝ) : ℝ := 1 / Real.sqrt (3 * (1 + R))
  42
  43/-- Sound speed is positive for R ≥ 0. -/
  44theorem sound_speed_positive (R : ℝ) (hR : -1 < R) :
  45    0 < sound_speed R := by
  46  unfold sound_speed
  47  apply div_pos one_pos
  48  apply Real.sqrt_pos_of_pos
  49  linarith
  50
  51/-- In the limit R → 0 (radiation dominated): c_s → c/√3. -/
  52theorem sound_speed_radiation_limit :
  53    sound_speed 0 = 1 / Real.sqrt 3 := by
  54  unfold sound_speed
  55  norm_num
  56
  57/-- Sound speed decreases with R (more baryons → slower sound). -/
  58theorem sound_speed_decreasing (R₁ R₂ : ℝ) (hR₁ : -1 < R₁) (hR₂ : -1 < R₂) (h : R₁ < R₂) :
  59    sound_speed R₂ < sound_speed R₁ := by
  60  unfold sound_speed
  61  apply div_lt_div_of_pos_left one_pos
  62  · apply Real.sqrt_pos_of_pos; linarith
  63  · apply Real.sqrt_lt_sqrt
  64    · linarith
  65    · linarith
  66
  67/-! ## RS Cosmological Parameters -/
  68
  69/-- **RS BARYON DENSITY**: Ω_b h² ≈ 0.022 from RS baryogenesis. -/
  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