Signature of the Regge colour factors: $P\,C_{ik}=(-1)^{k+1}C_{ik}$

Proved

NaculichRegge.regge_color_signature

by Lucas · Sep 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

color-algebramathematical-physicsscattering-amplitudes

For every admissible pair $(i,k)$ (eq. (4.25)), the Regge colour factor $C_{ik}$ has definite signature under the exchange of legs 2 and 3: it is odd when $k$ is even and even when $k$ is odd,

P\,C_{ik}=(-1)^{k+1}\,C_{ik}.

Preamble

import Definitions.Def_NaculichRegge_TraceBasis

open Polynomial

Formal statement

namespace NaculichRegge

/-- Naculich, Sec. 4.4 (below eq. (4.23)): the Regge colour factor `C_{ik}` has signature
`(−1)^{k+1}` under the exchange of legs 2 and 3. -/
theorem regge_color_signature (i k : ℕ) (h : IsReggeIndex i k) :
    crossing.mulVec (reggeColor i k) = ((-1 : ℂ[X]) ^ (k + 1)) • reggeColor i k := by sorry

end NaculichRegge

Source

S. G. Naculich, "All-loop-orders relation between Regge limits of N = 4 SYM and N = 8 supergravity four-point amplitudes", arXiv:2012.00030v2, https://arxiv.org/abs/2012.00030, p. 16, text below eq. (4.23)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; non-blind

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted these Lean statements, with full knowledge of the source paper and of the intended meaning; it was not produced by an independent, blind auditor. Reviewers must not treat it as independent evidence of faithfulness and should check it against the Lean code themselves.

For all natural numbers $i,k$ such that $(i,k)$ is admissible,

P\,C_{ik}=(-1)^{k+1}\,C_{ik},

where the scalar $(-1)^{k+1}$ is taken in $\mathbb C[N]$ and multiplies every component. Admissible pairs include $(0,0)$ (claim: $PC_{00}=-C_{00}$ ), $(1,1)$ , $(2,1),(2,2)$ and, for $i\ge3$ , $k\in\{1,i-1,i\}$ . No bound relative to a loop order is involved.

Definitions used. Throughout, $N$ denotes the polynomial variable $X$ of $\mathbb{C}[X]$ ; a colour vector is a column vector $v=(v_1,\dots,v_6)\in\mathbb{C}[X]^6$ (component $v_j$ is the coefficient of the trace-basis element $c[j]$ ), and a colour operator is a $6\times 6$ matrix over $\mathbb{C}[X]$ acting on column vectors by matrix–vector multiplication. $\mathbf T_t^2$ and $\mathbf T_{s-u}^2$ are the two fixed matrices

\mathbf T_t^2=\begin{pmatrix}N&0&0&0&0&-1\\0&2N&0&1&0&1\\0&0&N&-1&0&0\\0&2&0&2N&0&0\\-2&0&-2&0&0&0\\0&2&0&0&0&2N\end{pmatrix},\qquad \mathbf T_{s-u}^2=\begin{pmatrix}-\tfrac N2&0&0&0&-1&-\tfrac12\\0&0&0&-\tfrac12&0&\tfrac12\\0&0&\tfrac N2&\tfrac12&1&0\\0&1&2&N&0&0\\-1&0&1&0&0&0\\-2&-1&0&0&0&-N\end{pmatrix},

$C_{00}=(1,0,-1,0,0,0)^{T}$ , and $P$ ("crossing") is the permutation matrix exchanging coordinates $1\leftrightarrow 3$ and $4\leftrightarrow 6$ and fixing $2,5$ . With $[A,B]=AB-BA$ , the Regge colour factor $C_{ik}$ is $O_{ik}C_{00}$ , where $O_{ik}$ is: the identity if $i=0$ (for every $k$ ); otherwise $(\mathbf T_{s-u}^2)^i$ if $k=i$ ; otherwise $\mathrm{ad}_{\mathbf T_t^2}^{\,i-1}(\mathbf T_{s-u}^2)$ if $k=1$ ; otherwise $\mathrm{ad}_{\mathbf T_{s-u}^2}^{\,i-2}([\mathbf T_t^2,\mathbf T_{s-u}^2])$ if $k=i-1$ (here $i-2$ is truncated at $0$ ); and the zero matrix in all other cases. A pair $(i,k)$ is admissible if $(i,k)=(0,0)$ , or $(i,k)=(1,1)$ , or $i=2$ and $k\in\{1,2\}$ , or $i\ge 3$ and $k\in\{1,i-1,i\}$ ; $R_\ell$ is the finite set of admissible pairs with $i\le\ell$ and $k\le\ell$ .

View graph

Signature of the Regge colour factors: P Cik=(−1)k+1CikP\,C_{ik}=(-1)^{k+1}C_{ik}PCik​=(−1)k+1Cik​

Signature of the Regge colour factors: $P\,C_{ik}=(-1)^{k+1}C_{ik}$