Lemma 3 — $\Lambda<0$ : no vacuum solution spherically symmetric at infinity

Proved

FlatlyFoliated.lemma3_no_vacuum_negative_lambda

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

elliptic-pdegeneral-relativitymathematical-physics

Let $\Lambda<0$ . There is no pair of smooth fields $(\omega,\eta)$ on $\mathbb R^3$ with $\eta>0$ that solves the vacuum FFR equations (34)–(35) (with $\mu=0$ , $J=0$ ) and is spherically symmetric at infinity.

So existence fails when $\Lambda<0$ .

Preamble

import Mathlib
import Definitions.Def_FlatlyFoliatedRelativity_basic

open scoped ContDiff

Formal statement

namespace FlatlyFoliated

/-- Lemma 3: for `Λ < 0` there is no smooth vacuum solution with `η > 0` that is spherically
symmetric at infinity. -/
theorem lemma3_no_vacuum_negative_lambda (Λ : ℝ) (hΛ : Λ < 0) :
    ¬ ∃ (w : R3 → R3) (η : R3 → ℝ), ContDiff ℝ ∞ w ∧ ContDiff ℝ ∞ η ∧ (∀ x, 0 < η x) ∧
      FFREquations Λ 0 0 w η ∧ SphSymmAtInfty w η := by sorry

end FlatlyFoliated

Source

Bray, Hamm, Hirsch, Wheeler, Zhang, Flatly Foliated Relativity, arXiv:1911.00967v2, https://arxiv.org/abs/1911.00967, p. 20, Lemma 3 (eqs. (109)–(115))

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Lemma 3 — Λ<0\Lambda<0Λ<0: no vacuum solution spherically symmetric at infinity

Lemma 3 — $\Lambda<0$ : no vacuum solution spherically symmetric at infinity