The SpinRepresentations roadmap — annotated

The universal property is the tool that makes the Clifford algebra usable: CliffordAlgebra.lift and hom_ext say that a map out of CliffordAlgebra Q into an algebra A is exactly a linear map f : M →ₗ A with f m * f m = algebraMap R A (Q m) for every vector \(m\). The file records the two working identities — the Clifford square ι_sq_scalar, and the polarization ι_mul_ι_add_swap, which reads \(\iota a \cdot \iota b + \iota b \cdot \iota a = \mathrm{polar}\,Q\,a\,b\), so that orthogonal vectors anticommute (ι_mul_ι_comm_of_isOrtho). It also records the functor CliffordAlgebra.map and equivOfIsometry: an isometry of quadratic forms induces an algebra isomorphism, and consequently over \(\mathbb{C}\) the Clifford algebra depends only on the rank of the form.

Mathlib's evenOdd Q : ZMod 2 → Submodule R (CliffordAlgebra Q) is a genuine GradedAlgebra: the Clifford relation preserves parity, so the grading descends to the quotient. The file consumes evenOdd Q, the GradedAlgebra instance, evenOdd_isCompl (the two halves are complementary), and the even subalgebra even Q. The grade involution involute acts as \(+1\) on evenOdd Q 0 and \(-1\) on evenOdd Q 1; the records spinGroup.mem_even and spinGroup.involute_eq say the spin group sits in the even part and is fixed by involute. This grading is what distinguishes pinGroup from spinGroup.

filtration Q k is the span of the products of at most \(k\) generators: Submodule.span R {x | ∃ n ≤ k, ∃ v : Fin n → M, x = ∏ i, ι Q (v i)}, an increasing filtration with filtration Q 0 = range (algebraMap R _) (the scalars, the empty product), filtration Q 1 the scalars together with range ι, and union ⊤ (iSup_ι_range_eq_top). Multiplicativity filtration Q i · filtration Q j ≤ filtration Q (i + j) must be proved before anything downstream; this is deliberately not a power of a submodule — powers of submodules of a noncommutative algebra would collect products of exactly \(k\) generators, not at most \(k\).

For finite free \(M\), finrank (CliffordAlgebra Q) = 2 ^ finrank M, matching \(\sum_k \binom{\mathrm{finrank}\,M}{k}\). This is read off the module isomorphism equivExterior (valid in characteristic not two), which identifies the underlying module of the Clifford algebra with that of the exterior algebra: deforming the form deforms the multiplication and nothing else.

The graded-algebra isomorphism \(\mathrm{gr}\,\mathrm{Cliff}(V, Q) \cong \mathrm{ExteriorAlgebra}\,R\,M\) is a distinct milestone. Its graded pieces give filtrationGradedEquiv: \((\mathrm{filtration}\,Q\,(k+1) \big/ \mathrm{filtration}\,Q\,k) \simeq_{\mathbb{R}} \bigwedge_R^{\,k+1} M\) in characteristic not two. It is proved either from the universal property and the filtration directly, or by proving that CliffordAlgebra.equivExterior carries \(\mathrm{filtration}\,Q\,k\) onto \(\bigoplus_{i \le k} \bigwedge^{\,i} M\) and reading off the \(k\)-th quotient; equivExterior alone is only a module isomorphism, so the filtration-compatibility is content that must be proved, not assumed. In particular finrank (CliffordAlgebra Q) = 2 ^ finrank M for finite free \(M\), matching \(\sum_k \binom{\mathrm{finrank}\,M}{k}\).

Consume QuadraticForm.Nondegenerate; build the reduction of a nondegenerate \(Q\) over a field of characteristic not two to an orthogonal basis (a diagonal form), and over \(\mathbb{C}\) to the standard form \(\sum x_i^2\), so \(\mathrm{Cliff}(V, Q) \cong \mathrm{Cliff}(\sum x_i^2)\). This is where equivOfIsometry does its work; it also fixes the hyperbolic decomposition \(V = W \oplus W'\) used to build \(S\).

For \(Q\) nondegenerate on a \(2l\)-dimensional \(V\) over an algebraically closed field, CliffordAlgebra Q ≃ₐ[K] Matrix (Fin (2^l)) (Fin (2^l)) K, and the even subalgebra even Q ≃ₐ[K] Matrix (Fin (2^(l-1))) _ K × Matrix (Fin (2^(l-1))) _ K. This isomorphism is spinAction, the Clifford action on the spin module \(S = \bigwedge\! W\) of Layer 4, identified with a matrix algebra by the dimension count; the even subalgebra's two factors are the actions on the half-spin summands \(S^+, S^-\).

For \(Q\) nondegenerate on a \((2l+1)\)-dimensional \(V\), CliffordAlgebra Q ≃ₐ[K] Matrix (Fin (2^l)) _ K × Matrix (Fin (2^l)) _ K, while the even subalgebra is a single Matrix (Fin (2^l)) _ K. The center is \(K\) (even case) or \(K \times K\) (odd case); the two central idempotents in the odd case are the source of the two inequivalent restrictions to Pin.

Consume CliffordAlgebra.equivEven (\(\mathrm{Cliff}(Q) \cong \mathrm{even}(Q \oplus \langle -1 \rangle)\)) and CliffordAlgebra.prodEquiv (the graded tensor product over a direct sum of forms); these are the algebraic inputs the complex structure theorem and the real Bott periodicity of Layer 7 both rest on.

orthogonalGroup Q : Subgroup (M ≃ₗ[R] M) — \(\mathrm{orthogonalGroup}\,Q \le \mathrm{Subgroup}\,(M \simeq_{\mathbb{R}} M)\) — the linear automorphisms \(f\) with \(Q(f\,x) = Q\,x\) for all \(x\) (equivalently Nonempty (Q.IsometryEquiv Q) realized as a bundled automorphism group), and specialOrthogonalGroup Q its determinant-one subgroup. Prove the isomorphism with Matrix.orthogonalGroup (Fin n) K under a basis diagonalizing \(Q\) (for the standard form), so the abstract and matrix presentations agree.

Before the conjugation is an automorphism of \(M\), one needs the linear equivalence ιRangeEquiv Q : M ≃ₗ[R] range (ι Q), which over a field with nondegenerate \(Q\) comes from injectivity of \(\iota Q\). This is a named milestone, not a phrase; the conjugation action on \(M\) is defined by transporting spinGroup.involute_act_ι_mem_range_ι through ιRangeEquiv.

pinToOrthogonal Q : pinGroup Q →* orthogonalGroup Q, sending \(x\) to the automorphism \(v \mapsto \mathrm{ιRangeEquiv}^{-1}\,(\mathrm{involute}\,x \cdot \iota v \cdot x^{-1})\) of \(M\) (well-defined by spinGroup.involute_act_ι_mem_range_ι, and \(Q\)-preserving because \(\iota v \cdot \iota v = Q v\) is central). Its restriction spinToSpecialOrthogonal Q lands in the determinant-one subgroup (the spin group is generated by even products of unit vectors, each contributing two reflections). Prove functoriality and that a unit vector \(\iota v\) (with \(Q v\) a unit) maps to the reflection in \(v^{\perp}\).

For finite-dimensional \(V\) over an algebraically closed field (\(\mathbb{C}\) here) with nondegenerate \(Q\), pinToOrthogonal Q and spinToSpecialOrthogonal Q are surjective (Cartan–Dieudonné: every isometry is a product of reflections, each realized by a unit vector), with kernel \(\{\pm 1\}\) of order two (MonoidHom.ker (spinToSpecialOrthogonal Q) generated by \(-1\), Nat.card = 2). Assemble the short exact sequences \(1 \to \mathbb{Z}/2 \to \mathrm{Pin}(V) \to O(V) \to 1\) and \(1 \to \mathbb{Z}/2 \to \mathrm{Spin}(V) \to SO(V) \to 1\). Over a general field, pointwise surjectivity onto \(SO(Q)\) fails: the image is the kernel of the spinor norm \(SO(Q) \to K^*/(K^*)^2\), so state the general-field result as that spinor-norm exact sequence, and the algebraically closed and real cases separately.

The claim that Spin(V) is the universal cover of \(SO(V)\) is topological and split by case, out of the main dependency chain: the compact real case (Spin(n) → SO(n) universal covering for \(n \ge 3\), Spin(n) connected for \(n \ge 2\), simply connected for \(n \ge 3\), proved from path-connectedness of the sphere, with the real forms of Layer 7); the complex algebraic case (Spin(V) over \(\mathbb{C}\) is the algebraically simply connected group with root datum of type \(B_l/D_l\), distinct from topological simple-connectivity); and the indefinite real case (connectivity of Spin(p, q) for \(p, q > 0\), deferred to a later topology roadmap). None of these is needed to construct the spin representations.

Status: the Lie-subalgebra bullet landed canonically as quadraticLieSubalgebra Q by #2224 (chrisromanmiller); the exterior-bivector identification sits in review in #2335 (utensil), successor to the closed #1972. The image of \(\bigwedge_R^{\,2} M\) in even Cliff(V, Q) is closed under the commutator bracket; equip \(\bigwedge^2 V\) with the induced Lie-algebra structure. soEquivBivector: this is a Lie-algebra isomorphism \(\bigwedge_R^{\,2} M \simeq^{\mathrm{Lie}} \mathfrak{so}(V)\) onto the skew-adjoint endomorphisms, identified with LieAlgebra.Orthogonal.so under a basis. The defining property is the action, not a hard-coded scalar: the bivector \(\beta(u, v)\) acts on a vector \(x\) by \(\mathrm{ad}(\beta(u, v))(x) = B(v, x) \cdot u - B(u, x) \cdot v\), where \(B = \mathrm{QuadraticMap.polar}\,Q\). Choose the Clifford formula and scalar normalization (a multiple of \(\iota u \cdot \iota v - \iota v \cdot \iota u\)) so as to prove this identity against Mathlib's polar convention; do not fix the factor \(\frac12\) before the convention is pinned. The bracket of a bivector with \(\iota v\) is the infinitesimal rotation of \(v\), which is the differential of the Layer-2 conjugation. Stated here for the standard form on Fin n → R; Layer 9 restates the realization for an arbitrary nondegenerate \(Q\), as soEquivQuadratic against Mathlib's skewAdjointLieSubalgebra, pinned to the same action formula.

The Lie-algebra homomorphism differentiating spinToSpecialOrthogonal is the isomorphism soEquivBivector composed with the adjoint action; state the compatibility \(d(\mathrm{conjugation}) = \mathrm{ad}(\mathrm{bivector})\) as a named lemma, so the group double cover and the Lie-algebra identification are two views of one object. This is the hook that lets a spinGroup representation differentiate to an \(\mathfrak{so}(V)\)-module and be compared with the highest-weight roadmap.

Over \(\mathbb{C}\), a nondegenerate \(Q\) on a \(2l\)- or \((2l+1)\)-dimensional \(V\) has an isotropic subspace \(W\) with \(\mathrm{finrank}_{\mathbb{C}}\,W = l\) and (in even dimension) a complementary isotropic \(W'\) pairing with \(W\) by \(Q\), so \(V = W \oplus W'\) (even) or \(V = W \oplus W' \oplus \langle e \rangle\) (odd). Build \(W\), the pairing \(W' \simeq \mathrm{Module.Dual}_{\mathbb{C}}\,W\) induced by \(\mathrm{QuadraticMap.polar}\,Q\), and the isotropy Q.IsOrtho witnesses.

spinAction Q W : CliffordAlgebra Q →ₐ[ℂ] Module.End ℂ (ExteriorAlgebra ℂ W), the algebra homomorphism from the universal property, sending \(\iota w\) (for \(w \in W\)) to exterior multiplication \(w \wedge -\), and \(\iota w'\) (for \(w' \in W'\)) to the contraction contractLeft by the functional \(\mathrm{QuadraticMap.polar}\,Q\,w'\) restricted to \(W\). The defining check is the anticommutator identity \(c(x) \circ c(y) + c(y) \circ c(x) = \mathrm{polar}\,Q\,x\,y \cdot 1\) on \(V = W \oplus W'\) (\(w \wedge (w \wedge -) = 0\) gives the isotropy of \(W\), and the wedge/contraction anticommutator on mixed pairs gives the pairing), from which the Clifford relation \(\iota v \cdot \iota v = Q v\) follows via \(\mathrm{polar}\,Q\,v\,v = 2 \cdot Q v\). Pin the coefficient to polar, not a prose "twice". In even dimension it is an isomorphism onto End S (\(\dim S = 2^l\)), proved by exhibiting matrix units from wedge and contraction operators and a dimension count — exactly the Layer-1 structure theorem. In odd dimension spinAction is not injective: \(\dim \mathrm{Cliff}(V, Q) = 2 \cdot (2^l)^2\) exceeds \(\dim \mathrm{End}\,S = (2^l)^2\), so it factors through one of the two central-idempotent summands. Fix the action of the extra anisotropic vector \(e\) as the parity operator scaled so that \(c(e) \circ c(e) = Q e \cdot 1\); the faithful Clifford module in odd dimension is the direct sum of the two inequivalent spinor modules, not the single \(S\).

spinRep Q W : Representation ℂ (spinGroup Q) (ExteriorAlgebra ℂ W), the restriction of spinAction along spinGroup.toUnits; likewise pinRep for pinGroup. State the compatibility that spinRep differentiates to the \(\mathfrak{so}(V)\)-module of Layer 3 on \(S\).

The \(\mathbb{Z}/2\)-grading of the exterior algebra splits \(S = S^+ \oplus S^-\) (even and odd exterior degree); spinPlus Q W, spinMinus Q W, each of dimension \(2^{l-1}\) in even dimension, are spinGroup-subrepresentations (the spin group is even, so it preserves exterior parity). In odd dimension \(S\) is irreducible and does not split; in even dimension \(S^+\) and \(S^-\) are the two inequivalent half-spin representations.

spinRep is irreducible in odd dimension, and spinPlus, spinMinus are irreducible and inequivalent in even dimension. This is immediate once spinAction is known to be surjective onto the full matrix algebra (Layer 1, proved forward from this module): a module on which a full matrix algebra acts is simple, and the even subalgebra's two matrix factors act as the two simple modules \(S^+, S^-\).

Choose the Cartan subalgebra of \(\mathfrak{so}(V)\) spanned by the bivectors \(\beta(w_i, w_i')\) of dual isotropic pairs, and a compatible Borel; identify its roots with the abstract \(B_l/D_l\) root system of the root-systems roadmap, and prove the fundamental weights computed here correspond to the abstract fundamental weights. Without this explicit identification the highest-weight statement is only informal; it is a named milestone.

Diagonalize the chosen Cartan on \(S = \bigwedge\! W\); the weight of a basis vector \(w_{i_1} \wedge \cdots \wedge w_{i_k}\) is \(\tfrac12(\pm 1, \ldots, \pm 1)\) with the signs recording which \(w_i\) occur. The weights of \(S\) are exactly the \(2^l\) half-integer sign vectors; the highest is \(\omega_l = \tfrac12(1, \ldots, 1)\).

\(S\) (odd dimension) is the irreducible \(\mathfrak{so}(2l+1)\)-module with highest weight \(\omega_l\), the last fundamental weight; state \(S \cong L(\omega_l)\) as a LieModule, with finrank = 2^l, and separately that spinRep Q W differentiates to it. This is the fundamental representation of \(B_l\) whose weights lie in the half-integral coset, outside the lattice generated by the vector weights \(\pm e_i\), so it is not a constituent of any tensor power (in particular any \(\bigwedge^k V\)) of the standard \(\mathfrak{so}(2l+1)\)-module; it completes the classical-groups roadmap's \(B_l\) fundamentals.

\(S^+, S^-\) (even dimension) are the irreducible \(\mathfrak{so}(2l)\)-modules with highest weights \(\omega_l = \tfrac12(1, \ldots, 1)\) and \(\omega_{l-1} = \tfrac12(1, \ldots, 1, -1)\), the two fork-node fundamental weights of \(D_l\); state \(S^+ \cong L(\omega_l)\), \(S^- \cong L(\omega_{l-1})\) as LieModules, each of dimension \(2^{l-1}\). Their sum \(S\) is the restriction of the \(B_l\) spin module. The exchange \(\omega_l \leftrightarrow \omega_{l-1}\) is the \(D_l\) diagram automorphism, the seed of triality at \(l = 4\).

State the character of \(S\) as an element of the group algebra of the weight lattice, \(\sum_{\varepsilon_i = \pm 1} e^{\frac12 \sum_i \varepsilon_i e_i}\) (the Weyl character formula specialized); the familiar product form \(\prod_i (t_i^{1/2} + t_i^{-1/2})\) is its evaluation on a maximal torus, valid only after the spin maximal torus and its character lattice are defined (half-powers of adjoint-torus coordinates are not functions on the adjoint torus). Record that the other \(B_l/D_l\) fundamentals \(\bigwedge^k V\) are built in the classical-groups roadmap; together they are a full set of fundamental representations.

Each is an isomorphism of the spin group with a small classical group. spinGroup Q is a subgroup of the units of even Cliff(V, Q), so an isomorphism onto a bundled matrix group is not read off from the representation landing in that group; it needs three explicit milestones per case: (1) identify the even Clifford algebra with a matrix algebra (even Cliff₃ ≅ M₂(ℂ), even Cliff₆ ≅ M₄(ℂ), and so on), so spinGroup Q sits inside its units; (2) identify the defining condition of spinGroup (the reversal/Clifford-norm-one condition reverse x · x = 1) with the classical group's condition on that matrix algebra: determinant one for \(SL_n\), preservation of the reversal-induced symplectic form for \(Sp_4\); (3) prove the image is exactly the classical group, both directions, not merely that spinAction lands in it.

For \(V = \mathbb{C}^3\) (type \(B_1 = A_1\)), even Cliff(V, Q) ≅ M₂(ℂ) with \(\dim W = 1\), and the spinor-norm-one subgroup spinGroup Q is the determinant-one subgroup, giving spinGroup Q ≃* SL(2, ℂ); the \(2\)-dimensional spin representation \(S\) is the standard representation of \(SL_2\). Over \(\mathbb{R}\) this is \(\mathrm{Spin}(3) \cong SU(2)\).

For \(V = \mathbb{C}^4\) (type \(D_2 = A_1 \times A_1\)), spinGroup Q ≃* SL(2, ℂ) × SL(2, ℂ), with \(S^+\) and \(S^-\) the standard representations of the two factors; this is the reducibility of the \(D_2\) spin module into the two \(A_1\) standards.

For \(V = \mathbb{C}^5\) (type \(B_2 = C_2\)), spinGroup Q ≃* Sp(4, ℂ) (Matrix.symplecticGroup), with the \(4\)-dimensional spin representation \(S\) the standard representation of \(Sp_4\); the symplectic form on \(S\) comes from the reversal antiautomorphism.

For \(V = \mathbb{C}^6\) (type \(D_3 = A_3\)), spinGroup Q ≃* SL(4, ℂ), with \(S^+ \cong \mathbb{C}^4\) the standard representation and \(S^- \cong (\mathbb{C}^4)^*\) its dual; \(V \cong \bigwedge^2 (\mathbb{C}^4)\). These four exhaust the coincidences of the \(B_l/D_l\) diagrams with the \(A_l/C_l\) diagrams.

realCliffordForm p q : QuadraticForm ℝ (Fin (p+q) → ℝ), the diagonal form with \(p\) entries \(+1\) and \(q\) entries \(-1\), and Cliff(p, q) = CliffordAlgebra (realCliffordForm p q). The sign convention is fixed by four base entries stated as definitional acceptance tests, so the indexing of the periodicity table is unambiguous: \(\mathrm{Cliff}(1,0) \cong \mathbb{R} \times \mathbb{R}\), \(\mathrm{Cliff}(0,1) \cong \mathbb{C}\), \(\mathrm{Cliff}(0,2) \cong \mathbb{H}\), \(\mathrm{Cliff}(1,1) \cong M_2(\mathbb{R})\). Here \(\mathrm{Cliff}(0,1) \cong \mathbb{C}\) is Mathlib's CliffordAlgebraComplex.equiv (its \(Q r = -(r \cdot r)\) matches the \(q\) entry \(-1\)), and \(\mathrm{Cliff}(0,2) \cong \mathbb{H}\) is CliffordAlgebraQuaternion.equiv.

The isomorphisms \(\mathrm{Cliff}(p+1, q+1) \cong \mathrm{Cliff}(p, q) \otimes_{\mathbb{R}} M_2(\mathbb{R})\), \(\mathrm{Cliff}(p+8, q) \cong \mathrm{Cliff}(p, q) \otimes_{\mathbb{R}} M_{16}(\mathbb{R})\) (mod-\(8\) periodicity), built from CliffordAlgebra.equivEven and CliffordAlgebra.prodEquiv; the resulting classification table of \(\mathrm{Cliff}(p, q)\) as a matrix algebra over \(\mathbb{R}\), \(\mathbb{C}\), or \(\mathbb{H}\) (the eightfold way), stated as a function of \((q - p) \bmod 8\) in the convention fixed by the four base entries above (references that make generators square to \(+1\) index by \((p - q) \bmod 8\) instead; the base-entry tests pin which is meant).

spinPQ p q := spinGroup (realCliffordForm p q), the double cover of \(SO(p, q)\) from Layer 2 applied to the real form; the compact \(\mathrm{Spin}(n) = \mathrm{spinPQ}\,n\,0\) and the split and Lorentzian forms \(\mathrm{Spin}(p, q)\).

For the compact \(\mathrm{Spin}(n)\), prove \(\mathrm{Spin}(n)\) connected for \(n \ge 2\) and simply connected for \(n \ge 3\), so \(\mathrm{Spin}(n) \to SO(n)\) is the universal covering, from path-connectedness of the sphere in \(\mathbb{R}^n\). The indefinite \(\mathrm{Spin}(p, q)\) (both \(p, q > 0\)) has its own connectivity subtleties and is deferred to a later topology roadmap; it is not a prerequisite for the representation theory.

The \(D_4\) Dynkin diagram has an order-three symmetry cyclically permuting its three outer nodes; consume the graph automorphism from the root-systems roadmap and lift it to an order-three automorphism of the root datum of \(\mathfrak{so}(8)\) permuting the three fundamental weights \(\omega_1\) (the vector node) and \(\omega_3, \omega_4\) (the two spinor nodes). At this level triality is the statement that the three \(8\)-dimensional highest-weight modules \(V \cong S^0\), \(S^+\), \(S^-\) are cyclically permuted by the outer automorphism; this needs only Layer 5 and the diagram symmetry.

Realizing the diagram automorphism as an actual group automorphism trialityAut : spinGroup Q₈ ≃* spinGroup Q₈ (order three, \(\mathrm{trialityAut}^3 = 1\), and not inner) requires lifting a root-datum automorphism to the simply connected group, an integration/classification theorem for simply connected semisimple groups that is not supplied by the diagram symmetry alone. Its induced action on representations cyclically permutes the three \(8\)-dimensional irreducibles \(V \cong S^0\), \(S^+\), \(S^-\) (all of dimension \(8\), the numerical coincidence that makes triality possible). State the permutation as isomorphisms spinRep ∘ trialityAut ≅ (the vector representation), and so on around the cycle.

The order-\(3\) symmetry of the three \(8\)-dimensional representations, the \(\mathrm{Spin}_8\)-invariant trilinear form \(S^0 \otimes S^+ \otimes S^- \to \mathbb{C}\) permuted by triality, and the relation to the octonions (the multiplication \(\mathbb{O} \otimes \mathbb{O} \to \mathbb{O}\) as the triality form); state the trilinear form and its invariance as the concrete outcome, cross-referencing the octonion structure where it is available.

Landed in part via #2224 (Layer 3’s canonical package): the quadratic elements as a LieSubalgebra of Cliff(V, Q) (contained in even Q and in filtration Q 2). The quadratic element \(\beta(a, b) = \frac12 \cdot [\iota Q\,a, \iota Q\,b]\), pinned by the bracket identity \([\beta(a, b), \iota Q\,x] = \iota Q\,(\mathrm{polar}\,Q\,b\,x \cdot a - \mathrm{polar}\,Q\,a\,x \cdot b)\) with polar Mathlib's, exactly Layer 3's normalization; the quadratic elements as a LieSubalgebra of Cliff(V, Q) (contained in even Q and in filtration Q 2); and soEquivQuadratic, the Lie isomorphism from skewAdjointLieSubalgebra (polarBilin Q) onto them for nondegenerate \(Q\) on a finite-dimensional space, pinned by its own generator-action identity so no automorphism of \(\mathfrak{so}\) can be silently composed in.

A homomorphism \(\theta : \mathfrak{g} \to \mathfrak{so}(V, Q)\) composed with the quadratic realization and any Clifford action \(\rho : \mathrm{Cliff}(V, Q) \to_{\mathrm{alg}} \mathrm{End}(S)\) gives \(\mathfrak{g} \to \mathrm{End}(S)\) (cliffordInducedRep). The two actions on Cliff(V, Q) itself are named apart: the commutator action (cliffordDerivationRep, the exterior extension of the \(V\)-action under equivExterior, not isotypic) and the left-regular action (via Algebra.lmul, the isotypic one). The worked non-example pinning the distinction: \(\bigwedge \mathfrak{sl}_2 \cong 1 \oplus V(2) \oplus V(2) \oplus 1\) under the commutator action, against the four copies of the \(2\)-dimensional simple under left multiplication.

For a symmetric invariant nondegenerate \(B\) (the Killing form of a semisimple \(\mathfrak{g}\), or the trace form of a faithful representation where the Killing form is degenerate), \(\mathrm{ad} : \mathfrak{g} \to \mathfrak{so}(\mathfrak{g}, B)\) (adjointSO), pinned by \((\mathrm{adjointSO}\,\ldots\,x)\,y = [x, y]\). Two bookkeeping pins absent from Mathlib precede the multiplicity statements: LieAlgebra.rank ℂ 𝔤 = dim H for a Cartan subalgebra \(H\), and the parity identity \(d = l + 2 \cdot \#\Delta^+\), stated additively so the exponents \((d \pm l)/2\) below are exact divisions.

For Killing-semisimple \(\mathfrak{g}\) over \(\mathbb{C}\), the left-regular Cliff(𝔤, κ) (carrier the Clifford algebra of the Killing quadratic form, \([x, c] = q(\mathrm{ad}\,x) \cdot c\), identified with \(\bigwedge \mathfrak{g}\) by equivExterior and of dimension \(2^d\) by Layer 0): any two simple submodules are isomorphic, and the pinned decomposition equivalence exhibits \(2^{(d+l)/2}\) copies of one simple of dimension \(2^{(d-l)/2}\). In the vocabulary of the highest-weight roadmap the simple constituent is \(L(\rho)\), the irreducible of highest weight the half-sum of positive roots; that name is prose here (the Layer 5 device), and the Lean statements carry the content without it. Kostant's full \(\rho\)-decomposition \(C(\mathfrak{g}) \cong \mathrm{End}(V_\rho) \otimes C(P)\) (with the primitive subspace \(P\)) is strictly stronger and is a possible later strengthening, deliberately not pinned. The spin-module variant: the full spinor module \(\bigwedge\! W\) of Cliff(𝔤, κ) (Layer 4's spinAction composed with the adjoint quadratic lift; in even dimension it is \(S^+ \oplus S^-\), and the half-spin summands separately are smaller by a factor of two) is isotypic with multiplicity \(2^{\lfloor l/2 \rfloor}\).

\(\mathfrak{g} = \mathfrak{gl}_N\) is reductive, not Killing-semisimple, so its form is the trace form \(Q X = \mathrm{tr}(X^2)\) (nondegenerate where the Killing form is not), and its highest weight carries a half-integral central component. The generators \(d_{ab} = \iota (E_{ab})\) satisfy the CAR relations \(d_{ab} d_{cd} + d_{cd} d_{ab} = 2\,\delta_{bc}\,\delta_{ad}\) (pinned as the polar-form equation); the normal-ordered quadratics \(F_{ij} = \frac12 \sum_k d_{ik} d_{kj}\) form a Lie homomorphism glCliffordHom with \([F_{ij}, d_{kl}] = \delta_{jk} d_{il} - \delta_{li} d_{kj}\) (basis-free: bracketing a generator is the adjoint action), and differ from the antisymmetrized quadratic elements by the normal-ordering constant \(\frac{N}{2}\,\delta_{ij}\), the source of the half-integral central weight. The left-regular Cliff(M_N) (the fermionic Fock space \(\bigwedge (M_N)\) via equivExterior, dimension \(2^{N^2}\)) is isotypic with \(2^{N(N+1)/2}\) simple summands of dimension \(2^{N(N-1)/2}\), each containing a highest weight vector of weight \(\nu = (N - \tfrac12, \ldots, \tfrac12)\) for the matrix-unit positive system. This is Panyushev's Prop. 2.4 and Ex. 2.5(1), and the decomposition behind the CAR-matrix analysis of Shlyakhtenko (arXiv:2606.28648); the companion decomposition \(V^* \otimes L(\nu) \cong \bigoplus_{t=1}^{N} L(\nu - \varepsilon_t)\) is the dual-standard Pieri rule of the highest-weight roadmap, uniform in \(t\) because every \(\nu - \varepsilon_t\) stays dominant.

The \(\mathbb{R}\)-algebra isomorphisms CliffordAlgebraComplex.equiv (consumed) and Cliff(realCliffordForm 0 2) ≃ₐ[ℝ] ℍ[ℝ] (Layer 7), the first two entries of the Bott table; and \(\mathrm{Cliff}(1,1) \cong M_2(\mathbb{R})\), the periodicity step.

For \(V = \mathbb{C}^3\), spinGroup Q ≃* SL(2, ℂ) (Layer 6), with the \(2\)-dimensional spin representation spinRep Q W the standard representation of \(SL_2\) (finrank ℂ (ExteriorAlgebra ℂ W) = 2, \(\dim W = 1\)). Over \(\mathbb{R}\), Spin(3) ≅ SU(2), the double cover of \(SO(3)\) with kernel \(\{\pm 1\}\) (Layer 2), the smallest instance of the whole theory.

For type \(B_l\), spinRep Q W is irreducible of dimension \(2^l\) with highest weight \(\omega_l = \tfrac12(1, \ldots, 1)\) (Layers 4-5), and its weights are exactly the \(2^l\) half-integer sign vectors \(\tfrac12(\pm 1, \ldots, \pm 1)\). Acceptance: finrank ℂ (ExteriorAlgebra ℂ W) = 2 ^ l, and the highest weight is the last fundamental weight of \(B_l\), lying in the half-integral coset and outside the lattice generated by the vector weights \(\pm e_i\) (the lattice containing every weight of every tensor power of the standard module), which is the precise obstruction to being a tensor-power constituent.

For \(V = \mathbb{C}^8\) (type \(D_4\)), \(S^+\) and \(S^-\) are irreducible of dimension \(8\), equal to \(\dim V\); trialityAut (Layer 8) is an order-three automorphism of Spin₈ cyclically permuting \(V, S^+, S^-\), and the trilinear form \(V \otimes S^+ \otimes S^- \to \mathbb{C}\) is Spin₈-invariant. Acceptance: trialityAut ^ 3 = 1, trialityAut ≠ 1, and the three \(8\)-dimensional representations are cyclically permuted.

Under the commutator action, \(\bigwedge \mathfrak{sl}_2 \cong 1 \oplus V(2) \oplus V(2) \oplus 1\) (dimensions \(1 + 3 + 3 + 1 = 8 = 2^3\)), not isotypic; under left multiplication, Cliff(𝔰𝔩₂, κ) is four copies of one \(2\)-dimensional simple (\(d = 3\), \(l = 1\): simple dimension \(2^{(3-1)/2} = 2\), multiplicity \(2^{(3+1)/2} = 4\)). The pair is the acceptance check that the two actions are truly kept apart.

For \(\mathfrak{g} = \mathfrak{gl}_N\) with the trace form: the CAR relations from the polar-form pin (\(2\,\delta_{bc}\,\delta_{ad}\)), the \(\mathfrak{gl}_N\) relations \([F_{ij}, F_{kl}] = \delta_{jk} F_{il} - \delta_{li} F_{kj}\) from glCliffordHom, the normal-ordering constant \(\frac{N}{2}\,\delta_{ij}\), and the isotypic decomposition of the left-regular Cliff(M_N) into \(2^{N(N+1)/2}\) simples of dimension \(2^{N(N-1)/2}\) with highest weight \(\nu = (N - \tfrac12, \ldots, \tfrac12)\). Acceptance arithmetic: \(2^{N(N-1)/2} \cdot 2^{N(N+1)/2} = 2^{N^2} = \dim \bigwedge (M_N)\), and the \(d \pm l\) bookkeeping \(d + l = N^2 + N\), \(d - l = N^2 - N = 2 \cdot \#\Delta^+\).

The core summit of this roadmap is the complex spin representation theory: the hyperbolic Clifford module \(\bigwedge\! W\) (Layer 4), the \(\mathfrak{so}(V)\)-action through bivectors (Layer 3), irreducibility and the half-spin splitting (Layer 4), and the highest weights for \(B_l/D_l\) (Layer 5). Layer 0 (the algebra and the two gradings) is the algebraic foundation and comes first; the filtration and the PBW-type associated graded are used throughout. The structure theorem of Layer 1 is proved forward from the spin module; there is no reverse dependency and no circular use of a separately proved structure theorem. Layer 2 (the Pin/Spin double covers) needs Layer 0's grading, the vector equivalence ιRangeEquiv, and Cartan–Dieudonné diagonalization; its surjectivity (over \(\mathbb{C}\)) is the single hardest target. Layer 3 (\(\mathfrak{so}(V) \cong \bigwedge^2 V\)) needs Layer 0 and gives the differential of Layer 2; it is the interface to the highest-weight roadmap. Layer 5 needs Layers 3-4 and the highest-weight theory; Layer 6 needs Layers 4-5; Layer 7 needs Layer 1 and Layer 2, specialized to \(\mathbb{R}\); Layer 8 needs Layer 5 and the \(D_4\) diagram automorphism; Layer 9 needs Layer 0's filtration vocabulary, restates Layer 3's realization for an abstract nondegenerate form, consumes Layer 4's spinAction for its spin-module variant, and is independent of Layers 6-8 — so a contributor can reach Kostant's isotypy corollary directly from the core summit.