complexification_forced
plain-language theorem explainer
The eight-tick cyclic shift on the length-8 recognition carrier has eigenvalue i at mode k=2, and i is not real. Full diagonalization of that shift therefore requires complex scalars; over the reals one only gets 2×2 rotation blocks. Anyone citing the T7–T8 operator bridge or unitary evolution on Signal8 needs this fact. The underlying proof is a one-line pairing of the k=2 eigenvalue lemma with the elementary fact that x²+1 has no real root.
Claim. There exists a mode index $k\in\{0,\ldots,7\}$ such that the eigenvalue of the length-8 cyclic shift at $k$ equals $i$, and for every real $x$ one has $x^2+1\neq 0$. Hence the eigenspaces of the eight-tick shift cannot be fully diagonalized over $\mathbb{R}$; complex scalars are forced.
background
Recognition Science forces an eight-tick discrete clock (T7 in the unified forcing chain): the fundamental recognition carrier is a length-8 signal space, written Signal8, with a cyclic shift operator T that advances the tick. The DFT-8 modes diagonalize T, and the eigenvalue at mode $k$ is a primitive eighth root of unity.
The local module re-exports the complex-structure forcing package so that the operator core can cite a single name. The key upstream statement is the theorem that mode $k=2$ has eigenvalue exactly $i=\mathrm{Complex.I}$, together with the elementary real-algebra fact that $x^2+1$ has no real root. Over $\mathbb{R}$, $T$ is only block-diagonalizable into planar rotations; full spectral decomposition needs $\mathbb{C}$.
Sibling infrastructure includes the DFT-8 / IDFT-8 pair, the Hermitian inner product on Signal8, the complexified J-cost on modes, and the admissible unitary evolutions that preserve that inner product while not increasing total mode cost.
proof idea
This declaration is a pure abbrev re-export of the Foundation theorem of the same name; there is no local proof body. The underlying theorem is itself a one-line constructor: pair the concrete witness $k=2$ (with eigenvalue_2_is_I) against the lemma that no real satisfies $x^2+1=0$. No further algebraic reduction is required at this layer.
why it matters
This is the core "eight-tick forces $\mathbb{C}$" step. Downstream, the unified forcing chain plugs it directly into t7_t8_to_operator_bridge_holds as the complexification field of the T7–T8-to-operator-core bridge, so the forced dimension/eight-tick package supplies an analytic operator core over $\mathbb{C}$. The same name is referenced by the admissible UnitaryEvolution structure (inner-product preservation plus J-cost non-increase) and sits beside Hamiltonian emergence from the small-deviation expansion $J(1+\varepsilon)=\varepsilon^2/2+O(\varepsilon^3)$.
In the primer landmarks this closes the passage from T7 (eight-tick octave, period $2^3$) into complex quantum kinematics: without complexification one cannot write unitary tick evolution or a spectral Hamiltonian on the recognition carrier. It does not itself prove unitarity or the Hamiltonian limit; those are separate downstream theorems that assume the complex scalar field is available.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.