Gauge freedom: $\nabla\times(A+\nabla\varphi)=\nabla\times A$

Proved

GaussMagnetism.curl_add_grad

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 continuously differentiable vector field and $\varphi:\mathbb R^3\to\mathbb R$ a twice continuously differentiable scalar field. Then for every $x\in\mathbb R^3$ ,

\nabla\times(A+\nabla\varphi)(x)=\nabla\times A(x).

Consequently, if $A$ is a vector potential for a magnetic field $B$ (that is, $B=\nabla\times A$ ), then so is $A+\nabla\varphi$ for every such $\varphi$ ; this arbitrariness is called gauge freedom.

Formalization Note Regularity: $A$ is ContDiff ℝ 1, $\varphi$ is ContDiff ℝ 2.

Preamble

import Definitions.Def_GaussMagnetism_box_flux

open Larmor TongEM

Formal statement

namespace GaussMagnetism

theorem curl_add_grad (A : Vec → Vec) (φ : Vec → ℝ) (hA : ContDiff ℝ 1 A)
    (hφ : ContDiff ℝ 2 φ) (x : Vec) :
    curl (fun y => A y + grad φ y) x = curl A x := by sorry

end GaussMagnetism

Source

Wikipedia, "Gauss's law for magnetism" (uploaded PDF, 5 pp.), p. 2, section 'Vector potential': the identity for A + ∇φ and the paragraph on gauge freedom.

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 $A:\mathbb R^3\to\mathbb R^3$ be $C^1$ and $\varphi:\mathbb R^3\to\mathbb R$ be $C^2$ . Then for every $x\in\mathbb R^3$ , the curl at $x$ of the vector field $y\mapsto A(y)+\nabla\varphi(y)$ equals the curl of $A$ at $x$ :

\nabla\times(A+\nabla\varphi)(x)=\nabla\times A(x).

There are no other hypotheses; the claim is a pointwise equality of vectors in $\mathbb R^3$ for every $x$ . 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

Gauge freedom: ∇×(A+∇φ)=∇×A\nabla\times(A+\nabla\varphi)=\nabla\times A∇×(A+∇φ)=∇×A

Gauge freedom: $\nabla\times(A+\nabla\varphi)=\nabla\times A$