Equal self-energies: $\Delta$ reduces to the interaction energy

Proved

Penrose.delta_interaction

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

mathematical-physicspotential-theoryquantum-foundations

Suppose two smooth, rapidly decreasing mass distributions $\rho, \rho'$ on $\mathbb{R}^3$ have equal gravitational self-energies, $E(\rho) = E(\rho')$ . Then for any real $G$ , Penrose's measure of incompatibility satisfies

\Delta(\rho,\rho') = 8\pi G\, I(\rho,\rho') - 16\pi G\, E(\rho),

where $I(\rho,\rho') = -G\iint \rho(x)\rho'(y)/\|x-y\|\,dx\,dy$ is the gravitational interaction energy of the two distributions.

This is the precise content of the remark in Section 6 of Penrose (1996, p. 597): apart from the factor $4\pi$ , it does not make any difference which expression is used, provided the two individual states under superposition each have the same gravitational self-energy — the measure $\Delta$ is then determined, up to the explicit constants, by the interaction energy together with the common self-energy. For the two locations of a displaced lump this hypothesis holds by translation invariance.

Preamble

import Mathlib
import Definitions.Def_penrose
import Definitions.Def_penrose_energy

open MeasureTheory

Formal statement

namespace Penrose

theorem delta_interaction (G : ℝ) (ρ ρ' : SchwartzMap (EuclideanSpace ℝ (Fin 3)) ℝ)
    (h : gravSelfEnergy G ρ = gravSelfEnergy G ρ') :
    deltaMeasure G ρ ρ'
      = 8 * Real.pi * G * interactionEnergy G ρ ρ'
        - 16 * 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, p. 597 (apart from the factor 4π it does not make any difference which expression is used)

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. Suppose the hypothesis holds: the real numbers gravSelfEnergy G ρ and gravSelfEnergy G ρ' are equal (both defined in the preamble as $-(G/2)$ times the respective nested double integrals of the density against itself over the kernel $1/\|x-y\|$ ). The conclusion is the equality of real numbers

\Delta = 8\pi G \cdot I - 16\pi G \cdot E,

where $\Delta$ is the preamble's deltaMeasure (the Bochner integral of the squared norm of the difference of the two field gradients), $I$ is interactionEnergy G ρ ρ' (defined as $-G$ times the nested double integral of $\rho(x)\rho'(y)/\|x-y\|$ ), and $E$ is gravSelfEnergy G ρ. The coefficients are eight times $\pi$ times $G$ and sixteen times $\pi$ times $G$ respectively.

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

Equal self-energies: Δ\DeltaΔ reduces to the interaction energy

Equal self-energies: $\Delta$ reduces to the interaction energy