Pith. sign in
module module moderate

IndisputableMonolith.Foundation.CliffordBridge

show as:
view Lean formalization →

Bridges real Clifford algebras Cl(3) and Cl(8) to the eight-tick recognition cycle via Bott periodicity. Supplies Euclidean quadratic forms, the period-eight identification, and a mode-to-grading map used when forcing spatial dimension D = 3. DimensionForcing imports the package. Mostly definitions and short algebraic identities, not a long derivation.

claimModule introducing Euclidean quadratic forms $Q_3(v)=\sum_{i=1}^3 v_i^2$ and $Q_8$ on $\mathbb{R}^3$ and $\mathbb{R}^8$, the real Clifford algebras $\mathrm{Cl}(3)$ and $\mathrm{Cl}(8)$, the Clifford period equal to eight, Bott periodicity, and a grading group with an additive mode-to-grading map on the eight-tick cycle.

background

Recognition Science forces an eight-tick octave (T7) and spatial dimension $D=3$ (T8). Real Clifford algebras encode the geometric product on Euclidean space; Bott periodicity states that their stable isomorphism type repeats every eight dimensions. That period matches the recognition cycle length.

Upstream, Constants fixes the RS time quantum $\tau_0=1$ tick, and Spectral.DFT8 supplies the eight-point DFT backbone with primitive root $\omega=e^{-2\pi i/8}$ as the unitary basis of the cycle. This module sits between that spectral backbone and the dimension-forcing arguments.

It records the standard Euclidean quadratic form on $\mathbb{R}^3$ (specialized for the main application) and the analogous form on $\mathbb{R}^8$, packages $\mathrm{Cl}(3)$ and $\mathrm{Cl}(8)$, and ties the Clifford period to eight so grading data can talk to DFT-8 modes.

proof idea

Definition-and-bridge module, not a single deep theorem. It introduces the Euclidean quadratic forms in dimensions 3 and 8, names the associated real Clifford algebras, asserts that the Clifford period equals eight, records Bott periodicity as the structural fact behind that period, and builds a grading group with a mode-to-grading map shown compatible with addition on the cycle. Supporting lemmas are short equalities and structure-map identities meant for import, not a multi-step forcing proof.

why it matters in Recognition Science

Direct import of Foundation.DimensionForcing, whose stated goal is to prove that spatial dimension $D=3$ is forced by the RS framework (forcing-chain landmark T8). That module's linking and related arguments need Clifford structure on $\mathbb{R}^3$ together with a period-eight match to the eight-tick octave (T7).

By aligning the Bott period of real Clifford algebras with the DFT-8 recognition cycle, the bridge lets topological and grading steps in DimensionForcing cite a common period rather than an ad hoc identification. Without this package, the $D=3$ forcing chain would have to re-derive or re-import the Clifford side inline.

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)