An equivalence relation of thermal equilibrium admits an empirical temperature tagging

Proved

ZerothLawThermo.exists_empiricalTemperature_of_equivalence

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

equivalence-relationthermodynamicszeroth-law

Let $S$ be a type of thermodynamic systems and suppose thermal equilibrium $\mathrm{TE}$ is an equivalence relation on $S$ . Then there exist a set of labels $T$ and a labelling $t:S\to T$ which is an empirical temperature for $\mathrm{TE}$ :

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

Two systems carry the same tag exactly when they are in thermal equilibrium; the set of labels is arbitrary.

Formalization Note The label type $T$ is required to live in the same universe as $S$ .

Preamble

import Definitions.Def_ZerothLawThermo_Defs
import Mathlib

universe u

open ZerothLawThermo

Formal statement

theorem ZerothLawThermo.exists_empiricalTemperature_of_equivalence {S : Type u} (TE : S → S → Prop)
    (hTE : Equivalence 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; Section "Equivalence relation": "This means that a unique \"tag\" can be assigned to every system, and if the \"tags\" of two systems are the same, they are in thermal equilibrium with each other, and if different, they are not." Also section "Foundation of temperature": "This partitioning allows any member of the subset to be uniquely \"tagged\" with a label identifying the subset to which it belongs. Although the labeling may be quite arbitrary, temperature is just such a labeling process".

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 a binary relation $\mathrm{TE}$ on $S$ assumed to be an equivalence relation (reflexive, symmetric, transitive). The statement asserts that there exist a type $T$ in the same universe $u$ and a function $t:S\to T$ such that IsEmpiricalTemperature TE t, i.e. for all $A,B\in S$ :

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

No structure (order, reals, finiteness) is required of $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