Example. The rank-one polarized model [meinrenken2013clifford, Section 3.2.4, Theorem 3.3, p. 59] [fcap-001P]

Let \(W=Ke\) and choose \(e'\in W'\) with \(B_Q(e,e')=1\). In the ordered basis \((1,e)\) of \(S=\bigwedge W\), creation and contraction are \[\varepsilon _e= \begin {pmatrix}0&0\\1&0\end {pmatrix}, \qquad \iota _{e'}= \begin {pmatrix}0&1\\0&0\end {pmatrix}.\] Both are nilpotent, and \[\varepsilon _e\iota _{e'}+\iota _{e'}\varepsilon _e=I_2.\] Together with their products they give the four matrix units of \(\operatorname {End}_K(S)\). This is the rank-one calculation in Meinrenken's generation proof and a specialization of the general relation in Lemma [fcap-001J]. The formalized ingredients are TauCeti.SpinPolarizationData.contract_wedge and TauCeti.ExteriorAlgebra.creation_contraction_adjoin_eq_top; neither declaration formalizes this displayed choice of basis.