Mass–dimension relation $\Delta(\Delta-d-1)=(mL)^2$ (eq. 29)

Proved

HolographicQuantumMatter.power_law_solution_iff

by Lucas · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

ads-cftholographymathematical-physics

Let $d\ge 0$ be the number of boundary spatial dimensions, $L>0$ the AdS radius and $m^2\in\mathbb R$ the mass squared of a bulk scalar in Poincaré $\mathrm{AdS}_{d+2}$ . At zero frequency and zero momentum ( $\omega=k=0$ ) the radial equation (27) reads

\phi''(r)-\frac{d}{r}\,\phi'(r)-\frac{m^2L^2}{r^2}\,\phi(r)=0,\qquad r>0.

For every real exponent $\Delta$ , the power law $\phi(r)=r^{\Delta}$ solves this equation on $r>0$ if and only if

\Delta(\Delta-d-1)=m^2L^2 .

This is the relation (29) between the bulk mass and the scaling dimension $\Delta$ of the dual operator, obtained from the leading power behaviour of solutions near the boundary $r\to0$ .

Formalization Note The boundary theory has $d$ spatial dimensions (so the bulk is $\mathrm{AdS}_{d+2}$ ), following the source's convention. The bulk mass squared is a real parameter $m^2$ (called msq), allowed to be negative; the source writes $(mL)^2$ for $m^2L^2$ . Fields are real-valued functions of $r$ ; only their values on $r>0$ matter. The frequency/momentum terms are set to zero, which is where the power laws in (28) are exact solutions.

Preamble

import Mathlib
import Definitions.Def_HolographicQuantumMatter_ScalarAdS

Formal statement

namespace HolographicQuantumMatter

theorem power_law_solution_iff (d : ℕ) (msq L : ℝ) (hL : 0 < L) (Δ : ℝ) :
    IsRadialSolution d 0 0 msq L (fun r => r ^ Δ) ↔
      Δ * (Δ - ((d : ℝ) + 1)) = msq * L ^ 2 := by sorry

end HolographicQuantumMatter

Source

Hartnoll, Lucas, Sachdev, *Holographic quantum matter*, arXiv:1612.07324v3, https://arxiv.org/abs/1612.07324, Section 1.6.2, p. 10, eqs. (27)–(29)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) - drafting agent, non-blind

Non-blind read-back. This read-back is NOT independent testimony. It was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement, with full knowledge of the source and the intended meaning. Reviewers must not treat it as a blind audit; compare the Lean code against the source directly.

Fix a natural number $d$ , real numbers $m^2$ (written msq, any sign) and $L$ with $L>0$ , and a real number $\Delta$ . The statement asserts an equivalence between (i) and (ii):

the function $f(r)=r^{\Delta}$ (real power, only used for $r>0$ ) is twice continuously differentiable on the open half-line $(0,\infty)$ and, for every $r>0$ , satisfies $f''(r)-\frac{d}{r}f'(r)+\bigl(0^2-0^2-\frac{m^2L^2}{r^2}\bigr)f(r)=0$ , where $f'$ , $f''$ are the (total-function) first and second derivatives;
$\Delta\,(\Delta-(d+1))=m^2L^2$ .

Edge cases: $d=0$ is allowed; $\Delta=0$ is allowed (then $f\equiv1$ on $r>0$ ); the hypothesis $L>0$ is not needed for the equivalence to make sense, since $L$ only enters through $m^2L^2$ .

Human review

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

View graph

Mass–dimension relation Δ(Δ−d−1)=(mL)2\Delta(\Delta-d-1)=(mL)^2Δ(Δ−d−1)=(mL)2 (eq. 29)

Mass–dimension relation $\Delta(\Delta-d-1)=(mL)^2$ (eq. 29)