Reflexivity and the zeroth law make thermal equilibrium an equivalence relation

Proved

ZerothLawThermo.equivalence_of_refl_zerothLaw

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

equivalence-relationthermodynamicszeroth-law

Let $S$ be a type of thermodynamic systems and $\mathrm{TE}$ a binary relation on $S$ ("is in thermal equilibrium with"). Assume

every system is in thermal equilibrium with itself: $\mathrm{TE}(A,A)$ for all $A\in S$ ;
the zeroth law: whenever $\mathrm{TE}(A,C)$ and $\mathrm{TE}(B,C)$ , also $\mathrm{TE}(A,B)$ .

Then $\mathrm{TE}$ is an equivalence relation on $S$ , i.e. it is reflexive, symmetric and transitive.

This is the precise mathematical content of the zeroth law: thermal equilibrium is an equivalence relation, which is what allows it to be represented by equality of a temperature.

Preamble

import Definitions.Def_ZerothLawThermo_Defs
import Mathlib

open ZerothLawThermo

Formal statement

theorem ZerothLawThermo.equivalence_of_refl_zerothLaw {S : Type*} (TE : S → S → Prop)
    (hrefl : ∀ A : S, TE A A) (hzero : ZerothLaw TE) :
    Equivalence TE := 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" (paragraphs following the right-Euclidean statement: "Binary relations that are both reflexive and Euclidean are equivalence relations. Thus, again implicitly assuming reflexivity, the zeroth law is therefore often expressed as a right-Euclidean statement"); also lead section: "It makes the relation of thermal equilibrium between systems an equivalence relation"

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.

For an arbitrary type $S$ (any universe, possibly empty) and an arbitrary binary relation $\mathrm{TE}$ on $S$ , assume:

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

Conclusion: $\mathrm{TE}$ is an equivalence relation, meaning all three of: $\mathrm{TE}(x,x)$ for all $x$ ; $\mathrm{TE}(x,y)\Rightarrow \mathrm{TE}(y,x)$ for all $x,y$ ; and $\mathrm{TE}(x,y)\wedge\mathrm{TE}(y,z)\Rightarrow \mathrm{TE}(x,z)$ for all $x,y,z$ . Both hypotheses are satisfiable (e.g. by equality on any type), 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