Existence and uniqueness of the thermodynamic temperature scale

Proved

SecondLawThermo.thermodynamic_temperature

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

carnotmathematical-physicssecond-lawthermodynamics

Throughout, $\Theta$ is a type of empirical temperatures carrying a linear order ( $s<t$ means the reservoir at $s$ is colder than the one at $t$ ), and a cycle is a finitely supported function $c:\Theta\to\mathbb R$ : for each reservoir temperature $t$ , the number $c(t)$ is the net heat absorbed by the device from the reservoir at $t$ in one complete cycle (negative when heat is rejected to it), and only finitely many reservoirs are touched. The work delivered in the cycle is

W(c)=\sum_{t} c(t),

which is the first law for a device returning to its initial state. A set $\mathcal C$ of cycles stands for the physically realizable ones; it is assumed to be a convex cone: $0\in\mathcal C$ , $c+d\in\mathcal C$ (run two devices side by side), and $r\cdot c\in\mathcal C$ for $r\ge 0$ (scale a device). A cycle is reversible when $c\in\mathcal C$ and $-c\in\mathcal C$ . A cycle operates between $h$ and $k$ when $c(t)=0$ for every $t\notin\{h,k\}$ . A Carnot engine between a hot reservoir $h$ and a cold reservoir $k$ is a reversible cycle operating between $h$ and $k$ with $c(h)>0$ , $c(k)<0$ and $W(c)>0$ . The efficiency relative to the hot reservoir is $\eta=W(c)/c(h)$ .

Statement (goal). Let $\mathcal C$ be a convex cone of realizable cycles which satisfies the Clausius statement and admits a Carnot engine between every pair of reservoirs at different temperatures, and let $T_0$ be a reference reservoir (the triple point of water). Then there is a function $T:\Theta\to\mathbb R$ with

$T(t)>0$ for every $t$ ;
$T(T_0)=273.16$ ;
for all $k<h$ , every Carnot engine $e$ between $h$ and $k$ satisfies $\dfrac{|e(k)|}{|e(h)|}=\dfrac{T(k)}{T(h)}$ ;

and $T$ is the only function with these three properties.

This is the article's claim that "the second law allows a distinguished temperature scale, which defines an absolute, thermodynamic temperature, independent of the properties of any particular reference thermometric body": from the Clausius statement alone, the ratio of heats exchanged by any reversible engine between two reservoirs is a ratio of two numbers attached to the reservoirs themselves, normalized by the Kelvin convention $273.16$ at the triple point of water.

Preamble

import Definitions.Def_SecondLawThermo_Defs
import Mathlib

Formal statement

namespace SecondLawThermo

theorem thermodynamic_temperature {Θ : Type*} [LinearOrder Θ] (𝒞 : Set (Cycle Θ))
    (h𝒞 : IsCycleCone 𝒞) (hCl : ClausiusStatement 𝒞) (hCarnot : CarnotEnginesExist 𝒞)
    (T₀ : Θ) :
    ∃ T : Θ → ℝ, (∀ t, 0 < T t) ∧ T T₀ = 273.16 ∧
      (∀ (h k : Θ) (e : Cycle Θ), k < h → IsCarnotEngine 𝒞 e h k →
        |e k| / |e h| = T k / T h) ∧
      ∀ T' : Θ → ℝ, (∀ t, 0 < T' t) → T' T₀ = 273.16 →
        (∀ (h k : Θ) (e : Cycle Θ), k < h → IsCarnotEngine 𝒞 e h k →
          |e k| / |e h| = T' k / T' h) → T' = T := by sorry

end SecondLawThermo

Source

Wikipedia, "Second law of thermodynamics", revision oldid=1378607758, https://en.wikipedia.org/w/index.php?title=Second_law_of_thermodynamics&oldid=1378607758; sections "Relating the second law to the definition of temperature" and "Thermodynamic temperature" (through

T^*=273.16\,\mathrm{K}\cdot f(T_1,T)

T_1^*=273.16\,\mathrm{K}

)

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 $\Theta$ be a linearly ordered type and $\mathcal C$ a set of finitely supported functions $\Theta\to\mathbb R$ ; for such a function $c$ write $W(c)=\sum_t c(t)$ . Call $e$ a Carnot engine between $h$ and $k$ when $e\in\mathcal C$ , $-e\in\mathcal C$ , $e(t)=0$ for $t\notin\{h,k\}$ , $e(h)>0$ , $e(k)<0$ and $W(e)>0$ . Assume:

$0\in\mathcal C$ , and $\mathcal C$ is closed under addition and under multiplication by every real $r\ge0$ ;
for all $k<h$ , every $c\in\mathcal C$ vanishing outside $\{h,k\}$ with $W(c)=0$ satisfies $c(k)\le0$ ;
for all $k<h$ there exists a Carnot engine between $h$ and $k$ .

Let $T_0\in\Theta$ be arbitrary. Then there exists $T:\Theta\to\mathbb R$ such that

T(t)>0\ \ \text{for all } t,\qquad T(T_0)=273.16,\qquad \frac{|e(k)|}{|e(h)|}=\frac{T(k)}{T(h)}

for all $k<h$ and every Carnot engine $e$ between $h$ and $k$ ; and moreover every $T':\Theta\to\mathbb R$ that is everywhere positive, takes the value $273.16$ at $T_0$ , and satisfies the same ratio identity for all $k<h$ and all Carnot engines, is equal to $T$ as a function.

The number $273.16$ is a bare real constant; no unit is attached, and no physical interpretation of $T_0$ is part of the statement. The ratio identity is required of every Carnot engine between the two reservoirs, so it also asserts that this ratio does not depend on which engine is used. Nothing asserts that $T$ is monotone, nor that $T$ is related to the order on $\Theta$ beyond the displayed identity. If $\Theta$ has exactly one element, hypothesis 3 is vacuous and the constant function $273.16$ is the unique such $T$ .

Human review

Endorsed by Shuze Chen · Oct 10, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 10, 2026
Confirmed by the mission captain (proposal self-audit).

View graph