Prove2Me

Penrose's criterion: Δ\Delta is the self-energy of the difference distribution

Proved
Penrose.delta_self_energy

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

mathematical-physicspotential-theoryquantum-foundations

For any real gravitational constant GG and any two smooth, rapidly decreasing mass distributions ρ,ρ′\rho, \rho' on three-dimensional Euclidean space, Penrose's measure of incompatibility

Δ(ρ,ρ′)=∫R3∥∇Φρ−∇Φρ′∥2 dx\Delta(\rho,\rho') = \int_{\mathbb{R}^3} \|\nabla\Phi_\rho - \nabla\Phi_{\rho'}\|^2\,dx

is the gravitational self-energy of the difference of the two mass distributions, up to the explicit constant −8πG-8\pi G:

Δ(ρ,ρ′)=−8πG E(ρ−ρ′),E(σ)=−G2∬σ(x)σ(y)∥x−y∥ dx dy.\Delta(\rho,\rho') = -8\pi G\, E(\rho - \rho'), \qquad E(\sigma) = -\frac{G}{2}\iint \frac{\sigma(x)\sigma(y)}{\|x-y\|}\,dx\,dy.

This is the central identification of Section 6 of Penrose (1996, pp. 595–597): the measure of incompatibility of the two superposed space-time geometries — the quantity whose order of magnitude, divided into ℏ\hbar, gives the lifetime T≃ℏ/EΔT \simeq \hbar/E_\Delta of the superposed state — is basically just the gravitational self-energy of the difference between the two mass distributions. The paper itself notes the constant is loose (apart from the factor 4π4\pi it makes no difference which expression is used); here the constant is made fully explicit, and the two sides are defined independently: an L2L^2 norm of a field difference on the left, a double integral of densities on the right.

The statement places no hypothesis on ρ,ρ′\rho, \rho' beyond smoothness and rapid decrease, and none on the sign of GG.

Preamble
import Mathlib
import Definitions.Def_penrose
import Definitions.Def_penrose_energy

open MeasureTheory
Formal statement
namespace Penrose

theorem delta_self_energy (G : ℝ) (ρ ρ' : SchwartzMap (EuclideanSpace ℝ (Fin 3)) ℝ) :
    deltaMeasure G ρ ρ' = -8 * Real.pi * G * gravSelfEnergy G (ρ - ρ') := 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, pp. 595-597 (basically just the gravitational self-energy of the difference between the mass distributions)
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 and ρ,ρ′\rho, \rho' arbitrary Schwartz functions from three-dimensional Euclidean space to the reals. Write ρ−ρ′\rho - \rho' for their difference in the Schwartz space (a pointwise difference). The claim is the equality of real numbers

Δ=−8πG⋅E(ρ−ρ′),\Delta = -8\pi G \cdot E(\rho - \rho'),

where Δ\Delta is deltaMeasure G ρ ρ', defined in the preamble as the Bochner integral over xx of the squared Euclidean norm of the difference of the two field-gradient vectors (each an explicit integral vector), and E(σ)E(\sigma) is gravSelfEnergy G σ, defined in the preamble as −(G/2)-(G/2) times the nested Bochner integral of σ(x)σ(y)/∥x−y∥\sigma(x)\sigma(y)/\|x-y\|.

The two sides are defined independently: no definition in the preamble identifies them. No hypotheses appear; the statement quantifies over every real GG (zero and negative included) and every pair of Schwartz densities (including ρ=ρ′\rho = \rho', where both sides are 00, and densities taking negative values).

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