Theorem. The exterior Clifford action [meinrenken2013clifford, Section 3.2.2, Proposition 3.5, p. 57] [fcap-001K]

The square relation of Lemma [fcap-001J] 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.