euclideanQuadraticForm8
plain-language theorem explainer
Defines the standard Euclidean quadratic form Q(x)=∑x_i² on ℝ⁸. Anyone building Cl₈ or the Bott-periodicity bridge to the eight-tick register cites it. The body is a direct sum of squared coordinate projections, not a derived theorem.
Claim. The Euclidean quadratic form on $\mathbb{R}^8$ is $Q:\mathbb{R}^8\to\mathbb{R}$ given by $Q(x)=\sum_{i\in\{0,\ldots,7\}} x_i^2$, realized as a Mathlib `QuadraticForm` on `Fin 8 → ℝ`.
background
The module links Recognition Science's eight-tick structure to Clifford algebras and Bott periodicity. Clifford algebra Cl(V,Q) is the quotient of the tensor algebra T(V) by v⊗v = Q(v)·1. For the Euclidean form one recovers the classical sequence Cl₁≅ℂ, Cl₂≅ℍ, …, Cl₈≅M₁₆(ℝ).
Bott periodicity asserts Cl_{n+8} ≅ Cl_n ⊗ Cl_8. The module treats that 8-fold period as the algebraic reason the recognition register is an eight-tick cycle (forcing-chain T7), alongside real spinor period 8 and KO-theory period 8.
This declaration supplies the quadratic form on ℝ⁸ that Mathlib's Clifford construction needs. Sibling forms (e.g. the 3D Euclidean form for Cl₃ / Spin(3)≅SU(2)) play the same role in lower dimension.
proof idea
Definition only: Q is the Finset sum over i : Fin 8 of the square form composed with the i-th coordinate projection. No lemmas are applied; noncomputable is inherited from the Mathlib quadratic-form API.
why it matters
Feeds the type alias Cl₈ := CliffordAlgebra of this form, the carrier for the module's Bott-periodicity and 8-tick grading results (mode-to-grading, cliffordPeriod = 8). Without a concrete Euclidean Q on ℝ⁸, the isomorphism story Cl_{n+8} ≅ Cl_n ⊗ Cl_8 and the claimed match to the eight-tick DFT grading cannot even be stated in Lean.
In the Recognition framework this is the algebraic substrate for T7 (eight-tick octave, period 2³) and the spinor side of D=3 (via the parallel Cl₃ bridge). It does not itself prove periodicity; it is the form that makes Cl₈ the right object for those theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.