Q27: what entanglement does to the weights — local observations are reduced-state expectations

Category: CV (the composite arena's local statistics; BACKLOG Q27, queued from the 2026-08-20 external physicist review).

The question: for an entangled composite preparation, what are a local context's weights? The answer this module proves: local arena observations are exactly reduced-state expectations, for every composite point — and on an entangled point the reduced state is mixed, so entanglement is precisely what turns a local context's pure-state Born weights into mixed-state Born weights.

• reducedDM x — the reduced density of a composite ray: the right partial trace of arenaDM x read on the pair index. PSD (reducedDM_posSemidef), trace one (reducedDM_trace): a genuine density operator for every x.
• ★★ arenaObs_leftOp_eq_reduced — the bridge: for EVERY composite point x (entangled included) and every left-sector observable A, arenaObs (leftOp A) x = re tr(reducedDM x · A). Local observations on the composite arena ARE mixed-Born pairings against the reduced state — this is the re tr(D·E) form the LF2 mixed-state tier reads.
• ★ reducedDM_join — the unentangled contrast: on a product point arenaJoin p q the reduced state is the pure local state arenaDM p. Departure of reducedDM x from a rank-one projector is exactly what entanglement contributes.
• ★★ reducedDM_bell — the Bell answer, exactly: on the Bell ray over correlated patterns (x₀,y₀), (x₁,y₁), the reduced state is the equal mixture ½(∣x₀⟩⟨x₀∣ + ∣x₁⟩⟨x₁∣). Corollaries bell_local_weight₀/₁: the local weight of each correlated pattern is exactly 1/2. The same witness that shows the composite arena exceeds the pair (bell_not_join, P2) shows what the excess does: it maximally mixes the local weights across the correlated patterns — and since reducedDM never sees the remote sector's unitaries, this is also composite_no_signalling read as a consequence.

⚠️ Honest scope: weights are delivered in the re tr(reducedDM · A) mixed- Born form on the field-configuration index; transporting them through the Fin-indexed LF2 DensityOperatorIx mixed tier is index plumbing without new content and is not claimed here. Sequential/record-conditioned versions are Q25's territory.

References

specs/BACKLOG.md (Q27); CV/CompositeArena.lean (P2 — leftOp, arenaJoin, bellVec, compositeReindex); Mathlib/QuantumInfo/PartialTrace.lean (partialTraceRight, trace_mul_kronecker_one_right — rehomed there from Subadditivity.lean in this arc); LF2/ReducedDensity.lean, LF2/MixedEnsembleIx.lean (the mixed-Born tier this feeds); specs/future-work.md.

The reduced density of a composite ray

theorem CSD.CV.compositeReindex_symm_apply {K₁ K₂ N : ℕ} (M : Matrix (FieldConfig (K₁ + K₂) N) (FieldConfig (K₁ + K₂) N) ℂ) (a b : FieldConfig K₁ N × FieldConfig K₂ N) : compositeReindex.symm M a b = M (configSplit.symm a) (configSplit.symm b)

The composite reindex, inverted, in submatrix form.

theorem CSD.CV.trace_compositeReindex_symm {K₁ K₂ N : ℕ} (M : Matrix (FieldConfig (K₁ + K₂) N) (FieldConfig (K₁ + K₂) N) ℂ) : (compositeReindex.symm M).trace = M.trace

Traces are preserved by the inverted composite reindex.

noncomputable def CSD.CV.reducedDM {K₁ K₂ N : ℕ} (x : FieldArena (K₁ + K₂) N) : Matrix (FieldConfig K₁ N) (FieldConfig K₁ N) ℂ

The reduced density of a composite ray: trace out the right sector from the ray's density, read on the pair index.

Equations

• CSD.CV.reducedDM x = QuantumInfo.partialTraceRight (CSD.CV.compositeReindex.symm (CSD.CV.arenaDM x))

theorem CSD.CV.reducedDM_posSemidef {K₁ K₂ N : ℕ} (x : FieldArena (K₁ + K₂) N) : (reducedDM x).PosSemidef

The reduced density is positive semidefinite.

theorem CSD.CV.reducedDM_trace {K₁ K₂ N : ℕ} (x : FieldArena (K₁ + K₂) N) : (reducedDM x).trace = 1

The reduced density has unit trace: it is a genuine density operator.

The bridge: local observations are reduced-state expectations

theorem CSD.CV.arenaObs_leftOp_eq_reduced {K₁ K₂ N : ℕ} (A : Matrix (FieldConfig K₁ N) (FieldConfig K₁ N) ℂ) (x : FieldArena (K₁ + K₂) N) : arenaObs (leftOp A) x = RCLike.re (reducedDM x * A).trace

★★ Local arena observations are reduced-state expectations — for EVERY composite point, entangled included. arenaObs (leftOp A) x is the mixed-Born pairing re tr(reducedDM x · A). Entanglement's entire local effect is packaged in reducedDM x being mixed.

theorem CSD.CV.reducedDM_join {K₁ K₂ N : ℕ} (p : FieldArena K₁ N) (q : FieldArena K₂ N) : reducedDM (arenaJoin p q) = arenaDM p

★ The unentangled contrast: on a product point the reduced state is the pure local state. Whatever reducedDM x adds beyond a rank-one projector is entanglement's contribution.

The Bell instance: the local weights, exactly

theorem CSD.CV.bell_norm_sq {K₁ K₂ N : ℕ} {x₀ x₁ : FieldConfig K₁ N} (hx : x₀ ≠ x₁) (y₀ y₁ : FieldConfig K₂ N) : ‖bellVec x₀ x₁ y₀ y₁‖ ^ 2 = 2

The Bell vector's squared norm is 2 (two unit entries at distinct configuration pairs).

theorem CSD.CV.reducedDM_bell {K₁ K₂ N : ℕ} {x₀ x₁ : FieldConfig K₁ N} (hx : x₀ ≠ x₁) {y₀ y₁ : FieldConfig K₂ N} (hy : y₀ ≠ y₁) : reducedDM (Projectivization.mk ℂ (bellVec x₀ x₁ y₀ y₁) ⋯) = (1 / 2) • (Matrix.single x₀ x₀ 1 + Matrix.single x₁ x₁ 1)

★★ What entanglement does to the weights, exactly: the reduced state of the Bell ray over correlated patterns (x₀,y₀), (x₁,y₁) is the equal mixture ½(∣x₀⟩⟨x₀∣ + ∣x₁⟩⟨x₁∣). The remote pattern labels are gone — no signalling — and the local weights are maximally mixed across the two correlated patterns.

theorem CSD.CV.trace_mul_single {K₁ N : ℕ} (M : Matrix (FieldConfig K₁ N) (FieldConfig K₁ N) ℂ) (a : FieldConfig K₁ N) : (M * Matrix.single a a 1).trace = M a a

tr(M · ∣a⟩⟨a∣) = M a a — reading one diagonal weight.

theorem CSD.CV.bell_local_weight₀ {K₁ K₂ N : ℕ} {x₀ x₁ : FieldConfig K₁ N} (hx : x₀ ≠ x₁) {y₀ y₁ : FieldConfig K₂ N} (hy : y₀ ≠ y₁) : arenaObs (leftOp (Matrix.single x₀ x₀ 1)) (Projectivization.mk ℂ (bellVec x₀ x₁ y₀ y₁) ⋯) = 1 / 2

★ The Bell local weight at the first pattern is exactly 1/2.

theorem CSD.CV.bell_local_weight₁ {K₁ K₂ N : ℕ} {x₀ x₁ : FieldConfig K₁ N} (hx : x₀ ≠ x₁) {y₀ y₁ : FieldConfig K₂ N} (hy : y₀ ≠ y₁) : arenaObs (leftOp (Matrix.single x₁ x₁ 1)) (Projectivization.mk ℂ (bellVec x₀ x₁ y₀ y₁) ⋯) = 1 / 2

★ The Bell local weight at the second pattern is exactly 1/2. With bell_local_weight₀: entanglement mixes the local weights maximally across the correlated patterns.