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.

The finite classical key-copy map is a quantum channel

Statement

Let $K$ be a finite nonempty key alphabet with a fixed ordering, and let $H_{T}, H_{E}$ be finite-dimensional complex inner-product spaces with $H_{T} \neq {0}$ and $H_{E} \neq {0}$ . Give the key register $H_{A} = C^{K}$ its corresponding computational basis $(∣ k ⟩)_{k \in K}$ . For each $k \in K$ , define $L_{k} : H_{A} \otimes H_{T} \otimes H_{E} \to H_{A} \otimes H_{B} \otimes H_{T} \otimes H_{E}$ by

$L_{k} (∣ j ⟩ \otimes x) = {\begin{cases} ∣ k, k ⟩ \otimes x, & j = k, \\ 0, & j \neq k, \end{cases}$

and extend linearly, where $H_{B}$ is another copy of $H_{A}$ . Then

$C (X) : = \sum_{k \in K} L_{k} X L_{k}^{†}$

is a finite-dimensional quantum channel. On every input classical in $A$ , $ξ_{A T E} = \sum_{k} ∣ k ⟩ ⟨ k ∣ \otimes ξ_{T E}^{k}$ , it acts by

$C (ξ_{A T E}) = \sum_{k \in K} ∣ k, k ⟩ ⟨ k, k ∣ \otimes ξ_{T E}^{k} .$

This map copies a measured classical key register; it does not copy arbitrary quantum states.

Facts & Assumptions

Given: The finite nonempty key alphabet, the ordered finite-dimensional registers, and the operators $L_{k}$ in the Statement.

[F1]

Finite registers and their ordered computational bases and Ordered tensor registers, their inner product, and wire permutations: the displayed key vectors and their ordered product vectors form orthonormal bases.

[F2]

A finite Kraus sum is completely positive: any finite map of the form $X \mapsto \sum_{k} L_{k} X L_{k}^{†}$ is completely positive.

[F3]

The basis-independent trace of an endomorphism of a finite-dimensional vector space: trace is the finite sum of diagonal entries, so it is linear over finite sums.

[F4]

For $A \in M_{m \times n} (F)$ and $B \in M_{n \times m} (F)$ , $tr (A B) = tr (B A)$ : for compatible finite-dimensional maps, $tr (L_{k} X L_{k}^{†}) = tr (X L_{k}^{†} L_{k})$ .

[F5]

Finite-dimensional quantum channel: a finite-dimensional quantum channel is a linear, completely positive, trace-preserving map on the full operator space.

[F6]

The adjoint $T^{*} : W \to V$ is characterised by $⟨ T v, w ⟩_{W} = ⟨ v, T^{*} w ⟩_{V}$ : the adjoint is characterized by $⟨ L x, y ⟩ = ⟨ x, L^{†} y ⟩$ for every input $x$ and output $y$ .

Proof

1.1givenF1F6algebra

Let $e$ and $f$ range over an orthonormal product basis of $H_{T} \otimes H_{E}$ . For input basis vector $∣ j ⟩ \otimes e$ and output basis vector $∣ r, s ⟩ \otimes f$ , the definition and orthonormality [F1] give $⟨ L_{k} (∣ j ⟩ \otimes e), ∣ r, s ⟩ \otimes f ⟩ = ⟨ e, f ⟩$ if $j = r = s = k$ , and $0$ otherwise. By the defining adjoint identity [F6] and the fact that these product vectors form bases, $L_{k}^{†} (∣ r, s ⟩ \otimes f) = ∣ k ⟩ \otimes f$ when $r = s = k$ , and is $0$ otherwise. Hence $L_{k}^{†} L_{k} (∣ j ⟩ \otimes e) = ∣ j ⟩ \otimes e$ when $j = k$ and $0$ otherwise. Summing over $k$ proves $\sum_{k \in K} L_{k}^{†} L_{k} = I_{A T E}$ on a basis, so it holds on the full input space.

2.1givenF2F3F4F5step 1.1algebra

The formula in the Statement is a finite Kraus sum, so [F2] makes $C$ completely positive. For every operator $X$ , trace linearity [F3] and cyclicity [F4] give $tr (C (X)) = \sum_{k} tr (X L_{k}^{†} L_{k}) = tr (X \sum_{k} L_{k}^{†} L_{k}) = tr (X)$ by step 1.1. These are precisely the channel conditions [F5].

3.1givenF1F6algebra∎

For $ξ_{A T E} = \sum_{j} ∣ j ⟩ ⟨ j ∣ \otimes ξ_{T E}^{j}$ , the basis action gives $L_{k} ξ_{A T E} L_{k}^{†} = ∣ k, k ⟩ ⟨ k, k ∣ \otimes ξ_{T E}^{k}$ ; all other input-key blocks are annihilated by $L_{k}$ . Summing over $k$ yields the stated copy formula.

Depends on

Used by

Dependency tree · two levels

38 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

Christopher Portmann and Renato Renner, Cryptographic Security of Quantum Key Distribution (2014), §4.3 (standard reference, not scraped)
Joseph M. Renes, Quantum Information Theory, ETH Zürich lecture notes (HS2014; revised 4 February 2015), §8.3 (standard reference, not scraped)
John Watrous, The Theory of Quantum Information (2018), §§1.1.3 and 2.2.2 (standard reference, not scraped)