Prove2Me

The curl of a gradient vanishes: ∇×(∇φ)=0\nabla\times(\nabla\varphi)=0

Proved
GaussMagnetism.curl_grad_eq_zero

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

electromagnetismmathematical-physicsvector-calculus

Let φ:R3→R\varphi:\mathbb R^3\to\mathbb R be a twice continuously differentiable scalar field. Then for every x∈R3x\in\mathbb R^3,

∇×(∇φ)(x)=0.\nabla\times(\nabla\varphi)(x)=0.

This identity is what makes the magnetic vector potential non-unique: adding a gradient to a vector potential does not change its curl (gauge freedom).

Formalization Note C2C^2 regularity is stated as ContDiff ℝ 2 φ; grad is TongEM.grad and curl is Larmor.curl.

Preamble
import Definitions.Def_GaussMagnetism_box_flux

open Larmor TongEM
Formal statement
namespace GaussMagnetism

theorem curl_grad_eq_zero (φ : Vec → ℝ) (hφ : ContDiff ℝ 2 φ) (x : Vec) :
    curl (grad φ) x = 0 := by sorry

end GaussMagnetism
Source
Wikipedia, "Gauss's law for magnetism" (uploaded PDF, 5 pp.), p. 2, section 'Vector potential': 'since the curl of a gradient is the zero vector field'.
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, R3\mathbb R^3 is Euclidean three-space with coordinates x=(x0,x1,x2)x=(x_0,x_1,x_2) and standard basis e0,e1,e2e_0,e_1,e_2. For a vector field F=(F0,F1,F2):R3→R3F=(F_0,F_1,F_2):\mathbb R^3\to\mathbb R^3 and a scalar field φ:R3→R\varphi:\mathbb R^3\to\mathbb R, ∂j\partial_j is the partial derivative in the direction eje_j, ∇⋅F=∂0F0+∂1F1+∂2F2\nabla\cdot F=\partial_0F_0+\partial_1F_1+\partial_2F_2 is the divergence, ∇×F=(∂1F2−∂2F1, ∂2F0−∂0F2, ∂0F1−∂1F0)\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 ∇φ=(∂0φ,∂1φ,∂2φ)\nabla\varphi=(\partial_0\varphi,\partial_1\varphi,\partial_2\varphi) is the gradient.

Statement. For every function φ:R3→R\varphi:\mathbb R^3\to\mathbb R that is C2C^2 (twice continuously Fréchet differentiable) and every point x∈R3x\in\mathbb R^3, the curl of the vector field y↦∇φ(y)y\mapsto\nabla\varphi(y), evaluated at xx, is the zero vector:

(∂1∂2φ−∂2∂1φ, ∂2∂0φ−∂0∂2φ, ∂0∂1φ−∂1∂0φ)(x)=(0,0,0),\big(\partial_1\partial_2\varphi-\partial_2\partial_1\varphi,\ \partial_2\partial_0\varphi-\partial_0\partial_2\varphi,\ \partial_0\partial_1\varphi-\partial_1\partial_0\varphi\big)(x)=(0,0,0),

where ∂i∂jφ\partial_i\partial_j\varphi means ∂i\partial_i applied to the scalar field ∂jφ\partial_j\varphi. There are no other hypotheses. All partial derivatives are defined through the Fréchet derivative, which Lean sets to 00 at points where the function is not differentiable; under the stated smoothness hypotheses this junk value never occurs.

View graph