Continuity equation ⇒ total mass is conserved

Proved

ConservationLaws.total_mass_conserved_of_continuity_equation

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

conservation-lawcontinuity-equationfluid-dynamicsmass

Let $\rho(t,x)$ be a mass density and $u(t,x)$ a velocity field on $\mathbb{R}^n$ , both continuously differentiable in $(t,x)$ , with $\rho(t,\cdot)$ vanishing outside a fixed ball for all $t$ . If the continuity equation

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

holds everywhere, then the total mass $\int_{\mathbb{R}^n}\rho(t,x)\,dx$ does not depend on $t$ .

Preamble

import Mathlib

Formal statement

namespace ConservationLaws

theorem total_mass_conserved_of_continuity_equation
    {n : ℕ} (ρ : ℝ → EuclideanSpace ℝ (Fin n) → ℝ)
    (u : ℝ → EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n))
    (hρ : ContDiff ℝ 1 (fun p : ℝ × EuclideanSpace ℝ (Fin n) => ρ p.1 p.2))
    (hu : ContDiff ℝ 1 (fun p : ℝ × EuclideanSpace ℝ (Fin n) => u p.1 p.2))
    (hsupp : ∃ R : ℝ, ∀ t x, R < ‖x‖ → ρ t x = 0)
    (hcont : ∀ t x, deriv (fun s => ρ s x) t +
      ∑ k : Fin n, fderiv ℝ (fun y => ρ t y * u t y k) x (EuclideanSpace.single k 1) = 0) :
    ∀ t s, ∫ x, ρ t x = ∫ x, ρ s x := by sorry

end ConservationLaws

Source

Wikipedia, "Conservation of mass" (uploaded PDF), https://en.wikipedia.org/wiki/Conservation_of_mass, section "Formulation and examples" (continuity equation in differential form and

dM/dt = 0

for the whole isolated system)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as drafter, non-blind

Disclosure: NON-BLIND read-back. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement, with full knowledge of the source material and of the intended meaning. It is not independent or blind testimony and must not be treated as such by any reviewer. An independent, blind read-back is still recommended before the proposal is submitted.

Fix a natural number $n$ . Let $\rho : \mathbb{R} \times \mathbb{R}^n \to \mathbb{R}$ (written $\rho(t,x)$ ) and $u : \mathbb{R} \times \mathbb{R}^n \to \mathbb{R}^n$ (written $u(t,x)$ , with components $u_k(t,x)$ , $k = 1,\dots,n$ ), where $\mathbb{R}^n$ is Euclidean space. Assume:

$(t,x) \mapsto \rho(t,x)$ is continuously differentiable ( $C^1$ ) jointly on $\mathbb{R}\times\mathbb{R}^n$ ;
$(t,x) \mapsto u(t,x)$ is $C^1$ jointly;
there is a real $R$ such that $\rho(t,x) = 0$ whenever $\|x\| > R$ , for all $t$ (if $R < 0$ this forces $\rho \equiv 0$ );
for all $t, x$ :

\frac{\partial\rho}{\partial t}(t,x) + \sum_{k=1}^n \frac{\partial}{\partial x_k}\big(\rho(t,\cdot)\,u_k(t,\cdot)\big)(x) = 0,

where $\partial/\partial t$ is the ordinary derivative of $s \mapsto \rho(s,x)$ at $t$ , and $\partial/\partial x_k$ is the derivative of $y \mapsto \rho(t,y)u_k(t,y)$ at $x$ applied to the $k$ -th standard basis vector. (These derivatives exist by 1–2.)

Conclusion: for all real $t, s$ ,

\int_{\mathbb{R}^n}\rho(t,x)\,dx = \int_{\mathbb{R}^n}\rho(s,x)\,dx,

with respect to Lebesgue measure on $\mathbb{R}^n$ . Edge case $n = 0$ : $\mathbb{R}^0$ is a point carrying measure $1$ , the sum is empty, and the hypothesis says $\rho$ is constant in $t$ . No sign condition on $\rho$ is assumed.

Human review

Endorsed by Shuze Chen · Oct 10, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 10, 2026
Confirmed by the mission captain (proposal self-audit).

View graph