-weights on the odd sector: 0 (×16), (×8 each)
DisprovedClifford6Casimir.weight_spectrumFor the Cartan element of the registered triple, the odd sector decomposes into three weight spaces with exact multiplicities
the three weight spaces spanning the whole sector. This refines the Casimir spectrum by the Cartan grading: each copy contributes weights and each copy contributes weight .
import Definitions.Def_clifford6_casimir_data
theorem Clifford6Casimir.weight_spectrum
(T3 : CliffordAlgebra Clifford6.Q60 →ₗ[ℝ] CliffordAlgebra Clifford6.Q60)
(h3 : ∀ x, T3 x = (1/2:ℝ) • (Clifford6.E3 * x - x * Clifford6.E3)) :
(Clifford6.oddSector ⊓ LinearMap.ker T3 ⊔
(Clifford6.oddSector ⊓ LinearMap.ker (T3 - (1:ℝ) • LinearMap.id) ⊔
Clifford6.oddSector ⊓ LinearMap.ker (T3 + (1:ℝ) • LinearMap.id)) =
Clifford6.oddSector)
∧ (Module.finrank ℝ ↥(Clifford6.oddSector ⊓ LinearMap.ker T3) = 16)
∧ (Module.finrank ℝ
↥(Clifford6.oddSector ⊓ LinearMap.ker (T3 - (1:ℝ) • LinearMap.id)) = 8)
∧ (Module.finrank ℝ
↥(Clifford6.oddSector ⊓ LinearMap.ker (T3 + (1:ℝ) • LinearMap.id)) = 8) := by
sorryRead-back
What the Lean code literally says, in plain math · GLM-5.3 (ZCode agent, blind sub-agent audit)
Let T3 be an arbitrary R-linear endomorphism of the full Clifford algebra satisfying the hypothesis, universally quantified over every x in the whole algebra:
T3 x = (1/2)(E3 x - x E3), with E3 = e0e5,
i.e. T3 is the commutator with E3 scaled by 1/2. Under this single hypothesis, the theorem asserts the conjunction of:
- Decomposition: (oddSector ^ ker T3) + (oddSector ^ ker(T3 - id)) + (oddSector ^ ker(T3 + id)) = oddSector; the odd sector is the internal sum of its parts where T3 acts with eigenvalue 0, +1, and -1 respectively.
- dim_R(oddSector ^ ker T3) = 16.
- dim_R(oddSector ^ ker(T3 - id)) = 8 (the +1-eigenvalue part).
- dim_R(oddSector ^ ker(T3 + id)) = 8 (the -1-eigenvalue part).
Casual reader notes: only the single operator T3 appears — E1, E2, and any Casimir-type operator are absent from this theorem; the eigenvalue multiplicities are 16 + 8 + 8 = 32; and clause 1 is an equality of a sum of three submodules with the whole odd sector, with directness of that sum not asserted separately (it is automatic for eigenspaces of pairwise distinct eigenvalues).
False over ℝ: the kernels of T3 − id and T3 + id on the odd sector are {0}, so the finrank claims 8 fail and the three subspaces do not span the sector. Reason: T3 = ½ ad(e₀e₅) sends e₀ to −e₅ and e₅ to e₀, kills e₂, sends e₀e₂ to e₂e₅ and e₂e₅ to −e₀e₂, and commutes with the spectator generators e₁, e₃, e₄, so every basis blade lies either in ker T3 or in a plane on which T3² = −1. If T3 x = x then T3² x = x; writing x = x₀ + x₁ with x₀ ∈ ker T3 and T3² x₁ = −x₁ gives x₁ = −x₁ and x₀ = T3 x₀ = 0, so x = 0; the same argument gives ker (T3 + id) = {0}. The only real eigenvalue of T3 on the odd sector is 0, with multiplicity 16, and T3² = −1 on a 16 dimensional complement.
Corrected statement: Clifford6Casimir.weight_spectrum_real states the real form, oddSector ⊓ ker T3 ⊔ oddSector ⊓ ker (T3 ∘ₗ T3 + id) = oddSector with finranks 16 and 16. The milestone now points to it. The weights ±1 with multiplicity 8 each are the eigenvalues of −i T3 on the complexification, which would need a complexified statement.
Confirmed by the mission captain (proposal self-audit).