Charge conservation from Maxwell's equations: $\nabla\cdot\mathbf J+\partial_t\rho=0$

Proved

ContinuityEqWiki.charge_continuity_of_maxwell

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

continuity-equationmathematical-physics

Let $\mathbf H,\mathbf D,\mathbf J:\mathbb R\times\mathbb R^3\to\mathbb R^3$ and $\rho:\mathbb R\times\mathbb R^3\to\mathbb R$ be time-dependent fields. Assume that $\mathbf H(t,\cdot)$ is $C^2$ for every $t$ and that $\mathbf D$ is $C^2$ jointly in $(t,x)$ . Suppose Ampère's law with Maxwell's correction and Gauss's law hold everywhere:

\nabla\times\mathbf H=\mathbf J+\frac{\partial\mathbf D}{\partial t},\qquad \nabla\cdot\mathbf D=\rho .

Then the continuity equation for electric charge holds everywhere:

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

This is the statement that charge conservation is an automatic consequence of Maxwell's equations.

Preamble

import Mathlib
import Definitions.Def_ContinuityEqWiki_Defs

Formal statement

namespace ContinuityEqWiki

theorem charge_continuity_of_maxwell (H D J : ℝ → Space → Space) (ρ : ℝ → Space → ℝ)
    (hH : ∀ t, ContDiff ℝ 2 (H t)) (hD : ContDiff ℝ 2 (Function.uncurry D))
    (ampere : ∀ t x, curl (H t) x = J t x + timeDeriv D t x)
    (gauss : ∀ t x, div (D t) x = ρ t x) :
    ∀ t x, div (J t) x + timeDeriv ρ 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 "Electromagnetism", box "Consistency with Maxwell's equations"

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 $\mathbf H,\mathbf D,\mathbf J$ be arbitrary maps $\mathbb R\times\mathbb R^3\to\mathbb R^3$ and $\rho$ an arbitrary map $\mathbb R\times\mathbb R^3\to\mathbb R$ (written $f(t,x)$ ). Assume:

for every $t$ , $x\mapsto\mathbf H(t,x)$ is $C^2$ on $\mathbb R^3$ ;
$(t,x)\mapsto\mathbf D(t,x)$ is $C^2$ on $\mathbb R\times\mathbb R^3$ ;
for all $t,x$ : $\nabla\times\mathbf H(t,\cdot)(x)=\mathbf J(t,x)+\partial_t\mathbf D(t,x)$ , where $\partial_t\mathbf D(t,x)$ is the derivative of $s\mapsto\mathbf D(s,x)$ at $t$ ;
for all $t,x$ : $\nabla\cdot\mathbf D(t,\cdot)(x)=\rho(t,x)$ .

No regularity is assumed on $\mathbf J$ or $\rho$ separately. Conclusion: for all $t\in\mathbb R$ and $x\in\mathbb R^3$ ,

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

with $\nabla\cdot$ the sum of the three coordinate partial derivatives of the components and $\partial_t\rho(t,x)$ the derivative of $s\mapsto\rho(s,x)$ at $t$ .

View graph

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

Charge conservation from Maxwell's equations: $\nabla\cdot\mathbf J+\partial_t\rho=0$