Eight-step periodicity for real Clifford algebras

The matrix and quaternion recurrences combine to identify adding eight positive generators with tensoring by sixteen-by-sixteen real matrices.

Main result

• nonempty_realCliffordEightPeriodicityEquiv gives the eight-step equivalence for every real signature.

References

• H. B. Lawson and M.-L. Michelsohn, Spin Geometry, Chapter I.
• TauCeti SpinRepresentations roadmap, Layer 7

theorem TauCeti.nonempty_realCliffordEightPeriodicityEquiv (p q : ℕ) : Nonempty (CliffordAlgebra (realCliffordForm (p + 8) q) ≃ₐ[ℝ] TensorProduct ℝ (CliffordAlgebra (realCliffordForm p q)) (Matrix (Fin 16) (Fin 16) ℝ))

Eight-step periodicity for standard real Clifford algebras.