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

Finite-ancilla complete positivity of countable Kraus maps

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $H$ be a complex Hilbert space (Hilbert space), let $(M_{a})_{a \geq 1}$ be bounded operators on $H$ with $\sum_{a \leq N} M_{a}^{*} M_{a} \to I$ strongly, and let $Φ (ρ) = \sum_{a} M_{a} ρ M_{a}^{*}$ be the map of Countable Kraus normalization and trace-norm convergence. Here a map on trace-class operators is completely positive on finite-dimensional ancillas when, for every finite-dimensional complex inner product space $C$ , its matrixwise amplification $I_{C} \otimes Φ$ preserves self-adjoint positive trace-class operators on $C \hat{\otimes} H$ . Then for every finite-dimensional complex inner product space $C$ the amplification

$I_{C} \otimes Φ : S_{1} (C \hat{\otimes} H) \to S_{1} (C \hat{\otimes} H)$

is well defined by the trace-norm convergent series $\sum_{a} (I_{C} \otimes M_{a}) R (I_{C} \otimes M_{a}^{*})$ and preserves positivity: every self-adjoint positive trace-class $R$ (positivity in the sense of Self-adjoint, positive, unitary and normal operators) has $I_{C} \otimes Φ (R)$ self-adjoint positive. Hence $Φ$ is completely positive on every finite-dimensional ancilla in the stated sense.

Facts & Assumptions

Given: $H$ , $(M_{a})$ and $Φ$ as in the Statement; a finite-dimensional complex inner product space $C$ ; a positive trace-class $R$ on $C \hat{\otimes} H$ .

[F1]

The completed tensor product $C \hat{\otimes} H$ with the inner product $⟨ c \otimes h, c^{'} \otimes h^{'} ⟩ = ⟨ c, c^{'} ⟩ ⟨ h, h^{'} ⟩$ is a complex Hilbert space with dense span of elementary tensors; for bounded $S$ the amplification $I_{C} \otimes S$ is bounded with $∥ I_{C} \otimes S ∥ \leq ∥ S ∥$ (Hilbert tensor construction: inner product, completion and product bases, Bounded tensor maps: extension, norm estimate, adjoint and commutation).

[F2]

For every $R \geq 0$ in $S_{1}$ and every bounded $V$ , $V R V^{*} \geq 0$ and $tr (V R V^{*}) = tr (V^{*} V R)$ ; the trace-class operators are complete in trace norm (Nuclear bounded cyclicity for trace-class operators, Trace class is a two sided Banach operator ideal, Trace class operator).

[F3]

A positive trace-class operator $R$ on a Hilbert space has a spectral expansion $R = \sum_{n} w_{n} T_{ξ_{n}, ξ_{n}}$ with orthonormal $ξ_{n}$ , $w_{n} \geq 0$ and $\sum_{n} w_{n} = tr R$ (Density operators and scalar spectral probability).

[F4]

The partial sums $S_{N} = \sum_{a \leq N} M_{a}^{*} M_{a}$ satisfy $0 \leq S_{N} \leq I$ and converge strongly to $I$ . For finite-dimensional $C$ with orthonormal basis $(e_{k})_{k = 1}^{d}$ , every vector in $C \hat{\otimes} H$ has the form $ξ = \sum_{k} e_{k} \otimes h_{k}$ , so $I_{C} \otimes S_{N}$ acts coordinatewise, is a positive contraction, and converges strongly to $I$ (Bounded tensor maps: extension, norm estimate, adjoint and commutation, Hilbert tensor construction: inner product, completion and product bases).

Proof

1.1givenF1F4algebra

[The amplified family is strongly complete] For each $a$ , $(I_{C} \otimes M_{a})^{*} (I_{C} \otimes M_{a}) = I_{C} \otimes M_{a}^{*} M_{a}$ by [F1]. If $(e_{k})_{k = 1}^{d}$ is an orthonormal basis of $C$ and $ξ = \sum_{k} e_{k} \otimes h_{k}$ , then ${∥ (I_{C} \otimes \sum_{a \leq N} M_{a}^{*} M_{a} - I) ξ ∥}^{2} = \sum_{k = 1}^{d} {∥ (S_{N} - I) h_{k} ∥}^{2} ⟶ 0$ by the assumed strong convergence on $H$ . Thus the amplified family satisfies the hypothesis of Countable Kraus normalization and trace-norm convergence on $C \hat{\otimes} H$ , and that lemma applies to it.

2.1step 1.1F1F2F3algebra∎

[Positivity] If $C = {0}$ or $H = {0}$ , then $C \hat{\otimes} H = {0}$ , the only trace-class input is $R = 0$ , and the asserted series and its limit are zero, so the conclusion holds. Suppose henceforth that $C, H \neq {0}$ . For $R \geq 0$ and each $a$ , $(I_{C} \otimes M_{a}) R (I_{C} \otimes M_{a})^{*} \geq 0$ by [F2]; the partial sums are positive, and the trace-norm limit is positive because $⟨ S x, x ⟩ = \lim ⟨ S_{N} x, x ⟩ \geq 0$ for trace-norm convergent $S_{N} \to S$ . Alternatively, applying the spectral argument of Countable Kraus normalization and trace-norm convergence to the amplified family: by [F3], $R = \sum_{n} w_{n} T_{ξ_{n}, ξ_{n}}$ with $ξ_{n} \in C \hat{\otimes} H$ , the partial sums $\sum_{a \leq N} (I_{C} \otimes M_{a}) R (I_{C} \otimes M_{a})^{*} = \sum_{n} w_{n} \sum_{a \leq N} T_{(I_{C} \otimes M_{a}) ξ_{n}, (I_{C} \otimes M_{a}) ξ_{n}}$ are positive with traces $\sum_{n} w_{n} \sum_{a \leq N} ∥ (I_{C} \otimes M_{a}) ξ_{n} ∥^{2} ↑ \sum_{n} w_{n} ∥ ξ_{n} ∥^{2} = tr R$ by step 1.1, so they converge in trace norm to a positive limit with trace $tr R$ , and the series converges to $I_{C} \otimes Φ (R)$ .

Finite-ancilla complete positivity of countable Kraus maps

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources