Quasi-static adiabatic work through a reference state gives $-W_{A\to B}=U(B)-U(A)$

Proved

FirstLawThermo.quasiStatic_adiabatic_work_eq_neg_deltaU

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

first-lawinternal-energythermodynamics

Let $\sigma$ be a set of states of a closed system and let $W_{A\to B}$ denote the quasi-static adiabatic work done by the system in going from state $A$ to state $B$ . Fix a reference state $O$ and a function $U:\sigma\to\mathbb R$ . Assume

formula (1): $W_{A\to O}=-W_{O\to A}$ for every state $A$ ;
the work from $A$ to $B$ may be computed along a path through $O$ : $W_{A\to B}=W_{A\to O}+W_{O\to B}$ for all $A,B$ ;
$U(A)=U(O)-W_{O\to A}$ for every state $A$ .

Then for all states $A,B$ ,

-W_{A\to B}=U(B)-U(A).

This is the article's chain of equalities showing that quasi-static adiabatic work between any two states is a difference of values of the internal energy.

Formalization Note The quasi-static adiabatic work is modelled as a real-valued function of the pair of states, so its independence of the path is built into the representation.

Preamble

import Definitions.Def_FirstLawThermo_Defs
import Mathlib

open FirstLawThermo

Formal statement

theorem FirstLawThermo.quasiStatic_adiabatic_work_eq_neg_deltaU {σ : Type*}
    (W : σ → σ → ℝ) (U : σ → ℝ) (O : σ)
    (hrev : ∀ A : σ, W A O = -W O A)
    (hpath : ∀ A B : σ, W A B = W A O + W O B)
    (hU : ∀ A : σ, U A = U O - W O A) :
    ∀ A B : σ, -W A B = U B - U A := 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 "Evidence for the first law of thermodynamics for closed systems", subsection "Adiabatic processes": formula (1)

W^{\text{adiabatic, quasi-static}}_{A\to O}=-W^{\text{adiabatic, quasi-static}}_{O\to A}

, the definition

U(A)=U(O)-W^{\text{adiabatic}}_{O\to A}

, and the displayed chain

-W_{A\to B}=-W_{A\to O}-W_{O\to B}=W_{O\to A}-W_{O\to B}=-U(A)+U(B)=\Delta U

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$ (possibly empty), an arbitrary function $W:\sigma\times\sigma\to\mathbb R$ (written $W_{A\to B}$ ), an arbitrary function $U:\sigma\to\mathbb R$ and a point $O\in\sigma$ , assume

$W_{A\to O}=-W_{O\to A}$ for every $A\in\sigma$ ;
$W_{A\to B}=W_{A\to O}+W_{O\to B}$ for all $A,B\in\sigma$ ;
$U(A)=U(O)-W_{O\to A}$ for every $A\in\sigma$ .

Then for all $A,B\in\sigma$ ,

-W_{A\to B}=U(B)-U(A).

No notion of "process", "adiabatic" or "quasi-static" appears in the statement. $W$ is just a two-argument real function. Hypothesis 1 at $A=O$ forces $W_{O\to O}=0$ , and hypothesis 3 at $A=O$ is then automatic. The hypotheses are satisfiable, e.g. by $W\equiv 0$ and $U$ constant.

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

Quasi-static adiabatic work through a reference state gives −WA→B=U(B)−U(A)-W_{A\to B}=U(B)-U(A)−WA→B​=U(B)−U(A)

Quasi-static adiabatic work through a reference state gives $-W_{A\to B}=U(B)-U(A)$