Stable circular orbits exist for $n=3$

Proved

TegmarkDimensionality.stable_orbit_three_dims

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

classical-mechanicsmathematical-physics

Let $\mu>0$ , $k>0$ and $L\neq0$ . The effective potential of the three-dimensional Kepler problem,

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

has a strict local minimum at some $r_0>0$ . That is, there is $r_0>0$ with $U(r_0)<U(r)$ for all $r\neq r_0$ near $r_0$ .

So for $n=3$ the two-body problem has stable (circular, and nearby elliptic) orbits, unlike the case $n>3$ .

Preamble

import Mathlib
open Filter Topology

Formal statement

namespace TegmarkDimensionality

/-- In `n = 3` space dimensions, with the inverse-square attraction (potential `-k/r`) and
nonzero angular momentum, the effective radial potential `U(r) = L²/(2 μ r²) - k/r` has a
strict local minimum at some radius `r₀ > 0` (a stable circular orbit). -/
theorem stable_orbit_three_dims (μ k L : ℝ) (hμ : 0 < μ) (hk : 0 < k) (hL : L ≠ 0) :
    ∃ r₀ : ℝ, 0 < r₀ ∧
      ∀ᶠ r in 𝓝[≠] r₀,
        L ^ 2 / (2 * μ * r₀ ^ 2) - k / r₀ < L ^ 2 / (2 * μ * r ^ 2) - k / r := 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–L71 ('the familiar case, n = 3, which gives either stable elliptic orbits or non-bound parabolic and hyperbolic orbits')

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 $\mu,k,L$ be real numbers with $\mu>0$ , $k>0$ and $L\neq0$ . With $U(r)=\dfrac{L^2}{2\mu r^2}-\dfrac{k}{r}$ , using Lean's convention $x/0=0$ , the theorem asserts that there exists a real $r_0>0$ such that $U(r_0)<U(r)$ for every $r\neq r_0$ in some neighbourhood of $r_0$ . In other words, $U$ has a strict local minimum at some 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

Stable circular orbits exist for n=3n=3n=3

Stable circular orbits exist for $n=3$