Let \(K\) be a commutative ring, let \(V\) be a \(K\)-module, and let \(Q\) be a quadratic form. Polarization data consists of isotropic submodules \(W,W'\subseteq V\), an orthogonal remainder \(L\), and a linear equivalence \[(W\oplus W')\oplus L\simeq V.\] The polar form identifies \(W'\) with \(W^*\); the pairing is separating in both variables. A coordinate \(\ell :L\to K\) is injective and satisfies \(\ell (z)^2=Q(z)\). Thus \(L\) is an orthogonal remainder equipped with an injective coordinate. Over a field it is at most one-dimensional; it vanishes in the classical even split model. The carrier of the exterior spinor model is \[S=\bigwedge _K W.\]

Chevalley treats complementary totally singular subspaces in the split, even-dimensional field case. Meinrenken uses the equivalent Lagrangian model \(V=F^*\oplus F\) [meinrenken2013clifford, Section 3.2.2, Proposition 3.5, pp. 56--57]. The packaged remainder and commutative-ring hypotheses are TauCeti's stated generalization.

Let \(Q\) be a quadratic form on a module \(V\) over a commutative ring \(K\). Write \[B_Q(u,v)=Q(u+v)-Q(u)-Q(v)\] for its unhalved polar form, and reserve \(\iota _Q:V\to \mathcal {C}\kern -2pt\ell (Q)\) for the canonical Clifford generator map. Then \[\iota _Q(u)\iota _Q(v)+\iota _Q(v)\iota _Q(u) =B_Q(u,v)1.\] If \(2\) is invertible, write \(b_Q=\tfrac 12B_Q\); the same relation is then \(\{\iota _Q(u),\iota _Q(v)\}=2b_Q(u,v)1\). No use of \(b_Q\) is made when division by two is unavailable.

For polarization data \(V\simeq (W\oplus W')\oplus L\) and \(S=\bigwedge _K W\), the definitions are in Definition 3. Write \(\varepsilon _x:S\to S\) for creation, \(a_y=\iota _{\varphi _y}:S\to S\) for contraction, \(\alpha :S\to S\) for parity, \(\lambda _z:S\to S\) for the orthogonal-line action, and \(c(v):S\to S\) for the assembled Clifford operator. In particular, \[a_y\varepsilon _x+\varepsilon _xa_y =B_Q(x,y)\operatorname {id}_S.\] This is the normalization of TauCeti.SpinPolarizationData.contract_wedge; the assembled square \(c(v)^2=Q(v)\operatorname {id}_S\) is TauCeti.SpinPolarizationData.cliffordOperator_sq. The contracted notation \(\iota _y\) in Lemma 4 and Example 9 is a legacy alias for \(a_y=\iota _{\varphi _y}\); it does not denote the generator map \(\iota _Q\).

The source conventions translate as follows. Fulton--Harris use a symmetric bilinear form \(Q_{\mathrm {FH}}\) and write the anticommutator as \(2Q_{\mathrm {FH}}\); their contraction functional is also \(2Q_{\mathrm {FH}}(-,w')\) [fulton2004representation, Section 20.1, (20.1), Lemma 20.9 and (20.11), pp. 301, 304--305]. Meinrenken likewise starts from \(B\) with Clifford relation \(2B\) and, after choosing \(V=F^*\oplus F\), acts on \(\bigwedge F^*\) by creation from \(F^*\) and contraction from \(F\) [meinrenken2013clifford, Section 3.2.1--3.2.2, Proposition 3.5, pp. 55--57]. Thus \(Q_{\mathrm {FH}}=B=b_Q\) whenever \(b_Q\) exists. Goodman--Wallach instead name the anticommutator form \(\beta \); under their identification \(W_{\mathrm {GW}}^*=W\) and \(W_{\mathrm {GW}}=W'\), one has \(\beta =B_Q\) [goodman2009symmetry, Definition 6.1.1 and Theorem 6.1.3, proof, pp. 302, 304--305]. The formulas agree after these substitutions; the different letters do not signal different Clifford actions.

Let \(P\) be polarization data as in Definition 1, over a commutative ring \(K\), and set \(S=\bigwedge _K W\). For \(x\in W\), creation is exterior multiplication \[\varepsilon _x(s)=x\wedge s.\] For \(y\in W'\), let \(\varphi _y(x)=B_Q(x,y)\). Annihilation is contraction against this functional, \[a_y(s)=\iota _{\varphi _y}(s).\] If \(z\in L\), its operator is \[\lambda _z=\ell (z)\,\alpha ,\] where \(\alpha (s)=(-1)^r s\) for homogeneous \(s\in \bigwedge ^r W\). The Clifford operator attached to the decomposed vector \(v=x+y+z\) is therefore \[c(v)=\varepsilon _x+a_y+\lambda _z.\]

These symbols separate three maps that sources often denote similarly. The canonical generator map is \(\iota _Q:V\to \mathcal {C}\kern -2pt\ell (Q)\); the representation then satisfies \[\rho (\iota _Q(x))=\varepsilon _x,\qquad \rho (\iota _Q(y))=a_y,\qquad \rho (\iota _Q(z))=\lambda _z.\] Thus contraction is an operator on \(S\), not another use of the symbol for the Clifford generator. The normalization and source dictionary are fixed in Convention 2.

Chevalley obtains creation and contraction from left multiplication on a minimal ideal: one totally singular summand acts by exterior multiplication, and the complementary summand by antiderivations [chevalley1954algebraic, II.2.1--II.2.2, pp. 42--44]. Meinrenken's Lagrangian-complement construction gives the same pair as \(\varepsilon (\mu )+\iota (v)\) [meinrenken2013clifford, Section 3.2.2, Proposition 3.5, p. 57]. Fulton--Harris independently writes the two actions as exterior multiplication and derivation, with the derivation paired by their anticommutator form [fulton2004representation, Section 20.1, Lemma 20.9 and (20.11), pp. 304--305]. Fulton--Harris and Goodman--Wallach extend the model in odd dimension by sending a normalized orthogonal generator to parity [fulton2004representation, Lemma 20.16, p. 306], and [goodman2009symmetry, Theorem 6.1.3, proof, p. 305]. TauCeti packages this last step as the supplied coordinate \(\ell :L\to K\), so that every \(z\in L\) acts by \(\ell (z)\alpha \). Chevalley's cited result is the field case of maximal index; Meinrenken assumes a field of characteristic different from two, a split form, and a chosen Lagrangian complement; Fulton--Harris and Goodman--Wallach work with finite-dimensional nondegenerate complex spaces and chosen maximal isotropics. Once \(P\) is supplied, the four displayed TauCeti operators require no additional field, finite-dimensionality, nondegeneracy, or division-by-two hypothesis.

Creation and contraction satisfy \[\iota _y\varepsilon _x+\varepsilon _x\iota _y =B_Q(x,y)\operatorname {id}_S.\] Creation and contraction each square to zero. Parity anticommutes with both, while \(\lambda _z^2=Q(z)\operatorname {id}_S\). Consequently the operator \(c(v)\) assembled from the three polarization coordinates obeys \[c(v)^2=Q(v)\operatorname {id}_S.\] This is the quadratic form of the usual polarized anticommutation relation \(c(v)c(w)+c(w)c(v)=B_Q(v,w)\). Meinrenken states the latter as the defining condition for a Clifford module.

The square relation of Lemma 4 extends uniquely to an algebra homomorphism \[\rho :\mathcal {C}\kern -2pt\ell (Q)\longrightarrow \operatorname {End}_K(S).\] On the three summands it is determined by \[\rho (\iota (x))s=x\wedge s,\qquad \rho (\iota (y))s=\iota _y(s),\qquad \rho (\iota (z))s=\ell (z)\alpha (s).\] The corresponding formalized equations are TauCeti.spinAction_ι_wedge, TauCeti.spinAction_ι_contract, and TauCeti.spinAction_ι_lineOperator. Chevalley's split even-dimensional model has no remainder term; the third formula is TauCeti's odd-line extension of that construction.

Assume that \(W\) is finite and free over the commutative ring \(K\). The subalgebra of \(\operatorname {End}_K(\bigwedge W)\) generated by all creation operators and all contractions is the whole endomorphism algebra. Since the polar pairing identifies \(W'\) with \(W^*\), these generators lie in the image of the exterior Clifford action. Hence \[\rho :\mathcal {C}\kern -2pt\ell (Q)\twoheadrightarrow \operatorname {End}_K(\bigwedge W)\] is surjective.

Meinrenken proves generation first in rank one by four matrix units and then by tensor decomposition. Over a split field he combines surjectivity with a dimension calculation to obtain an isomorphism and irreducibility. TauCeti formalizes the generation and surjectivity statements over a finite free module. This card does not claim that \(S\) is irreducible, or that \(\rho \) is injective.

The groups \(\operatorname {Spin}(Q)\) and \(\operatorname {Pin}(Q)\) consist of units in the Clifford algebra. Restricting the action \(\rho \) of Theorem 5 along these two inclusions gives representations on the same exterior carrier: \[\operatorname {spinRep}:\operatorname {Spin}(Q)\longrightarrow \operatorname {Aut}_K(S), \qquad \operatorname {pinRep}:\operatorname {Pin}(Q)\longrightarrow \operatorname {Aut}_K(S).\] Meinrenken calls the restriction of a Clifford module to the Clifford group the spin representation. The definitions here require only the commutative ring, module, quadratic form, and polarization data already used for \(\rho \); no nondegeneracy or finite-dimensionality is added.

For every \(g\in \operatorname {Spin}(Q)\) and \(h\in \operatorname {Pin}(Q)\), the two representations act through their underlying Clifford units: \[\operatorname {spinRep}(g)=\rho (g),\qquad \operatorname {pinRep}(h)=\rho (h).\] Thus the group actions introduce no new formula on \(S\); they are the same Clifford action with a smaller domain. In particular, any equation proved for the action of the underlying Clifford element applies to its Spin or Pin restriction.

Let \(K\) be a commutative ring in which \(2\) is invertible, and consider polarization data for which \(W=Ke\) is free of rank one. Let \(e'\in W'\) be the dual vector, so \(B_Q(e,e')=1\). Following Convention 2, put \(c=\varepsilon _e\) and \(a=a_{e'}=\iota _{e'}\); the last expression uses the legacy contraction notation. In the ordered basis \((1,e)\) of \(S=\bigwedge W\), \[c=\begin {pmatrix}0&0\\1&0\end {pmatrix}, \qquad a=\begin {pmatrix}0&1\\0&0\end {pmatrix}.\] Thus \(c^2=a^2=0\), \(ca+ac=I_2\), and \[ac=\begin {pmatrix}1&0\\0&0\end {pmatrix}=E_{00}, \quad a=E_{01},\quad c=E_{10},\quad ca=\begin {pmatrix}0&0\\0&1\end {pmatrix}=E_{11}.\] These are all four matrix units of \(\operatorname {End}_K(S)\).

The product \[N:=ca\] is the one-mode number operator: \(N(1)=0\) and \(N(e)=e\). Centering its two eigenvalues gives \[H:=N-\tfrac 12 I_2 =\begin {pmatrix}-\tfrac 12&0\\0&\tfrac 12\end {pmatrix}.\] In several modes, \(N_i=c_i a_i\) tests whether the \(i\)-th exterior coordinate is occupied, and \(H_i=N_i-\frac 12\) is the diagonal operator used in Theorem 14.

Over his characteristic-not-two field, Meinrenken supplies the general creation--contraction exterior model [meinrenken2013clifford, Proposition 3.5, p. 57] and the normal-ordered isomorphism onto the full endomorphism space [meinrenken2013clifford, Remark 3.5 and (3.6), p. 60]. The four matrices above are the direct rank-one specialization made here. The centered occupation operator independently appears in the Fulton--Harris calculation [fulton2004representation, Proposition 20.15, proof, pp. 305--306].

The occupation identity for every exterior basis vector is TauCeti.SpinPolarizationData.wedge_contract_dualVector_basis, and the general finite-free statement that the Clifford action reaches every endomorphism is TauCeti.spinAction_surjective. The displayed \(2\times 2\) matrices and their labels \(E_{rs}\) are a basis calculation, not separately named formal declarations.

Let \(K\) be a field of characteristic different from \(2\), and let \(V\) be a finite-dimensional split quadratic space with a chosen polarization \(V=W\oplus W'\) into complementary isotropic subspaces. Put \(\dim _KW=\ell \), choose polar-dual bases \(e_i\in W\) and \(e_i'\in W'\) with \(B_Q(e_i,e_j')=\delta _{ij}\), and set \(S=\bigwedge W\). In the notation of Convention 2, write \[c_i=\varepsilon _{e_i},\qquad a_i=a_{e_i'},\qquad N_i=c_i a_i,\qquad P_0=\prod _i(1-N_i)=\prod _i a_i c_i.\] The commuting idempotents \(N_i\) record occupation, so \(P_0\) is the projection onto the vacuum line \(K1\). For increasing subsets \(I=\{i_1<\cdots <i_p\}\) and \(J=\{j_1<\cdots <j_q\}\), put \[c_I=c_{i_1}\cdots c_{i_p},\qquad a_J=a_{j_q}\cdots a_{j_1},\qquad F_{I,J}=c_IP_0a_J.\] The reversed contraction order is essential. If \(e_K\) denotes the increasing exterior basis vector, then \[F_{I,J}(e_K)=\delta _{J,K}e_I,\qquad F_{I,J}F_{K,L}=\delta _{J,K}F_{I,L}.\] Indeed, \(a_J(e_J)=1\). A missing index makes the contraction zero, while a properly larger \(K\) leaves positive exterior degree and is killed by \(P_0\). Finally \(c_I(1)=e_I\). Thus the \(F_{I,J}\) are all matrix units in the image of the Clifford action. This is the multimode extension of the rank-one calculation in Example 9.

The matrix units prove surjectivity, and the dimension equality \[\dim _K\mathcal {C}\kern -2pt\ell (Q)=2^{2\ell }=(2^\ell )^2 =\dim _K\operatorname {End}_K(S)\] then proves injectivity. Hence \[\mathcal {C}\kern -2pt\ell (Q)\simeq \operatorname {End}_K(S).\] This full equivalence is formalized by TauCeti.spinAction_bijective and TauCeti.SpinPolarizationData.cliffordEquivEnd. The displayed multi-index matrix units are the basis calculation supplied here, not a separately named declaration.

Every factor in \(P_0\) is even, so the Clifford parity of \(F_{I,J}\) is \(|I|+|J|\) modulo \(2\). The even matrix units are therefore exactly those with \(|I|\equiv |J|\pmod {2}\); they span the two diagonal blocks and give \[\mathcal {C}\kern -2pt\ell (Q)^0\simeq \operatorname {End}_K(S^+)\oplus \operatorname {End}_K(S^-),\qquad S^+=\bigwedge ^{\mathrm {even}}W,\quad S^-=\bigwedge ^{\mathrm {odd}}W.\] The exact formal block equivalence is TauCeti.SpinPolarizationData.evenCliffordEquivProdEnd. If \(\ell \geq 1\), each block has size \(2^{\ell -1}\) and each parity summand is simple for its full endomorphism block TauCeti.SpinPolarizationData.evenCliffordEquivProdMatrix. For \(\ell =0\), the full action still identifies \(K\) with \(\operatorname {End}_K(K)\), but \(S^-=0\) and is not called a simple summand.

At the group level, the block calculation alone does not prove irreducibility after restriction to \(\operatorname {Spin}(Q)\). When \(K\) is additionally separably closed and \(\ell \geq 1\), the formal Spin-spanning argument gives the two irreducible half-spin representations TauCeti.isIrreducible_spinPlusSubrep TauCeti.isIrreducible_spinMinusSubrep. This is stronger input than the occupation weights of Theorem 14.

[fulton2004representation, Lemma 20.9 and (20.13), pp. 304--305] derive the full complex action and its two exterior-parity blocks; their bilinear form is the half-polar form \(b_Q\), so their contraction coefficient \(2Q_{\mathrm {FH}}\) is our \(B_Q\).

[meinrenken2013clifford, Section 3.2.4, Theorem 3.3 and (3.5)--(3.6), pp. 59--60] give the split action as a superalgebra isomorphism and prove it by the rank-one tensor calculation; their creation space \(F^*\) is our \(W\) and their bilinear form is \(b_Q\).

[goodman2009symmetry, Theorem 6.1.3, proof, pp. 304--305] independently obtain the complex creation--contraction carrier; their creation space \(W_{\mathrm {GW}}^*\) is our \(W\), and their form \(\beta \) is our unhalved \(B_Q\). The formula \(F_{I,J}=c_IP_0a_J\) synthesizes these arguments in the fixed FCAP order rather than quoting one source verbatim.

Work over \(\mathbb C\) with \(V=W\oplus W'\oplus \mathbb C z\), where \(W,W'\) are polar-dual isotropic spaces of dimension \(\ell \), \(z\) is orthogonal to them, and \(Q(z)=1\). On \(S=\bigwedge W\), the two Clifford actions agree on \(W\oplus W'\) and differ on the last generator: \[\rho _+(\iota _Q(z))=\alpha ,\qquad \rho _-(\iota _Q(z))=-\alpha ,\] where \(\alpha \) is exterior parity. For polar-dual bases, normalize the hyperbolic chirality element by \[\Gamma =\prod _{i=1}^{\ell } \bigl (1-2\iota _Q(e_i)\iota _Q(e_i')\bigr ).\] The even-dimensional action sends \(\Gamma \) to \(\prod _i(1-2N_i)=\alpha \). Moreover \(\Gamma ^2=1\), and \(\Gamma \) anticommutes with every hyperbolic vector. Consequently \[\chi =\Gamma \iota _Q(z),\qquad \chi ^2=1\] is central in \(\mathcal {C}\kern -2pt\ell (Q)\). The complementary central idempotents \[p_+=\frac {1+\chi }{2},\qquad p_-=\frac {1-\chi }{2}\] satisfy \[\rho _+(p_+)=1,\quad \rho _+(p_-)=0,\qquad \rho _-(p_+)=0,\quad \rho _-(p_-)=1.\] Thus each odd action has a visible nonzero kernel.

The central idempotents also identify the whole algebra, rather than only showing a dimension mismatch. Given \(A\in \operatorname {End}_{\mathbb C}(S)\), the preceding theorem supplies a hyperbolic Clifford element \(a\) with common image \(A\). Therefore the joint map obeys \[(\rho _+,\rho _-)(p_+a)=(A,0),\qquad (\rho _+,\rho _-)(p_-a)=(0,A).\] It is surjective. Since \[\dim _{\mathbb C}\mathcal {C}\kern -2pt\ell (Q)=2^{2\ell +1} =2\dim _{\mathbb C}\operatorname {End}_{\mathbb C}(S),\] it is an isomorphism \[\mathcal {C}\kern -2pt\ell (Q)\simeq \operatorname {End}_{\mathbb C}(S)\oplus \operatorname {End}_{\mathbb C}(S).\] The corresponding abstract two-block existence theorem is CliffordAlgebra.nonempty_algEquiv_matrix_prod_of_finrank_eq_two_mul_add_one. The explicit joint-map proof determines how the two actions select its summands.

The restrictions \(\rho _+|_{\mathcal {C}\kern -2pt\ell (Q)^0}\) and \(\rho _-|_{\mathcal {C}\kern -2pt\ell (Q)^0}\) are parity-conjugate. When \(\ell \geq 1\) they are unequal, as the Spin element below shows; for \(\ell =0\) both are the same scalar action. For every even Clifford word, the number of hyperbolic factors has the same parity as the number of \(z\)-factors. Conjugation by \(\alpha \) contributes exactly that sign, so \[\rho _-(x)=\alpha \rho _+(x)\alpha ^{-1} \qquad (x\in \mathcal {C}\kern -2pt\ell (Q)^0).\] If \(\rho _+(x)=0\), conjugacy makes both coordinates of the joint isomorphism zero, hence \(x=0\). The even source and target have the same dimension, so either restriction is an isomorphism \[\mathcal {C}\kern -2pt\ell (Q)^0\simeq \operatorname {End}_{\mathbb C}(S).\] This faithful range is formalized by TauCeti.evenSpinAction_surjective and TauCeti.SpinPolarizationData.evenCliffordEquivEnd.

When \(\ell \geq 1\), exterior parity is not a decomposition into invariant odd-dimensional Spin modules. Fix \(i\), put \(u=e_i+e_i'\), and note \(Q(u)=Q(z)=1\). The even product \[g=\iota _Q(z)\iota _Q(u)\in \operatorname {Spin}(Q)\] belongs to the actual Spin carrier by the norm-one pair criterion CliffordAlgebra.ι_mul_ι_mem_spinGroup_of_norm_mul_norm_eq_one. Its plus action is \(\alpha (c_i+a_i)\) and satisfies \[1\longmapsto -e_i,\qquad e_i\longmapsto 1.\] Its minus action is the negative of this operator. Thus the two even restrictions are unequal, and this actual Spin element exchanges even and odd exterior degree. For \(\ell =0\), the carrier \(S\) is one-dimensional and \(S^-=0\); no two-summand parity claim is made.

[fulton2004representation, Lemma 20.16 and (20.18), p. 306] give the odd complex product algebra and the faithful even restriction. Their second full-Clifford module is written on \(\bigwedge W'\), rather than as a second sign on the same carrier.

[goodman2009symmetry, Theorem 6.1.3, proof, pp. 304--305] construct the exterior carrier. [goodman2009symmetry, Lemma 6.1.4(3), p. 306] put the two normalized odd-vector signs on this common carrier. This supplies the common-carrier translation used above.

[meinrenken2013clifford, Section 3.2.4, (3.5), p. 60] supplies the normalized chirality product on the hyperbolic block. His Theorem 3.3 is an even split theorem, not an odd product theorem. The two-idempotent conclusion here is restricted to the split complex setting; an odd Clifford center over a general real field need not split.

Let \(W=\mathbb C^m\), \(m\geq 1\), with ordered basis \(e_1,\ldots ,e_m\), and use the exterior action on \(S=\bigwedge W\) from Theorem 10. Write \([u]_{\mathrm {top}}\) for the coefficient of \(e_1\wedge \cdots \wedge e_m\), and let \(r\) reverse exterior products: \(r|_{\wedge ^kW}=(-1)^{k(k-1)/2}\). Then \[B(s,t)=[r(s)\wedge t]_{\mathrm {top}},\qquad B(t,s)=\epsilon _e B(s,t),\qquad \epsilon _e=(-1)^{m(m-1)/2}\] defines a nondegenerate complex bilinear Spin-invariant form in dimension \(2m\). It pairs complementary degrees. Hence for even \(m\) it restricts nondegenerately to each half-spin module; for odd \(m\) it pairs the two halves perfectly and vanishes on either half alone. In dimension \(2m+1\), use the odd action Proposition 11 and the adjusted form \[B_o(s,t)=B(\alpha ^m s,t),\qquad B_o(t,s)=\epsilon _o B_o(s,t),\qquad \epsilon _o=(-1)^{m(m+1)/2},\] where \(\alpha |_{\wedge ^kW}=(-1)^k\). This form is again nondegenerate and Spin-invariant.

In the exterior basis the matrix of \(B\) has one entry \(\pm 1\) in each row and column, pairing an index set with its complement; this proves nondegeneracy. The underlying perfect wedge pairing has the formal counterpart exteriorPower.instIsPerfPairWedgePairing, for complementary exterior powers of a finite free module over a commutative ring with a chosen top-degree trivialization. Reversal supplies the additional signs here. For degrees \(k\) and \(m-k\), commuting the two wedge factors and comparing their reversal signs gives \(\epsilon _e\). Also \(B(\alpha s,t)=(-1)^mB(s,\alpha t)\), proving the stated odd flip sign.

Every creation and contraction operator is self-adjoint for \(B\): \[B(c_i s,t)=B(s,c_i t),\qquad B(a_i s,t)=B(s,a_i t).\] For creation, \(r(e_i\wedge s)=r(s)\wedge e_i\). For contraction on degree \(k\), \(r(a_i s)=(-1)^{k-1}a_i r(s)\). Apply the contraction derivation rule to \(r(s)\wedge t=0\) in degree \(m+1\); its two terms give the second identity. All other degree combinations vanish on both sides. Thus \(B(\rho (x)s,t)=B(s,\rho (\operatorname {rev}x)t)\). The reverse-norm-one condition in Remark [fcap-0028] proves invariance under the actual Spin group. For \(B_o\), every hyperbolic vector has adjoint sign \((-1)^m\), because it anticommutes with \(\alpha \); the extra generator \(\alpha \) has the same sign. These signs cancel on even words, giving the same reversion identity and Spin invariance.

These bilinear forms also determine conjugate-linear structures for the compact real form \(\operatorname {Spin}(n,0)\), where \(n=2m\) or \(2m+1\). Give \(S\) the positive Hermitian form \(H(s,t)=\overline {s}^{\,T}t\) in the exterior basis, conjugate-linear in its first argument. The operators \(c_i+a_i\), \(i(c_i-a_i)\), and, in odd dimension, \(\alpha \), are self-adjoint, square to \(1\), and anticommute pairwise. They realize the positive real Clifford generators. Consequently reversion is Hermitian adjunction on this real algebra, and \(H\) is Spin-invariant.

Let \(M\) be the real signed permutation matrix of \(B\) or \(B_o\), and let \(\epsilon \) be its flip sign. Then \[J(s)=M^T\overline {s},\qquad H(Js,t)=s^TMt,\qquad J^2=\epsilon \,1.\] Indeed, \(M^T=\epsilon M\) and \(MM^T=1\). Invariance of both forms and nondegeneracy of \(H\) imply that \(J\) commutes with compact Spin. Writing \(\mathcal B\) for the chosen bilinear form, the comparison is the following commuting triangle of complex linear maps:

For \(\epsilon =1\), \(J\) is a real structure as in Example [fcap-003W], and its fixed vectors form a real Spin module whose complexification is \(S\) Representation.IsRealStructure.isRealForm. Explicitly, \[s=\frac {s+Js}{2}+i\frac {s-Js}{2i},\] with both displayed components fixed by \(J\). For \(\epsilon =-1\), \(J\) is a quaternionic structure: a conjugate-linear equivariant map squaring to \(-1\) Representation.IsQuaternionicStructure. It has no nonzero fixed vector; together with multiplication by \(i\) it gives the quaternion relations on the underlying real space.

To apply this to irreducible compact spinors, the restriction to Spin needs justification. Every even monomial in an orthonormal positive real Clifford basis has reverse norm one and lies in Spin. Such monomials span the real even algebra, hence their complex span is the complex even algebra. Therefore the block descriptions in Theorem 10 and Proposition 11 give irreducible compact half-spin modules in even dimension and an irreducible compact spin module in odd dimension. The even-dimensional halves are inequivalent because their two matrix blocks have different central supports.

In even dimension \(n=2m\), \(J\) preserves each half when \(m\) is even and exchanges them when \(m\) is odd. In the latter case no equivariant conjugate-linear bijection of one half to itself can exist: composing it with \(J\) would give a complex linear equivalence between the inequivalent halves. Thus the compact types follow directly from the two flip signs: \[\begin {array}{c|c} n\bmod 8&\text {type of an irreducible complex spinor}\\\hline 0,1,7&\text {real}\\ 3,4,5&\text {quaternionic}\\ 2,6&\text {two conjugate, inequivalent half-spin modules} \end {array}\] In the even rows the statement applies to each half-spin module. The general passage from an invariant nondegenerate complex bilinear form, symmetric or alternating, and a supplied positive definite invariant Hermitian form to a real or quaternionic structure is formalized, for finite-dimensional irreducible complex representations, by Representation.exists_isRealStructure_of_isInvariantForm_of_isInvariantSesqForm and Representation.exists_isQuaternionicStructure_of_isInvariantForm_of_isInvariantSesqForm. The explicit \(M\), odd adjustment, and compact residue calculation are the exterior-basis proof above.

The reversal pairing and its covariance are [meinrenken2013clifford, Section 3.4, Definition 3.6, Example 3.5, and Proposition 3.14, pp. 66--67]. The compact reality classification agrees with [lawson2016spin, Chapter I, items 5.12--5.16, pp. 35--37]. Their negative-square Clifford convention is translated in Proposition 13. The positive Hermitian argument here is specific to the compact real form; it does not assign the same types to other signatures.

Let \(A=M_d(D)\), where \(d\geq 1\) and \(D\in \{\mathbb R,\mathbb C,\mathbb H\}\), regarded as a real algebra. Its unique irreducible real left module is \(U=D^d\), with commutant \(D^{\mathrm {op}}\) acting by right multiplication. Its complexification has the following form: \[\begin {array}{c|c|c|c} D&A\otimes _{\mathbb R}\mathbb C&U\otimes _{\mathbb R}\mathbb C &\dim _{\mathbb C}S\\\hline \mathbb R&M_d(\mathbb C)&S&d\\ \mathbb C&M_d(\mathbb C)\oplus M_d(\mathbb C)&S\oplus \overline S&d\\ \mathbb H&M_{2d}(\mathbb C)&S\oplus S&2d \end {array}\] In the complex row, the two summands have different central supports; in the quaternionic row, they are isomorphic. For a product of real matrix algebras, first select one simple block. These statements apply to irreducible real Spin modules obtained from even Clifford algebras because the actual Spin group spans the even algebra.

For the matrix-module assertion, the idempotents \(E_{ii}\) split any module into its coordinate corners, and \(E_{ij}\) identify the corners with one another. A simple module therefore has a simple \(D\)-module in its first corner, which is one-dimensional over the division algebra \(D\); this gives \(D^d\). For an endomorphism commuting with the full algebra, the matrix units make all coordinate maps the same. Commutation with the \(D\)-valued diagonal entries makes this common map \(f\) left \(D\)-linear, so \(f(x)=xf(1)\). It is therefore right multiplication by a single element on every coordinate. With \(R_a(u)=ua\), composition is \(R_aR_b=R_{ba}\), explaining the opposite algebra. Conjugation identifies \(D^{\mathrm {op}}\) with \(D\) when only its real algebra type is recorded. This is the real matrix-module classification of [lawson2016spin, Chapter I, Theorem 5.6, pp. 31--32]. The matrix-corner reconstruction has the general formal counterpart ModuleCat.matrixEquivalence, an equivalence between modules over a ring and modules over its matrix ring with a finite nonempty index type. The three real types and their commutants are the specializations calculated here.

The real row complexifies by entrywise scalar extension; conjugation is the resulting real structure. For the other rows, give \(U\) the complex structure \(u\mapsto ui\). The complexification of an underlying real complex space decomposes as \(S\oplus \overline S\), the two eigenspaces of this operator after scalar extension. For \(D=\mathbb C\), the central element \(i1\) acts as \(i\) on one summand and \(-i\) on the other. They are therefore inequivalent. For \(D=\mathbb H\), right multiplication \(J(u)=uj\) commutes with the left algebra action and obeys \(J(uz)=J(u)\overline z\) and \(J^2=-1\). Thus it identifies \(\overline S\) with \(S\). The quaternion matrix embedding Quaternion.toComplexMatrix_apply sends \(1,i,j,k\) to a complex basis of \(M_2(\mathbb C)\). Scalar extension consequently gives \(\mathbb H\otimes _{\mathbb R}\mathbb C\simeq M_2(\mathbb C)\) and then the displayed matrix algebra for general \(d\). Its action on \(S\) is the defining simple module of complex dimension \(2d\).

Here is the promised group-to-algebra bridge in every nondegenerate real signature. Choose orthogonal Clifford generators \(e_i\) with \(e_i^2=\varepsilon _i\in \{1,-1\}\). The real span \(L\) of Spin is a unital subalgebra, since products of linear combinations expand into linear combinations of group products. For \(i\ne j\) with \(\varepsilon _i\varepsilon _j=1\), \(e_ie_j\) itself lies in Spin by Remark [fcap-0028]. For opposite signs put \[v=\frac {5\varepsilon _i}{3}e_i+\frac 43e_j,\qquad Q(v)=\varepsilon _i,\qquad g=e_iv=\frac 53+\frac 43e_ie_j\in \operatorname {Spin}(Q).\] The last inclusion again uses \(Q(e_i)Q(v)=1\), hence the actual norm-one Lipschitz carrier. Therefore \(e_ie_j=\frac 34(g-\frac 53\,1)\in L\). All bivectors lie in \(L\); their products and \(1\) span the even Clifford algebra by its orthogonal monomial basis. Thus \[\operatorname {span}_{\mathbb R}\operatorname {Spin}(p,q)=\mathcal {C}\kern -2pt\ell ^+(p,q).\] It follows that real invariant subspaces and commuting endomorphisms for Spin are exactly those for the even algebra. TauCeti's CliffordAlgebra.span_spinGroup_eq_even_of_isSquare proves the spanning conclusion under a square-normalization hypothesis for every pair of nonisotropic vectors. That hypothesis holds for a definite real form, but fails for opposite-sign pairs. The displayed rational combination supplies the indefinite case separately.

For the compact positive form with \(n\geq 1\), the generators \(e_ie_n\), \(1\leq i<n\), square to \(-1\), anticommute, and generate the even algebra. Equality of dimensions gives \[\mathcal {C}\kern -2pt\ell ^+(n,0)\simeq \mathcal {C}\kern -2pt\ell (0,n-1).\] Combining the real classification Remark [fcap-0016] with the three rows above recovers the compact module types of Theorem 12. Lawson--Michelsohn write \(\mathcal {C}\kern -2pt\ell _n\) for our \(\mathcal {C}\kern -2pt\ell (0,n)\); their even-algebra identification and module table use this convention [lawson2016spin, Chapter I, (5.4)--(5.5) and Theorem 5.8, Table III, pp. 32--33]. Their compact Spin-spanning argument appears in Proposition 5.12, p. 36; the opposite-sign calculation above extends the linear-span argument to indefinite forms.

Signature still changes the real module type: \[\begin {aligned} \mathcal {C}\kern -2pt\ell ^+(2,2)&\simeq M_2(\mathbb R)\oplus M_2(\mathbb R),\\ \mathcal {C}\kern -2pt\ell ^+(4,0)&\simeq \mathbb H\oplus \mathbb H. \end {aligned}\] The split case gives real two-dimensional half-spin modules. The compact case gives quaternionic complex two-dimensional halves, each with real dimension four. The Lorentz even algebra \(M_2(\mathbb C)\) in Example [fcap-002L] has a real four-dimensional simple module; its complexification is the pair of inequivalent complex two-dimensional Weyl modules. Thus the compact Hermitian comparison cannot simply be reused for noncompact signatures. In all cases the scalar \(-1\in \operatorname {Spin}\) acts as \(-\operatorname {id}\), retaining the descent obstruction of Proposition [fcap-003M].

Let \(V=W\oplus W'\) be a complex nondegenerate quadratic space of dimension \(2\ell \), with \(\ell \geq 1\). The summands are maximal isotropic and dual under the polar form \(B_Q\). Choose dual bases \(w_i\in W\) and \(w_i'\in W'\) with \(B_Q(w_i,w_j')=\delta _{ij}\). On \(S=\bigwedge W\), write \(u_I\) for the wedge basis vector indexed by \(I\). The even and odd exterior degrees are \(S^+\) and \(S^-\).

The diagonal Clifford bivector of Convention [fcap-000N] \[\widehat H_i=\beta _Q(w_i,w_i') =\tfrac 12[\iota _Q(w_i),\iota _Q(w_i')]\] has factors acting by \(c_i=\varepsilon _{w_i}\) and \(a_i=a_{w_i'}\) in the notation of Convention 2. Write \(H_i\) for the resulting endomorphism of \(S\). The relation \(c_i a_i+a_i c_i=1\) gives \[N_i:=c_i a_i,\qquad H_i=N_i-\tfrac 12\operatorname {id}_S.\] Since \(N_i\) projects onto the vectors containing \(i\), \[H_i u_I=\begin {cases} \frac 12 u_I,&i\in I,\\ -\frac 12 u_I,&i\notin I. \end {cases}\] The simultaneous weight space for each sign pattern is the line \(\mathbb C u_I\) TauCeti.spinWeightSpace_spinWeight. The lines with even \(|I|\) sum to \(S^+\), and those with odd \(|I|\) sum to \(S^-\). Each half has dimension \(2^{\ell -1}\), while \(S\) has dimension \(2^\ell \).

For \(\ell =2\), the occupation test gives the complete table \[\begin {array}{c|c|c|c} I&u_I&(H_1,H_2)&\text {summand}\\ \hline \varnothing &1&(-\tfrac 12,-\tfrac 12)&S^+\\ \{1\}&w_1&(\tfrac 12,-\tfrac 12)&S^-\\ \{2\}&w_2&(-\tfrac 12,\tfrac 12)&S^-\\ \{1,2\}&w_1\wedge w_2&(\tfrac 12,\tfrac 12)&S^+ \end {array}\] Every entry is obtained by applying the two rank-one operators of Example 9; the four displayed lines exhaust \(S\) in this case.

Fulton--Harris use \(B_Q=2Q_{\mathrm {FH}}\), so their standard hyperbolic basis becomes polar-dual here after setting \(w_i=e_i\) and \(w_i'=\frac 12e_{\ell +i}\). Their represented operator is then \(L_{e_i}D_{e_i^*}-\frac 12 I=N_i-\frac 12 I\), assigning the same positive sign to an occupied coordinate [fulton2004representation, Proposition 20.15, proof, pp. 305--306]. Thus their occupation signs and even/odd exterior-degree labels agree with the displayed TauCeti axes.

Goodman--Wallach realize the complex spinor carrier as the exterior algebra of the dual isotropic space [goodman2009symmetry, Theorem 6.1.3, proof, pp. 304--305]. Identify their creation space \(W_{\mathrm {GW}}^*\) with \(W\) here, and their annihilation space \(W_{\mathrm {GW}}\) with \(W'\), taking \(w_i=e_{-i}\) and \(w_i'=e_i\).

The reversed order in [goodman2009symmetry, Lemma 6.2.2 and (6.14), p. 313] gives \[\widehat H_i^{\mathrm {Tau}}=\beta _Q(e_{-i},e_i) =-\widehat H_i^{\mathrm {GW}}.\] Accordingly, their occupied eigenvalue \(-\frac 12\) and unoccupied eigenvalue \(+\frac 12\) negate every pair in the table [goodman2009symmetry, Proposition 6.2.3, proof, pp. 314--315]. The exterior vectors and parity labels remain fixed: \(S^+\) means even \(|I|\), and \(S^-\) means odd \(|I|\). This records the occupation operators, weight lines, and parity decomposition, without a root-system, highest-weight, or irreducibility assertion.

Let \(V=W\oplus W'\) be a complex nondegenerate quadratic space with a chosen split polarization of rank \(\ell \geq 4\). Choose polar-dual bases \(e_i\in W\) and \(e_i'\in W'\) with \(B_Q(e_i,e_j')=\delta _{ij}\), and put \(S=\bigwedge W\). Write \(c_i\) for left creation by \(e_i\), \(a_i\) for contraction by \(e_i'\), \(N_i=c_i a_i\), and \[H_i=N_i-\tfrac 12.\] Thus \(\epsilon _i(H_j)=\delta _{ij}\) fixes the Cartan coordinates, and the occupation signs are those of Theorem 14. We choose \[\Phi ^+=\{\epsilon _i-\epsilon _j,\ \epsilon _i+\epsilon _j:i<j\}\] and the Borel \(\mathfrak b=\mathfrak h\oplus \bigoplus _{\alpha \in \Phi ^+}\mathfrak g_\alpha \). Equivalently, \(\mathfrak b\) stabilizes the flag \(\langle e_1\rangle \subset \langle e_1,e_2\rangle \subset \cdots \subset W\); in the ordered Witt basis \(e_1,\ldots ,e_\ell ,e_\ell ',\ldots ,e_1'\) it is the upper-triangular Borel.

For the simple roots \(\alpha _i=\epsilon _i-\epsilon _{i+1}\) along the chain and \(\alpha _\ell =\epsilon _{\ell -1}+\epsilon _\ell \) at the fork, take \[\begin {aligned} E_i&=c_i a_{i+1},&F_i&=c_{i+1}a_i && (1\leq i<\ell ),\\ E_\ell &=c_{\ell -1}c_\ell ,& F_\ell &=a_\ell a_{\ell -1}.&& \end {aligned}\] The reversed contraction order in \(F_\ell \) fixes the bracket sign. On an increasing exterior word \(u_I\), a chain operator replaces an occupied \(i+1\) by an absent \(i\), or performs the reverse replacement, with coefficient \(1\); otherwise it gives zero. The fork operators create or remove the final pair, again with coefficient \(1\), when the corresponding occupancy condition holds. The CAR then gives \[[E_i,F_i]=h_i,\qquad h_i=N_i-N_{i+1}\ (i<\ell ),\qquad h_\ell =N_{\ell -1}+N_\ell -1.\] Under the bivector map these are the products \(e_i e_{i+1}'\), \(e_{i+1}e_i'\), \(e_{\ell -1}e_\ell \), and \(e_\ell 'e_{\ell -1}'\). Distinct orthogonal factors contribute no hidden scalar term. TauCeti identifies these exact Clifford representatives with the numbered type-D matrix roots and coroots TauCeti.SpinPolarizationData.typeDQuadraticEquiv_rootGenerator TauCeti.SpinPolarizationData.typeDQuadraticEquiv_cartanGenerator.

It remains to pass from the simple roots to the chosen Borel. Put \[X_{ij}=c_i a_j,\qquad Y_{ij}=c_i c_j\qquad (i<j).\] Their Cartan weights are \(\epsilon _i-\epsilon _j\) and \(\epsilon _i+\epsilon _j\). The identities \[\begin {aligned} [X_{ij},X_{jk}]&=X_{ik},\\ [X_{i,\ell -1},Y_{\ell -1,\ell }]&=Y_{i,\ell },\\ [X_{j,\ell },Y_{i,\ell }]&=Y_{ij} \end {aligned}\] for the indicated distinct ordered indices generate every positive \(X_{ij}\) and \(Y_{ij}\) from the simple operators. These are all positive root spaces of \(\mathfrak {so}(V,Q)\), so their span is the full nilradical \(\mathfrak n^+\). In particular, a vector killed by every \(E_i\) is killed by \(\mathfrak n^+\): brackets and linear combinations preserve its annihilator. This final root-space argument supplies the Borel bridge; the formal file presently proves over \(\mathbb Q\) annihilation by the Lie span of the simple positive generators, without identifying that span with a compatible Borel TauCeti.SpinPolarizationData.typeDSpinSerreRepresentation_positiveSimpleRootLieSpan_le_lieAnnihilator.

Continue with the Cartan and Borel of Proposition 15. For the increasing exterior basis \(u_I\), set \[\Omega =u_{\{1,\ldots ,\ell \}},\qquad \widehat \Omega =u_{\{1,\ldots ,\ell -1\}}.\] Every positive chain operator kills \(\Omega \) by duplicate creation. It kills \(\widehat \Omega \) either by the same mechanism or, on the final chain edge, because the contracted last coordinate is absent. The positive fork operator kills \(\Omega \) by duplicate creation and \(\widehat \Omega \) because coordinate \(\ell -1\) is already present. The preceding root-space generation therefore makes both vectors highest for \(\mathfrak b\).

Since \(H_i\) has eigenvalue \(+\frac 12\) on an occupied coordinate and \(-\frac 12\) on an unoccupied one, their weights are \[\operatorname {wt}(\Omega ) =\omega _\ell =\tfrac 12(\epsilon _1+\cdots +\epsilon _\ell ),\] \[\operatorname {wt}(\widehat \Omega ) =\omega _{\ell -1} =\tfrac 12(\epsilon _1+\cdots +\epsilon _{\ell -1}-\epsilon _\ell ).\] The first word lies in \(S^+=\bigwedge ^{\mathrm {even}}W\) exactly when \(\ell \) is even, while the second has the opposite parity. Hence, with \(S^\pm \) defined by exterior parity as in Theorem 14, \[\begin {array}{c|cc} &S^+&S^-\\ \hline \ell \text { even}&L(\omega _\ell )&L(\omega _{\ell -1})\\ \ell \text { odd}&L(\omega _{\ell -1})&L(\omega _\ell ) \end {array}\] The parity label is therefore not an independent name for the all-plus weight.

For completeness, each displayed module is irreducible for the type-D Lie action. The commuting \(H_i\) have distinct joint eigenvalues on the one-dimensional lines \(\mathbb C u_I\), so polynomial projections in the \(H_i\) extract a nonzero basis word from any nonzero invariant subspace. The chain operators move occupied coordinates, while the fork pair creates or removes two of them. Their occupancy graph connects all subsets of a fixed parity. The invariant subspace consequently contains every basis word of that parity. This proves irreducibility without identifying it with the separate group-level theorem.

The generator calculation is already defined over \(\mathbb Q\). In the standard model set \(S_{\mathbb Q}=\bigwedge _{\mathbb Q}\mathbb Q^\ell \). The basis map \[\begin {aligned} \mathbb C\otimes _{\mathbb Q}S_{\mathbb Q} &\longrightarrow \bigwedge _{\mathbb C}\mathbb C^\ell ,\\ z\otimes u_I&\longmapsto z u_I. \end {aligned}\] is an equivalence. Every \(E_i\) and \(F_i\) above has matrix entries \(0,1,-1\); the coroot matrices are integral and the \(H_i\) matrices are half-integral. Thus these actions, their annihilation identities, and their weights commute with extension from \(\mathbb Q\) to \(\mathbb C\). A chosen complex polar-dual basis then transports the standard calculation to \(W\oplus W'\). TauCeti proves the two simple-generator annihilation statements and exact fork weights over \(\mathbb Q\) TauCeti.SpinPolarizationData.typeDSpinRep_serreE_exteriorBasis_univ_eq_zero TauCeti.SpinPolarizationData.typeDSpinRep_serreE_exteriorBasis_univ_erase_last_eq_zero TauCeti.SpinPolarizationData.isCartanWeightVector_typeDSpinRep_exteriorBasis_univ TauCeti.SpinPolarizationData.isCartanWeightVector_typeDSpinRep_exteriorBasis_univ_erase_last. The displayed scalar-extension and Borel steps explain how this rational calculation gives the complex highest-weight identities; they do not assert a packaged Lean base-change theorem.

There are also direct highest-vector counterparts over any characteristic-zero field. They use a supplied polarization with no residual line, a basis of \(W\) of rank \(n\geq 4\), and the concrete type-D Cartan and Borel: TauCeti.SpinPolarizationData.isHighestWeightVector_typeDSpinLieRep_exteriorBasis_univ TauCeti.SpinPolarizationData.isHighestWeightVector_typeDSpinLieRep_exteriorBasis_univ_erase_last. With \(n=\ell \), their zero-based Cartan dual-basis indices \(n-1\) and \(n-2\) are our \(\omega _\ell \) and \(\omega _{\ell -1}\), respectively.

The restricted declarations also retain the parity assignment in the table. In even rank, \(\Omega \in S^+\) and \(\widehat \Omega \in S^-\) TauCeti.SpinPolarizationData.isHighestWeightVector_typeDSpinPlusLieRep_exteriorBasis_univ_of_even TauCeti.SpinPolarizationData.isHighestWeightVector_typeDSpinMinusLieRep_exteriorBasis_univ_erase_last_of_even; in odd rank, \(\Omega \in S^-\) and \(\widehat \Omega \in S^+\) TauCeti.SpinPolarizationData.isHighestWeightVector_typeDSpinMinusLieRep_exteriorBasis_univ_of_odd TauCeti.SpinPolarizationData.isHighestWeightVector_typeDSpinPlusLieRep_exteriorBasis_univ_erase_last_of_odd. These assert highest vectors in the indicated modules; the occupancy argument above supplies their irreducibility.

[fulton2004representation, Proposition 20.15 and proof, pp. 305--306] independently identify the two irreducible half-spin modules and give the same parity-dependent fork assignment after the polar-dual rescaling already recorded in Theorem 14. Their occupied Cartan sign is positive, as it is here.

[goodman2009symmetry, Proposition 6.2.3, pp. 314--315] independently gives the two irreducible modules and their signed half-sum weights. Its creation space is identified with our \(W\), but its occupied Cartan sign is negative. Under \(H_i^{\mathrm {Tau}}=-H_i^{\mathrm {GW}}\) the weights and positive systems both reverse. The exterior-parity labels remain fixed; the assignment of the two fork highest weights to them must be translated with the Cartan sign and Borel.

Let \(V=W\oplus W'\oplus \mathbb C z\) be a nondegenerate quadratic space of dimension \(2\ell +1\), with \(\ell \geq 1\). Assume \(W,W'\) are complementary polar-dual isotropic spaces, \(z\) is orthogonal to both, and \(Q(z)=1\). Choose bases \(e_i,e_i'\) with \(B_Q(e_i,e_j')=\delta _{ij}\) and the plus odd action on \(S=\bigwedge W\), \[\rho (\iota _Q(z))=\alpha ,\] where \(\alpha \) is exterior parity. This sign is part of the choice: \(Q(z)=1\) alone says only that the line coordinate squares to \(1\). Write \(c_i,a_i,N_i,H_i,\epsilon _i\) as in Theorem 14.

Choose the positive roots \[\Phi ^+=\{\epsilon _i-\epsilon _j,\ \epsilon _i+\epsilon _j:i<j\} \cup \{\epsilon _i:1\leq i\leq \ell \}.\] The chain simple roots use \(E_i=c_i a_{i+1}\) and \(F_i=c_{i+1}a_i\). At the terminal short root \(\alpha _\ell =\epsilon _\ell \), take \[E_\ell =c_\ell \alpha ,\qquad F_\ell =\alpha a_\ell ,\qquad [E_\ell ,F_\ell ]=2N_\ell -1.\] The matrix short root has a coefficient \(2\) because \(B_Q(z,z)=2\); the Clifford bivector is nevertheless exactly \(e_\ell z\), with no extra factor \(\frac 12\) TauCeti.SpinPolarizationData.typeBQuadraticEquiv_typeBShortRootGenerator. On an increasing word, the terminal creation or removal sign cancels the parity sign, so the short operators insert or remove coordinate \(\ell \) with coefficient \(1\) TauCeti.SpinPolarizationData.typeBSpinRep_shortRootGenerator_apply TauCeti.SpinPolarizationData.typeBSpinRep_shortNegativeRootGenerator_apply.

This convention gives the same flag Borel as in Proposition 15. For \(i<j\), put \(X_{ij}=c_i a_j\), \(Y_{ij}=c_i c_j\), and \(K_i=c_i\alpha \). The chain commutators generate every \(X_{ij}\), while \[[X_{ij},K_j]=K_i,\qquad [K_i,K_j]=-2Y_{ij}.\] Because \(2\) is invertible over \(\mathbb C\), the simple chain operators and \(K_\ell \) generate the root spaces of every positive short and long root. They therefore generate the full positive nilradical.

The top word \[\Omega _B=e_1\wedge \cdots \wedge e_\ell \] is killed by each positive chain root and by \(E_\ell \), since the relevant creation coordinate is already occupied. The chain coroots have eigenvalue \(0\), and the terminal coroot \(2N_\ell -1\) has eigenvalue \(1\). Hence \[\operatorname {wt}(\Omega _B) =\omega _\ell =\tfrac 12(\epsilon _1+\cdots +\epsilon _\ell ).\] The chain moves together with the terminal toggle connect all exterior basis words. As in Theorem 16, the distinct joint \(H_i\)-weights first project any nonzero invariant subspace onto a basis line; the root moves then reach every line. Thus \(S\) is the irreducible type-\(B_\ell \) module \(L(\omega _\ell )\). The short root changes exterior degree, so neither \(S^+\) nor \(S^-\) is a type-B submodule.

[fulton2004representation, Proposition 20.20, p. 307] independently identifies the odd-dimensional spin representation as the irreducible module of highest weight \(\frac 12(\epsilon _1+\cdots +\epsilon _\ell )\). The preceding short-root and nilradical calculations give that conclusion in the fixed FCAP operator convention.

[goodman2009symmetry, Proposition 6.2.4, p. 315] independently gives the same irreducible type-B module and its half-sign weights. As in Theorem 14, its occupied Cartan sign is opposite ours; negating its Cartan axes and positive system gives the displayed highest weight. TauCeti formalizes the short and difference-root actions and the integral simple-coroot eigenvalues TauCeti.SpinPolarizationData.typeBSpinRep_differenceRootGenerator_apply TauCeti.SpinPolarizationData.spinAction_typeBQuadraticEquiv_typeBSimpleCorootGenerator_basis.

The top word's weight and annihilation data are available over any field with \(2\) invertible, for a supplied polarization, basis of \(W\), and residual vector \(z\) with \(Q(z)=1\). The Cartan acts on \(\Omega _B\) through the terminal fundamental weight TauCeti.SpinPolarizationData.typeBSpinLieRep_apply_cartan_exteriorBasis_univ, and the Lie subalgebra generated by all positive simple-root generators annihilates it TauCeti.SpinPolarizationData.typeBSpinLieRep_lieSpan_range_simpleRootGenerator_le_lieAnnihilator_exteriorBasis_univ. The declarations index the rank by \(n+1=\ell \); their terminal \(\operatorname {Fin.last}(n)\) labels our \(\omega _\ell \).

The general highest-vector criterion is available separately: a nonzero Cartan weight vector is highest exactly when every raising generator kills it LieAlgebra.Basis.isHighestWeightVector_iff_forall_e. It assumes a characteristic-zero field, a finite-dimensional Lie algebra with nondegenerate Killing form, and a Lie basis. For type B, the Killing condition follows when every endomorphism in the full standard action is triangularizable, in particular over \(\mathbb C\) TauCeti.isKilling_typeB. Triangularizability of the diagonal Cartan alone is not this hypothesis. The selected spin-module declarations give the weight and annihilation data, rather than a separately packaged highest-vector conclusion. The Borel-generation and irreducibility arguments above complete the displayed module identification.

Work over the complex split models and positive systems fixed in the preceding type-B and type-D cards. In type \(B_\ell \) assume \(\ell \geq 1\); in type \(D_\ell \) assume \(\ell \geq 4\). For \(I\subseteq \{1,\ldots ,\ell \}\), put \[\lambda _I=\tfrac 12\left ( \sum _{i\in I}\epsilon _i-\sum _{i\notin I}\epsilon _i\right ).\] By Theorem 14, the line \(\mathbb C u_I\) has weight \(\lambda _I\); distinct subsets give distinct weights. Consequently \[\operatorname {ch}S_{B_\ell } =\sum _I e^{\lambda _I} =\prod _{i=1}^{\ell } \left (e^{\epsilon _i/2}+e^{-\epsilon _i/2}\right ),\] and the type-D parity carriers have \[\operatorname {ch}S_D^+ =\sum _{\lvert I\rvert \ {\rm even}}e^{\lambda _I},\qquad \operatorname {ch}S_D^- =\sum _{\lvert I\rvert \ {\rm odd}}e^{\lambda _I}.\] If \(a_i=e^{\epsilon _i/2}\) and \(b_i=e^{-\epsilon _i/2}\), sorting the product by occupied parity gives \[\operatorname {ch}S_D^\pm =\tfrac 12\left [ \prod _i(a_i+b_i)\ \mathbin {\pm }\ \prod _i(b_i-a_i)\right ].\] The order \(b_i-a_i\) makes an occupied coordinate contribute the minus sign. These are finite sums obtained from the exterior basis, without invoking a general character formula.

The complete half-sum weights above become honest characters on the Spin torus. Put \(A_i=e_i e_i'\), so its action is \(N_i\). For \(t\in \mathbb C^\times \), define \[g_i(t)=tA_i+t^{-1}(1-A_i) =(t e_i+t^{-1}e_i')(e_i+e_i').\] Both vector factors have quadratic value \(1\); the pair criterion therefore puts \(g_i(t)\) in the actual Spin carrier CliffordAlgebra.ι_mul_ι_mem_spinGroup_of_norm_mul_norm_eq_one. The elements for different coordinates commute, and \[g_i(t)u_I= \begin {cases}t\,u_I,&i\in I,\\t^{-1}u_I,&i\notin I.\end {cases}\] Their vector action scales \(e_i\) by \(t^2\), \(e_i'\) by \(t^{-2}\), and fixes the other coordinates. Thus \(g(t_1,\ldots ,t_\ell )=\prod _i g_i(t_i)\) covers the standard orthogonal torus by coordinatewise squaring.

The kernel of this parameterization is \[\{(t_i):t_i\in \{1,-1\},\ \prod _i t_i=1\}.\] Indeed, equality of its spinor action with the identity forces \(t_i^2=1\) by comparing weights that differ in coordinate \(i\), and the vacuum weight then forces \(\prod _i t_i=1\). Conversely such a tuple gives the actual Clifford scalar \(\prod _i t_i=1\). Thus both implications hold directly for the group parameterization. The image contains the scalar \(-1\); together with the usual \(\{1,-1\}\) kernel of \(\operatorname {Spin}\to SO\) [fulton2004representation, Proposition 20.28, pp. 308--309], this is the full inverse-image torus.

A Laurent monomial on the parameter torus descends through the displayed sign kernel exactly when all its integer exponents have the same parity. Relative to the orthogonal coordinates \(x_i=t_i^2\), the Spin weight lattice is therefore \[P=\mathbb Z^\ell \cup \left (\mathbb Z+\tfrac 12\right )^\ell .\] The complete signed sums \(\lambda _I\) lie in \(P\), while an individual symbol \(e^{\epsilon _i/2}\) need not itself be a character. The orthogonal torus has character lattice \(\mathbb Z^\ell \); every spinor half-sum takes the scalar \(-1\) to \(-1\) and hence does not descend to it. In type D the adjoint torus has the still smaller root lattice.

[goodman2009symmetry, Corollary 6.3.9, p. 322; Sections 7.1 and 7.2.3, pp. 330 and 346] independently identify complex Spin as algebraically simply connected, explain the single-valued square-root torus factors, and identify the torus-character lattice with the weight lattice. Those group results support the character interpretation. The pinned TauCeti results used above are Lie and Clifford statements; no formal integration or differentiation comparison is asserted.

For \(B_2\), the four distinct weights are summarized by \[\operatorname {ch}S_{B_2} =(x^{1/2}+x^{-1/2})(y^{1/2}+y^{-1/2}),\] with highest weight \((\epsilon _1+\epsilon _2)/2=\omega _2\). For \(D_4\), the even- and odd-cardinality sums contain eight weights each: \(\omega _4=(\epsilon _1+\epsilon _2+\epsilon _3+\epsilon _4)/2\) lies in \(S^+\), while \(\omega _3=(\epsilon _1+\epsilon _2+\epsilon _3-\epsilon _4)/2\) lies in \(S^-\). This is a finite character check, not a triality claim.

Let \(V\) be a three-dimensional complex quadratic space with a supplied nondegenerate polarization \[V=\mathbb C w\oplus \mathbb C z\oplus \mathbb C w',\qquad B_Q(w,w')=1,\quad Q(z)=1,\] and choose the line coordinate so that \(\rho (z)=\alpha \), exterior parity. On \(S=\bigwedge (\mathbb Cw)\), use the ordered basis \((1,w)\). The even Clifford action then gives a homomorphism \[\operatorname {Spin}(Q)\longrightarrow SL(S)\simeq SL_2(\mathbb C).\] Reversal is matrix adjugation in this basis, so reverse norm one forces determinant one. This is the determinant calculation behind the dimension-three case; the target is the complex group, rather than the compact real unit-quaternion group of Example [fcap-002H].

There is a concrete inverse. For \(c\in \mathbb C\), the two products \[(z+cw)z,\qquad z(z+cw')\] are products of two norm-one vectors and hence are actual Spin elements. Creation, contraction, and parity from Proposition 11 give their matrices \[I+cE_{21},\qquad I+cE_{12}\] in the ordered basis \((1,w)\). These elementary transvections generate \(SL_2(\mathbb C)\). Writing a target matrix as a word in them and replacing each factor by its displayed lift gives a preimage; faithfulness of the even Clifford action makes the result independent of the chosen word. Thus restriction and this lift are inverse group maps, and the same basis intertwines the spin action with the standard two-dimensional module.

TauCeti proves this exact group-and-module statement over any field with \(2\ne 0\), given polarization data and dimension three TauCeti.exists_spinGroup_mulEquiv_specialLinearGroup_and_spinRep_equiv_stdSLRep_of_finrank_eq_three. Its chosen finite basis may reindex the two exterior coordinates; the formulas above use the stated basis \((1,w)\) and the corresponding basis change. The theorem needs no additional separable-closure hypothesis once the polarization is supplied.

Fulton--Harris identify \(\operatorname {Spin}_3(\mathbb C)\) with \(SL_2(\mathbb C)\) and distinguish it from the compact real form \(SU(2)\) [fulton2004representation, Section 10.3, pp. 143--144; Exercise 20.39, p. 311]. Goodman--Wallach independently list the same complex exceptional isomorphism [goodman2009symmetry, Section 6.3.3, Exercise 1, p. 322]. Their statements name the target; the two Clifford products above supply the coordinate lifts used here. Meinrenken's \(\operatorname {Spin}(3)=SU(2)\) is instead the compact real comparison [meinrenken2013clifford, Section 3.7.6, p. 83].

Let \(V=W\oplus W'\) be a split nondegenerate complex quadratic space with \(\dim W=2\), and choose polar-dual bases \(e_1,e_2\) and \(e'_1,e'_2\). Put \(S^+=\bigwedge ^{\mathrm {even}}W\) and \(S^-=\bigwedge ^{\mathrm {odd}}W\), with ordered bases \((1,e_1\wedge e_2)\) and \((e_1,e_2)\). The paired half-spin action from Theorem 10 gives an algebra equivalence \[\Phi :\mathcal {C}\kern -2pt\ell (Q)^0\longrightarrow \operatorname {End}(S^+)\times \operatorname {End}(S^-) \simeq M_2(\mathbb C)\times M_2(\mathbb C)\] TauCeti.SpinPolarizationData.evenCliffordEquivProdEnd. The two factors here are the actions on the fixed exterior-parity summands, not merely two abstract matrix blocks.

For exterior spinors define \[\langle s,t\rangle = [e_1\wedge e_2]\bigl (\operatorname {rev}_{\wedge }(s)\wedge t\bigr ),\] where the bracket takes the coefficient of \(e_1\wedge e_2\). On each displayed half-spin basis its matrix is \[J=\begin {pmatrix}0&1\\-1&0\end {pmatrix},\] and the two parity summands are orthogonal. Each creation operator and each polar-dual contraction operator is self-adjoint for this pairing, so Clifford reversal becomes the symplectic adjoint on each factor. Consequently, if \(\Phi (x)=(A,D)\), then \[\Phi (\operatorname {rev}(x)) =\bigl (J^{-1}A^{\mathsf T}J,J^{-1}D^{\mathsf T}J\bigr ) =\bigl (\operatorname {adj}(A),\operatorname {adj}(D)\bigr ).\] Therefore \(\operatorname {rev}(x)x=1\) is equivalent to \(\det A=\det D=1\).

We use one carrier-completion observation. In any positive-dimensional nondegenerate complex quadratic space, suppose an even Clifford unit \(u\) satisfies \(\operatorname {rev}(u)u=1\) and is already known to normalize the vector subspace. Its conjugation action is an isometry, so choose a vector-generated Lipschitz unit with the same orthogonal action CliffordAlgebra.lipschitzToOrthogonal_surjective. The quotient of that lift and \(u\) satisfies \(\alpha (z)v=vz\); graded centrality makes it a nonzero scalar CliffordAlgebra.exists_eq_algebraMap_of_involute_mul_ι_eq_ι_mul. Such a scalar unit is Lipschitz CliffordAlgebra.unitsMap_algebraMap_mem_lipschitzGroup. Hence \(u\) is Lipschitz, even, and reverse-norm one, and the exact carrier criterion of Remark [fcap-0028] puts it in Spin.

The forward restriction is thus a group homomorphism \[\operatorname {Spin}(Q)\longrightarrow SL(S^+)\times SL(S^-).\] Conversely, take \((A,D)\in SL_2(\mathbb C)\times SL_2(\mathbb C)\) and let \(x=\Phi ^{-1}(A,D)\). The adjugate calculation makes \(x\) an even Clifford unit with \(\operatorname {rev}(x)x=1\). It remains to prove that this algebraic preimage lies in the actual vector-generated Spin group.

For \(v\in V\), set \(y=xvx^{-1}\). It is odd and reversal-fixed: \[\operatorname {rev}(y) =\operatorname {rev}(x^{-1})v\operatorname {rev}(x)=y.\] In an orthogonal-basis Clifford expansion in dimension four, the odd part has only grades one and three. Reversal has signs \(+1\) and \(-1\) on those grades, so \(y\in V\). Moreover \(y^2=Q(v)1\); conjugation hence induces an isometry of \((V,Q)\). The carrier-completion observation now places \(x\) in the actual Spin group.

The restriction and \((A,D)\mapsto \Phi ^{-1}(A,D)\) are now inverse group maps. Hence \[\operatorname {Spin}_4(\mathbb C)\simeq SL_2(\mathbb C)\times SL_2(\mathbb C),\] and the two half-spin representations are the two standard two-dimensional modules. [fulton2004representation, Exercise 20.39, p. 311] state this group-and-module identification. [goodman2009symmetry, Section 6.3.3, Exercise 1, p. 322] independently give the same complex group. The displayed pairing, adjugate calculation, and carrier argument provide the inverse.

[meinrenken2013clifford, Section 3.7.6, p. 83] identifies the compact real form as \(\operatorname {Spin}(4)=SU(2)\times SU(2)\). Its quaternion-pair model is Example [fcap-002K], while the Lorentzian real form \(SL_2(\mathbb C)\) is Example [fcap-002L]; neither replaces the split complex proof above. TauCeti formalizes the paired half-spin algebra and matrix maps TauCeti.SpinPolarizationData.evenCliffordEquivProdMatrix.

The actual group and both modules also have a direct formal counterpart TauCeti.exists_spinGroup_mulEquiv_specialLinearGroup_prod_and_halfSpin_equiv_stdSLRep_of_finrank_eq_four. For a supplied polarization over a field of characteristic different from two and ambient dimension four, it constructs a group equivalence \(\operatorname {Spin}(Q)\simeq SL_2(K)\times SL_2(K)\) together with equivalences from the existing plus and minus half-spin subrepresentations to the standard representations pulled back from the first and second factors. The dimension hypothesis forces the residual line to vanish. The theorem chooses bases of both half-spin spaces, so its matrix coordinates agree with the ordered bases used here after basis transport. The displayed pairing and carrier proof give the comparison in our explicit coordinates.

Let \(V=W\oplus \mathbb Cz\oplus W'\) be a five-dimensional complex quadratic space with a supplied nondegenerate polarization, where \(\dim W=2\), \(Q(z)=1\), and \(\rho (z)=\alpha \). On \(S=\bigwedge W\), use the ordered basis \[(1,e_1\wedge e_2,e_1,e_2).\] Define \[\langle s,t\rangle = [e_1\wedge e_2]\bigl (\operatorname {rev}_{\wedge }(s)\wedge t\bigr ).\] Its matrix is \(\Omega =\operatorname {diag}(J,J)\), where \(J=\left (\begin {smallmatrix}0&1\\-1&0\end {smallmatrix}\right )\). The pairing preserves exterior parity, so parity itself is self-adjoint. Each creation operator and each polar-dual contraction operator is self-adjoint as well. Consequently the faithful even Clifford equivalence from Proposition 11 takes reversal to \[A\longmapsto A^{\dagger } =\Omega ^{-1}A^{\mathsf T}\Omega \] TauCeti.SpinPolarizationData.evenCliffordEquivEnd. Reverse norm one is therefore exactly the symplectic equation \(A^{\mathsf T}\Omega A=\Omega \).

This norm calculation alone does not yet prove membership in the vector-generated Spin group. The five vector operators \[c_1,\ c_2,\ a_1,\ a_2,\ \alpha \] are linearly independent, traceless, and \(\Omega \)-self-adjoint. The self-adjoint subspace of \(M_4(\mathbb C)\) has dimension six, and its trace-zero part has dimension five because \(\operatorname {tr}(I)=4\). Hence the Clifford image of the vector space is exactly \[\rho (V)= \{T:T^{\dagger }=T,\ \operatorname {tr}(T)=0\}.\] Conjugation by every \(A\in Sp_{\Omega }(4,\mathbb C)\) preserves this subspace: symplectic conjugation preserves the adjoint condition, and trace is conjugation-invariant.

The odd Clifford action is injective on the vector subspace. More generally, if an odd Clifford value \(y\) acts by zero, then \(zy\) is even and acts by zero. Faithfulness of the even action and invertibility of \(z\) give \(y=0\). Thus preservation of the displayed matrix subspace lifts to preservation of \(V\) inside the Clifford algebra.

For \(A\in Sp_{\Omega }(4,\mathbb C)\), let \(x\) be its unique preimage under the even Clifford equivalence. The adjoint equation gives \(\operatorname {rev}(x)x=1\), while the preceding calculation proves \(xVx^{-1}=V\). The carrier-completion argument of Proposition 20 now places \(x\) in actual Spin. Conversely, every Spin element has symplectic matrix because its reverse norm is one. These assignments are inverse group maps, and the chosen exterior basis is the module intertwiner: \[\operatorname {Spin}_5(\mathbb C)\simeq Sp_{\Omega }(4,\mathbb C), \qquad S\simeq \mathbb C^4.\]

Fulton--Harris state the same group and standard spin-module identification [fulton2004representation, Exercise 20.39, p. 311]. Goodman--Wallach independently write the target as \(Sp(2,\mathbb C)\), the rank-two symplectic group on a four-dimensional complex space [goodman2009symmetry, Section 6.3.3, Exercise 1, p. 322]. The trace-zero normalization calculation supplies the actual group inverse rather than inferring the image from a dimension count. By contrast, Meinrenken's \(\operatorname {Spin}(5)=Sp(2)\) is the compact quaternionic real form [meinrenken2013clifford, Section 3.7.6, pp. 83--84].

TauCeti proves that in odd dimension the even Clifford action is an equivalence onto the full endomorphism algebra and is faithful TauCeti.SpinPolarizationData.evenCliffordEquivEnd TauCeti.evenSpinAction_injective. It does not package the invariant alternating form or the group image as \(Sp_4\); those calculations are the explicit argument above.

Let \(V=W\oplus W'\) be a split nondegenerate complex quadratic space with \(\dim W=3\). For polar-dual bases \(e_i,e'_i\), use \[S^+:(1,e_{12},e_{13},e_{23}),\qquad S^-:(e_{123},-e_3,e_2,-e_1).\] For \(\langle s,t\rangle =[e_{123}]\bigl ( \operatorname {rev}_{\wedge }(s)\wedge t\bigr )\), the second displayed basis is dual to the first, and the full pairing matrix on \(S^+\oplus S^-\) is \[\Omega =\begin {pmatrix}0&I_4\\-I_4&0\end {pmatrix}.\] Clifford generators are self-adjoint for this pairing. Under the paired even-algebra equivalence \(\Phi \) of Theorem 10, reversal therefore sends \[(A,D)\longmapsto (D^{\mathsf T},A^{\mathsf T}).\] Thus the even reverse-norm-one group is \[\{(A,A^{-\mathsf T}):A\in GL_4(\mathbb C)\}.\] At this stage it is \(GL_4\), not yet the actual Spin group.

The vector-normalization condition cuts out the determinant-one subgroup. If \(v=\sum _i x_i e_i+y_i e'_i\), its odd Clifford action has block form \[\rho (v)=\begin {pmatrix}0&B_v\\B_v^\sharp &0\end {pmatrix},\] where \[B_v=\begin {pmatrix} 0&-y_3&y_2&-y_1\\ y_3&0&x_1&x_2\\ -y_2&-x_1&0&x_3\\ y_1&-x_2&-x_3&0 \end {pmatrix}.\] These matrices run through all skew \(4\times 4\) matrices. For a skew matrix \(B\), define \(B^\sharp \) by \[\begin {aligned} (B^\sharp )_{01}&=B_{23},& (B^\sharp )_{02}&=-B_{13},& (B^\sharp )_{03}&=B_{12},\\ (B^\sharp )_{12}&=B_{03},& (B^\sharp )_{13}&=-B_{02},& (B^\sharp )_{23}&=B_{01}, \end {aligned}\] with skew extension. Then \((B^\sharp )^\sharp =B\), \(BB^\sharp =-\operatorname {Pf}(B)I\), and \(\operatorname {Pf}(B_v)=-\sum _i x_i y_i\). The last two identities give \(\rho (v)^2=Q(v)I\), matching the Clifford convention.

The complementary-minor identity is \[(ABA^{\mathsf T})^\sharp =\det (A)A^{-\mathsf T}B^\sharp A^{-1}.\] One derivation identifies a skew matrix with an alternating two-form: the operation \(B\mapsto B^\sharp \) is the complementary two-form determined by the ordered volume basis, while \(\bigwedge ^4 A\) multiplies that volume by \(\det A\). Evaluating on basis pairs gives the six coordinate rules above and the displayed identity.

Conjugation by \(\operatorname {diag}(A,A^{-\mathsf T})\) sends the two off-diagonal blocks to \[ABA^{\mathsf T},\qquad A^{-\mathsf T}B^\sharp A^{-1}.\] By the complementary-minor identity, it preserves the vector graph \(\{(B,B^\sharp ):B^{\mathsf T}=-B\}\) exactly when \(\det A=1\). Sufficiency is immediate. For necessity, choose any nonzero \(B^\sharp \); equality of the two lower blocks forces \(\det A=1\). Faithfulness of the full Clifford action in this even dimension lifts this matrix statement to normalization of the actual vector subspace.

Every Spin element therefore acts on \(S^+\) through \(SL_4(\mathbb C)\). Conversely, for \(A\in SL_4(\mathbb C)\), let \(x\) be the unique even Clifford preimage of \((A,A^{-\mathsf T})\). It has reverse norm one and, by the graph calculation, normalizes \(V\). The carrier-completion argument of Proposition 20 places \(x\) in actual Spin. The mutually inverse maps are \[g\longmapsto \rho _+(g),\qquad A\longmapsto \Phi ^{-1}(A,A^{-\mathsf T}).\] Hence \[\operatorname {Spin}_6(\mathbb C)\simeq SL_4(\mathbb C).\] In the displayed bases \(S^+\) is the standard four-dimensional module and \(S^-\) is its dual.

[fulton2004representation, Exercise 20.39, p. 311] give the group and standard \(S^+\) module. [goodman2009symmetry, Section 6.3.3, Exercise 1, p. 322] independently give the same complex group. Here the cross-pairing proves \(S^-\) is dual, and the vector-graph calculation proves the actual image.

[meinrenken2013clifford, Section 3.7.6, p. 84] gives the compact real form \(\operatorname {Spin}(6)=SU(4)\).

TauCeti formalizes the paired half-spin algebra and matrix equivalences TauCeti.SpinPolarizationData.evenCliffordEquivProdEnd TauCeti.SpinPolarizationData.evenCliffordEquivProdMatrix. The vector graph, determinant-one group image and inverse are proved above, not by these declarations.

Work over \(\mathbb C\) with the type-\(D_4\) Cartan and Borel of Proposition 15. In its orthonormal coordinates put \[\begin {aligned} \alpha _1&=\epsilon _1-\epsilon _2,& \alpha _2&=\epsilon _2-\epsilon _3,\\ \alpha _3&=\epsilon _3-\epsilon _4,& \alpha _4&=\epsilon _3+\epsilon _4. \end {aligned}\] The central node is \(2\); the outer nodes are \(1,3,4\). Their fundamental weights are \[\omega _1=\epsilon _1,\qquad \omega _3=\tfrac 12(\epsilon _1+\epsilon _2+\epsilon _3-\epsilon _4),\qquad \omega _4=\tfrac 12(\epsilon _1+\epsilon _2+\epsilon _3+\epsilon _4).\] The established exterior convention identifies the vector class with \(L(\omega _1)\), the all-plus half-spin class with \(S^+=L(\omega _4)\), and the other half-spin class with \(S^-=L(\omega _3)\); see Theorem 16 and Proposition 18. Each has dimension eight.

Let \(\sigma \) be any permutation of \(\{1,3,4\}\). The linear map specified on the simple-root basis by \[T_\sigma (\alpha _i)=\alpha _{\sigma (i)}\quad (i=1,3,4),\qquad T_\sigma (\alpha _2)=\alpha _2\] preserves the \(D_4\) Cartan matrix. Hence it is orthogonal, preserves the root and coroot systems, and preserves the weight and coweight lattices. It is therefore an automorphism of the simply connected based root datum. Duality with the simple coroots gives \[T_\sigma (\omega _i)=\omega _{\sigma (i)}\qquad (i=1,3,4).\] In particular an outer three-cycle has cube one and nontrivially cycles the three labeled highest-weight classes \[L(\omega _1),\qquad S^-=L(\omega _3),\qquad S^+=L(\omega _4).\] This is a permutation of based root data and of irreducible highest-weight labels. A literal pullback of concrete group modules would additionally require an actual group automorphism and a fixed direction; that stronger statement is not inferred from this diagram calculation.

[fulton2004representation, Section 20.3, pp. 312--314] give the same \(D_4\) diagram and identify the vector and two half-spin highest weights. [adams1996exceptional, Chapter 5, Theorem 5.6, pp. 33--35] independently identifies these as the three basic eight-dimensional classes permuted by outer automorphisms. The first source is the complex highest-weight comparison used here; Adams' theorem concerns the compact actual group and is not being claimed as proved by the root-datum calculation alone.

The pinned declaration TauCeti.D4Tripled.trialityAutomorphism has cube one on a tripled type-\(D_4\) toral-closure carrier and permutes its numbered root and represented-torus coordinates. The inspected file does not identify that carrier with standard \(\operatorname {Spin}_8\), prove its torus maximal, or identify its three factors with the vector and half-spin modules. It is precise formal context for the diagram symmetry, not a whole-card formalization of the proposition above.

Let \(Q_8^+\) be the positive quadratic form on \(\mathbb R^8\), and let \[G=\operatorname {Spin}(Q_8^+)\longrightarrow SO(8)\] be the actual vector-generated, reverse-norm-one carrier and its vector action \(\pi \). The concrete Lie-group and covering results of Proposition [fcap-0037] and Proposition [fcap-003A] make \(G\) compact, connected, and simply connected, with \(\pi \) its two-sheeted universal cover. The even-word sign-change map of Proposition [fcap-0039] identifies this positive-square carrier with the compact negative-square convention used in the classical source, compatibly with the vector action.

Let \(\nu _+\) and \(\nu _-\) be the two real eight-dimensional half-spin representations. Their complexifications have highest weights \(\omega _4\) and \(\omega _3\), so the comparison of Proposition 23 and the exterior construction of Theorem 16 identify them, up to chosen intertwiners, with the two concrete complex half-spin modules. Average a positive definite inner product over compact \(G\). In an orthonormal basis either representation gives \[\nu :G\longrightarrow O(8).\] Connectedness puts its image in \(SO(8)\). Since \(G\) is simply connected, the universal cover \(\pi \) has a unique based lift \[\Theta :G\longrightarrow G,\qquad \pi \circ \Theta =\nu .\] The two maps \(\Theta (xy)\) and \(\Theta (x)\Theta (y)\) are based lifts on the connected space \(G\times G\), so uniqueness makes \(\Theta \) a group homomorphism.

Its derivative is nonzero because the half-spin representation has nonzero weights. The kernel of the derivative is an ideal of the simple Lie algebra \(\mathfrak {so}_8\), hence it is zero. Equal dimensions make \(\Theta \) a local Lie-group isomorphism. Its image is open, and compactness makes it closed; connectedness of \(G\) makes the image all of \(G\). Thus \(\Theta \) is a covering of a simply connected target by a connected source and is a Lie-group automorphism. Let Lie-group automorphisms act on representation classes by inverse pullback, \[\varphi \mathbin {\cdot }[M]=[M\circ \varphi ^{-1}].\] With this left-action convention, \(\Theta ^{-1}\) sends the vector class to the chosen half-spin class because \(\pi \circ \Theta =\nu \).

Every Lie-group automorphism permutes the three classes. After inner conjugation it preserves a chosen maximal torus and positive Weyl chamber; its differential therefore induces a based \(D_4\) root-datum automorphism. The diagram calculation of Proposition 23 shows that it permutes precisely the outer-node weights \(\omega _1,\omega _3,\omega _4\). Inner automorphisms act trivially on isomorphism classes, so inverse pullback defines a homomorphism \[\operatorname {Out}_{\mathrm {Lie}}(G)\longrightarrow S_3.\] There is a second kind of actual Lie-group automorphism. Conjugation by any unit vector in the Clifford algebra preserves even vector products and reverse norm and has conjugation by its inverse as inverse. On the vector module it gives orthogonal conjugation of \(\pi \); on the odd Clifford action it interchanges \(S^+\) and \(S^-\). Its permutation fixes the vector class and swaps the two half-spin classes. Together with the lifted half-spin automorphism, these permutations generate \(S_3\).

This permutation action has inner kernel. Suppose an automorphism \(\varphi \) fixes all three representation classes. Equivalence of \(\pi \circ \varphi \) with \(\pi \) gives an intertwiner; after polar normalization it is a matrix \(A\in O(8)\). If \(\det A=1\), lift \(A\) to \(g\in G\). After composing \(\varphi \) with the inverse inner automorphism \(\operatorname {Int}(g)\), its projection agrees with \(\pi \). The pointwise discrepancy from the identity lies continuously in \(\ker \pi =\{1,-1\}\), hence is identically \(1\) on connected \(G\). The remaining automorphism is the identity. If \(\det A=-1\), first compose with unit-vector conjugation. The result is inner by the preceding case, but unit-vector conjugation swaps the two half-spin classes, contradicting the hypothesis. Therefore \[\operatorname {Out}_{\mathrm {Lie}}(G)\simeq S_3.\] A suitable composition of the two constructed outer classes maps to a three-cycle and therefore has order three in the outer group. This does not show that the chosen half-spin lift \(\Theta \) has order three, and no representative has been normalized here to cube to the identity. No splitting \(S_3\to \operatorname {Aut}_{\mathrm {Lie}}(G)\) is asserted.

[adams1996exceptional, Chapter 5, Theorem 5.6, pp. 34--35] proves the compact group theorem and the permutation of its three eight-dimensional representations. [fulton2004representation, Section 20.3, pp. 312--314] independently describe the corresponding complex vector/half-spin triality and root diagram. The carrier translation, universal-cover lift, surjectivity, and kernel argument above place that comparison on the actual FCAP Spin group.

The pinned declaration TauCeti.D4Tripled.trialityAutomorphism has literal cube one on a tripled toral-closure carrier. Its source file does not identify that carrier with the actual group \(G\). Accordingly it is not used to claim cube one for \(\Theta \) or as a formal badge for this theorem.

Complexify the compact model and use the split rank-four exterior carrier \(S=\bigwedge W\) with a chosen top form \(\operatorname {vol}=e_1\wedge e_2\wedge e_3\wedge e_4\). Define \[B(s,t)=[\operatorname {rev}_{\wedge }(s)\wedge t]_{\operatorname {vol}}.\] In degree four this form is symmetric; its restrictions \(B_+\) and \(B_-\) to \(S^+\) and \(S^-\) are nondegenerate. Each creation operator and each polar-dual contraction operator is individually self-adjoint for \(B\). Thus the adjoint of Clifford multiplication by \(x\) is multiplication by \(\operatorname {rev}(x)\), and actual Spin elements preserve \(B\).

For \(v\in V\), \(s_+\in S^+\), and \(s_-\in S^-\), put \[F(v,s_+,s_-)=B_-(\rho (v)s_+,s_-).\] Clifford covariance of \(\rho (v)\) and invariance of \(B\) give \[F(\pi (g)v,\rho _+(g)s_+,\rho _-(g)s_-)=F(v,s_+,s_-) \qquad (g\in \operatorname {Spin}_8).\] The form is nonzero: with the displayed orientation, \[F(e_1,1,e_2\wedge e_3\wedge e_4)=1.\] This is an explicit invariant tensor \(V\otimes S^+\otimes S^-\to \mathbb C\); changing the chosen top form rescales it.

It is unique up to scalar. The full odd Clifford range is \[\operatorname {Hom}(S^+,S^-)\oplus \operatorname {Hom}(S^-,S^+).\] Under equivariant antisymmetrization its degrees are \(1,3,5,7\). Multiplication by the normalized Clifford volume element of the eight-dimensional space \(V\) exchanges degrees \(k\) and \(8-k\); projecting to either chirality block therefore gives \[\operatorname {Hom}(S^+,S^-)\simeq V\oplus \bigwedge ^3V.\] The two summands are nonisomorphic irreducible \(\operatorname {Spin}_8\)-modules, so \(V\) occurs exactly once. The nondegenerate forms identify invariant trilinears with \(\operatorname {Hom}_{\operatorname {Spin}_8}(V,S^+\otimes S^-)\), which is therefore one-dimensional.

[adams1996exceptional, Chapter 5, Proposition 5.7, pp. 35--36] states the invariant trilinear and proves the required multiplicity-one decomposition.

[fulton2004representation, Section 20.3, pp. 313--314] independently construct the Clifford-multiplication trilinear in the complex modules. The displayed top-form formula fixes its normalization in the FCAP creation--contraction convention. It does not assert a normed composition algebra or an order-three isometry of the tensor.

Let \(G=\operatorname {Spin}(Q_8^+)\) be the compact positive-square Clifford group, and let \(V\) denote its complexified vector representation. There is a smooth outer automorphism \(\tau :G\to G\) of exact order three for which \[V\circ \tau \simeq S^+,\qquad V\circ \tau ^2\simeq S^-.\] Here \(S^+=L(\omega _4)\) and \(S^-=L(\omega _3)\) use the exterior convention of Proposition 23. These are literal pullbacks of representations of the compact real group.

The outer-class calculation in Theorem 24 is thereby realized by a chosen cube-one automorphism. TauCeti's Serre diagram automorphism formalizes generator reindexing and its order relation on the presented Lie algebra. Its compact real-form identification and integration to this Clifford group are additional steps proved above. The tripled-carrier automorphism discussed in Proposition 23 remains a different construction.

For the automorphism \(\tau \) of Theorem 26, one can choose real forms of \(S^+,S^-\), invariant positive inner products on them, and real isometries \[J_0:V_{\mathbb R}\longrightarrow S^+_{\mathbb R},\qquad J_1:S^+_{\mathbb R}\longrightarrow S^-_{\mathbb R},\qquad J_2:S^-_{\mathbb R}\longrightarrow V_{\mathbb R}\] whose cyclic direct-sum map \(J\) has \(J^3=1\). Their complex-linear extensions preserve exactly the trilinear \(F\) of Proposition 25: \[F(J_2s_-,J_0v,J_1s_+)=F(v,s_+,s_-).\] The chosen forward cycle intertwines the diagonal group action with \(\tau ^{-1}\). The real forms and inner products are specified in the construction below.

Proposition 5.7 in [adams1996exceptional, pp. 35--36] supplies the invariant-line and real-valued trilinear statements.

Exercises 20.50--20.51 in [fulton2004representation, pp. 314--315] describe the related cyclic tensor symmetry. The construction above obtains that symmetry from the chosen compact automorphism and the real invariant line. Its isometry claim uses the transported inner products just defined; it does not identify them with preselected exterior bilinear forms or assert a normed composition algebra.

The exterior model now has two distinct faithful-range results. In even split dimension, Theorem 10 constructs all matrix units, identifies the two even endomorphism blocks, and records irreducibility after restriction to Spin under its separably closed, positive-rank hypotheses. In odd complex dimension, Proposition 11 shows that either full Clifford action selects one simple summand, while its restriction to the even algebra is faithful and its actual Spin action exchanges exterior parity in positive rank. Thus exterior parity is not a decomposition into odd-dimensional Spin submodules.

The occupation lines of Theorem 14 have also been joined to root and highest-weight theory. The type-D calculation in Proposition 15 and Theorem 16 fixes a Borel, proves positive-nilradical generation, and identifies the two fork modules. The type-B calculation in Theorem 17 adds the short root and its irreducible spin module, while Proposition 18 derives the finite type-B and type-D characters on the actual Spin torus. The selected TauCeti declarations formalize the Clifford root actions, annihilation identities, and weight vectors. The complex Borel, scalar-extension, irreducibility, torus-descent, and character conclusions are the mathematical arguments in these notes, not one packaged formal theorem.

The low-dimensional complex group comparisons are explicit in Proposition 19, Proposition 20, Proposition 21, and Proposition 22: they identify the actual Spin carriers in dimensions three through six and the stated standard or half-spin modules. These group inverses and module intertwiners are separate from the real algebra classification in Remark [fcap-0016] and its signature-\((1,3)\) instance in Example [fcap-0026]. The concrete real differential comparison in Proposition [fcap-0037] realizes Spin as a closed Lie subgroup, identifies its tangent algebra with the quadratic Clifford lift, and differentiates the vector and finite-dimensional Clifford-module actions; Example [fcap-0038] fixes the planar half-angle normalization. The selected TauCeti declarations formalize the algebraic lift and generator action, while the Lie-group, exponential, and tangent conclusions are the source-grounded arguments in those cards. The based-root calculation in Proposition 23 fixes the permutation of the three eight-dimensional highest-weight classes. The actual compact-group lifts and kernel calculation in Theorem 24 prove \(\operatorname {Out}_{\mathrm {Lie}}(\operatorname {Spin}_8)\simeq S_3\), while Proposition 25 constructs the invariant vector--half-spin trilinear and proves its multiplicity-one uniqueness. The pinned tripled-carrier automorphism is formal context on its stated carrier; it is not used as a packaged theorem about the actual Spin group.