UnitaryEvolution
plain-language theorem explainer
Admissible evolution on the eight-tick signal space is defined as any map that preserves the DFT-8 inner product and does not raise total J-mode cost. Anyone citing the complex-structure forcing chain (cost axioms through unitary Hilbert dynamics) uses this as the precise notion of unitarity forced by recognition cost. It is a pure structure extending EvolutionOp; no proof body.
Claim. An admissible (unitary) evolution is a map $U$ on eight-tick signals such that $\langle Uf, Ug\rangle_8 = \langle f, g\rangle_8$ for all $f,g$, and the total mode cost satisfies $C(Uf)\le C(f)$ for every $f$. Together these encode norm preservation plus recognition-cost non-increase.
background
The module Complex Structure Forcing argues that the eight-tick cyclic shift $T$ (period $T^8=I$, forced by T7/T8) cannot be diagonalized over $\mathbb{R}$: its mode-$k=2$ eigenvalue is $i$, and $x^2+1>0$ for all real $x$. Complexification and the DFT-8 unitary diagonalization are therefore algebraic necessities, not modeling choices.
An evolution operator is simply a map on Signal8 (the eight-component ledger state). The inner product is the DFT-8 Parseval product; total mode cost aggregates the J-cost $J(x)=\cosh(\ln x)-1$ of spectral coefficients. J depends only on moduli, not phases (phase invariance), so cost-compatible dynamics can rotate phases freely while keeping norms.
Upstream landmarks: T5 uniqueness of $J$, T6 forcing of $\varphi$, T7 eight-tick octave, T8 $D=3$. The master certificate lists this structure as step 11: cost-preserving plus norm-preserving evolution is unitary.
proof idea
Definitional structure, not a proved theorem. It extends EvolutionOp by two fields: inner-product preservation for all pairs of signals, and pointwise non-increase of total mode cost. No tactics or lemmas are invoked; downstream results treat any inhabitant as the forced unitary class on $\mathbb{C}^8$.
why it matters
Closes the registry gap "complex Hilbert space from cost": after forcing $i$ via the eight-tick spectrum and identifying DFT-8 as the canonical unitary diagonalization, this packages the dynamical consequence. Cost axioms plus eight-tick geometry do not merely allow complex amplitudes; they force the admissible evolutions to be unitary on the DFT inner-product space.
The master certificate chain (T5–T8, shift period 8, eigenvalue $i$, no real root of $x^2+1$, complexification forced, DFT-8, Parseval, J phase invariance) ends here: unitary evolution is the recognition-theoretic stand-in for quantum time evolution. Downstream, OperatorCore re-exports the same structure as an abbrev for operator-level work. It does not yet construct a concrete generator or Schrödinger equation; it fixes the admissibility interface those constructions must satisfy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.