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 finite isometry extends after finite ancilla padding

Statement

Let $H, K, E$ be nonzero finite-dimensional complex inner-product spaces and let $V : H \to K \otimes E$ be a linear isometry. Put $h = \dim H$ , $k = \dim K$ , and $e = \dim E$ . Let $A = Q_{k e}$ and $B = Q_{h}$ be the finite-level registers from Finite registers and their ordered computational bases, with first computational basis vectors $a_{0}$ and $b_{0}$ . Then there is a surjective linear isometry $W : H \otimes A ⟶ K \otimes E \otimes B$ such that $W (x \otimes a_{0}) = V x \otimes b_{0}$ for every $x \in H$ .

Facts & Assumptions

Given: Nonzero finite-dimensional complex inner-product spaces $H, K, E$ and a linear isometry $V : H \to K \otimes E$ .

[F1]

Finite registers and their ordered computational bases: for every integer $d \geq 1$ , $Q_{d} = C^{d}$ has the standard coordinate pairing and standard ordered basis. Directly, $⟨ e_{i}, e_{j} ⟩ = \sum_{r < d} δ_{r i} δ_{r j} = δ_{i j}$ , so its computational basis is orthonormal and the specified first vectors of $A = Q_{k e}$ and $B = Q_{h}$ have norm one.

[F2]

Ordered tensor registers, their inner product, and wire permutations: the product inner product on elementary tensors is the product of the factor inner products.

[F3]

$R^{m} \otimes_{R} R^{n} ≅ R^{m n}$ with the product basis, and $\dim_{F} (V \otimes_{F} W) = \dim_{F} V \dim_{F} W$ : finite tensor-product dimensions multiply, including zero-dimensional factors.

[F4]

For a subspace $W$ of a finite-dimensional inner product space, $V = W \oplus W^{⊥}$ : a subspace of a finite-dimensional inner-product space and its orthogonal complement form an internal direct sum.

[F5]

Every finite-dimensional real or complex inner product space has an orthonormal basis: every finite-dimensional inner-product space has an orthonormal basis, including the empty basis.

[F6]

Linear isometries, and orthogonal or unitary operators on finite-dimensional inner product spaces: a linear isometry preserves norms, and a surjective isometry is an isometric isomorphism.

Proof

1.1givenF1F3algebra

Since $h, k, e \geq 1$ , the registers $A = Q_{k e}$ and $B = Q_{h}$ are nonzero. By [F1] and [F3], $\dim (H \otimes A) = h k e = \dim (K \otimes E \otimes B)$ .

1.2givenF1F2F5F6algebra

Choose an orthonormal basis $(u_{i})_{i < h}$ of $H$ using [F5]. By [F2], $(u_{i} \otimes a_{0})_{i < h}$ is orthonormal in $H \otimes A$ . The complex polarization identity for the first-linear inner-product convention, $⟨ x, y ⟩ = \frac{1}{4} (∥ x + y ∥^{2} - ∥ x - y ∥^{2} + i ∥ x + i y ∥^{2} - i ∥ x - i y ∥^{2}),$ and the linearity and norm preservation of $V$ from [F6] give $⟨ V u_{i}, V u_{j} ⟩ = ⟨ u_{i}, u_{j} ⟩ = δ_{i j}$ . Since $b_{0}$ has norm one by [F1], the product inner product [F2] makes $(V u_{i} \otimes b_{0})_{i < h}$ orthonormal in $K \otimes E \otimes B$ . The linear map sending $u_{i} \otimes a_{0}$ to $V u_{i} \otimes b_{0}$ is therefore an isometry between the two $h$ -dimensional subspaces they span.

2.1step 1.1step 1.2F4F5choosealgebra

Let $S$ and $T$ be those two spans. By [F4], each ambient space is the orthogonal direct sum of its span and orthogonal complement. Choose orthonormal bases of $S^{⊥}$ and $T^{⊥}$ by [F5], of lengths $p$ and $q$ . Concatenate each with the corresponding $h$ -vector orthonormal list from step 1.2. Each concatenated list spans its ambient space by the direct-sum decomposition. It is linearly independent: a zero linear combination splits as $s + z = 0$ with $s$ in the span and $z$ in its orthogonal complement, so directness gives $s = z = 0$ , and independence within each list makes every coefficient zero. Thus the concatenated lists are bases; by the definition of dimension, their lengths give $h k e = h + p$ and $h k e = h + q$ using step 1.1. Hence $p = q$ , establishing equal complement dimensions and giving completed orthonormal bases of the full input and output spaces.

3.1givenstep 1.2step 2.1F6construct∎

Map the completed input basis bijectively to the completed output basis, using the prescribed map on $(u_{i} \otimes a_{0})$ . Its linear extension is surjective and preserves inner products because it sends one orthonormal basis to another. It is the required $W$ by [F6]. Linearity gives $W (x \otimes a_{0}) = V x \otimes b_{0}$ for all $x$ . The argument uses only finite basis choices, not a choice axiom.

Remarks

This is a finite-dimensional existence statement only. It gives no decomposition of $W$ into a fixed finite gate alphabet and no gate or bit-cost bound.

Depends on

Used by

Finite instruments can be coherently deferred Theorem

Dependency tree · two levels

37 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 Computation, Chapter 3: Foundations II: Measurement and Evolution (standard reference, not scraped)
Ronald de Wolf, Quantum Computing: Lecture Notes, arXiv:1907.09415v6 (standard reference, not scraped)