LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge 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.

Polarized relations in a Clifford algebra

Statement

Let $k, V, B, Q$ be as in Universal Clifford algebra of a quadratic space, and let $\overset{ˉ}{v} = i_{Q} (v)$ . Then

$\overset{ˉ}{v} \overset{ˉ}{w} + \overset{ˉ}{w} \overset{ˉ}{v} = 2 B (v, w) 1$

for all $v, w \in V$ .

Facts & Assumptions

Given: A field $k$ of characteristic not $2$ , a finite-dimensional $k$ -vector space $V$ , a symmetric bilinear form $B$ , $Q (v) = B (v, v)$ , and $v, w \in V$ .

[F1]

The quotient map sends each $v \in V$ to an element satisfying $i_{Q} (v)^{2} = Q (v) 1$ (Universal Clifford algebra of a quadratic space).

Proof

technique · direct

1.1givenF1algebra

Applying [F1] to $v + w$ , $v$ , and $w$ , then subtracting the last two defining equalities from the first, gives $\overset{ˉ}{v} \overset{ˉ}{w} + \overset{ˉ}{w} \overset{ˉ}{v} = (Q (v + w) - Q (v) - Q (w)) 1$ .

2.1givenstep 1.1algebra∎

Bilinearity and symmetry give $Q (v + w) - Q (v) - Q (w) = B (v, w) + B (w, v) = 2 B (v, w)$ , proving the relation.

Depends on

Universal Clifford algebra of a quadratic space

Used by

Dependency tree · two levels

3 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 (standard reference, not scraped)