planck_positive
plain-language theorem explainer
Planck radiance is strictly positive for positive frequency and temperature. Workers deriving blackbody spectra in Recognition Science cite this to ground the CMB intensity. The proof unfolds the radiance definition then applies division positivity after verifying the exponential exceeds one via one_lt_exp_iff.
Claim. For all real numbers $ν > 0$ and $T > 0$, the spectral radiance $B_ν(T) := 2ν^3 / (e^{ν/T} - 1)$ (natural units) satisfies $B_ν(T) > 0$.
background
The CMB Temperature module derives T₀ = 2.725 K from the recombination redshift z* ≈ 1100 combined with recombination temperature T* ≈ 3000 K. Planck radiance is defined as the RS Gibbs distribution for photons (bosons, 8-tick full period): B_ν(T) = 2ν³ / (exp(ν/T) - 1) in units where ħ = c = k_B = 1. The module states that the CMB is a perfect blackbody from this distribution. Upstream, the fundamental period T is an abbrev for ℕ in Breath1024, and T(n) = n(n+1)/2 is the triangular number in Gap45.SyncMinimization.
proof idea
Unfold planck_radiance to expose the ratio 2ν³ / (exp(ν/T) - 1). Apply div_pos. The numerator is positive by positivity. For the denominator, obtain ν/T > 0 by div_pos on the hypotheses, then exp(ν/T) > 1 by Real.one_lt_exp_iff, and conclude the difference is positive by linarith.
why it matters
It is invoked directly by cmb_is_planck_spectrum to conclude that CMB photons follow the Planck spectrum at rs_cmb_temperature. This fills the planck_spectrum step in RS_CMB_Temperature.tex, confirming the blackbody property for bosons under the eight-tick period. It anchors positivity in the temperature derivation from the recombination epoch without new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.