First law (mechanical approach): adiabatic work determines internal energy, unique up to a constant

Proved

FirstLawThermo.first_law_internal_energy

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 done by the system;
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 an internal energy $U:\sigma\to\mathbb R$ for $\mathcal P$ , that is

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

any two internal energies $U,U'$ for $\mathcal P$ differ by a constant: there is $c\in\mathbb R$ with $U'(A)=U(A)+c$ for every state $A$ .

This is the first law of thermodynamics for closed systems in the mechanical approach (Bryan, Carathéodory, Born): the net work in adiabatic processes between two given states is the same regardless of the details of the process, and determines a state function, the internal energy, fixed up to an arbitrary additive constant.

Preamble

import Definitions.Def_FirstLawThermo_Defs
import Mathlib

open FirstLawThermo

Formal statement

theorem FirstLawThermo.first_law_internal_energy {σ : Type*} (procs : Set (Process σ)) (O : σ)
    (hcomp : ClosedUnderComp procs) (hnull : ContainsNull procs)
    (hpath : AdiabaticWorkPathIndependent procs) (hlink : AdiabaticallyLinkedTo procs O) :
    (∃ U : σ → ℝ, IsInternalEnergy procs U) ∧
      ∀ U U' : σ → ℝ, IsInternalEnergy procs U → IsInternalEnergy procs U' →
        ∃ c : ℝ, ∀ A : σ, U' A = U A + c := 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."; Section "Conceptually revised statement, according to the mechanical approach"; Section "Various statements of the law for closed systems" (Carathéodory 1909: internal energy is a function of state, changed by the amount of work done adiabatically); Section "Original statements: the thermodynamic approach" (defined only up to an arbitrary additive constant).

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, with 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 both of the following hold:

there exists $U:\sigma\to\mathbb R$ with $U(p_{\mathrm{finish}})-U(p_{\mathrm{start}})=-W(p)$ for every $p\in\mathcal P$ whose adiabatic proposition holds;
for all $U,U':\sigma\to\mathbb R$ that both have this property, there is a real $c$ with $U'(A)=U(A)+c$ for every $A\in\sigma$ .

Here $W(p)$ is the real number stored in the process $p$ as its work. The adiabatic label is an arbitrary proposition attached to each process. The type $\sigma$ is nonempty because the point $O$ is given.

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