complex_structure_certificate
plain-language theorem explainer
Packages five proved facts into the master certificate that complex structure is forced by cost plus the eight-tick: period-8 shift, eigenvalue i, no real root of x²+1, unitary DFT-8, and J-cost phase invariance. Cited by the T7-to-canonical-carrier bridge in the unified forcing chain. Proof is a pure structure inhabitant assembling five prior lemmas.
Claim. There exists a complex-structure certificate: the eight-tick shift on length-8 signals satisfies $T^8 = \mathrm{id}$; the mode-$2$ eigenvalue equals $i$; $x^2+1 \neq 0$ for all real $x$; the DFT-8 preserves the standard inner product; and total mode cost is invariant under arbitrary per-mode phase multiplications.
background
The module argues that the eight-tick shift on ledger signals cannot be diagonalized over $\mathbb{R}$, so complexification is algebraically forced. An eight-component signal lives on $\mathrm{Fin},8 \to \mathbb{C}$. The cyclic shift $T$ obeys $T^8 = I$ (T7). Its eigenvalues are the eighth roots of unity; the $k=2$ root is $e^{i\pi/2} = i$, which has no real representative because $x^2+1 > 0$ on $\mathbb{R}$.
The DFT-8 is the canonical unitary diagonalization (Parseval: $\langle F(f), F(g)\rangle = \langle f,g\rangle$). Recognition cost $J$ depends only on mode moduli, not arguments, so phase multiplications leave total mode cost fixed. The certificate structure records exactly these five properties as the master claim that cost axioms plus the eight-tick force complex Hilbert structure.
Upstream lemmas supply each field: period-8 of the iterated shift, the explicit eigenvalue identity for mode 2, the elementary real-polynomial fact, DFT-8 Plancherel, and mode-cost phase invariance.
proof idea
Term-mode structure inhabitant. Each field is filled by a named prior theorem: periodicity by shift_period_8; has_imaginary_eigenvalue by eigenvalue_2_is_I; imaginary_not_real by x2_plus_1_no_real_root; dft_unitary by dft8_preserves_inner (Parseval via root-of-unity orthogonality); cost_phase_invariant by mode_cost_phase_invariant. No new calculation occurs here; the certificate is the packaging.
why it matters
Closes the registry gap "Complex Hilbert space from cost": unitarity and complex structure are not postulated but forced by T5 (J-uniqueness), T7 (eight-tick octave), and T8 ($D=3$). Downstream, t7_to_canonical_carrier_bridge_holds in the unified forcing chain consumes the period-8 fact from this module to bridge T7 to the canonical recognition carrier.
The certificate is the single object a later development can cite instead of five separate lemmas. It sits immediately before the cost-phase duality section ($J(e^t) = \cosh t - 1$, with imaginary axis as phase), which needs complex structure already on the table. Framework landmarks: T5 J-cost, T7 eight-tick, T8 spatial dimension three.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.