def
definition
cmb_temperature
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.CMBTemperature on GitHub at line 68.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
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 : ℝ) : ℝ :=