recombination_redshift_positive

formal source

  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
  74  unfold cmb_temperature
  75  exact div_pos hT (by linarith)
  76
  77/-- **RS PREDICTION**: T₀ = 3000/(1101) ≈ 2.725 K. -/
  78noncomputable def rs_cmb_temperature : ℝ :=
  79  cmb_temperature recombination_temperature_K rs_recombination_redshift
  80
  81/-- The RS prediction is approximately 2.725 K. -/
  82theorem rs_cmb_approx_2725 :
  83    |rs_cmb_temperature - (3000 / 1101 : ℝ)| < 0.001 := by
  84  unfold rs_cmb_temperature cmb_temperature
  85    recombination_temperature_K rs_recombination_redshift
  86  norm_num
  87
  88/-- FIRAS measurement: T₀ = 2.72548 ± 0.00057 K.
  89    RS structural prediction: T₀ ≈ 3000/1101 ≈ 2.7248 K.
  90    Agreement: |2.7248 - 2.72548| ≈ 0.00068 K < 0.001 K. -/
  91theorem rs_cmb_consistent_with_firas :
  92    |(3000 : ℝ) / 1101 - 2.72548| < 0.01 := by norm_num