C^k(U) from CNOTs and single-qubit gates: the control-count recursion

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #85, part (e3) of R-005 (specs/magic-plan.md, "The split"); it closes the original row #72, whose other pieces are ControlledGate.lean (#83) and EulerDecomposition.lean with ControlledSingle.lean (#84).

★★ ctrlSetOf_mem_closure: a gate with any number of controls, on any control pattern, is a product of CNOTs and single-qubit gates. Nielsen–Chuang Figure 4.10, with no work qubits: the ancilla-free route is forced, because the work-qubit ladder is not a matrix identity (it reproduces C^k(U) only on the sector where the work qubits are 0, and #73 consumes an exact product).

Two ingredients, and both are new algebra rather than bookkeeping.

The pattern costs nothing. Conjugating by one X on a control qubit flips that control value (★ xGate_conj_ctrlSet), so only the number of controls matters. The mechanism is that X on qubit a is a permutation matrix, and multiplying by it relabels (xGate_mul_apply, mul_xGate_apply).

The recursion needs two target qubits at once. C(V) on the target and C^{k-1}(X) on the last control act on different qubits, so #84's one-control algebra does not reach it. pairSet is the family of gates that act by a 4 × 4 block on a pair of qubits — by one block on the labels matching the pattern on the control set, by another on the rest — and it is closed under products, blockwise in each branch (★★ pairSet_mul, through a four-element collapse). Every gate of the recursion is one of them, so ★★ ctrlSetOf_insert reduces to two 4 × 4 identities, which diagBlock and flipBlock settle in three rewrites: conjugating a block-diagonal gate by the flip swaps its two blocks, and

diag(1, V) · X · diag(1, V*) · X · diag(V, V) = diag(V* V, V V) = diag(1, U) when V² = U,

while on the labels where the controls do not match the same product is diag(1, V) · diag(1, V*), the identity. The square root V comes from Euler.exists_sqrt.

• flipBit, flipAt, xGate_apply, xGate_mul_apply, mul_xGate_apply, ★ xGate_conj_ctrlSet;
• diagBlock, flipBlock, diagBlock_apply_of_fst_eq, diagBlock_apply_of_fst_ne, flipBlock_apply_of_snd_eq, flipBlock_apply_of_snd_ne, diagBlock_mul, diagBlock_one, ★ flipBlock_conj_diagBlock, ★ diagBlock_five;
• pairSet, sum_collapse_pair, ★★ pairSet_mul;
• ctrlSetOf, pairSet_eq_ctrlOf, pairSet_eq_ctrlSetOf_fst, pairSet_eq_ctrlSetOf_snd, pairSet_eq_ctrlSetOf_insert, ★★ ctrlSetOf_insert;
• elementary, xGate_mem_elementary, ctrlOf_mem_closure, ★★ ctrlSetOf_mem_closure, ★★ ctrlGateOf_mem_closure.

Honest scope

⚠️ This is an exact product identity, not a gate count: the recursion is proved, and the number of elementary gates it produces is not claimed (that is BACKLOG #74, deliberately not claimed). ⚠️ Nothing here approximates a gate; the single-qubit gates in the product are exact. Approximating them by Clifford+T words is BACKLOG #81.

References: M. A. Nielsen, I. L. Chuang, Quantum Computation and Quantum Information §4.3, Figures 4.8 and 4.10; specs/magic-plan.md; specs/BACKLOG.md #85, #72, #73; specs/future-work.md.

The bit flip as a relabelling

def QuantumInfo.Controlled.flipBit (b : Fin 2) : Fin 2

The other bit.

Equations

• QuantumInfo.Controlled.flipBit b = if b = 0 then 1 else 0

@[simp]

theorem QuantumInfo.Controlled.flipBit_flipBit (b : Fin 2) : flipBit (flipBit b) = b

theorem QuantumInfo.Controlled.flipBit_ne (b : Fin 2) : flipBit b ≠ b

theorem QuantumInfo.Controlled.eq_flipBit_of_ne {b c : Fin 2} (h : b ≠ c) : c = flipBit b

def QuantumInfo.Controlled.flipAt {m : ℕ} (a : Fin m) (k : Fin m → Fin 2) : Fin m → Fin 2

The label with the a-th bit flipped.

Equations

• QuantumInfo.Controlled.flipAt a k = Function.update k a (QuantumInfo.Controlled.flipBit (k a))

@[simp]

theorem QuantumInfo.Controlled.flipAt_apply_self {m : ℕ} (a : Fin m) (k : Fin m → Fin 2) : flipAt a k a = flipBit (k a)

theorem QuantumInfo.Controlled.flipAt_apply_of_ne {m : ℕ} {a i : Fin m} (h : i ≠ a) (k : Fin m → Fin 2) : flipAt a k i = k i

@[simp]

theorem QuantumInfo.Controlled.flipAt_flipAt {m : ℕ} (a : Fin m) (k : Fin m → Fin 2) : flipAt a (flipAt a k) = k

theorem QuantumInfo.Controlled.flipAt_agree_iff {m : ℕ} {a j : Fin m} {k l : Fin m → Fin 2} : (∀ (i : Fin m), i ≠ j → flipAt a k i = flipAt a l i) ↔ ∀ (i : Fin m), i ≠ j → k i = l i

theorem QuantumInfo.Controlled.eq_flipAt_iff {m : ℕ} {a : Fin m} {k l : Fin m → Fin 2} : l = flipAt a k ↔ (∀ (i : Fin m), i ≠ a → k i = l i) ∧ k a ≠ l a

theorem QuantumInfo.Controlled.xGate_apply {m : ℕ} (a : Fin m) (k l : Fin m → Fin 2) : xGate a k l = if l = flipAt a k then 1 else 0

The bit flip is a permutation matrix.

theorem QuantumInfo.Controlled.xGate_mul_apply {m : ℕ} (a : Fin m) (G : Matrix (Fin m → Fin 2) (Fin m → Fin 2) ℂ) (k l : Fin m → Fin 2) : (xGate a * G) k l = G (flipAt a k) l

theorem QuantumInfo.Controlled.mul_xGate_apply {m : ℕ} (a : Fin m) (G : Matrix (Fin m → Fin 2) (Fin m → Fin 2) ℂ) (k l : Fin m → Fin 2) : (G * xGate a) k l = G k (flipAt a l)

theorem QuantumInfo.Controlled.xGate_conj_ctrlSet {m : ℕ} {S : Finset (Fin m)} {j u : Fin m} (hju : j ≠ u) (pat : Fin m → Fin 2) (a b c d : ℂ) : xGate u * ctrlSet S j pat a b c d * xGate u = ctrlSet S j (Function.update pat u (flipBit (pat u))) a b c d

★ Conjugating by one X on a control qubit flips that control value, so only the number of controls matters, never the pattern.

The 4 × 4 blocks

def QuantumInfo.Controlled.diagBlock (A B : Matrix (Fin 2) (Fin 2) ℂ) : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ

The block acting on the second qubit by A when the first carries 0 and by B when it carries 1, never changing the first.

Equations

• QuantumInfo.Controlled.diagBlock A B p q = if p.1 = q.1 then (if p.1 = 0 then A else B) p.2 q.2 else 0

def QuantumInfo.Controlled.flipBlock : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ

The block that flips the first qubit and leaves the second.

Equations

• QuantumInfo.Controlled.flipBlock p q = if p.2 = q.2 then QuantumInfo.Euler.xMat p.1 q.1 else 0

theorem QuantumInfo.Controlled.diagBlock_apply_of_fst_ne {A B : Matrix (Fin 2) (Fin 2) ℂ} {p q : Fin 2 × Fin 2} (h : p.1 ≠ q.1) : diagBlock A B p q = 0

theorem QuantumInfo.Controlled.diagBlock_apply_of_fst_eq {A B : Matrix (Fin 2) (Fin 2) ℂ} {p q : Fin 2 × Fin 2} (h : p.1 = q.1) : diagBlock A B p q = (if p.1 = 0 then A else B) p.2 q.2

theorem QuantumInfo.Controlled.flipBlock_apply_of_snd_ne {p q : Fin 2 × Fin 2} (h : p.2 ≠ q.2) : flipBlock p q = 0

theorem QuantumInfo.Controlled.flipBlock_apply_of_snd_eq {p q : Fin 2 × Fin 2} (h : p.2 = q.2) : flipBlock p q = Euler.xMat p.1 q.1

theorem QuantumInfo.Controlled.diagBlock_mul (A B C D : Matrix (Fin 2) (Fin 2) ℂ) : diagBlock A B * diagBlock C D = diagBlock (A * C) (B * D)

@[simp]

theorem QuantumInfo.Controlled.diagBlock_one : diagBlock 1 1 = 1

theorem QuantumInfo.Controlled.flipBlock_conj_diagBlock (A B : Matrix (Fin 2) (Fin 2) ℂ) : flipBlock * diagBlock A B * flipBlock = diagBlock B A

★ Conjugating by the flip swaps the two blocks.

theorem QuantumInfo.Controlled.diagBlock_five {U V : Matrix (Fin 2) (Fin 2) ℂ} (hV : star V * V = 1) (hVV : V * V = U) : diagBlock 1 V * flipBlock * diagBlock 1 (star V) * flipBlock * diagBlock V V = diagBlock 1 U

★ The block identity behind the recursion. With V² = U, inserting the two flips turns three controlled gates into one controlled U.

Gates on a pair of qubits

def QuantumInfo.Controlled.pairSet {m : ℕ} (S : Finset (Fin m)) (u t : Fin m) (pat : Fin m → Fin 2) (M N : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ) : Matrix (Fin m → Fin 2) (Fin m → Fin 2) ℂ

The gate acting by the 4 × 4 block M on the pair (u, t) of the labels that match pat on the control set S, and by N on all the others.

Equations

• QuantumInfo.Controlled.pairSet S u t pat M N k l = if ∀ (i : Fin m), i ≠ u → i ≠ t → k i = l i then (if ∀ i ∈ S, k i = pat i then M else N) (k u, k t) (l u, l t) else 0

theorem QuantumInfo.Controlled.pairSet_apply_of_agree {m : ℕ} {S : Finset (Fin m)} {u t : Fin m} {pat : Fin m → Fin 2} {M N : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ} {k l : Fin m → Fin 2} (hag : ∀ (i : Fin m), i ≠ u → i ≠ t → k i = l i) : pairSet S u t pat M N k l = (if ∀ i ∈ S, k i = pat i then M else N) (k u, k t) (l u, l t)

theorem QuantumInfo.Controlled.pairSet_apply_of_not_agree {m : ℕ} {S : Finset (Fin m)} {u t : Fin m} {pat : Fin m → Fin 2} {M N : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ} {k l : Fin m → Fin 2} (h : ¬∀ (i : Fin m), i ≠ u → i ≠ t → k i = l i) : pairSet S u t pat M N k l = 0

theorem QuantumInfo.Controlled.sum_collapse_pair {m : ℕ} {u t : Fin m} (hut : u ≠ t) (k : Fin m → Fin 2) (f : (Fin m → Fin 2) → ℂ) (hf : ∀ (p : Fin m → Fin 2), (¬∀ (i : Fin m), i ≠ u → i ≠ t → p i = k i) → f p = 0) : ∑ p : Fin m → Fin 2, f p = ∑ bb : Fin 2 × Fin 2, f (Function.update (Function.update k u bb.1) t bb.2)

Every sum here collapses to the four labels that agree with k away from the pair.

theorem QuantumInfo.Controlled.pairSet_mul {m : ℕ} {S : Finset (Fin m)} {u t : Fin m} {pat : Fin m → Fin 2} (hut : u ≠ t) (huS : u ∉ S) (htS : t ∉ S) (M N M' N' : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ) : pairSet S u t pat M N * pairSet S u t pat M' N' = pairSet S u t pat (M * M') (N * N')

★★ Pair gates multiply blockwise, in each branch separately.

The gates of the recursion are pair gates

def QuantumInfo.Controlled.ctrlSetOf {m : ℕ} (S : Finset (Fin m)) (j : Fin m) (pat : Fin m → Fin 2) (U : Matrix (Fin 2) (Fin 2) ℂ) : Matrix (Fin m → Fin 2) (Fin m → Fin 2) ℂ

The gate U on qubit j, controlled by the set S on the pattern pat.

Equations

• QuantumInfo.Controlled.ctrlSetOf S j pat U = QuantumInfo.Controlled.ctrlSet S j pat (U 0 0) (U 0 1) (U 1 0) (U 1 1)

theorem QuantumInfo.Controlled.ctrlSetOf_apply_block {m : ℕ} {S : Finset (Fin m)} {pat : Fin m → Fin 2} {j : Fin m} {U : Matrix (Fin 2) (Fin 2) ℂ} {k l : Fin m → Fin 2} (hag : ∀ (i : Fin m), i ≠ j → k i = l i) (hc : ∀ i ∈ S, k i = pat i) : ctrlSetOf S j pat U k l = U (k j) (l j)

theorem QuantumInfo.Controlled.ctrlSetOf_apply_id {m : ℕ} {S : Finset (Fin m)} {pat : Fin m → Fin 2} {j : Fin m} {U : Matrix (Fin 2) (Fin 2) ℂ} {k l : Fin m → Fin 2} (hag : ∀ (i : Fin m), i ≠ j → k i = l i) (hc : ¬∀ i ∈ S, k i = pat i) : ctrlSetOf S j pat U k l = 1 (k j) (l j)

theorem QuantumInfo.Controlled.ctrlSetOf_apply_of_not_agree {m : ℕ} {S : Finset (Fin m)} {pat : Fin m → Fin 2} {j : Fin m} {U : Matrix (Fin 2) (Fin 2) ℂ} {k l : Fin m → Fin 2} (h : ¬∀ (i : Fin m), i ≠ j → k i = l i) : ctrlSetOf S j pat U k l = 0

theorem QuantumInfo.Controlled.ctrlOf_eq_ctrlSetOf {m : ℕ} (a j : Fin m) (U : Matrix (Fin 2) (Fin 2) ℂ) : ctrlOf a j U = ctrlSetOf {a} j (fun (x : Fin m) => 1) U

theorem QuantumInfo.Controlled.one_pair_apply (p q : Fin 2 × Fin 2) : 1 p q = if p = q then 1 else 0

theorem QuantumInfo.Controlled.pairSet_eq_ctrlOf {m : ℕ} {S : Finset (Fin m)} {u t : Fin m} {pat : Fin m → Fin 2} (hut : u ≠ t) (V : Matrix (Fin 2) (Fin 2) ℂ) : pairSet S u t pat (diagBlock 1 V) (diagBlock 1 V) = ctrlOf u t V

The one-control gate on the pair: the control set plays no part in it.

theorem QuantumInfo.Controlled.pairSet_eq_ctrlSetOf_fst {m : ℕ} {S : Finset (Fin m)} {u t : Fin m} {pat : Fin m → Fin 2} (hut : u ≠ t) : pairSet S u t pat flipBlock 1 = ctrlSetOf S u pat Euler.xMat

The multiply-controlled gate on the first qubit of the pair.

theorem QuantumInfo.Controlled.pairSet_eq_ctrlSetOf_snd {m : ℕ} {S : Finset (Fin m)} {u t : Fin m} {pat : Fin m → Fin 2} (hut : u ≠ t) (V : Matrix (Fin 2) (Fin 2) ℂ) : pairSet S u t pat (diagBlock V V) 1 = ctrlSetOf S t pat V

The multiply-controlled gate on the second qubit of the pair.

theorem QuantumInfo.Controlled.pairSet_eq_ctrlSetOf_insert {m : ℕ} {S : Finset (Fin m)} {u t : Fin m} {pat : Fin m → Fin 2} (hut : u ≠ t) (hpu : pat u = 1) (U : Matrix (Fin 2) (Fin 2) ℂ) : pairSet S u t pat (diagBlock 1 U) 1 = ctrlSetOf (insert u S) t pat U

The gate with one more control: the first qubit of the pair joins the control set.

theorem QuantumInfo.Controlled.ctrlSetOf_insert {m : ℕ} {S : Finset (Fin m)} {u t : Fin m} {pat : Fin m → Fin 2} (hut : u ≠ t) (huS : u ∉ S) (htS : t ∉ S) (hpu : pat u = 1) {U V : Matrix (Fin 2) (Fin 2) ℂ} (hV : V ∈ Matrix.unitaryGroup (Fin 2) ℂ) (hVV : V * V = U) : ctrlSetOf (insert u S) t pat U = ctrlOf u t V * ctrlSetOf S u pat Euler.xMat * ctrlOf u t (star V) * ctrlSetOf S u pat Euler.xMat * ctrlSetOf S t pat V

★★ The control-count recursion (Nielsen–Chuang Figure 4.10, ancilla-free): one more control costs two one-control gates, two gates with the old control set on the new control qubit, and one gate with the old control set on the target, with V a square root of U.

Every controlled gate is a product of CNOTs and single-qubit gates

def QuantumInfo.Controlled.elementary (m : ℕ) : Set (Matrix (Fin m → Fin 2) (Fin m → Fin 2) ℂ)

The universal gate set: single-qubit gates and CNOTs.

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumInfo.Controlled.gateOf_mem_elementary {m : ℕ} (j : Fin m) {M : Matrix (Fin 2) (Fin 2) ℂ} (hM : M ∈ Matrix.unitaryGroup (Fin 2) ℂ) : gateOf j M ∈ elementary m

theorem QuantumInfo.Controlled.cnotGate'_mem_elementary {m : ℕ} {a b : Fin m} (hab : a ≠ b) : cnotGate' a b ∈ elementary m

theorem QuantumInfo.Controlled.xGate_eq_gateOf {m : ℕ} (j : Fin m) : xGate j = gateOf j Euler.xMat

theorem QuantumInfo.Controlled.xGate_mem_elementary {m : ℕ} (j : Fin m) : xGate j ∈ elementary m

theorem QuantumInfo.Controlled.phaseMat_eq (α : ℝ) : !![1, 0; 0, Euler.expI α] = Euler.expI (α / 2) • Euler.rzMat α

theorem QuantumInfo.Controlled.phaseMat_mem_unitaryGroup (α : ℝ) : !![1, 0; 0, Euler.expI α] ∈ Matrix.unitaryGroup (Fin 2) ℂ

theorem QuantumInfo.Controlled.singleGate_phase_eq_gateOf {m : ℕ} (a : Fin m) (α : ℝ) : singleGate a 1 0 0 (Euler.expI α) = gateOf a !![1, 0; 0, Euler.expI α]

theorem QuantumInfo.Controlled.ctrlOf_mem_closure {m : ℕ} {a j : Fin m} (haj : a ≠ j) {U : Matrix (Fin 2) (Fin 2) ℂ} (hU : U ∈ Matrix.unitaryGroup (Fin 2) ℂ) : ctrlOf a j U ∈ Submonoid.closure (elementary m)

A one-control gate is a product of elementary gates: #84's circuit.

theorem QuantumInfo.Controlled.ctrlSetOf_empty {m : ℕ} (j : Fin m) (pat : Fin m → Fin 2) (U : Matrix (Fin 2) (Fin 2) ℂ) : ctrlSetOf ∅ j pat U = gateOf j U

theorem QuantumInfo.Controlled.ctrlSetOf_mem_closure_aux {m : ℕ} (n : ℕ) (S : Finset (Fin m)) (j : Fin m) (pat : Fin m → Fin 2) (U : Matrix (Fin 2) (Fin 2) ℂ) : S.card = n → j ∉ S → U ∈ Matrix.unitaryGroup (Fin 2) ℂ → ctrlSetOf S j pat U ∈ Submonoid.closure (elementary m)

The induction behind ctrlSetOf_mem_closure, on the number of controls.

theorem QuantumInfo.Controlled.ctrlSetOf_mem_closure {m : ℕ} (S : Finset (Fin m)) (j : Fin m) (pat : Fin m → Fin 2) {U : Matrix (Fin 2) (Fin 2) ℂ} (hjS : j ∉ S) (hU : U ∈ Matrix.unitaryGroup (Fin 2) ℂ) : ctrlSetOf S j pat U ∈ Submonoid.closure (elementary m)

★★ A gate with any number of controls, on any control pattern, is a product of CNOTs and single-qubit gates.

theorem QuantumInfo.Controlled.ctrlGateOf_mem_closure {m : ℕ} (j : Fin m) (pat : Fin m → Fin 2) {U : Matrix (Fin 2) (Fin 2) ℂ} (hU : U ∈ Matrix.unitaryGroup (Fin 2) ℂ) : MultiControlled.ctrlGate j pat (U 0 0) (U 0 1) (U 1 0) (U 1 1) ∈ Submonoid.closure (elementary m)

★★ #71's multiply-controlled gate is a product of CNOTs and single-qubit gates — the form #73 consumes, since the two-level theory of #70 and #71 produces exactly these.