complexification_forced
plain-language theorem explainer
The 8-tick cyclic shift on ledger signals has eigenvalue i at mode k=2, and x²+1 has no real root, so T cannot be fully diagonalized over ℝ. Anyone citing the forced complex Hilbert structure from T7 uses this. The proof is a one-line packaging of the k=2 eigenvalue identity with the real-rootlessness of x²+1.
Claim. There exists a mode $k\in\{0,\ldots,7\}$ such that the eigenvalue of the 8-tick shift at $k$ equals $i$, and for every real $x$ one has $x^2+1\neq 0$.
background
This module shows that the 8-tick shift cannot be diagonalized over the reals: complexification is algebraically forced. Under T7 the ledger state space carries a cyclic shift $T$ with $T^8=I$. Its eigenvalues are the eighth roots of unity $\zeta^k=e^{2\pi i k/8}$.
A Signal8 is a map $\mathrm{Fin},8\to\mathbb{C}$. The mode eigenvalue is defined by $\mathrm{eigenvalue}(k)=\zeta^{k}$. Upstream, eigenvalue_2_is_I records that the $k=2$ value is exactly $i$, and x2_plus_1_no_real_root is the corollary that $x^2+1$ never vanishes on $\mathbb{R}$.
Over $\mathbb{R}$ alone, $T$ can at best be block-diagonalized into $2\times 2$ rotation blocks; full diagonalization requires $\mathbb{C}$. The DFT-8 is then the canonical unitary diagonalization.
proof idea
Term-mode packaging of two prior facts. The existential half is witnessed by $k=\langle 2,_\rangle$ together with eigenvalue_2_is_I (which reduces via the definition of eigenvalue to $\zeta^2=i$). The universal half is exactly x2_plus_1_no_real_root. The proof is exact ⟨⟨⟨2, by norm_num⟩, eigenvalue_2_is_I⟩, x2_plus_1_no_real_root⟩.
why it matters
Core forcing step: the eight-tick octave (T7) forces $\mathbb{C}$ as the scalar field for the recognition carrier. The module doc frames this as closing the "complex Hilbert space from cost" gap, depending on T5 (J-uniqueness), T7, and T8 ($D=3$).
Downstream, t7_t8_to_operator_bridge_holds installs this theorem as the complexification field of the T7/T8-to-operator-core bridge ("the forced dimension/eight-tick package supplies the analytic operator core"). It also underwrites UnitaryEvolution (admissible evolutions preserve the DFT-8 inner product and are J-cost non-increasing) and sits beside hamiltonian_emergence (quadratic small-deviation expansion of $J$ as kinetic energy). Without it, the path from cost axioms to genuine unitarity on a complex Hilbert space does not close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.