SigmaLayer/LocalLuders: the local-measurement Lüders map and marginal invariance (brick 1)

Category: dynamical measurement — dynamical no-signalling (A6, dynamical form), brick 1 of the recorded route: a local measurement on a composite is a block-degenerate measurement.

A measurement of the B factor of ℂ^{nA} ⊗ ℂ^{nB} in the computational basis acts by the local projectors Pⱼ = 1_A ⊗ |fⱼ⟩⟨fⱼ| — here in coordinate form (localProjB), with no Kronecker plumbing, exactly as OnticMarginals handles local unitaries. The projectors are idempotent, they resolve the identity (sum_localProjB), and their weights resolve the norm (sum_normSq_localProjB — the Born weights of the B-outcomes).

★ The marginal-invariance identity (reduceA_localLuders_mixture): for every composite preparation, the Born-weighted mixture of the post-measurement A-marginals equals the pre-measurement A-marginal:

∑ⱼ pⱼ · reduceA [Pⱼ v] = reduceA [v], pⱼ = ‖Pⱼv‖²/‖v‖².

This is the statics core of dynamical no-signalling: whatever B's apparatus does — and the corpus's degenerate-Lüders machinery realises exactly this update dynamically — the A side's density matrix, hence every A-side measurement statistic, is unchanged unless the outcome is communicated. The unnormalised form (traceRight_sum_vecOuter_localProjB) is a two-line entrywise computation: tracing out B collapses the projector sum before it can be seen.

⚠️ Honest scope. (2026-08-04: the propagator arrived in brick 2 — reduceA_blockLuders_mixture, SigmaLayer/LocalBlockBridge.lean; the sentence below scopes THIS module and stays true of it.) This brick is statics: the Lüders mixture is written down, not yet produced by a propagator. Brick 2 wires it to the dynamical layer — the local B-block structure b = snd under the Fin (nA·nB) ≃ Fin nA × Fin nB index bridge feeds BlockLudersObligation, whose join witness (joinWitness_blockLuders) supplies the ψ-dependent post-states dynamically; brick 3 is the eraser process (mark, then erase, as two sequential measurements). Zero-weight outcomes are handled honestly: the dite branch is multiplied by a vanishing weight, no positivity hypothesis is smuggled in.

References

specs/BACKLOG.md (the dynamical no-signalling + eraser row); specs/future-work.md; specs/reconstruction-status.md §2 (A6). Reused corpus API: reduceA/rayDensity (SigmaLayer/OnticMarginals.lean), traceRight + linearity (Mathlib/LinearAlgebra/Matrix/PartialTrace.lean staging); the operational-statics counterparts are csd_no_communication (Empirical/CSD/NoCommunication.lean) and singlet_hasNoSignalling (SigmaLayer/CompositeAdapters.lean).

The local projectors

noncomputable def CSD.RecordLayer.localProjB {nA nB : ℕ} (j : Fin nB) (v : EuclideanSpace ℂ (Fin nA × Fin nB)) : EuclideanSpace ℂ (Fin nA × Fin nB)

The local B-projector for outcome j: (Pⱼ v)(a, k) = v(a, k) if k = j, else 0 — the coordinate form of 1_A ⊗ |fⱼ⟩⟨fⱼ|.

Equations

• CSD.RecordLayer.localProjB j v = WithLp.toLp 2 fun (ak : Fin nA × Fin nB) => if ak.2 = j then v.ofLp ak else 0

@[simp]

theorem CSD.RecordLayer.localProjB_apply {nA nB : ℕ} (j : Fin nB) (v : EuclideanSpace ℂ (Fin nA × Fin nB)) (ak : Fin nA × Fin nB) : (localProjB j v).ofLp ak = if ak.2 = j then v.ofLp ak else 0

theorem CSD.RecordLayer.localProjB_idem {nA nB : ℕ} (j : Fin nB) (v : EuclideanSpace ℂ (Fin nA × Fin nB)) : localProjB j (localProjB j v) = localProjB j v

theorem CSD.RecordLayer.sum_localProjB {nA nB : ℕ} (v : EuclideanSpace ℂ (Fin nA × Fin nB)) : ∑ j : Fin nB, localProjB j v = v

The local projectors resolve the identity.

theorem CSD.RecordLayer.sum_normSq_localProjB {nA nB : ℕ} (v : EuclideanSpace ℂ (Fin nA × Fin nB)) : ∑ j : Fin nB, ‖localProjB j v‖ ^ 2 = ‖v‖ ^ 2

The Born weights of the B-outcomes resolve the norm: ∑ⱼ ‖Pⱼv‖² = ‖v‖².

The unnormalised outer product and the invariance identity

noncomputable def CSD.RecordLayer.vecOuter {nA nB : ℕ} (v : EuclideanSpace ℂ (Fin nA × Fin nB)) : Matrix (Fin nA × Fin nB) (Fin nA × Fin nB) ℂ

The unnormalised outer product v x · conj(v y) — rayDensity before normalisation.

Equations

• CSD.RecordLayer.vecOuter v = Matrix.of fun (x y : Fin nA × Fin nB) => v.ofLp x * star (v.ofLp y)

theorem CSD.RecordLayer.vecOuter_zero {nA nB : ℕ} : vecOuter 0 = 0

theorem CSD.RecordLayer.traceRight_sum_vecOuter_localProjB {nA nB : ℕ} (v : EuclideanSpace ℂ (Fin nA × Fin nB)) : ∑ j : Fin nB, (vecOuter (localProjB j v)).traceRight = (vecOuter v).traceRight

★ Tracing out B collapses the local Lüders sum: ∑ⱼ tr_B(Pⱼv ⊗ (Pⱼv)*) = tr_B(v ⊗ v*). The entrywise computation at the heart of dynamical no-signalling.

theorem CSD.RecordLayer.reduceA_mk {nA nB : ℕ} (v : EuclideanSpace ℂ (Fin nA × Fin nB)) (hv : v ≠ 0) : reduceA (Projectivization.mk ℂ v hv) = (↑(‖v‖ ^ 2))⁻¹ • (vecOuter v).traceRight

reduceA at a representative: the normalised partial trace of the outer product.

theorem CSD.RecordLayer.reduceA_localLuders_mixture {nA nB : ℕ} (v : EuclideanSpace ℂ (Fin nA × Fin nB)) (hv : v ≠ 0) : (∑ j : Fin nB, ↑(‖localProjB j v‖ ^ 2 / ‖v‖ ^ 2) • if h : localProjB j v = 0 then 0 else reduceA (Projectivization.mk ℂ (localProjB j v) h)) = reduceA (Projectivization.mk ℂ v hv)

★★ Dynamical no-signalling, the statics core: the Born-weighted mixture of the post-measurement A-marginals of a local B-measurement equals the pre-measurement A-marginal. Zero-weight outcomes carry weight 0 — no positivity hypothesis.