LemmaStatement: AI-adaptedProof: AI-generatedPipeline-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.

Detectable operators form a subspace and quantum distance is well defined

Statement

Let $P$ be the code projector of an isometric encoding into an $n$ -factor register and let $K$ be the logical dimension. Then:

The set $D (P) : = {E : P E P \in C P}$ of detectable operators is a complex linear subspace of $End (H_{P})$ .
Replacing the encoding $V$ by $V U$ for any unitary $U$ on $H_{L}$ leaves $P$ , detectability, and distance unchanged.
If $K = 1$ , every operator is detectable, so the distance convention $n + 1$ is appropriate. If $K \geq 2$ , a non-detectable operator of weight at most $n$ exists, while every weight-zero operator is detectable; hence the minimum defining distance exists and lies in ${1, \dots, n}$ .

Facts & Assumptions

Given: An isometric encoding $V : H_{L} \to H_{P}$ , its code projector $P = V V^{*}$ , logical dimension $K \geq 1$ , and an ordered $n$ -factor register with $n \geq 1$ .

[L1]

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

[L2]

Detectable operators and distance of a finite-register quantum code: $E$ is detectable exactly when $P E P = λ P$ for some scalar, and distance is the minimum weight of a non-detectable operator when $K \geq 2$ .

[L3]

Support and weight of an operator on a finite register: Every operator is supported on the full factor set; scalar identity operators have weight zero.

[L4]

An isometric quantum encoding gives an orthogonal code projector: The code projector is self-adjoint and acts as the identity on its range.

[F1]

Every finite-dimensional real or complex inner product space has an orthonormal basis: Every finite-dimensional inner-product subspace has an orthonormal basis.

[F2]

Orthogonal projection is linear, and an orthonormal basis $(e_{i})$ of $W$ gives $P_{W} v = \sum_{i} ⟨ v, e_{i} ⟩ e_{i}$ : Projection onto a unit vector $u$ acts by $x \mapsto ⟨ x, u ⟩ u$ under the first-variable-linear convention.

[F3]

Adjoints satisfy $(S + T)^{*} = S^{*} + T^{*}$ , $(λ T)^{*} = \overline{λ} T^{*}$ , $(S T)^{*} = T^{*} S^{*}$ , and $T^{* *} = T$ : The adjoint of a compatible composite satisfies $(S T)^{*} = T^{*} S^{*}$ .

[F4]

The adjoint $T^{*} : W \to V$ is characterised by $⟨ T v, w ⟩_{W} = ⟨ v, T^{*} w ⟩_{V}$ : $⟨ P x, u ⟩ = ⟨ x, P^{*} u ⟩$ .

[F5]

Rank-nullity: $\dim_{F} V = nullity T + rank T$ : For a linear map with finite-dimensional domain, $\dim V = \dim \ker T + \dim im T$ .

Proof

1.1L2algebra

If $E, F \in D (P)$ with $P E P = λ P$ and $P F P = μ P$ , then for $a, b \in C$ , $P (a E + b F) P = (a λ + b μ) P$ . Thus $a E + b F \in D (P)$ , proving linearity.

1.2F3L1L2givenalgebra

For a unitary $U$ on $H_{L}$ , [F3] gives $(V U)^{*} = U^{*} V^{*}$ , so $(V U) (V U)^{*} = V U U^{*} V^{*} = V V^{*} = P$ . The same projector gives the same detectable set, operator weights, and distance.

1.3F1F2L1given

If $K = 1$ , choose a unit vector $v$ spanning $im P$ . By [F2], $P x = ⟨ x, v ⟩ v$ , and therefore $P E P x = ⟨ x, v ⟩ ⟨ E v, v ⟩ v = ⟨ E v, v ⟩ P x$ for every $x$ and every $E$ . So every operator is detectable.

2.1F1F2F4F5L1L2L3L4givenalgebra∎

Suppose $K \geq 2$ . If $V x = 0$ , norm preservation gives $∥ x ∥ = 0$ , so positive definiteness gives $x = 0$ ; hence $\ker V = {0}$ . Rank-nullity [F5] gives $\dim im V = \dim H_{L} = K$ . By [L1], $im P = im V$ , so the code subspace is finite-dimensional of dimension at least two. Choose orthonormal $u, v$ in it using [F1], and let $E$ be projection onto $C u$ . Since $P u = u$ and $P = P^{*}$ by [L4], [F2] gives $P E = E$ ; [F4] gives $⟨ P x, u ⟩ = ⟨ x, P^{*} u ⟩ = ⟨ x, u ⟩$ , so $E P = E$ and $P E P = E$ . It cannot equal $λ P$ , since applying both sides to $u$ forces $λ = 1$ while applying them to $v$ forces $λ = 0$ . By [L3], $E$ has weight at most $n$ . If an operator has weight zero, the support definition uses $S = \emptyset$ , so it is $A_{\emptyset} \otimes I = λ I$ and satisfies $P E P = λ P$ . Thus the non-detectable weights form a nonempty subset of ${1, \dots, n}$ and have a minimum.

Remarks

No Pauli-only reduction is used: the definition and proof range over all endomorphisms. The current QC02 register and wire-permutation definitions fix the factor order used by the code and support definitions.

Depends on

Used by

Cited to discharge well-definedness by Detectable operators and distance of a finite-register quantum code.

Dependency tree · two levels

31 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

Richard Cleve, Quantum Information Processing course notes, §§36.1, 36.3, and 37.3 (standard reference, not scraped)
John Preskill, Quantum Computation, Chapter 7, §§7.1 and 7.4.1 (standard reference, not scraped)