Proposition. A Lorentz frame can be prescribed [fcap-002B]
✍️source

    Let \(V\) be four-dimensional over \(\mathbb R\), and let \(Q\) be a nondegenerate quadratic form with positive and negative indices \((1,3)\). Suppose \[Q(t)=1,\qquad Q(s)=-1,\qquad B_Q(t,s)=0.\] There is an isometry \(e:(\mathbb R^4,Q_{1,3})\simeq (V,Q)\) with \(e(e_0)=t\) and \(e(e_1)=s\). Moreover, \(H=\operatorname {span}(t,s)\) has an orthogonal complement of dimension two on which \(Q\) is negative definite. The sign convention for \(Q_{1,3}\) is the one fixed in Convention [fcap-0011].

    Proof. 

      For all \(a,b\in \mathbb R\), polarization gives \[Q(at+bs)=a^2-b^2.\] The polar Gram matrix of \(t,s\) is \(\operatorname {diag}(2,-2)\), so they are independent and \(H\) is regular of inertia \((1,1)\). By [bourbaki2007algebra, Section 7, no. 2, Theorem 1 and Definition 2, pp. 117--118], the real law of inertia gives an initial isometry \(j:(\mathbb R^4,Q_{1,3})\simeq (V,Q)\). The isometry from \(j(\operatorname {span}(e_0,e_1))\) to \(H\) sending \(j(e_0)\) to \(t\) and \(j(e_1)\) to \(s\) has regular source, so Witt extension supplies an ambient isometry \(g\) of \((V,Q)\) QuadraticMap.IsometryEquiv.exists_extension. Then \(e=g\circ j\) has the prescribed values.

      The orthogonal decomposition has summands \(H\) and \(H^\perp \). Additivity of the positive and negative indices QuadraticForm.sigPos_prod QuadraticForm.sigNeg_prod gives \[(1,3)=(1,1)+(0,2).\] Hence \(H^\perp \) is the required negative plane.

      The isometry transport in Proposition [fcap-0029] carries the standard first two Clifford generators to this prescribed pair and commutes with the Spin vector action. The hyperbolic split and quaternionic matrix calculation are already in Example [fcap-0026], which yields the abstract model \(\mathcal {C}\kern -2pt\ell (V,Q)\simeq M_2(\mathbb H)\). This does not identify a particular gamma-matrix homomorphism, its kernel, or its image.

      References

        Reference. Éléments de mathématique. Algèbre. Chapitre 9 [bourbaki2007algebra]

        • 2007
        • Nicolas Bourbaki
        @book{bourbaki2007algebra,
 title = {{\'E}l{\'e}ments de math{\'e}matique. {Alg{\`e}bre}.
{Chapitre} 9},
 author = {Bourbaki, Nicolas},
 year = {2007},
 isbn = {3-540-35338-0},
 edition = {Reprint of the 1959 original},
 publisher = {Berlin: Springer},
 language = {French}
}

        Context

          Hyperbolic recurrence, real signatures and quaternary centers [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. With the quaternion and eight-step recurrences, these steps yield the residue-indexed real algebra classification. In dimension three, an even algebra model becomes a group model only after reverse norm one is shown to imply membership in the vector-generated Spin carrier. For the compact and split real signatures this yields the unit Hamilton quaternions and \(SL_2(\mathbb R)\), respectively. The same carrier question in dimension four is settled by a reversal-fixed odd-degree argument. It upgrades the compact even algebra to a pair of unit-quaternion groups and the Lorentz even algebra to \(SL_2(\mathbb C)\), while their centers retain the split and nonsplit signature distinction. Over any field of characteristic different from two, the four-dimensional discriminant center similarly determines a product of two quaternion norm-one groups or one such group over a quadratic field. The compact vector actions become quaternion conjugation in dimension three and left and inverse-right multiplication in dimension four, with explicit coordinates relating these two descriptions. For the split real signatures, symmetric matrices give the action in dimension three, and a pair of real matrix groups acts by left and inverse-right multiplication in dimension four. The compact quaternion action also has a concrete special unitary matrix realization. The Lorentz action becomes congruence on Hermitian matrices, with an explicit sign and coordinate dictionary between the two Lorentz signatures. In dimension five, a central volume term survives reversal; the scalar-square equation eliminates it. In dimension six, a scalar plus a volume element instead supplies an even unit of reverse norm one that does not preserve vectors. These calculations explain the precise limit of the carrier shortcut. The real Pin and Spin groups otherwise 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--Michelsohn impose \(v^2=-q_{r,s}(v)1\) [lawson2016spin, I.3, Proposition 3.1, p. 21]. This swaps the indices while leaving the mixed \((1,1)\) recurrence unchanged: \[\mathcal {C}\kern -2pt\ell _{p,q}=\mathcal {C}\kern -2pt\ell ^{\mathrm {Lawson}}_{q,p}.\]

              Theorem. Witt extension and the regular-subspace interface [fcap-002A]

                Let \(K\) be a field of characteristic different from two, and let \((V,Q)\) and \((V',Q')\) be isometric finite-dimensional nondegenerate quadratic spaces. If \(U\subseteq V\) is any subspace and \(f:U\to V'\) is an injective linear map satisfying \[Q'(f(u))=Q(u),\] then \(f\) extends to an isometry \(\widetilde f:(V,Q)\simeq (V',Q')\). For two subspaces of one quadratic space, the assumption that the ambient spaces are isometric is automatic.

                [bourbaki2007algebra, Section 4, no. 3, Theorem 1, pp. 71--72] states the theorem with an arbitrary source subspace. In [serre1973course, Chapter IV, Section 1.5, Theorem 3, pp. 31--32], the proof explains why degeneracy of that subspace is harmless when the ambient form is nondegenerate: a radical vector can be paired with a new vector, enlarging the subspace toward a regular one. The regular case then splits orthogonally and closes by induction.

                TauCeti proves a complementary form. For a finite-dimensional quadratic space over a field with \(2\) invertible, an isometry equivalence between subspaces \(W,W'\) extends when \(Q|_W\) is nondegenerate; the ambient form itself may be degenerate QuadraticMap.IsometryEquiv.exists_extension. It also chooses an extension and records its value on \(W\) QuadraticMap.IsometryEquiv.extension QuadraticMap.IsometryEquiv.extension_apply. These formal declarations do not prove the arbitrary-subspace statement above.

                The distinction is visible inside \(Q_{1,3}\). The block \[A_0=\begin {pmatrix}5/4&3/4\\3/4&5/4\end {pmatrix}\] on the first positive and first negative coordinates, together with the identity on the other two coordinates, defines an ambient isometry \(A\). It satisfies \(A(e_0+e_1)=2(e_0+e_1)\), so its restriction to the null line is an isometry of a degenerate subspace. The classical theorem covers such a line; the regular-subspace formal declaration does not apply because the source restriction is degenerate.

                Proposition. A Lorentz frame can be prescribed [fcap-002B]
                ✍️source

                  Let \(V\) be four-dimensional over \(\mathbb R\), and let \(Q\) be a nondegenerate quadratic form with positive and negative indices \((1,3)\). Suppose \[Q(t)=1,\qquad Q(s)=-1,\qquad B_Q(t,s)=0.\] There is an isometry \(e:(\mathbb R^4,Q_{1,3})\simeq (V,Q)\) with \(e(e_0)=t\) and \(e(e_1)=s\). Moreover, \(H=\operatorname {span}(t,s)\) has an orthogonal complement of dimension two on which \(Q\) is negative definite. The sign convention for \(Q_{1,3}\) is the one fixed in Convention [fcap-0011].

                  Proof. 

                    For all \(a,b\in \mathbb R\), polarization gives \[Q(at+bs)=a^2-b^2.\] The polar Gram matrix of \(t,s\) is \(\operatorname {diag}(2,-2)\), so they are independent and \(H\) is regular of inertia \((1,1)\). By [bourbaki2007algebra, Section 7, no. 2, Theorem 1 and Definition 2, pp. 117--118], the real law of inertia gives an initial isometry \(j:(\mathbb R^4,Q_{1,3})\simeq (V,Q)\). The isometry from \(j(\operatorname {span}(e_0,e_1))\) to \(H\) sending \(j(e_0)\) to \(t\) and \(j(e_1)\) to \(s\) has regular source, so Witt extension supplies an ambient isometry \(g\) of \((V,Q)\) QuadraticMap.IsometryEquiv.exists_extension. Then \(e=g\circ j\) has the prescribed values.

                    The orthogonal decomposition has summands \(H\) and \(H^\perp \). Additivity of the positive and negative indices QuadraticForm.sigPos_prod QuadraticForm.sigNeg_prod gives \[(1,3)=(1,1)+(0,2).\] Hence \(H^\perp \) is the required negative plane.

                    The isometry transport in Proposition [fcap-0029] carries the standard first two Clifford generators to this prescribed pair and commutes with the Spin vector action. The hyperbolic split and quaternionic matrix calculation are already in Example [fcap-0026], which yields the abstract model \(\mathcal {C}\kern -2pt\ell (V,Q)\simeq M_2(\mathbb H)\). This does not identify a particular gamma-matrix homomorphism, its kernel, or its image.

                    Remark. The radical blocks an unqualified extension theorem [fcap-002C]

                      For \(Q(a,b,c)=a^2-b^2\) on \(\mathbb R^3\), with \(e_1,e_2,e_3\) the standard coordinate basis, the radical is \(\mathbb R e_3\). The zero-form lines \(\mathbb R e_3\) and \(\mathbb R(e_1+e_2)\) are isometric by \(e_3\mapsto e_1+e_2\), but this map has no ambient isometric extension. Every ambient isometry preserves the radical, whereas \[B_Q(e_1+e_2,e_1)=2,\] so \(e_1+e_2\) is not radical. This example lies outside both guards above: the ambient form is degenerate, and the source line is not regular.

                      For the projective-geometric-algebra form \(Q_{\mathrm {PGA}}(a,b,c)=a^2+b^2\), the positive, negative, and radical dimensions are \((2,0,1)\), with radical \(\mathbb R e_3\). Its radical quotient is a two-dimensional positive-definite space. Quotienting preserves the positive and negative indices QuadraticForm.sigPos_lift_radical QuadraticForm.sigNeg_lift_radical, but it changes the quadratic space. It therefore cannot silently replace the original degenerate Clifford algebra or its motor carrier. Failure of the classical ambient nondegeneracy hypothesis does not show that extension fails for PGA; TauCeti's regular-subspace theorem may still apply there.

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

                                  Lemma. Reverse norm one is the Spin carrier in real dimension three [fcap-002G]

                                    Let \(V\) be a three-dimensional real vector space and let \(Q\) be nondegenerate. Suppress the canonical generator map in Clifford products. For \(x\in \mathcal {C}\kern -2pt\ell ^{+}(Q)\), the following are equivalent: \[x\text { is the Clifford value of an element of }\operatorname {Spin}(Q), \qquad \operatorname {rev}(x)x=1.\] The forward implication is the even-unitary condition CliffordAlgebra.evenUnitaryGroup.mem_iff_reverse_mul_self_eq_one CliffordAlgebra.range_spinGroup_toUnits.

                                    For the converse, the scalar--bivector decomposition in dimension three writes \(x=a+Z\). Every nonzero bivector is decomposable. If \(Z\ne 0\), let \(P\) be its supporting two-plane. The plane contains \(u\) with \(Q(u)\ne 0\): otherwise polarization would give \(P\subseteq P^\perp \), impossible because \(\dim P=2\) and nondegeneracy gives \(\dim P^\perp =1\). Since \(\bigwedge ^2P\) is one-dimensional, choose \(w\in P\) so that \(Z=\beta _Q(u,w)\). If \(Z=0\), choose any nonisotropic \(u\) and take \(w=0\). Using the unhalved polar form from Convention [fcap-0027], \[\beta _Q(u,w)=uw-\frac 12B_Q(u,w),\qquad v:=ux=\left (a-\frac 12B_Q(u,w)\right )u+Q(u)w.\] Thus \(v\) is a vector. Reversal and the norm-one equation give \[Q(v)1=\operatorname {rev}(v)v =\operatorname {rev}(x)uux =Q(u)\operatorname {rev}(x)x=Q(u)1.\] The real scalar map is injective, so \(Q(v)=Q(u)\ne 0\). Consequently \[x=\left (\frac {u}{Q(u)}\right )v, \qquad Q\left (\frac {u}{Q(u)}\right )Q(v)=1.\] This is a product of two actual nonisotropic vectors, and TauCeti's pair criterion places it in Spin CliffordAlgebra.ι_mul_ι_mem_spinGroup_of_norm_mul_norm_eq_one. The proof includes the scalar case \(Z=0\); it uses neither a normalizer characterization nor a connectedness argument. The general distinction between reverse norm one and Lipschitz membership remains the one recorded in Remark [fcap-0028].

                                    Example. The compact three-dimensional Spin group is the unit quaternions [fcap-002H]

                                      Let \(Q_{3,0}(x_0,x_1,x_2)=x_0^2+x_1^2+x_2^2\) and write \(e_0,e_1,e_2\) for its coordinate basis. TauCeti's chosen algebra equivalence \(\theta :\mathcal {C}\kern -2pt\ell ^{+}(Q_{3,0})\simeq \mathbb H\) has the exact axes \[e_0e_1\longmapsto -k,\qquad e_0e_2\longmapsto i,\qquad e_1e_2\longmapsto j\] TauCeti.realCliffordThreeZeroEvenEquivQuaternion TauCeti.realCliffordThreeZeroEvenEquivQuaternion_ι_single_zero_one TauCeti.realCliffordThreeZeroEvenEquivQuaternion_ι_single_two_zero TauCeti.realCliffordThreeZeroEvenEquivQuaternion_ι_single_one_two. Hence \[\theta (s+A e_0e_1+B e_0e_2+C e_1e_2) =s+B i+C j-A k.\] Under \(\theta \), reversal is quaternion conjugation and reverse norm is \[s^2+A^2+B^2+C^2\] TauCeti.realCliffordThreeZeroEvenEquivQuaternion_reverseEven TauCeti.realCliffordThreeZeroEvenEquivQuaternion_map_reverseEven_mul_self_eq_normSq.

                                      Let \(\mathbb H^1=\{q\in \mathbb H:\bar q q=1\}\). Restricting \(\theta \) to Spin gives a homomorphism \[\operatorname {Spin}(Q_{3,0})\longrightarrow \mathbb H^1.\] For \(q=r+x i+y j+z k\in \mathbb H^1\), the inverse Clifford value is \[r-z e_0e_1+x e_0e_2+y e_1e_2.\] Its reverse norm is one, so the dimension-three carrier lemma places it in the actual Spin group. The algebra inverse proves both compositions and multiplicativity. Therefore \[\operatorname {Spin}(Q_{3,0})\simeq \mathbb H^1.\] TauCeti separately packages the algebra map as an equivalence between the even-unitary carrier and unit quaternions TauCeti.realCliffordThreeZeroEvenUnitaryEquivQuaternionUnitary; the preceding carrier lemma is what identifies that carrier with Spin in this real dimension-three case.

                                      In [gallier2014clifford, Section 1.4, pp. 28--29], the analogous compact calculation writes the even element, obtains its sum-of-four-squares norm, and identifies the unit quaternions. Its generators square to \(-1\). Likewise, [lawson2016spin, I.3, Theorem 3.7, pp. 23--24; I.4, (4.0), p. 25] uses \(v^2=-q(v)\) to reduce an even algebra and identify the quaternion base entry. Translating by \(Q=-q\) and the even sign-change equivalence gives the same compact algebra and norm. The displayed axis signs are the exact TauCeti choice above, rather than a relabeling imported from either source.

                                      Example. The compact three-dimensional Spin action is quaternion conjugation [fcap-003J]

                                      • October 8, 2026

                                      For \(Q_{3,0}=x_0^2+x_1^2+x_2^2\), use the algebra map \(\theta :\mathcal {C}\kern -2pt\ell ^+(Q_{3,0})\simeq \mathbb H\) of Example [fcap-002H]. The vector isometry to pure quaternions is \[\eta _3(v_0e_0+v_1e_1+v_2e_2)=-v_1i+v_0j-v_2k.\] For \(s\in \operatorname {Spin}(Q_{3,0})\) and \(q=\theta (s)\in \mathbb H^1\), the ordinary Clifford conjugation action satisfies \[\eta _3(svs^{-1})=q\eta _3(v)\bar q.\] These are the coordinates and action in TauCeti TauCeti.coe_realCliffordThreeZeroPureQuaternionEquiv_apply TauCeti.realSpinThreeEquivQuaternionUnitary_action.

                                      The volume element \(\omega =e_0e_1e_2\) is central and has \(\omega ^2=-1\). Multiplying a vector by it gives \[v\omega =v_0e_1e_2+v_1e_2e_0+v_2e_0e_1,\qquad \eta _3(v)=\theta (v\omega ).\] The three coefficients are only permuted and signed, so \(\eta _3\) is an isometry onto the pure quaternions. Since \(\omega \) is central, \[(svs^{-1})\omega =s(v\omega )s^{-1}.\] Apply \(\theta \); reversal on the even algebra becomes quaternion conjugation, and \(q^{-1}=\bar q\). This proves the displayed action formula.

                                      The axes also determine the sign of the rotation. For real \(t\), put \(s=\cos t+\sin t\,e_0e_1\). Its reverse norm is one, hence it belongs to Spin by Example [fcap-002H], and \(q=\cos t-\sin t\,k\). Direct multiplication gives \[\begin {aligned} se_0s^{-1}&=\cos (2t)e_0-\sin (2t)e_1,\\ se_1s^{-1}&=\sin (2t)e_0+\cos (2t)e_1,\\ se_2s^{-1}&=e_2. \end {aligned}\] In quaternion coordinates the first identity is \(qj\bar q=\cos (2t)j+\sin (2t)i\), since \(\eta _3(e_1)=-i\). Thus the rotor parameter is a half-angle with the orientation fixed by the stated Clifford and quaternion axes.

                                      Gallier [gallier2014clifford, Section 1.4, p. 29] proves the same volume-element transport to quaternion conjugation with compact generators of square \(-1\). His volume has square \(+1\), and his map is \(v\mapsto -\omega v\); for the positive squares here it is \(v\mapsto v\omega \), followed by the axes of Example [fcap-002H]. Porteous [porteous1995clifford, Chapter 8, Propositions 8.19--8.21, pp. 62--63] describes the resulting unit-quaternion rotations of pure quaternions. The signed half-angle calculation above specifies this action in the coordinates used here.

                                      Example. The split three-dimensional Spin group is \(SL_2(\mathbb R)\) [fcap-002I]

                                        For \(Q_{2,1}(x_0,x_1,x_2)=x_0^2+x_1^2-x_2^2\), set \(A=e_0e_1\), \(B=e_0e_2\), and \(C=e_1e_2\). Then \[A^2=-1,\qquad B^2=C^2=1,\qquad AB=-C.\] The assignments \[A\longmapsto \begin {pmatrix}0&1\\-1&0\end {pmatrix},\qquad B\longmapsto \begin {pmatrix}0&1\\1&0\end {pmatrix},\qquad C\longmapsto \begin {pmatrix}-1&0\\0&1\end {pmatrix}\] satisfy these relations, and the images of \(1,A,B,C\) form a basis of \(M_2(\mathbb R)\). They therefore define an algebra equivalence \(\Phi \) with \[\Phi (s+aA+bB+cC)= \begin {pmatrix}s-c&a+b\\-a+b&s+c\end {pmatrix}.\] Reversal negates \(A,B,C\), so it becomes matrix adjugation, and \[N_{\mathrm {rev}}(s+aA+bB+cC) =s^2+a^2-b^2-c^2=\det \Phi (s+aA+bB+cC)\] CliffordAlgebra.map_reverseEven_eq_adjugate_of_finrank_eq_three CliffordAlgebra.reverseEven_mul_eq_one_iff_det_eq_one_of_finrank_eq_three.

                                        Restriction gives \(\operatorname {Spin}(Q_{2,1})\to SL_2(\mathbb R)\). Conversely, if \(M=(m_{ij})\in SL_2(\mathbb R)\), put \[\begin {aligned} s&=\frac {m_{00}+m_{11}}2,& a&=\frac {m_{01}-m_{10}}2,\\ b&=\frac {m_{01}+m_{10}}2,& c&=\frac {m_{11}-m_{00}}2. \end {aligned}\] Then \(\Phi (s+aA+bB+cC)=M\), and its reverse norm is \(\det M=1\). The carrier lemma puts this inverse value in the actual Spin group; the algebra maps give two-sided multiplicative inverses. Thus \[\operatorname {Spin}(Q_{2,1})\simeq SL_2(\mathbb R).\]

                                        The source translation matters. Lawson--Michelsohn's convention turns this even algebra into \(\operatorname {Cl}_{0,2}\simeq M_2(\mathbb R)\) via [lawson2016spin, I.3, Theorem 3.7, pp. 23--24; I.4, (4.0), p. 25]. With the reversed index convention, [gallier2014clifford, Example 1.3, p. 33] independently records \(\operatorname {Cl}_{2,0}\simeq M_2(\mathbb R)\), the same real matrix base algebra. Their indefinite Pin/Spin carrier conventions allow factors of quadratic value \(\pm 1\) [lawson2016spin, I.2, (2.24)--(2.25), p. 18] [gallier2014clifford, Section 1.5, Definition 1.6, p. 31]. We use their algebra identifications but impose the displayed reverse-norm-one equation. For example, \(e_0e_2\) has reverse norm \(-1\) and maps to a determinant \(-1\) matrix, so it is excluded here.

                                        This split form has polarization \(W=\mathbb R(e_0+e_2)\), \(W'=\mathbb R((e_0-e_2)/4)\), and line \(\mathbb R e_1\): the unhalved polar pairing of the displayed generators is \(1\), and the line coordinate squares to \(Q_{2,1}\). TauCeti's polarized dimension-three theorem therefore gives an independent abstract group equivalence with \(SL_2(\mathbb R)\) TauCeti.exists_spinGroup_mulEquiv_specialLinearGroup_and_spinRep_equiv_stdSLRep_of_finrank_eq_three. The concrete map \(\Phi \) above is not asserted to be definitionally that map, and the theorem's representation refinement belongs to the later module packet. Likewise, the vector-action image is the spinor-norm kernel from Theorem [fcap-0023], not all of \(SO(2,1)\). No component or covering-space claim is made.

                                        Example. The split three-dimensional Spin action is symmetric matrix congruence [fcap-003X]

                                          For \(Q_{2,1}(v)=v_0^2+v_1^2-v_2^2\), keep the algebra map \(\Phi :\mathcal {C}\kern -2pt\ell ^+(Q_{2,1})\simeq M_2(\mathbb R)\) of Example [fcap-002I]. Multiplication by the last generator gives symmetric matrix coordinates \[X(v)=\Phi (ve_2)= \begin {pmatrix}-v_2-v_1&v_0\\v_0&-v_2+v_1\end {pmatrix}, \qquad \det X(v)=-Q_{2,1}(v).\] The inverse sends \(\begin {pmatrix}a&b\\b&d\end {pmatrix}\) to \((b,(d-a)/2,-(a+d)/2)\). Thus \(X\) is a real linear equivalence onto the symmetric matrices, with the stated negative determinant form TauCeti.coe_realCliffordTwoOneVectorEquivSymmetric_apply TauCeti.realCliffordTwoOneVectorEquivSymmetric_det. For \(s\in \operatorname {Spin}(Q_{2,1})\) and \(M=\Phi (s)\in SL_2(\mathbb R)\), the vector action becomes \[X(svs^{-1})=M X(v)M^{\mathsf T}.\]

                                          To prove the formula, write \(A=e_0e_1\), \(B=e_0e_2\), and \(C=e_1e_2\). Since \(e_2^2=-1\), conjugation by \(e_2\) is \(\gamma (x)=-e_2xe_2\). It fixes \(A\) and negates \(B,C\). On their three matrices in Example [fcap-002I], and on the identity, this gives \[\Phi (\gamma (x))=\operatorname {adj}(\Phi (x))^{\mathsf T}.\] Both sides are linear in \(x\), so the basis check proves the equality on the whole even algebra. Moreover, \[(svs^{-1})e_2=s(ve_2)\gamma (s^{-1}).\] The determinant-one equation gives \(\operatorname {adj}(M^{-1})=M\); applying \(\Phi \) proves the action. TauCeti's bilinear-generator formula sends \(A,B,C\) to exactly these three matrices, so its group map and action use this same \(\Phi \) TauCeti.realCliffordTwoOneEvenEquivMatrix_ι TauCeti.realSpinTwoOneEquivSpecialLinear_action.

                                          For example, let \(M=\operatorname {diag}(a,a^{-1})\) with \(a>0\), and choose its Spin preimage using Example [fcap-002I]. Put \(c=(a^2+a^{-2})/2\) and \(h=(a^2-a^{-2})/2\). The congruence action is \[v_0'=v_0,\qquad v_1'=cv_1+hv_2,\qquad v_2'=hv_1+cv_2.\] Here \(c^2-h^2=1\). The two null coordinates \(v_1+v_2\) and \(v_1-v_2\) are multiplied by \(a^2\) and \(a^{-2}\), respectively. This exhibits the action on both null directions in the chosen coordinates.

                                          For comparison, the compact quaternion action of Example [fcap-003J] has a complex matrix realization. Distinguish quaternion units \(\mathbf i,\mathbf j,\mathbf k\) from the complex scalar \(i\). The map \[\iota (a+b\mathbf i+c\mathbf j+d\mathbf k)= \begin {pmatrix}a+ib&c+id\\-c+id&a-ib\end {pmatrix}\] preserves multiplication and sends quaternion conjugation to conjugate transpose. Its determinant is \(a^2+b^2+c^2+d^2\), so it identifies the unit quaternions with \(SU(2)\). Indeed a special unitary matrix has the form \(\begin {pmatrix}z&w\\-\bar w&\bar z\end {pmatrix}\) with \(|z|^2+|w|^2=1\), which recovers the four real coordinates. These are Gallier's axes [gallier2014clifford, Section 1.1, pp. 8--9], and the exact embedding and group equivalence in TauCeti Quaternion.toComplexMatrix Quaternion.unitaryEquivSpecialUnitaryGroup.

                                          Keep \(\eta _3(v)=-v_1\mathbf i+v_0\mathbf j-v_2\mathbf k\) from Example [fcap-003J], and put \(K(v)=i\iota (\eta _3(v))\). It is a traceless Hermitian matrix. Applying \(i\iota \) to the already proved quaternion action gives \[K(svs^{-1})=U K(v)U^*,\qquad U=\iota (\theta (s))\in SU(2),\] where \(U^*\) is conjugate transpose. The composite Spin-to-\(SU(2)\) isomorphism is available in TauCeti TauCeti.realSpinThreeEquivSpecialUnitary. Its action theorem uses the unscaled matrix \(\iota (\eta _3(v))\) TauCeti.realSpinThreeEquivSpecialUnitary_action; multiplication by the central scalar \(i\) gives the displayed \(K\) formula. Thus neither quaternion nor vector axes change. The split formula uses real symmetric matrices and \(SL_2(\mathbb R)\) instead. The fixed-vector transport underlying these formulas is illustrated by [porteous1995clifford, Chapter 16, Proposition 16.9, pp. 143--144]. For the indefinite vector-action image, retain the spinor-norm kernel of Theorem [fcap-0023]; no component or covering-space assertion is needed.

                                          Definition [spin-000O]Definition [ca-001J]

                                          Lemma. Reverse norm one is the Spin carrier in real dimension four [fcap-002J]

                                            Let \(V\) be a four-dimensional real vector space and let \(Q\) be nondegenerate. Suppress the canonical generator map in Clifford products. For \(x\in \mathcal {C}\kern -2pt\ell ^{+}(Q)\), the following are equivalent: \[x\text { is the Clifford value of an element of }\operatorname {Spin}(Q), \qquad \operatorname {rev}(x)x=1.\] The forward implication follows from the exact Spin-carrier description CliffordAlgebra.range_spinGroup_toUnits.

                                            Conversely, suppose \(\operatorname {rev}(x)x=1\). Since the Clifford algebra is finite-dimensional, the displayed left inverse is also a right inverse, so \(x\) is a unit and \(x^{-1}=\operatorname {rev}(x)\). For \(v\in V\), put \(w=xvx^{-1}\). The element \(w\) is odd, and \[\operatorname {rev}(w) =\operatorname {rev}(x^{-1})v\operatorname {rev}(x) =xvx^{-1}=w.\] In an orthogonal-basis Clifford expansion in dimension four, the odd part has only degrees one and three. Reversal is \(+1\) on degree one and \(-1\) on degree three, so \(w\in V\). Gallier uses this observation in the compact calculation [gallier2014clifford, p. 30]; the same basis-and-reversal argument applies to every nondegenerate real form in dimension four. Also \(w^2=Q(v)1\). Conjugation is injective, and its restriction to the finite-dimensional space \(V\) is therefore an automorphism. Thus it defines \(g\in O(V,Q)\).

                                            Choose \(y\) in the vector-generated Lipschitz group whose twisted action is \(g\) CliffordAlgebra.lipschitzToOrthogonal_surjective, and set \(z=y^{-1}x\). Since \(x\) is even, equality of the two actions rearranges for the grading involution \(\alpha \) to \[\alpha (z)v=vz\qquad (v\in V).\] The graded-centrality theorem therefore gives \(z=c1\) for some real \(c\) CliffordAlgebra.exists_eq_algebraMap_of_involute_mul_ι_eq_ι_mul. The unit \(z\) has \(c\ne 0\). Nondegeneracy and positive dimension supply a nonisotropic vector, so every nonzero scalar unit belongs to the generated Lipschitz group CliffordAlgebra.unitsMap_algebraMap_mem_lipschitzGroup. Thus \(x=yz\) is Lipschitz. It is even and has reverse norm one, hence lies in Spin by Remark [fcap-0028]. This dimension-sensitive argument is not asserted in dimension five or six.

                                            Example. The compact four-dimensional Spin group is a pair of unit quaternions [fcap-002K]

                                              For \(Q_{4,0}=x_0^2+x_1^2+x_2^2+x_3^2\), let \(I=e_0e_1e_2e_3\). Then \(I^2=1\), \(\operatorname {rev}(I)=I\), and \(I\) commutes with the even algebra CliffordAlgebra.prod_map_ι_sq_scalar CliffordAlgebra.prod_map_ι_mul_ι_of_even_length. Let \(H_0\) be the quaternion subalgebra with basis \(1,e_0e_1,e_0e_2,e_1e_2\), and choose \(\theta _0:H_0\simeq \mathbb H\) with the quaternion axes of Example [fcap-002H]: \[e_0e_1\longmapsto -k,\qquad e_0e_2\longmapsto i,\qquad e_1e_2\longmapsto j.\] The eight even basis monomials show uniquely that every even value is \(u+Iv\) with \(u,v\in H_0\). Centrality and \(I^2=1\) make \[\Phi (u+Iv) =\bigl (\theta _0(u)+\theta _0(v),\theta _0(u)-\theta _0(v)\bigr )\] an algebra map. Its inverse is \[(q_+,q_-) \longmapsto \theta _0^{-1}\left (\frac {q_++q_-}{2}\right ) +I\theta _0^{-1}\left (\frac {q_+-q_-}{2}\right ).\] These formulas prove both multiplicativity and bijectivity.

                                              Reversal becomes quaternion conjugation in each factor. If \(\mathbb H^1=\{q\in \mathbb H:\bar q q=1\}\) and \(\Phi (x)=(q_+,q_-)\), then \[\Phi (\operatorname {rev}(x)x) =(\bar q_+q_+,\bar q_-q_-),\qquad \operatorname {Spin}(Q_{4,0})\simeq \mathbb H^1\times \mathbb H^1.\] The forward restriction lands in the displayed product. Conversely, the written algebra inverse sends a pair of unit quaternions to an even unit of reverse norm one, and the dimension-four carrier lemma places it in the actual Spin group. No connectedness or covering-space argument is used.

                                              Gallier computes the same \(u+Iv\mapsto (u+v,u-v)\) decomposition, norm equations, and compact group product using negative-square compact generators [gallier2014clifford, pp. 29--30]. Lawson--Michelsohn independently give the compact even-algebra reduction [lawson2016spin, I.3, Theorem 3.7, pp. 23--24] and the \(\mathbb H\oplus \mathbb H\) entry [lawson2016spin, I.4, Table I, p. 28]. Their relation \(v^2=-q(v)\) and the index translation of Convention [fcap-0011] account for the sign change. The axis labels above are those fixed in Example [fcap-002H], not labels imported from either source. Finally, \((1\pm I)/2\) are the two nonzero complementary central idempotents, so the even center is the split algebra \(\mathbb R\oplus \mathbb R\).

                                              Example. The compact four-dimensional Spin action is left and right quaternion multiplication [fcap-003K]

                                                For \(Q_{4,0}=x_0^2+x_1^2+x_2^2+x_3^2\), keep the algebra map \(\Phi :\mathcal {C}\kern -2pt\ell ^+(Q_{4,0})\simeq \mathbb H\times \mathbb H\) of Example [fcap-002K]. Write \(\Phi (s)=(q_+,q_-)\) for \(s\in \operatorname {Spin}(Q_{4,0})\). In the quaternion coordinates \[W(v_0e_0+v_1e_1+v_2e_2+v_3e_3)=-v_3-v_1i+v_0j-v_2k,\] the vector action is \[W(svs^{-1})=q_+W(v)\bar q_-.\] The signed permutation \(W\) identifies the Euclidean vector norm with the quaternion norm. Both factors are unit quaternions, so the right multiplier is the inverse of \(q_-\).

                                                To prove the formula, let \(I=e_0e_1e_2e_3\) and use the quaternion subalgebra \(H_0\) from Example [fcap-002K]. The vector \(e_3\) commutes with \(H_0\) and anticommutes with \(I\). Hence \(C(x)=e_3xe_3\) interchanges the two components of \(\Phi (x)\). The identities \[e_0e_3=-I e_1e_2,\qquad e_1e_3=I e_0e_2,\qquad e_2e_3=-I e_0e_1\] give \(\Phi _1(ve_3)=-W(v)\). Now \[(svs^{-1})e_3=s(ve_3)C(s^{-1}).\] Applying \(\Phi _1\) and negating proves the action formula. For the diagonal pair \((q,q)\), the vector \(e_3\) is fixed because \(W(e_3)=-1\); on its orthogonal complement \(W\) restricts to \(\eta _3\) of Example [fcap-003J]. Thus the three-dimensional conjugation action is the diagonal case.

                                                TauCeti chooses a different algebra equivalence, denoted here by \(\widehat \Phi \). Its bilinear-generator formula gives \[\begin {aligned} e_0e_1&\longmapsto (-k,-k),& e_0e_2&\longmapsto (j,-j),\\ e_0e_3&\longmapsto (i,i),& e_1e_2&\longmapsto (-i,i),\\ e_1e_3&\longmapsto (j,j),& e_2e_3&\longmapsto (k,-k) \end {aligned}\] TauCeti.realCliffordFourZeroEvenEquivQuaternionProd_ι. In particular, \(\widehat \Phi (I)=(1,-1)\). Define quaternion automorphisms \[\begin {aligned} A(a+bi+cj+dk)&=a-ci+bj+dk,\\ B(a+bi+cj+dk)&=a+ci-bj+dk. \end {aligned}\] They are conjugation by \((1+k)/\sqrt {2}\) and \((1-k)/\sqrt {2}\), respectively, and satisfy \(B(q)=kA(q)k^{-1}\). The rows for \(e_0e_1,e_0e_2,e_1e_2\) identify the restrictions to \(H_0\) as \(A\circ \theta _0\) and \(B\circ \theta _0\). Together with the image of \(I\), the decomposition \(x=u+Iu'\) therefore proves \[\widehat \Phi (x)=\bigl (A(\Phi _1(x)),B(\Phi _2(x))\bigr ).\]

                                                TauCeti's vector coordinates are \[\eta _4(v)=-v_2+v_1i-v_0j+v_3k=A(W(v))k^{-1}\] TauCeti.realCliffordFourZeroQuaternionEquiv_apply. Since \(A,B\) commute with quaternion conjugation and \(A(\bar q)k^{-1}=k^{-1}\overline {B(q)}\), the formula for \(W\) gives \[\eta _4(svs^{-1})=A(q_+)\eta _4(v)\overline {B(q_-)}.\] This is precisely the action in the \(\widehat \Phi \) coordinates TauCeti.realSpinFourEquivQuaternionUnitaryProd_action. The displayed changes of coordinates derive its relation to the natural pair \(\Phi \) used in Example [fcap-002K].

                                                Gallier [gallier2014clifford, Section 1.4, pp. 29--30] gives the compact even-algebra decomposition into two quaternion factors with negative-square generators; Example [fcap-002K] uses the positive-square convention. Porteous [porteous1995clifford, Chapter 8, Propositions 8.26--8.27, p. 65] describes the four-dimensional rotations \(z\mapsto qz\bar r\) for unit quaternions \(q,r\). The calculation with \(ve_3\) identifies these left and inverse-right factors for \(\Phi \); the explicit \(A,B,W,\eta _4\) formulas then give the coordinate translation to \(\widehat \Phi \).

                                                Example. The split four-dimensional Spin action is left and inverse-right multiplication [fcap-003Y]

                                                  For \(Q_{2,2}(v)=v_0^2+v_1^2-v_2^2-v_3^2\), the even Clifford algebra is a pair of real matrix algebras. We construct its coordinates to specify which Spin factor acts on each side of a vector. Set \(A=e_0e_1\), \(B=e_0e_2\), \(C=e_1e_2\), and \(I=e_0e_1e_2e_3\). The subalgebra \(H_0=\langle 1,A,B,C\rangle _{\mathbb R}\) has \(A^2=-1\), \(B^2=C^2=1\), and \(AB=-C\). Define \[J=\begin {pmatrix}0&1\\-1&0\end {pmatrix},\quad S=\begin {pmatrix}0&1\\1&0\end {pmatrix},\quad D=\begin {pmatrix}-1&0\\0&1\end {pmatrix}.\] The assignments \(\rho (A)=-J\), \(\rho (B)=D\), \(\rho (C)=S\) satisfy these relations and give a basis of \(M_2(\mathbb R)\) together with the identity. They define an algebra equivalence \(\rho \). The volume element \(I\) is central in the even algebra and \(I^2=1\). The eight even basis monomials give \(\mathcal {C}\kern -2pt\ell ^+(Q_{2,2})=H_0\oplus I H_0\). Hence the map \[\Phi (u+Iw)=\bigl (\rho (u)-\rho (w),\ S(\rho (u)+\rho (w))S\bigr )\] is an algebra equivalence to \(M_2(\mathbb R)\times M_2(\mathbb R)\). For a pair \((P,R)\), its inverse is recovered from \[\rho (u)=\tfrac 12(P+SRS),\qquad \rho (w)=\tfrac 12(SRS-P).\]

                                                  The reversion fixes \(I\) and negates \(A,B,C\). On \(H_0\), this is matrix adjugation, since \(\rho (A), \rho (B),\rho (C)\) are traceless. Conjugation by \(S\) commutes with adjugation, so \[\Phi (\operatorname {rev}(x))= \bigl (\operatorname {adj}(\Phi _1(x)), \operatorname {adj}(\Phi _2(x))\bigr ).\] Consequently \(\operatorname {rev}(x)x=1\) if and only if both component determinants are one. The carrier lemma Lemma [fcap-002J] therefore restricts \(\Phi \), with the displayed inverse, to the actual group \[\operatorname {Spin}(Q_{2,2})\simeq SL_2(\mathbb R)\times SL_2(\mathbb R).\] Porteous's norm-one subgroup is denoted \(\operatorname {Spin}^+\); his split-four entry is a pair of \(Sp_2(\mathbb R)\) factors [porteous1995clifford, Chapter 17, Theorem 17.9 and Table 14, p. 159]. In degree two, \(M^{\mathsf T}JM=(\det M)J\), so these are precisely \(SL_2(\mathbb R)\). The norm-one restriction is essential to that comparison.

                                                  Our pair map has the following six bivector images: \[\begin {aligned} e_0e_1&\longmapsto (-J,J),& e_0e_2&\longmapsto (D,-D),\\ e_0e_3&\longmapsto (-S,S),& e_1e_2&\longmapsto (S,S),\\ e_1e_3&\longmapsto (D,D),& e_2e_3&\longmapsto (-J,-J). \end {aligned}\] In particular \(\Phi (I)=(-1,1)\). These are the specializations of TauCeti's bilinear-generator formula TauCeti.realCliffordTwoTwoEvenEquivMatrixProd_ι. Since the bivectors generate the even algebra, this identifies \(\Phi \) with its concrete even-algebra map and hence identifies the restricted group equivalence TauCeti.realSpinTwoTwoEquivSpecialLinearProd.

                                                  Now encode vectors by \[X(v)=\Phi _1(ve_3)S= \begin {pmatrix}-v_0-v_2&-v_1-v_3\\v_1-v_3&-v_0+v_2\end {pmatrix}.\] The inverse sends \(\begin {pmatrix}a&b\\c&d\end {pmatrix}\) to \((-(a+d)/2,(c-b)/2,(d-a)/2,-(b+c)/2)\). A determinant expansion gives \(\det X(v)=Q_{2,2}(v)\). Thus \(X\) identifies the whole vector space with the determinant quadratic space of real two-by-two matrices TauCeti.realCliffordTwoTwoVectorEquivMatrix_apply TauCeti.realCliffordTwoTwoVectorEquivMatrix_det. Writing \(\Phi (s)=(P,R)\) for a Spin element, the action is \[X(svs^{-1})=P X(v)R^{-1}.\]

                                                  For the proof, \(e_3^2=-1\), and conjugation \(\gamma (x)=-e_3xe_3\) fixes \(H_0\) and negates \(I\). Therefore \[\Phi (\gamma (x))= \bigl (S\Phi _2(x)S,\ S\Phi _1(x)S\bigr ).\] The identities \[e_0e_3=IC,\qquad e_1e_3=-IB,\qquad e_2e_3=-IA\] give the displayed formula for \(X\). Apply \(\Phi _1\) to \((svs^{-1})e_3=s(ve_3)\gamma (s^{-1})\), then multiply on the right by \(S\). Since \(S^2=1\), the result is \(P X(v)R^{-1}\). This proves TauCeti's exact coordinate action TauCeti.realSpinTwoTwoEquivSpecialLinearProd_action.

                                                  The diagram records the two ways to calculate the same action:

                                                  For example, take \(P=\operatorname {diag}(a,a^{-1})\), \(R=1\), where \(a\ne 0\). The two rows of \(X(v)\) are multiplied by \(a\) and \(a^{-1}\). Thus the null cone is exactly the matrices of rank at most one, and its rank-one part is preserved. For \(P=R\), the matrix \(X(e_0)=-1\) is fixed; this diagonal subgroup fixes \(e_0\).

                                                  As in the compact action of Example [fcap-003K], multiplication by a fixed vector makes an odd vector accessible to the even algebra, and conjugation by that vector interchanges its two factors. Here the factors are real matrices, with the explicit \(S\)-conjugations above. This is the even-algebra action transport of [porteous1995clifford, Chapter 16, Proposition 16.9, pp. 143--144] in the stated axes. The construction gives the group and its vector action; its orthogonal image retains the spinor-norm qualification of Theorem [fcap-0023].

                                                  Definition [ca-000J]Definition [ca-001J]Definition [spin-0012]Definition [spin-000O]

                                                  Example. The Lorentzian four-dimensional Spin group is \(SL_2(\mathbb C)\) [fcap-002L]

                                                    For \(Q_{1,3}=x_0^2-x_1^2-x_2^2-x_3^2\), put \(A_j=e_0e_j\) for \(1\le j\le 3\) and \(I=e_0e_1e_2e_3\). Then the \(A_j\) square to \(1\) and anticommute, while \[I^2=-1,\qquad A_1A_2A_3=-I.\] For the Pauli matrices \[\sigma _1=\begin {pmatrix}0&1\\1&0\end {pmatrix},\quad \sigma _2=\begin {pmatrix}0&-i\\i&0\end {pmatrix},\quad \sigma _3=\begin {pmatrix}1&0\\0&-1\end {pmatrix},\] the assignments \(\Psi (A_j)=\sigma _j\) define a real-algebra map from the even Clifford algebra to \(M_2(\mathbb C)\). Since \(\sigma _1\sigma _2\sigma _3=i1\), necessarily \(\Psi (I)=-i1\). The images of \(1,A_1,A_2,A_3,I,IA_1,IA_2,IA_3\) form a real basis, so \(\Psi \) is an algebra equivalence.

                                                    Write a matrix uniquely as \[M=z_0 1+z_1\sigma _1+z_2\sigma _2+z_3\sigma _3, \qquad z_j=a_j+i b_j,\] where \[\begin {aligned} z_0&=(m_{11}+m_{22})/2,&z_3&=(m_{11}-m_{22})/2,\\ z_1&=(m_{12}+m_{21})/2,&z_2&=(m_{21}-m_{12})/(2i). \end {aligned}\] Then an explicit inverse is \[\Psi ^{-1}(M) =a_0+\sum _{j=1}^3a_jA_j -I\left (b_0+\sum _{j=1}^3b_jA_j\right ).\] Reversal fixes \(I\) and negates every \(A_j\); under \(\Psi \) it is the complex-linear matrix adjugate. Hence \[\Psi (\operatorname {rev}(x))=\operatorname {adj}(\Psi (x)),\qquad \Psi (\operatorname {rev}(x)x)=\det (\Psi (x))1.\] For an arbitrary even \(x\), this norm is algebra-valued: the determinant may be complex, corresponding to the even center. It is not yet the real scalar-valued Lipschitz norm, and adjugation is not conjugate transpose.

                                                    Restriction therefore gives a homomorphism \(\operatorname {Spin}(Q_{1,3})\to SL_2(\mathbb C)\). Conversely, a determinant-one matrix has adjugate as a two-sided inverse. Its displayed Clifford preimage is an even unit with \(\operatorname {rev}(x)x=1\), so the dimension-four carrier lemma places it in Spin. The written inverse proves both compositions and multiplicativity: \[\operatorname {Spin}(Q_{1,3})\simeq SL_2(\mathbb C).\]

                                                    The source indices require translation. [lawson2016spin, I.3, Theorem 3.7, pp. 23--24] use \(v^2=-q(v)\) and give the even-algebra reduction \[\operatorname {Cl}^{0}_{3,1}\simeq \operatorname {Cl}_{2,1}.\] Their base entries and recurrence then give \[\operatorname {Cl}_{2,1}\simeq M_2(\mathbb C)\] [lawson2016spin, I.4, (4.0) and Theorem 4.1, p. 25].

                                                    Gallier uses the opposite indexing. The positive-square \(A_j\) exhibit \(\operatorname {Cl}_{3,0}\). [gallier2014clifford, Example 1.3, p. 33] records the matrix base entries, while [gallier2014clifford, Lemma 1.15, p. 34] supplies the recurrence. Together they give \[\operatorname {Cl}_{3,0} \simeq \operatorname {Cl}_{0,1}\otimes \operatorname {Cl}_{2,0} \simeq M_2(\mathbb C).\]

                                                    [porteous1995clifford, Chapter 17, Proposition 17.5, pp. 151--152] identifies his norm-one subgroup \(\operatorname {Spin}^{+}(1,3)\) with \(SL_2(\mathbb C)\). He computes reversal as adjugation. His broader mixed-sign carrier permits norm \(\pm 1\), and his displayed axes are not the Pauli axes fixed above.

                                                    Here the even center is \(\mathbb R[I]\simeq \mathbb C\), with no nonzero complementary central idempotents. This contrasts with the split compact center \(\mathbb R\oplus \mathbb R\), although both even algebras have real dimension eight. The full algebra \(\mathcal {C}\kern -2pt\ell _{1,3}\simeq M_2(\mathbb H)\) in Example [fcap-0026] is a different algebra. The vector-action image remains the spinor-norm kernel from Theorem [fcap-0023]; no topological component or concrete gamma-map claim is made.

                                                    Lemma. Opposite Lorentz signatures share an even-algebra action dictionary [fcap-003Z]

                                                      Keep the Pauli convention of Example [fcap-002L]: \(Q_{1,3}(v)=t^2-x_1^2-x_2^2-x_3^2\), \(A_j=e_0e_j\), and \(\Psi (A_j)=\sigma _j\). For \(Q_{3,1}(y)=y_0^2+y_1^2+y_2^2-y_3^2\), write \(f_0,\ldots ,f_3\) for the coordinate generators. The real linear bijection \[T(t,x_1,x_2,x_3)=(-x_2,x_1,-x_3,t)\] satisfies \(Q_{3,1}(Tv)=-Q_{1,3}(v)\). There is a real algebra equivalence \[E:\mathcal {C}\kern -2pt\ell ^+(Q_{1,3})\longrightarrow \mathcal {C}\kern -2pt\ell ^+(Q_{3,1}), \qquad E(vw)=-T(v)T(w).\] It preserves reversion and restricts to an equivalence of the actual Spin groups. Their vector actions satisfy \[T(svs^{-1})=E(s)T(v)E(s)^{-1}.\]

                                                      For the construction, complexify and send \(v\mapsto iT(v)\). Its square is \(Q_{1,3}(v)\), so the Clifford universal property gives an algebra map. On an even word of length \(2k\) its value is \((-1)^kT(v_1)\cdots T(v_{2k})\), which is real. This defines \(E\) by scalar extension as in Theorem [fcap-003V]. The reverse construction sends \(w\mapsto iT^{-1}(w)\); the two composites negate generators and therefore fix every even word. Reversing an even word commutes with \(E\). The dimension-four carrier lemma Lemma [fcap-002J] now identifies the reverse-norm-one even units on both sides, so \(E\) and its inverse restrict to the stated actual groups. Applying the complex map to \(svs^{-1}\) and cancelling \(i\) proves the action identity. This is the sign-transfer mechanism used for compact forms in Proposition [fcap-0039], with the additional coordinate change \(T\).

                                                      The algebraic construction is also the composite of sign scaling and the isometry \(T:(-Q_{1,3})\to Q_{3,1}\). TauCeti's general scaling formula at the unit \(-1\) TauCeti.CliffordAlgebra.evenEquivEvenSMul_ι, its reversion compatibility TauCeti.CliffordAlgebra.evenEquivEvenSMul_reverseEven, and the isometry formula CliffordAlgebra.evenEquivOfIsometry_ι provide these three component statements. The displayed \(T\) and its Spin-action dictionary are the explicit specialization proved here.

                                                      Let \(\Phi :\mathcal {C}\kern -2pt\ell ^+(Q_{3,1})\to M_2(\mathbb C)\) be TauCeti's concrete matrix equivalence. Its bilinear-generator formula TauCeti.realCliffordThreeOneEvenEquivComplexMatrix_ι gives \[\begin {aligned} \Phi (f_0f_3)&=-\sigma _2,&\Phi (f_1f_3)&=\sigma _1,& \Phi (f_2f_3)&=-\sigma _3,\\ \Phi (f_0f_1)&=i\sigma _3,&\Phi (f_0f_2)&=i\sigma _1,& \Phi (f_1f_2)&=i\sigma _2. \end {aligned}\] Since \(T(e_0)=f_3\), \(T(e_1)=f_1\), \(T(e_2)=-f_0\), and \(T(e_3)=-f_2\), these formulas give \(\Phi (E(A_j))=\sigma _j\). The \(A_j\) generate the even algebra, hence \(\Phi \circ E=\Psi \). Also \(E(e_0e_1e_2e_3)=f_0f_1f_2f_3\), whose matrix is \(-i1\). Thus the Pauli group equivalence agrees, through \(E\), with TauCeti.realSpinThreeOneEquivSpecialLinear. This dictionary concerns the even algebras and their Spin actions; the full real Clifford algebras retain their different signature types.

                                                      Theorem [ca-000C]Definition [ca-000J]Definition [spin-000O]

                                                      Example. The Lorentz Spin action is Hermitian matrix congruence [fcap-0040]

                                                        In the Pauli model Example [fcap-002L], an odd vector becomes an even element after multiplication by \(e_0\). Encode \(v=te_0+x_1e_1+x_2e_2+x_3e_3\) by \[X(v)=\Psi (ve_0)=t1-\sum _{j=1}^3x_j\sigma _j =\begin {pmatrix}t-x_3&-x_1+i x_2\\-x_1-i x_2&t+x_3\end {pmatrix}.\] A matrix is Hermitian when \(Z^*=Z\), where \(*\) denotes conjugate transpose. Every Hermitian two-by-two matrix has the form \(Z=\begin {pmatrix}a&z\\\overline z&d\end {pmatrix}\) with \(a,d\in \mathbb R\). The inverse coordinates are \[X^{-1}(Z)=\left (\frac {a+d}{2},-\operatorname {Re}z, \operatorname {Im}z,\frac {d-a}{2}\right ).\] Thus \(X\) is a real linear equivalence, and direct expansion gives \[\det X(v)=t^2-x_1^2-x_2^2-x_3^2=Q_{1,3}(v).\]

                                                        For \(s\in \operatorname {Spin}(Q_{1,3})\), put \(M=\Psi (s)\in SL_2(\mathbb C)\). Then the vector action is \[X(svs^{-1})=M X(v)M^*.\] To prove it, conjugation by \(e_0\) defines an automorphism \(\gamma (x)=e_0xe_0\) of the even algebra. It negates each \(A_j=e_0e_j\) and the volume element \(I=e_0e_1e_2e_3\). On the matrix side, \(M\mapsto \operatorname {adj}(M)^*\) has the same effect on \(\sigma _j\) and \(-i1\). It is a real algebra automorphism: both adjugation and conjugate transpose reverse products, and in size two adjugation is linear. Checking the even generators therefore gives \[\Psi (\gamma (x))=\operatorname {adj}(\Psi (x))^*.\] Now multiply the Clifford action by \(e_0\): \[(svs^{-1})e_0=s(ve_0)\gamma (s^{-1}).\] Since \(\det M=1\), we have \(\operatorname {adj}(M^{-1})=M\). Applying \(\Psi \) proves the congruence formula. It preserves Hermitian matrices, and its determinant is unchanged because \(\det M=\det M^*=1\).

                                                        The square makes the coordinate meaning of the action explicit:

                                                        For example, let \(M=\operatorname {diag}(e^{r/2},e^{-r/2})\). Its congruence multiplies \(t-x_3\) by \(e^r\), multiplies \(t+x_3\) by \(e^{-r}\), and fixes the off-diagonal entries. Hence \[\begin {aligned} t'&=\cosh (r)t-\sinh (r)x_3,& x_1'&=x_1,\\ x_3'&=-\sinh (r)t+\cosh (r)x_3,& x_2'&=x_2. \end {aligned}\] This is the boost with the sign selected by \(X=t1-x\cdot \sigma \). The null cone is exactly the Hermitian matrices of rank at most one.

                                                        For comparison with the formal opposite-signature model, use \(T\) and \(E\) from Lemma [fcap-003Z]. TauCeti's vector equivalence has coordinates \[H(y)=\begin {pmatrix}y_3+y_2&-y_1-i y_0\\ -y_1+i y_0&y_3-y_2\end {pmatrix},\qquad \det H(y)=-Q_{3,1}(y)\] TauCeti.coe_realCliffordThreeOneVectorEquivHermitian_apply TauCeti.realCliffordThreeOneVectorEquivHermitian_det. Substitution gives \(H(Tv)=X(v)\). In the even algebra this is the same identity as \(E(ve_0)=-T(v)f_3\), since \(H(y)=\Phi (-yf_3)\). The group coercion formula TauCeti.coe_realSpinThreeOneEquivSpecialLinear_apply identifies the matrix of \(E(s)\) with \(\Phi (E(s))=\Psi (s)=M\). Consequently the action dictionary in Lemma [fcap-003Z] translates TauCeti's exact Hermitian congruence theorem TauCeti.realSpinThreeOneEquivSpecialLinear_action into the displayed Pauli action. This checks both the signature sign and the matrix axes, not just the abstract group type.

                                                        Multiplication by a fixed nonisotropic vector is the even-algebra action mechanism of [porteous1995clifford, Chapter 16, Proposition 16.9, pp. 143--144]. His Lorentz group calculation uses adjugation and the norm-one carrier [porteous1995clifford, Chapter 17, Proposition 17.5, pp. 151--152]. The coordinates and conjugate-transpose action above are derived in our chosen axes. The orthogonal image retains the spinor-norm condition of Theorem [fcap-0023]; a topological component identification is separate.

                                                        Definition [ca-000J]Definition [spin-000O]

                                                        Proposition. The discriminant center of a four-dimensional Spin group [fcap-0043]

                                                          Let \(K\) be a field of characteristic different from two, and let \(q=\langle a,b,c,d\rangle \) with \(a,b,c,d\in K^\times \). Thus \(q(x)=ax_1^2+bx_2^2+cx_3^2+dx_4^2\). The center of its even Clifford algebra determines whether the quaternion description of its Spin group has two factors over \(K\) or one factor over a quadratic field. Put \[\begin {aligned} \delta &=abcd,\\ E&=K[t]/(t^2-\delta ),\\ D&=(-ab,-ac\mid K), \end {aligned}\] using the quaternion algebra notation. The class of \(\delta \) in \(K^\times /(K^\times )^2\) is the signed discriminant in dimension four; changing the diagonalizing basis changes the determinant by a square. Lam's center theorem identifies the corresponding quadratic algebra; the explicit quaternion and group identifications below follow by calculation [lam2005quadratic, V.2, thms. 2.2--2.5, pp. 109--111].

                                                          Extend quaternion conjugation \(\overline i=-i\), \(\overline j=-j\) \(E\)-linearly to \(D_E=D\otimes _K E\). Write \(SL_1(D_E)=\{x\in D_E:x\overline x=1\}\) for its norm-one group. Indeed, for \(x=x_0+x_1i+x_2j+x_3ij\), with \(x_r\in E\), \[x\overline x=\overline x x =x_0^2+abx_1^2+acx_2^2+a^2bcx_3^2\in E.\] This extends the reduced norm to the displayed quaternion algebra, and \(x^{-1}=\overline x\) when the norm is one. There are algebra and group isomorphisms \[\begin {aligned} \mathcal {C}\kern -2pt\ell ^+(q)&\simeq D_E,\\ Z(\mathcal {C}\kern -2pt\ell ^+(q))&\simeq E,\\ \operatorname {Spin}(q)&\simeq SL_1(D_E), \end {aligned}\] where the algebra isomorphism takes grade reversion to quaternion conjugation. If \(\delta \) is a square in \(K^\times \), this gives \[\operatorname {Spin}(q)\simeq SL_1(D)\times SL_1(D).\] If \(\delta \) is nonsquare, it gives \[\operatorname {Spin}(q)\simeq SL_1(D\otimes _K K(\sqrt \delta )).\] All groups here consist of points over the indicated fields.

                                                          For a concrete comparison, take \(q_d=\langle 1,-1,1,-d\rangle \). Then \(\delta =d\) and \(D=(1,-1\mid K)\). The matrices \[i\longmapsto \begin {pmatrix}1&0\\0&-1\end {pmatrix},\qquad j\longmapsto \begin {pmatrix}0&1\\-1&0\end {pmatrix}\] have squares \(1,-1\), anticommute, and, together with their product and the identity, form a basis of \(M_2(K)\). They therefore identify \(D\) with \(M_2(K)\). Conjugation becomes matrix adjugation and the norm becomes the determinant, giving \(\operatorname {Spin}(q_d)\simeq SL_2(E)\). In particular, over \(K=\mathbb Q\), the members \(q_1\) and \(q_2\) satisfy \[\begin {aligned} \operatorname {Spin}(q_1)(\mathbb Q) &\simeq SL_2(\mathbb Q)\times SL_2(\mathbb Q),\\ \operatorname {Spin}(q_2)(\mathbb Q) &\simeq SL_2(\mathbb Q(\sqrt 2)). \end {aligned}\] These identities apply the proposition to the two centers \(\mathbb Q\times \mathbb Q\) and \(\mathbb Q(\sqrt 2)\).

                                                          Proof. 

                                                            Choose orthogonal Clifford generators with \(e_1^2=a,e_2^2=b,e_3^2=c,e_4^2=d\). Distinct generators anticommute. Set \(I=e_1e_2\), \(J=e_1e_3\), and \(w=e_1e_2e_3e_4\). Then \[\begin {aligned} I^2&=-ab,&J^2&=-ac,\\ IJ&=-JI,&w^2&=abcd. \end {aligned}\] The element \(w\) commutes with every even word. Thus \(i\mapsto I\), \(j\mapsto J\), \(t\mapsto w\) define an algebra homomorphism \(D\otimes _K E\longrightarrow \mathcal {C}\kern -2pt\ell ^+(q)\). The eight elements \[1,I,J,IJ,w,Iw,Jw,IJw\] map to nonzero scalar multiples of the eight distinct even Clifford basis monomials. Explicitly, \[\begin {aligned} IJ&=-ae_2e_3,&Iw&=-abe_3e_4,\\ Jw&=ace_2e_4,&IJw&=abce_1e_4. \end {aligned}\] They form a basis, proving bijectivity. Writing an element of \(D_E\) in the basis \(1,i,j,ij\), commutation with \(i\) forces its \(j,ij\) coefficients to vanish, and commutation with \(j\) forces its \(i\) coefficient to vanish. Here \(2,ab,ac\) are units, even when \(E\) is a product. The center is therefore exactly \(E\). Reversion negates \(I,J,IJ\) and fixes \(w\), so it is \(\overline {(\,\cdot \,)}\) on \(D_E\).

                                                            It remains to identify the actual vector-generated Spin group with all even elements of reverse norm one. The real four-dimensional argument of Lemma [fcap-002J] works over the stated field as follows. Suppose \(x\in \mathcal {C}\kern -2pt\ell ^+(q)\) and \(\operatorname {rev}(x)x=1\). Finite-dimensionality makes this left inverse a two-sided inverse. For every vector \(v\), \(xvx^{-1}\) is odd and fixed by reversion. In the orthogonal Clifford basis, reversal is \(+1\) on degree one and \(-1\) on degree three. Since two is invertible, \(xvx^{-1}\) is a vector. Its square is \(q(v)\), and conjugation is injective, hence induces an orthogonal automorphism \(g\) of the four-dimensional vector space.

                                                            By the Clifford group exact sequence, lift \(g\) to a vector-generated Clifford unit \(y\). For the grading involution \(\alpha \), equality of the twisted actions of \(y\) and the even element \(x\) implies that \(z=y^{-1}x\) satisfies \(\alpha (z)v=vz\) for every vector \(v\). The graded-centrality theorem used in Lemma [fcap-002J] gives \(z=c1\) with \(c\in K^\times \). Every such scalar belongs to the generated Clifford group: for \(q(v)\ne 0\), the two nonisotropic vectors \((c/q(v))v\) and \(v\) have Clifford product \(c1\). Thus \(x=yz\) is in that group. It is even with reverse norm one, so the carrier criterion Remark [fcap-0028] places it in Spin. Conversely, every Spin element is even with reverse norm one by that same criterion. Under the algebra isomorphism this is exactly \(SL_1(D_E)\).

                                                            If \(\delta =r^2\) with \(r\in K^\times \), evaluation at \(r,-r\) identifies \(E\) with \(K\times K\). The corresponding central idempotents are \((1+w/r)/2\) and \((1-w/r)/2\). Hence \(D_E\simeq D\times D\), with componentwise conjugation and norm, giving the displayed product of norm-one groups. If \(\delta \) is nonsquare, \(t^2-\delta \) is irreducible, so \(E=K(\sqrt \delta )\) and the second description follows.

                                                            The split-center group equivalence has a formal counterpart in CliffordAlgebra.spinGroupEquivSplitCenterCorners, given a center isomorphism with \(K\times K\). The field-center existence theorem CliffordAlgebra.exists_spinGroupEquivQuaternionUnitaryOverCenter_of_finrank_eq_four gives a quaternion norm-one model over the actual even center. Both assume nondegeneracy and dimension four over a field with two invertible. The explicit parameters \(-ab,-ac\) and the matrices for \(q_d\) are supplied by the calculation above.

                                                            Lemma. The volume term does not obstruct Spin in dimension five [fcap-003H]

                                                              Let \(K\) be a field of characteristic different from two, and let \((V,Q)\) be a nondegenerate quadratic space of dimension five over \(K\). For \(x\in \mathcal {C}\kern -2pt\ell ^{+}(Q)\), \[x\text { is the Clifford value of a Spin element} \quad \Longleftrightarrow \quad \operatorname {rev}(x)x=1.\] The norm condition implies Lipschitz membership in this dimension CliffordAlgebra.evenUnitaryGroup_le_lipschitzGroup_of_finrank_eq_five. The point is to remove the possible degree-five term left by the dimension-four argument of Lemma [fcap-002J].

                                                              Choose an orthogonal basis \(e_1,\ldots ,e_5\), suppress the generator map, and put \(\omega =e_1\cdots e_5\). Nondegeneracy gives \[\omega ^2=\delta 1,\qquad \delta =\prod _{i=1}^5 Q(e_i)\ne 0.\] The element \(\omega \) is central and invertible. Suppose \(\operatorname {rev}(x)x=1\). Finite dimensionality makes the left inverse a two-sided inverse. For any \(v\in V\), the element \(y=xvx^{-1}\) is odd and satisfies \(\operatorname {rev}(y)=y\). In the orthogonal monomial basis, reversal has signs \(+1,-1,+1\) on degrees one, three and five. Hence \[y=w+c\omega \qquad (w\in V,\ c\in K).\]

                                                              Conjugation preserves the scalar square of a vector. Since \(\omega \) is central, \[Q(v)1=y^2=Q(w)1+2c\omega w+c^2\delta 1.\] Each \(\omega e_i\) is a nonzero scalar multiple of the product of the other four basis vectors. Thus \(\omega w\) has pure degree four in this basis, whereas the other terms in the equation are scalar. Independence of the Clifford basis gives \(2c\omega w=0\). As two and \(\omega \) are invertible, either \(c=0\) or \(w=0\). In the latter case \(y=c\omega \) is central, so conjugating back gives \(v=x^{-1}yx=y=c\omega \). The degree-one and degree-five subspaces have zero intersection; therefore \(v=0\) and \(c=0\). In both cases \(y\in V\).

                                                              Thus \(x\) normalizes the vector space. The Clifford-group characterization makes it Lipschitz; together with evenness and reverse norm one, this is the Spin criterion of Remark [fcap-0028]. The reverse implication is that same criterion. In fact the carrier equality holds in every dimension from one through five CliffordAlgebra.range_spinGroup_toUnits_eq_evenUnitaryGroup. The lower bound matters: in dimension zero the vector-generated Lipschitz group is trivial, whereas the even-unitary group contains both \(1\) and \(-1\). This carrier equality alone supplies no symplectic matrix model; the spinor pairing and matrix inverse for complex dimension five remain the separate argument of Proposition [fcap-0033].

                                                              Porteous gives the real dimension-five proof by separating the vector, trivector and volume terms [porteous1995clifford, Chapter 16, Proposition 16.15, p. 147]. His relation is \(v^2=-q(v)\), so here \(Q=-q\); his conjugation is \(\operatorname {rev}\circ \alpha \), equal to reversal on even elements. His indefinite Spin carrier permits norm \(\pm 1\); we select norm \(+1\). The basis calculation above extends the norm-one argument from real spaces to the stated fields: orthogonality, nonzero basis squares and invertibility of two replace any need for real unit-length normalization. Gallier records the compact boundary at five and the failure at six [gallier2014clifford, Section 1.4, closing Remark, p. 31]; the next example computes that failure.

                                                              Example. A norm-one even unit can leave the vector space in dimension six [fcap-003I]

                                                                Let \(K\) be a field of characteristic different from two, and let \((V,Q)\) be a finite-dimensional nondegenerate quadratic space containing six orthogonal vectors \(e_1,\ldots ,e_6\) with \(Q(e_i)\ne 0\). Put \[\omega =e_1\cdots e_6,\qquad \delta =\prod _{i=1}^6 Q(e_i).\] Now \(\omega \) is even, \(\operatorname {rev}(\omega )=-\omega \), and \(\omega ^2=-\delta 1\). It anticommutes with each of the six displayed vectors. If \(a,b\in K\) satisfy \(a^2+\delta b^2=1\), then \[x=a+b\omega ,\qquad x^{-1}=\operatorname {rev}(x)=a-b\omega \] is an even unit of reverse norm one. Its action on a displayed basis vector is \[xe_i x^{-1}=(a^2-\delta b^2)e_i+2ab\omega e_i.\]

                                                                For \(ab\ne 0\), the last term is a nonzero degree-five monomial, up to a scalar. Extend the six vectors to an orthogonal basis; independence of the Clifford monomials shows that the displayed conjugate is not a vector. Since \(x\) is even, ordinary and twisted conjugation agree. Thus \(x\) is not Lipschitz and cannot belong to Spin, despite satisfying the norm equation CliffordAlgebra.notMem_lipschitzGroup_of_mem_evenUnitaryGroup_of_coe_eq. Only the selected six vectors are used: in higher dimension \(\omega \) commutes with an additional orthogonal vector, which does not affect this counterexample.

                                                                For a concrete compact example, take \(K=\mathbb R\) and \(Q(v)=v_1^2+\cdots +v_6^2\). With \(a=b=1/\sqrt 2\), one obtains \[x=\frac {1+\omega }{\sqrt 2},\qquad \operatorname {rev}(x)x=1,\qquad xe_1x^{-1}=\omega e_1=-e_2e_3e_4e_5e_6.\] Porteous [porteous1995clifford, Chapter 16, p. 146] exhibits the unnormalized element \(1+\omega \) of norm two.

                                                                Gallier [gallier2014clifford, Section 1.4, closing Remark, p. 31] uses the normalized element above.

                                                                Their compact generators square to \(-1\). With that choice the same six-vector product still squares to \(-1\), but \(\omega e_1=+e_2e_3e_4e_5e_6\). Both signs give the same obstruction. The calculation here uses the positive-square convention of Example [fcap-002H].

                                                                Over any infinite \(K\) as above, the conic always supplies \(a,b\ne 0\). Indeed, choose \(t\ne 0\) with \(1+\delta t^2\ne 0\) and \(1-\delta t^2\ne 0\), and set \[a=\frac {1-\delta t^2}{1+\delta t^2},\qquad b=\frac {2t}{1+\delta t^2}.\] Only finitely many values of \(t\) are excluded, and substitution gives \(a^2+\delta b^2=1\). Consequently the Spin image is a proper subgroup of the even-unitary group for every nondegenerate form of dimension at least six over an infinite field of characteristic different from two CliffordAlgebra.range_spinGroup_toUnits_ne_evenUnitaryGroup_of_six_le_finrank. This field extension follows from the displayed calculation; the cited book passages concern real spaces. Over a finite field the conditional six-vector construction remains valid, but this infinitude argument makes no assertion that a suitable conic point exists.

                                                                Remark. From real recurrences to the residue table [fcap-0016]

                                                                  The mixed \((1,1)\) recurrence removes matched axes but leaves a one-sided algebra \(\mathcal {C}\kern -2pt\ell _{r,0}\) or \(\mathcal {C}\kern -2pt\ell _{0,r}\), which it cannot classify. Together with the signature switch in Theorem [fcap-001X] and initial entries in Example [fcap-0015], the two recurrences below complete the calculation.

                                                                  The two one-sided recurrences are \[\begin {aligned} \mathcal {C}\kern -2pt\ell _{p,q+2}&\simeq \mathcal {C}\kern -2pt\ell _{q,p}\otimes _{\mathbb R}\mathbb H,\\ \mathcal {C}\kern -2pt\ell _{p+8,q}&\simeq \mathcal {C}\kern -2pt\ell _{p,q}\otimes _{\mathbb R}M_{16}(\mathbb R). \end {aligned}\] The first line is the actual equivalence TauCeti.realCliffordQuaternionRecurrenceEquiv. For the second, the formal theorem supplies existence TauCeti.nonempty_realCliffordEightPeriodicityEquiv.

                                                                  They yield the residue-indexed mod-eight classification TauCeti.realClifford_classification. The classical table is [lawson2016spin, I.4, Theorem 4.3 and Tables I--II, pp. 27--29].

                                                                  Example. The real Clifford algebra of signature (1,3) [fcap-0026]
                                                                  realClifford_classification_of_residue_eq_two
                                                                  L∃∀N

                                                                    Use the convention of Convention [fcap-0011]: \(p\) counts positive squares, \(q\) counts negative squares, and a Clifford generator obeys \(v^2=Q(v)1\). Then the real algebra for one positive and three negative axes is \[\mathcal {C}\kern -2pt\ell _{1,3}\simeq M_2(\mathbb H).\] The Tau Ceti classification theorem states existence of an abstract real algebra equivalence. Here \(q-p=2\) is its residue modulo \(8\), and its matrix size is \(2^{(p+q-2)/2}=2\).

                                                                    [chevalley1954algebraic, II.2.9, pp. 65--66] uses the same positive/negative index convention. Split off one hyperbolic plane of signature \((1,1)\); the orthogonal remainder is a negative plane of signature \((0,2)\). Chevalley's dimension-two definite calculation on p. 66 identifies its Clifford algebra with \(\mathbb H\). The hyperbolic-plane theorem [chevalley1954algebraic, II.2.1, pp. 42--43] gives \(\mathcal {C}\kern -2pt\ell _{1,1}\simeq M_2(\mathbb R)\).

                                                                    [chevalley1954algebraic, II.2.5, pp. 45--46] gives an orthogonal-sum tensor-product formula for an even-dimensional nondegenerate first summand; the second quadratic form is twisted. Here normalized hyperbolic generators \(e^2=1\) and \(f^2=-1\) have volume \(J=ef\) with \(J^2=1\). For a vector \(v\) in the orthogonal remainder, \(Jv\) commutes with \(e,f\) and still squares to \(Q(v)\). Since \(v=J(Jv)\), these commuting factors generate the full algebra. Thus the special hyperbolic split leaves that remainder unchanged: \[\begin {aligned} \mathcal {C}\kern -2pt\ell _{1,3}&\simeq \mathcal {C}\kern -2pt\ell _{1,1}\otimes _{\mathbb R}\mathcal {C}\kern -2pt\ell _{0,2}\\ &\simeq M_2(\mathbb R)\otimes _{\mathbb R}\mathbb H \simeq M_2(\mathbb H). \end {aligned}\] Both sides have real dimension \(16=2^4=4\dim _{\mathbb R}\mathbb H\). By comparison, \(M_4(\mathbb C)\) has real dimension \(32\). This abstract classification alone does not identify any particular gamma-matrix map, its kernel, or its image; the concrete Dirac map is treated in Proposition [fcap-002U].

                                                                    Proposition. The real algebra generated by the Dirac gamma matrices [fcap-002U]

                                                                      On \(\mathbb R^4\), let \[q_\gamma (v)=v_0^2-v_1^2-v_2^2-v_3^2.\] Under the coordinate identification \(\operatorname {Fin}(4)=\operatorname {Fin}(1+3)\), the identity map is an isometry from \(q_\gamma \) to the signature form \(Q_{1,3}\) of Example [fcap-0026]. This is equality of the displayed forms, rather than only equality of their signatures. Thus the Clifford transport of Proposition [fcap-0029] and the classification in Example [fcap-0026] give \[\mathcal {C}\kern -2pt\ell (q_\gamma )\simeq \mathcal {C}\kern -2pt\ell _{1,3}\simeq M_2(\mathbb H)\] as real algebras. The selected formal ingredients are the coordinate formula TauCeti.realCliffordForm_apply and the residue-two classification TauCeti.realClifford_classification_of_residue_eq_two; the latter supplies existence of an abstract equivalence, not a theorem about a particular gamma-matrix map.

                                                                      Let \(\xi :\operatorname {Fin}(1)\sqcup \operatorname {Fin}(3) \simeq \operatorname {Fin}(4)\) be the standard index equivalence, and write \[\Gamma _i=\operatorname {endEquivMatrix} \bigl (\operatorname {gamma}(\xi ^{-1}i)\bigr ).\] These are the concrete matrices \(\gamma ^0,\gamma ^1,\gamma ^2,\gamma ^3\); their squares are \(+1,-1,-1,-1\), and distinct matrices anticommute. Put \[D_\gamma =\operatorname {Alg}_{\mathbb R} \langle \Gamma _0,\Gamma _1,\Gamma _2,\Gamma _3\rangle \subset M_4(\mathbb C).\] Physlib constructs the real unital algebra homomorphism \[\rho :\mathcal {C}\kern -2pt\ell (q_\gamma )\longrightarrow D_\gamma ,\qquad \rho \bigl (\iota _{q_\gamma }(v)\bigr )=\sum _{i=0}^3v_i\Gamma _i\] from the Clifford universal property and proves that it is surjective onto \(D_\gamma \); see the generator-map source and the surjectivity source. The codomain here is the generated real subalgebra, not all of \(M_4(\mathbb C)\).

                                                                      It remains to prove that this actual map has zero kernel. First, \(M_2(\mathbb H)\) is simple. Let \(J\) be a nonzero two-sided ideal, choose a matrix \(A\in J\) with nonzero entry \(a=A_{ij}\), and let \(E_{kl}(b)\) denote the matrix whose only nonzero entry is \(b\) in position \((k,l)\). Since every nonzero quaternion is invertible, for all \(k,l\) one has \[E_{ki}(a^{-1})\,A\,E_{jl}(1)=E_{kl}(1)\in J.\] The order of the factors matters over \(\mathbb H\). Taking both diagonal matrix units and adding them gives \(1\in J\), so \(J=M_2(\mathbb H)\). Transport through the preceding equivalence makes \(\mathcal {C}\kern -2pt\ell (q_\gamma )\) simple. Hence \(\ker \rho \) is zero or the entire source. The second option is impossible because \(\rho \) is unital and the identity matrix in \(D_\gamma \subset M_4(\mathbb C)\) is nonzero. Therefore \(\rho \) is injective; together with the formal surjectivity, this proves that this same map is a real algebra equivalence \[\mathcal {C}\kern -2pt\ell (q_\gamma )\simeq _{\rho }D_\gamma .\]

                                                                      Consequently \[\dim _{\mathbb R}D_\gamma =\dim _{\mathbb R}M_2(\mathbb H)=4\cdot 4=16.\] For the ambient algebra, \[\dim _{\mathbb R}M_4(\mathbb C)=16\cdot 2=32.\] Thus \(D_\gamma \) is a proper real subalgebra of the ambient complex matrix algebra. This conclusion uses the proved equivalence and does not assume the image dimension in order to deduce injectivity.

                                                                      Lawson--Michelsohn invoke simplicity of \(M_n(K)\) for \(K=\mathbb R,\mathbb C,\mathbb H\) in their real representation theorem [lawson2016spin, I.5, Theorem 5.6, pp. 31--32]. The matrix-unit calculation above supplies that step for the quaternionic algebra and then applies it to Physlib's concrete homomorphism. Their convention is \(v^2=-q(v)1\), so our \(\mathcal {C}\kern -2pt\ell _{1,3}\) is their \(\mathcal {C}\kern -2pt\ell _{3,1}\). Their algebra in that convention is the quaternionic matrix algebra used in the simplicity argument. The abstract classification is formalized in Tau Ceti, and Physlib formalizes the concrete map and its surjectivity. The simplicity and kernel argument completing the equivalence here is informal; no whole-card formal badge is asserted.

                                                                      Related

                                                                        Proposition. Isometries transport the Spin vector action [fcap-0029]
                                                                        spinGroupMap_spinVectorAction
                                                                        L∃∀N

                                                                          Let \(R\) be a commutative ring, let \(M_1,M_2\) be \(R\)-modules with quadratic forms \(Q_1,Q_2\), and let \(f:M_1\to M_2\) be an \(R\)-linear map satisfying \[Q_2(f(m))=Q_1(m).\] The Clifford universal property gives an algebra homomorphism \(\operatorname {Cl}(f):\mathcal {C}\kern -2pt\ell (Q_1)\to \mathcal {C}\kern -2pt\ell (Q_2)\) characterized on generators by \[\operatorname {Cl}(f)(\iota _{Q_1}(m))=\iota _{Q_2}(f(m))\] CliffordAlgebra.map_apply_ι. It preserves the Spin carrier and therefore restricts to a group homomorphism \(\operatorname {Spin}(f):\operatorname {Spin}(Q_1)\to \operatorname {Spin}(Q_2)\) QuadraticMap.Isometry.spinGroupMap. Concretely, the Clifford map preserves Lipschitz membership QuadraticMap.Isometry.map_mem_lipschitzGroup, evenness CliffordAlgebra.map_mem_even, and Clifford conjugation CliffordAlgebra.map_star; these are the carrier conditions separated in Remark [fcap-0028]. Neither construction requires \(f\) to have an inverse.

                                                                          Now suppose that \(2\) is invertible in \(R\). If \(a_i\) denotes the Spin vector action on \(M_i\), then \[a_2\bigl (\operatorname {Spin}(f)(s),f(m)\bigr ) =f\bigl (a_1(s,m)\bigr ).\] This identity says that the square with horizontal maps \(a_1,a_2\) and vertical maps \(\operatorname {Spin}(f)\times f,f\) commutes. It is the vector-action naturality equation, with no finite-dimensionality or nondegeneracy hypothesis. If \(f\) is instead an isometry equivalence, it induces a Spin equivalence QuadraticMap.IsometryEquiv.spinGroupEquiv, and the same square packages as naturality of the Spin-to-special-orthogonal homomorphism source theorem.

                                                                          A changed Gram matrix shows why the target form is part of the data. Over \(\mathbb Q\), set \(Q_1(x,y)=x^2+y^2\) and \(T(x,y)=(2x,y)\). Keeping the same form on the target does not give an isometry: at \(e_1\), \[Q_1(Te_1)=4\ne 1=Q_1(e_1).\] Correspondingly, the source generator \(\iota _{Q_1}(e_1)\) squares to \(1\), while its proposed image \(\iota _{Q_1}(2e_1)\) squares to \(4\); that assignment cannot define the claimed Clifford map.

                                                                          For the transported target form \(Q_2(x,y)=x^2/4+y^2\), one has \(Q_2(Tv)=Q_1(v)\). In column coordinates, \[G_1=I,\qquad G_2=(T^{-1})^\top G_1T^{-1} =\begin {pmatrix}1/4&0\\0&1\end {pmatrix},\qquad T^\top G_2T=G_1.\] Now \(\iota _{Q_2}(2e_1)^2=Q_2(2e_1)=1\), so the generator relation is preserved. Thus an arbitrary basis scaling is not a fixed-form isometry; it becomes an isometry only after the domain and target forms are related in the correct direction. This differs from the module equivalence \(T_Q:\mathcal {C}\kern -2pt\ell (Q)\simeq \bigwedge M\) in Lemma [fcap-0004], which is not an algebra map.

                                                                          Meinrenken derives \(\operatorname {Cl}(f)\) from the same universal property for a bilinear-form-preserving linear map [meinrenken2013clifford, Section 2.2.2, Proposition 2.2, p. 29]. Chevalley's tensor-quotient construction gives the corresponding extension from generator images whose squares are \(Q(x)\) [chevalley1954algebraic, II.1.1, pp. 38--39]. In Meinrenken's convention \(Q(v)=B(v,v)\), so his \(B\) is the half-polar form \(b_Q\) of Convention [fcap-0027]. These sources work over finite-dimensional vector spaces over fields; Meinrenken assumes characteristic different from two. The formal action square above has the commutative-ring hypotheses stated here. This card makes no claim about scalar extension, orthogonal sums, or composition of extension maps.

                                                                          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--Michelsohn impose \(v^2=-q_{r,s}(v)1\) [lawson2016spin, I.3, Proposition 3.1, p. 21]. This swaps the indices while leaving the mixed \((1,1)\) recurrence unchanged: \[\mathcal {C}\kern -2pt\ell _{p,q}=\mathcal {C}\kern -2pt\ell ^{\mathrm {Lawson}}_{q,p}.\]

                                                                            Example. The real Clifford algebra of signature (1,3) [fcap-0026]
                                                                            realClifford_classification_of_residue_eq_two
                                                                            L∃∀N

                                                                              Use the convention of Convention [fcap-0011]: \(p\) counts positive squares, \(q\) counts negative squares, and a Clifford generator obeys \(v^2=Q(v)1\). Then the real algebra for one positive and three negative axes is \[\mathcal {C}\kern -2pt\ell _{1,3}\simeq M_2(\mathbb H).\] The Tau Ceti classification theorem states existence of an abstract real algebra equivalence. Here \(q-p=2\) is its residue modulo \(8\), and its matrix size is \(2^{(p+q-2)/2}=2\).

                                                                              [chevalley1954algebraic, II.2.9, pp. 65--66] uses the same positive/negative index convention. Split off one hyperbolic plane of signature \((1,1)\); the orthogonal remainder is a negative plane of signature \((0,2)\). Chevalley's dimension-two definite calculation on p. 66 identifies its Clifford algebra with \(\mathbb H\). The hyperbolic-plane theorem [chevalley1954algebraic, II.2.1, pp. 42--43] gives \(\mathcal {C}\kern -2pt\ell _{1,1}\simeq M_2(\mathbb R)\).

                                                                              [chevalley1954algebraic, II.2.5, pp. 45--46] gives an orthogonal-sum tensor-product formula for an even-dimensional nondegenerate first summand; the second quadratic form is twisted. Here normalized hyperbolic generators \(e^2=1\) and \(f^2=-1\) have volume \(J=ef\) with \(J^2=1\). For a vector \(v\) in the orthogonal remainder, \(Jv\) commutes with \(e,f\) and still squares to \(Q(v)\). Since \(v=J(Jv)\), these commuting factors generate the full algebra. Thus the special hyperbolic split leaves that remainder unchanged: \[\begin {aligned} \mathcal {C}\kern -2pt\ell _{1,3}&\simeq \mathcal {C}\kern -2pt\ell _{1,1}\otimes _{\mathbb R}\mathcal {C}\kern -2pt\ell _{0,2}\\ &\simeq M_2(\mathbb R)\otimes _{\mathbb R}\mathbb H \simeq M_2(\mathbb H). \end {aligned}\] Both sides have real dimension \(16=2^4=4\dim _{\mathbb R}\mathbb H\). By comparison, \(M_4(\mathbb C)\) has real dimension \(32\). This abstract classification alone does not identify any particular gamma-matrix map, its kernel, or its image; the concrete Dirac map is treated in Proposition [fcap-002U].