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

The printed relation (Δ+p)(Δ+p−d) agrees with the corrected (Δ−p)(Δ+p−d) only for p = 0 or Δ = d − p

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

\begin{aligned} & \htmlData{mx=9}{(\htmlData{mx=3}{\htmlData{mx=1}{\Delta} + \htmlData{mx=2}{p}}) \cdot (\htmlData{mx=8}{\htmlData{mx=6}{\htmlData{mx=4}{\Delta} + \htmlData{mx=5}{p}} - \htmlData{mx=7}{d}})} \mathrel{\htmlData{mx=19}{=}} \htmlData{mx=18}{(\htmlData{mx=12}{\htmlData{mx=10}{\Delta} - \htmlData{mx=11}{p}}) \cdot (\htmlData{mx=17}{\htmlData{mx=15}{\htmlData{mx=13}{\Delta} + \htmlData{mx=14}{p}} - \htmlData{mx=16}{d}})} \\ & \htmlData{mx=0}{\iff} \htmlData{mx=20}{p} \mathrel{\htmlData{mx=21}{=}} 0 \mathbin{\htmlData{mx=27}{\lor}} \htmlData{mx=24}{\htmlData{mx=22}{\Delta} + \htmlData{mx=23}{p}} \mathrel{\htmlData{mx=26}{=}} \htmlData{mx=25}{d} \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, Δ range over real numbers: the statement must hold for every choice. ((d p Δ : ℝ))
·Multiplication: Δ + p times Δ + p − d. ((Δ + p) * (Δ + p - d))
=Equality: (Δ + p) · (Δ + p − d) and (Δ − p) · (Δ + p − d) are the same. ((Δ + p) * (Δ + p - d) = (Δ - p) * (Δ + …)
⟺If and only if: (Δ + p) · (Δ + p − d) = (Δ − p) · (Δ + p − d) holds exactly when p = 0 ∨ Δ + p = d holds. ((Δ + p) * (Δ + p - d) = (Δ - p) * (Δ + …)
+Addition: Δ plus p. (Δ + p)
-Subtraction: Δ + p minus d. On ℕ, Lean's subtraction stops at 0: 2 − 5 = 0. (Δ + p - d)
∨Or: At least one holds: p = 0, or Δ + p = d. (p = 0 ∨ Δ + p = d)

theorem witten-9802150-printed-pform-relation-agrees-only-at-massless-root (d p Δ : ℝ) :
    (Δ + p) * (Δ + p - d) = (Δ - p) * (Δ + p - d) ↔ p = 0 ∨ Δ + p = d

The two relations of eq. (2.45) of hep-th/9802150 (as printed, and as corrected) coincide exactly when p = 0 (the scalar case) or Delta + p = d (the massless root Delta = d - p, the one case the paper checks). In particular they disagree at the other root of m^2 = 0, Delta = p, and for every massive p-form with p > 0. Decided in Alpha as wittonPrintedFormMassRelationLaw (massless root 1, Delta = p root 0).

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

The printed relation (Δ+p)(Δ+p−d) agrees with the corrected (Δ−p)(Δ+p−d) only for p = 0 or Δ = d − p

How it was proved

More proved statements