The odd sector is 32-dimensional
ProvedClifford6Casimir.odd_sector_finrankThe odd-grade sector , i.e. the linear span of all products of an odd number of orthonormal generators, has real dimension
This fixes the ambient dimension in which the adjoint-action spectra of the goal theorem are computed.
import Definitions.Def_clifford6_casimir_data
theorem Clifford6Casimir.odd_sector_finrank :
Module.finrank ℝ ↥Clifford6.oddSector = 32 := 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. It asserts that the odd sector — the R-span of all odd-grade monomials, i.e. the sum of the grade-1, grade-3, and grade-5 pieces — has dimension exactly 32 as a real vector space. No other dimension (of the full algebra, the even part, or any single graded piece) is asserted. Casual reader note: since the odd sector is defined by parity rather than by a single grade, the constant 32 is the total dimension of the entire odd part, not the dimension of, say, the grade-1 piece.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.