modeToGrading
plain-language theorem explainer
Sends each DFT mode index in Fin 8 to its residue class in the Clifford grading group Z/8Z. Anyone building the 8-tick to Cl8 bridge cites this as the mode-grade correspondence. The body is the natural cast of the underlying natural number.
Claim. For each DFT mode index $k \in \{0,\ldots,7\}$, the associated Clifford grading is the residue class of $k$ in $\mathbb{Z}/8\mathbb{Z}$.
background
The module links Recognition Science's eight-tick structure to Clifford algebras through Bott periodicity: Cl_{n+8} ≅ Cl_n ⊗ Cl_8, with the 8-tick DFT identified with the grading of Cl_8. Physical motivation is that real spinor representations, KO-theory, and the division-algebra tower all repeat with period 8, matching the forced eight-tick octave (T7).
The grading group is the abbreviation GradingGroup := Z/8Z, the standard Z/8Z grading for Clifford algebras. DFT modes live in Fin 8 (indices 0 through 7). This definition is the structure map that turns a mode index into a grading class, so later lemmas can treat mode arithmetic as group arithmetic in Z/8Z.
proof idea
Pure definition: the value is the underlying natural number of the Fin 8 index, interpreted in ZMod 8. No lemmas or tactics; the cast Fin.val → ZMod 8 is the entire content.
why it matters
Supplies the mode_grade_correspondence field of the canonical DFT-Clifford bridge, and is the map whose additivity is proved by grading_add_compatible (mode sum mod 8 equals sum of grades in Z/8Z). That pair is what makes the bridge a genuine group homomorphism from DFT mode addition to Clifford grading.
In the framework this is the concrete identification behind "8-tick as Cl_8": the eight DFT bins are the eight grading degrees. It sits under the Bott-periodicity story that explains why the forcing chain locks the octave at period 2^3 (T7) rather than some other cycle length.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.