Prove2Me

Theorem 3 — Λ>0\Lambda>0 gives a geometric arrow of time

Proved
FlatlyFoliated.theorem3_arrow_of_time

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

elliptic-pdegeneral-relativitymathematical-physics

Let Λ>0\Lambda>0, let μ≥0\mu\ge0 and JJ be smooth, and let smooth (ω,η)(\omega,\eta) with η>0\eta>0 solve the FFR equations (34)–(35). Then the mean curvature K=(∇⋅ω)/ηK=(\nabla\cdot\omega)/\eta of the flat foliation has a constant strict sign on R3\mathbb R^3:

(∀x, ∇⋅ω(x)η(x)>0)  or  (∀x, ∇⋅ω(x)η(x)<0).\Big(\forall x,\ \frac{\nabla\cdot\omega(x)}{\eta(x)}>0\Big)\ \ \text{or}\ \ \Big(\forall x,\ \frac{\nabla\cdot\omega(x)}{\eta(x)}<0\Big).

Hence the direction of the mean curvature vector K⃗=Kn\vec K=Kn defines a geometrically preferred arrow of time.

Preamble
import Mathlib
import Definitions.Def_FlatlyFoliatedRelativity_basic

open scoped ContDiff
Formal statement
namespace FlatlyFoliated

/-- Theorem 3: for `Λ > 0`, every `μ ≥ 0` smooth solution has a mean curvature
`K = (∇·w)/η` of constant sign (the geometric arrow of time). -/
theorem theorem3_arrow_of_time (Λ : ℝ) (hΛ : 0 < Λ) (μ : R3 → ℝ) (J : R3 → R3)
    (w : R3 → R3) (η : R3 → ℝ) (hμ : ContDiff ℝ ∞ μ) (hJ : ContDiff ℝ ∞ J)
    (hw : ContDiff ℝ ∞ w) (hη : ContDiff ℝ ∞ η) (hμnn : ∀ x, 0 ≤ μ x)
    (hηpos : ∀ x, 0 < η x) (hsol : FFREquations Λ μ J w η) :
    (∀ x, 0 < divg w x / η x) ∨ (∀ x, divg w x / η x < 0) := by sorry

end FlatlyFoliated
Source
Bray, Hamm, Hirsch, Wheeler, Zhang, Flatly Foliated Relativity, arXiv:1911.00967v2, https://arxiv.org/abs/1911.00967, p. 12, Theorem 3 (eqs. (52)–(53))
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