Chevalley constructs the classical filtration after choosing a finite basis of a vector space over a field. TauCeti's coordinate-free version below is defined for a quadratic form on a module over a commutative ring. The leading-symbol equivalences in Lemma 4.1.2 and Theorem 4.1.3 additionally assume that \(2\) is invertible.

Let \(R\) be a commutative ring, let \(M\) be an \(R\)-module, and let \(Q:M\to R\) be a quadratic form. In the Clifford algebra \(\mathcal {C}\kern -2pt\ell (Q)\), define \(F_n\mathcal {C}\kern -2pt\ell (Q)\) to be the \(R\)-submodule spanned by all products of at most \(n\) generators: \[F_n\mathcal {C}\kern -2pt\ell (Q)=\operatorname {span}_R\left \{\iota (v_1)\cdots \iota (v_r):0\le r\le n\right \}.\] The empty product gives \(F_0\mathcal {C}\kern -2pt\ell (Q)=R1\). Concatenating words makes the filtration multiplicative; in fact, \[F_i\mathcal {C}\kern -2pt\ell (Q)\,F_j\mathcal {C}\kern -2pt\ell (Q)=F_{i+j}\mathcal {C}\kern -2pt\ell (Q).\] Thus multiplication descends to the successive quotients and makes \[\operatorname {gr}_F\mathcal {C}\kern -2pt\ell (Q)=\bigoplus _{n\ge 0}F_n\mathcal {C}\kern -2pt\ell (Q)/F_{n-1}\mathcal {C}\kern -2pt\ell (Q)\] a graded algebra, with \(F_{-1}\mathcal {C}\kern -2pt\ell (Q)=0\).

Retain the coordinate-free commutative-ring and module setting of Definition 4.1.1, and assume that \(2\) is invertible in \(R\). This is TauCeti's extension of Chevalley's finite-basis, vector-space leading-symbol argument. For vectors \(v_1,\ldots ,v_n\in M\), the Clifford relation replaces an interchange by its alternating term plus a scalar contraction. Each contraction removes two generators. Consequently \[\iota (v_1)\cdots \iota (v_n) \equiv v_1\wedge \cdots \wedge v_n\pmod {F_{n-2}},\] where the right-hand side is read through the zero-form exterior model. In particular, the class of the Clifford word in \(F_n/F_{n-1}\) depends alternately on the vectors and is the leading exterior symbol.

Let \(R\), \(M\), and \(Q\) be as in Lemma 4.1.2. Chevalley's finite-dimensional field argument motivates the identification. TauCeti proves the following coordinate-free commutative-ring and module equivalence. For every \(n\ge 0\), the leading-symbol map gives \[F_n\mathcal {C}\kern -2pt\ell (Q)/F_{n-1}\mathcal {C}\kern -2pt\ell (Q)\simeq \bigwedge ^n_R M.\] At \(n=0\) this is the scalar equivalence \(F_0/0\simeq R=\bigwedge ^0_RM\). For \(n>0\), the inverse sends a decomposable exterior product to the class of the corresponding Clifford word.

The point of the quotient is that every contraction term has already fallen into a lower filtration step. Alternation is therefore exact in the graded piece even though it is not exact in the Clifford algebra itself.

Meinrenken's Proposition 2.6 assumes a finite-dimensional vector space over a characteristic-zero field. TauCeti proves the corresponding extension for an additive commutative group \(M\) with a module structure over a commutative ring \(R\), a quadratic form \(Q\) on \(M\), and invertible \(2\in R\). Under these hypotheses, the equivalences of Theorem 4.1.3 respect multiplication of homogeneous classes and assemble into a graded-algebra equivalence \[\operatorname {gr}_F\mathcal {C}\kern -2pt\ell (Q)\simeq _{\mathrm {grAlg}}\bigwedge _R M.\] The class of a product of an \(i\)-word and a \(j\)-word is carried to the exterior product of their leading symbols in degree \(i+j\).

This is a PBW theorem for the Clifford filtration. It does not make \(\mathcal {C}\kern -2pt\ell (Q)\) and \(\bigwedge _RM\) isomorphic as algebras. The quadratic form survives in the lower-degree contraction terms of Clifford multiplication; only the associated graded multiplication forgets it.

For \(u,v\in M\), write the Clifford product as \[\iota (u)\iota (v) =\frac 12\bigl (\iota (u)\iota (v)-\iota (v)\iota (u)\bigr ) +\frac 12B_Q(u,v)1.\] The second summand belongs to \(F_0\). Hence the degree-two class of \(\iota (u)\iota (v)\) is \(u\wedge v\). This is the two-generator instance of Chevalley's leading-symbol calculation cited in the title. The surviving half-commutator is the Clifford bivector studied next; the scalar polar term is invisible to the leading symbol.

Chevalley's proof chooses a basis, proves that ordered Clifford monomials form a basis, and identifies the underlying vector space with the exterior algebra [chevalley1954algebraic, II.1.2 and II.1.6, pp. 40--42]. Panyushev uses the resulting stable filtration and exterior associated graded as standard representation-theoretic background [panyushev2001exterior, Section 2, p. 7].

The quotient construction above is TauCeti's coordinate-free commutative-ring and module extension of that finite-dimensional field proof. It builds each graded piece from the word-length submodule and its predecessor, handles degree zero separately, and then takes their direct sum. This is a change of packaging and generality, not a stronger claim about unfiltered Clifford multiplication.

Lawson and Michelsohn write \[v^2=-q(v)1, \qquad vw+wv=-2q(v,w),\] where \(2q(v,w)=q(v+w)-q(v)-q(w)\). Mathlib and TauCeti instead use a quadratic form \(Q\) with \[\iota (v)^2=Q(v)1.\] The conventions agree after setting \(Q=-q\). The orthogonal group and its reflections are unchanged by this global sign reversal. A vector with \(q(v)=1\) therefore has \(Q(v)=-1\) in the convention used below. Mathlib's generator-square rule CliffordAlgebra.ι_sq_scalar uses this \(Q\)-convention.

Let \(F\) be a field of characteristic different from \(2\), let \(Q\) be a quadratic form on an \(F\)-vector space \(V\), and write \[B_Q(x,y)=Q(x+y)-Q(x)-Q(y)\] for its polar form. If \(Q(v)\ne 0\), the reflection with normal vector \(v\) is \[\rho _v(w)=w-\frac {B_Q(v,w)}{Q(v)}v.\] It fixes \(v^\perp \) pointwise, sends \(v\) to \(-v\), and preserves \(Q\). Multiplying \(v\) by a nonzero scalar does not change \(\rho _v\).

Let \(\alpha \) denote the grading involution of \(\mathcal {C}\kern -2pt\ell (Q)\). For \(Q(v)\ne 0\), the Clifford generator \(\iota (v)\) is invertible with \[\iota (v)^{-1}=Q(v)^{-1}\iota (v).\] Its twisted adjoint action on a generator is the reflection in Definition 4.2.2: \[\alpha (\iota (v))\,\iota (w)\,\iota (v)^{-1}=\iota (\rho _v(w)).\]

Lawson--Michelsohn make this product-and-scaling argument for a finite-dimensional quadratic vector space over a field. The statement below is TauCeti's extension to a quadratic module over a commutative ring. It assumes that \(2\) and \(Q(v)\) are invertible.

Let \(R\) be a commutative ring, let \(Q\) be a quadratic form on an \(R\)-module \(M\), and suppose \(2\) and \(Q(v)\) are invertible. If there is a scalar \(c\) such that \[c^2=-Q(v)^{-1},\] then \(Q(cv)=-1\). The normalized Clifford generator \(\iota (cv)\) belongs to the Pin group and its twisted adjoint action is \(\rho _v\), because \(\rho _{cv}=\rho _v\). Consequently \[\rho _v\in \operatorname {range}(\operatorname {pinToOrthogonal}).\] Equivalently, the required hypothesis is that \(-Q(v)^{-1}\) is a square. The conclusion is existential: it asserts that a Pin lift exists, not that a canonical square root has been chosen.

The cited product formulas are stated for a finite-dimensional quadratic vector space over a field. TauCeti packages the same scaling and Clifford-product calculation over the commutative-ring and module hypotheses inherited from Lemma 4.2.4.

Let \(R\), \(M\), and \(Q\) be as in Lemma 4.2.4. Suppose \(Q(v)\), \(Q(w)\), and \(2\) are invertible. If there is a scalar \(c\) such that \[c^2=Q(v)^{-1}Q(w)^{-1},\] then \[Q(cv)Q(w)=1.\] Set \(x=\iota (cv)\iota (w)\). The element \(x\) is a product of invertible Clifford generators, and \[x^{*}x =\iota (w)\iota (cv)^2\iota (w) =Q(cv)Q(w)=1.\] Thus \(x\) is a unitary element of the Lipschitz group. It has even degree, so it belongs to the Spin group. Its twisted adjoint action is the ordered product of reflections, and therefore \[\rho _v\rho _w\in \operatorname {range}(\operatorname {spinToOrthogonal}).\]

Equations (2.24)--(2.26) give the product descriptions and scaling invariance used here. The product-square condition is sharper than asking for separate normalizations of \(v\) and \(w\): one scalar normalizes the product even when neither vector has been normalized separately.

Let \(V=\mathbb {R}^n\) with Euclidean inner product and use the sign convention \[Q(x)=-\langle x,x\rangle .\] For a unit vector \(v\), one has \(Q(v)=-1\); thus \(c=1\) satisfies the square condition in Lemma 4.2.4. The Clifford generator \(\iota (v)\) is already Pin-normalized, and its action is the familiar hyperplane reflection \[\rho _v(w)=w-2\langle v,w\rangle v.\] For orthonormal \(v,w\), the even product \(\iota (v)\iota (w)\) lies in Spin and lifts the composition \(\rho _v\rho _w\). This is the Euclidean specialization of the general Pin and paired-Spin lifting statements in Lemma 4.2.4 and Theorem 4.2.5.

Lawson and Michelsohn supply the twisted-adjoint reflection formula, the definitions of Pin and Spin, the description by products of normalized vectors, and the square-root obstruction to normalization. The square-witness statements in Lemma 4.2.4 and Theorem 4.2.5 isolate the precise algebraic hypotheses under which one or two reflections lift.

An individual lift does not by itself show that all orthogonal transformations lift. That global conclusion requires finite dimension, nondegeneracy, and the Cartan--Dieudonne factorization developed next.

One reflection can enlarge the fixed subspace of an orthogonal transformation. Iterating this correction proves that reflections generate the orthogonal group. Once each reflection has a Pin lift, generation gives the Pin cover; determinant parity then restricts that cover to Spin over the special orthogonal group.

Theorem 4.2.8.7. Surjectivity of the Spin action [lawson2016spin, I.2, Theorem 2.9, pp. 18--19] [fcap-001B]

spinToSpecialOrthogonal_surjective_of_isSquarespinToSpecialOrthogonal_surjective

L∃∀NAGENTDRAFTED

Let \(K\) be a field of characteristic different from \(2\), let \(V\) be finite-dimensional, and let \(Q\) be nondegenerate. Suppose that for every nonisotropic \(v\in V\), the scalar \(-Q(v)^{-1}\) is a square in \(K\). Then the twisted-adjoint action restricts to a surjection \[\operatorname {Spin}(V,Q)\twoheadrightarrow SO(V,Q).\] The underlying homomorphism is TauCeti.CliffordAlgebra.spinToSpecialOrthogonal, and its action on vectors is the usual Spin action by TauCeti.CliffordAlgebra.coe_spinToSpecialOrthogonal_apply.

Indeed, the square-normalization hypothesis and Cartan--Dieudonne generation give the Pin surjection of Theorem 4.2.8.4. It lifts an element of \(SO(V,Q)\) to Pin; the lift has determinant \(1\), so Lemma 4.2.8.6 shows that it is even and therefore lies in Spin. The restriction square

commutes because both vertical maps are induced by the same twisted Clifford conjugation. Over a separably closed field the square condition is automatic, so nondegeneracy and finite dimension suffice. The general restriction principle from a surjective Pin action is TauCeti.CliffordAlgebra.spinToSpecialOrthogonal_surjective_of_pinToOrthogonal_surjective.

The square condition is TauCeti's fixed-sign sufficient hypothesis, stronger in general than Lawson--Michelsohn's option to normalize each vector to either sign; see Theorem 4.2.8.4. For a positive-definite real geometric form \(q\), the Clifford convention is \(Q=-q\); hence \(-Q(v)^{-1}>0\) for every nonzero \(v\), so the reflecting vectors can be normalized over \(\mathbb {R}\). This observation does not assert the square condition for arbitrary real signatures.

Meinrenken works throughout this chapter with finite-dimensional vector spaces over a characteristic-zero field. The cards below retain his normalization and formulas but follow TauCeti's extensions. Each card states the commutative-ring, module, invertible-\(2\), finite-dimensional, or nondegeneracy assumptions it needs.

Meinrenken starts with a symmetric bilinear form \(B\) and the relation \[uv+vu=2B(u,v)1.\] For the associated quadratic form \(Q(v)=B(v,v)\), the polar form used here is \(B_Q=2B\).

Meinrenken's quantization formula and the half-commutator agree: \[q(u\wedge v)=uv-B(u,v)1 =\frac 12(uv-vu)=:\beta (u,v).\] The induced action on a vector is \[[\beta (u,v),x] =B_Q(v,x)u-B_Q(u,x)v =2\bigl (B(v,x)u-B(u,x)v\bigr ).\] This is Meinrenken's formula \(-2\iota _{B(x,-)}(u\wedge v)\) and Kostant's formula \(-2\iota _x(u\wedge v)\) in the corresponding contraction convention [kostant1997clifford, Section 2.4, (12) and Theorem 8, pp. 283, 286]. The factor of two belongs to the passage from \(B\) to the unhalved polar form \(B_Q\); it is not an additional rescaling of \(\beta \).

For the formalized extension described in Convention 4.3.1, let \(R\) be a commutative ring in which \(2\) is invertible, let \(M\) be an \(R\)-module, and let \(Q\) be a quadratic form on \(M\). The Clifford bivector of \(u,v\in M\) is \[\beta _Q(u,v)=\frac 12\bigl (\iota (u)\iota (v)-\iota (v)\iota (u)\bigr ).\] It is alternating in \(u\) and \(v\), so it induces a linear map \[\beta _Q:\bigwedge _R^2M\longrightarrow \mathcal {C}\kern -2pt\ell (Q).\] The exterior model is a left inverse on its image: \[\operatorname {equivExterior}_Q\bigl (\beta _Q(z)\bigr )=z \qquad (z\in \bigwedge _R^2M).\] Hence \(\beta _Q\) is injective.

For \(u,v,x\in M\), the commutator of the bivector with a Clifford generator is \[[\beta _Q(u,v),\iota (x)] =\iota \left (B_Q(v,x)u-B_Q(u,x)v\right ).\] The endomorphism \[A_{u\wedge v}(x)=B_Q(v,x)u-B_Q(u,x)v\] is skew-adjoint for \(B_Q\), since \[B_Q(A_{u\wedge v}x,y)+B_Q(x,A_{u\wedge v}y)=0.\] Thus commutation by a degree-two Clifford element preserves the generating module and realizes the elementary infinitesimal orthogonal transformation attached to \(u\wedge v\).

Over the commutative ring and module of Definition 4.3.2, let \(\mathfrak {cl}^{(2)}(Q)\) be the submodule of \(\mathcal {C}\kern -2pt\ell (Q)\) spanned by the elements \(\beta _Q(u,v)\). This is TauCeti's module-general extension of Meinrenken's characteristic-zero vector-space construction. The commutator formula of Lemma 4.3.3, together with the Jacobi identity, shows that this submodule is closed under commutators. Transporting its bracket across \(\beta _Q\) gives a Lie algebra structure on \(\bigwedge _R^2M\) and a Lie equivalence \[\bigwedge _R^2M\simeq _{\mathrm {Lie}}\mathfrak {cl}^{(2)}(Q).\] On a decomposable bivector the equivalence is exactly \[u\wedge v\longmapsto \frac 12(uv-vu).\] No choice of basis enters this identification.

Meinrenken states this realization over a characteristic-zero field. TauCeti proves the extension below over any field of characteristic different from \(2\). Let \(K\) be such a field, let \(V\) be finite-dimensional, and let \(Q\) be nondegenerate. Write \(\mathfrak {so}(V,B_Q)\) for the Lie algebra of endomorphisms skew-adjoint for the polar form. Then commutation on generators gives a Lie equivalence \[\mathfrak {so}(V,B_Q)\simeq _{\mathrm {Lie}}\mathfrak {cl}^{(2)}(Q).\] If \(A\in \mathfrak {so}(V,B_Q)\) corresponds to \(z_A\in \mathfrak {cl}^{(2)}(Q)\), then \[[z_A,\iota (x)]=\iota (Ax)\qquad (x\in V).\] Combining this equivalence with Theorem 4.3.4 gives the basis-free chain \[\bigwedge _K^2V\simeq _{\mathrm {Lie}}\mathfrak {so}(V,B_Q) \simeq _{\mathrm {Lie}}\mathfrak {cl}^{(2)}(Q).\] Kostant identifies the same degree-two subspace with \(\operatorname {Lie}(\operatorname {Spin}(V))\) and the first equivalence with the differential of the double cover [kostant1997clifford, Section 2.4, Theorem 8, pp. 286--287].

This coordinate example specializes TauCeti's extension of the characteristic-zero construction summarized in Convention 4.3.1. Take \(V=R^n\) with the standard sum-of-squares quadratic form, and let \(e_i,e_j\) be distinct coordinate vectors. Under the standard-coordinate realization, \[e_i\wedge e_j\longmapsto 2(E_{ij}-E_{ji}).\] Thus its action on \(x=(x_k)\) is \[x\longmapsto 2x_j e_i-2x_i e_j.\] The factor \(2\) is the polar-form normalization from Convention 4.3.1: for the sum-of-squares form, \(B_Q(x,y)=2\sum _kx_ky_k\). The displayed matrix is the standard-coordinate specialization of the basis-free isomorphism in Meinrenken's proposition. Dividing the skew matrix by two would correspond to using the associated bilinear form \(B_Q/2\) instead.

The quadratic Clifford Lie algebra is the infinitesimal part of the same conjugation action that produces reflections. Kostant proves that \(\bigwedge ^2V=\operatorname {Lie}(\operatorname {Spin}(V))\), that its map to \(\mathfrak {so}(V)\) is the differential of \(\operatorname {Spin}(V)\to SO(V)\), and that its commutator action extends as the corresponding derivation of the exterior algebra [kostant1997clifford, Section 2.4, Theorem 8, pp. 286--287]. Chevalley obtains the same two-vector Lie algebra inside the Clifford group [chevalley1954algebraic, II.2.9, pp. 67--68].

The cards above identify the algebraic Lie layer. They do not construct Lie-group structures or identify a differential of a Lie-group covering map. The next chapter instead reaches the global orthogonal group by finite products of reflections.

Let \(K\) be a field in which \(2\) is invertible, let \(V\) be finite-dimensional, and let \(Q\) be nondegenerate. Suppose a \(K\)-Lie algebra \(L\) acts orthogonally on \(V\) through \[\theta :L\longrightarrow \mathfrak {so}(V,B_Q),\] and let \(\rho :\mathcal {C}\kern -2pt\ell (Q)\to \operatorname {End}_K(S)\) be any Clifford module. The equivalence of Theorem 4.3.5 lifts \(\theta \) to quadratic Clifford elements; composing with \(\rho \) gives a Lie representation \[\rho _{\mathcal {C}\kern -2pt\ell }:L\longrightarrow \operatorname {End}_K(S),\qquad \rho _{\mathcal {C}\kern -2pt\ell }(y)=\rho \bigl (\operatorname {soEquivQuadratic}(\theta (y))\bigr ).\] Kostant constructs this lift for a complex reductive group representation and then lets its quadratic elements act on the spin module. The formalized statement isolates the algebraic mechanism over the stated field and for an arbitrary Clifford module; it does not assert that \(\theta \) is a differential of a group representation.

Let \(G\) and \(H\) be finite-dimensional real Lie groups, with identities \(e_G\) and \(e_H\), and let \(\phi :G\to H\) be a smooth group homomorphism. Their Lie algebras are the tangent spaces \[\mathfrak g=T_{e_G}G, \qquad \mathfrak h=T_{e_H}H.\] The differential of \(\phi \) at the identity is the linear map \[\operatorname {Lie}(\phi )=d\phi _{e_G}: \mathfrak g\longrightarrow \mathfrak h.\] No connectedness or simply-connectedness hypothesis is needed to define this map. Those hypotheses enter the converse problem of integrating a Lie-algebra homomorphism, not the differentiation of a given smooth homomorphism.

For \(X\in \mathfrak g\), let \(\widetilde X\) be its left-invariant vector field, \[\widetilde X_g=d(L_g)_{e_G}X.\] The homomorphism identity \(\phi \circ L_g=L_{\phi (g)}\circ \phi \) gives \[d\phi _g(\widetilde X_g) =\widetilde {\operatorname {Lie}(\phi )(X)}_{\phi (g)}.\] Thus differentiation at the identity and transport by left translation are two descriptions of the same infinitesimal map.

In the setting of Definition 4.4.1, the differential is a Lie-algebra homomorphism: \[\operatorname {Lie}(\phi )([X,Y]) =[\operatorname {Lie}(\phi )(X), \operatorname {Lie}(\phi )(Y)].\] Indeed, the left-invariant fields \(\widetilde X\) and \(\widetilde Y\) are \(\phi \)-related to the left-invariant fields determined by their images. Brackets of related vector fields are again related. Evaluating that relation at \(e_G\) gives the displayed identity.

This argument is local at the identity. In particular, bracket preservation does not require \(G\) to be connected or simply connected.

Differentiation at the identity is functorial. For smooth homomorphisms \(G\xrightarrow {\phi }H\xrightarrow {\psi }K\), the chain rule gives \[\operatorname {Lie}(\operatorname {id}_G) =\operatorname {id}_{\mathfrak g}, \qquad \operatorname {Lie}(\psi \circ \phi ) =\operatorname {Lie}(\psi )\circ \operatorname {Lie}(\phi ).\] Together with Lemma 4.4.2, this defines a functor from Lie groups and smooth homomorphisms to Lie algebras and Lie-algebra homomorphisms.

The stronger correspondence between simply connected Lie groups and Lie algebras concerns existence and uniqueness in the reverse direction. It is not a hypothesis of these functor laws.

Let \(\phi :G\to H\) be a smooth Lie-group homomorphism. For every \(X\in \mathfrak g\), \[\phi (\exp _G X) =\exp _H\bigl (\operatorname {Lie}(\phi )(X)\bigr ).\] Equivalently, the square

Let \(V\) be a finite-dimensional real vector space and let \[\rho :G\longrightarrow \operatorname {GL}(V)\] be a smooth representation. Its differential is a Lie-algebra representation \[d\rho _{e_G}:\mathfrak g\longrightarrow \mathfrak {gl}(V).\] Naturality of the exponential becomes \[\rho (\exp _G X)=\exp \bigl (d\rho _{e_G}(X)\bigr ),\] where the exponential on the right is the ordinary matrix exponential. For example, for the determinant homomorphism \(\det :\operatorname {GL}_n(\mathbb R)\to \mathbb R^\times \), \[d(\det )_I(A)=\operatorname {tr}(A).\]

The constructions in Definition 4.4.1--Example 4.4.5 start with a smooth homomorphism. Their tangent map, bracket law, functor laws, and exponential naturality therefore do not require a theorem that upgrades a continuous homomorphism to a smooth one. The generic theorem does not invoke the closed-subgroup theorem; that theorem belongs to the later specialization to concrete matrix subgroups. This is the dependency split proposed in TauCetiRoadmap PR 224.

The exponential input is separate from the tangent and bracket input. Likewise, the Baker--Campbell--Hausdorff calculation can first be made in a matrix or general-linear group; using it inside a particular closed matrix subgroup additionally requires the subgroup's Lie structure. Liu describes the local exponential and BCH coordinates, while Isaev--Rubakov give the matrix Campbell--Hausdorff calculation.

The open TauCeti draft PR 3078 proposes the generic construction and its functor and exponential laws. It is not merged, so these cards carry no Lean markers. Even after that generic interface lands, the differential of \(\operatorname {Spin}(Q)\to SO(Q)\) still needs compatible Lie-group structures on the two abstract groups. The algebraic identification in Theorem 4.3.5 does not by itself supply those structures.

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.

For \(x\in W\), creation is exterior multiplication \[\varepsilon _x(s)=x\wedge s.\] For \(y\in W'\), contraction is the degree-\(-1\) operator \(\iota _y\) associated with the functional \(x\mapsto B_Q(x,y)\). Finally, if \(z\in L\), its operator is \[\lambda _z=\ell (z)\,\alpha ,\] where \(\alpha \) is parity: it is \(+1\) on even exterior degree and \(-1\) on odd exterior degree. Chevalley's formulas identify the first two operators as left Clifford multiplication on the minimal ideal model [chevalley1954algebraic, II.2.2, pp. 43--44].

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.5.3 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 4.5.4 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 \(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 4.5.3. The formalized ingredients are TauCeti.SpinPolarizationData.contract_wedge and TauCeti.ExteriorAlgebra.creation_contraction_adjoin_eq_top; neither declaration formalizes this displayed choice of basis.

The exterior action constructed above stops before several classical consequences in representation theory. Over a split field, irreducibility and the decomposition into two half-spin modules require further hypotheses and arguments; Meinrenken proves these results after establishing that the Clifford action is an isomorphism. The currently open TauCeti half-spin work is therefore not represented by a Lean marker here.

The generic mathematics of differentiating a smooth Lie-group homomorphism is developed in § 4.4. What remains missing for the Spin cover is more specific: compatible Lie-group structures on TauCeti's abstract \(\operatorname {Spin}(V)\) and \(SO(V)\), followed by the identification of their specialized differential with the algebraic quadratic action above. The open TauCeti PR linked in Remark 4.4.6 proposes only the generic Lie functor.

Highest weights, triality, and the Bott-periodic real table also belong to later layers. Kostant supplies the differential in the classical complex setting, and Lawson--Michelsohn treat the real Pin and Spin groups. None of these horizons follows merely from the algebraic restrictions \(\operatorname {spinRep}\) and \(\operatorname {pinRep}\).

For \(p,q\ge 0\), put \[Q_{p,q}(x)=\sum _{i<p}x_i^2-\sum _{p\le i<p+q}x_i^2\] on \(\mathbb {R}^{p+q}\), and write \(\mathcal {C}\kern -2pt\ell _{p,q}\) for \(\mathcal {C}\kern -2pt\ell (Q_{p,q})\). Thus the first \(p\) Clifford generators square to \(+1\), and the last \(q\) square to \(-1\). This agrees with Chevalley's convention for the quadratic form and with his positive/negative inertia indices.

Lawson and Michelsohn use the same signature \(q_{r,s}\) but impose \(v^2=-q_{r,s}(v)1\) [lawson2016spin, I.3, Proposition 3.1, p. 21]. Therefore the algebras are related by the exact index swap \[\mathcal {C}\kern -2pt\ell _{p,q}=\mathcal {C}\kern -2pt\ell ^{\mathrm {Lawson}}_{q,p}.\] The recurrence below adds one index of each sign, so it is invariant under this swap.

The real hyperbolic plane is \[H=(\mathbb {R}^2,Q_{1,1}),\qquad Q_{1,1}(s,t)=s^2-t^2.\] Its coordinate generators \(e_+\) and \(e_-\) satisfy \[e_+^2=1,\qquad e_-^2=-1,\qquad e_+e_-=-e_-e_+.\] For every signature, separating the last positive and negative coordinates gives an isometry \[(\mathbb {R}^{p+q+2},Q_{p+1,q+1}) \simeq (\mathbb {R}^{p+q},Q_{p,q})\perp H.\] The coordinate order is fixed: the retained \(p\) positive and \(q\) negative axes form the first factor, and the last positive and last negative axes form \(H\).

For finite-dimensional quadratic spaces, Lawson--Michelsohn state the signature recurrence \[\mathcal {C}\kern -2pt\ell _{p+1,q+1}\simeq _{\mathbb {R}\text {-alg}} \mathcal {C}\kern -2pt\ell _{p,q}\otimes _{\mathbb {R}}M_2(\mathbb {R}).\] TauCeti extends the recurrence to any real quadratic module \((M,Q)\) and supplies an explicit formula on generators: \[\mathcal {C}\kern -2pt\ell (Q\perp Q_{1,1})\simeq \mathcal {C}\kern -2pt\ell (Q)\otimes _{\mathbb {R}}M_2(\mathbb {R}).\] With \[\sigma _x=\begin {pmatrix}0&1\\1&0\end {pmatrix},\] the equivalence sends a generator \((m,(s,t))\) to \[\iota _Q(m)\otimes \sigma _x +1\otimes \begin {pmatrix}s&t\\-t&-s\end {pmatrix}.\] The first summand squares to \(Q(m)\), the second to \(s^2-t^2\), and the two anticommute. The universal property therefore gives the forward algebra map. In the other direction, the original Clifford algebra and the matrix algebra act through commuting algebra maps on the hyperbolic Clifford algebra; their tensor lift is inverse to the forward map. The two composites are checked on Clifford generators and pure tensors, which is why TauCeti's extension needs no finite-dimensional hypothesis. Chevalley's split-matrix theorem and orthogonal-sum calculation supply the classical structural mechanism [chevalley1954algebraic, II.2.1 and II.2.5, pp. 42--46].

Writing the displayed generator formula as \(f\), its universal extension is summarized by the commuting diagram

Chevalley splits a finite-dimensional real quadratic space into hyperbolic planes and a definite remainder. TauCeti combines that classical reduction with iteration of Theorem 4.6.3 and Kronecker equivalences to synthesize the explicit tensor and matrix packaging below. Iterating \(n\) times gives \[\mathcal {C}\kern -2pt\ell _{p+n,q+n}\simeq \mathcal {C}\kern -2pt\ell _{p,q}\otimes _{\mathbb {R}}M_{2^n}(\mathbb {R}).\] Taking \(n=\min (p,q)\) removes the common positive and negative part: \[\mathcal {C}\kern -2pt\ell _{p,q}\simeq \mathcal {C}\kern -2pt\ell _{p-n,q-n}\otimes _{\mathbb {R}}M_{2^n}(\mathbb {R}), \qquad n=\min (p,q).\] Thus if \(p\le q\), the residual algebra is \(\mathcal {C}\kern -2pt\ell _{0,q-p}\); if \(q\le p\), it is \(\mathcal {C}\kern -2pt\ell _{p-q,0}\). The matrix factors combine through the Kronecker equivalence \[M_{2^a}(\mathbb {R})\otimes M_{2^b}(\mathbb {R}) \simeq M_{2^{a+b}}(\mathbb {R}).\] Chevalley supplies the quadratic-space decomposition. The displayed \(M_{2^n}\) packaging and its named equivalences are TauCeti's formalized synthesis.

With the TauCeti signature convention of Convention 4.6.1, there is an algebra equivalence \[\mathcal {C}\kern -2pt\ell _{p+2,q}\simeq _{\mathbb R\text {-alg}} \mathcal {C}\kern -2pt\ell _{q,p}\otimes _{\mathbb R}M_2(\mathbb R).\] The construction first separates the last positive coordinate from \(Q_{p+2,q}\). Adjoining that positive line permits a Clifford sign switch; negating \(Q_{p+1,q}\) exchanges its positive and negative coordinate blocks. The resulting form is \(Q_{q+1,p+1}\), to which the hyperbolic recurrence of Theorem 4.6.3 applies.

The accompanying generator theorem SignatureSwitchRecurrenceEquiv_ι records this composition through the positive-coordinate splitter, the sign-switch isometry, and the generator formula for the hyperbolic equivalence. It fixes the equivalence on the canonical Clifford generators rather than asserting only that some algebra isomorphism exists.

After converting between the two signature conventions, inverting Lawson--Michelsohn's equation (4.1), using \(\mathcal {C}\kern -2pt\ell ^{\mathrm {Lawson}}_{0,2}\cong M_2(\mathbb R)\), and swapping the indices yields the displayed algebra isomorphism. Their equation (4.3) is instead the mixed \((1,1)\) recurrence used in Theorem 4.6.3. Chevalley's split-matrix and orthogonal-sum constructions give the same structural ingredients [chevalley1954algebraic, II.2.1 and II.2.5, pp. 42--46]. The exact splitter composition and generator formula are additional data recorded by TauCeti.

The recurrences in Theorem 4.6.3, Lemma 4.6.4, and Theorem 4.6.5 use Clifford universal properties, orthogonal sums, tensor products, coordinate isometries, and the real base entries. They do not use the Spin representation, the structure theorem obtained from a spinor module, or the Pin and Spin double covers. This is the algebraic branch of Layer 7.

The real groups \(\operatorname {Pin}(p,q)\) and \(\operatorname {Spin}(p,q)\) form a different branch. Their actions, kernels, and algebraic extensions specialize the group theory developed in § 4.2, and therefore genuinely consume the Layer-2 Pin/Spin work. The distinction between these branches is the dependency correction proposed in TauCetiRoadmap PR 225. It changes the order in which the mathematics can be built; it does not turn the roadmap proposal itself into a formal theorem.

With \(\mathcal {C}\kern -2pt\ell _{0,0}\simeq \mathbb {R}\) as the scalar anchor, the signature convention of Convention 4.6.1 gives four nontrivial base entries: \[\begin {aligned} \mathcal {C}\kern -2pt\ell _{0,0}&\simeq \mathbb {R}, & \mathcal {C}\kern -2pt\ell _{1,0}&\simeq \mathbb {R}\times \mathbb {R}, & \mathcal {C}\kern -2pt\ell _{0,1}&\simeq \mathbb {C},\\ \mathcal {C}\kern -2pt\ell _{0,2}&\simeq \mathbb {H}, & \mathcal {C}\kern -2pt\ell _{1,1}&\simeq M_2(\mathbb {R}). \end {aligned}\] For \(\mathcal {C}\kern -2pt\ell _{0,2}\), the two negative generators map to the quaternion units \(i\) and \(j\); their product maps to \(k\). Thus they square to \(-1\) and anticommute, as required by the Clifford relations. The exact generator map is recorded by TauCeti.realCliffordZeroTwoEquivQuaternion_ι.

For \(\mathcal {C}\kern -2pt\ell _{1,1}\), the positive and negative generators may be represented by \[e_+\longmapsto \begin {pmatrix}1&0\\0&-1\end {pmatrix}, \qquad e_-\longmapsto \begin {pmatrix}0&1\\-1&0\end {pmatrix}.\] Their squares are \(+I\) and \(-I\), and they anticommute. The last equivalence is also the case \(p=q=0\) of Theorem 4.6.3. The index swap in Convention 4.6.1 explains why Lawson's one-generator table lists \(\mathbb {C}\) and \(\mathbb {R}\times \mathbb {R}\) in the opposite order.

Hyperbolic reduction determines the matrix factor coming from matched positive and negative axes. It leaves a one-sided algebra \(\mathcal {C}\kern -2pt\ell _{r,0}\) or \(\mathcal {C}\kern -2pt\ell _{0,r}\). The signature-switch recurrence of Theorem 4.6.5 provides a second move, and Example 4.6.7 fixes the first real, complex, quaternionic, and matrix entries. These facts still have to be assembled into recurrences that close on each one-sided axis.

A reviewed local candidate called SPINREP-050 establishes the quaternion recurrence \[\mathcal {C}\kern -2pt\ell _{p,q+2}\simeq \mathcal {C}\kern -2pt\ell _{q,p}\otimes _{\mathbb R}\mathbb H,\] and another local candidate, SPINREP-053, iterates the recurrence chain to \[\mathcal {C}\kern -2pt\ell _{p+8,q}\simeq \mathcal {C}\kern -2pt\ell _{p,q}\otimes _{\mathbb R}M_{16}(\mathbb R).\] Neither candidate is a merged TauCeti declaration or a public TauCeti pull request, so neither receives a Lean marker here.

The residue-indexed mod-eight classification table remains unformalized. In particular, the mixed \((1,1)\) recurrence alone only removes matched axes; it cannot classify the one-sided remainder. Lawson--Michelsohn give the full classical periodicity and table in [lawson2016spin, I.4, Theorem 4.3 and Tables I--II, pp. 27--29].