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 local gate has a unique global wire embedding

Statement

Let $n \geq r \geq 1$ , let $w = (w_{0}, \dots, w_{r - 1})$ be an ordered tuple of distinct wires in $[n]$ , and let $U : Q_{r} \to Q_{r}$ be unitary. There is a unique unitary ${\tilde{U}}_{w} : Q_{n} \to Q_{n}$ that applies $U$ to the ordered wires $w_{0}, \dots, w_{r - 1}$ and acts as the identity on the other wires.

Facts & Assumptions

Given: The finite ordered register $Q_{n}$ , distinct target wires $w_{0}, \dots, w_{r - 1}$ , and a unitary $U$ on $Q_{r}$ .

[F1]

Finite circuit syntax and ordered wire labels: a gate occurrence names distinct wires in a specified order.

[F2]

Ordered tensor registers, their inner product, and wire permutations: the computational product basis is orthonormal, and the reordering of wire factors is the linear extension of its bijection on that basis.

[F3]

Tensor products of finitely many linear maps: the tensor map $U \otimes I$ acts on elementary tensors as $x \otimes z \mapsto U x \otimes z$ .

[F4]

Tensor maps preserve composition, identities, and adjoints: $(U \otimes I)^{†} = U^{†} \otimes I$ and tensor maps preserve composition and identities.

[F5]

Linear isometries, and orthogonal or unitary operators on finite-dimensional inner product spaces: a unitary is an invertible linear norm-preserving map. For an endomorphism in finite dimension, preserving lengths, preserving inner products, carrying orthonormal bases to orthonormal bases, and $T^{*} T = I$ are equivalent: a finite-dimensional unitary $U$ satisfies $U^{†} U = U U^{†} = I$ .

[F6]

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

Proof

1.1givenF1F2construct

List the complement wires as $c_{0} < \dots < c_{n - r - 1}$ . The rule $∣ x_{0}, \dots, x_{n - 1} ⟩ \mapsto ∣ x_{w_{0}}, \dots, x_{w_{r - 1}} ⟩ \otimes ∣ x_{c_{0}}, \dots, x_{c_{n - r - 1}} ⟩$ is a bijection from the computational basis of $Q_{n}$ to the product basis of $Q_{r} \otimes Q_{n - r}$ : the output lists each original coordinate once and records which coordinate occupies each position. Its linear extension $P_{w}$ sends one orthonormal basis bijectively to another, hence is unitary by [F2].

2.1givenstep 1.1F3F4F5F6algebra

Put $T = U \otimes I_{Q_{n - r}}$ . By [F3]–[F5], $T^{†} T = (U^{†} U) \otimes I = I$ and $T T^{†} = (U U^{†}) \otimes I = I$ . Thus $T^{†}$ is a two-sided inverse, and [F6] gives $∥ T z ∥^{2} = ⟨ T z, T z ⟩ = ⟨ z, T^{†} T z ⟩ = ∥ z ∥^{2}$ for every $z$ . Hence $T$ is unitary. Since $P_{w}$ is a surjective isometry by step 1.1, its inverse also preserves norms: for $y = P_{w} x$ , $∥ P_{w}^{- 1} y ∥ = ∥ x ∥ = ∥ P_{w} x ∥ = ∥ y ∥$ . Therefore the composite ${\tilde{U}}_{w} = P_{w}^{- 1} (U \otimes I_{Q_{n - r}}) P_{w}$ is invertible and norm-preserving, hence unitary by [F5]. Its action, by the definition of $P_{w}$ , applies $U$ to the selected factors in tuple order and leaves the complement factors fixed, as required.

3.1step 2.1algebra∎

The computational basis spans $Q_{n}$ . Any linear map with the specified action on its basis vectors is unique, so the embedding in step 2.1 is the unique one.

Depends on

Used by

Denotational semantics of a finite layered circuit Definition
Graph state of an ordered finite simple graph Definition
QFT circuit order and truncation examples Example
Clifford+T circuit entries lie in the dyadic cyclotomic ring Lemma
Exact Gray-code synthesis of multiplexed y- and z-axis rotations Lemma
Gates on disjoint wires commute Lemma
Clean ancilla controlled T circuit is exact Proposition
Exact binary QFT circuit correctness Theorem
Exact finite unitary synthesis from cosine-sine recursion Theorem
Finite universal-gate compilation cost for the truncated QFT Theorem
Operator-norm error of QFT truncation Theorem
Reversing a circuit implements its inverse Theorem
Two-qubit determinant obstruction to controlled T Theorem

Dependency tree · two levels

32 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 5: Classical and Quantum Circuits (standard reference, not scraped)
Ronald de Wolf, Quantum Computing: Lecture Notes, arXiv:1907.09415v6 (standard reference, not scraped)