cyclic_shift
plain-language theorem explainer
Local alias for the one-tick cyclic recognition update on the eight-component complex signal carrier. Gravity and recognition-operator developments cite it so multi-site ledger maps can reuse the single-site shift without re-importing the spectral definition. The body is a pure abbreviation redirect to the spectral cyclic shift.
Claim. Write $\mathrm{cyclic\_shift}:\mathrm{Signal}_8\to\mathrm{Signal}_8$ for the one-tick recognition update on the eight-tick analytic signal carrier (identified with the canonical complex eight-mode space). This is only a local name for the spectral cyclic shift already defined upstream.
background
Track 2.A of Gravity IV builds the macroscopic ledger Hilbert carrier: for a finite index set of sites, the carrier is the $\mathbb{C}$-tensor product of single-site eight-tick signal factors. Each factor carries the one-tick recognition update, which must be $\mathbb{C}$-linear so the product map is well-defined and linear on pure tensors.
The eight-tick signal is the analytic carrier forced by the octave structure (period $2^3$). Upstream, additivity and scalar homogeneity of the shift are already proved in the Schrödinger derivation (cyclic_shift_add, cyclic_shift_smul). Those facts license packaging the update as a linear endomorphism and then lifting it factor-wise via PiTensorProduct.map.
This module only needs a short local name for that single-site update so the macroscopic construction and its linearity lemmas stay readable.
proof idea
No proof content: the declaration is an abbreviation whose right-hand side is the spectral cyclic shift. Linearity is not re-proved here; sibling packaging later quotes the upstream additivity and scalar-homogeneity lemmas from the Schrödinger derivation when building the $\mathbb{C}$-linear endomorphism.
why it matters
Everything multi-site in this track starts from the single-site one-tick update. Downstream, the recognition operator iterates the shift, proves iterates preserve addition and scalar multiplication, and shows every DFT mode remains an eigenvector under iteration. Gap-weight projection defines the discrete one-step difference $(S-I)v$ and recovers the $\sin^2(\pi k/8)$ energy spectrum of eight-tick modes from the shift eigenvalues.
In the Recognition framework this is the concrete one-tick step on the eight-tick octave (forcing landmark T7). Macroscopic ledger superposition (Paper IV, Track 2.A) needs that step as a linear map on each tensor factor so multi-site superpositions stay physical under recognition. The abbreviation keeps Gravity IV aligned with the spectral and recognition-operator stacks without duplicating the definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.