Breitenlohner–Freedman bound: real $\Delta$ iff $m^2L^2\ge-(d+1)^2/4$

Proved

HolographicQuantumMatter.breitenlohner_freedman_bound

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

ads-cftholographymathematical-physics

Let $d\ge0$ and $m^2,L\in\mathbb R$ . The mass–dimension relation (29) has a real solution $\Delta$ if and only if the Breitenlohner–Freedman bound holds:

\bigl(\exists\,\Delta\in\mathbb R:\ \Delta(\Delta-d-1)=m^2L^2\bigr)\iff m^2L^2\ge-\frac{(d+1)^2}{4}.

Equivalently, the scaling dimension becomes complex exactly when $m^2L^2<-D_{\rm eff}^2/4$ with $D_{\rm eff}=d+1$ (eq. (627) for AdS $_{d+2}$ , where $z=1$ ), which signals an instability.

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 breitenlohner_freedman_bound (d : ℕ) (msq L : ℝ) :
    (∃ Δ : ℝ, Δ * (Δ - ((d : ℝ) + 1)) = msq * L ^ 2) ↔
      -(((d : ℝ) + 1) ^ 2) / 4 ≤ msq * L ^ 2 := by sorry

end HolographicQuantumMatter

Source

Hartnoll, Lucas, Sachdev, *Holographic quantum matter*, arXiv:1612.07324v3, https://arxiv.org/abs/1612.07324, Section 6.2, p. 126, eq. (627), with

D_{\rm eff}=z+d

from eq. (103) at

z=1

; see also p. 15

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.

For every natural number $d$ and all reals $m^2$ (msq) and $L$ : there exists a real number $\Delta$ with $\Delta(\Delta-(d+1))=m^2L^2$ if and only if $-\tfrac{(d+1)^2}{4}\le m^2L^2$ . No hypotheses; $L=0$ and negative $L$ are allowed.

View graph

Breitenlohner–Freedman bound: real Δ\DeltaΔ iff m2L2≥−(d+1)2/4m^2L^2\ge-(d+1)^2/4m2L2≥−(d+1)2/4

Breitenlohner–Freedman bound: real $\Delta$ iff $m^2L^2\ge-(d+1)^2/4$