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.

Exact recovery implies the Knill–Laflamme condition

Statement

Let $N (X) = \sum_{a = 1}^{m} E_{a} X E_{a}^{*}$ be a finite Kraus representation of a channel from $B (H_{P})$ to $B (H_{O})$ , and let $V : H_{L} \to H_{P}$ be an isometry with $H_{L} \neq {0}$ and $P = V V^{*}$ . If the code is exactly correctable in the sense of Exact recovery of an encoded quantum code, then there are scalars $C_{a b}$ such that $P E_{a}^{*} E_{b} P = C_{a b} P$ for all $a, b$ .

Facts & Assumptions

Given: The finite-dimensional encoding, Kraus channel, and an exact decoded recovery channel $R : B (H_{O}) \to B (H_{L})$ .

[A1]

Exact recovery of an encoded quantum code: exactness means $R \circ N \circ {Ad}_{V}$ is the identity channel on $B (H_{L})$ .

[A2]

Finite-dimensional quantum channel and Finite Kraus representation specify the CPTP channel and finite operator-sum conventions.

[A3]

Kraus and Choi characterizations of complete positivity: every finite-dimensional completely positive map has a finite Kraus representation.

[A4]

Trace preservation is Kraus normalization: a trace-preserving finite Kraus map satisfies $\sum_{j} R_{j}^{*} R_{j} = I$ .

[F1]

Kraus operators in an identity-channel representation are scalar: every operator in a finite Kraus representation of the identity channel is a scalar multiple of the identity.

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

Proof

1.1givenA1A2A3algebrachoose

By [A3], choose a finite Kraus representation $R (X) = \sum_{j} R_{j} X R_{j}^{*}$ . Composing its Kraus operators with the errors $E_{a}$ and the encoding $V$ gives the Kraus family $R_{j} E_{a} V : H_{L} \to H_{L}$ for $R \circ N \circ {Ad}_{V}$ . By exactness [A1], this family represents the identity channel.

2.1step 1.1F1

Apply [F1] to the finite Kraus family in step 1.1. For each $j, a$ there is a scalar $c_{j a}$ with $R_{j} E_{a} V = c_{j a} I_{H_{L}}$ .

3.1A4F2step 2.1algebra

Trace preservation of $R$ gives $\sum_{j} R_{j}^{*} R_{j} = I_{H_{O}}$ by [A4]. Therefore, for every $a, b$ , $V^{*} E_{a}^{*} E_{b} V = V^{*} E_{a}^{*} (\sum_{j} R_{j}^{*} R_{j}) E_{b} V = \sum_{j} (R_{j} E_{a} V)^{*} (R_{j} E_{b} V) = (\sum_{j} \overline{c_{j a}} c_{j b}) I_{H_{L}} .$

4.1givenstep 3.1algebra∎

Put $C_{a b} = \sum_{j} \overline{c_{j a}} c_{j b}$ . Since $P = V V^{*}$ , $P E_{a}^{*} E_{b} P = V (V^{*} E_{a}^{*} E_{b} V) V^{*} = C_{a b} P$ by step 3.1. This is the Knill–Laflamme condition for every pair of errors.

Depends on

Used by

The Knill–Laflamme criterion for a protected subsystem Theorem

Dependency tree · two levels

34 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 Preskill, Quantum Information, Chapter 7: Quantum Error Correction (working draft, March 2026) (standard reference, not scraped)
David W. Kribs, Raymond Laflamme, David Poulin, and Maia Lesosky, Operator Quantum Error Correction (standard reference, not scraped)