Unique ground state $\Rightarrow$ entropy tends to $0$ at absolute zero

Proved

ThirdLawThermo.gibbsEntropy_tendsto_zero_of_unique_groundState

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 (unique ground state, perfect crystal). If the ground state is unique, $|G|=1$ , then the entropy tends to zero at absolute zero:

\lim_{T\to0^+}S(T)=0 .

This is the case of a perfect crystal singled out by Planck's and Lewis–Randall's formulations: with a single accessible microstate at $T=0$ , the entropy at absolute zero is exactly $k_B\ln 1=0$ .

Preamble

import Definitions.Def_ThirdLawThermo_Defs
import Mathlib

open Filter Topology

Formal statement

namespace ThirdLawThermo

theorem gibbsEntropy_tendsto_zero_of_unique_groundState {ι : Type*} [Fintype ι] [Nonempty ι]
    (kB : ℝ) (hkB : 0 < kB) (E : ι → ℝ) (hE : (groundStates E).card = 1) :
    Tendsto (fun T => gibbsEntropy kB E T) (𝓝[>] 0) (𝓝 0) := 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 ("there is typically one unique state (called the ground state) with minimum energy. In such a case, the entropy at absolute zero will be exactly zero"), section "Explanation" ("The entropy of a perfect crystal lattice as defined by Nernst\'s theorem is zero provided that its ground state is unique, because ln(1) = 0").

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>0$ be real, and let $E:\iota\to\mathbb R$ be arbitrary. Assume that exactly one $i\in\iota$ satisfies $E_i=\min_{j}E_j$ . With $Z$ , $p_i$ and $S$ as in the definition file,

Z(T)=\sum_i e^{-E_i/(k_BT)},\quad p_i(T)=\frac{e^{-E_i/(k_BT)}}{Z(T)},\quad S(T)=-k_B\sum_ip_i(T)\ln p_i(T),

the statement is that $S(T)\to0$ as $T\to0$ with $T>0$ . Nothing is asserted about $S$ at $T\le0$ . The hypothesis is satisfiable (e.g. any injective $E$ , or $|\iota|=1$ ).

View graph

Unique ground state ⇒\Rightarrow⇒ entropy tends to 000 at absolute zero

Unique ground state $\Rightarrow$ entropy tends to $0$ at absolute zero