Thermal equilibrium is transitive

Proved

ZerothLawThermo.trans_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$ such that $\mathrm{TE}(A,A)$ for all $A$ , and satisfying the zeroth law ( $\mathrm{TE}(A,C)\wedge\mathrm{TE}(B,C)\Rightarrow\mathrm{TE}(A,B)$ ). Then for all systems $A,B,C$ ,

\mathrm{TE}(A,B)\ \wedge\ \mathrm{TE}(B,C)\ \Longrightarrow\ \mathrm{TE}(A,C).

This is the form of the law most often quoted in introductory texts.

Preamble

import Definitions.Def_ZerothLawThermo_Defs
import Mathlib

open ZerothLawThermo

Formal statement

theorem ZerothLawThermo.trans_of_refl_zerothLaw {S : Type*} (TE : S → S → Prop)
    (hrefl : ∀ A : S, TE A A) (hzero : ZerothLaw TE) (A B C : S)
    (hAB : TE A B) (hBC : TE B C) :
    TE A C := 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": "Another consequence of equivalence is that thermal equilibrium is described as a transitive relation: If A is in thermal equilibrium with B and if B is in thermal equilibrium with C, then A is in thermal equilibrium with C."

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 binary relation $\mathrm{TE}$ on $S$ , assume $\mathrm{TE}(X,X)$ for every $X\in S$ and ZerothLaw TE (for all $X,Y,Z$ : $\mathrm{TE}(X,Z)\wedge\mathrm{TE}(Y,Z)\Rightarrow\mathrm{TE}(X,Y)$ ). Then for any $A,B,C\in S$ with $\mathrm{TE}(A,B)$ and $\mathrm{TE}(B,C)$ , it follows that $\mathrm{TE}(A,C)$ .

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