cmb_temperature_positive

formal source

  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
  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. -/