Signal8
plain-language theorem explainer
An 8-tick signal is a complex-valued function on the cyclic index set of order 8. It is the ambient state type for the discrete shift and its DFT-8 diagonalization in the complex-structure forcing argument. Anyone citing the forced appearance of i as an eigenvalue of the tick shift works in this type. The declaration is a pure type synonym with no proof content.
Claim. An 8-tick signal is a map $s:\{0,1,\ldots,7\}\to\mathbb{C}$ (equivalently, a vector in $\mathbb{C}^8$ indexed by the cyclic group of order 8).
background
The module Complex Structure Forcing argues that the eight-tick evolution (T7) produces a cyclic shift $T$ with $T^8=I$ on ledger states, whose eigenvalues are the 8th roots of unity. One of those roots is $\omega^2=e^{i\pi/2}=i$, which has no real square root because $x^2+1>0$ for all real $x$. Hence $T$ cannot be diagonalized over $\mathbb{R}$; the passage to $\mathbb{C}$ is algebraically forced, and the DFT-8 is the canonical unitary diagonalization.
In that setting a signal is simply a complex assignment to each tick index. The fundamental time quantum is one tick ($\tau_0=1$ in RS-native units), and one octave is eight ticks. The type therefore packages the discrete period-8 domain together with the complex codomain required by the eigenvalue argument.
proof idea
Definitional abbreviation only: Signal8 is introduced as the function type Fin 8 → ℂ. No lemmas are applied and no tactics run.
why it matters
This type is the carrier for the shift operator, its iterates, the DFT-8 basis, and the eigenvalue identities (including $\omega^2=i$ and $\omega^6=-i$) that close the "complex Hilbert space from cost" gap. The module depends on T5 (J-cost uniqueness), T7 (eight-tick octave), and T8 ($D=3$). Downstream siblings use the type to prove that the real shift is not diagonalizable, that the DFT-8 unitarily diagonalizes it, and that J-cost depends only on DFT moduli (phase invariance), so admissibility-preserving maps are unitary. No used-by edges are recorded yet; the declaration is infrastructure for that chain rather than a cited theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.