standardDFT8Basis
plain-language theorem explainer
Packages the eight DFT-8 mode vectors as the canonical eight-tick basis: mode 0 is the constant DC mode, modes 1–7 are mean-free, and the full set is orthonormal in ℂ⁸. Spectral and 8-tick work cites this as the standard instance of the bundled basis structure. The body is a pure structure assembly that wires four already-proved mode lemmas into the fields.
Claim. The standard eight-point DFT basis is the eight-tick basis whose mode vectors are the columns of the unitary DFT-8 matrix $B_{t,k}=\omega^{tk}/\sqrt{8}$ with $\omega=e^{-2\pi i/8}$. Mode $0$ equals the constant $1/\sqrt{8}$ at every tick, each mode $k=1,\ldots,7$ has vanishing sum over ticks, and the eight modes are orthonormal under the standard Hermitian product on $\mathbb{C}^8$.
background
The DFT-8 module builds the spectral backbone of the forced eight-tick recognition cycle. The primitive root is $\omega=e^{-2\pi i/8}$; matrix entries are $\omega^{tk}/\sqrt{8}$; columns of that matrix are the mode vectors. Companion facts already record that the matrix is unitary, that it diagonalizes the cyclic shift (eigenvalue $\omega^k$ on mode $k$), and that modes $1..7$ span the mean-free subspace.
EightTickBasis is the bundled structure used for all 8-tick spectral operations: a map from mode index to $\mathbb{C}^8$ vector, together with three certificates (DC mode, neutrality of the rest, orthonormality). The cyclic shift itself is the discrete time-evolution generator $T$ on 8-signals, $(Tf)(k)=f(k+1\bmod 8)$, and the eight phases are $k\pi/4$.
Physically, the period $\tau_0=2^D$ with $D=3$ is forced by the Recognition axioms (T7/T8). DFT-8 is the unique (up to phase and permutation) unitary basis that diagonalizes time-translation, separates DC from neutral modes, and supplies $\varphi$-lattice quantization via complex exponentials. The Clifford bridge notes the same 8-periodicity via $\mathrm{Cl}_{n+8}\cong\mathrm{Cl}_n\otimes\mathrm{Cl}_8$.
proof idea
Definitional structure assembly, not a tactic proof. The modes field is set to the existing column map dft8_mode. The three proof fields are discharged by direct appeal to prior lemmas: constant DC mode (dft8_mode_zero_constant), vanishing sum on nonzero modes (dft8_mode_neutral), and column orthonormality of the DFT-8 matrix (dft8_column_orthonormal). No new algebra is performed here.
why it matters
This is the named standard instance that every 8-tick spectral construction is expected to use. Downstream it is the reference object in the canonicity hypothesis: any other orthonormal eight-tick basis that diagonalizes cyclic shift must equal this one up to unit-modulus phases and a permutation of modes. That hypothesis was demoted from an axiom because nothing yet depends on it, but the instance itself remains the concrete carrier of the DFT-8 backbone.
In the Recognition chain this sits under T7 (eight-tick octave, period $2^3$) and T8 ($D=3$), and under the physical claim that DFT-8 is the canonical unitary basis for the recognition cycle: it diagonalizes the shift, splits DC from neutral modes, and supplies the complex-exponential ladder used for $\varphi$-lattice quantization. It also aligns with the Clifford/Bott story that the 8-tick DFT grading matches $\mathrm{Cl}_8$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.