Seeliger's paradox: the Poisson equation (3) has no bounded potential for a uniform non-zero density

Proved

CosmoConstCentury.seeliger_poisson_no_bounded_potential

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

cosmologygeneral-relativitymathematical-physics

Let $G\neq0$ and let $\rho\neq0$ be a constant mass density filling all of Euclidean space $\mathbb R^3$ . Then the Poisson equation (3) of the review,

\nabla^2\Phi=4\pi G\rho\quad\text{on }\mathbb R^3,

has no solution $\Phi$ that is twice continuously differentiable and bounded.

This is the mathematical form of the difficulty noted by Seeliger: in an infinite, uniformly filled Newtonian universe the gravitational potential cannot be a finite, well-defined (bounded) function.

Preamble

import Mathlib
import Definitions.Def_CosmoConstCentury_Defs

open Filter Topology

Formal statement

namespace CosmoConstCentury

theorem seeliger_poisson_no_bounded_potential (G ρ : ℝ) (hG : G ≠ 0) (hρ : ρ ≠ 0) :
    ¬ ∃ Φ : EuclideanSpace ℝ (Fin 3) → ℝ, ContDiff ℝ 2 Φ ∧ (∃ M : ℝ, ∀ x, |Φ x| ≤ M) ∧
      ∀ x, laplacian3 Φ x = 4 * Real.pi * G * ρ := 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, eq. (3) and surrounding discussion.

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$ and $\rho$ be real numbers with $G\neq0$ and $\rho\neq0$ . The statement asserts that there is no function $\Phi:\mathbb R^3\to\mathbb R$ (on Euclidean three-space) satisfying all three of:

$\Phi$ is twice continuously differentiable on all of $\mathbb R^3$ ;
$\Phi$ is bounded: there is a real $M$ with $|\Phi(x)|\le M$ for every $x$ ;
for every $x\in\mathbb R^3$ , $\nabla^2\Phi(x)=4\pi G\rho$ , where $\nabla^2\Phi=\partial_1^2\Phi+\partial_2^2\Phi+\partial_3^2\Phi$ .

The right-hand side is the same constant at every point. No sign condition on $G$ or $\rho$ is imposed beyond both being non-zero. Unbounded solutions (such as quadratic polynomials) are not excluded by the statement.

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