Cl8
plain-language theorem explainer
Names the real Clifford algebra Cl₈ built from the standard Euclidean quadratic form on ℝ⁸. Anyone citing Bott periodicity or the 8-tick grading bridge in Recognition Science uses this type. The body is a one-line abbrev of Mathlib's CliffordAlgebra applied to that form.
Claim. Write $Cl_8$ for the Clifford algebra of $\mathbb{R}^8$ with the standard Euclidean quadratic form $Q(x)=\sum_{i=0}^{7} x_i^2$.
background
The module CliffordBridge links Recognition Science's eight-tick structure to Clifford algebras through Bott periodicity: $Cl_{n+8}\cong Cl_n\otimes Cl_8$. That period-8 fact is presented as the algebraic reason the RS evolution cycle has length eight (T7 in the forcing chain).
The quadratic form used here, euclideanQuadraticForm8, is the sum of squared coordinate projections on Fin 8 → ℝ, i.e. the standard positive-definite form on ℝ⁸. Mathlib's CliffordAlgebra then quotients the tensor algebra by the usual relation $v\otimes v=Q(v)\cdot 1$.
Sibling notation in the same file introduces the three-dimensional analogue and the period constant eight; the module also aims at a Spin(3)≅SU(2) bridge for D=3 spinors.
proof idea
Definitional abbrev only: expand to CliffordAlgebra euclideanQuadraticForm8. No tactics, no lemmas. All algebraic content is deferred to Mathlib's Clifford algebra API and to the separately defined Euclidean form on eight coordinates.
why it matters
Gives the concrete algebra whose grading and Bott period underwrite the claim that the RS eight-tick octave is not an ad hoc discrete choice. Module-level targets are Bott periodicity $Cl_{n+8}\cong Cl_n\otimes Cl_8$, an identification of the 8-tick DFT grading with the grading of Cl₈, and the Spin(3) bridge for three spatial dimensions (T7–T8 landmarks).
No downstream Lean users are recorded yet; the declaration is infrastructure for those periodicity and grading theorems in the same module. Classical references cited in the module doc are Atiyah–Bott–Shapiro and Lawson–Michelsohn.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.