MacroscopicShift_finite_sum
plain-language theorem explainer
Finite linear combinations of multi-site ledger states commute with the macroscopic recognition update: applying the update to a superposition equals the superposition of the updates. Gravity and ledger-superposition arguments cite this as the multi-site superposition principle. The proof is Finset induction, reducing each insert step to additivity and scalar homogeneity of the macroscopic shift.
Claim. Let $s$ be a finite index set, $c_\alpha\in\mathbb{C}$ amplitudes, and $\Psi_\alpha$ macroscopic ledger configurations (finite $\iota$-fold tensor products of single-site eight-tick signals). Then the macroscopic recognition update $\widehat{R}_{\mathrm{macro}}$ satisfies $\widehat{R}_{\mathrm{macro}}\bigl(\sum_{\alpha\in s} c_\alpha\,\Psi_\alpha\bigr)=\sum_{\alpha\in s} c_\alpha\,\widehat{R}_{\mathrm{macro}}(\Psi_\alpha)$.
background
Track 2.A of Gravity IV upgrades the macroscopic ledger Hilbert carrier from a conditional claim to a structural theorem. For a finite site index $\iota$, the carrier is the $\iota$-fold Pi-tensor product over $\mathbb{C}$ of single-site Signal8 factors (the eight-tick recognition register). The single-site recognition update is the $\mathbb{C}$-linearization of the cyclic shift on that register; the macroscopic update is the factor-wise Pi-tensor map of that linear map, hence automatically $\mathbb{C}$-linear and acting on pure tensors by shifting each factor.
Paper IV already has unconditional ledger superposition at one site. Multi-site configurations need the same statement at tensor-product level: superpositions of ledger states remain physical and are preserved by recognition. This lemma is the finite-sum clause of that package (clause 5 of the master certificate): the update commutes with finite linear combinations of multi-site configurations.
Upstream, additivity and scalar homogeneity of the macroscopic shift are already available as map lemmas; the pure-tensor action and single-site linearity sit one layer below in the same module and in LedgerSuperposition.
proof idea
Classical Finset induction on the support $s$. The empty-sum case is simp (both sides zero). On insert of an index $\alpha$ outside $s$, rewrite both sides by Finset.sum_insert, then apply additivity of the macroscopic shift, scalar homogeneity on the new term, and the induction hypothesis on the remainder. No new analytic content: the step is pure linearity of a $\mathbb{C}$-linear map under finite sums.
why it matters
This is the explicit multi-site superposition principle for macroscopic ledger configurations. It feeds the master certificate macroscopicLedgerTheorem, whose fifth clause (finite_superposition) is exactly this commutation with finite linear combinations. Together with single-site linearity, pure-tensor factor-wise action, additivity, and scalar homogeneity, it discharges Track 2.A: the macroscopic ledger Hilbert carrier is a structural theorem (zero sorry, zero RS-internal axiom), not a definition or conditional claim.
In the broader Recognition framework this is the gravity-side lift of single-site ledger superposition to an arbitrary finite site set, so multi-site recognition updates stay inside the linear Hilbert carrier. It does not itself force $D=3$ or the eight-tick period (those sit in the T0–T8 forcing chain); it consumes the eight-tick Signal8 carrier and the linearized cyclic shift as given inputs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.