Path-independent adiabatic work defines an internal energy

Proved

FirstLawThermo.exists_isInternalEnergy

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

first-lawinternal-energythermodynamics

Let $\mathcal P$ be a set of processes of a closed system with state set $\sigma$ , and let $O\in\sigma$ be a reference state. Assume

$\mathcal P$ is closed under sequential composition of consecutive stages;
$\mathcal P$ contains the null process at every state;
adiabatic work is path independent in $\mathcal P$ : adiabatic processes in $\mathcal P$ with the same initial and final states involve the same work;
every state $A$ is linked to $O$ by an adiabatic process in $\mathcal P$ , from $O$ to $A$ or from $A$ to $O$ .

Then there is a function $U:\sigma\to\mathbb R$ with $U(O)=0$ such that

U(p_{\mathrm{finish}})-U(p_{\mathrm{start}})=-W(p)\qquad\text{for every adiabatic }p\in\mathcal P.

This is the existence half of the statement that the net adiabatic work "determines a state function called internal energy, $U$ ". The normalization $U(O)=0$ fixes the arbitrary reference level at the reference state.

Preamble

import Definitions.Def_FirstLawThermo_Defs
import Mathlib

open FirstLawThermo

Formal statement

theorem FirstLawThermo.exists_isInternalEnergy {σ : Type*} (procs : Set (Process σ)) (O : σ)
    (hcomp : ClosedUnderComp procs) (hnull : ContainsNull procs)
    (hpath : AdiabaticWorkPathIndependent procs) (hlink : AdiabaticallyLinkedTo procs O) :
    ∃ U : σ → ℝ, IsInternalEnergy procs U ∧ U O = 0 := 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": "For all adiabatic processes between two specified states of a closed system of any nature, the net work done is the same regardless the details of the process, and determines a state function called internal energy, U."; also "In an adiabatic process, adiabatic work takes the system either from a reference state

O

with internal energy

U(O)

to an arbitrary one

A

with internal energy

U(A)

, or from the state

A

to the state

O

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

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

", and the discussion of "the time order of the stages, and their relative magnitudes".

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 set $\mathcal P$ of processes on $\sigma$ and a point $O\in\sigma$ , assume

for all $p,q\in\mathcal P$ with $p_{\mathrm{finish}}=q_{\mathrm{start}}$ , the process (start $p_{\mathrm{start}}$ , finish $q_{\mathrm{finish}}$ , work $W(p)+W(q)$ , adiabatic proposition " $p$ adiabatic and $q$ adiabatic") is in $\mathcal P$ ;
for every $A\in\sigma$ , the process (start $A$ , finish $A$ , work $0$ , adiabatic proposition True) is in $\mathcal P$ ;
any two $p,q\in\mathcal P$ whose adiabatic propositions hold and which have equal starts and equal finishes have $W(p)=W(q)$ ;
for every $A\in\sigma$ some $p\in\mathcal P$ whose adiabatic proposition holds goes from $O$ to $A$ or from $A$ to $O$ .

Then there exists $U:\sigma\to\mathbb R$ with $U(O)=0$ and

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

for every $p\in\mathcal P$ whose adiabatic proposition holds.

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