No stable orbits in the two-body problem for $n>3$

Proved

TegmarkDimensionality.no_stable_orbits_above_three_dims

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

classical-mechanicsmathematical-physics

Let $n>3$ be the number of space dimensions. Consider a particle of reduced mass $\mu>0$ moving in the attractive potential $V(r)=-k\,r^{2-n}$ , $k>0$ , with angular momentum $L\in\mathbb R$ . Its radial motion is governed by the effective potential

U(r)=\frac{L^2}{2\mu r^2}-k\,r^{2-n},\qquad r>0.

Then $U$ has no strict local minimum at any radius $r_0>0$ . In other words, there is no $r_0>0$ such that $U(r_0)<U(r)$ for all $r\neq r_0$ sufficiently close to $r_0$ .

Strict local minima of $U$ are exactly the stable circular orbits, so the two-body problem has no stable orbits when $n>3$ . This is in contrast with $n=3$ , treated in the next milestone.

Formalization Note A strict local minimum is used because for $n=4$ and $L^2=2\mu k$ the potential $U$ is constant, and every radius is then a non-strict, neutrally unstable critical point.

Preamble

import Mathlib
open Filter Topology

Formal statement

namespace TegmarkDimensionality

/-- For `n > 3` space dimensions the attractive two-body problem with potential
`-k r^{2-n}` has no stable orbit: the effective radial potential
`U(r) = L²/(2 μ r²) - k r^{2-n}` has no strict local minimum at any radius `r₀ > 0`. -/
theorem no_stable_orbits_above_three_dims (n : ℕ) (hn : 3 < n)
    (μ k L : ℝ) (hμ : 0 < μ) (hk : 0 < k) :
    ¬ ∃ r₀ : ℝ, 0 < r₀ ∧
      ∀ᶠ r in 𝓝[≠] r₀,
        L ^ 2 / (2 * μ * r₀ ^ 2) - k * r₀ ^ ((2 : ℝ) - n) <
          L ^ 2 / (2 * μ * r ^ 2) - k * r ^ ((2 : ℝ) - n) := 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. L70, first paragraph ('When n > 3, the two-body problem no longer has any stable orbits as solutions'), citing Büchel 1963 and Freeman 1969

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 $\mu,k,L$ be real numbers with $\mu>0$ and $k>0$ . $L$ is arbitrary and may be $0$ . For real $r$ put

U(r)=\frac{L^2}{2\mu r^2}-k\,r^{2-n},

with real-exponent power $r^{2-n}$ and Lean's convention that division by $0$ gives $0$ . The theorem asserts that there is no real $r_0>0$ for which $U(r_0)<U(r)$ holds for all $r$ in some punctured neighbourhood of $r_0$ , i.e. for all $r\neq r_0$ close enough to $r_0$ . Equivalently, $U$ has no strict local minimum at any positive point.

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 stable orbits in the two-body problem for n>3n>3n>3

No stable orbits in the two-body problem for $n>3$