LF2: reduced density operators via partial trace

Category: 3-Local.

An index-parametric density-operator structure DensityOperatorIx ι (Hermitian, PSD, trace one, on Matrix ι ι ℂ) and its reduced density operator DensityOperatorIx.reduced : DensityOperatorIx (m × n) → DensityOperatorIx m, obtained by tracing out the second tensor factor (CsdLean4/Mathlib/LinearAlgebra/Matrix/PartialTrace.lean).

This is the object the no-communication theorem in reduced-density form (E3b) and no-broadcasting (E2) consume: "Bob's reduced state" of a bipartite density operator. The three reduced-operator structure fields discharge directly from the partial-trace API:

• isHermitian ← Matrix.IsHermitian.traceRight,
• nonneg ← Matrix.PosSemidef.traceRight,
• trace_one ← Matrix.trace_traceRight + the original trace_one.

Why a new structure (index-parametric ι, vs LF2's Fin N-indexed DensityOperator): partial trace lives natively on a product index m × n, so a Fin N-only structure would force a Fin (m*n) ≃ Fin m × Fin n reindex through every call. DensityOperatorIx ι is the more natural object and avoids that friction (decision recorded 2026-06-01, specs/partial-trace-plan.md). The two structures agree under finProdFinEquiv should a bridge ever be needed.

structure CSD.LF2.DensityOperatorIx (ι : Type u_1) [Fintype ι] [DecidableEq ι] : Type u_1

Index-parametric density operator. A Hermitian, positive-semidefinite, trace-one matrix on an arbitrary finite index ι. Generalises the Fin N-indexed DensityOperator so that partial traces (which land on a sub-index) stay inside the structure.

• M : Matrix ι ι ℂ

  Underlying matrix.

• isHermitian : self.M.IsHermitian

  ρ is Hermitian.

• nonneg : self.M.PosSemidef

  0 ≤ ρ.

• trace_one : self.M.trace = 1

  Tr(ρ) = 1.

noncomputable def CSD.LF2.DensityOperatorIx.reduced {m : Type u_1} {n : Type u_2} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] (ρ : DensityOperatorIx (m × n)) : DensityOperatorIx m

Reduced density operator (Bob's state). Trace out the second tensor factor n of a bipartite density operator on m × n, leaving a density operator on m. All three fields discharge from the partial-trace API.

Equations

• ρ.reduced = { M := ρ.M.traceRight, isHermitian := ⋯, nonneg := ⋯, trace_one := ⋯ }

noncomputable def CSD.LF2.DensityOperatorIx.reducedLeft {m : Type u_1} {n : Type u_2} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] (ρ : DensityOperatorIx (m × n)) : DensityOperatorIx n

Reduced density operator (Alice's state). Trace out the first factor m, leaving a density operator on n.

Equations

• ρ.reducedLeft = { M := ρ.M.traceLeft, isHermitian := ⋯, nonneg := ⋯, trace_one := ⋯ }

@[simp]

theorem CSD.LF2.DensityOperatorIx.reduced_M {m : Type u_1} {n : Type u_2} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] (ρ : DensityOperatorIx (m × n)) : ρ.reduced.M = ρ.M.traceRight

@[simp]

theorem CSD.LF2.DensityOperatorIx.reducedLeft_M {m : Type u_1} {n : Type u_2} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] (ρ : DensityOperatorIx (m × n)) : ρ.reducedLeft.M = ρ.M.traceLeft