Zero temperature cannot be reached adiabatically from a positive temperature

Proved

ThirdLawThermo.adiabatic_unattainability

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

mathematical-physicsstatistical-mechanicsthermodynamicsthird-law

Let $X$ be a set of values of an external parameter (for example the applied magnetic field or the pressure), and let $S(T,x)$ be the equilibrium entropy of a system at temperature $T\ge0$ and parameter value $x\in X$ . Assume that at each fixed $x$ the entropy is strictly increasing in $T$ on $[0,\infty)$ (positive heat capacity). Assume moreover the third law in Nernst's form: the entropy at absolute zero does not depend on the parameter, $S(0,x)=S(0,y)$ for all $x,y\in X$ .

Theorem (adiabatic accessibility statement). A reversible adiabatic (isentropic) process cannot take a state of positive temperature to a state of zero temperature: if $T>0$ , $T'\ge0$ and

S(T',x')=S(T,x),

then $T'\neq0$ .

This is the formulation of the third law "in adiabatic accessibility", derived here from the parameter-independence of the zero-temperature entropy.

Formalization Note Adiabatic processes are modelled as reversible ones, i.e. as preserving the equilibrium entropy; the strict monotonicity in $T$ encodes positivity of the heat capacity.

Preamble

import Definitions.Def_ThirdLawThermo_Defs
import Mathlib

open Filter Topology

Formal statement

namespace ThirdLawThermo

theorem adiabatic_unattainability {X : Type*} (S : ℝ → X → ℝ)
    (hmono : ∀ x : X, StrictMonoOn (fun T => S T x) (Set.Ici 0))
    (hNernst : ∀ x y : X, S 0 x = S 0 y)
    (T : ℝ) (x : X) (T' : ℝ) (x' : X) (hT : 0 < T) (hT' : 0 ≤ T')
    (hS : S T' x' = S T x) :
    T' ≠ 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; section "Formulations", "The statement in adiabatic accessibility: It is impossible to start from a state of positive temperature, and adiabatically reach a state with zero temperature"; the Nernst hypothesis is the "Nernst statement" of the same section ("At absolute zero, the entropy change becomes independent of the process path").

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 $X$ be an arbitrary type and $S:\mathbb R\times X\to\mathbb R$ an arbitrary function, written $S(T,x)$ . Assume

for every $x\in X$ , $T\mapsto S(T,x)$ is strictly increasing on $[0,\infty)$ : $0\le T_1<T_2$ implies $S(T_1,x)<S(T_2,x)$ ;
$S(0,x)=S(0,y)$ for all $x,y\in X$ .

Then for all reals $T,T'$ and all $x,x'\in X$ with $T>0$ , $T'\ge0$ and $S(T',x')=S(T,x)$ , one has $T'\ne0$ (equivalently, with $T'\ge0$ , $T'>0$ ). Nothing is assumed about $S$ at negative temperatures, about continuity, or about the existence of such a $T'$ ; $X$ may be empty or a singleton.

View graph