proofs
Provedads-cfthep-th-9802150sign-auditp-form

The p-form mass/dimension relation obtained from the radial exponent (hep-th/9802150, eq. 2.45 corrected)

For all d,p,Δ,m2∈R\htmlData{mx=1}{d, p, \Delta, m_{2} \in \htmlData{mx=0}{\mathbb{R}}}:

(d−p−Δ)⋅(d−p−Δ+2p−d)=m2  ⟺  (Δ−p)⋅(Δ+p−d)=m2\begin{aligned} & \htmlData{mx=16}{(\htmlData{mx=5}{\htmlData{mx=3}{\htmlData{mx=1}{d} - \htmlData{mx=2}{p}} - \htmlData{mx=4}{\Delta}}) \cdot (\htmlData{mx=15}{\htmlData{mx=13}{\htmlData{mx=10}{\htmlData{mx=8}{\htmlData{mx=6}{d} - \htmlData{mx=7}{p}} - \htmlData{mx=9}{\Delta}} + \htmlData{mx=12}{2\htmlData{mx=11}{p}}} - \htmlData{mx=14}{d}})} \mathrel{\htmlData{mx=18}{=}} \htmlData{mx=17}{m_{2}} \\ & \htmlData{mx=0}{\iff} \htmlData{mx=27}{(\htmlData{mx=21}{\htmlData{mx=19}{\Delta} - \htmlData{mx=20}{p}}) \cdot (\htmlData{mx=26}{\htmlData{mx=24}{\htmlData{mx=22}{\Delta} + \htmlData{mx=23}{p}} - \htmlData{mx=25}{d}})} \mathrel{\htmlData{mx=29}{=}} \htmlData{mx=28}{m_{2}} \end{aligned}
What the notation means · or point at any symbol
RReal numbers
The real numbers: every point on the number line. (ℝ)
x ∈ TVariables
d, p, Δ, m2 range over real numbers: the statement must hold for every choice. ((d p Δ m2 : ℝ))
=Equality
(d − p − Δ) · (d − p − Δ + 2 · p − d) and m2 are the same. ((d - p - Δ) * (d - p - Δ + 2 * p - d) =…)
⟺If and only if
(d − p − Δ) · (d − p − Δ + 2 · p − d) = m2 holds exactly when (Δ − p) · (Δ + p − d) = m2 holds. ((d - p - Δ) * (d - p - Δ + 2 * p - d) =…)
-Subtraction
d minus p. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (d - p)
+Addition
d − p − Δ plus 2 · p. (d - p - Δ + 2 * p)
·Multiplication
2 times p. (2 * p)

A p-form with boundary indices behaves as x0^alpha near the boundary of AdS_{d+1} with alpha(alpha + 2p - d) = m^2 (the Proca operator on x0^alpha), and the operator it couples to has dimension Delta = d - p - alpha. Eliminating alpha gives (Delta - p)(Delta + p - d) = m^2. Witten's (2.45) prints (Delta + p)(Delta + p - d) = m^2, the result of substituting into the scalar relation. This statement is the elimination step: the relation in alpha = d - p - Delta is equivalent to the corrected relation in Delta. Decided in Alpha as wittonFormMassRelationLaw (systems/witton/src/Witton/MassDimensionRoots.alpha, github.com/thomasdavis/alpha, branch witton-system).

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

More proved statements