Degenerate ground state: zero-temperature entropy $\ge k_B\ln 2$

Proved

ThirdLawThermo.kB_log_two_le_zeroTemp_gibbsEntropy

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

mathematical-physicsstatistical-mechanicsthermodynamicsthird-law

Let $\iota$ be a finite nonempty set of microstates with energies $E_i$ , let $k_B>0$ be the Boltzmann constant, and write $G=\{i:E_i=\min_jE_j\}$ for the set of ground states. At temperature $T>0$ the system is in canonical equilibrium with probabilities $p_i(T)=e^{-E_i/(k_BT)}/Z(T)$ , $Z(T)=\sum_je^{-E_j/(k_BT)}$ , and has Gibbs entropy $S(T)=-k_B\sum_ip_i(T)\ln p_i(T)$ (see the definition file ThirdLawThermo_Defs).

Theorem (residual entropy of a degenerate ground state). If the ground state is degenerate, $|G|\ge2$ (for instance the two time-reversed ground states of a system with half-integer net spin), then the entropy has a limit $S_0$ at absolute zero and this zero-point entropy is at least $k_B\ln 2$ :

S_0=\lim_{T\to0^+}S(T)\ \text{exists and}\ S_0\ge k_B\ln 2 .

This shows that the third law does not force zero entropy at $T=0$ : a non-unique ground state leaves a residual entropy.

Preamble

import Definitions.Def_ThirdLawThermo_Defs
import Mathlib

open Filter Topology

Formal statement

namespace ThirdLawThermo

theorem kB_log_two_le_zeroTemp_gibbsEntropy {ι : Type*} [Fintype ι] [Nonempty ι]
    (kB : ℝ) (hkB : 0 < kB) (E : ι → ℝ) (hE : 2 ≤ (groundStates E).card) :
    ∃ S₀ : ℝ, Tendsto (fun T => gibbsEntropy kB E T) (𝓝[>] 0) (𝓝 S₀) ∧
      kB * Real.log 2 ≤ S₀ := by sorry

end ThirdLawThermo

Source

Wikipedia, "Third law of thermodynamics", revision oldid=1369622029, https://en.wikipedia.org/w/index.php?title=Third_law_of_thermodynamics&oldid=1369622029; section "Systems with non-zero entropy at absolute zero" ("An example of a system that does not have a unique ground state is one whose net spin is a half-integer, for which time-reversal symmetry gives two degenerate ground states. For such systems, the entropy at zero temperature is at least kB ln(2)").

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic), the drafting agent itself; non-blind read-back

Disclosure: this read-back is NOT blind. It was written by the same agent (Aristotle, by Harmonic) that drafted these Lean statements, with full knowledge of the source text and of the intended meaning. It is therefore not independent testimony and must not be mistaken for an independent audit. Reviewers should check the Lean code against the source themselves.

Let $\iota$ be any finite, nonempty type, $k_B>0$ real, and $E:\iota\to\mathbb R$ arbitrary, and assume that the set $G=\{i: E_i=\min_jE_j\}$ has at least $2$ elements. With $S(T)=-k_B\sum_ip_i(T)\ln p_i(T)$ , $p_i(T)=e^{-E_i/(k_BT)}/\sum_je^{-E_j/(k_BT)}$ , the statement asserts that there is a real number $S_0$ such that

$S(T)\to S_0$ as $T\to0$ with $T>0$ , and
$k_B\ln 2\le S_0$ .

No spin or time-reversal structure is modelled; the only hypothesis is the counting condition $|G|\ge2$ .

View graph

Degenerate ground state: zero-temperature entropy ≥kBln⁡2\ge k_B\ln 2≥kB​ln2

Degenerate ground state: zero-temperature entropy $\ge k_B\ln 2$