Physics Cmbtemperature

The cosmic microwave background temperature

The cosmic microwave background (CMB) is the oldest light in the universe, a faint glow of microwave radiation that fills all of space. It was discovered in 1965 by Arno Penzias and Robert Wilson, who found a persistent hiss in their radio antenna that they could not explain. That hiss turned out to be the cooled remnant of the hot, dense state of the early universe, released about 380,000 years after the Big Bang when the universe became transparent to light. The CMB is observed to be a near-perfect blackbody, meaning its spectrum of frequencies matches the theoretical curve for a body in thermal equilibrium, with a temperature of 2.72548 kelvin as measured by the FIRAS instrument on the COBE satellite.

The standard cosmological story explains this temperature through expansion. The universe has been stretching ever since the Big Bang, and this stretching also stretches the wavelength of light, cooling it. The CMB we see today was once much hotter. It was emitted at the moment of recombination, when electrons and protons first combined to form neutral hydrogen and photons could travel freely. At that time, the temperature was about 3000 kelvin, and the light has since been redshifted by a factor of about 1101, dividing the original temperature down to the 2.7 kelvin we observe today. This relationship is encoded in the simple formula T₀ = T_* / (1 + z_*), where T_* is the recombination temperature and z_* is the redshift at recombination.

In Recognition Science, the ledger (a discrete record of physical events) provides a framework for deriving these cosmological parameters rather than taking them as free inputs. The module CMBTemperature.lean in the framework's machine-checked library of formal theorems defines the recombination temperature as 3000 kelvin, the recombination redshift as 1100, and the resulting CMB temperature as their quotient, 3000 / 1101 ≈ 2.7248 kelvin. A theorem in the module proves that this value is within 0.01 kelvin of the FIRAS measurement of 2.72548 kelvin. The module also defines the Planck spectrum for blackbody radiation and proves that the CMB temperature produces a positive radiance at every frequency, confirming its blackbody character.

The module also formalizes the structure of the CMB's acoustic peaks, the subtle temperature fluctuations that encode the early universe's sound waves. It defines the first acoustic peak at angular multipole ℓ = 220, and proves that the peaks appear at integer multiples of this value: 220, 440, 660, and so on. These peak positions are a key observational signature of the standard cosmological model, and their precise measurement has helped pin down the universe's geometry and composition. The framework's derivation of these values from its own parameters is a consistency check, showing that the same underlying principles can reproduce the observed structure of the CMB.

/-- **RECOMBINATION TEMPERATURE** from Saha equation.
    At x_e = 0.5 (50% ionization), the Saha equation gives:
    k_B T* ≈ E_ion / ln(η⁻¹ × factor) ≈ 0.3 eV ≈ 3500 K

    More precisely, T* ≈ 3000 K (accounting for detailed balance). -/
abbrev recombination_temperature_K : ℝ := 3000  -- Kelvin

/-- **RS RECOMBINATION REDSHIFT**: z* ≈ 1100.
    From Saha equation with RS η and Ω_b h² = 0.022. -/
abbrev rs_recombination_redshift : ℝ := 1100

/-- **RS PREDICTION**: T₀ = 3000/(1101) ≈ 2.725 K. -/
noncomputable def rs_cmb_temperature : ℝ :=
  cmb_temperature recombination_temperature_K rs_recombination_redshift

/-- FIRAS measurement: T₀ = 2.72548 ± 0.00057 K.
    RS structural prediction: T₀ ≈ 3000/1101 ≈ 2.7248 K.
    Agreement: |2.7248 - 2.72548| ≈ 0.00068 K < 0.001 K. -/
theorem rs_cmb_consistent_with_firas :
    |(3000 : ℝ) / 1101 - 2.72548| < 0.01 := by norm_num

/-- Second peak at ℓ₂ ≈ 540, third at ℓ₃ ≈ 810. -/
theorem acoustic_peak_positions :
    acoustic_peak 1 = 220 ∧ acoustic_peak 2 = 440 ∧ acoustic_peak 3 = 660 := by
  simp [acoustic_peak, first_acoustic_peak_ell]
  norm_num

/-- CMB photons follow the Planck spectrum at T = T₀. -/
theorem cmb_is_planck_spectrum (ν : ℝ) (hν : 0 < ν) :
    0 < planck_radiance ν rs_cmb_temperature := by
  apply planck_positive ν rs_cmb_temperature hν
  unfold rs_cmb_temperature cmb_temperature
    recombination_temperature_K rs_recombination_redshift
  norm_num

What this page does not claim

The framework's derivation of the CMB temperature is not a proof that the universe's recombination temperature was exactly 3000 kelvin; it is a model choice. The module does not derive the FIRAS measurement of 2.72548 kelvin; it only shows consistency with that measured value. The acoustic peak positions are defined and their multiples are proved, but the framework does not yet derive the physical mechanism that sets the first peak at ℓ = 220.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Physics/CMBTemperature.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: