recombination_temperature_K

formal source

  40    k_B T* ≈ E_ion / ln(η⁻¹ × factor) ≈ 0.3 eV ≈ 3500 K
  41
  42    More precisely, T* ≈ 3000 K (accounting for detailed balance). -/
  43abbrev recombination_temperature_K : ℝ := 3000  -- Kelvin
  44
  45/-- Recombination temperature is positive. -/
  46theorem recombination_temperature_positive :
  47    0 < recombination_temperature_K := by norm_num
  48
  49/-- In energy units: k_B T* ≈ 0.26 eV. -/
  50theorem recombination_energy_approx_eV :
  51    0.25 < kB_eV_per_K * recombination_temperature_K ∧
  52    kB_eV_per_K * recombination_temperature_K < 0.27 := by
  53  constructor <;> norm_num [kB_eV_per_K]
  54
  55/-! ## Recombination Redshift -/
  56
  57/-- **RS RECOMBINATION REDSHIFT**: z* ≈ 1100.
  58    From Saha equation with RS η and Ω_b h² = 0.022. -/
  59abbrev rs_recombination_redshift : ℝ := 1100
  60
  61/-- Recombination redshift is positive. -/
  62theorem recombination_redshift_positive : 0 < rs_recombination_redshift := by norm_num
  63
  64/-! ## CMB Temperature Formula -/
  65
  66/-- **CMB TEMPERATURE**: T₀ = T*/(1+z*)
  67    The photon temperature redshifts with cosmic expansion. -/
  68noncomputable def cmb_temperature (T_star z_star : ℝ) : ℝ := T_star / (1 + z_star)
  69
  70/-- CMB temperature is positive for positive T* and z* > -1. -/
  71theorem cmb_temperature_positive (T_star z_star : ℝ)
  72    (hT : 0 < T_star) (hz : -1 < z_star) :
  73    0 < cmb_temperature T_star z_star := by