cyclicShiftLinear_map_add
plain-language theorem explainer
The single-site recognition update on the eight-tick signal carrier is additive: the cyclic shift of a sum equals the sum of the shifted signals. Gravity and ledger-superposition arguments cite this when packaging the update as a ℂ-linear map before lifting to multi-site tensor products. The proof is a one-line wrapper on the LinearMap additivity field of that packaged endomorphism.
Claim. For any two eight-tick signals $\psi,\varphi$, the $\mathbb{C}$-linear cyclic recognition update $L$ satisfies $L(\psi+\varphi)=L(\psi)+L(\varphi)$.
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 space forced by the octave structure (period $2^3$). The one-tick recognition update on that carrier is the cyclic shift of the eight components.
That update is packaged as a ℂ-linear endomorphism of Signal8, with additivity and scalar homogeneity taken from the Schrödinger-derivation lemmas on the cyclic shift. The present statement is exactly the additivity half of that packaging: the endomorphism applied to a sum equals the sum of the images.
The module then lifts the same map factor-wise through PiTensorProduct.map so that multi-site pure tensors transform by applying the cyclic shift on each factor. Additivity at the single-site level is the first ingredient needed for that lift to be linear.
proof idea
One-line wrapper. The packaged endomorphism already stores additivity in its map_add' field (filled by the foundation lemma that the bare cyclic shift preserves sums). The proof simply applies that field to the two signals.
why it matters
Paper IV's single-site Ledger Superposition theorem is already unconditional; the macroscopic claim needs the same linearity at the tensor-product level. This lemma records the additive half of the single-site linear packaging that the macroscopic construction consumes when it builds the factor-wise recognition update.
It sits next to the matching scalar-homogeneity statement and feeds the definitions of the macroscopic shift on pure tensors. In the forcing chain it rests on the eight-tick octave (T7): the carrier is eight-dimensional precisely because the recognition clock has period $2^3$. No downstream theorem currently names this wrapper directly; its role is structural bookkeeping inside the Track 2.A discharge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.