cyclicShiftLinear_apply
plain-language theorem explainer
The ℂ-linear packaging of the one-tick recognition update on the eight-tick signal carrier agrees pointwise with the bare cyclic shift. Anyone simplifying single-site ledger updates or building the macroscopic tensor-product map will cite this simp bridge. The proof is pure reflexivity on the underlying function field.
Claim. For every eight-tick signal $\psi$, the $\mathbb{C}$-linear endomorphism that packages the one-tick recognition update evaluates to the same value as the bare cyclic shift of $\psi$.
background
Track 2.A of Gravity IV upgrades the macroscopic ledger Hilbert carrier from a conditional claim to a structural theorem. The single-site carrier is Signal8, the eight-tick analytic signal (identified with the foundation complex-structure forcing carrier). The one-tick recognition update on that carrier is the cyclic shift of the eight components.
That update is already known to be ℂ-linear (additivity and scalar homogeneity from the Schrödinger-derivation lemmas). The module packages it as an explicit linear endomorphism whose underlying function is the cyclic shift. The present lemma is the pointwise bridge between the linear-map object and that bare function.
The macroscopic construction then applies the linear map factor-wise via the universal property of the finite Pi tensor product over an arbitrary site index set, so pure tensors transform by cyclic-shifting each factor.
proof idea
One-line term proof by reflexivity. The linear endomorphism is defined with toFun equal to the cyclic shift, so applying the map is definitionally the bare update; rfl closes the equality. Marked @[simp] so downstream rewrites unfold the packaging automatically.
why it matters
This is a small but load-bearing simp fact in the single-site layer of Track 2.A. Paper IV's Theorem 1 (ledger superposition) is unconditional on one site; the macroscopic claim needs the recognition update as a genuine ℂ-linear endomorphism so that PiTensorProduct.map yields a linear multi-site update acting by cyclic shift on pure tensors. Without the pointwise agreement, simp and rewrite chains cannot move between the linear-map API and the spectral cyclic-shift lemmas.
It sits next to the additivity and scalar-homogeneity lemmas for the same packaging, and underwrites the macroscopic shift on the ι-fold tensor product of eight-tick carriers. Framework-wise it supports the eight-tick octave (T7) as the single-site period that is tensored up to macroscopic ledgers. No downstream dependents are recorded yet; the immediate consumers are the sibling macroscopic-shift lemmas in this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.