Prove2Me

The incompatibility measure as the potential–density pairing

Proved
Penrose.delta_pairing

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 R3\mathbb{R}^3 and any real GG, Penrose's measure of incompatibility satisfies

Δ(ρ,ρ′)=4πG∫R3(Φρ−Φρ′)(x) (ρ−ρ′)(x) dx.\Delta(\rho,\rho') = 4\pi G \int_{\mathbb{R}^3} (\Phi_\rho - \Phi_{\rho'})(x)\,(\rho - \rho')(x)\,dx.

This is the third displayed step of the chain in Section 6 of Penrose (1996, p. 595): substituting Poisson's equation ∇2Φ=−4πGρ\nabla^2\Phi = -4\pi G\rho into the integration-by-parts identity expresses the incompatibility measure as 4πG4\pi G times the pairing of the potential difference with the density difference. Under the mission's sign convention this identity holds verbatim as displayed in the paper.

This is the step where the space-time quantity Δ\Delta first becomes a quantity of Newtonian potential theory.

Preamble
import Mathlib
import Definitions.Def_penrose

open MeasureTheory
Formal statement
namespace Penrose

theorem delta_pairing (G : ℝ) (ρ ρ' : SchwartzMap (EuclideanSpace ℝ (Fin 3)) ℝ) :
    deltaMeasure G ρ ρ'
      = 4 * Real.pi * G * ∫ x, (newtonianPotential G ρ x - newtonianPotential G ρ' x)
            * (⇑ρ x - ⇑ρ' x) ∂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, Δ = 4πG∫(Φ-Φ')(ρ-ρ')d³x
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. Let Δ\Delta be the preamble's deltaMeasure (the Bochner integral of the squared norm of the difference of the two field gradients), and let Φ,Φ′\Phi, \Phi' be the two potentials. The claim is the equality of real numbers

Δ=4πG∫(Φ(x)−Φ′(x))(ρ(x)−ρ′(x)) dx,\Delta = 4\pi G \int \bigl(\Phi(x) - \Phi'(x)\bigr)\bigl(\rho(x) - \rho'(x)\bigr)\,dx,

the integral being the Bochner integral over all of Euclidean three-space with respect to the standard volume. No hypotheses appear; the statement quantifies over all real GG and all Schwartz ρ,ρ′\rho, \rho', including cases where the two densities coincide (both sides are then the real number 00).

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