shift
plain-language theorem explainer
Occupation shift on the eight-tick cycle: for a complex amplitude ψ on ℤ/8ℤ, (Sψ)(k)=ψ(k−1), advancing occupation by one recognition tick. Anyone citing the finite Heisenberg–Weyl pair (shift, clock) or the eight-tick Weyl relation uses this operator. The body is a one-line function definition, not a proved identity.
Claim. Define the occupation shift $S$ on complex amplitudes over the eight-tick cycle by $(S\psi)(k)=\psi(k-1)$ for $\psi:\mathbb{Z}/8\mathbb{Z}\to\mathbb{C}$ and $k\in\mathbb{Z}/8\mathbb{Z}$. Equivalently, $S$ advances the occupation label by one tick on the cycle.
background
The module develops the eight-tick Weyl relation as the recognition-first root of canonical non-commutativity. On the cycle $\mathbb{Z}/8\mathbb{Z}$, occupation and cost-rate are realized as the shift and clock operators of the finite Heisenberg–Weyl group; they satisfy $\mathrm{clock}\circ\mathrm{shift}=\omega,(\mathrm{shift}\circ\mathrm{clock})$ with $\omega$ a primitive eighth root of unity, so they do not commute. Conventional QM postulates $[x,p]=i\hbar$; here non-commutativity is the cyclic recognition structure (T7: eight-tick octave, period $2^3$).
The fundamental time quantum is the tick $\tau_0=1$ in RS-native units; one octave is eight ticks. An upstream cyclic shift on eight-slot signals advances the reading index by one tick and is described as the discrete time-evolution generator. The present operator is the matching occupation shift on complex amplitudes $\mathbb{Z}/8\mathbb{Z}\to\mathbb{C}$, paired with the cost-rate clock (phase by $\omega^k$). Continuum $[x,p]=i\hbar$ and the magnitude $\hbar=\varphi^{-5}$ remain open outside this file.
proof idea
Definition only: $S$ is introduced by the lambda $k\mapsto\psi(k-1)$ on $\mathrm{ZMod},8\to\mathbb{C}$. No lemmas, tactics, or algebraic obligations; subtraction is the ring operation in $\mathbb{Z}/8\mathbb{Z}$. Sibling facts ($\omega^8=1$, $\omega\neq 1$, the Weyl relation) are proved elsewhere and consume this operator as data.
why it matters
This is one generator of the finite Heisenberg–Weyl pair that the module uses to derive canonical non-commutativity from the eight-tick recognition cycle rather than postulate it. It sits under the T7 eight-tick octave landmark and feeds the Weyl relation and the canonical non-commutativity statement in the same module.
Downstream, the same shift vocabulary appears in Noether time translation on trajectories, cost-algebra reciprocal identities, DFT-8 mode norms, and the pulsar-period-from-rung track (recycling rung shift of eight ticks between normal and millisecond families, bimodal ratio $\varphi^8$). The continuum limit $[x,p]=i\hbar$ and tying $\hbar=\varphi^{-5}$ through the J-cost quantum are explicitly open (node D6); this definition only supplies the discrete occupation half of the braiding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.