LemmaStatement: Literature-sourcedProof: 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.

A positive Choi matrix yields finite Kraus operators

Statement

Let $H, K$ be finite-dimensional complex inner-product spaces, let $B = (e_{i})_{i < n}$ be an ordered orthonormal basis of $H$ , and let $Φ : L (H) \to L (K)$ be complex-linear. If $J_{B} (Φ)$ is non-negative, then $Φ$ has a finite Kraus representation with at most $\dim (H) \dim (K)$ operators.

Facts & Assumptions

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

[F1]

A non-negative operator is equivalently self-adjoint with nonnegative eigenvalues, a positive semidefinite matrix in an orthonormal basis, or an operator of the form S^*S: a non-negative finite-dimensional operator has an orthonormal eigenbasis with non-negative real eigenvalues.

[F2]

A non-negative operator has a unique non-negative square root: a non-negative finite-dimensional operator has a non-negative square root $S$ with $S^{2} = J$ .

[F3]

Every finite-dimensional real or complex inner product space has an orthonormal basis: finite-dimensional $H$ and $K$ admit ordered orthonormal bases, including empty bases when a space is zero.

[F4]

Coordinate columns $[v]_{B}$ and matrices $[T]_{B}^{C}$ of linear maps relative to ordered bases: a linear map is determined by its coordinate columns on an ordered basis.

[F5]

Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes: matrix products are row-by-column finite sums, including zero-sized shapes.

[F6]

In orthonormal bases, the matrix of the adjoint is the conjugate transpose of the matrix: in orthonormal bases, the matrix of an adjoint is the conjugate transpose.

[F7]

The product basis is orthonormal and tensor dimensions multiply: the product basis $(e_{i} \otimes f_{α})_{i < n, α < m}$ is orthonormal and has size $n m$ , including zero-dimensional factors.

[L1]

Choi matrix with input factor first (same-page definition): in the input-first product basis, $J_{B} (Φ) = \sum_{i, j < n} E_{i j} \otimes Φ (E_{i j})$ .

[L2]

Finite Kraus representation (same-page definition): a Kraus representation is a finite family of maps $K_{a} : H \to K$ with $Φ (X) = \sum_{a} K_{a} X K_{a}^{†}$ for every $X$ .

Proof

1.1givenF3F4F5F7L1algebrachoose

If $\dim H = 0$ or $\dim K = 0$ , the input or output operator space is zero, so $Φ = 0$ and the empty family is a Kraus representation. Assume both dimensions are positive and choose an ordered orthonormal basis $(f_{α})_{α < m}$ of $K$ by [F3]. If $J_{B} (Φ) = 0$ , its $(i, α), (j, β)$ product-basis entry is the $(α, β)$ entry of $Φ (E_{i j})$ by [L1], so every $Φ (E_{i j}) = 0$ . For each $X \in L (H)$ , the finite sum $\sum_{i, j < n} x_{i j} E_{i j}$ whose coordinate entries are those of $X$ agrees with $X$ on each $e_{j}$ ; [F4] therefore makes it equal to $X$ . Thus $Φ = 0$ and the empty family works also in this case.

1.2givenF1F2F3F7chooseconstruct

Suppose $J_{B} (Φ) \neq 0$ . Let $S = J_{B} (Φ)^{1 / 2}$ be its non-negative square root from [F2]. By [F1], choose an orthonormal eigenbasis $(v_{a})_{a < n m}$ of $S$ with eigenvalues $s_{a} \geq 0$ . Then $J_{B} (Φ) = S^{2} = \sum_{a : s_{a} > 0} s_{a}^{2} v_{a} v_{a}^{†}$ . For each $a$ with $s_{a} > 0$ , put $w_{a} = s_{a} v_{a}$ and write $w_{a} = \sum_{i < n, α < m} w_{a, i α} e_{i} \otimes f_{α}$ . Define the linear map $K_{a} : H \to K$ on the basis by $K_{a} e_{i} = \sum_{α < m} w_{a, i α} f_{α}$ .

2.1F4F5F6L1step 1.2algebra

For every $i, j < n$ and $α, β < m$ , the $(i, α), (j, β)$ entry of [L1] is $\sum_{a : s_{a} > 0} w_{a, i α} \overline{w_{a, j β}}$ . The $(α, β)$ entry of $\sum_{a} K_{a} E_{i j} K_{a}^{†}$ is $\sum_{a} (K_{a})_{α i} \overline{(K_{a})_{β j}}$ , which is the same sum because $(K_{a})_{α i} = w_{a, i α}$ by construction and [F6] gives the conjugate-transpose matrix of $K_{a}^{†}$ . Therefore $Φ (E_{i j}) = \sum_{a} K_{a} E_{i j} K_{a}^{†}$ for every matrix unit.

3.1step 1.1step 2.1F4F7L2algebra∎

Every $X \in L (H)$ is the finite coordinate combination $\sum_{i, j < n} x_{i j} E_{i j}$ established in step 1.1. By linearity, step 2.1 therefore gives $Φ (X) = \sum_{a} K_{a} X K_{a}^{†}$ for every $X$ . There are at most $n m = \dim (H) \dim (K)$ retained operators because the eigenbasis of $S$ has $n m$ elements; when $J = 0$ the empty family was handled in step 1.1. This is a finite Kraus representation by [L2].

Depends on

Used by

Kraus and Choi characterizations of complete positivity Theorem

Dependency tree · two levels

48 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), §2.2.2 (standard reference, not scraped)
John Preskill, Quantum Computation, Chapter 3, §§3.3.1–3.3.2 (standard reference, not scraped)