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.

Complete finite Choi-Kraus equivalence

Statement

Let $d, e \geq 1$ and let $Φ : M_{d} (C) \to M_{e} (C)$ be complex-linear. Choose the standard input basis $(∣ i ⟩)_{i = 1}^{d}$ , let $E_{i j} = ∣ i ⟩ ⟨ j ∣$ , and use the ordered tensor convention input-reference $\otimes$ output. Define the (unnormalized) Choi matrix

$J (Φ) : = \sum_{i, j = 1}^{d} E_{i j} \otimes Φ (E_{i j}) \in M_{d} (C) \otimes M_{e} (C) .$ Then $Φ$ is completely positive if and only if $J (Φ) \geq 0$ , and this holds if and only if there are $q \leq d e$ matrices $K_{1}, \dots, K_{q} : C^{d} \to C^{e}$ such that $Φ (X) = \sum_{a = 1}^{q} K_{a} X K_{a}^{*} (X \in M_{d} (C)) .$

The empty sum is allowed when $Φ = 0$ . For any such Kraus representation, $Φ$ is trace-preserving if and only if $\sum_{a = 1}^{q} K_{a}^{*} K_{a} = I_{d}$ .

Facts & Assumptions

Given: Integers $d, e \geq 1$ , a complex-linear map $Φ : M_{d} (C) \to M_{e} (C)$ , the standard ordered bases, and the input-reference $\otimes$ output Choi convention in the Statement.

[F1]

Finite completely positive trace-preserving maps: complete positivity means that ${id}_{r} \otimes Φ$ preserves positive semidefinite matrices for every finite $r \geq 1$ ; trace preservation means $Tr Φ (X) = Tr X$ for every $X$ .

[F2]

Finite matrix spectral and state calculus: every finite Hermitian matrix has an orthonormal eigenbasis with real eigenvalues, and positive square roots are defined by its finite spectral projections.

[F3]

Finite matrix trace cyclicity and nondegeneracy: for rectangular factors, ${Tr}_{e} (A B) = {Tr}_{d} (B A)$ ; the square bilinear trace pairing is nondegenerate.

Proof

1.1givenF1algebra

Let $Ω = \sum_{i = 1}^{d} ∣ i ⟩ \otimes ∣ i ⟩$ in the input-reference and input tensor factors. Then $Ω Ω^{*} = \sum_{i, j} E_{i j} \otimes E_{i j} \geq 0$ , and $({id}_{d} \otimes Φ) (Ω Ω^{*}) = J (Φ)$ . If $Φ$ is completely positive, [F1] applied with ancilla dimension $d$ gives $J (Φ) \geq 0$ .

1.2givenF2construct

Suppose $J (Φ) \geq 0$ . By [F2], choose an orthonormal eigenbasis of $J (Φ)$ , absorb each positive eigenvalue's square root into its eigenvector, and write $J (Φ) = \sum_{a = 1}^{q} ∣ w_{a} ⟩ ⟨ w_{a} ∣$ , where $q = rank J (Φ) \leq d e$ ; if $J (Φ) = 0$ , take $q = 0$ . For each $a$ , uniquely define $K_{a} : C^{d} \to C^{e}$ by $w_{a} = \sum_{i} ∣ i ⟩ \otimes K_{a} ∣ i ⟩$ .

2.1step 1.2algebra

Expanding each rank-one term gives $∣ w_{a} ⟩ ⟨ w_{a} ∣ = \sum_{i, j} E_{i j} \otimes K_{a} E_{i j} K_{a}^{*}$ . Comparing the coefficients of the linearly independent first-factor matrix units in $J (Φ)$ yields $Φ (E_{i j}) = \sum_{a} K_{a} E_{i j} K_{a}^{*}$ . Since $(E_{i j})$ is a basis and both sides are linear in the input, $Φ (X) = \sum_{a} K_{a} X K_{a}^{*}$ for every $X$ .

3.1givenF1F3step 2.1algebra∎

For any $r \geq 1$ and any $P \geq 0$ on $C^{r} \otimes C^{d}$ , the Kraus formula gives $({id}_{r} \otimes Φ) (P) = \sum_{a} (I_{r} \otimes K_{a}) P (I_{r} \otimes K_{a})^{*} \geq 0$ ; hence $Φ$ is completely positive. For a Kraus representation, cyclicity [F3] gives $Tr Φ (X) = Tr (X \sum_{a} K_{a}^{*} K_{a})$ . Thus $\sum_{a} K_{a}^{*} K_{a} = I_{d}$ implies trace preservation, and if trace preservation holds then testing $Tr (X (\sum_{a} K_{a}^{*} K_{a} - I_{d})) = 0$ on every matrix unit $X = E_{i j}$ forces every entry of the difference to vanish.

Remarks

The input-reference $\otimes$ output order is fixed here. Watrous writes the output factor first; the two Choi matrices are related by the tensor-factor swap unitary, which preserves positivity. This finite result asserts neither an infinite-dimensional classification nor a physical bath limit.

Complete finite Choi-Kraus equivalence

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources