omega8_abs
plain-language theorem explainer
The primitive eighth root of unity for the DFT-8 backbone has complex modulus one. Spectral and Schrödinger-derivation proofs cite this to keep norms invariant under multiplications by powers of ω. The argument rewrites ω as a pure-phase exponential and applies the standard identity ‖e^{iθ}‖ = 1.
Claim. If $\omega = e^{-2\pi i/8}$ is the primitive eighth root of unity used by the eight-point DFT, then $\|\omega\| = 1$.
background
The DFT-8 module builds the canonical unitary basis for the eight-tick recognition cycle forced by T7 (period $2^3$ with $D=3$). Its generator is the local primitive root $\omega = e^{-2\pi i/8}$ (equivalently $e^{-i\pi/4}$), the DFT convention with negative frequency sign.
Entries of the DFT-8 matrix are $\omega^{tk}/\sqrt{8}$. Unit modulus of $\omega$ is the elementary complex-analytic fact that makes every pure phase factor norm-preserving, and therefore makes the DFT columns unit vectors once the $1/\sqrt{8}$ normalization is in place.
Upstream, a related root appears in the cycle-operator layer (there with the opposite sign convention $e^{+i\pi/4}$). Both conventions satisfy $|\omega|=1$; only the local DFT definition is used here.
proof idea
Unfold the local definition of $\omega$ and rewrite the exponent so that $\omega = \exp\bigl((-\pi/4), i\bigr)$ as a real multiple of $i$. Then apply Complex.norm_exp_ofReal_mul_I, which states $|e^{i\theta}|=1$ for every real $\theta$. The algebraic cleanup is a short simp/ring congruence on the real coefficient; no spectral or ledger facts are needed.
why it matters
One-tick evolution on DFT modes multiplies each mode $k$ by $\omega^k$. Downstream, eigenmode_norm_preserved in the Schrödinger derivation uses $|\omega|=1$ (via $|\omega^k|=1$) to conclude that cyclic shift preserves the pointwise norm of every scaled eigenmode, the discrete unitarity step behind the continuum Schrödinger limit.
In the Recognition framework this sits on the T7 eight-tick octave: DFT-8 is the unique (up to permutation/phase) unitary basis that diagonalizes the cyclic shift and splits DC from the neutral subspace. Without unit modulus, the DFT columns would not be normalized and the shift would not act isometrically on modes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.