cyclicShiftLinear_map_smul
plain-language theorem explainer
Scalar homogeneity of the single-site recognition update on the eight-tick signal carrier: scaling the input by a complex constant scales the output the same way. Cited when lifting ℂ-linearity from one site to the multi-site PiTensorProduct ledger. Proof is a one-line appeal to the LinearMap scalar axiom already built into the packaged endomorphism.
Claim. For every $c \in \mathbb{C}$ and every eight-tick signal $\psi$, the linearized cyclic recognition update $T$ satisfies $T(c \cdot \psi) = c \cdot T(\psi)$.
background
Track 2.A of Gravity IV upgrades the macroscopic ledger Hilbert carrier from a paper-level conditional claim to a structural Lean theorem. The single-site carrier is Signal8, the eight-tick analytic signal space forced by the octave structure (T7). On that space the one-tick recognition update is the cyclic shift of the eight components.
That shift is packaged as a genuine $\mathbb{C}$-linear endomorphism: additivity and scalar homogeneity come from the Schrödinger-derivation lemmas cyclic_shift_add and cyclic_shift_smul. The present statement is exactly the scalar half of that linearity, exposed as a named theorem so downstream tensor-product constructions can cite it without unpacking the LinearMap record.
The macroscopic object is then the finite PiTensorProduct of Signal8 factors over an arbitrary finite site index set; factor-wise application of the linearized shift yields the multi-site recognition update automatically $\mathbb{C}$-linear by the universal property of PiTensorProduct.map.
proof idea
One-line term proof. The definition of the linearized cyclic shift already installs map_smul' from the foundation lemma cyclic_shift_smul. The theorem simply projects that field: apply LinearMap.map_smul of the packaged endomorphism to the given scalar and signal. No extra algebra.
why it matters
Paper IV's single-site Ledger Superposition theorem is already unconditional; the macroscopic claim (multi-site superpositions remain physical and are preserved by recognition) needs the same linearity at tensor-product level. This lemma is the scalar half of that single-site linearity, paired with the sibling additivity statement, and is the local ingredient that lets MacroscopicShift inherit map_smul via PiTensorProduct.map.
It sits inside the eight-tick octave forced at T7: the carrier is eight-dimensional precisely because the recognition clock has period $2^3$. Closing Track 2.A converts the multi-site superposition claim from CONDITIONAL THEOREM to STRUCTURAL THEOREM (0 sorry, 0 RS-internal axiom). No further downstream theorems currently depend on this name alone, but the sibling macroscopic shift lemmas reuse the same pattern.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.