$d+1-\Delta_\pm=\Delta_\mp$

Proved

HolographicQuantumMatter.d_add_one_sub_delta

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

ads-cftholographymathematical-physics

Let $d\ge0$ and $m^2,L\in\mathbb R$ , and let $\Delta_\pm=\frac{d+1}{2}\pm\sqrt{\frac{(d+1)^2}{4}+m^2L^2}$ . Then

d+1-\Delta_+=\Delta_-\qquad\text{and}\qquad d+1-\Delta_-=\Delta_+ .

In the expansion (28) the source term scales as $r^{d+1-\Delta}$ and the response as $r^{\Delta}$ ; this identity says the two exponents are exactly $\Delta_-$ and $\Delta_+$ .

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. No bound on $m^2L^2$ is assumed: below the Breitenlohner–Freedman bound the square root takes Lean's junk value $0$ , and the identity still holds.

Preamble

import Mathlib
import Definitions.Def_HolographicQuantumMatter_ScalarAdS

Formal statement

namespace HolographicQuantumMatter

theorem d_add_one_sub_delta (d : ℕ) (msq L : ℝ) :
    ((d : ℝ) + 1) - deltaPlus d msq L = deltaMinus d msq L ∧
      ((d : ℝ) + 1) - deltaMinus d msq L = deltaPlus 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: "Note that

d+1-\Delta_\pm=\Delta_\mp

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$ , with $\Delta_\pm=\tfrac{d+1}{2}\pm\sqrt{\tfrac{(d+1)^2}{4}+m^2L^2}$ where $\sqrt{x}$ is the real square root with the convention $\sqrt{x}=0$ for $x<0$ , both $d+1-\Delta_+=\Delta_-$ and $d+1-\Delta_-=\Delta_+$ hold. There are no hypotheses.

View graph

d+1−Δ±=Δ∓d+1-\Delta_\pm=\Delta_\mpd+1−Δ±​=Δ∓​

$d+1-\Delta_\pm=\Delta_\mp$