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.

An explicit syndrome recovery corrects a Knill–Laflamme error family

Statement

Let $V : H_{L} \to H_{P}$ be an isometry with $H_{L} \neq {0}$ and $P = V V^{*}$ . 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})$ . If $P E_{a}^{*} E_{b} P = C_{a b} P$ for all $a, b$ , then there is a finite Kraus recovery channel $R : B (H_{O}) \to B (H_{L})$ satisfying $R \circ N \circ {Ad}_{V} = {id}_{B (H_{L})}$ . It is obtained by diagonalizing $C$ , decoding each nonzero orthogonal error range, and sending the orthogonal complement to a fixed logical state. For this recovery and every $X \in B (H_{L})$ , the off-diagonal error action is $R (E_{a} V X V^{*} E_{b}^{*}) = C_{b a} X$ .

Facts & Assumptions

Given: The finite-dimensional code isometry, the finite Kraus channel, and the displayed scalar-compression condition.

[F1]

Quantum code as an isometric encoding and its code projector: $V$ is an isometric encoding and $P = V V^{*}$ .

[F2]

An isometric quantum encoding gives an orthogonal code projector: $V^{*} V = I_{H_{L}}$ .

[F3]

Finite-dimensional quantum channel and Finite Kraus representation: channels are completely positive and trace-preserving, and a finite Kraus family represents the map on the full operator space.

[F4]

Trace preservation is Kraus normalization: a finite Kraus representation is trace-preserving exactly when its adjoint-square sum is the identity.

[F5]

A finite Kraus sum is completely positive: every finite Kraus sum is completely positive.

[F6]

A unitary error-basis change gives orthogonal error ranges: after unitary error mixing, each nonzero restriction is $\sqrt{λ_{i}} W_{i}$ with $W_{i}^{*} W_{j} = δ_{i j} I$ ; zero-eigenvalue restrictions vanish.

[F7]

Orthogonal error restrictions determine syndrome projections: the ranges of the $W_{i}$ have orthogonal projections $P_{i} = W_{i} W_{i}^{*}$ and $Q = I - \sum_{i} P_{i}$ is the projection onto their orthogonal complement.

[F8]

Every finite-dimensional real or complex inner product space has an orthonormal basis: every finite-dimensional inner-product space has an orthonormal basis, including its finite-dimensional subspaces.

[F9]

The adjoint $T^{*} : W \to V$ is characterised by $⟨ T v, w ⟩_{W} = ⟨ v, T^{*} w ⟩_{V}$ , Every linear map between finite-dimensional inner product spaces has a unique adjoint, and Adjoints satisfy $(S + T)^{*} = S^{*} + T^{*}$ , $(λ T)^{*} = \overline{λ} T^{*}$ , $(S T)^{*} = T^{*} S^{*}$ , and $T^{* *} = T$ : adjoints exist uniquely in finite dimension, $T^{* *} = T$ , and $(S T)^{*} = T^{*} S^{*}$ .

[F10]

Agreement on pure states implies complete agreement: if two complex-linear maps agree on all rank-one projectors, they agree on the whole operator space and after tensoring with the identity on any finite reference.

Proof

1.1givenF1F6

Apply [F6] to diagonalize the coefficient matrix and replace the Kraus operators by the unitarily mixed family $F_{i}$ . The operator-sum map remains $N$ , the positive eigenvalues are $λ_{i}$ , and $F_{i} V = \sqrt{λ_{i}} W_{i}$ for $λ_{i} > 0$ , while $F_{i} V = 0$ when $λ_{i} = 0$ .

1.2F7F8constructchoose

For each $λ_{i} > 0$ , define $R_{i} = W_{i}^{*} : H_{O} \to H_{L}$ . Choose a unit vector $ℓ_{0} \in H_{L}$ and an orthonormal basis $(q_{s})$ of $Q H_{O}$ using [F8]; for each basis vector define $T_{s} x = ⟨ x, q_{s} ⟩ ℓ_{0}$ . These are finite Kraus operators.

2.1givenF2F4step 1.1algebra

Trace preservation [F4] and $V^{*} V = I$ from [F2] give $V^{*} (\sum_{i} F_{i}^{*} F_{i}) V = I_{H_{L}}$ . Using step 1.1, the left side is $(\sum_{i} λ_{i}) I_{H_{L}}$ . Since $H_{L}$ is nonzero, $\sum_{i} λ_{i} = 1$ .

2.2F3F4F5F7F9step 1.2algebra

By [F9], $R_{i}^{*} R_{i} = W_{i} W_{i}^{*}$ . From $T_{s} x = ⟨ x, q_{s} ⟩ ℓ_{0}$ and the adjoint definition, $T_{s}^{*} y = ⟨ y, ℓ_{0} ⟩ q_{s}$ ; hence $T_{s}^{*} T_{s} x = ⟨ x, q_{s} ⟩ q_{s}$ . Summing over the orthonormal basis of $Q H_{O}$ gives $\sum_{s} T_{s}^{*} T_{s} = Q$ . Therefore $\sum_{λ_{i} > 0} R_{i}^{*} R_{i} + \sum_{s} T_{s}^{*} T_{s} = \sum_{λ_{i} > 0} W_{i} W_{i}^{*} + Q = I_{H_{O}}$ by [F7]. The finite Kraus map is completely positive by [F5] and trace-preserving by [F4], so it is a recovery channel.

3.1step 1.1step 2.1step 1.2F6F7F9algebra

For positive $λ_{j}$ , $R_{i} F_{j} V = \sqrt{λ_{j}} W_{i}^{*} W_{j} = δ_{i j} \sqrt{λ_{j}} I_{H_{L}}$ ; if $λ_{j} = 0$ then $F_{j} V = 0$ . Also $T_{s} F_{j} V = 0$ because $Q W_{j} = 0$ . Hence for every $X \in B (H_{L})$ , $(R \circ N \circ {Ad}_{V}) (X) = \sum_{j} λ_{j} X = X$ by step 2.1.

4.1step 3.1F10

The equality in step 3.1 is equality of linear maps on all operators. Tensoring that equality with the identity on any finite reference gives the same equality there by [F10].

5.1step 1.1step 1.2step 2.2step 3.1F6F7F9algebra∎

The same recovery Kraus actions in step 3.1 show $R (F_{i} V X V^{*} F_{j}^{*}) = δ_{i j} λ_{i} X$ for every $X \in B (H_{L})$ ; zero-eigenvalue terms vanish because $F_{i} V = 0$ . Since $F_{i} = \sum_{a} E_{a} U_{a i}$ , unitarity gives $E_{a} = \sum_{i} F_{i} \overline{U_{a i}}$ . Therefore $R (E_{a} V X V^{*} E_{b}^{*}) = \sum_{i} \overline{U_{a i}} U_{b i} λ_{i} X = C_{b a} X$ , using $C = U diag (λ_{i}) U^{*}$ .

Depends on

Used by

Distance corrects unlocated errors and known erasures Corollary
Fault-Tolerant Gadget and Proper-Code Contract Definition
A degenerate code with a non-diagonal Knill–Laflamme matrix Example
Orthogonal error spaces and a recovery branch Example
CSS syndrome correction Theorem
Stabilizer distance detection and correction Theorem
The Knill–Laflamme criterion for a protected subsystem Theorem

Dependency tree · two levels

53 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)