eigenmode_evolution_exact
plain-language theorem explainer
The one-tick recognition operator multiplies each DFT-8 eigenmode by the pure phase ω₈^k = exp(-iπk/4). Anyone extracting the discrete Schrödinger flow on the eight-tick carrier cites this spectral identity. The proof is a one-line term wrapper of the DFT diagonalization lemma for the cyclic shift.
Claim. For every mode index $k \in \{0,\ldots,7\}$, the cyclic shift of the $k$-th DFT-8 basis vector equals $\omega_8^{k}$ times that same vector, where $\omega_8 = \exp(-i\pi/4)$ is the primitive eighth root of unity used by the DFT-8 basis.
background
This module derives the Schrödinger equation from the Recognition Science forcing chain. T7 forces the eight-tick period $2^D$ with $D=3$, so the carrier is $\mathrm{Signal8} = \mathrm{Fin},8 \to \mathbb{C}$ and the one-tick recognition operator acts as the cyclic shift: $(Rv)(t) = v((t+1)\bmod 8)$.
The DFT-8 modes are the unique (up to phase and permutation) unitary basis that diagonalizes that shift. Mode $k$ is the function $t \mapsto \omega_8^{tk}/\sqrt{8}$. The primitive root here is $\omega_8 = \exp(-i\pi/4)$, so $\omega_8^8 = 1$.
Upstream, dft8_shift_eigenvector already records the eigenvector identity: cyclic shift on mode $k$ multiplies by $\omega_8^k$. The present declaration re-exports that fact under the Schrödinger-derivation namespace as the first certified step of the chain.
proof idea
One-line term proof: apply the upstream DFT lemma dft8_shift_eigenvector at the given mode index $k$. No extra algebra is performed here; the equality is exactly the statement that DFT diagonalizes the cyclic shift on $\mathbb{C}^8$.
why it matters
This is row 1 of the module's certified table: the exact one-tick eigenmode equation $\hat{R}\psi_k = \omega_8^k\psi_k$. It is the spectral identity that lets later steps read $\omega_8^k = \exp(-i E_k\tau_0/\hbar)$ and recover discrete Schrödinger flow on each mode.
Downstream it is consumed by the scaled linearity lemma (same eigenvalue on $c\cdot\psi_k$), by the inhabited SchrodingerEquationCert bundle, and by the forcing-chain bridge t7_t8_to_canonical_schrodinger_bridge_holds, which packages T7 (eight-tick octave) and T8 ($D=3$) into the canonical Schrödinger bridge. Without this eigenvector fact, Hamiltonian extraction and the discrete-to-continuum passage have no eigenbasis to act on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.