Zeroth law of thermodynamics: existence of an empirical temperature

Proved

ZerothLawThermo.existence_of_temperature

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

equivalence-relationthermodynamicszeroth-law

This is the "existence of temperature" form of the zeroth law of thermodynamics.

Let $S$ be a type of thermodynamic systems and $\mathrm{TE}$ the relation of thermal equilibrium on $S$ . Assume

every system is in thermal equilibrium with itself: $\mathrm{TE}(A,A)$ for all $A\in S$ ;
the zeroth law: if two systems are both in thermal equilibrium with a third system, they are in thermal equilibrium with each other, i.e. $\mathrm{TE}(A,C)\wedge\mathrm{TE}(B,C)\Rightarrow\mathrm{TE}(A,B)$ .

Then there exist a set of labels $T$ and a single-valued function $t:S\to T$ (an empirical temperature) such that

\forall A,B\in S,\qquad \mathrm{TE}(A,B)\iff t(A)=t(B).

In words, the condition for thermal equilibrium between systems is equality of a temperature. This is the logical foundation for thermometry and for empirical temperature scales.

Formalization Note The label type $T$ is arbitrary (it lives in the same universe as $S$ ); order and continuity properties of real temperature scales are not part of the zeroth law and are not asserted.

Preamble

import Definitions.Def_ZerothLawThermo_Defs
import Mathlib

universe u

open ZerothLawThermo

Formal statement

theorem ZerothLawThermo.existence_of_temperature {S : Type u} (TE : S → S → Prop)
    (hrefl : ∀ A : S, TE A A) (hzero : ZerothLaw TE) :
    ∃ (T : Type u) (t : S → T), IsEmpiricalTemperature TE t := by sorry

Source

Wikipedia, "Zeroth law of thermodynamics", revision oldid=1328026962, https://en.wikipedia.org/w/index.php?title=Zeroth_law_of_thermodynamics&oldid=1328026962; Lead section ("A quantity that is the same for two systems, if they can be placed in thermal equilibrium with each other, is a scale of temperature. The zeroth law is needed for the definition of such scales"); section "Equivalence relation"; section "History", Fowler & Guggenheim (ref. 17): "If two assemblies are each in thermal equilibrium with a third assembly, they are in thermal equilibrium with each other ... it may be shown to follow that the condition for thermal equilibrium between several assemblies is the equality of a certain single-valued function of the thermodynamic states of the assemblies, which may be called the temperature t"

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; non-blind

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.

Fix a universe level $u$ , a type $S$ in universe $u$ (possibly empty) and an arbitrary binary relation $\mathrm{TE}$ on $S$ . Assume:

$\mathrm{TE}(A,A)$ for every $A\in S$ ;
ZerothLaw TE: for all $A,B,C\in S$ , $\mathrm{TE}(A,C)$ and $\mathrm{TE}(B,C)$ together imply $\mathrm{TE}(A,B)$ .

Conclusion: there exist a type $T$ in the same universe $u$ and a function $t:S\to T$ such that for all $A,B\in S$ ,

\mathrm{TE}(A,B)\iff t(A)=t(B).

Nothing further is required of $T$ or $t$ (no ordering, no real values, no injectivity or surjectivity). Symmetry and transitivity of $\mathrm{TE}$ are not hypotheses. The hypotheses are satisfiable (e.g. by equality on $S$ ), so the statement is not vacuous.

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