star_

The module Complex Structure Forcing shows that the eight-tick shift (T7) cannot be diagonalized over $\mathbb{R}$, so complexification is algebraically forced. The cyclic shift $T$ on the ledger state space satisfies $T^8=I$; its eigenvalues are the eighth roots of unity $\omega^k=e^{2\pi i k/8}$. In particular $\omega^2=i$ has no real representative, since $x^2+1>0$ for all real $x$.

Locally one works with a primitive root $\zeta=\exp(2\pi i/8)$. The spectral layer already exports a canonical DFT-8 root $\omega_8$. Conjugation must identify these two roots so that the local DFT transform can be rewritten as multiplication by the standard DFT-8 matrix, and so that conjugated powers stay aligned with the backbone.

The broader chain depends on T5 (J-cost uniqueness), T7 (eight-tick octave), and T8 ($D=3$), and aims to close the gap from cost axioms to a complex Hilbert-space structure with genuine unitarity and Parseval.

First prove an auxiliary fact on the argument: conjugating $2\pi i/8$ yields $-i\pi/4$, by Complex.ext plus simp on star_def and div_eq_mul_inv, then ring. The main calc unfolds ζ, rewrites conjugation through Complex.exp via exp_conj, substitutes the argument identity, and finishes by rfl against the definition of omega8.

This private lemma is the root identification that lets conjugated powers of ζ match powers of the canonical DFT-8 root, and thereby lets the local DFT equal multiplication by the standard DFT-8 matrix. That alignment is required for the module's claim that DFT-8 is the canonical unitary diagonalization of the eight-tick shift, that Parseval holds, and that J-cost (depending only on modulus) is phase-invariant. In the forcing chain it supports the step from T7's cyclic shift to a complex Hilbert space forced rather than postulated, closing the registry gap "Complex Hilbert space from cost".