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.

The split even Clifford algebra in signature (1,1)

Example

For signature $(1, 1)$ , let $E = e_{+} e_{-}$ with $e_{+}^{2} = 1$ , $e_{-}^{2} = - 1$ . Then $E^{2} = 1$ and ${C l}_{1, 1}^{0} ≅ R \oplus R$ . The two one-dimensional modules $M_{\pm}$ defined by $E \cdot t = \pm t$ are inequivalent irreducible real Clifford spinor representations of Spin, obtained by restricting the two unital even-Clifford modules.

Facts & Assumptions

Given: The $(1, 1)$ Clifford relations and the real even-algebra module classification of Real Spin modules from the even Clifford algebra.

[F1]

Full-even Spin consists of even normalized products, and its linear span is the even Clifford algebra (Normalized Pin products and Clifford norm, Real Spin modules from the even Clifford algebra).

[F2]

A simple module for a split factor $R$ is one-dimensional over $R$ (Real Spin modules from the even Clifford algebra).

[F3]

The ordered even Clifford monomials form a basis of ${C l}^{0}$ (PBW basis and exterior associated graded for a Clifford algebra).

Verification

technique · direct

1.1givenF3algebra

The polarized Clifford relation gives $e_{+} e_{-} = - e_{-} e_{+}$ and hence $E^{2} = - e_{+}^{2} e_{-}^{2} = 1$ . By [F3], $1, E$ form a basis of ${C l}_{1, 1}^{0}$ . The map $a + b E \mapsto (a + b, a - b)$ preserves products and is bijective, so it identifies this algebra with $R \oplus R$ .

2.1F1F2step 1.1algebra∎

The idempotents $p_{\pm} = (1 \pm E) / 2$ are the two factor identities. Let each factor act on $R$ by its scalar coordinate and the other factor by zero. Each module is one-dimensional and hence irreducible; they are inequivalent because $E$ acts by opposite scalars. By [F1], invariance under full-even Spin is equivalent to invariance under its linear span ${C l}^{0}$ , so these are precisely the two split-row Clifford spinor types in this example.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

17 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

M. F. Atiyah, R. Bott, and A. Shapiro, Clifford Modules, Part I (standard reference, not scraped)
Konstantin Wernli, Lecture Notes on Spin Geometry, §1.5.4, pp. 32–33 (standard reference, not scraped)