GradingGroup
plain-language theorem explainer
The grading group of the Clifford bridge is the cyclic group of order 8. Anyone linking the eight-tick DFT to Cl₈ cites this as the common Z/8Z index set for modes and grades. It is a one-line type synonym for ZMod 8, so no proof work is required.
Claim. Write $G := \mathbb{Z}/8\mathbb{Z}$ for the grading group of the Clifford algebra side of the bridge (equivalently, the additive group of residues mod 8).
background
The module CliffordBridge ties Recognition Science's forced eight-tick octave (T7) to Bott periodicity of real Clifford algebras: Cl_{n+8} ≅ Cl_n ⊗ Cl_8. On the spectral side, the 8-point DFT uses the primitive eighth root ω = e^{-2πi/8}; on the algebraic side, Cl₈ carries a natural Z/8Z grading from its tensor-product structure.
The grading group is the common index set for those two pictures. Downstream, DFT modes k ∈ Fin 8 are sent to grades in this group, and addition of modes must match addition of grades mod 8. The module also records Spin(3) ≅ SU(2) for the D = 3 spinor structure (T8), but that is separate from the grading abbreviation itself.
proof idea
Pure definitional abbreviation: GradingGroup is declared equal to Mathlib's ZMod 8. No tactics, no lemmas, no reduction. Downstream maps such as modeToGrading simply coerce a Fin 8 value into this type.
why it matters
This name is the carrier type for the DFT–Clifford bridge. The structure DFTCliffordBridge requires a map Fin 8 → GradingGroup that preserves addition mod 8 and sends eigenvalues of the cyclic shift to Clifford grades; modeToGrading and grading_add_compatible fill those fields, and canonicalBridge packages them. Without a shared Z/8Z, the claim that the eight-tick DFT is isomorphic to the grading of Cl₈ has no type-level home.
In the RS forcing chain this is the algebraic face of T7 (eight-tick octave, period 2^3) and of Bott periodicity as the reason the period is forced rather than chosen. It does not itself prove Bott periodicity or the spinor bridge; it only supplies the grading group those results act on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.