UnitaryEvolution
plain-language theorem explainer
Re-export of the admissible discrete evolution structure: operators on eight-mode signals that preserve the inner product and do not raise total J-mode cost. Anyone citing the complex-structure forcing chain uses this type for unitary eight-tick steps. The body is a pure abbreviation of the parent Foundation structure; no new mathematics is proved here.
Claim. An admissible evolution is an operator $U$ on eight-mode complex signals such that $\langle Uf, Ug \rangle = \langle f, g \rangle$ for all signals $f,g$, and the total mode cost satisfies $C(Uf) \le C(f)$ for every $f$. Together these are the discrete stand-in for unitarity under the Recognition $J$-cost.
background
The parent module builds a discrete complex structure on eight-tick signals (the Recognition octave period $2^3$). Signals are length-8 complex arrays; inner8 is their standard Hermitian product; the DFT/IDFT pair diagonalizes cyclic shifts. Mode costs are assembled from the complex $J$-cost $J_\mathbb{C}$ on Fourier amplitudes, and totalModeCost sums those costs over the eight modes.
An evolution operator is any map on such signals. Admissibility adds two axioms: exact preservation of inner8, and non-increase of total mode cost. The module doc frames these two conditions as the discrete meaning of unitarity: norm preservation plus recognition-cost minimization.
This OperatorCore file only re-exports that structure under a short local name so downstream OperatorCore lemmas can cite it without the long Foundation path.
proof idea
One-line abbreviation: the local name is definitionally equal to IndisputableMonolith.Foundation.ComplexStructureForcing.UnitaryEvolution. No tactics, no lemmas, no new fields.
why it matters
Sits in the complex-structure forcing stack that ties the eight-tick octave (forcing landmark T7) to a unitary discrete time step. Downstream material in the same Foundation module uses the structure as the admissible class of evolutions before the complete forcing chain (Part 7). The two axioms package the Recognition Composition Law's cost geometry with ordinary Hilbert-space unitarity on the eight-mode space, so later uniqueness or existence results can quantify over a single named type rather than repeating the pair of inequalities.
As a pure re-export it closes no open question by itself; it only stabilizes the API between OperatorCore and the parent ComplexStructureForcing development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.