Correctness of Gray-Path Two-Level Synthesis

By [F2] and [F3], each path swap is an $X$ controlled on the other bits' fixed values, so it exchanges exactly the two indicated basis labels and fixes every other basis vector. Each swap is a permutation of the orthonormal computational basis [F6], hence a unitary. Their chronological product $P$ sends $x=g_0$ to $g_{d-1}$ and fixes $y=g_d$, because the last path edge is deliberately omitted.

For the algorithm's single-control list $S$, direct multiplication of the rotation matrices in [F11] gives $ABC=I$ and $AXBXC=e^{-i\delta }W$. Its two control branches therefore have target blocks $I$ and $e^{-i\delta }W$; the final phase gate makes them $I,W$ exactly, as required by [F9]. The list in [F10] contains exactly two CNOTs and four one-qubit occurrences, even when one is the identity. For the fixed matrix $J$, the orthogonal projectors $(I+X)\mathrm{/}2$ and $(I-X)\mathrm{/}2$ give $J^2=X$ and unitarity. The list $T(a,b;t)$ restores $b$ and applies target exponent $b-(b\oplus a)+a=2ab$ of $J$, hence is exactly Toffoli. Its cost is $3(2,4)+(2,0)=(8,12)$.

For the ladder $L$ of [F10] with $s\ge 3$, each of its two compute/target/uncompute lists restores all spares, since the central $H$ changes only the target. Let $u_j,v_j$ be the values of $a_j$ just before $H$ in the first and second lists. The common initial spare values give $u_1=a_1\oplus c_1{c}_2$, $v_1=a_1$ and $u_j=a_j\oplus c_{j+1}{u}_{j-1}$, $v_j=a_j\oplus c_{j+1}{v}_{j-1}$ for $j\ge 2$. Induction yields $u_j\oplus v_j={\prod }_{h=1}^{j+1}{c}_h$, so the two target toggles sum to $c_s(u_{s-2}\oplus v_{s-2})={\prod }_{h=1}^s{c}_h$. Thus $L$ is the exact controlled $X$ and restores its arbitrary spares. Its lists contain $2s-3$ and $2s-5$ Toffolis, giving $E_s=(4s-8)(8,12)$; the CNOT and Toffoli base cases give $E_1,E_2$.

At the level of ideal data gates, let $M$ be the middle operation and $P$ the forward swap permutation. The middle gate acts only on $(g_{d-1},g_d)$; using $XVX$ when the target bit of $g_{d-1}$ is $1$ makes its ordered action exactly $V$. By [F4], the data product is $P^{\ast }MP$. Since $P$ sends $(x,y)$ to $(g_{d-1},g_d)$ and no other basis vector into this active pair, the conjugate acts by $V$ on $(x,y)$ and fixes every other data basis vector. Thus the ideal data circuit is the exact two-level unitary, including its scalar phase.

For the balanced list $D$ in [F10], put $a={\prod }_{c\in A}c$ and $b={\prod }_{c\in B}c$. The ideal actions of $F,G,F,G$ send $z$ to $z\oplus a$ and back and toggle $t$ by $b(z\oplus a)\oplus bz=ab$. Step 2.1 restores the temporary spares after each ladder, so this is valid even when the spares include the other call's controls or target. The inequalities $q+1\ge p-2$ and $p\ge q-1$ ensure enough spares. Two calls of each size have pair $2E_p+2E_{q+1}=B_r$; the one- and two-control cases have pairs $B_1,B_2$. Equality on every basis word extends by [F6] to the full operator $C^r(X)\otimes I_z$, including entangled inputs, so these literal lists meet the borrowed-wire contract of [F8]. All spares are existing wires in each invocation of $D$.

For the no-workspace list $N$, [F12] gives the unitary square root $Z$ prescribed in [F10]: each eigenvalue has modulus one, its half-angle scalar squares to it by the double-angle identities, and that scalar has modulus one. For at least two controls, put $A_0={\prod }_{c\in A}c$. The two $D(A;b;t)$ calls restore their borrowed data target exactly by step 3.1. Thus on a basis control branch the target exponent of $Z$ in the five-call list is $b-(b\oplus A_0)+A_0=2A_{0}b$. Induction on the number of controls, with the one-control case of step 1.2 and the zero-control gate as bases, proves its exact $C^m(W)$ action. No new wire is used. Its literal cost is $Q_{m-1}+2B_{m-1}+2(2,4)$, with $Q_1=(2,4)$ and $Q_0=(0,1)$; the recursion decreases the number of controls and terminates.

In the clean branch, $D(C;w;t)$ computes the controls' AND into $w$, restoring the borrowed data target by step 3.1. The list $S(w,t;W)$ applies $W$ precisely on that branch, and the reversed adjoint $D$ list restores $w=0$ for every data input. Linearity extends this basis calculation to superposed or entangled data. This gives the exact clean-input data operation and pair $2B_m+(2,4)=K_m$ for $m\ge 1$; with no controls the sole gate has pair $K_0=Q_0$. No claim about the other initial workspace sector is required.

There are $d-1$ swaps, their $d-1$ inverses, and one controlled-$V$ call. Each zero-valued pattern control is implemented by an $X$ before and after the positive-control call, adding exactly two one-qubit occurrences under [F5]. Steps 4.1–4.2 prove that these selected expansions implement the ideal data gates exactly and each clean-bit call returns its work bit to zero, in the model of [F7]. Sequential composition therefore permits reuse of that bit.

If $d=1$, the swap lists are empty and the single controlled target block acts on $(x,y)$ directly. If $n=1$, there are no controls and the construction is one gate on the sole wire: its matrix is $V$ when $x=0,y=1$, and $XVX$ when $x=1,y=0$, so its action on the selected ordered pair is $V$ in both cases. For the other cases, steps 4.1–4.2 supply the elementary expansions used in step 5.1 with the stated work-bit return, consistently with [F7]. Thus every case is an exact elementary implementation.

A zero control adds two one-qubit $X$ gates, independently of the selected positive-control circuit. The reversed adjoint list has the same pair as its forward list. Adding all forward, reverse, and middle lists therefore gives the claimed total pair. Since $B_r=O(r)$, the recurrence sums to $Q_m=O(m^2)$, whereas $K_m=O(m)$. There are $2d-1$ calls, and at most $m$ negative controls per call, giving the two claimed total bounds for $n\ge 2$. Sequential exact clean return permits reuse of one bit even on superposed data. The empty swap lists when $d=1$ and the direct ordered one-qubit block when $n=1$ give the stated boundary cases.