Under reflexivity, the two Euclidean forms of the zeroth law are equivalent
ProvedZerothLawThermo.zerothLaw_iff_zerothLawPlanck_of_reflLet be a type of thermodynamic systems and a binary relation on such that for all . Then the following are equivalent:
- the zeroth law (right-Euclidean form): for all ;
- Planck's form (left-Euclidean form): for all .
This justifies the source's passage from Planck's statement to the now-standard statement of the law, once reflexivity is assumed.
import Definitions.Def_ZerothLawThermo_Defs import Mathlib open ZerothLawThermo
theorem ZerothLawThermo.zerothLaw_iff_zerothLawPlanck_of_refl {S : Type*} (TE : S → S → Prop)
(hrefl : ∀ A : S, TE A A) :
ZerothLaw TE ↔ ZerothLawPlanck TE := by sorryRead-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 (any universe, possibly empty) and an arbitrary binary relation on with for every , the statement asserts the logical equivalence
where the left side means: for all , ; and the right side means: for all , . Reflexivity is the only hypothesis; both directions of the equivalence are asserted.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.