Internal energy is unique up to an additive constant

Proved

FirstLawThermo.isInternalEnergy_unique_up_to_const

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 such that every state $A$ is linked to $O$ by an adiabatic process in $\mathcal P$ , going either from $O$ to $A$ or from $A$ to $O$ . If $U$ and $U'$ are both internal energies for $\mathcal P$ , then there is a constant $c\in\mathbb R$ with

U'(A)=U(A)+c\qquad\text{for every state }A.

Together with the previous milestone this says that internal energy is determined exactly up to an additive constant. It is "customarily stated relative to a conventionally chosen standard reference state of the system".

Formalization Note Only one direction of adiabatic accessibility is required for each state, in line with Münster's remark (quoted in the article) that it is not always possible to reach any state from any other by an adiabatic process.

Preamble

import Definitions.Def_FirstLawThermo_Defs
import Mathlib

open FirstLawThermo

Formal statement

theorem FirstLawThermo.isInternalEnergy_unique_up_to_const {σ : Type*}
    (procs : Set (Process σ)) (O : σ) (hlink : AdiabaticallyLinkedTo procs O)
    (U U' : σ → ℝ) (hU : IsInternalEnergy procs U) (hU' : 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 "Original statements: the thermodynamic approach": "It is defined only up to an arbitrary additive constant of integration ... The internal energy is customarily stated relative to a conventionally chosen standard reference state of the system."; Section "Evidence ...", subsection "Adiabatic processes" (adiabatic work from a reference state

O

to an arbitrary state

A

, or from

A

O

); Section "Various statements of the law for closed systems" (Münster 1970: not every state is adiabatically accessible from every other).

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 that for every $A\in\sigma$ there is a $p\in\mathcal P$ whose adiabatic proposition holds and which goes from $O$ to $A$ or from $A$ to $O$ (start/finish equal to these states). Let $U,U':\sigma\to\mathbb R$ both satisfy $V(p_{\mathrm{finish}})-V(p_{\mathrm{start}})=-W(p)$ for every $p\in\mathcal P$ whose adiabatic proposition holds ( $V=U$ and $V=U'$ ). Then there exists a real $c$ such that

U'(A)=U(A)+c\quad\text{for all }A\in\sigma.

No composition, null-process or path-independence assumption is made.

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