CorollaryStatement: 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.

Distance corrects unlocated errors and known erasures

Statement

Let $V : H_{L} \to H_{P}$ be an isometric encoding into an ordered register of $n$ finite factors, as in Quantum code as an isometric encoding and its code projector, with code projector $P = V V^{*}$ and quantum distance $d$ as in Detectable operators and distance of a finite-register quantum code. Let $N (X) = \sum_{a} E_{a} X E_{a}^{*}$ be a channel on $H_{P}$ with a finite Kraus family, and let $t \geq 0$ be an integer. Support and weight have the factor-order convention of Support and weight of an operator on a finite register. If every Kraus error $E_{a}$ has weight at most $t$ and $2 t < d$ , then the code is exactly correctable. If a fixed, known erased set $S \subseteq [n]$ supports every Kraus error and $∣ S ∣ < d$ , then the code is exactly correctable. The first claim permits different unknown supports; the second uses the one known support.

Facts & Assumptions

Given: The finite code isometry and channel in the Statement, together with the stated support hypotheses.

[F1]

Support and weight of an operator on a finite register: $E$ is supported in $S$ when the declared factor permutation makes it $E_{S} \otimes I_{S^{c}}$ , and $wt (E)$ is the minimum support size.

[F2]

Finite registers and their ordered computational bases, Ordered tensor registers, their inner product, and wire permutations, Tensor products of finitely many linear maps, The adjoint $T^{*} : W \to V$ is characterised by $⟨ T v, w ⟩_{W} = ⟨ v, T^{*} w ⟩_{V}$ , Adjoints satisfy $(S + T)^{*} = S^{*} + T^{*}$ , $(λ T)^{*} = \overline{λ} T^{*}$ , $(S T)^{*} = T^{*} S^{*}$ , and $T^{* *} = T$ , Tensor maps preserve composition, identities, and adjoints, and Finite wire permutations are unitary basis permutations: the register factors have the declared order; tensor maps act factorwise, preserve composition and adjoints, and wire permutations are bijective isometries of the ordered product spaces.

[F3]

Detectable operators and distance of a finite-register quantum code and Every operator below the quantum code distance is detectable: an operator of weight strictly below $d$ compresses to a scalar multiple of $P$ .

[F4]

Finite Kraus representation and Finite-dimensional quantum channel: the finite Kraus family represents a CPTP map.

[F5]

An explicit syndrome recovery corrects a Knill–Laflamme error family: if all products $E_{a}^{*} E_{b}$ compress to scalar multiples of the code projector, a finite trace-preserving recovery corrects the channel.

Proof

1.1givenF1F2choosealgebra

Fix Kraus errors $E_{a}, E_{b}$ and choose supports $S_{a}, S_{b}$ with $∣ S_{a} ∣, ∣ S_{b} ∣ \leq t$ , as allowed by [F1]. Put $U = S_{a} \cup S_{b}$ . Since $S_{a}, S_{b} \subseteq U$ , extend each local operator by identity on the additional factors of $U$ and use the wire permutations in [F2] to put both operators in the same factor order $H_{U} \otimes H_{U^{c}}$ . On every product basis vector in that order, each conjugated error acts on its own $S_{a}$ or $S_{b}$ coordinates and leaves every other coordinate fixed. The tensor-map definition in [F2] therefore gives forms ${\tilde{E}}_{a} \otimes I_{U^{c}}$ and ${\tilde{E}}_{b} \otimes I_{U^{c}}$ . The adjoint and composition identities in [F2] give $E_{a}^{*} E_{b} = ({\tilde{E}}_{a}^{*} {\tilde{E}}_{b}) \otimes I_{U^{c}}$ in that order. Thus $E_{a}^{*} E_{b}$ is supported in $U$ and has weight at most $∣ U ∣ \leq ∣ S_{a} ∣ + ∣ S_{b} ∣ \leq 2 t < d$ .

2.1step 1.1F3F4F5

By [F3], each product in step 1.1 is detectable, so there are scalars $C_{a b}$ with $P E_{a}^{*} E_{b} P = C_{a b} P$ . Applying [F5] gives one recovery for the entire Kraus family.

3.1givenF1F2F3F4F5algebra∎

If the known affected set is a fixed $S$ , every $E_{a}$ acts as the identity outside $S$ , and so does every product $E_{a}^{*} E_{b}$ by [F1,F2]. Its weight is at most $∣ S ∣ < d$ . Applying [F3] and then [F5] gives exact recovery. This uses the one known support $S$ rather than a union of two unknown supports.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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