Zeros and signs of the Gaussian entropy curves

Proved

HighEntropyLimit.gaussian_entropy_zero_points

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

mathematical-physicsquantum-mechanics

Let $\hbar>0$ . Then

$S_Q(\hbar/2) = 0$ : the quantum entropy vanishes at the Heisenberg bound;
$S_Q(\Sigma) > 0$ for every $\Sigma > \hbar/2$ ;
$S_C(\hbar/e) = 0$ ;
$S_C(\Sigma) < 0$ for every $0 < \Sigma < \hbar/e$ .

So the quantum curve reaches zero at $\hbar/2$ , while the classical curve reaches zero at $\hbar/e$ and then continues into negative values.

Preamble

import Mathlib
import Definitions.Def_HighEntropyLimit_gaussian_entropy

Formal statement

namespace HighEntropyLimit
theorem gaussian_entropy_zero_points (hbar : ℝ) (hhbar : 0 < hbar) :
    quantumGaussianEntropy hbar (hbar / 2) = 0 ∧
    (∀ Sig : ℝ, hbar / 2 < Sig → 0 < quantumGaussianEntropy hbar Sig) ∧
    classicalGaussianEntropy hbar (hbar / Real.exp 1) = 0 ∧
    (∀ Sig : ℝ, 0 < Sig → Sig < hbar / Real.exp 1 → classicalGaussianEntropy hbar Sig < 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. 3, Section 2.2, text after Eq. (3): 'in quantum mechanics the entropy ... reaches zero at ħ/2 ...; classical mechanics reaches zero entropy for ħ/e, and then continues in the negative region'

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