SigmaLayer/LocalLudersBasis: local measurements in every basis (brick 3a)

Category: dynamical measurement — dynamical no-signalling (A6, dynamical form), brick 3a: the local Lüders map for an arbitrary orthonormal basis on the measured factor.

LocalLuders handled the computational-basis marker measurement. The eraser's erase arm measures the marker in the ± basis — and rather than hand-build those two projectors, this module generalises: for any orthonormal basis g of the B factor,

(localProjOn g j v)(a, k) = ⟪gⱼ, v(a,·)⟫ · gⱼ(k)

is the local projector 1_A ⊗ |gⱼ⟩⟨gⱼ|. The computational case is recovered exactly (localProjOn_basisFun). Everything brick 1 proved survives, with Parseval doing the work the ite-collapse did before:

• the projectors resolve the identity (sum_localProjOn — basis expansion, slice by slice);
• the Born weights resolve the norm (sum_normSq_localProjOn — Parseval per slice);
• ★★ marginal invariance in every basis (reduceA_localLudersOn_mixture): the Born-weighted mixture of the post-measurement A-marginals equals the pre-measurement A-marginal, whatever basis B's apparatus measures in. Alice cannot learn Bob's basis choice any more than his outcome — the statics core of no-signalling, now basis-universal.

⚠️ Honest scope. As in brick 1, this is the statics layer, in the states-and-weights vocabulary that BlockLudersObligation names and the join witness inhabits dynamically; the rotated block structure enters the dynamical machinery through the brick-2 index bridge composed with the local unitary rotating g to the computational basis (the RotatedSwap idiom) — not re-proved here. Brick 3b instantiates the 2 ⊗ 2 eraser: the computational marker measurement (which-path, no fringe) and the ± marker measurement (fringes restored, the QuantumEraserVolume statistics).

References

specs/BACKLOG.md (the dynamical no-signalling + eraser row); specs/future-work.md. Reused corpus API: localProjB/vecOuter/reduceA_mk (SigmaLayer/LocalLuders.lean), normSq_eq_sum_mul_star (SigmaLayer/OnticMarginals.lean), OrthonormalBasis.sum_inner_mul_inner + OrthonormalBasis.sum_repr' (Mathlib).

The B-slice and the rotated local projector

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

The B-slice of a composite vector at A-index a.

Equations

• CSD.RecordLayer.sliceB v a = WithLp.toLp 2 fun (k : Fin nB) => v.ofLp (a, k)

@[simp]

theorem CSD.RecordLayer.sliceB_apply {nA nB : ℕ} (v : EuclideanSpace ℂ (Fin nA × Fin nB)) (a : Fin nA) (k : Fin nB) : (sliceB v a).ofLp k = v.ofLp (a, k)

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

The local projector 1_A ⊗ |gⱼ⟩⟨gⱼ| for an arbitrary orthonormal basis g of the B factor: (Pⱼ v)(a, k) = ⟪gⱼ, v(a,·)⟫ · gⱼ(k).

Equations

• CSD.RecordLayer.localProjOn g j v = WithLp.toLp 2 fun (ak : Fin nA × Fin nB) => inner ℂ (g j) (CSD.RecordLayer.sliceB v ak.1) * (g j).ofLp ak.2

@[simp]

theorem CSD.RecordLayer.localProjOn_apply {nA nB : ℕ} (g : OrthonormalBasis (Fin nB) ℂ (EuclideanSpace ℂ (Fin nB))) (j : Fin nB) (v : EuclideanSpace ℂ (Fin nA × Fin nB)) (ak : Fin nA × Fin nB) : (localProjOn g j v).ofLp ak = inner ℂ (g j) (sliceB v ak.1) * (g j).ofLp ak.2

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

The computational basis recovers localProjB.

Identity and norm resolution

theorem CSD.RecordLayer.sum_normSq_inner_orthonormal {nB : ℕ} (g : OrthonormalBasis (Fin nB) ℂ (EuclideanSpace ℂ (Fin nB))) (x : EuclideanSpace ℂ (Fin nB)) : ∑ j : Fin nB, ‖inner ℂ (g j) x‖ ^ 2 = ‖x‖ ^ 2

Parseval for a slice: the squared inner products against an orthonormal basis resolve the squared norm.

theorem CSD.RecordLayer.sum_localProjOn {nA nB : ℕ} (g : OrthonormalBasis (Fin nB) ℂ (EuclideanSpace ℂ (Fin nB))) (v : EuclideanSpace ℂ (Fin nA × Fin nB)) : ∑ j : Fin nB, localProjOn g j v = v

The rotated projectors resolve the identity — basis expansion, slice by slice.

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

The Born weights of the rotated outcomes resolve the norm — Parseval per slice.

The marginal-invariance identity, in every basis

theorem CSD.RecordLayer.traceRight_sum_vecOuter_localProjOn {nA nB : ℕ} (g : OrthonormalBasis (Fin nB) ℂ (EuclideanSpace ℂ (Fin nB))) (v : EuclideanSpace ℂ (Fin nA × Fin nB)) : ∑ j : Fin nB, (vecOuter (localProjOn g j v)).traceRight = (vecOuter v).traceRight

★ Tracing out B collapses the rotated Lüders sum — Parseval where brick 1 had the ite-collapse.

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

★★ Dynamical no-signalling, in every measurement basis: the Born-weighted mixture of the post-measurement A-marginals of a local B-measurement in any orthonormal basis equals the pre-measurement A-marginal. Alice cannot detect Bob's outcome or his choice of basis. Zero-weight outcomes carry weight 0 — no positivity hypothesis.