EvolutionOp
plain-language theorem explainer
An evolution operator on the eight-tick ledger is any map from complex 8-signals to themselves. Downstream unitarity and cost-admissibility sit on this carrier. The declaration is a bare structure with one field; no proof content.
Claim. An evolution operator is a function $U:(\mathrm{Fin}\,8\to\mathbb{C})\to(\mathrm{Fin}\,8\to\mathbb{C})$ on complex-valued signals indexed by the eight-tick cycle.
background
The module Complex Structure Forcing shows that the T7 eight-tick cyclic shift on ledger states cannot be diagonalized over $\mathbb{R}$: its spectrum includes the 8th roots of unity, and $\omega^2=i$ has no real representative because $x^2+1>0$ for all real $x$. Complexification is therefore algebraically forced, with DFT-8 as the canonical unitary diagonalization.
A signal on that cycle is a map $\mathrm{Fin},8\to\mathbb{C}$. The Recognition cost $J$ (T5 uniqueness: $J(x)=(x+x^{-1})/2-1$) depends only on mode moduli, not phases, so phase-preserving dynamics are cost-neutral once norms are fixed. Evolution operators are the raw maps on which those constraints will be imposed.
proof idea
No proof: a structure definition with a single field evolve of type Signal8 → Signal8. Admissibility (inner-product preservation and J-cost non-increase) is added later by the extending structure UnitaryEvolution.
why it matters
This is the bare carrier for dynamics in the complex-structure forcing chain. UnitaryEvolution extends it by requiring inner-product preservation and non-increasing total mode cost; together those conditions encode unitarity of the recognition operator on the forced complex Hilbert space.
It sits under the module's registry close of the "complex Hilbert space from cost" gap, which depends on T5 (J uniqueness), T7 (eight-tick octave), and T8 ($D=3$). Without a named map type on Signal8, the later Parseval and cost-phase-invariance arguments have nowhere to attach.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.