Classical and quantum Gaussian entropies agree at large uncertainty

Proved

HighEntropyLimit.classical_sub_quantum_entropy_tendsto_zero

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

mathematical-physicsquantum-mechanics

Let $\hbar>0$ . The classical and quantum Gaussian entropies have the same asymptotics:

\lim_{\Sigma\to\infty}\big(S_C(\Sigma) - S_Q(\Sigma)\big) = 0.

This is the 'convergent prediction at high entropy' shown by the dashed difference curve in Fig. 2.

Preamble

import Mathlib
import Definitions.Def_HighEntropyLimit_gaussian_entropy
open Filter Topology

Formal statement

namespace HighEntropyLimit
theorem classical_sub_quantum_entropy_tendsto_zero (hbar : ℝ) (hhbar : 0 < hbar) :
    Tendsto (fun Sig : ℝ => classicalGaussianEntropy hbar Sig - quantumGaussianEntropy hbar Sig)
      atTop (𝓝 0) := 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. 4, Fig. 2 and the following paragraph ('The convergent prediction at high entropy ...')

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