grading_add_compatible
plain-language theorem explainer
Addition of DFT mode indices modulo 8 is preserved by the map into the Clifford grading group Z/8Z. Anyone assembling the DFT–Clifford bridge cites this as the additive homomorphism property of the mode-to-grade correspondence. The proof is a two-line simplification: unfold the map and apply the quotient arithmetic of Z/8Z.
Claim. For all mode indices $k,k'\in\{0,\ldots,7\}$, the Clifford grading of the sum of modes modulo 8 equals the sum of the gradings: $\mathrm{grade}((k+k')\bmod 8)=\mathrm{grade}(k)+\mathrm{grade}(k')$ in the grading group $\mathbb{Z}/8\mathbb{Z}$.
background
The CliffordBridge module links Recognition Science's eight-tick structure to Clifford algebras via Bott periodicity. The physical claim is that the 8-tick DFT cycle is the same periodicity that grades Cl₈ and underlies real spinor representations in three spatial dimensions (T7/T8 landmarks: period 2³ and D=3).
DFT modes are indexed by Fin 8. The map modeToGrading sends a mode index k to its value in the grading group GradingGroup (identified with Z/8Z). That map is the candidate correspondence between the eigenvalue label ω^k of the cyclic shift and the grade-k component of Cl₈.
For the correspondence to be a bridge, it must be a group homomorphism from mode addition mod 8 into the grading group. This lemma is exactly that compatibility statement.
proof idea
Term-style proof by simplification. First unfold modeToGrading, which is the coercion of the Fin 8 value into GradingGroup. The left-hand side then becomes the natural-number sum reduced mod 8, cast into Z/8Z. Two simp lemmas finish it: ZMod.natCast_mod (casting a residue class is the class itself) and Nat.cast_add (casts preserve addition). No case split on the eight residues is required; the quotient structure does the work.
why it matters
This is the additive half of the canonical DFT–Clifford bridge. Downstream, canonicalBridge packages modeToGrading together with this lemma as preserves_addition, plus a one-line check that grade 8 vanishes, yielding the structure DFTCliffordBridge.
In the Recognition framework the lemma underwrites why the eight-tick octave (T7) is not an ad-hoc clock: mode addition on the DFT side matches grade addition on the Cl₈ side, so the same Z/8Z organises both the spectral cycle and the Clifford grading. That identification is the concrete content of the module claim that "the 8-tick DFT structure is isomorphic to the grading of Cl₈" and sits under the Bott-periodicity story Cl_{n+8} ≅ Cl_n ⊗ Cl_8.
It does not by itself prove Bott periodicity or the Spin(3)≅SU(2) bridge; those are sibling results. It closes the homomorphism obligation needed before the bridge object can be inhabited.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.