ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Pin lift squares and the Spin(2) double-angle map

Example

In ${C l}_{1, 0}$ the lift of the nonidentity reflection in $O (1)$ squares to $+ 1$ , while in ${C l}_{0, 1}$ it squares to $- 1$ . In positive two-dimensional signature, $Spin (2)$ is the unit circle in the even Clifford algebra and its map to $S O (2)$ doubles the angle.

An explicit complex Clifford spinor module is $S = C^{2}$ , of complex dimension $2$ , with positive-square generators acting by $c (e_{1}) = A : = (\begin{array}{cc} 0 & 1 \\ 1 & 0 \end{array}), c (e_{2}) = B : = (\begin{array}{cc} 0 & i \\ - i & 0 \end{array}) .$ It is irreducible as a complex Clifford module. For $E = e_{1} e_{2}$ , the positive-square chirality $ω = i E$ acts as $diag (1, - 1)$ . Its half-spin spaces $S^{+} = C (1, 0)$ and $S^{-} = C (0, 1)$ are inequivalent irreducible complex Spin $(2)$ modules, each of complex dimension $1$ . Their characters on $a + b E$ , where $a^{2} + b^{2} = 1$ , are $χ_{+} (a + b E) = a - i b, χ_{-} (a + b E) = a + i b .$ Thus the lift $g_{θ} = \cos (θ / 2) - E \sin (θ / 2)$ of rotation by $θ$ acts on $S^{\pm}$ by $\cos (θ / 2) \pm i \sin (θ / 2)$ , respectively. The $2 π$ lift acts by $- 1$ on both lines, whereas the $4 π$ lift acts by $1$ .

Facts & Assumptions

Given: The conventions Pin $^{+} (n) \subset {C l}_{n, 0}$ , Pin $^{-} (n) \subset {C l}_{0, n}$ and the full-even Spin definition.

[F1]

Pin is generated by vectors with $∣ Q (u) ∣ = 1$ , full Spin is its even subgroup, and the Clifford norm on vector products is $\prod (- Q (u_{j}))$ (Real Clifford group, Pin, and the two Spin subgroups, Normalized Pin products and Clifford norm).

[F2]

The twisted action of an anisotropic vector is its hyperplane reflection (Twisted Clifford action, reflections, and scalar kernel).

[F3]

Ordered square-free monomials form a basis of the Clifford algebra (PBW basis and exterior associated graded for a Clifford algebra).

[F4]

Over $C$ , a complex-linear map from a quadratic space to a unital associative complex algebra satisfying $c (v)^{2} = Q (v) I$ extends uniquely to a unital Clifford algebra homomorphism (Universal property of the Clifford algebra).

Verification

technique · direct

1.1givenF1algebra

In ${C l}_{1, 0}$ , $e^{2} = 1$ and the unit-vector-generated Pin group is ${1, - 1, e, - e}$ ; its reflection lift $e$ has square $+ 1$ . In ${C l}_{0, 1}$ , $f^{2} = - 1$ and Pin is ${1, - 1, f, - f} ≅ C_{4}$ ; its reflection lift has square $- 1$ . In both cases the even subgroup is ${1, - 1}$ .

1.2F1F3algebra

In ${C l}_{2, 0}$ put $E = e_{1} e_{2}$ . Then $E^{2} = - 1$ , and by [F3] the even algebra is exactly $R \oplus R E ≅ C$ . For $a^{2} + b^{2} = 1$ , $a + b E$ is a product of two unit vectors: $e_{1} (a e_{1} + b e_{2}) = a + b E$ . Thus every unit $a + b E$ belongs to Spin, and conversely every even unit product has norm one, so Spin $(2) = {a + b E : a^{2} + b^{2} = 1}$ .

1.3F3F4constructalgebra

The matrices in the Example satisfy $A^{2} = B^{2} = I$ and $A B = - B A = diag (- i, i)$ . Hence $(z_{1} A + z_{2} B)^{2} = (z_{1}^{2} + z_{2}^{2}) I$ for all $z_{1}, z_{2} \in C$ . Applying [F4] to the complexification of the positive plane defines a unital complex Clifford action on $S$ . Its image contains $P_{+} = (I + i A B) / 2 = diag (1, 0)$ and $P_{-} = (I - i A B) / 2 = diag (0, 1)$ , as well as $P_{+} A$ and $P_{-} A$ , which are the other two matrix units. The image is therefore all of $M_{2} (C)$ ; [F3] gives complex dimension $4$ for the source, so this map is an algebra isomorphism. Every nonzero invariant subspace contains both coordinate vectors by applying these matrix units to a nonzero vector, proving irreducibility of the complex dimension- $2$ Clifford module.

2.1F2step 1.2algebra

For $θ \in R$ , let $g_{θ} = \cos (θ / 2) - E \sin (θ / 2)$ . Since $g_{θ}^{- 1} = \cos (θ / 2) + E \sin (θ / 2)$ , direct multiplication using $E e_{1} = - e_{2}$ and $e_{1} E = e_{2}$ gives $ρ_{g_{θ}} (e_{1}) = \cos θ e_{1} + \sin θ e_{2}$ and $ρ_{g_{θ}} (e_{2}) = - \sin θ e_{1} + \cos θ e_{2}$ . Therefore the angle doubles; $g_{2 π} = - 1$ and $g_{4 π} = 1$ .

3.1step 1.2step 2.1step 1.3algebra∎

Since $c (E) = A B = diag (- i, i)$ , the operator $c (ω) = i A B$ has the displayed eigenspaces $S^{\pm}$ , each a complex line. Restricting the Clifford action to the circle in step 1.2 gives on these lines the scalars $a - i b$ and $a + i b$ , of absolute value one. The scalar functions are continuous in $(a, b)$ , and multiplicativity of the Clifford action makes them group characters; the one-dimensional modules are irreducible. They are inequivalent because the Spin element $E$ acts by $- i$ on $S^{+}$ and $i$ on $S^{-}$ . Substituting $a = \cos (θ / 2)$ and $b = - \sin (θ / 2)$ yields the two asserted half-angle actions. In particular the kernel element $g_{2 π} = - 1$ acts by $- 1$ and $g_{4 π} = 1$ acts by $1$ , consistently with the vector double-angle map in step 2.1.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

16 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Jean Gallier, Clifford Algebras, Clifford Groups, and a Generalization of the Quaternions: The Pin and Spin Groups, §§1.4–1.5 (standard reference, not scraped)
Konstantin Wernli, Lecture Notes on Spin Geometry, §1.5.3, pp. 29–31 (standard reference, not scraped)