shift_matrix
plain-language theorem explainer
The 8×8 complex matrix of the cyclic forward shift on the eight-tick register: entry (t,s) is 1 exactly when s ≡ t+1 (mod 8). Anyone proving that DFT-8 diagonalizes time translation cites this operator. The body is a pure pointwise definition, no proof obligations.
Claim. Define the cyclic shift matrix $S \in M_8(\mathbb{C})$ by $S_{t,s} = 1$ if $s \equiv t+1 \pmod{8}$ and $S_{t,s} = 0$ otherwise, for indices $t,s \in \{0,\ldots,7\}$.
background
The DFT-8 module builds the canonical unitary basis for the Recognition Science eight-tick cycle. The period $\tau_0 = 2^D$ with $D=3$ is forced upstream (T7), so the discrete time-translation generator lives on $\mathbb{C}^8$.
Sibling objects include the primitive root $\omega = e^{-2\pi i/8}$, the DFT matrix with entries $\omega^{tk}/\sqrt{8}$, and the functional cyclic shift on 8-vectors. The matrix form here is the linear-algebra avatar of that shift: the permutation matrix of the 8-cycle.
Physically, $S$ is the discrete time-step on the recognition register. Spectral theory of the cycle reduces to simultaneous diagonalization of $S$ by the DFT basis, separating the DC mode from the seven neutral modes.
proof idea
Pure definition: the matrix is the function sending indices $(t,s)$ to $1$ when $s.val = (t.val + 1) \bmod 8$ and to $0$ otherwise. No lemmas, tactics, or obligations; Mathlib's Matrix API treats this as an ordinary pointwise matrix.
why it matters
This is the concrete operator whose spectral theorem the module is built around. Downstream, shift_mul_dft8_entry shows $S$ multiplies DFT column $j$ by $\omega^j$; conjTranspose_shift_mul and dft8_diagonalizes_shift assemble that into $B^H S B = \mathrm{diag}(1,\omega,\ldots,\omega^7)$. The uniqueness hypothesis then states that any unitary basis diagonalizing this same $S$ agrees with DFT-8 up to permutation and phase.
In the forcing chain this sits under T7 (eight-tick octave): time-translation symmetry on the forced period must be diagonalized by the canonical spectral basis. Without an explicit matrix $S$, the diagonalization and uniqueness statements have nothing to act on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.