Clausius–Duhem inequality in terms of specific internal energy

Proved

ClausiusDuhem.internal_energy_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 with $\rho,\eta,\mathbf v,\mathbf q,T,e$ jointly $C^1$ , $s$ jointly continuous and absolute temperature $T>0$ everywhere. Assume the differential Clausius–Duhem inequality $\rho\dot\eta\ge-\nabla\cdot(\mathbf q/T)+\rho s/T$ and the balance of energy

\rho\dot e-\boldsymbol\sigma:\nabla\mathbf v+\nabla\cdot\mathbf q-\rho s=0

at every time and point. Then 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 form incorporates the balance of energy into the Clausius–Duhem inequality and is the form used to restrict constitutive relations.

Preamble

import Definitions.Def_ClausiusDuhem_thermo_process

Formal statement

namespace ClausiusDuhem
theorem internal_energy_inequality (P : ThermoProcess) (hP : P.Smooth)
    (hT : ∀ t x, 0 < P.temp t x) (hEntropy : P.EntropyInequality)
    (hEnergy : P.EnergyBalance) :
    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 "Clausius–Duhem inequality in terms of specific internal energy" (statement and Proof).

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. Assume:

$\rho,\eta,v,q,T,e$ are jointly $C^1$ and $s$ is jointly continuous;
$T(t,x)>0$ for all $t,x$ ;
for all $t,x$ : $\rho\dot\eta\ge-\nabla\cdot(T^{-1}q)(t,\cdot)(x)+\rho s/T$ ;
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$ and $\sigma:\nabla v=\sum_{i,j}\sigma_{ij}(\nabla v)_{ij}$ , all spatial derivatives at fixed $t$ .

Conclusion: for all $t,x$ :

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

all quantities evaluated at $(t,x)$ . No conservation of mass and no integral inequality is assumed; no symmetry or regularity of $\sigma$ is assumed.

View graph