$r^{2-n}$ is harmonic away from the origin for $n>2$

Proved

TegmarkDimensionality.greens_function_harmonic

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

mathematical-physicspdepotential-theory

Let $n>2$ . The function $\phi(y)=|y|^{2-n}$ on $\mathbb R^n$ satisfies the Laplace equation at every point other than the origin:

\nabla^2\big(|y|^{2-n}\big)(x)=0\qquad\text{for all }x\in\mathbb R^n,\ x\neq0.

Up to a dimensional constant, $|y|^{2-n}$ is the potential of a point charge or point mass in $n$ space dimensions. The corresponding force decays like $r^{1-n}$ , so the inverse-square law of $n=3$ becomes an inverse-cube law for $n=4$ .

Formalization Note The statement records the harmonicity of $r^{2-n}$ away from the source. The distributional identity $\nabla^2 r^{2-n}=c_n\delta$ is not part of this milestone.

Preamble

import Mathlib
import Definitions.Def_tegmark_laplacian

Formal statement

namespace TegmarkDimensionality

/-- For `n > 2`, the potential `r^{2-n}` of a point source in `ℝⁿ` satisfies the Laplace
equation away from the source. -/
theorem greens_function_harmonic (n : ℕ) (hn : 2 < n)
    (x : EuclideanSpace ℝ (Fin n)) (hx : x ≠ 0) :
    laplacian (fun y : EuclideanSpace ℝ (Fin n) => ‖y‖ ^ ((2 : ℝ) - n)) x = 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. L70, first paragraph ('the fundamental Green's function of the Poisson equation ... is r^{2-n} for n > 2')

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>2$ , so $n\ge3$ , and let $x\in\mathbb R^n$ with $x\neq0$ . Define $f:\mathbb R^n\to\mathbb R$ by $f(y)=\|y\|^{2-n}$ , using the Euclidean norm and the real power with real exponent $2-n<0$ . At $y=0$ this real power evaluates to $0$ by Lean's convention. The theorem asserts

\nabla^2 f(x)=\sum_{i=1}^n D^2f(x)(e_i,e_i)=0,

i.e. the sum of the pure second derivatives of $f$ along the standard basis directions vanishes at $x$ .

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

r2−nr^{2-n}r2−n is harmonic away from the origin for n>2n>2n>2

$r^{2-n}$ is harmonic away from the origin for $n>2$