planck_radiance
plain-language theorem explainer
The planck_radiance supplies the blackbody spectral radiance B_ν(T) for photons in RS units with ħ = c = k_B = 1. CMB modelers cite it to confirm the spectrum at the derived temperature T₀ = 2.725 K. The definition is a one-line transcription of the standard Planck formula specialized to natural units.
Claim. The spectral radiance is defined by $B_ν(T) := 2ν³ / (e^{ν/T} - 1)$ in units where ħ = c = k_B = 1. This is the Gibbs distribution for bosons obeying the eight-tick period.
background
The CMB Temperature module derives T₀ = 2.725 K from recombination redshift z* ≈ 1100 and T* ≈ 3000 K via the Saha equation with RS η. Planck radiance supplies the blackbody spectrum for photons. Upstream results include hbar = φ^{-5} in native units from Constants and the Breath1024 period T that encodes the eight-tick octave. The module doc states that the CMB is a perfect blackbody from the RS Gibbs distribution.
proof idea
The definition is a direct algebraic expression. It applies no lemmas and simply writes the closed form 2 * ν^3 / (exp(ν/T) - 1) in natural units.
why it matters
This definition feeds the theorems cmb_is_planck_spectrum and planck_positive, which establish that CMB photons obey the Planck law at rs_cmb_temperature. It implements the T7 eight-tick octave for photon statistics within the forcing chain from T0 to T8. The paper RS_CMB_Temperature.tex relies on it to match the observed temperature.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.