Div–curl identity: $\nabla\cdot(\nabla\times F)=0$

Proved

MaxwellWiki.div_curl_eq_zero

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

electromagnetismmaxwell-equationsvector-calculus

Div–curl identity. Let $F:\mathbb{R}^3\to\mathbb{R}^3$ be a vector field of class $C^2$ . Then at every point $x\in\mathbb{R}^3$ ,

\nabla\cdot(\nabla\times F)(x)=0 .

This is the vector-calculus identity invoked in the Charge conservation section to show that the left-hand side $\nabla\times\mathbf B$ of the Ampère–Maxwell law has zero divergence.

Formalization Note $C^2$ regularity is assumed so that mixed second partial derivatives commute; divergence and curl are those of the shared definition file.

Preamble

import Mathlib
import Definitions.Def_MaxwellWiki_Defs

open MaxwellWiki

Formal statement

namespace MaxwellWiki

theorem div_curl_eq_zero (F : Vec3 → Vec3) (hF : ContDiff ℝ 2 F) (x : Vec3) :
    div (curl F) 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" (p. 8 of the snapshot): "The left-hand side of the Ampère–Maxwell law has zero divergence by the div–curl identity."

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 every map $F:\mathrm{Vec3}\to\mathrm{Vec3}$ (coordinate triples to coordinate triples) that is $C^2$ (twice continuously Fréchet-differentiable on all of $\mathbb{R}^3$ ), and for every point $x$ , the divergence of the curl of $F$ at $x$ equals $0$ :

\sum_{i=0}^{2}\partial_i\big[(\nabla\times F)_i\big](x)=0,

with $\partial_i$ , $\nabla\cdot$ and $\nabla\times$ exactly as in the shared definition file (Fréchet derivative applied to the basis vector $e_i$ ; curl components $\partial_1F_2-\partial_2F_1$ , $\partial_2F_0-\partial_0F_2$ , $\partial_0F_1-\partial_1F_0$ ). There are no other hypotheses.

View graph

Div–curl identity: ∇⋅(∇×F)=0\nabla\cdot(\nabla\times F)=0∇⋅(∇×F)=0

Div–curl identity: $\nabla\cdot(\nabla\times F)=0$