Cl3
plain-language theorem explainer
Type alias for the real Clifford algebra Cl(3) built from the standard Euclidean quadratic form on ℝ³. Researchers linking Recognition Science's forced D=3 spatial structure to spinor geometry and the Spin(3)≅SU(2) bridge cite this. It is a one-line abbreviation of Mathlib's CliffordAlgebra applied to the sum-of-squares form on Fin 3 → ℝ.
Claim. Let $Q_3$ be the standard Euclidean quadratic form on $\mathbb{R}^3$, given by $Q_3(v)=v_0^2+v_1^2+v_2^2$. Write $\mathrm{Cl}_3$ for the Clifford algebra $\mathrm{Cl}(\mathbb{R}^3,Q_3)$.
background
The module CliffordBridge connects Recognition Science's eight-tick register to classical Clifford algebra theory through Bott periodicity. Its stated aims include the period-8 isomorphism $\mathrm{Cl}_{n+8}\cong\mathrm{Cl}_n\otimes\mathrm{Cl}_8$, an identification of the 8-tick DFT grading with that of $\mathrm{Cl}_8$, and the spin-group bridge $\mathrm{Spin}(3)\cong\mathrm{SU}(2)$ that supplies spinors once space is three-dimensional.
The quadratic form used here is the Euclidean sum of squares on $\mathbb{R}^3$: $Q(v)=\sum_{i=0}^{2}v_i^2$, defined as the sum of three projected square maps on $\mathrm{Fin},3\to\mathbb{R}$. Mathlib's CliffordAlgebra constructor then builds the unital associative algebra generated by that quadratic space subject to $v^2=Q(v)\cdot 1$.
Specializing to $n=3$ is deliberate: the forcing chain already yields $D=3$ spatial dimensions (T8), so the Euclidean Clifford algebra on three generators is the natural home for the spatial spinor structure.
proof idea
One-line type abbreviation: $\mathrm{Cl}_3$ is defined to be Mathlib's CliffordAlgebra applied to the already-constructed Euclidean quadratic form on $\mathbb{R}^3$. No lemmas are invoked and there are no proof obligations.
why it matters
This alias is the $n=3$ endpoint of the Clifford bridge. The module's main physical claim is that Bott period 8 is why Recognition Science needs exactly eight ticks, while $\mathrm{Spin}(3)\cong\mathrm{SU}(2)$ supplies the spinor structure once T8 has forced three spatial dimensions. Naming $\mathrm{Cl}_3$ keeps that spin-group side of the story aligned with the parallel $\mathrm{Cl}_8$ alias used for the eight-tick grading. Downstream work on mode-to-grading maps and Bott periodicity statements can then refer to a single short name rather than the full quadratic-form constructor. No used-by edges are recorded yet; the declaration is infrastructure for those later bridges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.