LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)

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.

Real Clifford signature recurrences and eightfold periodicity

Statement

Let ${C l}_{p, q}$ be the real algebra for the form with $p$ positive and $q$ negative squares, using $v^{2} = Q (v) 1$ . As ungraded real algebras, for $p, q, n \geq 0$ ,

${C l}_{p + 1, q + 1} ≅ {C l}_{p, q} \otimes_{R} M_{2} (R), {C l}_{n + 2, 0} ≅ {C l}_{0, n} \otimes_{R} M_{2} (R), {C l}_{0, n + 2} ≅ {C l}_{n, 0} \otimes_{R} H .$

The pure-signature algebras through dimension eight are

$n$	${C l}_{n, 0}$	${C l}_{0, n}$
$0$	$R$	$R$
$1$	$R \oplus R$	$C$
$2$	$M_{2} (R)$	$H$
$3$	$M_{2} (C)$	$H \oplus H$
$4$	$M_{2} (H)$	$M_{2} (H)$
$5$	$M_{2} (H) \oplus M_{2} (H)$	$M_{4} (C)$
$6$	$M_{4} (H)$	$M_{8} (R)$
$7$	$M_{8} (C)$	$M_{8} (R) \oplus M_{8} (R)$
$8$	$M_{16} (R)$	$M_{16} (R)$

For every $n \geq 0$ , the pure algebras satisfy

${C l}_{n + 8, 0} ≅ M_{16} ({C l}_{n, 0}), {C l}_{0, n + 8} ≅ M_{16} ({C l}_{0, n}) .$

Facts & Assumptions

Given: The standard real quadratic forms with signature $(p, q)$ and the positive-square-first convention.

[F1]

Each canonical Clifford generator squares to its assigned $+ 1$ or $- 1$ value (Universal Clifford algebra of a quadratic space).

[F2]

A linear map satisfying the quadratic relation extends uniquely to a Clifford algebra homomorphism (Universal property of the Clifford algebra).

[F3]

A real Clifford algebra on $m$ generators has dimension $2^{m}$ by its ordered square-free basis (PBW basis and exterior associated graded for a Clifford algebra).

[F4]

The low-dimensional algebras are ${C l}_{1, 0} = R \oplus R$ , ${C l}_{0, 1} = C$ , ${C l}_{2, 0} = M_{2} (R)$ , ${C l}_{1, 1} = M_{2} (R)$ , and ${C l}_{0, 2} = H$ (Low-dimensional real Clifford algebra models).

[F5]

The real coefficient tensor identities include $C \otimes H ≅ M_{2} (C)$ , $H \otimes H ≅ M_{4} (R)$ , and $M_{m} (D) \otimes M_{n} (R) ≅ M_{m n} (D)$ (Tensor identities for the real division algebras).

[F6]

$R$ is a field (The reals form a totally ordered field).

[F7]

The Clifford algebra of the zero real vector space is $R$ (The zero-dimensional Clifford algebra is the base field).

[F8]

Ordinary tensor products of real vector spaces have canonical associative reparenthesizations and flips on elementary tensors (Symmetry and associativity isomorphisms for tensor products over a commutative ring).

[F9]

Tensoring over $R$ commutes with direct sums, including the isomorphism $(A \oplus B) \otimes C ≅ (A \otimes C) \oplus (B \otimes C)$ (Tensor products commute with arbitrary direct sums).

[F10]

Images of orthogonal Clifford vectors anticommute, by $\overset{ˉ}{x} \overset{ˉ}{y} + \overset{ˉ}{y} \overset{ˉ}{x} = 2 B (x, y) 1$ (Polarized relations in a Clifford algebra).

Proof

technique · generator maps, PBW dimensions, and iteration

1.1givenF1F2F10constructalgebra

Let $u, v$ generate ${C l}_{1, 1}$ with $u^{2} = 1$ , $v^{2} = - 1$ , and $u v = - v u$ by [F10], and put $τ = u v$ . Then $τ^{2} = - u^{2} v^{2} = 1$ , and $τ$ anticommutes with both $u$ and $v$ . Send each old positive or negative generator $x_{i}$ of ${C l}_{p, q}$ to $x_{i} \otimes τ$ , and send the new positive and negative generators to $1 \otimes u$ and $1 \otimes v$ . The images satisfy the standard quadratic relations: the old squares are unchanged because $τ^{2} = 1$ , the new squares are $+ 1, - 1$ , old pairs anticommute by [F10], and all cross anticommutators vanish because $τ$ anticommutes with $u, v$ . Thus every linear combination has its prescribed square, and [F2] gives a homomorphism ${C l}_{p + 1, q + 1} \to {C l}_{p, q} \otimes {C l}_{1, 1}$ .

1.2F1F2F4F10constructalgebra

Let $r, s$ be the positive generators of ${C l}_{2, 0}$ . By [F10], $r s = - s r$ ; put $σ = r s$ . Then $σ^{2} = r s r s = - r^{2} s^{2} = - 1$ , and $σ$ anticommutes with $r, s$ . Send each negative generator $y_{i}$ of ${C l}_{0, n}$ to $y_{i} \otimes σ$ and the two new positive generators to $1 \otimes r, 1 \otimes s$ . Each old image squares to $(- 1) (- 1) = + 1$ , the new images square to $+ 1$ , old pairs anticommute by [F10], and the cross anticommutators vanish. Hence every linear combination has its prescribed square, and [F2] gives the homomorphism used in the second recurrence.

1.3F1F2F4F10constructalgebra

Let $r, s$ be the two negative generators of ${C l}_{0, 2} ≅ H$ . By [F10], $r s = - s r$ ; put $σ = r s$ , so $σ^{2} = r s r s = - r^{2} s^{2} = - 1$ and $σ$ anticommutes with each. Send every positive generator $x_{i}$ of ${C l}_{n, 0}$ to $x_{i} \otimes σ$ and the two new negative generators to $1 \otimes r, 1 \otimes s$ . Old images square to $- 1$ , new images square to $- 1$ , old pairs anticommute by [F10], and cross anticommutators vanish. Thus every linear combination has its prescribed square, and [F2] gives a homomorphism ${C l}_{0, n + 2} \to {C l}_{n, 0} \otimes H$ .

1.4F6F7algebra

Since $R$ is a field by [F6], specialize [F7] to identify ${C l}_{0, 0}$ with $R$ . This supplies the $n = 0$ row of both pure-signature columns.

2.1F3F4step 1.1algebra

The map in step 1.1 is surjective: its image contains $1 \otimes u, 1 \otimes v$ , hence $1 \otimes τ$ and the second factor; multiplying $x_{i} \otimes τ$ by $1 \otimes τ$ recovers $x_{i} \otimes 1$ , which generates the first factor (when $p + q = 0$ , the first factor is just the scalar algebra generated by the unit). The source dimension is $2^{p + q + 2}$ by [F3], equal to the target dimension $2^{p + q} \cdot 4$ by [F3]–[F4]. Therefore the map is an isomorphism. Substituting ${C l}_{1, 1} ≅ M_{2} (R)$ from [F4] proves the first recurrence.

2.2F3F4step 1.3algebra

The images generate the two tensor factors because $σ$ is invertible (when $n = 0$ , the first factor is only the scalar algebra), and both sides have dimension $2^{n + 2}$ : the source has this dimension by [F3], while the target has dimension $2^{n} \cdot 4$ by [F3] and [F4]. Thus the homomorphism is an isomorphism.

2.3F3F4step 1.2algebra

Using the generator-map construction in step 1.2, the images generate both tensor factors because $σ$ is invertible (when $n = 0$ , the first factor is only the scalar algebra), so the induced homomorphism is surjective. Its source and target both have dimension $2^{n + 2}$ by [F3] and [F4]; hence it is an isomorphism, and [F4] identifies the second factor with $M_{2} (R)$ .

3.1F4F5F9step 2.3step 2.2algebra

Applying the second and third recurrences to [F4] gives ${C l}_{3, 0} ≅ {C l}_{0, 1} \otimes M_{2} (R) ≅ M_{2} (C)$ , ${C l}_{4, 0} ≅ {C l}_{0, 2} \otimes M_{2} (R) ≅ M_{2} (H)$ , ${C l}_{0, 3} ≅ {C l}_{1, 0} \otimes H ≅ H \oplus H$ , and ${C l}_{0, 4} ≅ {C l}_{2, 0} \otimes H ≅ M_{2} (H)$ . The first two use $C \otimes M_{2} (R) ≅ M_{2} (C)$ and $H \otimes M_{2} (R) ≅ M_{2} (H)$ from [F5]; the third uses $(R \oplus R) \otimes H ≅ H \oplus H$ by [F9], and the fourth uses $M_{2} (R) \otimes H ≅ M_{2} (H)$ by [F5].

4.1F4F5F9step 2.3step 2.2step 1.4step 3.1algebra

Applying the recurrences again and the tensor identities [F5] yields ${C l}_{5, 0} ≅ (H \oplus H) \otimes M_{2} (R) ≅ M_{2} (H) \oplus M_{2} (H)$ , ${C l}_{6, 0} ≅ M_{2} (H) \otimes M_{2} (R) ≅ M_{4} (H)$ , ${C l}_{7, 0} ≅ M_{4} (C) \otimes M_{2} (R) ≅ M_{8} (C)$ , ${C l}_{8, 0} ≅ M_{8} (R) \otimes M_{2} (R) ≅ M_{16} (R)$ , ${C l}_{0, 5} ≅ M_{2} (C) \otimes H ≅ M_{4} (C)$ , ${C l}_{0, 6} ≅ M_{2} (H) \otimes H ≅ M_{8} (R)$ , ${C l}_{0, 7} ≅ (M_{2} (H) \oplus M_{2} (H)) \otimes H ≅ M_{8} (R) \oplus M_{8} (R)$ , and ${C l}_{0, 8} ≅ M_{4} (H) \otimes H ≅ M_{16} (R)$ . The recurrences used are respectively ${C l}_{n + 2, 0} ≅ {C l}_{0, n} \otimes M_{2} (R)$ and ${C l}_{0, n + 2} ≅ {C l}_{n, 0} \otimes H$ ; [F9] distributes tensor products across the split factors, [F4] supplies the initial rows through $n = 2$ , and step 1.4 supplies $n = 0$ . Thus these entries give every row of the displayed pure-signature table.

5.1F5F8step 2.3step 2.2algebra∎

Iterating the second recurrence in step 2.3 and the third recurrence in step 2.2 gives ${C l}_{n + 8, 0} ≅ {C l}_{0, n + 6} \otimes M_{2} (R) ≅ {C l}_{n + 4, 0} \otimes H \otimes M_{2} (R) ≅ {C l}_{0, n + 2} \otimes M_{2} (R) \otimes H \otimes M_{2} (R) ≅ {C l}_{n, 0} \otimes H \otimes M_{2} (R) \otimes H \otimes M_{2} (R)$ and ${C l}_{0, n + 8} ≅ {C l}_{n + 6, 0} \otimes H ≅ {C l}_{0, n + 4} \otimes M_{2} (R) \otimes H ≅ {C l}_{n + 2, 0} \otimes H \otimes M_{2} (R) \otimes H ≅ {C l}_{0, n} \otimes M_{2} (R) \otimes H \otimes M_{2} (R) \otimes H$ . The reassociations and flips in [F8] preserve multiplication on elementary tensors, so they are algebra isomorphisms; they reorder the four extra factors as $H \otimes H \otimes M_{2} (R) \otimes M_{2} (R)$ . By [F5], $H \otimes H ≅ M_{4} (R)$ and then $M_{4} (R) \otimes M_{2} (R) \otimes M_{2} (R) ≅ M_{16} (R)$ . This proves both eightfold identities.

Depends on

Used by

Dependency tree · two levels

37 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.6, Lemma 1.15 and Theorem 1.17 (standard reference, not scraped)
M. F. Atiyah, R. Bott, and A. Shapiro, Clifford Modules, Part I, §4, Table 1 (standard reference, not scraped)
Konstantin Wernli, Lecture Notes on Spin Geometry, §1.4.1, Theorem 1.4.4 and Table 1.1 (standard reference, not scraped)