Prove2Me

Planck's law reduces to Rayleigh–Jeans at high temperature

Proved
HighEntropyLimit.planck_div_rayleigh_jeans_tendsto_one

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

mathematical-physicsquantum-mechanics

Let h,c,ν>0h, c, \nu > 0. As the inverse temperature β→0+\beta\to0^+ (high temperature, hence high entropy), Planck's law is asymptotic to the Rayleigh–Jeans law:

lim⁡β→0+2hν3c21ehβν−12ν2c2β=1.\lim_{\beta\to0^+}\frac{\dfrac{2h\nu^3}{c^2}\dfrac{1}{e^{h\beta\nu}-1}}{\dfrac{2\nu^2}{c^2\beta}} = 1.
Preamble
import Mathlib
import Definitions.Def_HighEntropyLimit_blackbody
open Filter Topology
Formal statement
namespace HighEntropyLimit
theorem planck_div_rayleigh_jeans_tendsto_one (h c ν : ℝ) (hh : 0 < h) (hc : 0 < c)
    (hν : 0 < ν) :
    Tendsto (fun β : ℝ => planckSpectrum h c ν β / rayleighJeansSpectrum c ν β) (𝓝[>] 0)
      (𝓝 1) := by sorry
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, Eq. (8)
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