TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Finite partial trace, Schmidt decomposition and finite no-signalling

Statement

Let $V, W$ be nonzero finite-dimensional complex inner product spaces with orthonormal bases $(e_{1}, \dots, e_{m})$ of $V$ and $(f_{1}, \dots, f_{n})$ of $W$ , let $V \otimes W$ be their tensor product with the inner product of Hilbert tensor construction: inner product, completion and product bases, and let $tr$ denote the basis-independent trace of an endomorphism (The basis-independent trace of an endomorphism of a finite-dimensional vector space).

(a) For every endomorphism $R$ of $V \otimes W$ there is a unique endomorphism ${Tr}_{W} R$ of $V$ with

$tr (({Tr}_{W} R) A) = tr (R (A \otimes I_{W})) for every A \in End (V),$

namely ${Tr}_{W} R = \sum_{j = 1}^{n} φ_{j} \circ R \circ ι_{j}$ , where $ι_{j} (v) = v \otimes f_{j}$ and $φ_{j} (x \otimes w) = ⟨ w, f_{j} ⟩ x$ ; it does not depend on the orthonormal basis $(f_{j})$ of $W$ , and the analogous definition gives ${Tr}_{V} R$ with $tr (({Tr}_{V} R) B) = tr (R (I_{V} \otimes B))$ .

(b) ${Tr}_{W}$ is linear, positive (it maps positive endomorphisms to positive endomorphisms) and trace preserving on density matrices: if $R \geq 0$ and $tr R = 1$ then ${Tr}_{W} R \geq 0$ and $tr {Tr}_{W} R = 1$ ; and ${Tr}_{W} T_{Ψ, Ψ} = C C^{*}$ for every $Ψ \in V \otimes W$ , where $C : W \to V$ is the coefficient map determined by $Ψ = \sum_{j} C f_{j} \otimes f_{j}$ .

$Ψ = \sum_{r = 1}^{k} s_{r} v_{r} \otimes u_{r},$

with $k \leq \min (m, n)$ , orthonormal families $(v_{r}) \subseteq V$ , $(u_{r}) \subseteq W$ and $s_{1} \geq \dots \geq s_{k} > 0$ uniquely determined by $Ψ$ as the positive singular values of the coefficient map; moreover $∥ Ψ ∥^{2} = \sum_{r} s_{r}^{2}$ . For $∥ Ψ ∥ = 1$ the reduced density $ρ = {Tr}_{W} T_{Ψ, Ψ}$ satisfies $tr ρ^{2} = \sum_{r} s_{r}^{4}$ , and $tr ρ^{2} = 1$ holds exactly when $k = 1$ , i.e. exactly when $Ψ$ is a product vector; mixed-state separability is not decided by this criterion.

(d) Finite nonselective no-signalling. If $(M_{a})_{a = 1}^{p}$ are endomorphisms of $W$ with $\sum_{a} M_{a}^{*} M_{a} = I_{W}$ then for every endomorphism $R$ of $V \otimes W$

${Tr}_{W} (\sum_{a} (I_{V} \otimes M_{a}) R (I_{V} \otimes M_{a}^{*})) = {Tr}_{W} R .$

This is an identity for the specified finite local instrument; selective conditioning (dividing one summand by its nonzero trace) is not covered.

Facts & Assumptions

Given: Finite-dimensional complex inner product spaces $V, W$ with orthonormal bases $(e_{i}), (f_{j})$ ; an endomorphism $R$ of $V \otimes W$ ; in (c) a vector $Ψ$ ; in (d) endomorphisms $M_{a}$ of $W$ .

[F1]

The tensor product $V \otimes W$ with the inner product $⟨ u \otimes v, u^{'} \otimes v^{'} ⟩ = ⟨ u, u^{'} ⟩_{V} ⟨ v, v^{'} ⟩_{W}$ is a finite-dimensional inner product space; $(e_{i} \otimes f_{j})_{i, j}$ is an orthonormal basis, and every tensor has a unique expansion $\sum_{i, j} c_{i j} e_{i} \otimes f_{j}$ with $∥ Ψ ∥^{2} = \sum_{i, j} ∣ c_{i j} ∣^{2}$ ; the inclusion and the bilinear relations are those of Hilbert tensor construction: inner product, completion and product bases.

[F2]

For endomorphisms $S : V_{1} \to V_{2}$ and $T : V_{2} \to V_{1}$ of finite-dimensional spaces, $tr (S T) = tr (T S)$ ; the trace of an endomorphism is computed as the trace of its matrix in any ordered basis (For $A \in M_{m \times n} (F)$ and $B \in M_{n \times m} (F)$ , $tr (A B) = tr (B A)$ , The basis-independent trace of an endomorphism of a finite-dimensional vector space, Coordinate columns $[v]_{B}$ and matrices $[T]_{B}^{C}$ of linear maps relative to ordered bases).

[F3]

Every linear map $C : W \to V$ of finite-dimensional inner product spaces has a singular value decomposition: orthonormal bases $(u_{1}, \dots, u_{n})$ of $W$ and $(v_{1}, \dots, v_{m})$ of $V$ and $s_{1} \geq \dots \geq s_{k} > 0$ with $C w = \sum_{r = 1}^{k} s_{r} ⟨ w, u_{r} ⟩ v_{r}$ (Every linear map between finite-dimensional real or complex inner product spaces admits a singular value decomposition); the positive numbers $s_{r}^{2}$ are the nonzero eigenvalues of $C C^{*}$ , counted with multiplicity (Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely, A normal endomorphism is a sum of its eigenvalues times pairwise orthogonal projections, and each spectral projection is a polynomial in the endomorphism, Self-adjoint and normal endomorphisms of a finite-dimensional real or complex inner product space).

[F4]

Non-negative means $⟨ T v, v ⟩ \geq 0$ for all $v$ (Non-negative and positive operators); every finite-dimensional inner product space has an orthonormal basis (Every finite-dimensional real or complex inner product space has an orthonormal basis).

Proof

1.1givenF1F2algebra

[Existence and uniqueness of the partial trace] Define ${Tr}_{W} R : = \sum_{j = 1}^{n} φ_{j} R ι_{j}$ , a linear endomorphism of $V$ . Computed in the basis $(e_{i} \otimes f_{j})$ and using [F2], the matrix of $φ_{j}$ contracts the $W$ -index into $f_{j}$ , and the total matrix of ${Tr}_{W} R$ has entries $({Tr}_{W} R)_{i i^{'}} = \sum_{j} R_{i j, i^{'} j}$ ; hence, with $(A)_{i^{'} i^{''}}$ the matrix of $A$ , $tr (({Tr}_{W} R) A) = \sum_{i, i^{'}, j} R_{i j, i^{'} j} A_{i^{'} i} = tr (R (A \otimes I_{W}))$ . Uniqueness: if $S$ and $S^{'}$ both satisfy the pairing identity, then $tr ((S - S^{'}) A) = 0$ for all $A$ ; taking $A = T_{α, β}$ (the rank-one endomorphism $v \mapsto ⟨ v, β ⟩ α$ ) for $α, β$ ranging over a basis of $V$ and using [F1] and [F2] extracts every matrix entry of $S - S^{'}$ , so $S = S^{'}$ . Basis independence: the defining identity involves only the basis-independent trace [F2]; equivalently the formula with another orthonormal basis $(g_{j})$ yields the same operator by the uniqueness just proved.

2.1step 1.1givenF4algebra

[Positivity and trace preservation] If $R \geq 0$ then for every $x \in V$ , $⟨ ({Tr}_{W} R) x, x ⟩ = \sum_{j} ⟨ R (x \otimes f_{j}), x \otimes f_{j} ⟩ \geq 0$ because $R \geq 0$ [F4] and each summand is a nonnegative real; hence ${Tr}_{W} R \geq 0$ . Taking $A = I_{V}$ in the defining identity gives $tr {Tr}_{W} R = tr R$ ; consequently a density matrix $R$ (positive, $tr R = 1$ , in the sense of Density operators and scalar spectral probability) has ${Tr}_{W} R \geq 0$ and trace $1$ , so $({Tr}_{W})$ maps density matrices to density matrices.

2.2step 1.1F1F2algebra

[Reduced state of a pure vector] Let $Ψ = \sum_{i, j} c_{i j} e_{i} \otimes f_{j}$ and define $C : W \to V$ by $C f_{j} = \sum_{i} c_{i j} e_{i}$ , so that $Ψ = \sum_{j} C f_{j} \otimes f_{j}$ by [F1] (insert the expansions of the $C f_{j}$ ). For the rank-one endomorphism $T_{Ψ, Ψ}$ and $A \in End (V)$ , the defining identity of step 1.1 gives $tr (({Tr}_{W} T_{Ψ, Ψ}) A) = tr (T_{Ψ, Ψ} (A \otimes I)) = ⟨ (A \otimes I) Ψ, Ψ ⟩$ , and substituting the expansion yields $\sum_{i, i^{'}} ⟨ A e_{i}, e_{i^{'}} ⟩ \sum_{j} c_{i j} \overline{c_{i^{'} j}} = tr (A C C^{*})$ , using the matrix of $C C^{*}$ in the basis $(e_{i})$ . Since this holds for all $A$ and the operator is determined by its pairings with all $A$ (step 1.1), ${Tr}_{W} T_{Ψ, Ψ} = C C^{*}$ .

3.1step 2.2F1F3algebra

[Schmidt expansion with the complex convention] Apply [F3] to the coefficient map $C$ : there are orthonormal right singular vectors $q_{r} \in W$ and left singular vectors $v_{r} \in V$ such that $C f_{j} = \sum_{r} s_{r} ⟨ f_{j}, q_{r} ⟩ v_{r}$ . Define $u_{r} : = \sum_{j} ⟨ f_{j}, q_{r} ⟩ f_{j}$ , the coordinate conjugate of $q_{r}$ in the fixed basis $(f_{j})$ . The coordinate conjugation reverses inner products, so $⟨ u_{r}, u_{t} ⟩ = \overline{⟨ q_{r}, q_{t} ⟩} = δ_{r t}$ . Substituting the formula for $C f_{j}$ into $Ψ = \sum_{j} C f_{j} \otimes f_{j}$ gives $Ψ = \sum_{r} s_{r} v_{r} \otimes u_{r}$ . Thus the claimed Schmidt expansion holds, with singular values $s_{r}$ of $C$ . Changing the factor bases changes the coefficient matrix by unitary matrices (with transpose rather than adjoint on the second factor); hence the singular values remain unchanged. Orthogonality of the elementary Schmidt products gives $∥ Ψ ∥^{2} = \sum_{r} s_{r}^{2}$ .

4.1step 2.2step 3.1algebra

[Purity and the product criterion] By steps 2.2 and 3.1, $ρ = {Tr}_{W} T_{Ψ, Ψ} = C C^{*}$ has eigenvalues $s_{r}^{2}$ with multiplicity by [F3], so for $∥ Ψ ∥ = 1$ we have $tr ρ^{2} = \sum_{r} s_{r}^{4}$ and $tr ρ = 1 = \sum_{r} s_{r}^{2}$ . Since all $s_{r}$ are positive, $\sum_{r} s_{r}^{4} \leq (\sum_{r} s_{r}^{2})^{2} = 1$ with equality exactly when at most one $s_{r}$ is nonzero, i.e. $k = 1$ ; and $k = 1$ means $Ψ = s_{1} v_{1} \otimes u_{1}$ is a product vector, conversely a product vector has $C$ of rank one by step 2.2. This is the stated criterion; it concerns pure vectors only.

5.1step 1.1F2algebra∎

[Finite nonselective no-signalling] Let $(M_{a})$ satisfy $\sum_{a} M_{a}^{*} M_{a} = I_{W}$ . For $A \in End (V)$ , using the defining identity of step 1.1 and the identity $(I \otimes M_{a}^{*}) (A \otimes I) = (A \otimes M_{a}^{*})$ together with cyclicity [F2] inside the finite trace, $tr (({Tr}_{W} \sum_{a} (I \otimes M_{a}) R (I \otimes M_{a}^{*})) A) = \sum_{a} tr (R (A \otimes M_{a}^{*} M_{a})) = tr (R (A \otimes \sum_{a} M_{a}^{*} M_{a})) = tr (R (A \otimes I)) = tr (({Tr}_{W} R) A)$ ; since this holds for every $A$ , the uniqueness in step 1.1 gives ${Tr}_{W} (\sum_{a} (I \otimes M_{a}) R (I \otimes M_{a}^{*})) = {Tr}_{W} R$ .

Finite partial trace, Schmidt decomposition and finite no-signalling

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources