Over a cycle, net work done equals net heat taken in

Proved

FirstLawThermo.work_eq_heat_of_cyclic

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

first-lawinternal-energythermodynamics

Let $\sigma$ be the state set of a closed system, $U:\sigma\to\mathbb R$ a function, and $p$ a cyclic process, i.e. one returning the system to its initial state: $p_{\mathrm{start}}=p_{\mathrm{finish}}$ . Then the net work done by the system equals the net heat taken in:

W(p)=Q_U(p).

This is Clausius' cyclic form of the first law: in each repetition of a cyclic process, the net work done by the system is proportional to the heat consumed (equal, when heat and work are measured in the same units).

Formalization Note Heat and work are measured in the same units, so Joule's mechanical equivalent of heat is normalized to $1$ .

Preamble

import Definitions.Def_FirstLawThermo_Defs
import Mathlib

open FirstLawThermo

Formal statement

theorem FirstLawThermo.work_eq_heat_of_cyclic {σ : Type*} (U : σ → ℝ) (p : Process σ)
    (hcyc : p.IsCyclic) :
    p.work = heat U p := by sorry

Source

Wikipedia, "First law of thermodynamics", revision oldid=1366986255, https://en.wikipedia.org/w/index.php?title=First_law_of_thermodynamics&oldid=1366986255; Section "Description", subsection "Cyclic processes": "A cyclic process is one that can be repeated indefinitely often, returning the system to its initial state. Of particular interest for single cycle of a cyclic process are the net work done, and the net heat taken in ... In each repetition of a cyclic process, the net work done by the system, measured in mechanical units, is proportional to the heat consumed, measured in calorimetric units."; Section "Original statements": Clausius, "a quantity of heat is consumed which is proportional to the work done".

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.

For an arbitrary type $\sigma$ , an arbitrary function $U:\sigma\to\mathbb R$ and an arbitrary process $p$ with $p_{\mathrm{start}}=p_{\mathrm{finish}}$ (no membership in any set and no internal-energy assumption on $U$ ):

W(p)=U(p_{\mathrm{finish}})-U(p_{\mathrm{start}})+W(p).

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