Newtonian limit (11) of Einstein's modified equations: a bounded potential exists iff $c^2\Lambda=4\pi G\rho$

Proved

CosmoConstCentury.einstein_newtonian_limit_bounded_iff

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

cosmologygeneral-relativitymathematical-physics

Let $G$ , $c$ , $\Lambda$ be real constants and let $\rho$ be a constant mass density on $\mathbb R^3$ . The Newtonian limit of Einstein's modified field equations is equation (11) of the review,

\nabla^2\phi+c^2\Lambda=4\pi G\rho .

This equation has a bounded, twice continuously differentiable solution $\phi$ on $\mathbb R^3$ if and only if

c^2\Lambda=4\pi G\rho .

Thus, unlike Seeliger's equation (4), equation (11) admits a finite potential for a uniform infinite distribution of matter only for one exact balance between the density and the cosmological constant; this is the discrepancy between (4) and (11) noted in Section 3.1.

Preamble

import Mathlib
import Definitions.Def_CosmoConstCentury_Defs

open Filter Topology

Formal statement

namespace CosmoConstCentury

theorem einstein_newtonian_limit_bounded_iff (G c Λ ρ : ℝ) :
    (∃ φ : EuclideanSpace ℝ (Fin 3) → ℝ, ContDiff ℝ 2 φ ∧ (∃ M : ℝ, ∀ x, |φ x| ≤ M) ∧
      ∀ x, laplacian3 φ x + c ^ 2 * Λ = 4 * Real.pi * G * ρ) ↔
    c ^ 2 * Λ = 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 3.1, p. 80, eq. (11) compared with eq. (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,c,\Lambda,\rho$ be arbitrary real numbers. The statement asserts the equivalence of:

there exists $\phi:\mathbb R^3\to\mathbb R$ (Euclidean three-space) that is twice continuously differentiable on all of $\mathbb R^3$ , bounded (some $M$ with $|\phi(x)|\le M$ for all $x$ ), and satisfies $\nabla^2\phi(x)+c^2\Lambda=4\pi G\rho$ for every $x$ , with $\nabla^2=\partial_1^2+\partial_2^2+\partial_3^2$ ;
$c^2\Lambda=4\pi G\rho$ .

The density is a single constant, not a function of position. No sign conditions are imposed on any of the constants.

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

Newtonian limit (11) of Einstein's modified equations: a bounded potential exists iff c2Λ=4πGρc^2\Lambda=4\pi G\rhoc2Λ=4πGρ

Newtonian limit (11) of Einstein's modified equations: a bounded potential exists iff $c^2\Lambda=4\pi G\rho$