EightTickBasis
plain-language theorem explainer
Bundles an eight-mode complex basis on the discrete 8-tick cycle with three axioms: mode 0 is the constant DC vector of amplitude 1/√8, modes 1–7 are mean-free, and the full set is orthonormal. Anyone working on 8-tick spectral decompositions or shift-diagonal bases cites this as the interface type. It is a pure structure definition; instances supply the fields.
Claim. An eight-tick basis is a map $B:\{0,\ldots,7\}\to(\mathbb{C}^8)$ such that (i) the zero mode is constant, $B_0(t)=1/\sqrt{8}$ for all $t$; (ii) every nonzero mode is mean-free, $\sum_t B_k(t)=0$ for $k\neq 0$; (iii) the modes are orthonormal, $\sum_t \overline{B_k(t)}B_{k'}(t)=\delta_{kk'}$.
background
The DFT-8 module treats the eight-tick recognition cycle forced by the RS octave (period $2^3$, landmark T7 with $D=3$). The primitive root $\omega=e^{-2\pi i/8}$ builds matrix entries $\omega^{tk}/\sqrt{8}$; columns of that unitary matrix are the standard modes. The cyclic shift on 8-vectors is diagonalized by this basis, with eigenvalue $\omega^k$ on mode $k$.
Physically one needs a clean split between the DC (constant) channel and the seven neutral, mean-free channels that carry oscillatory content on the $\varphi$-lattice. The structure packages exactly those three properties so later lemmas can quantify over any basis meeting them, not only the concrete DFT columns.
Module results already record unitarity of the DFT-8 matrix, diagonalization of cyclic shift, and that modes $k=1..7$ span the neutral subspace. This structure is the abstract type those facts inhabit.
proof idea
No proof body: this is a structure declaration. The four fields are the data and the three Prop fields that any instance must discharge. Concrete filling is deferred to the standard instance, which sets modes to the DFT columns and cites the existing lemmas that the zero column is constant $1/\sqrt{8}$, nonzero columns sum to zero, and columns are orthonormal.
why it matters
Gives the typed interface for all 8-tick spectral work in the monolith. Downstream, the standard DFT-8 basis is the canonical instance, and the canonicity hypothesis states that any orthonormal eight-tick basis that diagonalizes cyclic shift equals the standard one up to unit-modulus phases and a permutation of modes. That hypothesis was demoted from an axiom because nothing yet depends on uniqueness; the structure itself remains the place where DC/neutral/orthonormality are required.
In the RS forcing chain this sits under T7 (eight-tick octave) and the claim that DFT-8 is the unique (up to phase/permutation) unitary basis separating DC from neutral modes while diagonalizing time-translation on the cycle. Parent consumers are therefore any spectral identity stated for a generic eight-tick basis rather than hard-coded DFT columns.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.