rs_cmb_temperature

formal source

  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
  93
  94/-! ## Planck Spectrum -/
  95
  96/-- **PLANCK SPECTRAL RADIANCE**: B_ν(T) = (2hν³/c²) × 1/(e^{hν/k_BT} - 1)
  97    This is the RS Gibbs distribution for photons (bosons, 8-tick full period). -/
  98noncomputable def planck_radiance (ν T : ℝ) : ℝ :=
  99  2 * ν ^ 3 / (Real.exp (ν / T) - 1)   -- in natural units hbar=c=kB=1
 100
 101/-- Planck spectrum is positive for T > 0, ν > 0. -/
 102theorem planck_positive (ν T : ℝ) (hν : 0 < ν) (hT : 0 < T) :
 103    0 < planck_radiance ν T := by
 104  unfold planck_radiance
 105  apply div_pos
 106  · positivity
 107  · have harg : 0 < ν / T := div_pos hν hT
 108    linarith [Real.one_lt_exp_iff.mpr harg]