No gravitational force in general relativity for $n<3$

Proved

TegmarkDimensionality.no_gravity_below_three_space_dims

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

general-relativitylinear-algebramathematical-physics

Let $n<3$ , so spacetime has dimension $n+1\le3$ . Let $g$ be a nondegenerate symmetric $(n+1)\times(n+1)$ real matrix (a metric at a point) and let $R_{abcd}$ be a real 4-index array with the algebraic symmetries of the Riemann tensor:

R_{abcd}=-R_{bacd}=-R_{abdc},\qquad R_{abcd}=R_{cdab},\qquad R_{abcd}+R_{acdb}+R_{adbc}=0.

If its Ricci contraction vanishes, $\sum_{a,c}(g^{-1})^{ac}R_{abcd}=0$ for all $b,d$ , then $R_{abcd}=0$ for all indices.

Vacuum solutions of Einstein's equations are Ricci-flat. So when $n<3$ they are flat at every point, there are no tidal forces, and matter exerts no gravitational force on distant test particles.

Formalization Note The statement is pointwise and purely algebraic. It formalizes the curvature-algebra fact behind the paper's remark.

Preamble

import Mathlib

Formal statement

namespace TegmarkDimensionality

/-- In a spacetime of dimension `n + 1` with `n < 3` space dimensions, every tensor
`R_{abcd}` with the algebraic symmetries of the Riemann tensor whose Ricci contraction
with respect to a nondegenerate symmetric metric `g` vanishes is identically zero
(vacuum general relativity has no curvature, hence no gravitational force). -/
theorem no_gravity_below_three_space_dims (n : ℕ) (hn : n < 3)
    (g : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ) (hg : g.IsSymm) (hdet : g.det ≠ 0)
    (R : Fin (n + 1) → Fin (n + 1) → Fin (n + 1) → Fin (n + 1) → ℝ)
    (hR₁ : ∀ a b c d, R a b c d = -R b a c d)
    (hR₂ : ∀ a b c d, R a b c d = -R a b d c)
    (hR₃ : ∀ a b c d, R a b c d = R c d a b)
    (hBianchi : ∀ a b c d, R a b c d + R a c d b + R a d b c = 0)
    (hRicci : ∀ b d, ∑ a, ∑ c, g⁻¹ a c * R a b c d = 0) :
    ∀ a b c d, R a b c d = 0 := by sorry

end TegmarkDimensionality

Source

M. Tegmark, *On the dimensionality of spacetime*, Class. Quantum Grav. 14 (1997) L69–L75, https://doi.org/10.1088/0264-9381/14/4/002, p. L71, second paragraph ('there is no gravitational force in general relativity with n < 3'), citing Misner–Thorne–Wheeler p. 1205 and Deser–Jackiw–'t Hooft 1984

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

NON-BLIND READ-BACK — NOT INDEPENDENT TESTIMONY. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement below, with full knowledge of the source paper and of the intended meaning. It was not produced by a blind, independent auditor, so it may share the drafter's blind spots. Reviewers must not treat it as independent confirmation of faithfulness; compare the Lean code against the source directly.

Let $n$ be a natural number with $n<3$ , and let $D=n+1\in\{1,2,3\}$ . Let $g$ be a real $D\times D$ matrix that is symmetric and has nonzero determinant, and let $R:\{1..D\}^4\to\mathbb R$ , $(a,b,c,d)\mapsto R_{abcd}$ . Assume, for all indices:

$R_{abcd}=-R_{bacd}$ ;
$R_{abcd}=-R_{abdc}$ ;
$R_{abcd}=R_{cdab}$ ;
$R_{abcd}+R_{acdb}+R_{adbc}=0$ ;
for all $b,d$ : $\displaystyle\sum_{a=1}^D\sum_{c=1}^D (g^{-1})_{ac}\,R_{abcd}=0$ , where $g^{-1}$ is the matrix inverse (it exists because $\det g\ne0$ ).

The theorem asserts $R_{abcd}=0$ for all $a,b,c,d$ .

Human review

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

View graph

No gravitational force in general relativity for n<3n<3n<3

No gravitational force in general relativity for $n<3$