The divergence of a curl vanishes: $\nabla\cdot(\nabla\times A)=0$

Proved

GaussMagnetism.div_curl_eq_zero

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

electromagnetismmathematical-physicsvector-calculus

Let $A:\mathbb R^3\to\mathbb R^3$ be a twice continuously differentiable vector field. Then for every $x\in\mathbb R^3$ ,

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

In particular, every magnetic field of the form $B=\nabla\times A$ satisfies Gauss's law for magnetism $\nabla\cdot B=0$ ; this is the easy direction of the equivalence between Gauss's law for magnetism and the existence of a vector potential.

Formalization Note $C^2$ regularity is stated as ContDiff ℝ 2 A.

Preamble

import Definitions.Def_GaussMagnetism_box_flux

open Larmor TongEM

Formal statement

namespace GaussMagnetism

theorem div_curl_eq_zero (A : Vec → Vec) (hA : ContDiff ℝ 2 A) (x : Vec) :
    divg (curl A) x = 0 := by sorry

end GaussMagnetism

Source

Wikipedia, "Gauss's law for magnetism" (uploaded PDF, 5 pp.), p. 2, section 'Vector potential' (Gauss's law for magnetism is equivalent to the existence of A with B = ∇×A); Wikipedia, "Maxwell's equations" (uploaded PDF, 24 pp.), p. 8, 'the div–curl identity' (section 'Charge conservation').

Read-back

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

Non-blind read-back. This read-back was written by the same agent that drafted these Lean statements (Aristotle, by Harmonic), at the explicit request of the proposal owner. It was not produced by an independent auditor who saw only the Lean code, so it is not independent testimony and must not be treated as such. Compare it with the Lean code directly.

Throughout, $\mathbb R^3$ is Euclidean three-space with coordinates $x=(x_0,x_1,x_2)$ and standard basis $e_0,e_1,e_2$ . For a vector field $F=(F_0,F_1,F_2):\mathbb R^3\to\mathbb R^3$ and a scalar field $\varphi:\mathbb R^3\to\mathbb R$ , $\partial_j$ is the partial derivative in the direction $e_j$ , $\nabla\cdot F=\partial_0F_0+\partial_1F_1+\partial_2F_2$ is the divergence, $\nabla\times F=(\partial_1F_2-\partial_2F_1,\ \partial_2F_0-\partial_0F_2,\ \partial_0F_1-\partial_1F_0)$ is the curl, and $\nabla\varphi=(\partial_0\varphi,\partial_1\varphi,\partial_2\varphi)$ is the gradient.

Statement. For every $C^2$ vector field $A:\mathbb R^3\to\mathbb R^3$ and every point $x\in\mathbb R^3$ , the divergence at $x$ of the vector field $\nabla\times A$ is zero:

\partial_0(\partial_1A_2-\partial_2A_1)(x)+\partial_1(\partial_2A_0-\partial_0A_2)(x)+\partial_2(\partial_0A_1-\partial_1A_0)(x)=0.

There are no other hypotheses. All partial derivatives are defined through the Fréchet derivative, which Lean sets to $0$ at points where the function is not differentiable; under the stated smoothness hypotheses this junk value never occurs.

View graph

The divergence of a curl vanishes: ∇⋅(∇×A)=0\nabla\cdot(\nabla\times A)=0∇⋅(∇×A)=0

The divergence of a curl vanishes: $\nabla\cdot(\nabla\times A)=0$