The measure as the self-energy double integral of the difference

Proved

Penrose.delta_double_integral

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

mathematical-physicspotential-theoryquantum-foundations

For two smooth, rapidly decreasing mass densities $\rho, \rho'$ on $\mathbb{R}^3$ and any real $G$ , Penrose's measure of incompatibility satisfies

\Delta(\rho,\rho') = 4\pi G^2 \iint_{\mathbb{R}^3\times\mathbb{R}^3} \frac{(\rho-\rho')(x)\,(\rho-\rho')(y)}{\|x-y\|}\,dx\,dy.

This is the final displayed formula of the chain in Section 6 of Penrose (1996, p. 595): substituting the integral formula for the potential into the pairing expresses $\Delta$ as $4\pi G^2$ times the double integral of the difference distribution against itself over the Newtonian kernel. The paper displays this formula with coefficient $-4\pi G$ ; under the sign convention that makes the first three steps of its chain verbatim, the correct coefficient is $+4\pi G^2$ — a sign and constant slip in the paper's display, documented in the mission description.

Up to the explicit constant, the right-hand side is the gravitational self-energy of the difference distribution — the content of the mission's goal theorem.

Preamble

import Mathlib
import Definitions.Def_penrose

open MeasureTheory

Formal statement

namespace Penrose

theorem delta_double_integral (G : ℝ) (ρ ρ' : SchwartzMap (EuclideanSpace ℝ (Fin 3)) ℝ) :
    deltaMeasure G ρ ρ'
      = 4 * Real.pi * G ^ 2
        * ∫ x, ∫ y, (⇑ρ x - ⇑ρ' x) * (⇑ρ y - ⇑ρ' y) / ‖x - y‖ ∂volume ∂volume := 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, final displayed formula Δ = -4πG∬(ρ-ρ')(ρ-ρ')/|x-y|d³xd³y (sign and constant corrected under the mission's convention; see mission description)

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 and $\rho, \rho'$ arbitrary Schwartz functions from three-dimensional Euclidean space to the reals. Let $\Delta$ be the preamble's deltaMeasure. The claim is the equality of real numbers

\Delta = 4\pi G^2 \iint \frac{\bigl(\rho(x)-\rho'(x)\bigr)\bigl(\rho(y)-\rho'(y)\bigr)}{\|x-y\|}\,dy\,dx,

a nested Bochner integral, the inner integral over $y$ , the outer over $x$ , both with respect to the standard volume on Euclidean three-space, and $\|x-y\|$ the Euclidean distance. The factor multiplying the double integral is $4\pi G^2$ : four, times the real number $\pi$ , times the square of $G$ . No hypotheses appear; the statement quantifies over all real $G$ and all Schwartz $\rho, \rho'$ .

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