shiftLinear
plain-language theorem explainer
The one-tick cyclic shift on eight-component complex signals, packaged as a ℂ-linear map. Anyone building the recognition update (projector after shift) or proving odd-mode invariance under propagation cites this. Linearity is the standard check: additivity and scalar homogeneity reduce by simp to the pointwise mod-8 index shift.
Claim. The map sending an eight-tick complex signal $f$ to the cyclically advanced signal $(Sf)(t)=f(t+1\bmod 8)$ is a $\mathbb{C}$-linear operator $S:\mathbb{C}^{8}\to\mathbb{C}^{8}$.
background
In the Recognition Operator module the working state space is an eight-component complex signal (the analytic 8-tick carrier forced by the octave period). The bare one-tick advance on that carrier is the cyclic index shift: each sample moves to the next slot modulo 8.
That pointwise shift already exists in the spectral DFT-8 layer ("shifts indices by 1 mod 8") and is re-exported as a local abbreviation on the ledger side. Here it is promoted from a bare function to a bundled linear map so it can sit inside the operator algebra used by sector projectors and structured updates.
The surrounding file keeps a legacy ledger compatibility surface, but the canonical analytic object is this linear operator on the eight-tick signal.
proof idea
Definitional packaging, not a deep argument. The underlying function is the existing cyclic shift. Additivity is proved by introducing two signals, extensionality on the tick index, and simp unfolding the shift. Scalar homogeneity is the same pattern with a complex scalar. Both obligations are pure pointwise arithmetic on Fin 8.
why it matters
This is the bare one-tick propagation piece of the recognition operator. Downstream, the concrete recognition update is defined as sector-projector composed with this linear shift ("projector-after-shift"). The same map is the object in the theorem that the odd-mode (quarter-turn) core is invariant under one-tick propagation, via a change-of-view to the linear operator and span induction.
In the forcing chain this sits under T7: the eight-tick octave. Without a linear one-tick advance there is no clean composition with projectors, no Fourier-mode bookkeeping, and no invariance statements for the quarter-turn core that feed the complex-structure story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.