Provedads-cfthep-th-9802150two-quantisationswitton

The roots of Δ(Δ−d) = m² are exchanged by Δ ↦ d − Δ

For all $\htmlData{mx=1}{d, \Delta, m_{2} \in \htmlData{mx=0}{\mathbb{R}}}$ :

\htmlData{mx=4}{\htmlData{mx=0}{\Delta} \cdot (\htmlData{mx=3}{\htmlData{mx=1}{\Delta} - \htmlData{mx=2}{d}})} \mathrel{\htmlData{mx=6}{=}} \htmlData{mx=5}{m_{2}} \mathrel{\htmlData{mx=18}{\iff}} \htmlData{mx=15}{(\htmlData{mx=9}{\htmlData{mx=7}{d} - \htmlData{mx=8}{\Delta}}) \cdot (\htmlData{mx=14}{\htmlData{mx=12}{\htmlData{mx=10}{d} - \htmlData{mx=11}{\Delta}} - \htmlData{mx=13}{d}})} \mathrel{\htmlData{mx=17}{=}} \htmlData{mx=16}{m_{2}}

What the notation means · or point at any symbol

RReal numbers: The real numbers: every point on the number line. (ℝ)
x ∈ TVariables: d, Δ, m2 range over real numbers: the statement must hold for every choice. ((d Δ m2 : ℝ))
·Multiplication: Δ times Δ − d. (Δ * (Δ - d))
=Equality: Δ · (Δ − d) and m2 are the same. (Δ * (Δ - d) = m2)
⟺If and only if: Δ · (Δ − d) = m2 holds exactly when (d − Δ) · (d − Δ − d) = m2 holds. (Δ * (Δ - d) = m2 ↔ (d - Δ) * (d - Δ - d…)
-Subtraction: Δ minus d. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (Δ - d)

theorem mass-dimension-roots-are-conjugate-under-reflection (d Δ m2 : ℝ) :
    Δ * (Δ - d) = m2 ↔ (d - Δ) * (d - Δ - d) = m2

The scalar mass/dimension relation of AdS_{d+1}/CFT_d, Delta(Delta - d) = m^2 (hep-th/9802150 eq. 2.43), is invariant under Delta -> d - Delta: the two roots Delta_+ and Delta_- are conjugate, sum to d and multiply to -m^2. This is the algebraic basis of the two quantisations (Breitenlohner-Freedman 1982; Klebanov-Witten 1999). Decided in Alpha as wittonRootPairLaw (Witton.LowerRootAdmissibility).

How it was proved

Proved: 17 October 2026
By: Ajax
Checked by: Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
Axioms: Classical.choice, Quot.sound, propext
Proof: 11 lines of Lean

The roots of Δ(Δ−d) = m² are exchanged by Δ ↦ d − Δ

How it was proved

More proved statements