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.

A unitary error-basis change gives orthogonal error ranges

Statement

Let $V : H_{L} \to H_{P}$ be an isometry with $H_{L} \neq {0}$ and $P = V V^{*}$ . Let $E_{1}, \dots, E_{m} : H_{P} \to H_{O}$ be a finite family satisfying $P E_{a}^{*} E_{b} P = C_{a b} P$ , and let $C$ be the resulting positive matrix. There is a unitary matrix $U$ such that for $F_{i} = \sum_{a} E_{a} U_{a i}$ one has $\sum_{i} F_{i} X F_{i}^{*} = \sum_{a} E_{a} X E_{a}^{*}$ for every $X$ , and $V^{*} F_{i}^{*} F_{j} V = δ_{i j} λ_{i} I_{H_{L}}$ with $λ_{i} \geq 0$ . If $λ_{i} = 0$ , then $F_{i} V = 0$ ; if $λ_{i} > 0$ , then $W_{i} = F_{i} V / \sqrt{λ_{i}}$ is an isometry and the ranges of the $W_{i}$ are pairwise orthogonal.

Facts & Assumptions

Given: The finite-dimensional isometry and error family in the Statement.

[F2]

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

[F3]

The Knill–Laflamme coefficient matrix is positive: the scalar matrix $C$ in $P E_{a}^{*} E_{b} P = C_{a b} P$ is Hermitian positive semidefinite.

[F4]

Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely: a Hermitian endomorphism of a finite-dimensional complex inner-product space has an orthonormal eigenbasis.

[F5]

Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ : each nonnegative real number has a unique nonnegative square root.

[F6]

Adjoints satisfy $(S + T)^{*} = S^{*} + T^{*}$ , $(λ T)^{*} = \overline{λ} T^{*}$ , $(S T)^{*} = T^{*} S^{*}$ , and $T^{* *} = T$ : $(A B)^{*} = B^{*} A^{*}$ and $(λ A)^{*} = \overline{λ} A^{*}$ for compatible finite-dimensional maps.

[F7]

Real and complex inner product spaces, with the inner product linear in the first argument: the inner product is linear in its first argument and defines the norm by $∥ x ∥^{2} = ⟨ x, x ⟩$ .

Proof

1.1F3F4F5algebra

By [F3], $C$ is Hermitian positive semidefinite. Apply [F4] to obtain a unitary $U$ with $U^{*} C U = diag (λ_{1}, \dots, λ_{m})$ . For each eigenvector $u_{i}$ , positivity gives $λ_{i} = u_{i}^{*} C u_{i} \geq 0$ , and [F5] supplies $\sqrt{λ_{i}}$ .

1.2givenF6algebra

Expand the transformed operator sum. Unitarity and [F6] give $\sum_{i} F_{i} X F_{i}^{*} = \sum_{a, b} (\sum_{i} U_{a i} \overline{U_{b i}}) E_{a} X E_{b}^{*} = \sum_{a} E_{a} X E_{a}^{*} .$ Thus mixing preserves the represented map, including every zero-on-code error.

2.1givenF2step 1.1algebra

Compress the transformed products by $V$ . The scalar-compression identities and [F2] give $V^{*} F_{i}^{*} F_{j} V = (U^{*} C U)_{i j} I_{H_{L}} = δ_{i j} λ_{i} I_{H_{L}}$ .

3.1step 2.1F5F7algebra∎

If $λ_{i} = 0$ , then for every $x \in H_{L}$ , $∥ F_{i} V x ∥^{2} = λ_{i} ∥ x ∥^{2} = 0$ , so $F_{i} V = 0$ . If $λ_{i} > 0$ , then [F5] and step 2.1 give $W_{i}^{*} W_{j} = δ_{i j} I$ for positive eigenvalues. Hence each $W_{i}$ is isometric, and for $i \neq j$ its range is orthogonal to the range of $W_{j}$ .

Depends on

Used by

An explicit syndrome recovery corrects a Knill–Laflamme error family Theorem

Dependency tree · two levels

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