Clausius–Duhem (dissipation) inequality from the integral second law

Proved

ClausiusDuhem.dissipation_inequality

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

continuum-mechanicsmathematical-physicsthermodynamics

Let $(\rho,\eta,\mathbf v,\mathbf q,s,T,e,\boldsymbol\sigma)$ be a thermomechanical process on $\mathbb R^3$ : mass density, specific entropy, velocity, heat flux, energy source per unit mass, absolute temperature, specific internal energy and Cauchy stress. Assume

$\rho,\eta,\mathbf v,\mathbf q,T,e$ are $C^1$ jointly in $(t,x)$ and $s$ is jointly continuous;
$T>0$ everywhere;
the integral Clausius–Duhem inequality holds on every fixed control volume $\Omega$ (every non-degenerate closed box):

\frac{d}{dt}\int_\Omega\rho\eta\,dV\ge-\int_{\partial\Omega}\rho\eta\,\mathbf v\cdot\mathbf n\,dA-\int_{\partial\Omega}\frac{\mathbf q\cdot\mathbf n}{T}\,dA+\int_\Omega\frac{\rho s}{T}\,dV;

conservation of mass $\dot\rho+\rho\,\nabla\cdot\mathbf v=0$ ;
balance of energy $\rho\dot e-\boldsymbol\sigma:\nabla\mathbf v+\nabla\cdot\mathbf q-\rho s=0$ .

Then the dissipation is nonnegative at every time and every point:

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

This combines the article's three results: the integral second law implies the differential (entropy) form, which together with the balance of energy gives the internal-energy form, equivalently the dissipation inequality.

Formalization Note Control volumes are the non-degenerate closed boxes with fixed boundary ( $u_n=0$ ).

Preamble

import Definitions.Def_ClausiusDuhem_thermo_process

Formal statement

namespace ClausiusDuhem
theorem dissipation_inequality (P : ThermoProcess) (hP : P.Smooth)
    (hT : ∀ t x, 0 < P.temp t x) (hInt : P.IntegralEntropyInequality)
    (hMass : P.MassConservation) (hEnergy : P.EnergyBalance) :
    ∀ t x, 0 ≤ P.dissipation t x := 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, all sections: integral form (fixed control volume), differential form, internal-energy form, and "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.

Let $P=(\rho,\eta,v,q,s,T,e,\sigma)$ be any thermomechanical process (eight fields of $(t,x)\in\mathbb R\times\mathbb R^3$ ; $\sigma$ is $3\times3$ -matrix-valued). Assume:

$\rho,\eta,v,q,T,e$ are jointly $C^1$ in $(t,x)$ and $(t,x)\mapsto s(t,x)$ is continuous;
$T(t,x)>0$ for all $t,x$ ;
for all $a,b\in\mathbb R^3$ with $a_i<b_i$ ( $i=0,1,2$ ) and all $t$ :

\frac{d}{d\tau}\Big|_{t}\int_{[a,b]}\rho\eta\,dx\ge-\Phi_{[a,b]}(\rho\eta\,v)-\Phi_{[a,b]}(T^{-1}q)+\int_{[a,b]}\frac{\rho s}{T}\,dx,

with $\Phi_{[a,b]}(F)$ the sum over $i$ of the integral of $F_i$ over the face $x_i=b_i$ minus the integral of $F_i$ over the face $x_i=a_i$ (two-dimensional Lebesgue measure on each face), fields at time $t$ ; 4. for all $t,x$ : $\dot\rho+\rho\,\nabla\cdot v=0$ ; 5. for all $t,x$ : $\rho\dot e-\sigma:\nabla v+\nabla\cdot q-\rho s=0$ .

Here $\dot\varphi=\partial_t\varphi+\nabla\varphi\cdot v$ , $(\nabla v)_{ij}=\partial_jv_i$ , $\sigma:\nabla v=\sum_{i,j}\sigma_{ij}(\nabla v)_{ij}$ , spatial derivatives at fixed $t$ .

Conclusion: for every $t\in\mathbb R$ and $x\in\mathbb R^3$ ,

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

all quantities evaluated at $(t,x)$ .

View graph