Matrix partial trace (K1-B.1)

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate).

Glossary: https://glossary.constraintsurfacedynamics.com/partial-trace/ Plain-language, CSD-role and formal statements of the partial trace, with this module as the Lean anchor. Kept symmetric by scripts/check-glossary.sh.

The partial trace of a bipartite matrix M : Matrix (n × m) (n × m) ℂ. Mathlib has no matrix partial trace (the only partialTrace declarations are category-theoretic / probability kernels), so this is genuinely new infrastructure. It is the shared prerequisite for K1-B subadditivity (specs/k1-plan.md), the gated decoherence / entangled D1 tier, and the Landauer / ontic-entropy touchpoint.

For M : Matrix (n × m) (n × m) ℂ:

• partialTraceRight M : Matrix n n ℂ, (Tr_B M) i j = ∑ₖ M (i,k) (j,k) — trace out the second (B) factor, leaving the first (A) factor;
• partialTraceLeft M : Matrix m m ℂ, (Tr_A M) k l = ∑ᵢ M (i,k) (i,l) — trace out the first (A) factor.

Delivered, foundational-triple-only and AxiomAudit-pinned:

• linearity (_add, _smul, and the bundled partialTraceRightₗ/partialTraceLeftₗ LinearMaps);
• trace preservation trace (Tr_B M) = trace M (partialTraceRight_trace, partialTraceLeft_trace), via Fintype.sum_prod_type;
• tensor reduction Tr_B (ρ ⊗ₖ σ) = (trace σ) • ρ and Tr_A (ρ ⊗ₖ σ) = (trace ρ) • σ (partialTraceRight_kronecker, partialTraceLeft_kronecker) — note the trace of the traced-out factor multiplies the surviving one;
• IsHermitian preservation (partialTraceRight_isHermitian, partialTraceLeft_isHermitian);
• PosSemidef preservation (partialTraceRight_posSemidef, partialTraceLeft_posSemidef), via the witness vectors w_k (i,k') = if k' = k then v i else 0 (a v ⊗ eₖ tensor), for which star v ⬝ᵥ (Tr_B M) *ᵥ v = ∑ₖ star (w_k) ⬝ᵥ M *ᵥ (w_k), each summand ≥ 0 by M.PosSemidef;
• density ↦ density (partialTraceRight_density, partialTraceLeft_density): the reduced state of a density operator is a density operator.

Definitions

noncomputable def QuantumInfo.partialTraceRight {n : Type u_1} {m : Type u_2} [Fintype m] (M : Matrix (n × m) (n × m) ℂ) : Matrix n n ℂ

The right partial trace Tr_B : Matrix (n × m) (n × m) ℂ → Matrix n n ℂ, tracing out the second (B) factor: (Tr_B M) i j = ∑ₖ M (i,k) (j,k). Leaves the first (A) factor.

Equations

• QuantumInfo.partialTraceRight M = Matrix.of fun (i j : n) => ∑ k : m, M (i, k) (j, k)

noncomputable def QuantumInfo.partialTraceLeft {n : Type u_1} {m : Type u_2} [Fintype n] (M : Matrix (n × m) (n × m) ℂ) : Matrix m m ℂ

The left partial trace Tr_A : Matrix (n × m) (n × m) ℂ → Matrix m m ℂ, tracing out the first (A) factor: (Tr_A M) k l = ∑ᵢ M (i,k) (i,l). Leaves the second (B) factor.

Equations

• QuantumInfo.partialTraceLeft M = Matrix.of fun (k l : m) => ∑ i : n, M (i, k) (i, l)

theorem QuantumInfo.partialTraceRight_apply {n : Type u_1} {m : Type u_2} [Fintype m] (M : Matrix (n × m) (n × m) ℂ) (i j : n) : partialTraceRight M i j = ∑ k : m, M (i, k) (j, k)

theorem QuantumInfo.partialTraceLeft_apply {n : Type u_1} {m : Type u_2} [Fintype n] (M : Matrix (n × m) (n × m) ℂ) (k l : m) : partialTraceLeft M k l = ∑ i : n, M (i, k) (i, l)

Linearity

theorem QuantumInfo.partialTraceRight_add {n : Type u_1} {m : Type u_2} [Fintype m] (A B : Matrix (n × m) (n × m) ℂ) : partialTraceRight (A + B) = partialTraceRight A + partialTraceRight B

theorem QuantumInfo.partialTraceRight_smul {n : Type u_1} {m : Type u_2} [Fintype m] (c : ℂ) (A : Matrix (n × m) (n × m) ℂ) : partialTraceRight (c • A) = c • partialTraceRight A

theorem QuantumInfo.partialTraceLeft_add {n : Type u_1} {m : Type u_2} [Fintype n] (A B : Matrix (n × m) (n × m) ℂ) : partialTraceLeft (A + B) = partialTraceLeft A + partialTraceLeft B

theorem QuantumInfo.partialTraceLeft_smul {n : Type u_1} {m : Type u_2} [Fintype n] (c : ℂ) (A : Matrix (n × m) (n × m) ℂ) : partialTraceLeft (c • A) = c • partialTraceLeft A

noncomputable def QuantumInfo.partialTraceRightₗ {n : Type u_1} {m : Type u_2} [Fintype m] : Matrix (n × m) (n × m) ℂ →ₗ[ℂ] Matrix n n ℂ

The right partial trace bundled as a ℂ-linear map.

Equations

• QuantumInfo.partialTraceRightₗ = { toFun := QuantumInfo.partialTraceRight, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def QuantumInfo.partialTraceLeftₗ {n : Type u_1} {m : Type u_2} [Fintype n] : Matrix (n × m) (n × m) ℂ →ₗ[ℂ] Matrix m m ℂ

The left partial trace bundled as a ℂ-linear map.

Equations

• QuantumInfo.partialTraceLeftₗ = { toFun := QuantumInfo.partialTraceLeft, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem QuantumInfo.partialTraceRightₗ_apply {n : Type u_1} {m : Type u_2} [Fintype m] (M : Matrix (n × m) (n × m) ℂ) : partialTraceRightₗ M = partialTraceRight M

@[simp]

theorem QuantumInfo.partialTraceLeftₗ_apply {n : Type u_1} {m : Type u_2} [Fintype n] (M : Matrix (n × m) (n × m) ℂ) : partialTraceLeftₗ M = partialTraceLeft M

Trace preservation

@[simp]

theorem QuantumInfo.partialTraceRight_trace {n : Type u_1} {m : Type u_2} [Fintype n] [Fintype m] (M : Matrix (n × m) (n × m) ℂ) : (partialTraceRight M).trace = M.trace

Trace preservation: trace (Tr_B M) = trace M. ∑ᵢ ∑ₖ M (i,k) (i,k) = ∑_{(i,k)} M (i,k) (i,k) = trace M via Fintype.sum_prod_type.

@[simp]

theorem QuantumInfo.partialTraceLeft_trace {n : Type u_1} {m : Type u_2} [Fintype n] [Fintype m] (M : Matrix (n × m) (n × m) ℂ) : (partialTraceLeft M).trace = M.trace

Trace preservation: trace (Tr_A M) = trace M.

Tensor reduction

@[simp]

theorem QuantumInfo.partialTraceRight_kronecker {n : Type u_1} {m : Type u_2} [Fintype m] (ρ : Matrix n n ℂ) (σ : Matrix m m ℂ) : partialTraceRight (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ρ σ) = σ.trace • ρ

Tensor reduction: Tr_B (ρ ⊗ₖ σ) = (trace σ) • ρ. The trace of the traced-out factor σ multiplies the surviving factor ρ: (ρ⊗σ)((i,k),(j,k)) = ρ i j · σ k k, so ∑ₖ ρ i j · σ k k = ρ i j · trace σ.

@[simp]

theorem QuantumInfo.partialTraceLeft_kronecker {n : Type u_1} {m : Type u_2} [Fintype n] (ρ : Matrix n n ℂ) (σ : Matrix m m ℂ) : partialTraceLeft (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ρ σ) = ρ.trace • σ

Tensor reduction: Tr_A (ρ ⊗ₖ σ) = (trace ρ) • σ. The trace of the traced-out factor ρ multiplies the surviving factor σ.

theorem QuantumInfo.partialTraceRight_kronecker_trace_one {n : Type u_1} {m : Type u_2} [Fintype m] (ρ : Matrix n n ℂ) (σ : Matrix m m ℂ) (hσ : σ.trace = 1) : partialTraceRight (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ρ σ) = ρ

Reduced product state: Tr_B (ρ ⊗ₖ σ) = ρ when trace σ = 1. The K1-B.2 consumer: the right reduced state of a product density operator is its left factor.

theorem QuantumInfo.partialTraceLeft_kronecker_trace_one {n : Type u_1} {m : Type u_2} [Fintype n] (ρ : Matrix n n ℂ) (σ : Matrix m m ℂ) (hρ : ρ.trace = 1) : partialTraceLeft (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ρ σ) = σ

Reduced product state: Tr_A (ρ ⊗ₖ σ) = σ when trace ρ = 1.

IsHermitian preservation

theorem QuantumInfo.partialTraceRight_isHermitian {n : Type u_1} {m : Type u_2} [Fintype m] {M : Matrix (n × m) (n × m) ℂ} (hM : M.IsHermitian) : (partialTraceRight M).IsHermitian

IsHermitian preservation: M.IsHermitian → (Tr_B M).IsHermitian. From M (a) (b) = star (M b a) (the Hermitian condition Mᴴ = M), the sum (Tr_B M)ᴴ i j = star (∑ₖ M (j,k) (i,k)) = ∑ₖ M (i,k) (j,k) = (Tr_B M) i j.

theorem QuantumInfo.partialTraceLeft_isHermitian {n : Type u_1} {m : Type u_2} [Fintype n] {M : Matrix (n × m) (n × m) ℂ} (hM : M.IsHermitian) : (partialTraceLeft M).IsHermitian

IsHermitian preservation: M.IsHermitian → (Tr_A M).IsHermitian.

PosSemidef preservation

theorem QuantumInfo.star_dotProduct_mulVec_eq_sum {ι : Type u_3} [Fintype ι] (M : Matrix ι ι ℂ) (u : ι → ℂ) : star u ⬝ᵥ M.mulVec u = ∑ p : ι, ∑ q : ι, star (u p) * M p q * u q

The Hermitian quadratic form expanded as an explicit double sum: star u ⬝ᵥ (M *ᵥ u) = ∑ p, ∑ q, star (u p) * M p q * u q. A bookkeeping helper for the partial-trace PosSemidef proofs.

theorem QuantumInfo.partialTraceRight_posSemidef {n : Type u_1} {m : Type u_2} [Fintype n] [Fintype m] [DecidableEq m] {M : Matrix (n × m) (n × m) ℂ} (hM : M.PosSemidef) : (partialTraceRight M).PosSemidef

PosSemidef preservation: M.PosSemidef → (Tr_B M).PosSemidef.

The quadratic form on the reduced operator unfolds, for any v : n → ℂ, into a sum over the traced-out index k of the quadratic form of M on the tensor witnesses wₖ : n × m → ℂ, wₖ (i, k') = if k' = k then v i else 0 (i.e. v ⊗ eₖ):

star v ⬝ᵥ (Tr_B M) *ᵥ v = ∑ₖ star (wₖ) ⬝ᵥ M *ᵥ (wₖ) ≥ 0,

each summand ≥ 0 by M.PosSemidef.

theorem QuantumInfo.partialTraceLeft_posSemidef {n : Type u_1} {m : Type u_2} [Fintype n] [Fintype m] [DecidableEq n] {M : Matrix (n × m) (n × m) ℂ} (hM : M.PosSemidef) : (partialTraceLeft M).PosSemidef

PosSemidef preservation: M.PosSemidef → (Tr_A M).PosSemidef. Witnesses wᵢ : n × m → ℂ, wᵢ (i', k) = if i' = i then v k else 0 (i.e. eᵢ ⊗ v).

Density ↦ density

theorem QuantumInfo.partialTraceRight_density {n : Type u_1} {m : Type u_2} [Fintype n] [Fintype m] [DecidableEq m] {M : Matrix (n × m) (n × m) ℂ} (hM : M.PosSemidef) (htr : M.trace = 1) : (partialTraceRight M).PosSemidef ∧ (partialTraceRight M).trace = 1

The reduced state of a density operator is a density operator (right factor). From PSD preservation + trace preservation: if M is PSD with unit trace then so is Tr_B M.

theorem QuantumInfo.partialTraceLeft_density {n : Type u_1} {m : Type u_2} [Fintype n] [Fintype m] [DecidableEq n] {M : Matrix (n × m) (n × m) ℂ} (hM : M.PosSemidef) (htr : M.trace = 1) : (partialTraceLeft M).PosSemidef ∧ (partialTraceLeft M).trace = 1

The reduced state of a density operator is a density operator (left factor).

Reduced-trace identities

Rehomed from Subadditivity.lean (2026-08-20, the Q27 arc): the defining property of the partial trace belongs beside the definition, and the CV entangled-weights bridge (CV/EntangledWeights.lean) consumes it without the entropy stack. Both K1-B consumers (Subadditivity.lean, StrongSubadditivity.lean) keep resolving the names through their public import of this module.

theorem QuantumInfo.trace_mul_kronecker_one_right {n : Type u_1} {m : Type u_2} [Fintype n] [Fintype m] [DecidableEq m] (M : Matrix (n × m) (n × m) ℂ) (X : Matrix n n ℂ) : (M * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) X 1).trace = (partialTraceRight M * X).trace

Reduced-trace identity (right): Tr(M · (X ⊗ I)) = Tr(Tr_B(M) · X). Pairing a bipartite operator against a X ⊗ I_B observable collapses to the right partial trace. Basis-free; from expanding the trace, collapsing the I_B Kronecker factor (l = k), and Finset.sum_comm.

theorem QuantumInfo.trace_mul_one_kronecker_left {n : Type u_1} {m : Type u_2} [Fintype n] [Fintype m] [DecidableEq n] (M : Matrix (n × m) (n × m) ℂ) (Y : Matrix m m ℂ) : (M * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 Y).trace = (partialTraceLeft M * Y).trace

Reduced-trace identity (left): Tr(M · (I ⊗ Y)) = Tr(Tr_A(M) · Y).