The two roots $\Delta_\pm$ of the mass–dimension relation

Proved

HolographicQuantumMatter.mass_dimension_roots

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

ads-cftholographymathematical-physics

Let $d\ge0$ , $L\in\mathbb R$ and $m^2\in\mathbb R$ satisfy $m^2L^2\ge-\frac{(d+1)^2}{4}$ . Define

\Delta_\pm=\frac{d+1}{2}\pm\sqrt{\frac{(d+1)^2}{4}+m^2L^2}.

Then for every real $\Delta$ ,

\Delta(\Delta-d-1)=m^2L^2\iff \Delta=\Delta_+\ \text{or}\ \Delta=\Delta_- .

The source notes that for a given bulk mass, (29) has two solutions $\Delta_\pm$ ; the larger one $\Delta_+$ is the dimension in standard quantization and $\Delta_-$ in alternate quantization.

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.

Preamble

import Mathlib
import Definitions.Def_HolographicQuantumMatter_ScalarAdS

Formal statement

namespace HolographicQuantumMatter

theorem mass_dimension_roots (d : ℕ) (msq L : ℝ)
    (hBF : -(((d : ℝ) + 1) ^ 2) / 4 ≤ msq * L ^ 2) (Δ : ℝ) :
    Δ * (Δ - ((d : ℝ) + 1)) = msq * L ^ 2 ↔
      Δ = deltaPlus d msq L ∨ Δ = deltaMinus d msq L := 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 (text after eq. (30)) and p. 15 (alternate quantization)

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$ and reals $m^2$ (msq) and $L$ with $-\frac{(d+1)^2}{4}\le m^2L^2$ , and a real $\Delta$ . With $s=\sqrt{\tfrac{(d+1)^2}{4}+m^2L^2}$ (the radicand is $\ge0$ by the hypothesis, so no junk value of the square root arises), $\Delta_+=\tfrac{d+1}{2}+s$ and $\Delta_-=\tfrac{d+1}{2}-s$ , the statement asserts

\Delta(\Delta-(d+1))=m^2L^2\iff(\Delta=\Delta_+\ \text{or}\ \Delta=\Delta_-).

No sign condition on $L$ is imposed; at equality in the hypothesis $\Delta_+=\Delta_-=\tfrac{d+1}{2}$ .

View graph

The two roots Δ±\Delta_\pmΔ±​ of the mass–dimension relation

The two roots $\Delta_\pm$ of the mass–dimension relation