ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generated

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.

Low-signature real Clifford algebras as C, H, and matrix algebras

Example

With $v^{2} = Q (v) 1$ and signatures ordered $(+^{p}, -^{q})$ , the five signatures $(1, 0)$ , $(0, 1)$ , $(2, 0)$ , $(1, 1)$ , and $(0, 2)$ give respectively

R \oplus R, C, M_{2} (R), M_{2} (R), H .

This checks the sign and indexing conventions at the smallest dimensions.

Facts & Assumptions

Given: The five standard real forms listed above.

[F1]

The real classification table depends on $p - q m o d 8$ and the total dimension (Real and complex Clifford algebra classification with explicit signature).

[F2]

The low-dimensional algebra identifications 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).

[F3]

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

[F4]

Ordered square-free monomials form a Clifford basis, of dimension $2^{n}$ in dimension $n$ (PBW basis and exterior associated graded for a Clifford algebra).

[F5]

The coefficient algebras have real bases $1, i$ for $C$ and $1, i, j, k$ for $H$ , with $i^{2} = j^{2} = - 1$ and $i j = - j i = k$ in $H$ (Real, complex, and quaternion coefficient algebras and matrix notation).

Verification

1.1givenF1algebra

For $(p, q) = (1, 0)$ , $n = 1$ and $r = 1$ , so [F1] gives $R \oplus R$ . For $(0, 1)$ , $r = 7$ , giving $C$ . For $(2, 0)$ , $n = 2, r = 2$ , giving $M_{2} (R)$ ; for $(1, 1)$ , $r = 0$ , also $M_{2} (R)$ ; and for $(0, 2)$ , $r = 6$ , giving $H$ .

1.2givenconstructalgebra

Set $A = (\begin{array}{cc} 1 & 0 \\ 0 & - 1 \end{array})$ , $B_{+} = (\begin{array}{cc} 0 & 1 \\ 1 & 0 \end{array})$ , and $B_{-} = (\begin{array}{cc} 0 & 1 \\ - 1 & 0 \end{array})$ . Direct multiplication gives $A^{2} = B_{+}^{2} = I$ , $B_{-}^{2} = - I$ , $A B_{+} = - B_{+} A = B_{-}$ , and $A B_{-} = - B_{-} A = B_{+}$ . Thus $(x A + y B_{+})^{2} = (x^{2} + y^{2}) I$ and $(x A + y B_{-})^{2} = (x^{2} - y^{2}) I$ . The four matrices $I, A, B_{+}, B_{-}$ are linearly independent: a zero linear combination has diagonal entries $a + b = a - b = 0$ and off-diagonal entries $c + d = c - d = 0$ , forcing all coefficients to vanish.

2.1F2F3F4F5step 1.1step 1.2constructalgebra∎

For the five signatures in order, send the standard generators to $(1, - 1)$ , to $i \in C$ , to $A, B_{+}$ , to $A, B_{-}$ , and to $i, j \in H$ . The one-generator images have the required squares; step 1.2 checks every linear combination in both matrix cases; and [F5] gives $(x i + y j)^{2} = - (x^{2} + y^{2})$ in the quaternion case. Hence [F3] extends each linear map to a unital algebra homomorphism. The images of the ordered monomials are respectively the real bases $(1, 1), (1, - 1)$ ; $1, i$ ; $I, A, B_{+}, B_{-}$ ; $I, A, B_{-}, B_{+}$ ; and $1, i, j, k$ . They span each target and are linearly independent by step 1.2 and [F5], and the source dimensions are $2, 2, 4, 4, 4$ by [F4]. Each homomorphism is therefore an isomorphism, explicitly realizing [F2] and agreeing with step 1.1.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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