The active triple closes as
ProvedClifford6Casimir.su2_tripleThe three registered bivectors , , in satisfy the commutation relations with Clifford structure constants:
Here is the algebra commutator. This identifies the subalgebra generated by the triple on the index set as a copy of inside the even part of , the prerequisite for any representation-theoretic spectral statement about the adjoint action on the odd sector.
import Definitions.Def_clifford6_casimir_data
theorem Clifford6Casimir.su2_triple :
Clifford6.E1 * Clifford6.E2 - Clifford6.E2 * Clifford6.E1 = (2:ℝ) • Clifford6.E3
∧ Clifford6.E2 * Clifford6.E3 - Clifford6.E3 * Clifford6.E2 = (2:ℝ) • Clifford6.E1
∧ Clifford6.E3 * Clifford6.E1 - Clifford6.E1 * Clifford6.E3 = (2:ℝ) • Clifford6.E2 := by
sorryRead-back
What the Lean code literally says, in plain math · GLM-5.3 (ZCode agent, blind sub-agent audit)
This theorem is unconditional (no parameters, no hypotheses). It asserts that, in the real Clifford algebra of R^6 with Q60(x) = sum x_i^2 and E1 = e0e2, E2 = e2e5, E3 = e0e5 with e_i = iota(delta_i), the following three identities hold simultaneously:
[E1,E2] = 2 E3, [E2,E3] = 2 E1, [E3,E1] = 2 E2,
where the products and differences are taken in the Clifford algebra and 2* is multiplication by the real scalar 2. Notes for the casual reader: the coefficient is exactly +2 in each identity, in the displayed cyclic order; a different constant, sign, or commutator order would be a different statement. The theorem asserts only these three equalities of algebra elements; it claims nothing about the E_i being nonzero, linearly independent, of pure grade 2, or forming a Lie algebra, and nothing about any action on a subspace.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.