Theorem 2 — FFR equations ⟺ elliptic form

Proved

FlatlyFoliated.theorem2_equivalence

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

elliptic-pdegeneral-relativitymathematical-physics

Fix $\Lambda\in\mathbb R$ and smooth $\mu:\mathbb R^3\to\mathbb R$ , $J:\mathbb R^3\to\mathbb R^3$ , $\eta:\mathbb R^3\to\mathbb R$ with $\eta>0$ .

If smooth $(\omega,\eta)$ solve the FFR equations (34)–(35) and a smooth $f$ solves $\Delta f=\nabla\cdot\omega$ , then with $\zeta=\omega-df$ the triple $(f,\zeta,\eta)$ solves the elliptic form (39)–(41), including $\lim_{x\to\infty}\nabla\cdot\zeta=0$ .
Conversely, if smooth $(f,\zeta,\eta)$ solve (39)–(41) together with $\lim_{x\to\infty}\nabla\cdot\zeta=0$ , then $\omega=df+\zeta$ solves (34)–(35) and $\Delta f=\nabla\cdot\omega$ .

This is what allows the elliptic system to replace the original FFR equations.

Preamble

import Mathlib
import Definitions.Def_FlatlyFoliatedRelativity_basic

open scoped ContDiff

Formal statement

namespace FlatlyFoliated

/-- Theorem 2: equivalence of (34)–(35) (+ a solution of `Δf = ∇·ω`) with the elliptic
form (39)–(41) (+ `lim ∇·ζ = 0`), via `w = df + ζ`. -/
theorem theorem2_equivalence (Λ : ℝ) (μ : R3 → ℝ) (J : R3 → R3) (η : R3 → ℝ)
    (hμ : ContDiff ℝ ∞ μ) (hJ : ContDiff ℝ ∞ J) (hη : ContDiff ℝ ∞ η)
    (hηpos : ∀ x, 0 < η x) :
    (∀ (w : R3 → R3) (f : R3 → ℝ), ContDiff ℝ ∞ w → ContDiff ℝ ∞ f →
        FFREquations Λ μ J w η → (∀ x, lap f x = divg w x) →
        EllipticSystem Λ μ J f (fun x => w x - grad f x) η) ∧
    (∀ (f : R3 → ℝ) (ζ : R3 → R3), ContDiff ℝ ∞ f → ContDiff ℝ ∞ ζ →
        EllipticSystem Λ μ J f ζ η →
        FFREquations Λ μ J (fun x => grad f x + ζ x) η ∧
          ∀ x, lap f x = divg (fun y => grad f y + ζ y) x) := by sorry

end FlatlyFoliated

Source

Bray, Hamm, Hirsch, Wheeler, Zhang, Flatly Foliated Relativity, arXiv:1911.00967v2, https://arxiv.org/abs/1911.00967, p. 10, Theorem 2 (equations (34), (35), (37)–(41))

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