Prove2Me

Seeliger's modified Poisson equation (4): the unique bounded solution is the constant −4πGρ/λ-4\pi G\rho/\lambda

Proved
CosmoConstCentury.seeliger_modified_poisson_bounded_solution

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

cosmologygeneral-relativitymathematical-physics

Let λ>0\lambda>0 be Seeliger's decay constant, GG Newton's constant and ρ\rho a constant mass density on R3\mathbb R^3. Let Φ\Phi be a twice continuously differentiable, bounded function on R3\mathbb R^3. Then Φ\Phi solves the modified Poisson equation (4),

∇2Φ−λΦ=4πGρon R3,\nabla^2\Phi-\lambda\Phi=4\pi G\rho\quad\text{on }\mathbb R^3,

if and only if Φ\Phi is the constant function

Φ≡−4πGρλ.\Phi\equiv-\frac{4\pi G\rho}{\lambda}.

In contrast with equation (3), Seeliger's modification yields a well-defined potential for an infinite, uniformly filled universe, and this potential is unique among bounded functions.

Preamble
import Mathlib
import Definitions.Def_CosmoConstCentury_Defs

open Filter Topology
Formal statement
namespace CosmoConstCentury

theorem seeliger_modified_poisson_bounded_solution (G ρ lam : ℝ) (hlam : 0 < lam)
    (Φ : EuclideanSpace ℝ (Fin 3) → ℝ) (hΦ : ContDiff ℝ 2 Φ) (hbdd : ∃ M : ℝ, ∀ x, |Φ x| ≤ M) :
    (∀ x, laplacian3 Φ x - lam * Φ x = 4 * Real.pi * G * ρ) ↔
      ∀ x, Φ x = -(4 * Real.pi * G * ρ) / lam := by sorry

end CosmoConstCentury
Source
C. O'Raifeartaigh, M. O'Keeffe, W. Nahm, S. Mitton, "One hundred years of the cosmological constant: from 'superfluous stunt' to dark energy", Eur. Phys. J. H 43, 73-117 (2018), https://doi.org/10.1140/epjh/e2017-80061-7; Section 2, p. 75, eqs. (2) and (4).
Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Disclosure: non-blind read-back. This read-back was written by the same agent that drafted the Lean statement (Aristotle, by Harmonic), at the explicit request of the proposal owner. It is not an independent or blind audit, and it must not be treated as independent testimony: its author knew the source paper and the intended meaning while writing it. Reviewers should compare it against the Lean code themselves.

Let G,ρ,λG,\rho,\lambda be real numbers with λ>0\lambda>0 (GG and ρ\rho arbitrary, possibly zero). Let Φ:R3→R\Phi:\mathbb R^3\to\mathbb R be twice continuously differentiable on all of Euclidean three-space and bounded (there is MM with ∣Φ(x)∣≤M|\Phi(x)|\le M for all xx). Then the following are equivalent:

  1. for every x∈R3x\in\mathbb R^3: ∇2Φ(x)−λ Φ(x)=4πGρ\nabla^2\Phi(x)-\lambda\,\Phi(x)=4\pi G\rho, with ∇2=∂12+∂22+∂32\nabla^2=\partial_1^2+\partial_2^2+\partial_3^2;
  2. for every x∈R3x\in\mathbb R^3: Φ(x)=−4πGρλ\Phi(x)=-\dfrac{4\pi G\rho}{\lambda}.

Boundedness and C2C^2 regularity are hypotheses on Φ\Phi, so the equivalence says nothing about unbounded solutions. If Gρ=0G\rho=0 the constant is 00.

Human review

  • Endorsed by Shuze Chen · Oct 8, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 8, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph