Divergence-free smooth fields on $\mathbb R^3$ have a vector potential

Proved

GaussMagnetism.exists_vector_potential

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

electromagnetismmathematical-physicsvector-calculus

Let $B:\mathbb R^3\to\mathbb R^3$ be a smooth ( $C^\infty$ ) vector field satisfying Gauss's law for magnetism, $\nabla\cdot B=0$ everywhere on $\mathbb R^3$ . Then there exists a smooth vector field $A:\mathbb R^3\to\mathbb R^3$ , a magnetic vector potential, with

\nabla\times A(x)=B(x)\quad\text{for all }x\in\mathbb R^3.

This is the substantial direction of the equivalence between Gauss's law for magnetism and the existence of a vector potential.

Formalization Note Smoothness is TongEM.SmoothV (i.e. ContDiff ℝ ⊤ with ⊤ : ℕ∞). The whole space $\mathbb R^3$ is the domain; the result is false on general non-simply-shaped domains, which are not considered here.

Preamble

import Definitions.Def_GaussMagnetism_box_flux

open Larmor TongEM

Formal statement

namespace GaussMagnetism

theorem exists_vector_potential (B : Vec → Vec) (hB : SmoothV B)
    (hdiv : ∀ x, divg B x = 0) :
    ∃ A : Vec → Vec, SmoothV A ∧ ∀ x, curl A x = B x := by sorry

end GaussMagnetism

Source

Wikipedia, "Gauss's law for magnetism" (uploaded PDF, 5 pp.), p. 2, section 'Vector potential': 'Due to the Helmholtz decomposition theorem, Gauss's law for magnetism is equivalent to the following statement: There exists a vector field A such that B = ∇ × A.'

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. Let $B:\mathbb R^3\to\mathbb R^3$ be $C^\infty$ (infinitely continuously differentiable) and assume $\nabla\cdot B(x)=0$ for every $x\in\mathbb R^3$ . Then there exists a function $A:\mathbb R^3\to\mathbb R^3$ such that

$A$ is $C^\infty$ , and
$\nabla\times A(x)=B(x)$ for every $x\in\mathbb R^3$ .

No uniqueness, decay or boundary condition on $A$ is asserted. 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

Divergence-free smooth fields on R3\mathbb R^3R3 have a vector potential

Divergence-free smooth fields on $\mathbb R^3$ have a vector potential