The Clausius statement implies the Kelvin statement
ProvedSecondLawThermo.kelvin_of_clausiusThroughout, is a type of empirical temperatures carrying a linear order ( means the reservoir at is colder than the one at ), and a cycle is a finitely supported function : for each reservoir temperature , the number is the net heat absorbed by the device from the reservoir at in one complete cycle (negative when heat is rejected to it), and only finitely many reservoirs are touched. The work delivered in the cycle is
which is the first law for a device returning to its initial state. A set of cycles stands for the physically realizable ones; it is assumed to be a convex cone: , (run two devices side by side), and for (scale a device). A cycle is reversible when and . A cycle operates between and when for every . A Carnot engine between a hot reservoir and a cold reservoir is a reversible cycle operating between and with , and . The efficiency relative to the hot reservoir is .
Statement. Let have at least two elements and let be a convex cone of realizable cycles admitting a Carnot engine between every pair of reservoirs at different temperatures. If the Clausius statement holds for , then so does the Kelvin statement:
This is the direction the article argues explicitly: an engine draining heat from a single reservoir and converting it entirely into work, paired with a reversed Carnot engine, has as its net and sole effect the transfer of heat from a cooler to a hotter reservoir.
Formalization Note At least two reservoir temperatures must exist for the Clausius statement to have any content; with a single temperature it holds vacuously while the Kelvin statement can fail.
import Definitions.Def_SecondLawThermo_Defs import Mathlib
namespace SecondLawThermo
theorem kelvin_of_clausius {Θ : Type*} [LinearOrder Θ] [Nontrivial Θ] (𝒞 : Set (Cycle Θ))
(h𝒞 : IsCycleCone 𝒞) (hCarnot : CarnotEnginesExist 𝒞) (hCl : ClausiusStatement 𝒞) :
KelvinStatement 𝒞 := by sorry
end SecondLawThermoRead-back
What the Lean code literally says, in plain math · Aristotle (Harmonic), the drafting agent itself; non-blind read-back
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.
Let be a linearly ordered type with at least two distinct elements, and let be a set of finitely supported functions , with . Assume:
- , is closed under addition, and under multiplication by every real ;
- for all there exists with , for , , , ;
- for all and every vanishing outside with , one has .
Then for every and every vanishing at every , one has (equivalently ).
The assumption that has at least two elements is used as a hypothesis of the theorem, not derived.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.