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

Complete positivity implies Choi positivity

Statement

Let $H$ and $K$ be finite-dimensional complex inner-product spaces, fix an ordered orthonormal basis $B$ of $H$ , and let $Φ : L (H) \to L (K)$ be completely positive. Then $J_{B} (Φ)$ is non-negative.

Facts & Assumptions

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

[F1]

Non-negative and positive operators: an endomorphism is non-negative when it is self-adjoint and its quadratic form is non-negative.

[F2]

Every finite-dimensional real or complex inner product space has an orthonormal basis: each finite-dimensional inner-product space has an ordered orthonormal basis, including the empty basis in dimension zero.

[F3]

Finite-dimensional vector space, and its dimension $\dim_{F} V$ ; infinite-dimensional means having no finite basis: a space of dimension zero is the zero space.

[F4]

The adjoint $T^{*} : W \to V$ is characterised by $⟨ T v, w ⟩_{W} = ⟨ v, T^{*} w ⟩_{V}$ and Adjoints satisfy $(S + T)^{*} = S^{*} + T^{*}$ , $(λ T)^{*} = \overline{λ} T^{*}$ , $(S T)^{*} = T^{*} S^{*}$ , and $T^{* *} = T$ : adjoints satisfy their defining pairing identity, $(S T)^{†} = T^{†} S^{†}$ , and $(T^{†})^{†} = T$ for compatible finite-dimensional maps.

[F5]

The standard formulas $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ and $\sum_{k < n} x_{k} \overline{y_{k}}$ on $C^{n}$ are inner products: the standard basis of $C^{n}$ is orthonormal for its standard coordinate inner product.

[F6]

Finite-dimensional linear isometries satisfy the adjoint identity: a surjective linear isometry between finite-dimensional complex inner-product spaces satisfies $W^{†} W = I$ and $W W^{†} = I$ .

[A1]

Completely positive maps: for each integer $r \geq 1$ , the block amplification $Φ^{(r)}$ sends non-negative operators on $H \otimes C^{r}$ to non-negative operators on $K \otimes C^{r}$ .

[A2]

Ordered tensor registers, their inner product, and wire permutations and The product basis is orthonormal and tensor dimensions multiply: the product basis is ordered with the displayed factor order and is orthonormal.

[A3]

Tensor products of finitely many linear maps: on elementary tensors, an operator tensor acts by applying its first and second factor maps to their respective factors.

[L1]

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

Proof

1.1givenF1F3F5algebra

If $\dim H = 0$ , [F3] makes the Choi sum empty. If $\dim K = 0$ , the output operator space contains only the zero map, so every $Φ (E_{i j}) = 0$ . In either case $J_{B} (Φ) = 0$ is non-negative. Assume now both spaces are nonzero, write $B = (e_{i})_{i < n}$ , let $R = C^{n}$ have its standard orthonormal basis $(c_{i})_{i < n}$ by [F5], and set $Ω = \sum_{i < n} e_{i} \otimes c_{i}$ . Define $Q_{Ω} x = ⟨ x, Ω ⟩ Ω$ . The root pairing is linear in its first argument, so $Q_{Ω}$ is linear. For all $x, y$ , $⟨ Q_{Ω} x, y ⟩ = ⟨ x, Ω ⟩ ⟨ Ω, y ⟩ = ⟨ x, Q_{Ω} y ⟩$ , and $⟨ Q_{Ω} x, x ⟩ = ∣ ⟨ x, Ω ⟩ ∣^{2} \geq 0$ . Thus $Q_{Ω}$ is non-negative by [F1].

2.1givenA1A2A3step 1.1algebra

For $i, j < n$ , let $F_{i j} : R \to R$ be the matrix unit $F_{i j} c_{k} = 0$ for $k \neq j$ and $F_{i j} c_{j} = c_{i}$ . On the product basis $(e_{k} \otimes c_{l})$ , the product pairing gives $Q_{Ω} (e_{k} \otimes c_{l}) = 0$ if $k \neq l$ , and $Q_{Ω} (e_{k} \otimes c_{k}) = Ω$ . The same action is given by $\sum_{i, j < n} E_{i j} \otimes F_{i j}$ , so $Q_{Ω} = \sum_{i, j < n} E_{i j} \otimes F_{i j}$ by [A2] and [A3]. The $R$ -blocks of $Q_{Ω}$ are therefore $E_{i j}$ ; the actual block rule in [A1] gives the non-negative operator $Y = Φ^{(n)} (Q_{Ω}) = \sum_{i, j < n} Φ (E_{i j}) \otimes F_{i j}$ on $K \otimes R$ .

3.1givenF2F6A2A3L1step 2.1chooseconstruct

Choose an ordered orthonormal basis $(f_{α})_{α < m}$ of $K$ by [F2]. By [A2], both $(f_{α} \otimes c_{j})_{α, j}$ and $(e_{j} \otimes f_{α})_{j, α}$ are orthonormal bases. Let $W : K \otimes R \to H \otimes K$ be the linear map sending $f_{α} \otimes c_{j}$ to $e_{j} \otimes f_{α}$ . This bijection of orthonormal bases is a surjective linear isometry; [F6] gives $W^{†} W = I$ and $W W^{†} = I$ . Applying the map and its inverse to product basis vectors shows $W (Φ (E_{i j}) \otimes F_{i j}) W^{†} = E_{i j} \otimes Φ (E_{i j})$ for each $i, j$ . Hence $W Y W^{†} = J_{B} (Φ)$ by [L1].

4.1F1F4step 2.1step 3.1algebra∎

By [F4], $W Y W^{†}$ is self-adjoint because $Y$ is self-adjoint. For every $z \in H \otimes K$ , the adjoint identity gives $⟨ W Y W^{†} z, z ⟩ = ⟨ Y W^{†} z, W^{†} z ⟩ \geq 0$ , since $Y$ is non-negative. Therefore $J_{B} (Φ)$ is non-negative.

Depends on

Used by

Kraus and Choi characterizations of complete positivity Theorem

Dependency tree · two levels

53 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.2.6 and 3.3.1 (standard reference, not scraped)