Cyclic heat-engine model: cycles, realizable cones, the Clausius and Kelvin statements, Carnot engines

Definition

SecondLawThermo_Defs

by Lucas · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

carnotmathematical-physicssecond-lawthermodynamics

Throughout, $\Theta$ is a type of empirical temperatures carrying a linear order ( $s<t$ means the reservoir at $s$ is colder than the one at $t$ ), and a cycle is a finitely supported function $c:\Theta\to\mathbb R$ : for each reservoir temperature $t$ , the number $c(t)$ is the net heat absorbed by the device from the reservoir at $t$ 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

W(c)=\sum_{t} c(t),

which is the first law for a device returning to its initial state. A set $\mathcal C$ of cycles stands for the physically realizable ones; it is assumed to be a convex cone: $0\in\mathcal C$ , $c+d\in\mathcal C$ (run two devices side by side), and $r\cdot c\in\mathcal C$ for $r\ge 0$ (scale a device). A cycle is reversible when $c\in\mathcal C$ and $-c\in\mathcal C$ . A cycle operates between $h$ and $k$ when $c(t)=0$ for every $t\notin\{h,k\}$ . A Carnot engine between a hot reservoir $h$ and a cold reservoir $k$ is a reversible cycle operating between $h$ and $k$ with $c(h)>0$ , $c(k)<0$ and $W(c)>0$ . The efficiency relative to the hot reservoir is $\eta=W(c)/c(h)$ .

Two impossibility statements are expressed in this language.

Clausius statement ("Heat can never pass from a colder to a warmer body without some other change, connected therewith, occurring at the same time."): for all temperatures $k<h$ , every realizable cycle operating between $h$ and $k$ with $W(c)=0$ satisfies $c(k)\le 0$ — a device whose only effect is to run through a cycle, exchanging heat with just these two reservoirs and doing no net work, cannot take heat out of the colder one.

Kelvin statement ("It is impossible for any system to operate in a thermodynamic cycle and deliver a net amount of energy by work to its surroundings while receiving energy by heat transfer from a single thermal reservoir."): every realizable cycle that exchanges heat with a single reservoir satisfies $W(c)\le 0$ .

Finally, $\mathcal C$ admits Carnot engines when for every pair $k<h$ there is a Carnot engine between $h$ and $k$ .

Formalization Note Cycles are modelled as finitely supported real-valued functions on the temperature type, so that running devices side by side is addition and scaling a device is scalar multiplication; the heat sign convention is "positive into the device". "Adiabatic enclosure", working substance, and the internal mechanism of a device play no role: a device is recorded only by the heat it draws from each reservoir.

Definition code

import Mathlib

namespace SecondLawThermo

/-- A cyclic process (one complete cycle of a cyclically operating device) exchanging heat with
finitely many thermal reservoirs. Reservoirs are labelled by their empirical temperature, an
element of the linearly ordered type `Θ` (`s < t` means that the reservoir at `s` is colder than
the one at `t`). The value `c t` is the net heat absorbed by the device from the reservoir at
temperature `t` during one cycle (heat entering the device is positive, heat leaving it is
negative); all but finitely many values vanish. -/
abbrev Cycle (Θ : Type*) := Θ →₀ ℝ

variable {Θ : Type*}

/-- The net work delivered by the device to its surroundings during one cycle. Since the device
returns to its initial state, the first law of thermodynamics makes it equal to the total net
heat absorbed from all reservoirs. -/
noncomputable def work (c : Cycle Θ) : ℝ := c.sum fun _ q => q

/-- The set `𝒞` of cycles that can actually be realized forms a convex cone: doing nothing is
realizable, two realizable devices may be run side by side (their heat exchanges add up), and a
realizable device may be scaled by any nonnegative factor. -/
structure IsCycleCone (𝒞 : Set (Cycle Θ)) : Prop where
  zero_mem : (0 : Cycle Θ) ∈ 𝒞
  add_mem : ∀ c d, c ∈ 𝒞 → d ∈ 𝒞 → c + d ∈ 𝒞
  smul_mem : ∀ (r : ℝ) (c : Cycle Θ), 0 ≤ r → c ∈ 𝒞 → r • c ∈ 𝒞

/-- A cycle is reversible (with respect to the realizable cycles `𝒞`) if both it and the exactly
reversed cycle, in which every heat exchange changes sign, are realizable. -/
def IsReversible (𝒞 : Set (Cycle Θ)) (c : Cycle Θ) : Prop := c ∈ 𝒞 ∧ -c ∈ 𝒞

/-- The cycle `c` exchanges heat only with the reservoirs at temperatures `h` and `k`. -/
def OperatesBetween (c : Cycle Θ) (h k : Θ) : Prop := ∀ t, t ≠ h → t ≠ k → c t = 0

/-- **Clausius statement.** Heat can never pass from a colder to a warmer body without some other
change: no realizable cycle that exchanges heat only with a hotter reservoir at `h` and a colder
reservoir at `k < h`, and produces no net work, absorbs a positive amount of heat from the colder
reservoir. -/
def ClausiusStatement [LinearOrder Θ] (𝒞 : Set (Cycle Θ)) : Prop :=
  ∀ h k : Θ, k < h → ∀ c ∈ 𝒞, OperatesBetween c h k → work c = 0 → c k ≤ 0

/-- **Kelvin statement.** No realizable cycle that exchanges heat with a single thermal reservoir
delivers a positive net amount of work. -/
def KelvinStatement (𝒞 : Set (Cycle Θ)) : Prop :=
  ∀ t : Θ, ∀ c ∈ 𝒞, (∀ s, s ≠ t → c s = 0) → work c ≤ 0

/-- A **Carnot engine** between the hot reservoir `h` and the cold reservoir `k`: a reversible
cycle exchanging heat only with these two reservoirs, absorbing a positive heat `q_H = c h` from
the hot reservoir, rejecting heat to the cold one (`q_C = c k < 0`) and delivering positive net
work. -/
def IsCarnotEngine (𝒞 : Set (Cycle Θ)) (c : Cycle Θ) (h k : Θ) : Prop :=
  IsReversible 𝒞 c ∧ OperatesBetween c h k ∧ 0 < c h ∧ c k < 0 ∧ 0 < work c

/-- Every pair of reservoirs at different temperatures admits a Carnot engine operating between
them. -/
def CarnotEnginesExist [LinearOrder Θ] (𝒞 : Set (Cycle Θ)) : Prop :=
  ∀ h k : Θ, k < h → ∃ c, IsCarnotEngine 𝒞 c h k

/-- The efficiency `η = W / q_H` of a cycle, relative to its hot reservoir `h`: net work per cycle
divided by the heat absorbed from `h` (meaningful when `c h > 0`). -/
noncomputable def efficiency (c : Cycle Θ) (h : Θ) : ℝ := work c / c h

end SecondLawThermo

Source

Wikipedia, "Second law of thermodynamics", revision oldid=1378607758, https://en.wikipedia.org/w/index.php?title=Second_law_of_thermodynamics&oldid=1378607758; sections "Clausius statement", "Kelvin statements", "Carnot's principle", "Thermodynamic temperature" (eq. (1))

Read-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.

This bundle declares, for an arbitrary type $\Theta$ :

Cycle. $\mathrm{Cycle}(\Theta)$ is the type of finitely supported functions $\Theta\to\mathbb R$ : a function $c$ assigning a real number $c(t)$ to each $t\in\Theta$ , with $c(t)=0$ for all but finitely many $t$ .
Work. $W(c)$ is the sum $\sum_{t\in\mathrm{supp}(c)}c(t)$ of the values of $c$ over its (finite) support. For $c=0$ this is $0$ .
Cycle cone. For a set $\mathcal C$ of cycles, $\mathrm{IsCycleCone}(\mathcal C)$ is the conjunction of three clauses: the zero function lies in $\mathcal C$ ; for all $c,d$ , if $c\in\mathcal C$ and $d\in\mathcal C$ then $c+d\in\mathcal C$ ; and for every real $r$ and every cycle $c$ , if $r\ge0$ and $c\in\mathcal C$ then $r\cdot c\in\mathcal C$ . Nothing requires $\mathcal C$ to be closed under negation, nor to be topologically closed.
Reversibility. $\mathrm{IsReversible}(\mathcal C,c)$ is the conjunction $c\in\mathcal C$ and $-c\in\mathcal C$ , where $(-c)(t)=-c(t)$ for every $t$ .
Two-reservoir support. $\mathrm{OperatesBetween}(c,h,k)$ says: for every $t\in\Theta$ , if $t\ne h$ and $t\ne k$ then $c(t)=0$ . It does not require $h\ne k$ , nor $c(h)\ne0$ or $c(k)\ne0$ ; the zero cycle satisfies it for every pair, and if $h=k$ it says that $c$ is supported in $\{h\}$ .
Clausius statement (needs a linear order on $\Theta$ ). $\mathrm{ClausiusStatement}(\mathcal C)$ says: for all $h,k\in\Theta$ with $k<h$ , and every $c\in\mathcal C$ such that $c(t)=0$ for all $t\notin\{h,k\}$ and $\sum_t c(t)=0$ , one has $c(k)\le0$ . The inequality is non-strict, so $c(k)=0$ is allowed. Nothing is said about cycles with nonzero net work, about cycles touching three or more reservoirs, or about $c(h)$ beyond what $\sum_t c(t)=0$ forces.
Kelvin statement. $\mathrm{KelvinStatement}(\mathcal C)$ says: for every $t\in\Theta$ and every $c\in\mathcal C$ such that $c(s)=0$ for all $s\ne t$ , one has $\sum_s c(s)\le0$ , which here is the same as $c(t)\le0$ . No order on $\Theta$ is used.
Carnot engine. $\mathrm{IsCarnotEngine}(\mathcal C,c,h,k)$ is the conjunction of five clauses: $c\in\mathcal C$ and $-c\in\mathcal C$ ; $c(t)=0$ for $t\notin\{h,k\}$ ; $c(h)>0$ ; $c(k)<0$ ; and $\sum_t c(t)>0$ . The last three force $h\ne k$ and $|c(h)|>|c(k)|$ . The predicate does not itself require any order relation between $h$ and $k$ .
Existence of Carnot engines (needs a linear order). $\mathrm{CarnotEnginesExist}(\mathcal C)$ says: for all $h,k$ with $k<h$ there is a $c$ with $\mathrm{IsCarnotEngine}(\mathcal C,c,h,k)$ . If $\Theta$ has at most one element, this holds vacuously.
Efficiency. $\mathrm{efficiency}(c,h)=\bigl(\sum_t c(t)\bigr)/c(h)$ . This is a total function: when $c(h)=0$ , Lean's division gives it the junk value $0$ .

These are definitions only. The bundle asserts and proves nothing.

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