Cl(6,0) odd-sector Casimir data

Definition

clifford6_casimir_data

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

clifford-algebralinear-algebrarepresentation-theory

Basic data for the adjoint Casimir computation on the real Clifford algebra $\mathrm{Cl}(6,0)$ of Euclidean $\mathbb{R}^6$ .

Let $Q_{60} = \mathrm{diag}(1,1,1,1,1,1)$ be the Euclidean quadratic form on $\mathbb{R}^6$ , let $e_i$ be the $i$ -th orthonormal generator of $\mathrm{Cl}(6,0)$ , and let $\mathrm{Cl}^-(6,0)$ denote the odd-grade sector, the linear span of all products of an odd number of generators.

The file also fixes three bivectors $E_1 = e_0e_2$ , $E_2 = e_2e_5$ , $E_3 = e_0e_5$ , built on the index triple $\{0,2,5\}$ . These are the distinguished generators of an $\mathfrak{su}(2)$ subalgebra acting on the odd sector by the halved adjoint action; the associated quadratic Casimir and its spectrum are the subject of the companion theorems.

Definition code

import Mathlib

namespace Clifford6

/-- The Euclidean quadratic form diag(1,1,1,1,1,1) on R^6. -/
noncomputable def Q60 : QuadraticForm ℝ (Fin 6 → ℝ) :=
  QuadraticMap.weightedSumSquares ℝ (fun _ => 1)

/-- The i-th orthonormal generator of Cl(6,0). -/
noncomputable def e6 (i : Fin 6) : CliffordAlgebra Q60 :=
  CliffordAlgebra.ι Q60 (Pi.single i 1)

/-- The odd-grade sector Cl⁻(6,0) = grades 1, 3, 5. -/
noncomputable def oddSector : Submodule ℝ (CliffordAlgebra Q60) :=
  CliffordAlgebra.evenOdd Q60 1

/-- First generator of the active su(2) triple: e₀e₂. -/
noncomputable def E1 : CliffordAlgebra Q60 := e6 0 * e6 2

/-- Second generator: e₂e₅. -/
noncomputable def E2 : CliffordAlgebra Q60 := e6 2 * e6 5

/-- Third generator: e₀e₅. -/
noncomputable def E3 : CliffordAlgebra Q60 := e6 0 * e6 5

end Clifford6

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)

This block defines six objects, all built over the real Clifford algebra of R^6 with its standard Euclidean form. First, Q60 is the quadratic form on R^6 (formalized as the space of functions {0,...,5} -> R) given by the weighted sum of squares with all weights equal to 1: Q60(x) = sum x_i^2. Second, for each i, e_i is the element iota(delta_i) of the Clifford algebra, where iota is the canonical map (satisfying iota(v)^2 = Q60(v) * 1) and delta_i is the standard basis vector. Note: the file defines these elements but asserts no relations about them; e_i^2 = 1 and anticommutation are consequences of the underlying construction, not claims in this file. Third, oddSector is the R-submodule given by the odd part of the canonical Z/2-grading: the span of all odd-fold products. A casual reader should note that the argument 1 is a parity, not a grade: this submodule is the sum of the grade-1, grade-3, and grade-5 pieces together, not the grade-1 piece alone. Finally, three elements are defined by Clifford multiplication of two specific distinct generators: E1 = e0 e2, E2 = e2 e5, E3 = e0 e5.

View graph