Zero-temperature entropy equals $k_B\ln(\#\text{ground states})$

Proved

ThirdLawThermo.gibbsEntropy_tendsto_kB_log_card_groundStates

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 (statistical form of the third law). As the temperature decreases to absolute zero, the entropy approaches a constant, namely the Boltzmann constant times the natural logarithm of the number of ground states:

\lim_{T\to0^+}S(T)=k_B\ln|G| .

The limit depends on the system only through the degeneracy $|G|$ of its ground state, and not on the excited energy levels; this is the precise sense in which the zero-temperature entropy is "a constant value" fixed by the ground state. When the ground state is unique the limit is $0$ , and when it is degenerate the limit is the residual entropy $k_B\ln|G|>0$ .

Formalization Note The limit is one-sided ( $T\to0^+$ through $T>0$ ), so the junk value of the Lean definition at $T=0$ plays no role.

Preamble

import Definitions.Def_ThirdLawThermo_Defs
import Mathlib

open Filter Topology

Formal statement

namespace ThirdLawThermo

theorem gibbsEntropy_tendsto_kB_log_card_groundStates {ι : Type*} [Fintype ι] [Nonempty ι]
    (kB : ℝ) (hkB : 0 < kB) (E : ι → ℝ) :
    Tendsto (fun T => gibbsEntropy kB E T) (𝓝[>] 0)
      (𝓝 (kB * Real.log (groundStates E).card)) := 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; lead section ("the entropy of a closed system at thermodynamic equilibrium approaches a constant value when its temperature approaches absolute zero"; "there is typically one unique state (called the ground state) with minimum energy"), section "History" ("its entropy is determined only by the degeneracy of the ground state"), section "Explanation" ("the absolute entropy of any system at zero temperature is the natural log of the number of ground states times the Boltzmann constant kB").

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, let $k_B$ be a real number with $k_B>0$ , and let $E:\iota\to\mathbb R$ be an arbitrary function (no further conditions; energies may be negative or repeated).

For $T\in\mathbb R$ put $Z(T)=\sum_{i\in\iota}\exp(-E_i/(k_BT))$ , $p_i(T)=\exp(-E_i/(k_BT))/Z(T)$ and $S(T)=-k_B\sum_{i\in\iota}p_i(T)\ln p_i(T)$ . Let $G=\{i\in\iota: E_i=\min_{j\in\iota}E_j\}$ (a nonempty finite set) and $|G|$ its number of elements. The statement is that

S(T)\longrightarrow k_B\ln|G|\qquad\text{as }T\to0\text{ with }T>0,

i.e. for every $\varepsilon>0$ there is $\delta>0$ such that $|S(T)-k_B\ln|G||<\varepsilon$ whenever $0<T<\delta$ . Values of $S$ at $T\le 0$ are not constrained. If $|\iota|=1$ then $|G|=1$ and the asserted limit is $0$ .

View graph

Zero-temperature entropy equals kBln⁡(#ground states)k_B\ln(\#\text{ground states})kB​ln(#ground states)

Zero-temperature entropy equals $k_B\ln(\#\text{ground states})$