Coordinate representations [fcap-0002]
✍️source

    A basis of the generating module gives coordinates on the exterior algebra, and the exterior equivalence transports those coordinates to the Clifford algebra. The empty and singleton coordinates fix the scalar and generator conventions. Orthogonality then controls how certain ordered products pass between the two algebras.

    Definition 1. Transported exterior-basis coordinates [wieser2024formalizing, 9.3.5] [fcap-0003]

      Let \(R\) be a commutative ring in which \(2\) is invertible, let \(M\) be an \(R\)-module, and choose a basis \(b\) indexed by a linearly ordered type. Write \(E_b(s)\) for the exterior-basis vector indexed by a finite subset \(s\). For a quadratic form \(Q\), the Mathlib linear equivalence CliffordAlgebra.equivExterior from \(\mathcal {C}\kern -2pt\ell (Q)\) to \(\bigwedge _R M\) gives a coordinate basis \[B_{Q,b}(s) = \operatorname {equivExterior}(Q)^{-1}(E_b(s)).\] This basis is transported through a linear equivalence. It does not say that the equivalence preserves multiplication or that Clifford multiplication becomes exterior multiplication. The basis-free construction is developed in [wieser2022formalizing].

      The exterior equivalence is treated in [wieser2024formalizing, 9.3.5].

      Two calculations anchor the choice. The empty subset maps to the scalar unit, \[B_{Q,b}(\varnothing ) = 1,\] and a singleton maps to the corresponding Clifford generator, \[B_{Q,b}(\{i\}) = \iota _Q(b(i)).\] These are module-level identities: they determine the first two coordinate types but do not determine multiplication of arbitrary coordinates.

      For subsets with several elements, a coordinate formula additionally needs an ordering convention and its attendant signs. No such convention is implicit in the transported basis.

      Lemma 2. Orthogonal pair transport [wieser2024formalizing, 8.4] [fcap-0004]

        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\). Write \(T_Q\) for the linear equivalence from \(\mathcal {C}\kern -2pt\ell (Q)\) to the exterior algebra supplied by CliffordAlgebra.equivExterior. It is a module equivalence, not an algebra equivalence.

        For vectors \(m,n \in M\), the change-of-form calculation for \(T_Q(\iota _Q(m)\iota _Q(n))\) has one extra scalar contribution, evaluated by the bilinear form associated to \(-Q\). If \(m\) and \(n\) are \(Q\)-orthogonal, that contribution vanishes. The resulting two-generator calculation is \[T_Q\bigl (\iota _Q(m)\iota _Q(n)\bigr )=\iota _0(m)\iota _0(n).\] This is the first point at which an orthogonality hypothesis changes the transport calculation. It does not turn \(T_Q\) into a multiplicative map.

        The change-of-form construction is the relevant mathematical background in [wieser2024formalizing, 8.4], and the Lean construction of \(\operatorname {equivExterior}\) is described in [wieser2024formalizing, 9.3.5]. The concrete geometric-product discussion in [wieser2024formalizing, 2.1.2] motivates the role of orthogonality, but does not provide this note's formal interface.

        Thus orthogonality removes precisely the scalar correction in the two-generator change-of-form identity. No basis or reordering convention is needed.

        References

          Reference. Formalizing clifford algebras and related constructions in the lean theorem prover [wieser2024formalizing]

          @phdthesis{wieser2024formalizing,
 title = {Formalizing Clifford algebras and related constructions in the Lean theorem prover},
 author = {Wieser, Eric},
 year = {2024}
}

          Reference. Formalizing geometric algebra in lean [wieser2022formalizing]

          • 2022
          • Eric Wieser, Utensil Song
          @article{wieser2022formalizing,
 title = {Formalizing geometric algebra in lean},
 author = {Wieser, Eric and Song, Utensil},
 year = {2022},
 journal = {Advances in Applied Clifford Algebras},
 volume = {32},
 number = {3},
 pages = {28},
 publisher = {Springer}
}

          Context

            Formalized Clifford Algebra Programme [fcap-0001]
            📄PDF

            These are the accompanying mathematical notes for the experimental research project FCAP. FCAP is read “F-cap,” and studies whether Lean can serve both as a formal language for the abstract and concrete mathematics of Clifford algebras and as an implementation language for efficient symbolic and numerical computation. It is also a coined acronym for “Formalized Clifford Algebra Programme.”

            FCAP's formalization is still at an early spike-test stage. The current storyline follows that agent-led spike test through coordinate representations and orthogonal-product transport.

            Coordinate representations [fcap-0002]
            ✍️source

              A basis of the generating module gives coordinates on the exterior algebra, and the exterior equivalence transports those coordinates to the Clifford algebra. The empty and singleton coordinates fix the scalar and generator conventions. Orthogonality then controls how certain ordered products pass between the two algebras.

              Definition. Transported exterior-basis coordinates [wieser2024formalizing, 9.3.5] [fcap-0003]

                Let \(R\) be a commutative ring in which \(2\) is invertible, let \(M\) be an \(R\)-module, and choose a basis \(b\) indexed by a linearly ordered type. Write \(E_b(s)\) for the exterior-basis vector indexed by a finite subset \(s\). For a quadratic form \(Q\), the Mathlib linear equivalence CliffordAlgebra.equivExterior from \(\mathcal {C}\kern -2pt\ell (Q)\) to \(\bigwedge _R M\) gives a coordinate basis \[B_{Q,b}(s) = \operatorname {equivExterior}(Q)^{-1}(E_b(s)).\] This basis is transported through a linear equivalence. It does not say that the equivalence preserves multiplication or that Clifford multiplication becomes exterior multiplication. The basis-free construction is developed in [wieser2022formalizing].

                The exterior equivalence is treated in [wieser2024formalizing, 9.3.5].

                Two calculations anchor the choice. The empty subset maps to the scalar unit, \[B_{Q,b}(\varnothing ) = 1,\] and a singleton maps to the corresponding Clifford generator, \[B_{Q,b}(\{i\}) = \iota _Q(b(i)).\] These are module-level identities: they determine the first two coordinate types but do not determine multiplication of arbitrary coordinates.

                For subsets with several elements, a coordinate formula additionally needs an ordering convention and its attendant signs. No such convention is implicit in the transported basis.

                Lemma. Orthogonal pair transport [wieser2024formalizing, 8.4] [fcap-0004]

                  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\). Write \(T_Q\) for the linear equivalence from \(\mathcal {C}\kern -2pt\ell (Q)\) to the exterior algebra supplied by CliffordAlgebra.equivExterior. It is a module equivalence, not an algebra equivalence.

                  For vectors \(m,n \in M\), the change-of-form calculation for \(T_Q(\iota _Q(m)\iota _Q(n))\) has one extra scalar contribution, evaluated by the bilinear form associated to \(-Q\). If \(m\) and \(n\) are \(Q\)-orthogonal, that contribution vanishes. The resulting two-generator calculation is \[T_Q\bigl (\iota _Q(m)\iota _Q(n)\bigr )=\iota _0(m)\iota _0(n).\] This is the first point at which an orthogonality hypothesis changes the transport calculation. It does not turn \(T_Q\) into a multiplicative map.

                  The change-of-form construction is the relevant mathematical background in [wieser2024formalizing, 8.4], and the Lean construction of \(\operatorname {equivExterior}\) is described in [wieser2024formalizing, 9.3.5]. The concrete geometric-product discussion in [wieser2024formalizing, 2.1.2] motivates the role of orthogonality, but does not provide this note's formal interface.

                  Thus orthogonality removes precisely the scalar correction in the two-generator change-of-form identity. No basis or reordering convention is needed.

                  Lemma. Vanishing list contraction [wieser2024formalizing, 8.4, (8.54)] [fcap-0005]

                    Let \(R\) be a commutative ring, \(M\) an \(R\)-module, \(Q\) a quadratic form on \(M\), and \(d : M \to R\) a linear functional. For a list \(l\) of generators, define an ordered product by \[P_Q([])=1, \qquad P_Q(m::l)=\iota _Q(m)P_Q(l),\] and write \(C_{Q,d}\) for left contraction by \(d\). The condition \(\forall m\in l,\ d(m)=0\) forces \(C_{Q,d}(P_Q(l))=0\).

                    There is one induction calculation. The empty product contracts to zero. At a head \(m\), the generator recurrence \[C_{Q,d}(P_Q(m::l))=d(m)P_Q(l)-\iota _Q(m)C_{Q,d}(P_Q(l))\] is the local rule in [wieser2024formalizing, 8.4, (8.54)]. The hypothesis deletes the first summand, and the induction hypothesis deletes the second. This turns the recurrence into a finite-list vanishing criterion rather than a calculation for one fixed product.

                    The conclusion depends only on the ordered recurrence and pointwise vanishing of \(d\) on the list. In particular, it is independent of a basis or any reordering convention.

                    Theorem. Pairwise orthogonal list transport [wieser2024formalizing, 8.4, (8.55)] [fcap-0006]

                      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\). For a list \(l\) of vectors, write \[P_Q([])=1, \qquad P_Q(m::l)=\iota _Q(m)P_Q(l),\] and write \(T_Q\) for the linear equivalence CliffordAlgebra.equivExterior from \(\mathcal {C}\kern -2pt\ell (Q)\) to \(\bigwedge _R M\). In the corresponding zero-form product notation, suppose every earlier vector in \(l\) is \(Q\)-orthogonal to every later vector. Then \[T_Q(P_Q(l))=P_0(l).\] The order of the list is unchanged. The equality concerns this product under the stated orthogonality condition; it does not say that \(T_Q\) preserves arbitrary products.

                      The calculation proceeds from the head of the list. The one-generator change-of-form recurrence separates \(T_Q(P_Q(m::l))\) into the zero-form generator \(\iota _0(m)\) times the transported tail and a left-contraction correction. Pairwise orthogonality makes the associated dual vector vanish on every member of the tail. The criterion in Lemma [fcap-0005] therefore kills the correction, and the induction hypothesis transports the tail.

                      The contraction recurrence in [wieser2024formalizing, 8.4, (8.54)], the change-of-form recurrence in [wieser2024formalizing, 8.4, (8.55)], and the exterior equivalence in [wieser2024formalizing, 9.3.5] supply the local identities. Their induction over a pairwise-orthogonal list gives the displayed theorem; the source locations do not state that finite-list consequence separately.

                      The order of the list is fixed throughout. Reordering would require an additional permutation-sign calculation and is not a consequence of this theorem.

                      Spin-representation roadmap [fcap-0019]

                        This appendix follows the mathematical dependencies of the spin-representation roadmap of Tau Ceti. The filtered Clifford algebra first exposes its exterior shadow. Reflections then lead to the global Pin and Spin extensions, while bivectors provide the algebraic infinitesimal orthogonal action. The Lie functor records the separate differential bridge from smooth group homomorphisms. A polarization joins the algebraic group and Lie constructions in the exterior spinor model. The real-signature recurrence and classification form a parallel algebraic branch and do not depend on the spinor-module or double-cover join.

                        The exterior shadow of a Clifford algebra [fcap-000F]

                          The Clifford relation lowers word length by two. Filtering by word length therefore separates a word from its contraction terms: the highest-degree part is alternating, and the associated graded algebra is the exterior algebra.

                          § [ca-0001]

                          Definition. Word-length filtration [chevalley1954algebraic, II.1.2 and II.1.6, pp. 40--42] [fcap-000G]
                          filtrationfiltration_mul
                          L∃∀N

                            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 [fcap-000H] and Theorem [fcap-000I] 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\).

                            Lemma. The leading symbol is exterior [chevalley1954algebraic, II.1.6, pp. 41--42] [fcap-000H]
                            changeForm_prod_map_ι_sub_prod_map_ι_mem_filtrationfiltrationLeadingTerm_apply_ιMulti
                            L∃∀N

                              Retain the coordinate-free commutative-ring and module setting of Definition [fcap-000G], 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.

                              Proof. 

                                Move a generator through the word using \[\iota (u)\iota (v)+\iota (v)\iota (u)=B_Q(u,v)1.\] The swapped word contributes the alternating sign, whereas the polar term has two fewer generators. Iterating separates the fully alternating word from terms in \(F_{n-2}\). Equivalently, changing from \(Q\) to the zero quadratic form changes a word only below its leading filtration degree.

                                Theorem. The graded pieces are exterior powers [chevalley1954algebraic, II.1.6, pp. 41--42] [fcap-000I]
                                filtrationGradedPieceEquivExteriorPowerfiltrationLeadingTerm_eq_filtrationGradedEquiv_symm
                                L∃∀N

                                  Let \(R\), \(M\), and \(Q\) be as in Lemma [fcap-000H]. 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.

                                  Theorem. PBW equivalence with the exterior algebra [meinrenken2013clifford, Proposition 2.6, pp. 33--34] [fcap-000J]
                                  filtrationAssociatedGradedEquivExterior
                                  L∃∀N

                                    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 [fcap-000I] 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.

                                    Example. The degree-two symbol [chevalley1954algebraic, II.1.6, pp. 41--42] [fcap-000K]
                                    filtrationAssociatedGradedEquivExterior_apply_of_succ
                                    L∃∀N

                                      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.

                                      Remark. Basis proof and quotient proof [fcap-000L]

                                        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.

                                        Reflections and square-normalized Clifford lifts [fcap-0007]

                                          A nonisotropic vector acts on the generating space by a reflection through twisted Clifford conjugation. Normalizing such vectors gives elements of Pin, while determinant parity detects the even products that belong to Spin. The cards pass from local lifts to reflection generation, Pin surjectivity, and finally Spin surjectivity onto the special orthogonal group.

                                          § [ca-0001]

                                          Convention. Quadratic-form sign [lawson2016spin, I.1, (1.3)--(1.4), p. 8] [fcap-0008]

                                            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.

                                            Definition. Reflection in a nonisotropic vector [lawson2016spin, I.2, (2.12), p. 14] [fcap-0009]
                                            reflection
                                            L∃∀N

                                              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\).

                                              Lemma. Twisted Clifford conjugation is a reflection [lawson2016spin, I.2, Proposition 2.2 and (2.8), p. 13; (2.11)--(2.12), p. 14] [fcap-000A]

                                                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 [fcap-0009]: \[\alpha (\iota (v))\,\iota (w)\,\iota (v)^{-1}=\iota (\rho _v(w)).\]

                                                Proof. 

                                                  The generator-square rule CliffordAlgebra.ι_sq_scalar and the anticommutator rule CliffordAlgebra.ι_mul_ι_add_swap give \[\iota (v)\iota (w)+\iota (w)\iota (v)=B_Q(v,w).\] Since \(\alpha (\iota (v))=-\iota (v)\) and \(\iota (v)^2=Q(v)\), substitution yields \[-\iota (v)\iota (w)\frac {\iota (v)}{Q(v)} =\iota (w)-\frac {B_Q(v,w)}{Q(v)}\iota (v) =\iota (\rho _v(w)).\] The ordinary adjoint differs by the leading minus sign; the twisted adjoint is the action that gives the reflection itself.

                                                  Lemma. Square-normalized Pin lift [lawson2016spin, I.2, Definition 2.3 and (2.26), pp. 14, 18] [fcap-000B]
                                                  reflection_mem_range_pinToOrthogonal_of_isSquare
                                                  L∃∀N

                                                    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.

                                                    Theorem. Paired reflections have a product-square Spin lift [lawson2016spin, I.2, (2.24)--(2.26), p. 18] [fcap-000C]
                                                    reflection_mul_reflection_mem_range_spinToOrthogonal_of_isSquare
                                                    L∃∀N

                                                      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 [fcap-000B].

                                                      Let \(R\), \(M\), and \(Q\) be as in Lemma [fcap-000B]. 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}).\]

                                                      Proof. 

                                                        The displayed square identity gives \(Q(cv)Q(w)=c^2Q(v)Q(w)=1\). Each generator is a Clifford unit and lies in the Lipschitz group, while the star calculation above establishes the unitary condition. The twisted adjoint is multiplicative on Clifford units, and scalar rescaling does not change a reflection. Hence the action of \(x\) is \(\rho _{cv}\rho _w=\rho _v\rho _w\); its even degree supplies the remaining Spin condition.

                                                        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.

                                                        Example. A Euclidean unit normal [lawson2016spin, I.2, (2.12), p. 14; (2.24)--(2.26), p. 18] [fcap-000D]

                                                          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 [fcap-000B]. 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 [fcap-000B] and Theorem [fcap-000C].

                                                          Remark. From individual lifts to generation [lawson2016spin, I.2, Proposition 2.2, Definition 2.3, and (2.24)--(2.26), pp. 13--18] [fcap-000E]

                                                            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 [fcap-000B] and Theorem [fcap-000C] 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.

                                                            From reflection generation to Pin and Spin [fcap-000U]

                                                              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.

                                                              Lemma. Fixed-subspace correction by reflections [cartan1981theory, Section 10, pp. 10--12] [fcap-000V]
                                                              exists_mem_subgroup_mul_eqOn_sup_span_singleton_of_reflection_mem
                                                              L∃∀N

                                                                Cartan proves reflection factorization by an induction that enlarges the fixed subspace. The subgroup-valued statement below is a formalized TauCeti lemma extracted from that method. Cartan's one- or two-reflection correction is repackaged as an element of \(H\) acting trivially on \(W+Kx\).

                                                                Let \(K\) be a field of characteristic different from \(2\), let \(Q\) be a quadratic form on a \(K\)-vector space \(V\), and let \(H\le O(V,Q)\) contain every reflection in a nonisotropic vector. Suppose \(g\in O(V,Q)\) fixes a subspace \(W\) pointwise and \(x\in W^{\perp }\) has \(Q(x)\ne 0\). Then there is an element \(r\in H\) such that \[rg\vert _{W+Kx}=\operatorname {id}.\] The correction leaves the previously fixed space untouched and fixes one additional nonisotropic direction. It is either one reflection or a product of two reflections.

                                                                Proof. 

                                                                  Compare \(x\) with \(g(x)\). When \(g(x)-x\) is nonisotropic, reflection in that difference carries \(g(x)\) to \(x\); because the difference is orthogonal to \(W\), the reflection fixes \(W\). In the exceptional case \(g(x)+x\) is nonisotropic: reflection in this sum carries \(g(x)\) to \(-x\), and reflection in \(x\) supplies the second factor. Both factors fix \(W\), so their product gives the required correction.

                                                                  Lemma. Pin-range refinement of the correction [cartan1981theory, Section 10, pp. 10--12]; [lawson2016spin, I.2, (2.26) and Theorem 2.9, pp. 18--19] [fcap-0018]
                                                                  exists_mem_range_pinToOrthogonal_mul_eqOn_sup_span_singleton
                                                                  L∃∀N

                                                                    Under the hypotheses of Lemma [fcap-000V], suppose moreover that \(K\) is separably closed and take \(H\) to be the range of the Pin action. Over a separably closed field, TauCeti's fixed-sign square condition from Theorem [fcap-000X] holds, so every reflection factor used by the correction has a square-normalized Pin lift by Lemma [fcap-000B]. The correcting element \(r\) can therefore be chosen in \[\operatorname {range}(\operatorname {pinToOrthogonal}),\] and still satisfies \(rg\vert _{W+Kx}=\operatorname {id}\). The statement concerns the correcting element in the Pin-action range; in the exceptional case it is the image of a product of two Pin lifts, not the image of a single reflecting vector.

                                                                    Theorem. Cartan--Dieudonne generation [lawson2016spin, I.2, Theorem 2.7, p. 17] [fcap-000W]
                                                                    subgroup_eq_top_of_reflection_mem
                                                                    L∃∀N

                                                                      Let \(K\) be a field of characteristic different from \(2\), let \(V\) be finite-dimensional, and let \(Q\) be nondegenerate. Every orthogonal transformation is a product of reflections in nonisotropic vectors. Equivalently, if a subgroup \(H\le O(V,Q)\) contains every such reflection, then \[H=O(V,Q).\] This formulation asserts generation only; it records neither a sharp bound on the number of reflection factors nor a parity formula for such a factorization.

                                                                      Proof. 

                                                                        Begin with the zero fixed subspace, whose restricted polar form is nondegenerate. If the current nondegenerate fixed subspace is not all of \(V\), its orthogonal complement is nonzero and nondegenerate, hence contains a nonisotropic vector. The correction step of Lemma [fcap-000V] enlarges the fixed subspace by that orthogonal line and preserves nondegeneracy. Finite-dimensional induction eventually makes the corrected product the identity, expressing the original transformation as a product of reflections. Cartan gives this fixed-vector induction, including the isotropic-difference case, in [cartan1981theory, Section 10, pp. 10--12].

                                                                        Theorem. Surjectivity of the Pin action [lawson2016spin, I.2, Theorem 2.9, pp. 18--19] [fcap-000X]
                                                                        pinToOrthogonal_surjective_of_isSquarepinToOrthogonal_surjective
                                                                        L∃∀N

                                                                          Let \(K\), \(V\), and \(Q\) be as in Theorem [fcap-000W]. Suppose every scalar \(-Q(v)^{-1}\) attached to a nonisotropic vector is a square in \(K\). Then the twisted-adjoint homomorphism is surjective: \[\operatorname {pinToOrthogonal}:\operatorname {Pin}(V,Q)\twoheadrightarrow O(V,Q).\] Indeed, Lemma [fcap-000B] puts every reflection in its range, and Theorem [fcap-000W] says that those reflections generate the target. In particular the conclusion holds over a separably closed field.

                                                                          Lawson and Michelsohn ask whether a nonzero vector can be rescaled to quadratic length either \(+1\) or \(-1\); see (2.26) and the discussion preceding Theorem 2.9. Under the convention \(Q=-q\), TauCeti's hypothesis asks for the particular scalar \(-Q(v)^{-1}\) to be a square, so every reflecting vector is normalized to one fixed sign. This is a sufficient and generally stronger condition, not an equivalent reformulation of Lawson--Michelsohn's condition.

                                                                          Example. A planar rotation as two reflections [lawson2016spin, I.2, (2.24)--(2.26), p. 18] [fcap-000Y]

                                                                            In an oriented Euclidean plane, let \(u\) and \(v\) be unit normals whose directed angle is \(\frac {\theta }{2}\). Reflection in \(u^{\perp }\) followed by reflection in \(v^{\perp }\) is rotation through \(\theta \). With the convention \(Q=-\langle -,-\rangle \), both vectors have \(Q=-1\), and \[s=\iota (v)\iota (u)\in \operatorname {Spin}(V,Q)\] lifts that rotation. In an oriented orthonormal basis \(e_1,e_2\), the familiar rotor form is \[\pm s=\cos \left (\frac {\theta }{2}\right )+\sin \left (\frac {\theta }{2}\right )\,\iota (e_1)\iota (e_2),\] after choosing the central sign and the order convention for the two reflections. This is the two-dimensional specialization of the paired lift in Theorem [fcap-000C]; the half-angle appears because the Spin element acts by conjugation on vectors.

                                                                            Lemma. Determinant parity detects the even lift [lawson2016spin, I.2, Theorems 2.7 and 2.9, pp. 17--19] [fcap-001A]
                                                                            det_reflectionmem_even_of_det_pinToOrthogonal_eq_one
                                                                            L∃∀N

                                                                              Let \(R\) be a commutative ring in which \(2\) is invertible, let \(M\) be a finite free \(R\)-module, and let \(Q\) be a quadratic form on \(M\). A reflection in a vector of invertible quadratic value has determinant \(-1\). Therefore a product of \(r\) such reflections has determinant \[(-1)^r.\] In particular, every product of an even number of reflections belongs to \(SO(M,Q)\).

                                                                              Lawson--Michelsohn state this parity argument for quadratic vector spaces over a field. The finite-free commutative-ring statement above is the formalized extension: its determinant calculation uses freeness and finiteness, while invertibility of \(2\) identifies the fixed part of the grading involution with the even subalgebra.

                                                                              The Clifford lift remembers this parity. If \(p\in \operatorname {Pin}(M,Q)\) and its orthogonal action has determinant \(1\), then \(p\) lies in the even Clifford subalgebra. Hence \(p\) is a Spin element. Thus any Pin lift of a special orthogonal transformation is automatically even.

                                                                              Proof. 

                                                                                Multiplicativity of the determinant gives the first assertion from \(\det (\rho _v)=-1\). For the second, the grading involution of a Lipschitz element is its determinant sign times that element. If the determinant is \(1\), the involution fixes the Pin element. Because \(2\) is invertible, the fixed submodule of the grading involution is precisely the even Clifford subalgebra.

                                                                                Theorem. Surjectivity of the Spin action [lawson2016spin, I.2, Theorem 2.9, pp. 18--19] [fcap-001B]
                                                                                spinToSpecialOrthogonal_surjective_of_isSquarespinToSpecialOrthogonal_surjective
                                                                                L∃∀N

                                                                                  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 [fcap-000X]. It lifts an element of \(SO(V,Q)\) to Pin; the lift has determinant \(1\), so Lemma [fcap-001A] 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 [fcap-000X]. 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.

                                                                                  Lemma. The real Spin kernel is the scalar pair [gallier2014clifford, Section 1.8, Proposition 1.21, pp. 39--40] [fcap-001C]
                                                                                  zmodTwoMulEquivKerSpinToSpecialOrthogonal
                                                                                  L∃∀N

                                                                                    For a real quadratic space of signature \((p,q)\), the kernel of the Spin action is the scalar pair: \[(\mathbb Z/2\mathbb Z)_{\mathrm {mult}} \simeq \ker \bigl (\operatorname {Spin}(p,q)\longrightarrow SO(p,q)\bigr ).\] The nontrivial residue class maps to the scalar Clifford element \(-1\). Thus the two kernel elements are precisely \(1\) and \(-1\). This is the kernel used in Gallier's real double-cover theorem.

                                                                                    TauCeti proves the analogous algebraic statement over a field \(K\): \(V\) is nontrivial and finite-dimensional, \(Q\) is nondegenerate, and \(2\) is invertible in \(K\). Under exactly those hypotheses it constructs the displayed canonical multiplicative equivalence. This is a generalization of the cited real result, not an attribution of arbitrary-field kernel classification to Gallier.

                                                                                    Theorem. The algebraic Spin extension [meinrenken2013clifford, Definition 3.2, pp. 51--52] [fcap-001D]
                                                                                    spinDoubleCoverOfSurjectivespinDoubleCover
                                                                                    L∃∀N

                                                                                      Let \(K\) be a characteristic-zero field, let \(V\) be finite-dimensional, and let its bilinear form be nondegenerate. Meinrenken defines Spin as the even part of the norm-one Clifford group. Its kernel is the scalar pair. If the Spin action is surjective, these data form the group extension \[1\longrightarrow (\mathbb Z/2\mathbb Z)_{\mathrm {mult}} \longrightarrow \operatorname {Spin}(Q)\longrightarrow SO(Q)\longrightarrow 1.\] The left map sends the nontrivial class to \(-1\); the right map is the Spin action. TauCeti packages this generic construction from an explicit surjectivity proof. The group-extension constructor used in that package is GroupExtension.ofMulEquivKer.

                                                                                      Meinrenken warns that the map to \(SO(V)\) need not be surjective over a general field; it is surjective when every element of \(K\) has a square root, because lifts can then be rescaled to have norm one. TauCeti separates this issue explicitly. Its generic construction assumes a field, a nontrivial finite-dimensional module, invertible \(2\), a nondegenerate quadratic form, and a supplied surjectivity proof. Over a separably closed field, Theorem [fcap-001B] supplies that proof and yields the specialized extension.

                                                                                      Lemma. The real Pin kernel is the scalar pair [gallier2014clifford, Section 1.8, Proposition 1.21, pp. 39--40] [fcap-001E]
                                                                                      zmodTwoMulEquivKerPinToOrthogonal
                                                                                      L∃∀N

                                                                                        For a real quadratic space of signature \((p,q)\), the Pin action has the same two-element kernel: \[(\mathbb Z/2\mathbb Z)_{\mathrm {mult}} \simeq \ker \bigl (\operatorname {Pin}(p,q)\longrightarrow O(p,q)\bigr ).\] Its nontrivial generator is the image in Pin of the scalar Spin element \(-1\). The identification is obtained by comparing the Pin kernel with the Spin kernel, not by adding a second pair of central elements. Gallier's real double-cover proof uses exactly the quotient by \(\{\pm 1\}\).

                                                                                        TauCeti transports the Spin-kernel equivalence to Pin over a field \(K\) when the module is nontrivial and finite-dimensional, \(Q\) is nondegenerate, and \(2\) is invertible. These are the formal theorem's exact assumptions; the cited scholarly claim is the real case.

                                                                                        Theorem. The algebraic Pin extension [meinrenken2013clifford, Definition 3.2, pp. 51--52] [fcap-001F]
                                                                                        pinDoubleCoverOfSurjectivepinDoubleCover
                                                                                        L∃∀N

                                                                                          In Meinrenken's characteristic-zero, finite-dimensional, nondegenerate setting, Pin is the kernel of the norm on the Clifford group. Its scalar kernel and any proof that the Pin action is surjective determine the group extension \[1\longrightarrow (\mathbb Z/2\mathbb Z)_{\mathrm {mult}} \longrightarrow \operatorname {Pin}(Q)\longrightarrow O(Q)\longrightarrow 1.\] The inclusion sends the nontrivial class to the scalar \(-1\), and the projection is the Pin action. Meinrenken notes that surjectivity can fail over a general field and that square roots for all field elements suffice to normalize lifts. TauCeti's generic theorem instead assumes a field, a nontrivial finite-dimensional module, invertible \(2\), a nondegenerate quadratic form, and an explicit surjectivity proof. Its separably closed specialization obtains that proof from the formal Cartan--Dieudonne route.

                                                                                          Remark. Algebraic extension versus topological cover [fcap-000Z]

                                                                                            The extensions in Theorem [fcap-001D] and Theorem [fcap-001F] are exact sequences of abstract groups. They record a surjective homomorphism and its two-element kernel. No topology on the groups is used.

                                                                                            For real quadratic spaces of arbitrary signature, Gallier proves that the two maps \[\operatorname {Pin}(p,q)\longrightarrow O(p,q),\qquad \operatorname {Spin}(p,q)\longrightarrow SO(p,q)\] are topological double covers [gallier2014clifford, Section 1.8, Proposition 1.21, pp. 39--40].

                                                                                            Gallier then treats the compact groups: \(\operatorname {Spin}(n)\) is path-connected for \(n\geq 2\), and for \(n\geq 3\) it is simply connected and hence the universal cover of \(SO(n)\) [gallier2014clifford, Section 1.8, pp. 40--42]. These claims are not being extended here to arbitrary signature. Kostant identifies the differential of the complex Spin cover with the quadratic Clifford Lie algebra [kostant1997clifford, Section 2.4, Theorem 8, pp. 286--287]. Those conclusions require topological or Lie-theoretic structure not supplied by an abstract group extension. They are not asserted by the four cards above.

                                                                                            Bivectors and the orthogonal Lie algebra [fcap-000M]

                                                                                              The second exterior power singled out by the PBW filtration has a second life inside the Clifford algebra. Its half-commutators are closed under the commutator bracket, and their action on generators is exactly the infinitesimal orthogonal action.

                                                                                              § [ca-0001]

                                                                                              Convention. Bivector normalizations [meinrenken2013clifford, Section 2.2.5, Proposition 2.5, p. 33] [fcap-000N]
                                                                                              bivector_defbivector_lie_ι
                                                                                              L∃∀N

                                                                                                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 \).

                                                                                                Definition. Clifford bivector [meinrenken2013clifford, Section 2.2.5, Proposition 2.5, p. 33] [fcap-000O]
                                                                                                bivectorExteriorequivExterior_bivectorExterior
                                                                                                L∃∀N

                                                                                                  For the formalized extension described in Convention [fcap-000N], 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.

                                                                                                  Lemma. A bivector acts by an infinitesimal rotation [meinrenken2013clifford, Section 2.2.10, Theorem 2.1, pp. 39--40] [fcap-000P]
                                                                                                  bivector_lie_ι
                                                                                                  L∃∀N

                                                                                                    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\).

                                                                                                    Proof. 

                                                                                                      Expand the half-commutator and move \(\iota (x)\) past \(\iota (u)\) and \(\iota (v)\) using the Clifford relation. The cubic terms cancel; the two polar terms combine to the displayed generator. Symmetry of \(B_Q\) then makes the skew-adjointness equation cancel in pairs.

                                                                                                      Theorem. Exterior bivectors are the quadratic Clifford Lie algebra [meinrenken2013clifford, Section 2.2.10, Theorem 2.1, pp. 39--40] [fcap-000Q]
                                                                                                      bivectorExteriorEquivQuadraticLieSubalgebrabivectorLieEquiv
                                                                                                      L∃∀N

                                                                                                        Over the commutative ring and module of Definition [fcap-000O], 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 [fcap-000P], 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.

                                                                                                        Theorem. Quadratic elements realize the orthogonal Lie algebra [meinrenken2013clifford, Section 2.2.10, Proposition 2.12, p. 40] [fcap-000R]
                                                                                                        soEquivQuadraticsoEquivQuadratic_lie_ι
                                                                                                        L∃∀N

                                                                                                          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 [fcap-000Q] 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].

                                                                                                          Example. An elementary skew matrix [meinrenken2013clifford, Section 2.2.10, Proposition 2.12, p. 40] [fcap-000S]
                                                                                                          bivectorEquivSo_apply_ιMultibivectorEquivSo_apply_ιMulti_mulVec
                                                                                                          L∃∀N

                                                                                                            This coordinate example specializes TauCeti's extension of the characteristic-zero construction summarized in Convention [fcap-000N]. 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 [fcap-000N]: 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.

                                                                                                            Remark. Infinitesimal and global Clifford symmetry [fcap-000T]

                                                                                                              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.

                                                                                                              Theorem. An orthogonal Lie action lifts to every Clifford module [kostant1997clifford, Section 3.1, pp. 294--295] [fcap-001O]
                                                                                                              cliffordInducedRepcliffordInducedRep_apply
                                                                                                              L∃∀N

                                                                                                                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 [fcap-000R] 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.

                                                                                                                Differentiating smooth group homomorphisms [fcap-001Q]

                                                                                                                  The quadratic Clifford construction in the preceding section is algebraic. A different bridge starts from a smooth homomorphism of Lie groups and differentiates it at the identity. This produces the functor from Lie groups to Lie algebras and explains which part of the Spin-representation roadmap is generic differential geometry, before any Lie-group structure on the abstract Spin and special orthogonal groups has been supplied.

                                                                                                                  Definition. The differential of a smooth homomorphism [liu2016lie, Section 2.1, p. 9] [fcap-001R]

                                                                                                                    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.

                                                                                                                    Lemma. The differential preserves the Lie bracket [liu2016lie, Section 2.1, p. 9] [fcap-001S]

                                                                                                                      In the setting of Definition [fcap-001R], 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.

                                                                                                                      Theorem. The Lie functor [liu2016lie, Section 2.2, p. 10] [fcap-001T]

                                                                                                                        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 [fcap-001S], 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.

                                                                                                                        Theorem. Naturality of the exponential [liu2016lie, Section 2.4, pp. 12--13] [fcap-001U]

                                                                                                                          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

                                                                                                                          commutes.

                                                                                                                          Proof. 

                                                                                                                            The curve \(t\mapsto \phi (\exp _G(tX))\) is a one-parameter subgroup of \(H\). Its tangent vector at \(t=0\) is \(\operatorname {Lie}(\phi )(X)\). The curve \(t\mapsto \exp _H(t\operatorname {Lie}(\phi )(X))\) has the same property and the same tangent vector. Uniqueness of the one-parameter subgroup with a given tangent vector identifies the curves; setting \(t=1\) proves the formula.

                                                                                                                            Example. Differentiating a matrix representation [liu2016lie, Sections 2.1 and 2.4, pp. 9, 12] [fcap-001V]

                                                                                                                              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).\]

                                                                                                                              Remark. Why explicit smoothness changes the roadmap [liu2016lie, Sections 2.1--2.4 and 2.8, pp. 9--13, 19--20]; [isaev2018theory, Section 3.1.2, pp. 106--107] [fcap-001W]

                                                                                                                                The constructions in Definition [fcap-001R]--Example [fcap-001V] 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 [fcap-000R] does not by itself supply those structures.

                                                                                                                                Polarization and the exterior spinor model [fcap-001G]

                                                                                                                                  A polarization turns Clifford generators into creation, contraction, and parity operators on an exterior algebra. The resulting Clifford action has two group restrictions and receives every orthogonal Lie action through the quadratic Clifford realization.

                                                                                                                                  Write \(S=\bigwedge _K W\) for the exterior carrier and \(\rho :\mathcal {C}\kern -2pt\ell (Q)\to \operatorname {End}(S)\) for its Clifford action. Let \(\mathfrak g\) be an external Lie algebra with an orthogonal action \(\theta :\mathfrak g\to \mathfrak {so}(V,Q)\). The diagram records the induced Lie action at the top and the Pin and Spin restrictions of \(\rho \) below.

                                                                                                                                  § [ca-0001]

                                                                                                                                  Definition. Polarization data and its carrier [chevalley1954algebraic, II.2.1--II.2.2, pp. 42--44] [fcap-001H]
                                                                                                                                  SpinPolarizationData
                                                                                                                                  L∃∀N

                                                                                                                                    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.

                                                                                                                                    Definition. Creation, contraction, and the line operator [meinrenken2013clifford, Section 3.2.2, Proposition 3.5, p. 57] [fcap-001I]
                                                                                                                                    wedgecontractlineOperator
                                                                                                                                    L∃∀N

                                                                                                                                      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].

                                                                                                                                      Lemma. The polarized Clifford relation [meinrenken2013clifford, Section 3.2.1, pp. 54--55] [fcap-001J]
                                                                                                                                      contract_wedgecliffordOperator_sq
                                                                                                                                      L∃∀N

                                                                                                                                        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.

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

                                                                                                                                          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.

                                                                                                                                          Theorem. Creation and contraction generate all endomorphisms [meinrenken2013clifford, Section 3.2.4, Theorem 3.3, pp. 59--60] [fcap-001L]
                                                                                                                                          creation_contraction_adjoin_eq_topspinAction_surjective
                                                                                                                                          L∃∀N

                                                                                                                                            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.

                                                                                                                                            Definition. The Spin and Pin representations [meinrenken2013clifford, Section 3.2.1, pp. 55--56] [fcap-001M]
                                                                                                                                            spinReppinRep
                                                                                                                                            L∃∀N

                                                                                                                                              The groups \(\operatorname {Spin}(Q)\) and \(\operatorname {Pin}(Q)\) consist of units in the Clifford algebra. Restricting the action \(\rho \) of Theorem [fcap-001K] 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.

                                                                                                                                              Lemma. The restricted actions are the Clifford action [meinrenken2013clifford, Section 3.2.1, pp. 55--56] [fcap-001N]
                                                                                                                                              spinRep_applypinRep_apply
                                                                                                                                              L∃∀N

                                                                                                                                                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.

                                                                                                                                                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.

                                                                                                                                                  Remark. Horizons beyond the exterior model [meinrenken2013clifford, Section 3.2.4, Theorem 3.3, pp. 59--60]; [kostant1997clifford, Section 2.4, Theorem 8, pp. 286--287]; [lawson2016spin, I.2, pp. 13--19] [fcap-0017]

                                                                                                                                                    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 § [fcap-001Q]. 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 [fcap-001W] 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}\).

                                                                                                                                                    Hyperbolic recurrence and real signatures [fcap-0010]

                                                                                                                                                      A positive and a negative generator form a hyperbolic plane. Adjoining that plane tensors the Clifford algebra with two-by-two real matrices. Iteration removes the common part of a real signature, while a sign switch gives a complementary one-sided recurrence. These are algebraic steps toward the real classification; the real Pin and Spin groups follow a separate branch through the double-cover theory.

                                                                                                                                                      § [ca-0001]

                                                                                                                                                      Convention. Real signature and Clifford signs [chevalley1954algebraic, II.2.9, pp. 65--66] [fcap-0011]
                                                                                                                                                      realCliffordFormrealCliffordForm_apply
                                                                                                                                                      L∃∀N

                                                                                                                                                        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.

                                                                                                                                                        Definition. The hyperbolic plane [lawson2016spin, I.4, Theorem 4.1 and (4.3), pp. 25--26] [fcap-0012]
                                                                                                                                                        realCliffordForm_one_one_applyrealBottSplitIsometry
                                                                                                                                                        L∃∀N

                                                                                                                                                          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\).

                                                                                                                                                          Theorem. The hyperbolic matrix recurrence [lawson2016spin, I.4, Theorem 4.1, (4.3), pp. 25--26] [fcap-0013]
                                                                                                                                                          hyperbolicEquivTensorrealCliffordBottEquiv_ι
                                                                                                                                                          L∃∀N

                                                                                                                                                            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

                                                                                                                                                            Lemma. Finite hyperbolic reduction [chevalley1954algebraic, II.2.9, pp. 65--66] [fcap-0014]
                                                                                                                                                            realCliffordBottIterEquivrealCliffordSignatureReductionEquiv
                                                                                                                                                            L∃∀N

                                                                                                                                                              Chevalley splits a finite-dimensional real quadratic space into hyperbolic planes and a definite remainder. TauCeti combines that classical reduction with iteration of Theorem [fcap-0013] 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.

                                                                                                                                                              Theorem. The signature-switch recurrence [lawson2016spin, I.4, Theorem 4.1 and (4.1), pp. 25--26] [fcap-001X]
                                                                                                                                                              realCliffordSignatureSwitchRecurrenceEquiv
                                                                                                                                                              L∃∀N

                                                                                                                                                                With the TauCeti signature convention of Convention [fcap-0011], 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 [fcap-0013] 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 [fcap-0013]. 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.

                                                                                                                                                                Remark. Why algebraic periodicity is a separate branch [chevalley1954algebraic, II.2.1, II.2.5, and II.2.9, pp. 42--46, 65--66]; [lawson2016spin, I.4, Theorems 4.1 and 4.3, pp. 25--29] [fcap-001Y]

                                                                                                                                                                  The recurrences in Theorem [fcap-0013], Lemma [fcap-0014], and Theorem [fcap-001X] 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 § [fcap-0007], 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.

                                                                                                                                                                  Example. Four real Clifford base entries [lawson2016spin, I.4, Theorem 4.3 and Tables I--II, pp. 27--29] [fcap-0015]
                                                                                                                                                                  realCliffordOneZeroEquivProdrealCliffordZeroOneEquivComplexrealCliffordZeroTwoEquivQuaternionrealCliffordOneOneEquivMatrix
                                                                                                                                                                  L∃∀N

                                                                                                                                                                    With \(\mathcal {C}\kern -2pt\ell _{0,0}\simeq \mathbb {R}\) as the scalar anchor, the signature convention of Convention [fcap-0011] 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 [fcap-0013]. The index swap in Convention [fcap-0011] explains why Lawson's one-generator table lists \(\mathbb {C}\) and \(\mathbb {R}\times \mathbb {R}\) in the opposite order.

                                                                                                                                                                    Remark. What the recurrence does not classify [fcap-0016]

                                                                                                                                                                      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 [fcap-001X] provides a second move, and Example [fcap-0015] 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].