dft8_unique_up_to_phase_hypothesis
plain-language theorem explainer
Among unitary 8×8 matrices that diagonalize the cyclic shift on ℂ⁸, the DFT-8 matrix is unique up to column permutation and unimodular diagonal phases. Anyone fixing the spectral basis of the eight-tick recognition cycle would cite this uniqueness. The declaration is only a Prop packaging that claim (formerly an unused axiom); no proof is attached.
Claim. For every unitary $B \in U(8)$ that diagonalizes the cyclic shift on $\mathbb{C}^8$, there exist phases $\varphi_k$ with $|\varphi_k|=1$ and a permutation $\sigma$ of $\{0,\ldots,7\}$ such that $B_{t,k} = \varphi_k \, F_{t,\sigma(k)}$ for all $t,k$, where $F$ is the standard DFT-8 matrix with entries $\omega^{tk}/\sqrt{8}$ and $\omega = e^{-2\pi i/8}$.
background
The module builds the 8-point DFT as the canonical unitary basis for the eight-tick recognition cycle. The period $2^D$ with $D=3$ is the forced octave (T7/T8): eight ticks, hence an 8-dimensional discrete time circle. The primitive root $\omega = e^{-2\pi i/8}$ supplies the characters of $\mathbb{Z}/8\mathbb{Z}$; DFT-8 entries are $\omega^{tk}/\sqrt{8}$, assembled into the unitary matrix $F$.
The cyclic shift operator on $\mathbb{C}^8$ is the time-translation generator of the tick lattice. DFT-8 diagonalizes it, with eigenvalue $\omega^k$ on mode $k$, and splits the DC mode ($k=0$) from the mean-free neutral subspace ($k=1..7$). Uniqueness of that eigenbasis is the representation-theoretic fact that $\mathbb{Z}/8\mathbb{Z}$ has eight distinct 1-dimensional irreps, so eigenspaces are lines and eigenvectors are unique up to phase (and ordering).
proof idea
No proof: the declaration is a bare Prop definition, not a theorem. It encodes three hypotheses on an arbitrary $B$: unitarity ($B^H B = I$), simultaneous diagonalization of the cyclic shift matrix, and the conclusion that $B$ equals DFT-8 after a unimodular diagonal phase matrix and a column permutation. The doc-comment sketches the intended argument (characters of $\mathbb{Z}/8\mathbb{Z}$, 1-dimensional eigenspaces) but nothing is formalized here. The object was demoted from an axiom because no downstream proof consumed it.
why it matters
DFT-8 is advertised as the unique (up to perm/phase) unitary basis that diagonalizes tick-shift, separates DC from neutral modes, and supplies $\varphi$-lattice phases on the eight-tick octave forced by T7 ($2^3$) and T8 ($D=3$). This Prop is the precise uniqueness statement behind that canonicity claim in the module header.
It currently has no used_by edges: the formal development does not depend on it. The doc-comment records the demotion from axiom to unused hypothesis. Closing it as a real theorem would pin the "canonical spectral basis" slogan to representation theory of cyclic groups; leaving it open means canonicity of DFT-8 in the monolith rests on the constructive definitions (dft8_matrix, dft8_unitary, dft8_diagonalizes_shift) rather than on uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.