Prove2Me

Integration by parts: Δ=−∫(Φ−Φ′)(∇2Φ−∇2Φ′)\Delta = -\int(\Phi-\Phi')(\nabla^2\Phi-\nabla^2\Phi')

Proved
Penrose.delta_laplacian

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

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

satisfies the whole-space integration-by-parts identity

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

This is the second displayed step of the chain in Section 6 of Penrose (1996, p. 595). The boundary terms at infinity vanish because the difference potential and its gradient decay; for a difference distribution with nonzero total mass the difference potential decays only like 1/∥x∥1/\|x\|, so the decay is a genuine estimate, not an assumption.

Preamble
import Mathlib
import Definitions.Def_penrose

open MeasureTheory
Formal statement
namespace Penrose

theorem delta_laplacian (G : ℝ) (ρ ρ' : SchwartzMap (EuclideanSpace ℝ (Fin 3)) ℝ) :
    deltaMeasure G ρ ρ'
      = -∫ x, (newtonianPotential G ρ x - newtonianPotential G ρ' x)
            * laplacian (fun y => newtonianPotential G ρ y - newtonianPotential G ρ' y) 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, second displayed chain identity Δ = -∫(Φ-Φ')(∇²Φ-∇²Φ')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 deltaMeasure G ρ ρ' be the preamble's quantity: the Bochner integral over xx of the squared Euclidean norm of the difference of the two field-gradient vectors (each itself defined as an explicit integral). Let Φ,Φ′\Phi, \Phi' denote the two potentials (newtonianPotential G ρ and newtonianPotential G ρ') and let uu be their pointwise difference, the function y↦Φ(y)−Φ′(y)y \mapsto \Phi(y) - \Phi'(y). The claim is the equality of real numbers

Δ=−∫(Φ(x)−Φ′(x))⋅∇2u(x) dx,\Delta = -\int \bigl(\Phi(x) - \Phi'(x)\bigr)\cdot \nabla^2 u(x)\, dx,

where ∇2u(x)\nabla^2 u(x) is the preamble's laplacian of the pointwise difference function at xx (sum of second directional derivatives along the standard basis). The Laplacian is applied to the difference function, not to each potential separately. No hypotheses appear; GG, ρ\rho, ρ′\rho' are universally quantified.

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