$\mathcal D\ge0$ is the internal-energy Clausius–Duhem inequality

Proved

ClausiusDuhem.dissipation_nonneg_iff

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

continuum-mechanicsmathematical-physicsthermodynamics

For any thermomechanical process, define the dissipation

\mathcal D=\rho\,(T\dot\eta-\dot e)+\boldsymbol\sigma:\nabla\mathbf v-\frac{\mathbf q\cdot\nabla T}{T}.

Then $\mathcal D\ge0$ at every time and point if and only if, at every time and point,

\rho\,(\dot e-T\dot\eta)-\boldsymbol\sigma:\nabla\mathbf v\le-\frac{\mathbf q\cdot\nabla T}{T}.

This is why the Clausius–Duhem inequality is also called the dissipation inequality.

Preamble

import Definitions.Def_ClausiusDuhem_thermo_process

Formal statement

namespace ClausiusDuhem
theorem dissipation_nonneg_iff (P : ThermoProcess) :
    (∀ t x, 0 ≤ P.dissipation t x) ↔ P.InternalEnergyInequality := by sorry
end ClausiusDuhem

Source

Wikipedia, "Clausius–Duhem inequality", revision oldid=1182390552, https://en.wikipedia.org/w/index.php?title=Clausius%E2%80%93Duhem_inequality&oldid=1182390552, section "Dissipation".

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) - non-blind, same agent as the drafter

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statements, with full knowledge of the source article and of the intended meaning. It was not produced by a blind, independent auditor, so it must not be mistaken for independent testimony; reviewers should compare it against the Lean code themselves.

For every thermomechanical process $P=(\rho,\eta,v,q,s,T,e,\sigma)$ , with no hypotheses at all (no regularity, no sign of $T$ ), the following are equivalent:

for all $t,x$ : $0\le\mathcal D(t,x)$ , where $\mathcal D=\rho(T\dot\eta-\dot e)+\sigma:\nabla v-\dfrac{q\cdot\nabla T}{T}$ at $(t,x)$ ;
for all $t,x$ : $\rho(\dot e-T\dot\eta)-\sigma:\nabla v\le-\dfrac{q\cdot\nabla T}{T}$ at $(t,x)$ .

Material derivatives, gradients and $\nabla v$ are as in the field-calculus definitions (with the convention that non-existent derivatives are $0$ , and $/T=0$ where $T=0$ ; the equivalence holds regardless).

View graph

D≥0\mathcal D\ge0D≥0 is the internal-energy Clausius–Duhem inequality

$\mathcal D\ge0$ is the internal-energy Clausius–Duhem inequality