proofs
Provedads-cftunitarity-boundtwo-quantisationshep-th-9905104

The lower root Δ₋ = d/2 − √(d²/4 + m²) satisfies the unitarity bound 2Δ > d − 2 exactly when m² < 1 − d²/4

For all d,m2∈R\htmlData{mx=1}{d, m_{2} \in \htmlData{mx=0}{\mathbb{R}}}, if −d24≤m2\htmlData{mx=3}{\frac{\htmlData{mx=2}{-\htmlData{mx=1}{\htmlData{mx=0}{d}^{2}}}}{4}} \mathrel{\htmlData{mx=5}{\leq}} \htmlData{mx=4}{m_{2}}, then

d−2<2(d2−d24+m2)  ⟺  m2<1−d24\htmlData{mx=1}{\htmlData{mx=0}{d} - 2} \mathrel{\htmlData{mx=12}{<}} \htmlData{mx=11}{2\left(\htmlData{mx=10}{\htmlData{mx=3}{\frac{\htmlData{mx=2}{d}}{2}} - \htmlData{mx=9}{\sqrt{\htmlData{mx=8}{\htmlData{mx=6}{\frac{\htmlData{mx=5}{\htmlData{mx=4}{d}^{2}}}{4}} + \htmlData{mx=7}{m_{2}}}}}}\right)} \mathrel{\htmlData{mx=19}{\iff}} \htmlData{mx=13}{m_{2}} \mathrel{\htmlData{mx=18}{<}} \htmlData{mx=17}{1 - \htmlData{mx=16}{\frac{\htmlData{mx=15}{\htmlData{mx=14}{d}^{2}}}{4}}}
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 : ℝ))
−xNegation
The negative of d^2. (-(d ^ 2))
a/bDivision
−(d^2) divided by 4. In Lean, dividing by 0 gives 0. (-(d ^ 2) / 4)
≤At most
−(d^2)/4 is less than or equal to m2. (-(d ^ 2) / 4 ≤ m2)
-Subtraction
d minus 2. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (d - 2)
<Less than
d − 2 is strictly smaller than 2 · (d/2 − √(d^2/4 + m2)). (d - 2 < 2 * (d / 2 - Real.sqrt (d ^ 2 /…)
⟺If and only if
d − 2 < 2 · (d/2 − √(d^2/4 + m2)) holds exactly when m2 < 1 − d^2/4 holds. (d - 2 < 2 * (d / 2 - Real.sqrt (d ^ 2 /…)
aᵇPower
d raised to the power 2. (d ^ 2)
·Multiplication
2 times d/2 − √(d^2/4 + m2). (2 * (d / 2 - Real.sqrt (d ^ 2 / 4 + m2)))
√Square root
The non-negative number whose square is d^2/4 + m2. (Real.sqrt (d ^ 2 / 4 + m2))
+Addition
d^2/4 plus m2. (d ^ 2 / 4 + m2)

For m^2 >= -d^2/4 (the Breitenlohner-Freedman bound), the lower root of Delta(Delta - d) = m^2 obeys the scalar unitarity bound Delta > (d - 2)/2 (Klebanov-Witten, hep-th/9905104, eq. 2.8) if and only if m^2 < 1 - d^2/4. The window -d^2/4 <= m^2 < 1 - d^2/4 is where both quantisations exist; Witten's hep-th/9802150 keeps only the upper root (eq. 2.47). Decided in Alpha as wittonLowerRootWindowLaw.

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
19 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.

More proved statements