LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

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.

Gray-Code Synthesis of a Multiplexed Axis Rotation

Statement

Let $k \geq 0$ controls have computational labels $x \in {0, 1}^{k}$ , and let $θ_{x} \in R$ . Fix $a \in {x, y, z}$ . On one target qubit define $M = \sum_{x \in {0, 1}^{k}} ∣ x ⟩ ⟨ x ∣ \otimes R_{a} (θ_{x}), R_{a} (t) = \exp (- i t σ_{a} / 2) .$ Then $M$ is exactly synthesized with $2^{k}$ CNOTs for $k > 0$ (the final CNOT restores the parity network). For $a = y, z$ it uses $2^{k}$ target rotations $R_{a} (β_{j})$ ; for $a = x$ it uses $2^{k}$ $R_{y}$ rotations in the fixed target basis described below; for $k = 0$ it is one rotation and no CNOT. For $a = x$ and $k > 0$ the implementation also uses two fixed target basis-change gates; the $y, z$ implementations need none. One may replace the cyclic Gray traversal by a traversal that omits the final restoration and absorb that final parity into the next block only when that block is explicitly specified.

Facts & Assumptions

Given: The real angles $(θ_{x})$ , the computational-basis order on the controls, and the rotation convention $R_{a} (t) = \exp (- i t σ_{a} / 2)$ . For a control bit $x_{r}$ and target bit $b$ , define ${C N O T}_{r \to t} ∣ x, b ⟩ = ∣ x, b \oplus x_{r} ⟩$ , extending linearly; its matrix is a permutation and is self-inverse.

[F1]

Big-endian encoding of ordered bit strings: the ordered $n$ -qubit basis assigns bit word $x$ the big-endian index ${enc}_{n} (x) = \sum_{r < n} x_{r} 2^{n - 1 - r}$ , so the first wire is the most significant bit.

[F2]

Pauli formula for an axis rotation: $R_{n} (t) = \cos (t / 2) I - i \sin (t / 2) (n \cdot σ)$ for real unit $n$ .

[F3]

The Pauli matrices: $Y = (\begin{matrix} 0 & - i \\ i & 0 \end{matrix})$ in the ordered computational basis.

[F4]

CNOT and Control-Target Order: the first-wire-control CNOT maps $∣ a, t ⟩$ to $∣ a, t \oplus a ⟩$ and is self-inverse.

[F5]

Denotational semantics of a finite layered circuit: later-applied gates multiply on the left of earlier gates in the circuit denotation.

[F6]

Finite circuit resource accounting: the declared gate count is the number of occurrences from the operation model's allowed alphabet.

[F7]

The computational basis is orthonormal: the ordered computational basis is orthonormal.

Proof

1.1givenF1choosealgebra

For $k > 0$ , construct the reflected list $G_{1} = (0, 1)$ and $G_{k} = (0 G_{k - 1}, 1 rev (G_{k - 1}))$ for $k \geq 2$ . Induction shows that each mask occurs once, adjacent masks differ in one coordinate, and the last mask differs from the first in one coordinate. Enumerate these $2^{k}$ masks as $p_{j}$ , beginning at $p_{0} = 0$ . For $k = 0$ , take the singleton list containing the empty mask and use no coordinate transition. Set $H_{x j} = (- 1)^{p_{j} \cdot x}$ and choose $β_{j} = 2^{- k} \sum_{y} H_{y j} θ_{y}$ . For $z = x \oplus y$ , summing over all masks factors as $\sum_{p} (- 1)^{p \cdot z} = \prod_{r = 0}^{k - 1} (1 + (- 1)^{z_{r}})$ , which equals $2^{k}$ when $z = 0$ and $0$ otherwise. Substituting the chosen $β_{j}$ therefore gives $\sum_{j} H_{x j} β_{j} = θ_{x}$ .

2.1step 1.1F2F3F4F5F6F7algebra

Assume $k > 0$ . Substitute $n = (0, 1, 0)$ in [F2] and use [F3]; this gives $R_{y} (t) = (\begin{matrix} \cos (t / 2) & - \sin (t / 2) \\ \sin (t / 2) & \cos (t / 2) \end{matrix})$ . Apply $R_{y} (β_{0})$ , then toggle the single control coordinate taking $p_{0}$ to $p_{1}$ with a CNOT and apply $R_{y} (β_{1})$ , continuing through $p_{2^{k} - 1}$ and using one final CNOT to restore mask $0$ . On a fixed control basis state $∣ x ⟩$ , the accumulated target bit flip before the $j$ th rotation is $p_{j} \cdot x$ modulo two by [F4]. The CNOT network consists of basis permutations and hence is unitary by [F7]. Conjugation by $X$ gives $X R_{y} (t) X = R_{y} (- t)$ by direct multiplication of the displayed matrix, so that rotation acts as $R_{y} ((- 1)^{p_{j} \cdot x} β_{j})$ . Its ordered application agrees with [F5], and [F6] counts these gate occurrences.

3.1step 1.1step 2.1F2F3algebra

Direct multiplication of the $R_{y}$ matrices from step 2.1 gives $R_{y} (s) R_{y} (t) = R_{y} (s + t)$ . Thus on branch $x$ the target product is $R_{y} (\sum_{j} H_{x j} β_{j}) = R_{y} (θ_{x})$ by step 1.1. The final CNOT returns the parity network to zero and hence leaves no extra control-dependent permutation. This proves the exact block action for every computational branch; linearity proves it on every superposition. For $k = 0$ , there is one branch and the circuit is just $R_{y} (θ_{0})$ .

4.1step 1.1step 2.1step 3.1F2algebra∎

For $a = z$ , use exactly the same masks and angles with $R_{z}$ in place of $R_{y}$ : the diagonal formula $R_{z} (t) = diag (e^{- i t / 2}, e^{i t / 2})$ gives $X R_{z} (t) X = R_{z} (- t)$ and $R_{z} (s) R_{z} (t) = R_{z} (s + t)$ , proving the same branch calculation. For $a = x$ , put $B = R_{z} (- π / 2)$ . Direct Pauli multiplication gives $B Y B^{*} = X$ , hence $B R_{y} (t) B^{*} = R_{x} (t)$ by [F2]. Conjugate the entire $y$ circuit by the two target gates $B^{*}, B$ in chronological order. Its branch action is $B R_{y} (θ_{x}) B^{*} = R_{x} (θ_{x})$ . This implementation retains the original $y$ network unchanged between the two external basis changes, so it has exactly $2^{k}$ CNOTs, $2^{k}$ $R_{y}$ rotations, and those two additional one-qubit gates. For $k = 0$ , directly apply $R_{a} (θ_{0})$ .

Depends on

Used by

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

Vivek V. Shende, Stephen S. Bullock, and Igor L. Markov, Synthesis of Quantum Logic Circuits, arXiv:quant-ph/0406176v5 (standard reference, not scraped)
Ronald de Wolf, Quantum Computing: Lecture Notes, arXiv:1907.09415v6 (standard reference, not scraped)