Faraday's law propagates $\nabla\cdot B=0$ from the initial time

Proved

GaussMagnetism.faraday_preserves_divg_B_eq_zero

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

electromagnetismmathematical-physicsvector-calculus

Let $E,B:\mathbb R\times\mathbb R^3\to\mathbb R^3$ be time-dependent electric and magnetic fields that are smooth jointly in time $t$ and position $x$ , and suppose they satisfy the Maxwell–Faraday law

\nabla\times E(t,\cdot)(x)=-\frac{\partial B}{\partial t}(t,x)\quad\text{for all }t\in\mathbb R,\ x\in\mathbb R^3.

If Gauss's law for magnetism holds at the initial time, $\nabla\cdot B(0,\cdot)(x)=0$ for all $x$ , then it holds at every time: $\nabla\cdot B(t,\cdot)(x)=0$ for all $t\in\mathbb R$ and $x\in\mathbb R^3$ .

This is the magnetic half of the redundancy of Maxwell's equations: a system satisfying Faraday's law automatically satisfies Gauss's law for magnetism, as long as the initial condition does.

Formalization Note Joint smoothness is TongEM.SmoothTV. The time derivative is Lean's deriv in $t$ at fixed $x$ . Divergence and curl act on the spatial variable only. Times $t<0$ are included.

Preamble

import Definitions.Def_GaussMagnetism_box_flux

open Larmor TongEM

Formal statement

namespace GaussMagnetism

theorem faraday_preserves_divg_B_eq_zero (E B : ℝ → Vec → Vec)
    (hE : SmoothTV E) (hB : SmoothTV B)
    (hfaraday : ∀ t x, curl (E t) x = -deriv (fun s => B s x) t)
    (hinit : ∀ x, divg (B 0) x = 0) :
    ∀ t x, divg (B t) x = 0 := by sorry

end GaussMagnetism

Source

Wikipedia, "Maxwell's equations" (uploaded PDF, 24 pp.), p. 16, section 'Overdetermination of Maxwell's equations': 'any system satisfying Faraday's law and Ampère's circuital law automatically also satisfies the two Gauss's laws, as long as the system's initial condition does' (magnetic part).

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 $E,B:\mathbb R\to(\mathbb R^3\to\mathbb R^3)$ , written $E(t,x)$ , $B(t,x)$ , be such that the maps $(t,x)\mapsto E(t,x)$ and $(t,x)\mapsto B(t,x)$ from $\mathbb R\times\mathbb R^3$ to $\mathbb R^3$ are $C^\infty$ . Assume:

for every $t\in\mathbb R$ and $x\in\mathbb R^3$ , the spatial curl of $E(t,\cdot)$ at $x$ equals $-\frac{d}{ds}\big|_{s=t}B(s,x)$ (the ordinary derivative in time of the vector $B(s,x)$ at fixed $x$ );
for every $x\in\mathbb R^3$ , the spatial divergence of $B(0,\cdot)$ at $x$ is $0$ .

Then for every $t\in\mathbb R$ (positive or negative) and every $x\in\mathbb R^3$ , the spatial divergence of $B(t,\cdot)$ at $x$ is $0$ . No relation to charge, current or the Ampère–Maxwell law is assumed. 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

Faraday's law propagates ∇⋅B=0\nabla\cdot B=0∇⋅B=0 from the initial time

Faraday's law propagates $\nabla\cdot B=0$ from the initial time