shiftLinear_apply
plain-language theorem explainer
On eight-tick complex signals, the bare one-tick linear propagation operator acts exactly by cyclic shift of the time index. Anyone proving invariance of the quarter-turn core or simplifying recognition-operator identities will cite this. The equality is definitional: the linear map is built with that shift as its underlying function, so the proof is reflexivity.
Claim. For every eight-tick complex signal $f$, the bare one-tick linear propagation operator applied to $f$ equals the cyclic shift of $f$ (indices advanced by one modulo $8$).
background
The ambient setting is the analytic eight-tick recognition operator on Signal8, the type of maps $\mathrm{Fin},8\to\mathbb{C}$ imported from the complex-structure forcing layer. This is the RS-native carrier for one octave of discrete time (forcing landmark T7: period $2^3$).
The cyclic shift sends $v$ to $t\mapsto v((t+1)\bmod 8)$. The bare one-tick propagation operator is the $\mathbb{C}$-linear map whose underlying function is exactly that shift; additivity and homogeneity are checked componentwise in its definition.
This simp lemma is the apply-form of that definition: evaluating the linear map recovers the pointwise cyclic shift. Downstream proofs often rewrite through the linear map so they can use submodule machinery.
proof idea
Term-mode reflexivity. The linear map is defined with toFun equal to the cyclic shift, so the stated equality holds by definitional reduction (rfl). No lemmas are invoked.
why it matters
Feeds the invariance theorem that the odd-mode (quarter-turn) core is closed under one-tick propagation: that proof immediately rewrites the cyclic shift as the linear operator, then runs submodule span induction. Without the apply identity, the change-of-view step between the spectral shift and the linear recognition operator would be manual.
In the broader framework this sits inside the eight-tick octave (T7) and the analytic recognition operator that propagates ledger signals tick by tick. It is bookkeeping rather than a new physical claim, but it is the hinge that lets linear-algebra arguments talk about the same one-tick update used in the spectral DFT8 layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.