Differential form $\rho\dot\eta\ge-\nabla\cdot(\mathbf q/T)+\rho s/T$

Proved

ClausiusDuhem.entropy_inequality_of_local

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$ and $s$ jointly continuous. Assume that at every time and point

\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},

and that mass is conserved, $\dot\rho+\rho\,\nabla\cdot\mathbf v=0$ . Then at every time and point

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

This is the Clausius–Duhem inequality in differential form, expressed with the specific entropy.

Preamble

import Definitions.Def_ClausiusDuhem_thermo_process

Formal statement

namespace ClausiusDuhem
theorem entropy_inequality_of_local (P : ThermoProcess) (hP : P.Smooth)
    (hLocal : ∀ 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)
    (hMass : P.MassConservation) :
    P.EntropyInequality := 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", differential form and Proof, from "Expanding out" to the final display.

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$ in $(t,x)$ and $s$ is jointly continuous;
for all $t,x$ :

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

(time derivative of $\tau\mapsto\rho(\tau,x)\eta(\tau,x)$ ; divergences in space at fixed $t$ ); 3. for all $t,x$ : $\dot\rho+\rho\,\nabla\cdot v=0$ , where $\dot\rho=\partial_t\rho+\nabla\rho\cdot v$ .

Conclusion: for all $t,x$ :

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

with $\dot\eta=\partial_t\eta+\nabla\eta\cdot v$ . No positivity of $T$ (nor of $\rho$ ) is assumed; where $T=0$ , $T^{-1}$ and $/T$ evaluate to $0$ .

View graph

Differential form ρη˙≥−∇⋅(q/T)+ρs/T\rho\dot\eta\ge-\nabla\cdot(\mathbf q/T)+\rho s/Tρη˙​≥−∇⋅(q/T)+ρs/T

Differential form $\rho\dot\eta\ge-\nabla\cdot(\mathbf q/T)+\rho s/T$