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 Knill–Laflamme coefficient matrix is positive

Statement

Let $H_{L}, H_{P}, H_{O}$ be finite-dimensional complex inner-product spaces, $V : H_{L} \to H_{P}$ an isometric encoding of nonzero logical space, and $P = V V^{*}$ . For a finite family of linear error operators $E_{1}, \dots, E_{m} : H_{P} \to H_{O}$ , suppose scalars $C_{a b}$ satisfy $P E_{a}^{*} E_{b} P = C_{a b} P$ for all $a, b$ . Then the matrix $C = (C_{a b})$ is Hermitian positive semidefinite.

Facts & Assumptions

Given: The finite-dimensional encoding and error family in the Statement, and the displayed Knill–Laflamme scalar-compression identities.

[F2]

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

[F3]

Real and complex inner product spaces, with the inner product linear in the first argument: the complex inner product is linear in its first argument and conjugate-linear in its second.

[F4]

The adjoint $T^{*} : W \to V$ is characterised by $⟨ T v, w ⟩_{W} = ⟨ v, T^{*} w ⟩_{V}$ and Every linear map between finite-dimensional inner product spaces has a unique adjoint: finite-dimensional maps have unique adjoints satisfying $⟨ T u, v ⟩ = ⟨ u, T^{*} v ⟩$ .

Proof

1.1givenF2F4choosealgebra

By [F2], $P V = V$ , $V^{*} P = V^{*}$ and $V^{*} V = I_{H_{L}}$ . Multiplying $P E_{a}^{*} E_{b} P = C_{a b} P$ by $V^{*}$ and $V$ therefore gives $V^{*} E_{a}^{*} E_{b} V = C_{a b} I_{H_{L}}$ . Choose a unit vector $ψ \in H_{L}$ , possible because $H_{L} \neq {0}$ . The adjoint identity [F4] yields $C_{a b} = ⟨ E_{a}^{*} E_{b} V ψ, V ψ ⟩ = ⟨ E_{b} V ψ, E_{a} V ψ ⟩$ .

2.1step 1.1F3algebra∎

For any $z = (z_{1}, \dots, z_{m}) \in C^{m}$ , the first-argument linearity and conjugate symmetry in [F3] give $z^{*} C z = \sum_{a, b} \overline{z_{a}} z_{b} ⟨ E_{b} V ψ, E_{a} V ψ ⟩ = {∥ \sum_{b} z_{b} E_{b} V ψ ∥}^{2} \geq 0.$ Also $C_{b a} = \overline{C_{a b}}$ , so $C$ is Hermitian. The nonnegative quadratic form is exactly positive semidefiniteness.

Depends on

Used by

A unitary error-basis change gives orthogonal error ranges Lemma

Dependency tree · two levels

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