cyclicShiftLinear
plain-language theorem explainer
The one-tick recognition update on the eight-component signal carrier is packaged as a complex-linear endomorphism. Anyone citing the macroscopic ledger Hilbert carrier or multi-site recognition needs this map as the single-site factor. Construction is a LinearMap whose additivity and scalar homogeneity are discharged by the existing cyclic-shift linearity lemmas from the Schrödinger derivation module.
Claim. The cyclic index shift on eight-tick signals is a $\mathbb{C}$-linear endomorphism $S:\mathrm{Signal}_8\to_\ell\mathrm{Signal}_8$, acting by $S(v)_t=v_{(t+1)\bmod 8}$. Additivity and $\mathbb{C}$-homogeneity are those of the pointwise cyclic shift.
background
In Recognition Science the single-site analytic carrier is an eight-component complex signal (the eight-tick octave, forcing step T7). The one-tick recognition update is the cyclic index shift $v_t\mapsto v_{(t+1)\bmod 8}$ on that carrier.
This module (Gravity IV, Track 2.A) upgrades the macroscopic ledger Hilbert carrier from a conditional claim to a structural theorem: the recognition update must extend $\mathbb{C}$-linearly from one site to a finite tensor product over an arbitrary finite index set of sites. The local abbreviation for the carrier is the canonical eight-tick type from ComplexStructureForcing; the local cyclic shift is the spectral DFT8 shift.
Upstream, the Schrödinger-derivation lemmas already record that the pointwise cyclic shift is additive and homogeneous over $\mathbb{C}$ (proved by funext and simplification of the Pi action). Those two facts are exactly the structure fields a Mathlib linear map needs.
proof idea
The definition builds a LinearMap whose underlying function is the cyclic shift. The two structure obligations map_add' and map_smul' are filled by direct application of the upstream theorems that the cyclic shift is additive and $\mathbb{C}$-homogeneous. No new algebra: it is a packaging of existing pointwise linearity into Mathlib's linear-map type so the map can be fed to tensor-product combinators.
why it matters
Track 2.A of Paper IV needs a $\mathbb{C}$-linear single-site update so that the finite Pi-tensor-product map can lift it factor-wise to the macroscopic ledger $\bigotimes_{i\in\iota}\mathrm{Signal}_8$. Downstream, the certificate structure for the macroscopic ledger theorem lists single-site linearity as clause (1), and the verifying construction discharges that clause from this map's additivity and scalar homogeneity. Simp lemmas and explicit add/smul wrappers sit immediately on top of it; the macroscopic shift and its finite-sum forms consume it as the factor map. The eight-tick period (T7) fixes the carrier dimension. Without this linear packaging the multi-site recognition update would remain conditional rather than structural.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.