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.

A finite Kraus sum is completely positive

Statement

Let $H, K$ be finite-dimensional complex inner-product spaces and let $Φ : L (H) \to L (K)$ have a finite Kraus representation $Φ (X) = \sum_{a \in A} K_{a} X K_{a}^{†}$ . Then $Φ$ is completely positive.

Facts & Assumptions

Given: Finite-dimensional complex inner-product spaces $H, K$ , a finite family of linear maps $K_{a} : H \to K$ , and the Kraus formula for $Φ$ .

[F1]

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

[F2]

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 the defining pairing identity and reverse compatible compositions.

[F3]

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^{r}$ is orthonormal.

[F4]

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

[F5]

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

[F6]

Every finite-dimensional real or complex inner product space has an orthonormal basis: finite-dimensional complex inner-product spaces admit ordered orthonormal bases, with the empty basis in dimension zero.

[L1]

Finite Kraus representation (same-page definition): $Φ (X) = \sum_{a} K_{a} X K_{a}^{†}$ for every $X \in L (H)$ .

[A1]

Completely positive maps: for every $r \geq 1$ , the block amplification $Φ^{(r)}$ on $H \otimes C^{r}$ sends non-negative operators 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: ordered orthonormal bases of the factors give ordered orthonormal product bases of $H \otimes C^{r}$ and $K \otimes C^{r}$ .

[A3]

Tensor products of finitely many linear maps: tensor maps act on elementary tensors by applying factor maps in the displayed order.

[A4]

Tensor maps preserve composition, identities, and adjoints: tensor maps preserve composition and $(K_{a} \otimes I_{R})^{†} = K_{a}^{†} \otimes I_{R}$ .

Proof

1.1givenF3F4F5F6A1A2A3A4L1algebrachoose

Fix $r \geq 1$ and put $R = C^{r}$ with its standard ordered basis $(c_{k})_{k < r}$ , the basis used for the block amplification in [A1]. Choose ordered orthonormal bases $(e_{i})$ of $H$ and $(f_{j})$ of $K$ by [F6], allowing an empty basis. If $H = 0$ , the domain $L (H \otimes R)$ is zero and the identity below holds for its sole operator. Otherwise let $E_{i j}$ be the matrix units of $H$ in the basis $(e_{i})$ and let $F_{k l}$ be the matrix units of $R$ in its standard basis $(c_{k})$ . By [A2], $(e_{i} \otimes c_{k})$ is a basis; the operators $E_{i j} \otimes F_{k l}$ are its matrix units, so they span $L (H \otimes R)$ by [F4] and [F5]. For such a product matrix unit, its only nonzero ancilla block is block $(k, l)$ , equal to $E_{i j}$ . The block rule in [A1] therefore gives $Φ^{(r)} (E_{i j} \otimes F_{k l}) = Φ (E_{i j}) \otimes F_{k l}$ . On the other hand, [A3], [A4], and [L1] give $\sum_{a} (K_{a} \otimes I_{R}) (E_{i j} \otimes F_{k l}) (K_{a}^{†} \otimes I_{R}) = \sum_{a} (K_{a} E_{i j} K_{a}^{†}) \otimes F_{k l} = Φ (E_{i j}) \otimes F_{k l}$ . By linearity the two maps agree for every $X \in L (H \otimes R)$ .

2.1givenF1F2step 1.1algebra

Let $X$ be non-negative and put $T_{a} = K_{a} \otimes I_{R}$ . Each $T_{a} X T_{a}^{†}$ is self-adjoint because $(T_{a} X T_{a}^{†})^{†} = T_{a} X^{†} T_{a}^{†} = T_{a} X T_{a}^{†}$ by [F2]. For every $y$ , the adjoint identity in [F2] gives $⟨ T_{a} X T_{a}^{†} y, y ⟩ = ⟨ X T_{a}^{†} y, T_{a}^{†} y ⟩ \geq 0$ by [F1]. Thus each summand and their finite sum are non-negative. If $A$ is empty, the sum is zero and has the same property.

3.1A1step 2.1∎

Since $r \geq 1$ was arbitrary, [A1] and step 2.1 show that every finite ancilla block amplification preserves non-negativity. This is precisely complete positivity by [A1].

Depends on

Used by

Exact correction of a protected subsystem Definition
A degenerate code with a non-diagonal Knill–Laflamme matrix Example
Orthogonal error spaces and a recovery branch Example
Complement and degradation maps of the erasure channel Lemma
Optimal Cloner Attains Bound Lemma
Preserving the logical marginal forces a gauge-only channel Lemma
The finite classical key-copy map is a quantum channel Lemma
Unitary conjugation is a channel Proposition
An explicit syndrome recovery corrects a Knill–Laflamme error family Theorem
An isometry followed by partial trace is a channel Theorem
Channel Diamond Norm One Theorem
Finite-dimensional channels compose and tensor Theorem
Full Rank Pair No Broadcasting Theorem
Kraus and Choi characterizations of complete positivity Theorem
Singular Pair No Broadcasting Theorem
State Family No Broadcasting Iff Commuting Theorem
The Knill–Laflamme criterion for a protected subsystem Theorem

Dependency tree · two levels

42 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.1 and 3.2.6 (standard reference, not scraped)