Exact binary QFT circuit correctness

If $n=0$, the exact algorithm has no gates, so [A1] gives the identity on the one-dimensional register; by [F1], ${\mathrm{QFT}}_1$ is also the identity. Thus the claimed basis action holds in this case. Now suppose $n\ge 1$ and fix a basis input $\mathrm{\mid }{x}_{n-1}\cdots x_0⟩$. In the descending loop, before the step targeting $q_j$, every lower wire $q_i$ with $i<j$ is still in its original basis state $\mathrm{\mid }{x}_i⟩$: earlier gates targeted only higher wires, and the lower wires occur only as controls, which the diagonal controlled-phase matrix in [F2] leaves unchanged. The local embedding action [F6] therefore leaves those control bits unchanged. The Hadamard on $q_j$ contributes relative phase $(-1{)}^{x_j}=e^{2\pi i{x}_j\mathrm{/}2}$, while the controlled phases from lower controls contribute $e^{2\pi i{\sum }_{i<j}{x}_i{2}^{-(j-i+1)}}$. Thus target $q_j$ has state $R_j$. The state before the final swaps is $R_{n-1}\otimes \cdots \otimes R_0$. The tensor order and coordinate-ket convention are [F3] and [F4]; interpreting this finite gate trace as the circuit's operator product requires [A1].

For $n\ge 1$, the final swaps reverse those ordered factors by [F3], producing $R_0\otimes \cdots \otimes R_{n-1}$; [F1] identifies this with the positive-sign Fourier output on $\mathrm{\mid }x⟩$. Together with the $n=0$ case established in step 1.1, the circuit agrees with ${\mathrm{QFT}}_{2^n}$ on every basis vector.

Both the circuit denotation and ${\mathrm{QFT}}_{2^n}$ are linear operators by [A1], so equality on the standard basis [F4] implies equality on every finite linear combination of basis vectors. Reversing the gate sequence and taking adjoints is its inverse by [F5]; the reverse list has the same number of gates, and each adjoint is still a Hadamard, controlled phase of opposite angle, or SWAP. The adjoint controlled phases have unit ideal cost by [F2], so the inverse QFT has the same ideal gate count and uses the negative-sign convention by [L1].