schrodinger_linear
plain-language theorem explainer
The one-tick recognition operator on eight-component complex signals is ℂ-linear: it sends a linear combination of two signals to the same combination of their images. Anyone extending the discrete Schrödinger flow from DFT-8 eigenmodes to general superpositions cites this. The proof is a three-rewrite chain from additivity and scalar homogeneity of the cyclic shift.
Claim. For any two signals $\psi,\phi:\mathrm{Fin}\,8\to\mathbb{C}$ and any $a,b\in\mathbb{C}$, the one-tick cyclic shift satisfies $\widehat{R}(a\psi+b\phi)=a\,\widehat{R}\psi+b\,\widehat{R}\phi$.
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}$. The one-tick recognition operator acts as cyclic shift on this carrier; T9 selects the DFT-8 basis that diagonalizes it.
On each eigenmode the shift multiplies by $\omega_8^k=\exp(-i\pi k/4)$, identified with the integrated Schrödinger phase $\exp(-i E_k\tau_0/\hbar)$ at energy $E_k=\hbar\cdot\pi k/(4\tau_0)$. Eigenmode evolution is therefore exact discrete Schrödinger flow. Extending that identity from pure modes to arbitrary states requires $\mathbb{C}$-linearity of the shift.
Upstream, cyclic_shift_smul gives homogeneity under scalar multiplication and cyclic_shift_add gives additivity; both are pointwise on $\mathrm{Fin},8\to\mathbb{C}$. The fundamental tick is $\tau_0=1$ in RS-native units.
proof idea
One-line tactic proof. Rewrite the left-hand side first by additivity of the cyclic shift, then apply scalar homogeneity twice (once for each coefficient). The resulting right-hand side is exactly $a\cdot\widehat{R}\psi+b\cdot\widehat{R}\phi$. No spectral facts or energy identities are used; only the two elementary linearity lemmas.
why it matters
Module table entry 6: linear superposition that upgrades eigenmode discrete Schrödinger flow to general states in $\mathrm{Signal8}$. Downstream, ledger_superposition_preserved is this statement repackaged for ledger language; schrodinger_equation_from_RS and the SchrodingerEquationCert package sit on the eigenmode side, while the forcing-chain bridge t7_t8_to_canonical_schrodinger_bridge_holds records the T7/T8 path to the canonical Schrödinger package. Gravity-side consumers (AmplitudeLinearForced, ledger superposition) treat this as the forced $\mathbb{C}$-linearity of the recognition update. Framework landmarks: T7 eight-tick octave and T8 $D=3$ fix the carrier on which linearity is stated; without it the discrete Schrödinger equation would stop at pure DFT modes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.