Jordan powers and power-of-two indirect CNOT

Open

QAlgorithms.Papers.Independent.Intakethird100.P39.jordan_power_and_indirect_cnot

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

prove2quantum

For $\ell\ge0$ , let $J$ be the $(\ell+1)\times(\ell+1)$ lower bidiagonal matrix with ones on the diagonal and first lower diagonal. Over the natural numbers,

(J^\ell)_{ij}=\begin{cases}\binom{\ell}{i-j},&j\le i,\\0,&i<j.\end{cases}

If $\ell=2^p$ with $p\ge1$ , reduction modulo two gives

J^\ell=I+E_{\ell,0}.

Consequently, $\ell$ repetitions of either neighboring CNOT sweep (targets in increasing order, or in decreasing order) apply the endpoint CNOT: $x_\ell\mapsto x_\ell\oplus x_0$ , with all other bits fixed, for every input bit string. Thus both Fig. 12 circuits restore every borrowed intermediate bit. Equality of these basis permutations gives the corresponding exact quantum circuit identities by linear extension.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P39

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P39

open scoped BigOperators

/-- PDF pp.13-14, Eqs. (36)-(38) and both Fig.12 identities: the natural
binomial formula and its binary reduction, together with the exact actions
of both repeated neighboring sweeps. Intermediate bits are borrowed,
never initialized. The bit identities extend linearly to quantum registers. -/
theorem jordan_power_and_indirect_cnot :
    (∀ (ell : ℕ) (i j : Fin (ell + 1)),
      (jordanMatrix ℕ ell ^ ell) i j =
        if j.val ≤ i.val then Nat.choose ell (i.val - j.val) else 0) ∧
    (∀ p : ℕ, 1 ≤ p →
      jordanMatrix (ZMod 2) (2 ^ p) ^ (2 ^ p) = endpointMatrix (2 ^ p) ∧
      ∀ x : Qubits (2 ^ p + 1),
        (ascendingSweep (2 ^ p))^[2 ^ p] x = endpointCnot (2 ^ p) x ∧
        (descendingSweep (2 ^ p))^[2 ^ p] x = endpointCnot (2 ^ p) x) := 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. 13, Jordan power and power-of-two indirect CNOT, Eqs. (36)–(38), Fig. 12

Read-back

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

For a natural number $\ell$ and $R=\mathbb N$ or $R=\mathbb Z/2\mathbb Z$ , let $J_{R,\ell}$ be the matrix with rows and columns indexed by $0,\ldots,\ell$ , whose $(i,j)$ -entry is $1$ if $i=j$ or $i=j+1$ , and $0$ otherwise. The assertion is the conjunction of the following two claims. First, for every $\ell\in\mathbb N$ , including $0$ , and every $i,j\in\{0,\ldots,\ell\}$ ,

(J_{\mathbb N,\ell}^{\,\ell})_{ij} = \begin{cases} \binom{\ell}{i-j},&j\le i,\\ 0,&j>i. \end{cases}

For $\ell=0$ , this uses the zeroth matrix power, namely the identity matrix. Second, for every natural number $p\ge1$ , putting $L=2^p$ , one has $J_{\mathbb Z/2\mathbb Z,L}^{\,L}=I+E_{L,0}$ , where $E_{L,0}$ has a single $1$ in row $L$ , column $0$ , and zero elsewhere; and, for every Boolean string $x=(x_0,\ldots,x_L)$ , both $L$ repetitions of the ascending sweep and $L$ repetitions of the descending sweep yield the string whose last bit is $x_L\mathbin{\oplus}x_0$ and whose other bits equal those of $x$ . Each ascending sweep successively updates the current bit $y_{i+1}\leftarrow y_{i+1}\mathbin{\oplus}y_i$ for $i=0,\ldots,L-1$ ; each descending sweep performs those updates in the reverse order, and each update leaves all other bits unchanged. Here repetitions mean function iteration, $\oplus$ is Boolean exclusive-or, and the restriction $p\ge1$ excludes $p=0$ .

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