schrodinger_difference_eigenmode
plain-language theorem explainer
On each DFT-8 eigenmode, the one-tick increment equals the integrated Schrödinger phase factor minus one, acting on the starting state. Anyone deriving a finite-difference form of discrete Schrödinger evolution from the eight-tick carrier would cite this. The proof rewrites by the multiplicative eigenmode flow, then factors the scalar via sub_smul.
Claim. For every mode index $k\in\{0,\ldots,7\}$ and amplitude $c\in\mathbb{C}$, if $\psi=c\cdot u_k$ with $u_k$ the $k$-th DFT-8 mode, then $\hat R\psi-\psi=\bigl(\exp(-i E_k\tau_0/\hbar)-1\bigr)\psi$, where $\hat R$ is the one-tick cyclic shift and $E_k$ is the quarter-turn energy of mode $k$.
background
This module derives the Schrödinger equation from the Recognition forcing chain. T7 forces the eight-tick carrier Signal8 = Fin 8 → ℂ with one-tick operator the cyclic shift. The DFT-8 modes diagonalize that shift: each mode $u_k$ is an eigenvector with eigenvalue $\omega_8^k=\exp(-i\pi k/4)$.
Identifying $\omega_8^k=\exp(-i E_k\tau_0/\hbar)$ extracts the recognition-Hamiltonian eigenvalues $E_k=\hbar\cdot\pi k/(4\tau_0)$ (the quarter-turn energies). In RS-native units $\hbar=\varphi^{-5}$ and $\tau_0=1$ (one tick). The sibling result discrete_schrodinger_eigenmode already states the multiplicative one-tick flow $\hat R(c\cdot u_k)=\exp(-i E_k\tau_0/\hbar),(c\cdot u_k)$.
The present statement is the equivalent difference form: the one-tick increment equals that phase factor minus the identity, applied to the same eigenmode state.
proof idea
Short rewrite proof. First apply discrete_schrodinger_eigenmode to replace the cyclic shift of $c\cdot u_k$ by the scalar $\exp(-i E_k\tau_0/\hbar)$ times that vector. The goal becomes a pure scalar identity on the left-hand side. Then sub_smul and one_smul rewrite $(\alpha\cdot v)-v$ as $(\alpha-1)\cdot v$, which is exactly the claimed difference form.
why it matters
Fills the difference-form companion to step 4 of the module program (discrete Schrödinger on eigenmodes). The multiplicative flow is the integrated Schrödinger step $\psi(\tau_0)=e^{-iE_k\tau_0/\hbar}\psi(0)$; subtracting the identity yields the finite-difference version used when one wants increments rather than absolute evolved states.
It sits on the T7 eight-tick octave and the DFT-8 diagonalization of the recognition operator, with energies read from matching $\omega_8^k$ to the Schrödinger phase. Hermitian structure and nonnegativity of $E_k$ are handled by sibling lemmas on quarter-turn energy. No downstream uses are recorded yet; the natural consumers are continuum/Taylor remainder arguments and any linear superposition that needs an increment form before extending off the eigenbasis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.