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.

The zero-dimensional Clifford algebra is the base field

Statement

Let $k$ be a field of characteristic not $2$ , let $V = 0$ , and let $Q$ be the unique quadratic form on $V$ . Then the plus- $Q$ Clifford algebra is $C l (0, Q) ≅ k$ as a unital $k$ -algebra.

Facts & Assumptions

Given: A field $k$ with $char (k) \neq 2$ , the zero vector space $V = 0$ , and its unique quadratic form $Q = 0$ .

[F1]

The plus- $Q$ Clifford algebra is the quotient of $T_{k} (V)$ by the smallest two-sided ideal containing $j (v)^{2} - Q (v) 1$ for every $v \in V$ (Universal Clifford algebra of a quadratic space).

[F2]

$T_{k} (V) = ⨁_{m \geq 0} V^{\otimes m}$ with $V^{\otimes 0} = k$ and multiplication by concatenation (Tensor algebra of a vector space).

Proof

technique · evaluate the quotient in dimension zero

1.1givenF2algebra

Since $V = 0$ , every tensor power $V^{\otimes m}$ with $m \geq 1$ is zero. By [F2], $T_{k} (0) = k$ and the canonical inclusion $j : V \to T_{k} (V)$ has only the value $j (0) = 0$ .

2.1givenF1step 1.1algebra∎

The only defining relation in [F1] is $j (0)^{2} - Q (0) 1 = 0$ . The zero ideal already contains this relation, so it is the smallest such two-sided ideal; hence the quotient is $T_{k} (0) / 0 = k$ as a unital $k$ -algebra.

Depends on

Used by

Dependency tree · two levels

7 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.2 (standard reference, not scraped)
M. F. Atiyah, R. Bott, and A. Shapiro, Clifford Modules, Part I, §1, statements (1.1)–(1.4) (standard reference, not scraped)