Self-energy is invariant under translation of the mass distribution

Proved

Penrose.self_energy_translation

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

mathematical-physicspotential-theoryquantum-foundations

If a smooth, rapidly decreasing mass distribution $\rho'$ on $\mathbb{R}^3$ is a translate of $\rho$ , in the sense that for some vector $v$

\rho'(x) = \rho(x - v) \quad\text{for all } x,

then for any real $G$ the gravitational self-energies coincide:

E(\rho) = E(\rho'), \qquad E(\sigma) = -\frac{G}{2}\iint \frac{\sigma(x)\sigma(y)}{\|x-y\|}\,dx\,dy.

The kernel $1/\|x-y\|$ depends only on the difference $x-y$ , so the double integral is invariant under translating both arguments simultaneously. This is the structural fact behind the lump thought experiment of Section 2 of Penrose (1996, pp. 584–585): a rigid lump placed in two different locations gives two mass distributions that are translates of one another, so their individual gravitational self-energies are equal — the hypothesis under which the paper says either expression, the incompatibility measure or the interaction energy, determines the scale of the energy uncertainty (Section 6, p. 597).

Preamble

import Mathlib
import Definitions.Def_penrose
import Definitions.Def_penrose_energy

open MeasureTheory

Formal statement

namespace Penrose

theorem self_energy_translation (G : ℝ) (ρ ρ' : SchwartzMap (EuclideanSpace ℝ (Fin 3)) ℝ)
    (v : EuclideanSpace ℝ (Fin 3)) (h : ∀ x, ⇑ρ' x = ⇑ρ (x - v)) :
    gravSelfEnergy 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 2, pp. 584-585 (lump in two locations) and Section 6, p. 597 (equal individual self-energies)

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, \rho'$ be Schwartz functions from three-dimensional Euclidean space to the reals; let $v$ be a vector in that space. Suppose the hypothesis holds: for every point $x$ , the value $\rho'(x)$ equals the value $\rho(x - v)$ (subtraction in the Euclidean space). The conclusion is that the two real numbers gravSelfEnergy G ρ and gravSelfEnergy G ρ' are equal, where gravSelfEnergy G σ is the preamble's quantity $-(G/2)$ times the nested Bochner integral of $\sigma(x)\sigma(y)/\|x-y\|$ .

The hypothesis says precisely that $\rho'$ is the translate of $\rho$ by the vector $v$ . The quantifiers include the zero vector $v = 0$ (where the hypothesis forces $\rho = \rho'$ pointwise and the conclusion is trivial) and every real $G$ .

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