Clausius form of the first law: $\Delta U = Q - W$

Proved

FirstLawThermo.deltaU_eq_heat_sub_work

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$ any process, with work $W(p)$ done by the system. With the heat supplied defined as the residual $Q_U(p)=U(p_{\mathrm{finish}})-U(p_{\mathrm{start}})+W(p)$ ,

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

This is the first law in the sign convention of Clausius, $\Delta U=Q-W$ : heat supplied to the system counts as positive and work done by the system is subtracted. In the mechanical approach followed here it holds for every process, because heat is defined as the part of the change of internal energy not accounted for by work.

Preamble

import Definitions.Def_FirstLawThermo_Defs
import Mathlib

open FirstLawThermo

Formal statement

theorem FirstLawThermo.deltaU_eq_heat_sub_work {σ : Type*} (U : σ → ℝ) (p : Process σ) :
    U p.finish - U p.start = heat U p - p.work := 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 "Definition": "With the sign convention of Rudolf Clausius, that heat supplied to the system is positive, but work done by the system is subtracted, a change in the internal energy,

\Delta U

, is written

\Delta U = Q - W

."; Section "Various statements of the law for closed systems": heat "is defined as a residual difference between change of internal energy and work done on the system".

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$ on $\sigma$ (no membership in any set, no adiabatic assumption):

U(p_{\mathrm{finish}})-U(p_{\mathrm{start}})=\bigl(U(p_{\mathrm{finish}})-U(p_{\mathrm{start}})+W(p)\bigr)-W(p),

where the bracket is the definition of the heat $Q_U(p)$ . The statement is an identity that follows from the definition of heat.

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

Clausius form of the first law: ΔU=Q−W\Delta U = Q - WΔU=Q−W

Clausius form of the first law: $\Delta U = Q - W$