planck_radiance
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not include frequency-dependent corrections from cosmic expansion.
- Does not address polarization or anisotropy details.
- Does not derive the temperature value itself.
Lean usage
theorem cmb_spectrum_positive (ν : ℝ) (hν : 0 < ν) : 0 < planck_radiance ν rs_cmb_temperature := by apply planck_positive ν rs_cmb_temperature hν; unfold rs_cmb_temperature; norm_numformal statement (Lean)
98noncomputable def planck_radiance (ν T : ℝ) : ℝ :=
proof body
Definition body.
99 2 * ν ^ 3 / (Real.exp (ν / T) - 1) -- in natural units hbar=c=kB=1
100
101/-- Planck spectrum is positive for T > 0, ν > 0. -/