shift
plain-language theorem explainer
Re-export of the cyclic shift on eight-tick signals: advance the sample index by one step modulo 8. Anyone working with discrete time evolution, DFT modes, or the eight-tick octave cites this operator as the generator of the cycle. The declaration is a pure abbreviation with no proof content.
Claim. Write $T$ for the cyclic shift on eight-component signals $f:\mathbb{Z}/8\mathbb{Z}\to\mathbb{C}$ by $(Tf)(k)=f(k+1\bmod 8)$. This abbreviation names that operator in the operator-core module.
background
Recognition Science forces an eight-tick discrete clock (forcing chain T7: period $2^3$). Signals on that clock are maps from $\mathbb{Z}/8\mathbb{Z}$ into a value type (here complex amplitudes). The next-index map steps the reading head by one tick modulo 8.
The upstream definition states: the cyclic shift $T$ advances the reading index by one tick, $(Tf)(k)=f(k+1\bmod 8)$, and is the fundamental discrete time-evolution generator. A parallel occupation-shift appears in the eight-tick Weyl package (advance occupation by one tick), confirming the same clock structure in the quantum layer.
This module sits in Foundation.OperatorCore and packages complex-structure forcing around that eight-tick shift, its iterates, eigenvalues, and the length-8 DFT.
proof idea
No proof: the declaration is an abbreviation that aliases the foundation definition shift f k = f (nextIdx k). All mathematical content lives in that upstream def and in lemmas such as period-8 of the shift.
why it matters
The eight-tick shift is the discrete time generator underlying T7 (eight-tick octave) and feeds a wide fan-out: Noether time-translation on real trajectories, cost-algebra reciprocal identities, DFT mode norms, and the pulsar-period track.
Downstream, the pulsar one-statement theorem uses the canonical 8-tick recycling shift between normal and millisecond $\varphi$-ladder families, with bimodal ratio $\varphi^8>30$. The same operator seeds unitary evolution and mode-cost accounting in the complex-structure forcing stack. Without a named cyclic shift, the discrete clock and its spectral theory have no generator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.