ComplexStructureCertificate
plain-language theorem explainer
Bundles five algebraic facts that force complex structure from the 8-tick shift and J-cost: period-8 of the cyclic shift, eigenvalue i at mode 2, no real root of x²+1, unitarity of DFT-8, and phase invariance of total mode cost. Anyone citing the T7→canonical-carrier bridge or the complex-Hilbert-space forcing chain uses this certificate type. It is a pure structure definition; satisfaction is proved separately by assembling named lemmas.
Claim. A complex-structure certificate is a record of five properties on 8-tick signals $f:\mathrm{Fin}\,8\to\mathbb{C}$: (i) the cyclic shift satisfies $T^8=\mathrm{id}$; (ii) the mode-$2$ eigenvalue of $T$ equals $i$; (iii) $x^2+1\neq 0$ for all real $x$; (iv) the DFT-8 preserves the standard inner product $\langle f,g\rangle=\sum_k \overline{f(k)}g(k)$; (v) total mode cost $\sum_k J(\|c_k\|)$ is invariant under independent phase multiplications of the modes.
background
The module closes the gap from cost axioms plus the eight-tick period to a complex Hilbert space. An 8-tick signal is a map $\mathrm{Fin},8\to\mathbb{C}$. The shift $T$ advances the tick index mod 8; its iterates are shiftIter, and the spectrum is the 8th roots of unity via eigenvalue $k\mapsto\zeta^k$.
The standard inner product is inner8, and dft8 is the normalized DFT-8 that diagonalizes $T$. Total mode cost sums the Recognition cost $J$ on mode moduli: $\sum_k J(|f(k)|)$. Upstream, $J$ is the unique cost from T5 ($J(x)=\cosh(\ln x)-1$), and T7 forces the period-$2^3$ octave.
Module thesis: $T$ cannot be diagonalized over $\mathbb{R}$ because $\omega^2=i$ has no real representative, so complexification is algebraically forced rather than postulated. DFT-8 is the canonical unitary diagonalization; phase invariance of $J$ then ties admissible evolution to unitarity.
proof idea
No proof body: this is a structure (record type) packing five Prop fields. Instantiation is deferred to the companion theorem complex_structure_certificate, which fills the fields by named lemmas: shift_period_8 (periodicity), eigenvalue_2_is_I (mode-2 eigenvalue $i$), x2_plus_1_no_real_root (no real root of $x^2+1$), dft8_preserves_inner (Parseval/unitarity of DFT-8), and mode_cost_phase_invariant (phase invariance of total mode cost). The structure itself only names the interface those lemmas must satisfy.
why it matters
This is the master certificate type for "complex Hilbert space from cost": it packages the chain from T5–T8 through shift spectrum, the real-obstruction $x^2+1\neq 0$, DFT-8 unitarity, and J-phase invariance into one object. Downstream, complex_structure_certificate proves the certificate is inhabited, and T7_To_CanonicalCarrier_Bridge in the unified forcing chain cites it to name the canonical carrier $\mathrm{Signal8}=\mathrm{Fin},8\to\mathbb{C}$, the period-8 shift with $i$ in the spectrum, and the algebraic obstruction forcing $\mathbb{C}$ over $\mathbb{R}$.
Framework landmarks: T7 (eight-tick octave), T8 ($D=3$), and the cost uniqueness T5 that supplies $J$. It closes the registry gap "Complex Hilbert space from cost" without assuming $\mathbb{C}^8$ a priori. Related structure UnitaryEvolution then reads cost-nonincreasing plus inner-product preservation as unitarity on that forced carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.