Internal energy may be shifted by an arbitrary constant

Proved

FirstLawThermo.isInternalEnergy_add_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 $U:\sigma\to\mathbb R$ be an internal energy for $\mathcal P$ , i.e. $U(p_{\mathrm{finish}})-U(p_{\mathrm{start}})=-W(p)$ for every adiabatic $p\in\mathcal P$ . Then for every constant $c\in\mathbb R$ the function

A\longmapsto U(A)+c

is again an internal energy for $\mathcal P$ .

This is half of the statement that the internal energy is defined only up to an arbitrary additive constant, which can be adjusted to give an arbitrary reference zero level.

Preamble

import Definitions.Def_FirstLawThermo_Defs
import Mathlib

open FirstLawThermo

Formal statement

theorem FirstLawThermo.isInternalEnergy_add_const {σ : Type*} (procs : Set (Process σ))
    (U : σ → ℝ) (hU : IsInternalEnergy procs U) (c : ℝ) :
    IsInternalEnergy procs (fun 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": "Because of its definition in terms of increments, the value of the internal energy of a system is not uniquely defined. It is defined only up to an arbitrary additive constant of integration, which can be adjusted to give arbitrary reference zero levels."

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$ , a function $U:\sigma\to\mathbb R$ such that $U(p_{\mathrm{finish}})-U(p_{\mathrm{start}})=-W(p)$ for every $p\in\mathcal P$ whose adiabatic proposition holds, and any real $c$ : the function $A\mapsto U(A)+c$ also satisfies

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

for every $p\in\mathcal P$ whose adiabatic proposition holds. No assumption is made on $\mathcal P$ .

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