Pith. sign in
module module moderate

IndisputableMonolith.Foundation.CliffordBridge

show as:
view Lean formalization →

Bridge from Euclidean Clifford algebras Cl(3) and Cl(8) to the RS eight-tick cycle. Defines the standard quadratic forms, Bott periodicity, and a grading map from DFT-8 modes into the Z/2 grading. DimensionForcing imports it to force spatial D = 3. Structure is mostly definitions plus the theorem that the Clifford period equals eight.

claimPackage of the Euclidean Clifford algebras $\mathrm{Cl}(3)$ and $\mathrm{Cl}(8)$ for $Q(v)=\sum_i v_i^2$, the Bott period of real Clifford algebras, and a grading homomorphism from the eight DFT-8 modes into the $\mathbb{Z}/2$ grading group, with the identity that the Clifford period equals $8$.

background

Recognition Science forces an eight-tick recognition cycle (period $2^3$) and, downstream, spatial dimension $D=3$. Clifford algebras supply the algebraic skeleton that matches both: the real Clifford algebra of Euclidean $\mathbb{R}^n$ is generated by vectors with $v^2=Q(v)$, and Bott periodicity says the stable isomorphism type of $\mathrm{Cl}(n)$ repeats every $8$ in $n$.

This module specializes the Euclidean quadratic form to $n=3$ and $n=8$, names the corresponding algebras $\mathrm{Cl}(3)$ and $\mathrm{Cl}(8)$, and records the classical period-$8$ fact. It also ties the spectral side in: the DFT-8 backbone (primitive eighth root $\omega=e^{-2\pi i/8}$) supplies eight modes that are mapped into the $\mathbb{Z}/2$ grading group of the Clifford algebra, with an additivity compatibility lemma.

Constants supplies the RS tick $\tau_0$; DFT8 supplies the unitary eight-mode basis. Together they fix the discrete time and frequency scaffolding that the Clifford grading is asked to match.

proof idea

Definition-heavy module. Euclidean quadratic forms on $\mathbb{R}^3$ and $\mathbb{R}^8$ are introduced by the standard sum-of-squares recipe. $\mathrm{Cl}(3)$ and $\mathrm{Cl}(8)$ are the associated Clifford algebras. Bott periodicity is stated as a named structure; the theorem cliffordPeriod_eq_eight discharges the period claim by appeal to that classical fact (one-line or short algebraic wrapper). Grading data (GradingGroup, modeToGrading, grading_add_compatible) wire DFT-8 mode indices into the $\mathbb{Z}/2$ grading and check additivity. No long tactic developments; the load-bearing content is the period identity and the grading bridge.

why it matters in Recognition Science

Feeds Foundation.DimensionForcing, whose module doc states that spatial $D=3$ is forced by the RS framework and opens with a topological linking argument. The Clifford side supplies the algebraic reason $3$ and $8$ appear together: $\mathrm{Cl}(3)$ is the spatial algebra, while Bott period $8$ matches the eight-tick octave (primer T7) that DimensionForcing uses en route to T8 ($D=3$).

Without a clean Cl(3)/Cl(8) and period-$8$ interface, the dimension-forcing chain would have to re-derive Bott periodicity and the mode grading in situ. This module isolates that bridge so DimensionForcing can cite period eight and the grading map rather than rebuild them. It does not itself prove $D=3$; it is the algebraic prerequisite.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (31)