schrodinger_dft_decomposition
plain-language theorem explainer
On the eight-tick carrier, any state expanded in the DFT-8 eigenbasis evolves under one cyclic shift by multiplying each mode by the Schrödinger phase exp(-i E_k τ₀/ℏ). Anyone deriving discrete-to-continuum quantum evolution from the recognition octave cites this superposition identity. The proof is linearity of the shift plus the per-mode discrete Schrödinger lemma.
Claim. Let $c:\mathrm{Fin}\,8\to\mathbb{C}$ and write $\psi=\sum_k c_k\,u_k$ with $u_k$ the DFT-8 modes. One tick of the cyclic shift satisfies $\widehat{R}\psi=\sum_k e^{-i E_k\tau_0/\hbar}\,c_k\,u_k$, where $E_k$ is the quarter-turn energy of mode $k$, $\tau_0$ the fundamental tick, and $\hbar$ the RS-native action quantum.
background
The module derives the Schrödinger equation from the Recognition 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 cyclic shift on that carrier.
Complex-structure forcing selects the DFT-8 basis as the unitary eigenbasis of the shift: each mode $u_k$ has eigenvalue $\omega_8^k=\exp(-i\pi k/4)$. Matching $\omega_8^k=\exp(-i E_k\tau_0/\hbar)$ defines the recognition-Hamiltonian eigenvalues $E_k=\hbar\cdot\pi k/(4\tau_0)$ (quarter-turn energy). In RS-native units $\hbar=\varphi^{-5}$ and $\tau_0=1$.
Upstream, the per-mode identity already states that cyclic shift on a scaled eigenmode multiplies by exactly that Schrödinger phase factor. The present result extends that identity from pure modes to arbitrary linear combinations.
proof idea
First prove that cyclic shift commutes with finite sums: induct on the Finset of modes, using that the shift preserves addition (cyclic_shift_add) and the empty-sum base case. Rewrite the left-hand side as $\sum_k$ cyclic_shift$(c_k\bullet u_k)$. Then Finset.sum_congr reduces each summand to the already-proved discrete_schrodinger_eigenmode lemma applied to coefficient $c_k$ and mode index $k$. No new spectral work is required; the argument is pure linearity plus the eigenmode flow.
why it matters
This is step 4 of the module's five-step derivation: the exact discrete Schrödinger equation on a general state in Signal8, obtained by linear superposition of the eigenmode flows. It sits on T7 (eight-tick octave), the DFT-8 diagonalization of the recognition operator, and the identification $\omega_8^k=\exp(-i E_k\tau_0/\hbar)$ that extracts the recognition Hamiltonian.
Together with Hermitianness and nonnegativity of the quarter-turn energies, it supplies the full one-tick unitary $e^{-i\widehat{H}\tau_0/\hbar}$ on the discrete carrier before the continuum Taylor remainder (step 5) recovers $i\hbar\partial_t\psi=\widehat{H}_{\mathrm{RS}}\psi$. No downstream dependents are recorded yet; the declaration is the general-state closure named in the module table as linear superposition of the discrete flow.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.