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

Product operator matrix units form a basis

Statement

Let $H_{G}, H_{Q}$ be finite-dimensional complex inner-product spaces with fixed ordered orthonormal bases $(g_{s})_{s < m}$ and $(q_{α})_{α < n}$ ; either index set may be empty. Put $B (H) = {End}_{C} (H)$ . For each $s, t < m$ and $α, β < n$ , define $M_{s α, t β} x = ⟨ x, g_{t} \otimes q_{β} ⟩ (g_{s} \otimes q_{α}) .$ Then the family $(M_{s α, t β})_{s, t, α, β}$ is a basis of $B (H_{G} \otimes H_{Q})$ . If either factor is zero-dimensional, this is the empty basis of the zero endomorphism space.

Facts & Assumptions

Given: The finite-dimensional spaces and their ordered orthonormal bases in the Statement.

[F1]

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, so $x \mapsto ⟨ x, v ⟩$ is linear for fixed $v$ .

[F2]

The product basis is orthonormal and tensor dimensions multiply: the elementary product tensors $g_{s} \otimes q_{α}$ form an orthonormal basis of $H_{G} \otimes H_{Q}$ , including the empty and zero-dimensional cases.

[F3]

Linear map between vector spaces over the same field: a linear map is determined by its values on a spanning set.

[F4]

A finite list $v : n \to V$ is an ordered basis if and only if every $x \in V$ equals $\sum_{i < n} λ_{i} v_{i}$ for exactly one $λ : n \to F$ ; those scalars are the coordinates of $x$ in that ordered basis: each vector has a unique finite coordinate expansion in an ordered basis.

Proof

1.1F1F2algebra

By [F1], each $M_{s α, t β}$ is linear. Applying it to a product basis vector gives $M_{s α, t β} (g_{t^{'}} \otimes q_{β^{'}}) = g_{s} \otimes q_{α}$ when $(t^{'}, β^{'}) = (t, β)$ and $0$ otherwise, by [F2]. Thus these operators have the individual matrix-unit columns of the product basis.

2.1givenF2F3F4step 1.1algebra∎

If either basis is empty, [F2] makes $H_{G} \otimes H_{Q} = {0}$ ; its endomorphism space is the zero vector space, whose empty family is a basis, as asserted. Otherwise, for any $T \in B (H_{G} \otimes H_{Q})$ and each input basis vector $g_{t} \otimes q_{β}$ , write $T (g_{t} \otimes q_{β}) = \sum_{s, α} c_{s α, t β} (g_{s} \otimes q_{α})$ using [F2, F4]. The finite sum $\sum_{s, α, t, β} c_{s α, t β} M_{s α, t β}$ has the same value as $T$ on every basis vector by step 1.1, hence equals $T$ by [F3]. If a linear combination of the $M_{s α, t β}$ is zero, applying it to each input basis vector shows each coefficient is zero by [F2]. Therefore this family spans and is linearly independent.

Depends on

Used by

Dependency tree · two levels

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