eigenmode_evolution_scaled
plain-language theorem explainer
One-tick cyclic shift acts on any complex multiple of a DFT-8 mode by the same eigenvalue ω₈^k. Anyone deriving the discrete Schrödinger flow or unitarity on Signal8 cites this linearity step. The proof is a three-rewrite chain: scalar-homogeneity of the shift, the unscaled eigenmode equation, then commutativity of scalar multiplication.
Claim. For every mode index $k \in \{0,\ldots,7\}$ and every $c \in \mathbb{C}$, the one-tick cyclic shift satisfies $\widehat{R}(c\,\psi_k)=\omega_8^{k}\,(c\,\psi_k)$, where $\psi_k$ is the $k$-th DFT-8 eigenmode and $\omega_8=e^{i\pi/4}$ is the primitive eighth root of unity.
background
This module derives the Schrödinger equation from the Recognition forcing chain. T7 forces the eight-tick carrier Signal8 = Fin 8 → ℂ, on which the one-tick recognition operator acts as cyclic shift. Complex-structure forcing then selects the DFT-8 basis: each mode ψ_k is an eigenvector of that shift with eigenvalue ω₈^k = exp(-iπk/4) (equivalently exp(iπk/4) depending on root convention; here ω₈ = exp(2πi/8)).
The unscaled eigenmode equation already states R̂ ψ_k = ω₈^k ψ_k. The present result extends that identity to arbitrary complex multiples c · ψ_k, which is the linearity needed before superposing modes or reading off Hamiltonian eigenvalues. Upstream constants fix τ₀ = 1 (one tick) and supply the phase ladder kπ/4 used later to identify E_k.
proof idea
Three rewrites, no case splits. First apply scalar-homogeneity of the cyclic shift (cyclic_shift_smul): R̂(c · ψ_k) = c · R̂ ψ_k. Then replace R̂ ψ_k by the exact eigenmode identity (eigenmode_evolution_exact): c · (ω₈^k · ψ_k). Finally commute the two complex scalars (smul_comm) to obtain ω₈^k · (c · ψ_k). The goal is then definitionally closed.
why it matters
This is the linearity bridge between the bare eigenmode equation and the discrete Schrödinger statement on modes. Downstream, discrete_schrodinger_eigenmode rewrites through this lemma then through omega8_pow_eq_evolution_factor to obtain ψ(τ₀) = exp(-i E_k τ₀/ℏ) · ψ(0) with the RS-native quanta ℏ = φ^{-5}, τ₀ = 1. The same rewrite opens eigenmode_norm_preserved, which proves one-tick unitarity on each mode because |ω₈^k| = 1.
In the module's five-step plan this sits inside step 4 (exact discrete Schrödinger on eigenmodes), after T7 → Signal8 and T9 → DFT-8 diagonalization, and before continuum Taylor recovery. It does not itself extract E_k; that identification is the next link in the chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.