cyclic_shift_smul
plain-language theorem explainer
The one-tick cyclic shift on eight-component complex signals commutes with scalar multiplication: shifting c·v equals c times the shifted signal. Anyone proving ℂ-linearity of the recognition update (discrete Schrödinger flow, ledger superposition, or the LinearMap packaging) cites this. The proof is a one-line pointwise unfolding via function extensionality and the definition of Pi scalar action.
Claim. For every scalar $c \in \mathbb{C}$ and every eight-tick signal $v : \mathrm{Fin}\,8 \to \mathbb{C}$, the cyclic shift satisfies $\widehat{R}(c \cdot v) = c \cdot \widehat{R}(v)$, where $\widehat{R}$ advances the tick index by one modulo $8$.
background
The module derives the Schrödinger equation from the Recognition forcing chain. Step 1 uses T7 (the eight-tick octave, period $2^3$ with $D=3$) to fix the carrier $\mathrm{Signal8} = \mathrm{Fin},8 \to \mathbb{C}$. The one-tick recognition operator acts as cyclic shift on that carrier: $(\widehat{R} v)(t) = v((t+1)\bmod 8)$.
Upstream, Spectral.DFT8 defines that shift, and MacroscopicLedger re-exports it as the local one-tick update on ledger signals. Scalar homogeneity is the first half of $\mathbb{C}$-linearity needed before eigenmode scaling and superposition can be stated; additivity is the sibling fact.
In the five-step derivation, linearity lets the exact one-tick eigenmode law $R\psi_k = \omega_8^k \psi_k$ extend from DFT-8 modes to arbitrary linear combinations, which is the discrete Schrödinger equation on general states.
proof idea
Term-mode proof by pointwise equality. Apply function extensionality on the tick index $t$, then simplify: unfold the definition of cyclic shift (index plus one mod 8) and the pointwise scalar action on Fin 8 → ℂ. Both sides reduce to $c \cdot v((t+1)\bmod 8)$, so they match. No external lemmas beyond the definition and Pi.smul_apply.
why it matters
This is the scalar half of recognition-update linearity in the Schrödinger derivation (module status: theorem, zero sorry). Downstream, eigenmode_evolution_scaled rewrites through it to get $\widehat{R}(c\cdot\mathrm{dft8_mode},k)=\omega_8^k\cdot(c\cdot\mathrm{dft8_mode},k)$. The full discrete Schrödinger law schrodinger_linear chains additivity with two applications of this fact so $\widehat{R}(a\psi+b\phi)=a\widehat{R}\psi+b\widehat{R}\phi$.
Gravity packaging uses it twice: cyclicShiftLinear installs map_smul' from this theorem, and ledger_superposition_finite_sum (T1.i) needs scalar homogeneity so the recognition update commutes with finite ledger superpositions $\sum c_\alpha |L_\alpha\rangle$. Framework landmark: T7 eight-tick carrier; without scalar linearity the step-4 extension from eigenmodes to general $\psi\in\mathrm{Signal8}$ fails.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.