Fig. 1: equal entropies at $T=0$ — no finite number of cooling steps reaches absolute zero

Proved

ThirdLawThermo.demagnetization_cycles_never_reach_zero

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

mathematical-physicsstatistical-mechanicsthermodynamicsthird-law

Let $S(T,x)$ be the equilibrium entropy at temperature $T\ge0$ and parameter value $x$ , and fix two parameter values $X_1,X_2$ (in magnetic refrigeration, a lower and a higher magnetic field). One cooling step at temperature $T_n$ consists of an isothermal change of the parameter from $X_1$ to $X_2$ at temperature $T_n$ , followed by an isentropic (reversible adiabatic) change back from $X_2$ to $X_1$ , which ends at the temperature $T_{n+1}\ge0$ determined by

S(T_{n+1},X_1)=S(T_n,X_2).

Assume that $T\mapsto S(T,X_2)$ is strictly increasing on $[0,\infty)$ and that there is no entropy difference at absolute zero, $S(0,X_1)=S(0,X_2)$ .

Theorem. Starting from $T_0>0$ , every finite sequence of $m$ such cooling steps ends at a positive temperature: $T_m>0$ . Hence absolute zero cannot be reached in a finite number of steps.

This is the right-hand panel of Fig. 1 of the source, the mechanism by which the third law implies the unattainability of absolute zero.

Formalization Note The temperatures are given as a sequence $T:\mathbb N\to\mathbb R$ of which only $T_0,\dots,T_m$ are constrained. The converse situation of the left-hand panel ( $S(0,X_1)\neq S(0,X_2)$ ) is not part of this statement.

Preamble

import Definitions.Def_ThirdLawThermo_Defs
import Mathlib

open Filter Topology

Formal statement

namespace ThirdLawThermo

theorem demagnetization_cycles_never_reach_zero {X : Type*} (S : ℝ → X → ℝ) (x₁ x₂ : X)
    (hmono₂ : StrictMonoOn (fun T => S T x₂) (Set.Ici 0))
    (hNernst : S 0 x₁ = S 0 x₂)
    (T : ℕ → ℝ) (m : ℕ) (hT₀ : 0 < T 0)
    (hstep : ∀ n < m, 0 ≤ T (n + 1) ∧ S (T (n + 1)) x₁ = S (T n) x₂) :
    0 < T m := 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 "Consequences", subsection "Absolute zero" and Fig. 1 ("Suppose that the temperature of a substance can be reduced in an isentropic process by changing the parameter X from X2 to X1 ... If there were an entropy difference at absolute zero, T = 0 could be reached in a finite number of steps. However, at T = 0 there is no entropy difference, so an infinite number of steps would be needed"; caption: "Right: An infinite number of steps is needed since S(0, X1) = S(0, X2)"); subsection "Example: magnetic refrigeration" for the two-step cycle.

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

$T\mapsto S(T,x_2)$ is strictly increasing on $[0,\infty)$ (no monotonicity is assumed in the variable $T$ for $x_1$ );
$S(0,x_1)=S(0,x_2)$ .

Let $T_0,T_1,T_2,\dots$ be any real sequence and $m$ any natural number, with $T_0>0$ , and assume that for every $n<m$ :

T_{n+1}\ge0\quad\text{and}\quad S(T_{n+1},x_1)=S(T_n,x_2).

Then $T_m>0$ . For $m=0$ the claim is just $T_0>0$ . Terms $T_n$ with $n>m$ are unconstrained.

View graph

Fig. 1: equal entropies at T=0T=0T=0 — no finite number of cooling steps reaches absolute zero

Fig. 1: equal entropies at $T=0$ — no finite number of cooling steps reaches absolute zero