TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)

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.

The Choi partial trace characterizes trace preservation

Statement

Let $H, K$ be finite-dimensional complex inner-product spaces, fix an ordered orthonormal basis $B = (e_{i})_{i < n}$ of $H$ , and let $Φ : L (H) \to L (K)$ be completely positive. Then ${tr}_{K} (Φ (X)) = {tr}_{H} (X)$ for every $X \in L (H)$ if and only if ${Tr}_{K} J_{B} (Φ) = I_{H},$ where ${Tr}_{K}$ is the partial trace over the output factor in the input-first/output-second Choi convention.

Facts & Assumptions

Given: Finite-dimensional complex inner-product spaces $H, K$ , an ordered orthonormal input basis $B = (e_{i})_{i < n}$ , and a completely positive complex-linear map $Φ : L (H) \to L (K)$ .

[F1]

Kraus and Choi characterizations of complete positivity: complete positivity gives a finite Kraus representation of $Φ$ .

[F2]

Trace preservation is Kraus normalization: for such a Kraus representation, trace preservation on every input is equivalent to $S : = \sum_{a} K_{a}^{†} K_{a} = I_{H}$ .

[F3]

Choi matrix with input factor first: $J_{B} (Φ) = \sum_{i, j < n} E_{i j} \otimes Φ (E_{i j})$ , with input factor first and $E_{i j} x = ⟨ x, e_{j} ⟩ e_{i}$ .

[F4]

Partial trace over a finite tensor factor and The partial trace is characterized by the trace pairing and is basis-independent: the partial trace over $K$ is basis-independent and in a product orthonormal basis its $(i, j)$ entry is $\sum_{α} R_{(i, α), (j, α)}$ .

[F5]

Coordinate columns $[v]_{B}$ and matrices $[T]_{B}^{C}$ of linear maps relative to ordered bases and Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes: matrix entries are the coefficients on basis vectors, and the identity has entries $δ_{i j}$ .

[F6]

Every finite-dimensional real or complex inner product space has an orthonormal basis: finite-dimensional $K$ admits an ordered orthonormal basis, including the empty basis when $K = 0$ .

[F7]

In orthonormal bases, the matrix of the adjoint is the conjugate transpose of the matrix: in the chosen orthonormal bases, $[K_{a}^{†}] = [K_{a}]^{†}$ .

Proof

1.1givenF1F2F3F4F5F6F7choosealgebra

By [F1], choose a finite Kraus family $(K_{a})$ for $Φ$ , and put $S = \sum_{a} K_{a}^{†} K_{a}$ . Choose an ordered orthonormal basis $(f_{α})_{α < m}$ of $K$ . The $(i, α), (j, β)$ entry of [F3] is the $(α, β)$ entry of $Φ (E_{i j})$ , which by the Kraus formula is $\sum_{a} (K_{a})_{α i} \overline{(K_{a})_{β j}}$ using the adjoint matrix formula. Taking the partial trace in [F4] therefore gives $({Tr}_{K} J_{B} (Φ))_{i j} = \sum_{α, a} (K_{a})_{α i} \overline{(K_{a})_{α j}} = S_{j i}$ . Thus ${Tr}_{K} J_{B} (Φ) = \sum_{i, j < n} S_{j i} E_{i j}$ . If $Φ$ is trace-preserving on all input operators, [F2] gives $S = I_{H}$ ; then $S_{j i} = δ_{j i} = δ_{i j}$ and the partial trace equals $\sum_{i} E_{i i} = I_{H}$ .

2.1givenF2F5step 1.1algebra∎

Conversely, suppose ${Tr}_{K} J_{B} (Φ) = I_{H}$ . By the entry formula in step 1.1 and uniqueness of matrix entries [F5], $S_{j i} = δ_{i j}$ for every $i, j$ , hence $S = I_{H}$ . By [F2], this is exactly trace preservation on every input. If $H = 0$ , both sides are the unique zero endomorphism and trace preservation is vacuous. If $K = 0$ and $H \neq 0$ , the partial trace and $S$ are zero while $I_{H} \neq 0$ , so neither condition holds.

Depends on

Used by

Finite channel, Kraus, Choi, and Stinespring equivalence Theorem

Dependency tree · two levels

62 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

John Watrous, The Theory of Quantum Information (2018), Theorem 2.26 and Corollary 2.27 (standard reference, not scraped)
John Preskill, Quantum Computation, Chapter 3, §§3.2.6 and 3.3.1 (standard reference, not scraped)