TheoremStatement: Literature-sourcedProof: 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.

Exact state transfer on the Boolean hypercube

Statement

For every integer $n \geq 0$ , the algorithm Hypercube continuous-time state transfer evolves the initial vector $e_{0^{n}}$ to $U_{A_{n}} (π / 2) e_{0^{n}} = (- i)^{n} e_{1^{n}} .$ Consequently its computational-basis measurement outputs $1^{n}$ with probability one, including the empty word when $n = 0$ .

Facts & Assumptions

Given: An integer $n \geq 0$ , the standard $n$ -qubit register, and $A_{n} = \sum_{j < n} X_{j}$ as in the algorithm.

[F1]

Hypercube continuous-time state transfer: the Hamiltonian is $A_{n} = \sum_{j < n} X_{j}$ and the initial vector is $e_{0^{n}}$ .

[F2]

Finite registers and their ordered computational bases: the computational basis is the ordered standard basis of $C^{2}$ on each qubit.

[F3]

Ordered tensor registers, their inner product, and wire permutations: the product basis of an ordered tensor register is the lexicographically ordered tensor of its factor bases; the empty tensor product is $C$ .

[F4]

Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely: a finite normal endomorphism has an orthonormal eigenbasis.

[F5]

$\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential: $e^{z + w} = e^{z} e^{w}$ for complex $z, w$ .

[F6]

$\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ : $e^{i t} = \cos t + i \sin t$ for real $t$ .

[F7]

Quarter-turn values and shifts by pi/2 and pi: $\cos (π / 2) = 0$ and $\sin (π / 2) = 1$ .

[F8]

The measurement law for a finite continuous-time walk: in a finite register, the computational-basis outcome probability is the squared modulus of the corresponding output coordinate.

[F9]

Finite Hermitian matrix dynamics: $U_{A_{n}} (t)$ acts on an eigenvector of $A_{n}$ with eigenvalue $λ$ by multiplication by $e^{- i t λ}$ .

[F10]

Tensor products of finitely many linear maps: tensor maps act factorwise on elementary tensors; the empty tensor map is the identity on $C$ .

Proof

technique · direct

1.1givenF1F2F3F10algebra

In $C^{2}$ , put $f_{+} = (e_{0} + e_{1}) / \sqrt{2}$ and $f_{-} = (e_{0} - e_{1}) / \sqrt{2}$ . Direct inner-product calculation makes $(f_{+}, f_{-})$ an orthonormal basis, and direct matrix multiplication gives $X f_{+} = f_{+}$ and $X f_{-} = - f_{-}$ . By [F3], the vectors $f_{s_{0}} \otimes \dots \otimes f_{s_{n - 1}}$ form an orthonormal basis of the $n$ -qubit register; for $n = 0$ this is the singleton basis of $C$ . By [F10], each $X_{j}$ acts on this vector by $(- 1)^{s_{j}}$ , so $A_{n}$ has the real eigenvalue $\sum_{j < n} (- 1)^{s_{j}}$ . This basis diagonalizes every $X_{j}$ with real eigenvalues as well. Hence $A_{n}$ and each $X_{j}$ are self-adjoint and their finite matrix evolutions are defined.

2.1step 1.1F4F5F9F10algebra

The eigenbasis in step 1.1 and the spectral functional-calculus rule [F4], [F9] give that $U_{A_{n}} (t)$ acts on that basis vector by $e^{- i t \sum_{j} (- 1)^{s_{j}}}$ . Repeated use of [F5] makes this the product of the one-qubit eigenvalues. By [F10], this is the action of $⨂_{j < n} U_{X} (t)$ on that basis vector, so the maps agree on a basis. Also, each $U_{X_{j}} (t)$ acts on the same vector by $e^{- i t (- 1)^{s_{j}}}$ , by step 1.1 and [F4], [F9]. Their chronological composition $U_{X_{n - 1}} (t) \dots U_{X_{0}} (t)$ therefore has the same eigenvalue $e^{- i t \sum_{j} (- 1)^{s_{j}}}$ on every basis vector. It equals $U_{A_{n}} (t)$ , so the local-operation branch implements the whole evolution. For $n = 0$ , the composition is empty and equals the identity on $C$ .

3.1step 2.1F2F6F7F10algebra

At $t = π / 2$ , the eigenvalues of $U_{X} (t)$ on $f_{+}, f_{-}$ are $- i, i$ by [F6]–[F7]. These are the eigenvalues of $- i X$ on the same basis, so $U_{X} (π / 2) = - i X$ . By [F10], each of the $n$ factors contributes the scalar $- i$ on elementary tensors, and these tensors span the register; hence $U_{A_{n}} (π / 2) = (- i)^{n} X^{\otimes n}$ .

4.1F1F2F10step 2.1step 3.1algebra

Each $X$ exchanges $e_{0}$ and $e_{1}$ , hence [F10] gives $X^{\otimes n} e_{0^{n}} = e_{1^{n}}$ . By step 2.1, both the whole-operation branch and the local-operation branch have net evolution $U_{A_{n}} (π / 2)$ ; step 3.1 therefore gives their output vector $(- i)^{n} e_{1^{n}}$ . For $n = 0$ it reads $I_{C} e_{()} = e_{()}$ .

5.1step 4.1F8algebra∎

The vector in step 4.1 has norm one, and [F8] assigns probability $∣ (- i)^{n} ∣^{2} = 1$ to the outcome $1^{n}$ . Thus every other basis outcome has probability zero.

Depends on

Used by

Small hypercube transfer Example
Continuous-time walk resource accounting Theorem

Dependency tree · two levels

67 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

Andrew M. Childs, Lecture Notes on Quantum Algorithms, Chapter 17 §17.2 (standard reference, not scraped)
Ronald de Wolf, Quantum Computing: Lecture Notes, Chapter 9 §9.1 (standard reference, not scraped)