In an adynamic process the heat supplied equals $\Delta U$

Proved

FirstLawThermo.heat_eq_deltaU_of_adynamic

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, and $p$ an adynamic process, i.e. one with no transfer of energy as work, $W(p)=0$ . Then the heat supplied to the system equals the increase of its internal energy:

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

This is the article's statement $Q^{\text{adynamic}}_{A\to B}=\Delta U$ , the observable aspect of the first law that concerns heat transfer and is measured by calorimetry.

Preamble

import Definitions.Def_FirstLawThermo_Defs
import Mathlib

open FirstLawThermo

Formal statement

theorem FirstLawThermo.heat_eq_deltaU_of_adynamic {σ : Type*} (U : σ → ℝ) (p : Process σ)
    (hp : p.IsAdynamic) :
    heat U p = U p.finish - U p.start := 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 "Adynamic processes": "When the system evolves with transfer of energy as heat, without energy being transferred as work, in an adynamic process, the heat transferred to the system is equal to the increase in its internal energy:

Q^{\text{adynamic}}_{A\to B}=\Delta U

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$ and an arbitrary process $p$ on $\sigma$ with $W(p)=0$ (no membership in any set and no internal-energy assumption on $U$ ):

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

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

In an adynamic process the heat supplied equals ΔU\Delta UΔU

In an adynamic process the heat supplied equals $\Delta U$