Theorem. The two top exterior words are the type-D fork highest vectors [fcap-002Y]

✍️sourceAGENTDRAFTED

Continue with the Cartan and Borel of Proposition [fcap-002X]. 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 [fcap-0025], \[\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 [fcap-0025]. 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.