$C_{00}$ is an eigenvector of $\mathbf T_t^2$ with eigenvalue $N$

Proved

NaculichRegge.tt2_C00_eigen

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

color-algebramathematical-physicsscattering-amplitudes

The tree-level $t$ -channel colour factor is an eigenvector of the $t$ -channel Casimir: $\mathbf T_t^2C_{00}=N\,C_{00}$ . In the paper this is $\mathbf T_1\cdot\mathbf T_4C_{00}=-\tfrac12NC_{00}$ (eq. (4.2)) combined with $\mathbf T_t^2=2N+2\mathbf T_1\cdot\mathbf T_4$ (eq. (4.7)); here it is stated for the matrix of eq. (4.15).

Preamble

import Definitions.Def_NaculichRegge_TraceBasis

open Polynomial

Formal statement

namespace NaculichRegge

/-- Naculich, eqs. (4.2), (4.7): `C₀₀` is an eigenvector of `𝐓_t²` with eigenvalue `N`. -/
theorem tt2_C00_eigen : Tt2.mulVec C00 = (X : ℂ[X]) • 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. 11–13, eqs. (4.2), (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 asserts the equality of colour vectors

\mathbf T_t^2\,C_{00}=N\cdot C_{00},

i.e. the matrix $\mathbf T_t^2$ applied to $C_{00}=(1,0,-1,0,0,0)^T$ equals $(N,0,-N,0,0,0)^T$ , as vectors of polynomials in $N$ with complex coefficients. It has no hypotheses.

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

C00C_{00}C00​ is an eigenvector of Tt2\mathbf T_t^2Tt2​ with eigenvalue NNN

$C_{00}$ is an eigenvector of $\mathbf T_t^2$ with eigenvalue $N$