Heat does not depend on the reference level of internal energy

Proved

FirstLawThermo.heat_add_const

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

first-lawinternal-energythermodynamics

Let $\sigma$ be the state set of a closed system, $U:\sigma\to\mathbb R$ a function, $c\in\mathbb R$ a constant and $p$ any process. Then

Q_{U+c}(p)=Q_U(p),

where $U+c$ denotes the function $A\mapsto U(A)+c$ .

Since the internal energy is only defined up to an additive constant, this shows that the heat, defined as a residual, is nevertheless a well-defined quantity attached to the process.

Preamble

import Definitions.Def_FirstLawThermo_Defs
import Mathlib

open FirstLawThermo

Formal statement

theorem FirstLawThermo.heat_add_const {σ : Type*} (U : σ → ℝ) (c : ℝ) (p : Process σ) :
    heat (fun A => U A + c) p = heat U p := 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" (internal energy defined only up to an additive constant); Section "Various statements of the law for closed systems" (heat defined as a residual difference between change of internal energy and work); Section "Definition": "Heat and work are said to be path dependent, while change in internal energy depends only on the initial and final states".

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 function $U:\sigma\to\mathbb R$ , a real $c$ and an arbitrary process $p$ :

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

No assumption is made on $U$ or $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