Exact truncated phase-swap circuit equivalences

Open

QAlgorithms.Papers.Independent.Intakethird100.P39.truncated_cpSwap_panels

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

On two five-bit blocks, a type- $j\ge1$ phase-swap exchanges the blocks and contributes one pair phase $\pi/2^{5(j-1)+1+a+b}$ for each occupied bit pair $a,b\in\{0,\ldots,4\}$ . Delete angles strictly below $\pi/1024$ , retaining equality. Let $\widetilde{CP}_j$ denote this truncated module. Define panels A, B, C by moving each second-block bit left across the five first-block bits with adjacent phase-SWAP crossings, in the order drawn in Fig. 17. Then

\widetilde{CP}_1=CP_1=C_A,\qquad\widetilde{CP}_2=C_B,\qquad\widetilde{CP}_j=SWAP_{5,5}=C_C\quad(j\ge3).

Panel A retains all 25 pair phases, from $\pi/2$ to $\pi/512$ . Panel B retains exactly $a+b\le4$ , with angles $\pi/64$ through $\pi/1024$ . Panel C is the pure block exchange. These are exact equalities of truncated modules and do not assert the undefined whole-QFT relative-error claim.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P39

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P39

open scoped BigOperators

/-- PDF pp.10,19, Appendix B Fig.17: exact equivalence of all three
truncated circuits. This makes no whole-QFT approximation-error claim. -/
theorem truncated_cpSwap_panels :
    (truncatedCpSwap 5 1 10 = cpSwap 5 1 ∧
      truncatedCpSwap 5 1 10 = blockCircuitMatrix 10 panelA) ∧
    truncatedCpSwap 5 2 10 = blockCircuitMatrix 10 panelB ∧
    (∀ j : ℕ, 3 ≤ j → truncatedCpSwap 5 j 10 = blockSwap 5 ∧
      truncatedCpSwap 5 j 10 = blockCircuitMatrix 10 panelC) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P39

Source

Quantum CISC Compilation by Optimal Control and Scalable Assembly of Complex Instruction Sets beyond Two-Qubit Gates, arXiv:0712.3227v2, PDF p. 19, Appendix B, Fig. 17: truncated cp-swap circuit equivalences

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

Let the rows and columns of all matrices below be indexed by ten-bit strings $x,y:\{0,\ldots,9\}\to\{\mathrm{false},\mathrm{true}\}$ , identify each bit with $0$ or $1$ when used numerically, let $\sigma x$ exchange the first five bits with the last five, and put $A(x)=\sum_{a=0}^{4}x_a2^{4-a}$ and $B(x)=\sum_{b=0}^{4}x_{5+b}2^{4-b}$ . For every natural number $j$ , define $M_j(y,x)=0$ unless $y=\sigma x$ , and otherwise define

M_j(\sigma x,x) =\exp\!\left( i\sum_{a=0}^{4}\sum_{b=0}^{4} \begin{cases} \displaystyle\frac{\pi}{2^{5(j-1)+1+a+b}} &x_a=x_{5+b}=1\ \text{and }5(j-1)+1+a+b\le10,\\ 0&\text{otherwise}, \end{cases} \right),

where $j-1=\max(j-1,0)$ . Define $C(y,x)=0$ unless $y=\sigma x$ , with $C(\sigma x,x)=\exp(2\pi iA(x)B(x)/2^{10})$ , and define $S(y,x)$ to be $1$ when $y=\sigma x$ and $0$ otherwise. To describe the three circuit matrices, a local phase-swap of offset $o$ and phase index $p$ exchanges bits $o,o+1$ , leaves all other bits unchanged, and assigns the resulting transition the coefficient $\exp(2\pi i x_ox_{o+1}/2^{p+1})$ ; its other entries are zero. A local swap has the same bit exchange with coefficient $1$ . Form three ordered lists by taking $b=0,\ldots,4$ in increasing order and, for each $b$ , $a=4,\ldots,0$ in decreasing order: list A uses local phase-swaps of offset $a+b$ and index $1+a+b$ ; list B uses local phase-swaps of offset $a+b$ and index $6+a+b$ when $a+b\le4$ , and local swaps otherwise; list C uses local swaps of offset $a+b$ . Let $P_A,P_B,P_C$ be the products of their respective matrices with the last listed matrix on the left, so that the first listed step acts first. The theorem asserts

(M_1=C\ \land\ M_1=P_A) \ \land\ M_2=P_B \ \land\ \bigl(\forall j\in\mathbb N,\ j\ge3\ \Longrightarrow\ (M_j=S\ \land\ M_j=P_C)\bigr).

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph