Continuity equation $\partial_t\rho+\nabla\cdot\mathbf J=0$ from Maxwell's equations

Proved

MaxwellWiki.continuity_equation

by Lucas · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

electromagnetismmaxwell-equationsvector-calculus

Charge conservation (differential form). Let $\varepsilon_0>0$ and $\mu_0>0$ . Let $\mathbf E,\mathbf B,\mathbf J:\mathbb{R}\times\mathbb{R}^3\to\mathbb{R}^3$ and $\rho:\mathbb{R}\times\mathbb{R}^3\to\mathbb{R}$ satisfy Maxwell's microscopic equations in SI units at every time and point,

\nabla\cdot\mathbf E=\frac{\rho}{\varepsilon_0},\qquad \nabla\cdot\mathbf B=0,\qquad \nabla\times\mathbf E=-\frac{\partial\mathbf B}{\partial t},\qquad \nabla\times\mathbf B=\mu_0\Big(\mathbf J+\varepsilon_0\frac{\partial\mathbf E}{\partial t}\Big),

and assume $\mathbf E$ and $\mathbf B$ are $C^2$ jointly in $(t,x)$ . Then for every $t$ and $x$ ,

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

This is the continuity equation the article derives "as a corollary of Maxwell's equations"; it expresses local conservation of electric charge.

Formalization Note No regularity is assumed on $\rho$ and $\mathbf J$ : they are determined by $\mathbf E$ and $\mathbf B$ through Gauss's law and the Ampère–Maxwell law. The $C^2$ assumption on $\mathbf E,\mathbf B$ makes explicit the smoothness the article leaves implicit.

Preamble

import Mathlib
import Definitions.Def_MaxwellWiki_Defs

open MaxwellWiki

Formal statement

namespace MaxwellWiki

theorem continuity_equation (ε₀ μ₀ : ℝ) (hε₀ : 0 < ε₀) (hμ₀ : 0 < μ₀)
    (E B J : ℝ → Vec3 → Vec3) (ρ : ℝ → Vec3 → ℝ)
    (hE : ContDiff ℝ 2 (Function.uncurry E)) (hB : ContDiff ℝ 2 (Function.uncurry B))
    (hM : IsMaxwellSolution ε₀ μ₀ E B J ρ) (t : ℝ) (x : Vec3) :
    timeDeriv ρ t x + div (J t) x = 0 := by sorry

end MaxwellWiki

Source

Wikipedia, "Maxwell's equations", https://en.wikipedia.org/wiki/Maxwell%27s_equations (24-page PDF snapshot supplied by the proposer), section "Charge conservation" (pp. 8–9 of the snapshot): the displayed chain

0=\nabla\cdot(\nabla\times\mathbf B)=\dots=\mu_0(\nabla\cdot\mathbf J+\partial\rho/\partial t)

, "i.e.,

\partial\rho/\partial t+\nabla\cdot\mathbf J=0

"; Maxwell's equations as in section "Summary — Microscopic version in SI units" (p. 2).

Read-back

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

Non-blind read-back. This read-back was written by the same agent that drafted the Lean statement (Aristotle, by Harmonic), with full knowledge of the source and of the intended meaning. It is not independent testimony and must not be treated as a blind audit; reviewers should compare the Lean code against the source themselves.

For all real numbers $\varepsilon_0>0$ and $\mu_0>0$ , all maps $\mathbf E,\mathbf B,\mathbf J:\mathbb{R}\to\mathrm{Vec3}\to\mathrm{Vec3}$ and $\rho:\mathbb{R}\to\mathrm{Vec3}\to\mathbb{R}$ such that

$(t,x)\mapsto\mathbf E(t,x)$ is $C^2$ on $\mathbb{R}\times\mathbb{R}^3$ ,
$(t,x)\mapsto\mathbf B(t,x)$ is $C^2$ on $\mathbb{R}\times\mathbb{R}^3$ ,
IsMaxwellSolution $(\varepsilon_0,\mu_0,\mathbf E,\mathbf B,\mathbf J,\rho)$ holds, i.e. for all $t,x$ : $\nabla\cdot\mathbf E(t,\cdot)(x)=\rho(t,x)/\varepsilon_0$ , $\nabla\cdot\mathbf B(t,\cdot)(x)=0$ , $\nabla\times\mathbf E(t,\cdot)(x)=-\partial_t\mathbf B(t,x)$ , $\nabla\times\mathbf B(t,\cdot)(x)=\mu_0\big(\mathbf J(t,x)+\varepsilon_0\partial_t\mathbf E(t,x)\big)$ ,

and for every $t\in\mathbb{R}$ , $x\in\mathrm{Vec3}$ :

\partial_t\rho(t,x)+\big(\nabla\cdot\mathbf J(t,\cdot)\big)(x)=0,

where $\partial_t\rho(t,x)$ is the derivative at $t$ of $s\mapsto\rho(s,x)$ (taken as $0$ where it does not exist) and divergence is as in the shared definition file. No regularity is assumed on $\rho$ or $\mathbf J$ . The hypotheses are satisfiable (e.g. all fields identically zero).

View graph

Continuity equation ∂tρ+∇⋅J=0\partial_t\rho+\nabla\cdot\mathbf J=0∂t​ρ+∇⋅J=0 from Maxwell's equations

Continuity equation $\partial_t\rho+\nabla\cdot\mathbf J=0$ from Maxwell's equations