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.

Countable Kraus isometric dilation and partial-trace recovery

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $H$ be a nonzero complex Hilbert space (Hilbert space) and let $(M_{a, r})_{a, r \geq 1}$ be bounded operators on $H$ with

$\sum_{a \leq A, r \leq R} M_{a, r}^{*} M_{a, r} ⟶ I strongly as A, R \to \infty .$

Let $(e_{a, r})_{a, r \geq 1}$ be the standard orthonormal basis of $ℓ^{2}$ and form $H \hat{\otimes} ℓ^{2}$ (Hilbert tensor construction: inner product, completion and product bases). Then

$W : H \to H \hat{\otimes} ℓ^{2}, W ψ : = \sum_{a, r \geq 1} M_{a, r} ψ \otimes e_{a, r}$

is a linear isometry; for each outcome label $a$ the strong limit $P_{a} : = \sum_{r \geq 1} I_{H} \otimes T_{e_{a, r}, e_{a, r}}$ is an orthogonal projection (The Hilbert orthogonal projection onto a closed subspace), the family $(P_{a})_{a \geq 1}$ consists of pairwise orthogonal projections with $\sum_{a} P_{a} = I$ strongly, and

$W^{*} P_{a} W = \sum_{r \geq 1} M_{a, r}^{*} M_{a, r} = : F_{a};$

moreover the partial trace of the dilated state over $ℓ^{2}$ recovers the Kraus instrument: for every trace-class $ρ$ on $H$ ,

${Tr}_{ℓ^{2}} (W ρ W^{*}) = \sum_{a, r \geq 1} M_{a, r} ρ M_{a, r}^{*},$

the series converging in trace norm and the right side being the map of Countable Kraus normalization and trace-norm convergence. This realizes the specified family; it is not a classification of all channels.

Facts & Assumptions

Given: $H$ ; the family $(M_{a, r})$ with the stated strong completeness; the orthonormal basis $(e_{a, r})$ of $ℓ^{2}$ .

[F1]

For $ψ \in H$ , the nonnegative double series $\sum_{a, r} ∥ M_{a, r} ψ ∥^{2}$ has value $∥ ψ ∥^{2}$ , and $∥ W ψ ∥^{2} = \sum_{a, r} ∥ M_{a, r} ψ ∥^{2}$ whenever the partial sums converge (Countable Kraus normalization and trace-norm convergence, Hilbert tensor construction: inner product, completion and product bases, Parseval equivalences for an orthonormal family).

[F2]

The operators $T_{e_{a, r}, e_{a, r}}$ are orthogonal projections onto $C e_{a, r}$ , pairwise orthogonal, with $\sum_{a, r} T_{e_{a, r}, e_{a, r}} = I$ strongly; a strong sum of pairwise orthogonal projections is the orthogonal projection onto the closed span of their ranges, and telescoping strong sums behave additively (Weak and strong additivity of orthogonal projections, The Hilbert orthogonal projection onto a closed subspace, Finite effects and instruments: normalization and non-determination of the update).

[F3]

${Tr}_{ℓ^{2}}$ is the trace-norm continuous linear map with defining identity $tr (({Tr}_{ℓ^{2}} T) A) = tr (T (A \otimes I))$ for bounded $A$ , and on rank-one operators ${Tr}_{ℓ^{2}} T_{u \otimes e, u^{'} \otimes e^{'}} = ⟨ e, e^{'} ⟩ T_{u, u^{'}}$ (Separable partial trace and its basic properties).

[F4]

$tr (T_{x, z}) = ⟨ x, z ⟩$ , and for bounded $B$ , $T_{x, z} B = T_{x, B^{*} z}$ (Rank-one operator calculus, Nuclear bounded cyclicity for trace-class operators).

Proof

1.1givenF1algebra

[The dilation is an isometry] The series defining $W ψ$ converges: the partial sums $\sum_{a \leq A, r \leq R} M_{a, r} ψ \otimes e_{a, r}$ are Cauchy because for $A^{'} \geq A$ , $R^{'} \geq R$ the squared norm of the difference is the corresponding nonnegative subsum, which is bounded by the tail of the summable series $\sum_{a, r} ∥ M_{a, r} ψ ∥^{2}$ ; by [F1] the limit $W ψ$ has $∥ W ψ ∥^{2} = \sum_{a, r} ∥ M_{a, r} ψ ∥^{2} = ∥ ψ ∥^{2}$ , so $W$ is linear and isometric.

2.1step 1.1F2algebra

[Outcome projections] By [F2] each $P_{a} = \sum_{r} I \otimes T_{e_{a, r}, e_{a, r}}$ is the orthogonal projection onto $H \hat{\otimes} \overset{}{span} {e_{a, r} : r \geq 1}$ , the strong sums over $a$ telescope to $I$ , and $P_{a} P_{b} = δ_{a b} P_{a}$ .

3.1step 2.1F1algebra

[Compression] As in the finite case, $W^{*} (ξ \otimes e_{a, r}) = M_{a, r}^{*} ξ$ because $W$ is an isometry with the displayed action, so $W^{*} P_{a} W ψ = \sum_{r} M_{a, r}^{*} M_{a, r} ψ$ for every $ψ$ , the strong limit defining $F_{a}$ .

4.1step 1.1step 3.1F1F3F4algebra∎

[Partial-trace recovery by truncations] For $x, y \in H$ and a finite rectangle $D$ of index pairs put $w_{D} : = \sum_{(a, r) \in D} M_{a, r} x \otimes e_{a, r}$ and $z_{D} : = \sum_{(a, r) \in D} M_{a, r} y \otimes e_{a, r}$ . Then $w_{D} \to W x$ , $z_{D} \to W y$ by step 1.1, and rank-one trace-norm continuity gives $T_{w_{D}, z_{D}} \to T_{W x, W y} = W T_{x, y} W^{*}$ . For each finite rectangle the elementary formula [F3] gives ${Tr}_{ℓ^{2}} T_{w_{D}, z_{D}} = \sum_{(a, r) \in D} T_{M_{a, r} x, M_{a, r} y}$ ; Cauchy–Schwarz and [F1] give $\sum_{a, r} ∥ M_{a, r} x ∥ ∥ M_{a, r} y ∥ \leq ∥ x ∥ ∥ y ∥$ , so these diagonal terms converge absolutely in trace norm. Taking limits using [F3] proves the Kraus formula on rank-one inputs. Both sides are bounded linear maps on trace class: the left side by the two-sided ideal bound for $W, W^{*}$ and [F3], and the right side by nuclear expansion and the preceding rank-one bound. Finite rank-one sums are trace-norm dense by the nuclear characterization in Nuclear bounded cyclicity for trace-class operators, so the identity extends to every trace-class input and equals the map of Countable Kraus normalization and trace-norm convergence.

Countable Kraus isometric dilation and partial-trace recovery

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources