Odd-sector Casimir spectrum: eigenvalue 2 (×24) and 0 (×8)

Proved

Clifford6Casimir.spectrum

by lisamegawatts · Sep 19, 2026 · Mathlib 0df444a (Lean v4.33.1)

clifford-algebrarepresentation-theory

Let $T_i = \tfrac12\,\mathrm{ad}_{E_i}$ be the halved adjoint action of the registered $\mathfrak{su}(2)$ triple on $\mathrm{Cl}(6,0)$ , and let $C = -(T_1^2+T_2^2+T_3^2)$ be the associated quadratic Casimir endomorphism. All four endomorphisms preserve the odd sector $\mathrm{Cl}^-(6,0)$ , and on it the Casimir has exactly two eigenvalues with the multiplicities

C = 2 \ \text{with multiplicity } 24, \qquad C = 0 \ \text{with multiplicity } 8,

the two eigenspaces spanning the whole 32-dimensional odd sector. Representation-theoretically this is the decomposition $\mathrm{Cl}^-(6,0) \cong 8\,V_{j=1} \oplus 8\,V_{j=0}$ of the odd sector under the generated $\mathrm{Spin}(3)$ .

The statement is an eigenspace decomposition with exact multiplicities, not a pointwise eigenvalue claim; it asserts nothing about particles, generations, or any other physical object.

Preamble

import Definitions.Def_clifford6_casimir_data

Formal statement

theorem Clifford6Casimir.spectrum
    (T1 T2 T3 C : CliffordAlgebra Clifford6.Q60 →ₗ[ℝ] CliffordAlgebra Clifford6.Q60)
    (h1 : ∀ x, T1 x = (1/2:ℝ) • (Clifford6.E1 * x - x * Clifford6.E1))
    (h2 : ∀ x, T2 x = (1/2:ℝ) • (Clifford6.E2 * x - x * Clifford6.E2))
    (h3 : ∀ x, T3 x = (1/2:ℝ) • (Clifford6.E3 * x - x * Clifford6.E3))
    (hC : ∀ x, C x = -(T1 (T1 x) + T2 (T2 x) + T3 (T3 x))) :
    (∀ x ∈ Clifford6.oddSector,
      T1 x ∈ Clifford6.oddSector ∧ T2 x ∈ Clifford6.oddSector ∧
        T3 x ∈ Clifford6.oddSector ∧ C x ∈ Clifford6.oddSector)
      ∧ (Clifford6.oddSector ⊓ LinearMap.ker (C - (2:ℝ) • LinearMap.id) ⊔
          Clifford6.oddSector ⊓ LinearMap.ker C = Clifford6.oddSector)
      ∧ (Module.finrank ℝ
          ↥(Clifford6.oddSector ⊓ LinearMap.ker (C - (2:ℝ) • LinearMap.id)) = 24)
      ∧ (Module.finrank ℝ ↥(Clifford6.oddSector ⊓ LinearMap.ker C) = 8) := by
  sorry

Source

MonumentalSystems/LeanProofs research memory #2561 (2026-09-12): exact full-sector SU(2) decomposition on Cl⁻(6,0); frozen internal targets Rosetta/Cl60OddSectorCasimirSpectrumV1Targets.lean and program research/cl60-casimir-spectrum-v1/program.json, https://github.com/MonumentalSystems/LeanProofs

Read-back

What the Lean code literally says, in plain math · GLM-5.3 (ZCode agent, blind sub-agent audit)

Let T1, T2, T3, C be arbitrary R-linear endomorphisms of the full Clifford algebra. Hypotheses (each universally quantified over every element x of the whole algebra, not just the odd sector):

T1 x = (1/2)(E1 x - x E1), T2 x = (1/2)(E2 x - x E2), T3 x = (1/2)(E3 x - x E3), C x = -(T1(T1 x) + T2(T2 x) + T3(T3 x)),

with E1 = e0e2, E2 = e2e5, E3 = e0e5. These pointwise identities pin down each map uniquely, so the hypotheses are jointly satisfiable in exactly one way; note the minus sign: C is the negative of T1^2 + T2^2 + T3^2, not the positive sum. Under these hypotheses, the theorem asserts the conjunction of:

Stability: for every x in the odd sector, each of T1 x, T2 x, T3 x, C x again lies in the odd sector.
Decomposition: (oddSector ^ ker(C - 2 id)) + (oddSector ^ ker C) = oddSector, where + is the sum (join) of submodules; the odd sector is the internal sum of the part on which C acts with eigenvalue 2 and the part on which C acts with eigenvalue 0.
dim_R(oddSector ^ ker(C - 2 id)) = 24.
dim_R(oddSector ^ ker C) = 8.

Casual reader notes: only the eigenvalues 2 and 0 of C appear, with asserted multiplicities 24 and 8 (summing to 32); triviality of the intersection of the two summands is not asserted separately (it is automatic for eigenspaces of distinct eigenvalues); the conclusion mentions only C and the odd sector — T1, T2, T3 enter only through the hypotheses; and although the hypotheses fix the operators on the entire algebra, every conclusion clause concerns only the odd sector.

Human review

Endorsed by Shuze Chen · Sep 24, 2026
Confirmed by the moderator at approval.
Endorsed by lisamegawatts · Sep 24, 2026
Confirmed by the mission captain (proposal self-audit).

View graph