Provedads-cftunitarity-boundhep-th-9802150witton

Witten's bound 2Δ ≥ d (eq. 2.47) admits the lower root only at the double root m² = −d²/4

For all $\htmlData{mx=1}{d, m_{2} \in \htmlData{mx=0}{\mathbb{R}}}$ , if $\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

\htmlData{mx=0}{d} \mathrel{\htmlData{mx=11}{\leq}} \htmlData{mx=10}{2\left(\htmlData{mx=9}{\htmlData{mx=2}{\frac{\htmlData{mx=1}{d}}{2}} - \htmlData{mx=8}{\sqrt{\htmlData{mx=7}{\htmlData{mx=5}{\frac{\htmlData{mx=4}{\htmlData{mx=3}{d}^{2}}}{4}} + \htmlData{mx=6}{m_{2}}}}}}\right)} \mathrel{\htmlData{mx=18}{\iff}} \htmlData{mx=12}{m_{2}} \mathrel{\htmlData{mx=17}{=}} \htmlData{mx=16}{\frac{\htmlData{mx=15}{-\htmlData{mx=14}{\htmlData{mx=13}{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)
⟺If and only if: d ≤ 2 · (d/2 − √(d^2/4 + m2)) holds exactly when m2 = −(d^2)/4 holds. (d ≤ 2 * (d / 2 - Real.sqrt (d ^ 2 / 4 +…)
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)))
-Subtraction: d/2 minus √(d^2/4 + m2). On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (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)
=Equality: m2 and −(d^2)/4 are the same. (m2 = -(d ^ 2) / 4)

theorem upper-root-bound-admits-lower-root-only-at-double-root (d m2 : ℝ) (hm : -(d ^ 2) / 4 ≤ m2) :
    d ≤ 2 * (d / 2 - Real.sqrt (d ^ 2 / 4 + m2)) ↔ m2 = -(d ^ 2) / 4

The bound Delta >= d/2 of hep-th/9802150 eq. (2.47) is satisfied by the lower root Delta_- = d/2 - sqrt(d^2/4 + m^2) exactly when the square root vanishes, i.e. at the Breitenlohner-Freedman bound where the two roots coincide. So (2.47) is the bound for the upper branch only, not the unitarity bound (d - 2)/2. Decided in Alpha as wittonUpperBoundExcludesLowerRoot.

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: 22 lines of Lean

Witten's bound 2Δ ≥ d (eq. 2.47) admits the lower root only at the double root m² = −d²/4

How it was proved

More proved statements