MacroscopicShift_map_add
plain-language theorem explainer
The macroscopic recognition update preserves addition on multi-site ledger states: applying it to Ψ + Φ equals the sum of the updates. Gravity and ledger-superposition arguments cite this as the additive half of ℂ-linearity. The proof is a one-line wrapper on the LinearMap additivity built into PiTensorProduct.map.
Claim. For any finite site index set $\iota$ and any two macroscopic ledger states $\Psi,\Phi$ in the $\iota$-fold tensor product $\bigotimes_{i\in\iota}\mathrm{Signal}_8$ over $\mathbb{C}$, the macroscopic recognition update $\widehat{R}_{\mathrm{macro}}$ satisfies $\widehat{R}_{\mathrm{macro}}(\Psi+\Phi)=\widehat{R}_{\mathrm{macro}}(\Psi)+\widehat{R}_{\mathrm{macro}}(\Phi)$.
background
Track 2.A of Gravity IV upgrades the macroscopic ledger Hilbert carrier from a conditional claim to a structural theorem. For a finite indexing set $\iota$ of sites, the carrier is the $\iota$-fold PiTensorProduct over $\mathbb{C}$ of single-site Signal8 factors (the eight-tick octave carrier from the single-site ledger superposition module).
The macroscopic recognition update is defined as PiTensorProduct.map of the single-site cyclic-shift linear map on each factor. By construction that map is a $\mathbb{C}$-linear endomorphism of the tensor product. The single-site cyclic shift is already proved linear in LedgerSuperposition; the multi-site object inherits linearity from the universal property of the tensor product map.
This lemma isolates the additive half of that linearity. The companion scalar-multiplicativity statement completes the LinearMap package used by the finite-sum superposition principle.
proof idea
One-line wrapper: the declaration is definitionally a LinearMap (PiTensorProduct.map of cyclicShiftLinear on each factor), so Mathlib's LinearMap.map_add applies directly to the two arguments. No extra algebraic work; the additivity is the universal property restated at the theorem level.
why it matters
Paper IV's single-site Ledger Superposition theorem is unconditional; the macroscopic claim (multi-site ledger superpositions are physical and preserved by recognition) needs the same linearity at tensor-product level. This additivity feeds MacroscopicShift_finite_sum, which states that the update commutes with finite linear combinations of multi-site configurations, and is packaged into macroscopicLedgerTheorem as part of the verified Track 2.A interface.
In the Recognition framework this is structural scaffolding for gravity: the eight-tick Signal8 factor and its cyclic recognition update extend canonically and linearly to arbitrary finite site sets, so macroscopic ledger superpositions remain inside the carrier. It does not yet derive dynamics or the mass ladder; it closes the Hilbert-carrier linearity gap that Paper IV left conditional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.