Prove2Me

Poisson's equation: ∇2Φ=−4πGρ\nabla^2\Phi = -4\pi G\rho

Proved
Penrose.poisson_equation

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

mathematical-physicspotential-theoryquantum-foundations

For every real gravitational constant GG, every smooth, rapidly decreasing mass density ρ\rho on R3\mathbb{R}^3, and every point xx, the Laplacian of the Newtonian potential Φρ(x)=G∫ρ(y)/∥x−y∥ dy\Phi_\rho(x) = G\int \rho(y)/\|x-y\|\,dy satisfies

∇2Φρ(x)=−4πG ρ(x).\nabla^2\Phi_\rho(x) = -4\pi G\,\rho(x).

This is Poisson's equation for the Newtonian gravitational potential, the first displayed formula in the chain of Section 6 of Penrose (1996, p. 595), stated here under the sign convention fixed by the mission (∇2Φ=−4πGρ\nabla^2\Phi = -4\pi G\rho). The claim is pointwise, at every xx — including points carrying mass, where the potential kernel is singular — and requires no hypothesis beyond the smoothness and rapid decrease of ρ\rho.

Solving Poisson's equation is how the difference ∇2Φρ−∇2Φρ′=−4πG(ρ−ρ′)\nabla^2\Phi_\rho - \nabla^2\Phi_{\rho'} = -4\pi G(\rho - \rho') enters the computation of the incompatibility measure Δ\Delta.

Preamble
import Mathlib
import Definitions.Def_penrose

open MeasureTheory
Formal statement
namespace Penrose

theorem poisson_equation (G : ℝ) (ρ : SchwartzMap (EuclideanSpace ℝ (Fin 3)) ℝ)
    (x : EuclideanSpace ℝ (Fin 3)) :
    laplacian (newtonianPotential G ρ) x = -(4 * Real.pi) * G * ⇑ρ 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, Poisson's formula ∇²Φ = -4πGρ
Read-back

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

The statement asserts the following. Let GG be an arbitrary real number, ρ\rho an arbitrary Schwartz function from three-dimensional Euclidean space to the reals, and xx an arbitrary point. Let Φ\Phi be the Newtonian potential of ρ\rho as defined in the preamble (the Bochner integral of Gρ(y)/∥x−y∥G\rho(y)/\|x-y\|), and let the Laplacian be the preamble's laplacian: the sum, over the three standard basis vectors, of the second Fréchet derivative of the function at the point evaluated on that basis vector in both arguments. The claim is the equality of real numbers

∇2Φ(x)=−4π G ρ(x).\nabla^2\Phi(x) = -4\pi \, G \, \rho(x).

In particular the second Fréchet derivatives occurring on the left are asserted to exist as part of the claim. The statement covers every point xx and every real GG, including G=0G = 0 (where it reads ∇2Φ=0\nabla^2\Phi = 0 for the zero potential) and negative GG.

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