cmb_is_planck_spectrum
plain-language theorem explainer
CMB photons follow the Planck spectral radiance at the Recognition Science temperature T₀ ≈ 2.725 K. Cosmologists confirming the thermal character of the cosmic microwave background would cite the result when verifying positivity of the radiance at all frequencies. The proof is a direct application of the general planck_positive lemma to the RS temperature, followed by unfolding the temperature definition and numerical normalization.
Claim. For every real frequency ν > 0, the Planck radiance B_ν(T₀) > 0, where T₀ is the cosmic microwave background temperature obtained by dividing the recombination temperature 3000 K by one plus the recombination redshift.
background
The module derives the present-day CMB temperature from the recombination epoch. Recombination temperature is fixed at 3000 K by the Saha equation at 50 percent ionization using the RS baryon-to-photon ratio. The CMB temperature is then defined as recombination temperature divided by one plus recombination redshift, yielding the RS prediction of approximately 2.725 K. Planck radiance is the spectral function 2ν³ / (exp(ν/T) - 1) in natural units, which is the Gibbs distribution for photons under the eight-tick periodicity.
proof idea
The proof applies the planck_positive theorem to the supplied frequency and the RS CMB temperature, using the positivity hypothesis on ν. It then unfolds rs_cmb_temperature, cmb_temperature, recombination_temperature_K and rs_recombination_redshift. Norm_num finishes the inequality after the definitions reduce to explicit numbers.
why it matters
The result places the CMB inside the Recognition Science framework by confirming that its radiance is positive and matches the Planck form required by the Gibbs distribution for bosons. It anchors the module claim that T₀ = 2.725 K follows from recombination at z* ≈ 1100, consistent with the eight-tick octave for photons. The declaration supports the subsequent section on acoustic peaks at ℓ ≈ 220.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.