Zeroth law of thermodynamics: thermal equilibrium vocabulary
DefinitionZerothLawThermo_DefsThis definition file fixes the vocabulary for the mission. Throughout, is a type of thermodynamic systems and is a binary relation on , with read as " is in thermal equilibrium with ".
- Zeroth law (right-Euclidean form): satisfies the zeroth law if
i.e. two systems both in thermal equilibrium with a third are in thermal equilibrium with each other. 2. Planck's form (left-Euclidean form):
i.e. if a body is in thermal equilibrium with two bodies and , then and are in thermal equilibrium with one another. 3. Empirical temperature: a map into an arbitrary type is an empirical temperature for if
These are the objects in terms of which all theorems of the mission are stated.
Formalization Note Reflexivity of is deliberately not built into these definitions; theorems that need it state it as a hypothesis.
import Mathlib
namespace ZerothLawThermo
/-- The zeroth law of thermodynamics in its usual ("right-Euclidean") form, for a relation
`TE` of thermal equilibrium on a type `S` of thermodynamic systems: if two systems `A` and `B`
are both in thermal equilibrium with a third system `C`, then `A` and `B` are in thermal
equilibrium with each other. -/
def ZerothLaw {S : Type*} (TE : S → S → Prop) : Prop :=
∀ A B C : S, TE A C → TE B C → TE A B
/-- Planck's ("left-Euclidean") form of the zeroth law: if a system `C` is in thermal
equilibrium with two other systems `A` and `B`, then `A` and `B` are in thermal equilibrium
with one another. -/
def ZerothLawPlanck {S : Type*} (TE : S → S → Prop) : Prop :=
∀ A B C : S, TE C A → TE C B → TE A B
/-- A tagging `t : S → T` of systems is an empirical temperature scale for the thermal
equilibrium relation `TE` if two systems are in thermal equilibrium exactly when they carry
the same tag. -/
def IsEmpiricalTemperature {S T : Type*} (TE : S → S → Prop) (t : S → T) : Prop :=
∀ A B : S, TE A B ↔ t A = t B
end ZerothLawThermo
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.
The file declares three predicates in the namespace ZerothLawThermo, each taking a type (in any universe) and a binary relation on with values in propositions; no other hypotheses are imposed (in particular may be empty and is not assumed reflexive or symmetric).
ZerothLaw TEholds iff for all : if and , then . (The common system is in the second argument of both hypotheses.)ZerothLawPlanck TEholds iff for all : if and , then . (The common system is in the first argument of both hypotheses.)- For a further type (any universe) and a function ,
IsEmpiricalTemperature TE tholds iff for all :
Nothing is assumed about (no order, no real-number structure); equality is ordinary equality in .
The file imports all of Mathlib and contains no theorems, axioms or sorry.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.