x2_plus_1_divides_x8_minus_1

The module Complex Structure Forcing argues that the eight-tick cyclic shift $T$ on ledger signals cannot be diagonalized over $\mathbb{R}$. By T7 the evolution period is eight ticks, so $T^8 = I$ and the spectrum of $T$ consists of the 8th roots of unity $\zeta^k = e^{2\pi i k/8}$.

Mode $k=2$ gives $\zeta^2 = i$, which solves $x^2+1=0$. The companion fact that no real $x$ satisfies that equation then forces the eigenspaces out of $\mathbb{R}$ into $\mathbb{C}$. The present lemma is the pure algebraic link: solutions of $x^2+1=0$ already lie on the unit circle of order dividing 8, so they are legitimate eigenvalues of an order-8 unitary shift.

Upstream, eigenvalue packages $\zeta^k$ and shift is the cyclic advance on Signal8; the tick constant fixes the discrete time quantum underlying the octave.

Rewrite the hypothesis as $x^2 = -1$ via add_eq_zero_iff_eq_neg. Then expand $x^8 = (x^2)^4$ by ring, substitute to get $(-1)^4$, and finish with norm_num. No spectral or RS-specific lemmas are needed; it is elementary field arithmetic in $\mathbb{C}$.

This is a supporting algebraic step in the complexification-forcing chain (module closes the "complex Hilbert space from cost" gap, depending on T5, T7, T8). Once $i$ is known to be an 8th root of unity, the DFT-8 diagonalization of the shift is legitimate and the non-reality of $i$ (sibling no_real_root_x2_plus_1) shows that full diagonalization requires $\mathbb{C}$, not merely $2\times 2$ real rotation blocks.

Downstream the core theorem states that the shift has eigenvalue $i$ at $k=2$ and therefore complexification is forced, not chosen. The lemma underwrites that identification: roots of $x^2+1$ sit inside the cyclotomic spectrum forced by the eight-tick octave. No direct used_by edges are recorded yet; the natural consumers are eigenvalue_2_is_I and the complexification theorem itself.