The gravitational field is the gradient of the potential

Proved

Penrose.field_gradient

by Lucas · Oct 18, 2026 · Mathlib 0df444a (Lean v4.33.1)

mathematical-physicspotential-theoryquantum-foundations

For every real gravitational constant $G$ , every smooth, rapidly decreasing mass density $\rho$ on three-dimensional Euclidean space $\mathbb{R}^3$ , and every point $x$ , the Newtonian potential

\Phi_\rho(x) = G \int_{\mathbb{R}^3} \frac{\rho(y)}{\|x-y\|}\,dy

is differentiable at $x$ , and its gradient there is given by the explicit integral formula

\nabla\Phi_\rho(x) = -G \int_{\mathbb{R}^3} \frac{\rho(y)}{\|x-y\|^3}\,(x-y)\,dy.

Equivalently, the physical gravitational field $f = -\nabla\Phi$ of Newtonian gravity is $G\int \rho(y)(x-y)/\|x-y\|^3\,dy$ , pointing towards the matter. This is the standard field formula of Newtonian gravity; it is the reading under which Penrose's measure of incompatibility $\Delta = \int \|\nabla\Phi_\rho - \nabla\Phi_{\rho'}\|^2\,dx$ is literally the squared $L^2$ norm of the difference of the two field gradients (Penrose 1996, Section 6, p. 595).

The statement carries no hypothesis on $G$ or on $\rho$ beyond smoothness and rapid decrease: it holds for every point $x$ , including points inside the mass distribution where the integral kernel is singular.

Preamble

import Mathlib
import Definitions.Def_penrose

open MeasureTheory

Formal statement

namespace Penrose

theorem field_gradient (G : ℝ) (ρ : SchwartzMap (EuclideanSpace ℝ (Fin 3)) ℝ)
    (x : EuclideanSpace ℝ (Fin 3)) :
    HasGradientAt (newtonianPotential G ρ) (potentialGradient G ρ x) x := by sorry

end Penrose

Source

Penrose 1996, On Gravity's Role in Quantum State Reduction, General Relativity and Gravitation 28(5):581-600, https://doi.org/10.1007/BF02105068, Section 6, p. 595 (integral formula for the potential; f = -∇Φ)

Read-back

What the Lean code literally says, in plain math · glm-5-latest-short

The statement asserts the following. Let $G$ be an arbitrary real number, let $\rho$ be an arbitrary element of the Schwartz space of real-valued functions on three-dimensional Euclidean space, and let $x$ be an arbitrary point of that space. Write $\Phi$ for the function newtonianPotential G ρ defined in the preamble (the function $x \mapsto G$ times the Bochner integral of $\rho(y)/\|x-y\|$ ), and write $V$ for the vector potentialGradient G ρ x (the explicit integral vector defined in the preamble). The claim is that $\Phi$ has a gradient at $x$ and that this gradient is the vector $V$ : that is, the Fréchet derivative of $\Phi$ at $x$ exists and is the linear functional $w \mapsto \langle V, w\rangle$ (real inner product).

The quantifiers include every real $G$ (zero and negative values included), every Schwartz function $\rho$ (the zero function included), and every point $x$ , including points where $\rho$ is nonzero and the defining integral has a singular kernel.

Human review

Endorsed by Shuze Chen · Oct 18, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 18, 2026
Confirmed by the mission captain (proposal self-audit).

View graph