Provedads-cftunitarity-boundtwo-quantisationshep-th-9802150

At the window's edge, 2Δ₋ = d − 2 exactly when m² = 1 − 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=9}{2\left(\htmlData{mx=8}{\htmlData{mx=1}{\frac{\htmlData{mx=0}{d}}{2}} - \htmlData{mx=7}{\sqrt{\htmlData{mx=6}{\htmlData{mx=4}{\frac{\htmlData{mx=3}{\htmlData{mx=2}{d}^{2}}}{4}} + \htmlData{mx=5}{m_{2}}}}}}\right)} \mathrel{\htmlData{mx=12}{=}} \htmlData{mx=11}{\htmlData{mx=10}{d} - 2} \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)
·Multiplication: 2 times d/2 − √(d^2/4 + m2). (2 * (d / 2 - Real.sqrt (d ^ 2 / 4 + m2)))
=Equality: 2 · (d/2 − √(d^2/4 + m2)) and d − 2 are the same. (2 * (d / 2 - Real.sqrt (d ^ 2 / 4 + m2)…)
⟺If and only if: 2 · (d/2 − √(d^2/4 + m2)) = d − 2 holds exactly when m2 = 1 − d^2/4 holds. (2 * (d / 2 - Real.sqrt (d ^ 2 / 4 + m2)…)
aᵇPower: d raised to the power 2. (d ^ 2)
-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)

theorem lower-root-at-window-edge-is-free-field-dimension (d m2 : ℝ) (hm : -(d ^ 2) / 4 ≤ m2) :
    2 * (d / 2 - Real.sqrt (d ^ 2 / 4 + m2)) = d - 2 ↔ m2 = 1 - d ^ 2 / 4

The lower root sits on the unitarity bound (the free-field dimension (d-2)/2) exactly at the top of the window, m^2 = 1 - d^2/4. For d = 4 this is m^2 = -3, Delta_- = 1: the 'k = 1' state of section 2.6 of hep-th/9802150, which the paper excludes by its bound (2.47) and which the strict unitarity bound excludes too. Decided in Alpha as wittonWindowEdgeLaw.

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

At the window's edge, 2Δ₋ = d − 2 exactly when m² = 1 − d²/4

How it was proved

More proved statements