MacroscopicShift_tprod
plain-language theorem explainer
On a pure multi-site tensor state, the macroscopic recognition update acts factorwise: each site is advanced by one tick of the cyclic shift. Gravity and ledger-superposition arguments cite this to pass from single-site Signal8 dynamics to finite tensor products. The proof unfolds the map definition and applies the universal property of PiTensorProduct.map on pure tensors.
Claim. For any finite index set of sites and any family of single-site eight-tick signals $\psi_i$, the macroscopic recognition update satisfies $\widehat{R}_{\mathrm{macro}}\bigl(\bigotimes_i \psi_i\bigr) = \bigotimes_i \widehat{R}(\psi_i)$, where $\widehat{R}$ is the one-tick cyclic shift on each factor.
background
Track 2.A of Gravity IV upgrades the macroscopic ledger Hilbert carrier from a paper-level conditional claim to a structural Lean theorem. For a finite site set $\iota$, the carrier is the $\iota$-fold complex Pi-tensor product of single-site Signal8 factors (the eight-tick analytic signal carrier forced by the octave structure).
The one-tick recognition update on each factor is the cyclic shift on Signal8, already linearized as a $\mathbb{C}$-linear map in LedgerSuperposition. The macroscopic update is defined as the factorwise Pi-tensor product of those linear maps, so it is $\mathbb{C}$-linear by construction.
This lemma records the pure-tensor action that the universal property of PiTensorProduct.map guarantees: the multi-site update does not mix sites on elementary product configurations.
proof idea
Short term-mode proof. Unfold the definition of the macroscopic update (Pi-tensor product of the single-site cyclic-shift linear maps). Rewrite with PiTensorProduct.map_tprod, which states that the mapped pure tensor is the pure tensor of the images. The remaining equality is definitional (rfl).
why it matters
Paper IV's single-site Ledger Superposition theorem is already unconditional; the multi-site claim needs the same statement at tensor-product level. This pure-tensor identity is the computational core of that upgrade and feeds macroscopicLedgerTheorem, which packages linearity and superposition preservation for the macroscopic carrier.
In the Recognition framework it connects the eight-tick octave (T7) single-site dynamics to finite multi-site ledgers without extra axioms. It does not yet address continuum limits or gravitational field equations; it only secures that recognition updates remain product-preserving on elementary multi-site states, which is the structural prerequisite for macroscopic ledger superposition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.