Crossing parity: $\mathbf T_t^2$ even, $\mathbf T_{s-u}^2$ odd, $C_{00}$ odd

Proved

NaculichRegge.crossing_parity_ops

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

color-algebramathematical-physicsscattering-amplitudes

Let $P$ be the action of exchanging external legs 2 and 3 on the trace basis ( $c[1]\leftrightarrow c[3]$ , $c[4]\leftrightarrow c[6]$ , $c[2],c[5]$ fixed). Then

P\,\mathbf T_t^2\,P=\mathbf T_t^2,\qquad P\,\mathbf T_{s-u}^2\,P=-\mathbf T_{s-u}^2,\qquad P\,C_{00}=-C_{00}.

Preamble

import Definitions.Def_NaculichRegge_TraceBasis

open Polynomial

Formal statement

namespace NaculichRegge

/-- Naculich, eqs. (3.7), (4.7): under the exchange of legs 2 and 3, `𝐓_t²` is even,
`𝐓_{s-u}²` is odd, and `C₀₀` is odd. -/
theorem crossing_parity_ops :
    crossing * Tt2 * crossing = Tt2 ∧ crossing * Tsu2 * crossing = -Tsu2 ∧
      crossing.mulVec C00 = -C00 := 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, pp. 8, 12–13, eqs. (3.7), (4.7), (4.15)

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.

The statement is the conjunction of three equalities, with no hypotheses:

P\,\mathbf T_t^2\,P=\mathbf T_t^2,\qquad P\,\mathbf T_{s-u}^2\,P=-\mathbf T_{s-u}^2\qquad(\text{as }6\times6\text{ matrices over }\mathbb C[N]),

and $P\,C_{00}=-C_{00}$ (as colour vectors). Products are ordinary matrix products.

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

Crossing parity: Tt2\mathbf T_t^2Tt2​ even, Ts−u2\mathbf T_{s-u}^2Ts−u2​ odd, C00C_{00}C00​ odd

Crossing parity: $\mathbf T_t^2$ even, $\mathbf T_{s-u}^2$ odd, $C_{00}$ odd