Incompressible flow: mass continuity reduces to $\nabla\cdot\mathbf u=0$

Proved

ContinuityEqWiki.div_velocity_eq_zero_of_incompressible

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

continuity-equationmathematical-physics

Let $\rho:\mathbb R\times\mathbb R^3\to\mathbb R$ be a fluid density, $C^1$ jointly in $(t,x)$ and strictly positive, and let $\mathbf u:\mathbb R\times\mathbb R^3\to\mathbb R^3$ be a flow velocity field with $\mathbf u(t,\cdot)$ of class $C^1$ for every $t$ . Suppose the mass continuity equation

\frac{\partial\rho}{\partial t}+\nabla\cdot(\rho\mathbf u)=0

holds everywhere, and that the flow is incompressible, i.e. the material derivative of the density vanishes:

\frac{\partial\rho}{\partial t}+\mathbf u\cdot\nabla\rho=0 .

Then the velocity field is divergence-free everywhere:

\nabla\cdot\mathbf u=0 .

This is the volume continuity equation of the source's Fluid dynamics section.

Formalization Note The source describes incompressibility parenthetically as "volumetric strain rate is zero". Taken literally that is already $\nabla\cdot\mathbf u=0$ , so incompressibility is encoded here by the standard condition $D\rho/Dt=0$ , which makes the reduction a real statement.

Preamble

import Mathlib
import Definitions.Def_ContinuityEqWiki_Defs

Formal statement

namespace ContinuityEqWiki

theorem div_velocity_eq_zero_of_incompressible (ρ : ℝ → Space → ℝ) (u : ℝ → Space → Space)
    (hρ : ContDiff ℝ 1 (Function.uncurry ρ)) (hu : ∀ t, ContDiff ℝ 1 (u t))
    (hpos : ∀ t x, 0 < ρ t x)
    (mass : ∀ t x, timeDeriv ρ t x + div (fun y => ρ t y • u t y) x = 0)
    (incompressible : ∀ t x, timeDeriv ρ t x + ∑ i, u t x i * partialDeriv i (ρ t) x = 0) :
    ∀ t x, div (u t) x = 0 := by sorry

end ContinuityEqWiki

Source

Wikipedia, "Continuity equation", revision oldid=1378634825, https://en.wikipedia.org/w/index.php?title=Continuity_equation&oldid=1378634825, section "Fluid dynamics" (mass continuity equation and the volume continuity equation for incompressible fluids)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) - drafting agent, non-blind read-back

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement it describes, at the explicit request of the proposal owner. Its author knew the source text and the intended meaning while writing it, so it must not be mistaken for a blind, independent audit. Reviewers should compare the Lean code against the source themselves.

Let $\rho:\mathbb R\times\mathbb R^3\to\mathbb R$ and $\mathbf u:\mathbb R\times\mathbb R^3\to\mathbb R^3$ . Assume:

$(t,x)\mapsto\rho(t,x)$ is $C^1$ on $\mathbb R\times\mathbb R^3$ ;
for every $t$ , $x\mapsto\mathbf u(t,x)$ is $C^1$ ;
$\rho(t,x)>0$ for all $t,x$ ;
for all $t,x$ : $\partial_t\rho(t,x)+\nabla\cdot\big(y\mapsto\rho(t,y)\,\mathbf u(t,y)\big)(x)=0$ ;
for all $t,x$ : $\partial_t\rho(t,x)+\sum_{i=0}^{2}\mathbf u(t,x)_i\,\partial_i\rho(t,\cdot)(x)=0$ .

Conclusion: for all $t,x$ , $\nabla\cdot\mathbf u(t,\cdot)(x)=\sum_{i}\partial_i\mathbf u(t,\cdot)_i(x)=0$ .

View graph

Incompressible flow: mass continuity reduces to ∇⋅u=0\nabla\cdot\mathbf u=0∇⋅u=0

Incompressible flow: mass continuity reduces to $\nabla\cdot\mathbf u=0$