Hydrogen atom has no ground state for $n>3$

Proved

TegmarkDimensionality.hydrogen_energy_unbounded_below

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

mathematical-physicspdequantum-mechanics

Let $n>3$ and $\kappa>0$ , and if $n=4$ assume moreover $\kappa>1$ . In units with $\hbar^2/2m=1$ , the energy of a real state $\psi$ in the $n$ -dimensional Coulomb potential $-\kappa|x|^{2-n}$ is

\mathcal E[\psi]=\int_{\mathbb R^n}|\nabla\psi(x)|^2\,dx-\kappa\int_{\mathbb R^n}|x|^{2-n}\,\psi(x)^2\,dx.

This energy is unbounded below. For every $E\in\mathbb R$ there is a smooth, compactly supported $\psi$ with $\int\psi^2=1$ and

\mathcal E[\psi]<E.

So the $n$ -dimensional hydrogen atom has no ground state, but states of arbitrarily negative energy.

Formalization Note For $n\ge5$ the claim holds for every $\kappa>0$ . For $n=4$ the potential scales like the kinetic term, and by Hardy's inequality $\int|\nabla\psi|^2\ge\int\psi^2/|x|^2$ the energy is bounded below when $\kappa\le1$ . The four-dimensional case is therefore stated only for supercritical coupling $\kappa>1$ . This qualification is not in the paper.

Preamble

import Mathlib
open MeasureTheory
open scoped ContDiff

Formal statement

namespace TegmarkDimensionality

/-- For `n > 3` space dimensions, the hydrogen-like Schrödinger energy
`E[ψ] = ∫ |∇ψ|² - κ ∫ |x|^{2-n} ψ²` (Coulomb potential `-κ |x|^{2-n}` of `ℝⁿ`, units with
`ħ²/2m = 1`) is unbounded below on normalized smooth compactly supported states; for
`n = 4` this is asserted for supercritical coupling `κ > 1`. -/
theorem hydrogen_energy_unbounded_below (n : ℕ) (hn : 3 < n) (κ : ℝ) (hκ : 0 < κ)
    (hκ4 : n = 4 → 1 < κ) (E : ℝ) :
    ∃ ψ : EuclideanSpace ℝ (Fin n) → ℝ,
      ContDiff ℝ ∞ ψ ∧ HasCompactSupport ψ ∧ (∫ x, ψ x ^ 2) = 1 ∧
        (∫ x, ‖fderiv ℝ ψ x‖ ^ 2) - κ * (∫ x, ‖x‖ ^ ((2 : ℝ) - n) * ψ x ^ 2) < E := 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, first paragraph ('the hydrogen atom has no bound states for n > 3 ... no ground state, but time-dependent states of arbitrarily negative energy'), citing Tangherlini 1963

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$ , let $\kappa>0$ be real, assume that $n=4$ implies $\kappa>1$ , and let $E$ be any real number. The theorem asserts that there exists a function $\psi:\mathbb R^n\to\mathbb R$ such that:

$\psi$ is $C^\infty$ (infinitely differentiable, not necessarily analytic);
$\psi$ has compact support;
$\displaystyle\int_{\mathbb R^n}\psi(x)^2\,dx=1$ (Lebesgue measure);
$\displaystyle\int_{\mathbb R^n}\|D\psi(x)\|^2\,dx-\kappa\int_{\mathbb R^n}\|x\|^{2-n}\psi(x)^2\,dx<E$ .

Here $\|D\psi(x)\|$ is the operator norm of the derivative, which equals the Euclidean length of the gradient, and $\|x\|^{2-n}$ is the real power, equal to $0$ at $x=0$ by convention. The integrals are Bochner integrals and would be $0$ if an integrand were not integrable.

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

Hydrogen atom has no ground state for n>3n>3n>3

Hydrogen atom has no ground state for $n>3$