Thermal equilibrium partitions the systems into classes of mutual equilibrium

Proved

ZerothLawThermo.exists_partition_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 is a family $\mathcal P$ of subsets of $S$ such that

$\mathcal P$ is a partition of $S$ : no member of $\mathcal P$ is empty, and every system $A\in S$ belongs to exactly one member of $\mathcal P$ ;
for all systems $A,B$ ,

\mathrm{TE}(A,B)\iff \exists\, c\in\mathcal P,\ A\in c\ \text{and}\ B\in c.

In words: systems split into disjoint classes; two systems are in thermal equilibrium exactly when they lie in the same class.

Preamble

import Definitions.Def_ZerothLawThermo_Defs
import Mathlib

open ZerothLawThermo

Formal statement

theorem ZerothLawThermo.exists_partition_of_equivalence {S : Type*} (TE : S → S → Prop)
    (hTE : Equivalence TE) :
    ∃ P : Set (Set S), Setoid.IsPartition P ∧
      ∀ A B : S, TE A B ↔ ∃ c ∈ P, A ∈ c ∧ B ∈ 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": "In other words, the set of all systems each in its own state of internal thermodynamic equilibrium may be divided into subsets in which every system belongs to one and only one subset, and is in thermal equilibrium with every other member of that subset, and is not in thermal equilibrium with a member of any other subset." Also section "Foundation of temperature", first paragraph after the list.

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 a binary relation $\mathrm{TE}$ on $S$ that is assumed to be an equivalence relation (reflexive, symmetric, transitive), the statement asserts that there exists a set $\mathcal P$ of subsets of $S$ such that:

$\mathcal P$ satisfies Mathlib's Setoid.IsPartition: the empty set is not a member of $\mathcal P$ , and for every $a\in S$ there is a unique $b\in\mathcal P$ with $a\in b$ ;
for all $A,B\in S$ : $\mathrm{TE}(A,B)$ holds if and only if there is some $c\in\mathcal P$ containing both $A$ and $B$ .

When $S$ is empty, $\mathcal P=\varnothing$ satisfies both conditions.

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