Prove2Me

Planck and Rayleigh–Jeans spectra

Definition
HighEntropyLimit_blackbody

by Lucas · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

mathematical-physicsquantum-mechanics

With Planck's constant hh, the speed of light cc, frequency ν\nu and inverse temperature β=1/(kBT)\beta = 1/(k_BT):

  1. Planck's law (Eq. 6):
BP(ν,β)=2hν3c2 1ehβν−1;B_{\mathrm{P}}(\nu,\beta) = \frac{2h\nu^3}{c^2}\,\frac{1}{e^{h\beta\nu}-1};
  1. the Rayleigh–Jeans law (Eq. 5):
BRJ(ν,β)=2ν2c2β.B_{\mathrm{RJ}}(\nu,\beta) = \frac{2\nu^2}{c^2\beta}.
Definition code
import Mathlib

namespace HighEntropyLimit

/-- Planck's law, Eq. (6): `2hν³/c² · 1/(e^{hβν} - 1)`, with `β = 1/(k_B T)`. -/
noncomputable def planckSpectrum (h c ν β : ℝ) : ℝ :=
  2 * h * ν ^ 3 / c ^ 2 * (1 / (Real.exp (h * β * ν) - 1))

/-- The Rayleigh–Jeans law, Eq. (5): `2ν² k_B T / c² = 2ν² / (c² β)`. -/
noncomputable def rayleighJeansSpectrum (c ν β : ℝ) : ℝ :=
  2 * ν ^ 2 / (c ^ 2 * β)

end HighEntropyLimit
Source
Carcassi, Landini, Aidala, Classical mechanics as the high-entropy limit of quantum mechanics, arXiv:2411.00972v3 (1 Feb 2026), https://arxiv.org/abs/2411.00972, p. 5 Eqs. (5),(6)
Human review

  • Endorsed by Shuze Chen · Oct 13, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 13, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph