Localization of the integral Clausius–Duhem inequality

Proved

ClausiusDuhem.local_of_integral

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 such that $\rho,\eta,\mathbf v,\mathbf q,T,e$ are $C^1$ jointly in $(t,x)$ , $s$ is jointly continuous, and $T>0$ everywhere. Suppose that for every non-degenerate closed box $\Omega=[a,b]\subset\mathbb R^3$ (a fixed control volume) and every time $t$ ,

\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.

Then at every time $t$ and every point $x$ ,

\frac{\partial}{\partial t}(\rho\eta)\ge-\nabla\cdot(\rho\eta\,\mathbf v)-\nabla\cdot\Big(\frac{\mathbf q}{T}\Big)+\frac{\rho s}{T}.

This is the step from the integral (global) statement of the second law to a pointwise statement.

Formalization Note Boxes serve as control volumes; their boundary integrals are sums of face integrals with outward normals $\pm\mathbf e_i$ .

Preamble

import Definitions.Def_ClausiusDuhem_thermo_process

Formal statement

namespace ClausiusDuhem
theorem local_of_integral (P : ThermoProcess) (hP : P.Smooth)
    (hT : ∀ t x, 0 < P.temp t x) (hInt : P.IntegralEntropyInequality) :
    ∀ t x, timeDeriv (fun τ y => P.rho τ y * P.eta τ y) t x ≥
      -div (fun y => (P.rho t y * P.eta t y) • P.vel t y) x
      - div (fun y => (P.temp t y)⁻¹ • P.heatFlux t y) x
      + P.rho t x * P.source t x / P.temp 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, section "Clausius–Duhem inequality in terms of the specific entropy", Proof, from "Assume that Ω is an arbitrary fixed control volume" to "Since Ω is arbitrary, we must have".

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

$\rho,\eta,v,q,T,e$ are jointly $C^1$ in $(t,x)$ and $s$ is jointly continuous ( $\sigma$ is unrestricted);
$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,

where $\Phi_{[a,b]}(F)=\sum_i\big(\int_{R_i}F_i|_{x_i=b_i}-\int_{R_i}F_i|_{x_i=a_i}\big)$ is the sum of signed face integrals over the six faces of the box (two-dimensional Lebesgue measure on each face rectangle $R_i$ ), and all fields are at time $t$ .

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

\partial_t(\rho\eta)(t,x)\ge-\nabla\cdot\big(y\mapsto\rho(t,y)\eta(t,y)v(t,y)\big)(x)-\nabla\cdot\big(y\mapsto T(t,y)^{-1}q(t,y)\big)(x)+\frac{\rho(t,x)s(t,x)}{T(t,x)},

where $\partial_t(\rho\eta)(t,x)$ is the derivative in $\tau$ at $t$ of $\tau\mapsto\rho(\tau,x)\eta(\tau,x)$ and the divergences are taken in $y$ with $t$ fixed. No conservation of mass or energy balance is assumed.

View graph