Controlled gates on a set of control qubits

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #83, the reachable core of the re-split row #72 (R-005; specs/magic-plan.md, "The split").

One definition covers the whole gate vocabulary of the Clifford+T chain. For a control set S, a target j ∉ S and a control pattern pat, ctrlSet S j pat a b c d applies the 2 × 2 block !![a, b; c, d] to qubit j of those basis labels that match pat on S, and the identity on the rest:

• S = ∅ is a single-qubit gate (singleGate, and xGate for the bit flip);
• S = {a} with the flip block is CNOT (cnotGate');
• S = univ.erase j is the multiply-controlled gate of #71 — ★ ctrlSet_erase_eq_ctrlGate identifies them, so the two-level theory of #70 and #71 applies verbatim.

The algebra is blockwise, and that is the point: ★★ ctrlSet_mul says controlled gates on a fixed (S, j, pat) multiply by multiplying their 2 × 2 blocks, so they are a copy of the 2 × 2 matrices inside the big matrix algebra; ★ ctrlSet_conjTranspose transposes the block, ctrlSet_one is the identity, and hence ★ ctrlSet_mem_unitaryGroup — such a gate is unitary exactly when its block is.

• agree_off_iff, sum_collapse_update — the two-element collapse every computation here uses;
• ctrlSet, its three entry lemmas, ctrlSet_one, ★★ ctrlSet_mul, ★ ctrlSet_conjTranspose, ★ ctrlSet_mem_unitaryGroup;
• singleGate, xGate, cnotGate' and their unitarity, xGate_mul_self; ★ ctrlSet_erase_eq_ctrlGate.

Honest scope

⚠️ This is the vocabulary, not yet the decomposition. Writing a multiply-controlled gate as a product of CNOTs and single-qubit gates needs three further pieces, and they are numbered: the control pattern must be freed by conjugating with X gates on the control qubits, so that only the number of controls matters (BACKLOG #83's companion, also #85); the z-y-z Euler decomposition of a 2 × 2 unitary with the ABC identity for one control (#84, shared with #81); and the control-count recursion through square roots (#85). The work-qubit ladder is not a substitute: it reproduces a multiply-controlled gate only on the sector where the work qubits are 0, not as a matrix identity, which is what #73 consumes.

References: M. A. Nielsen, I. L. Chuang, Quantum Computation and Quantum Information §4.3; A. Barenco et al., PRA 52 (1995) 3457 §V–VII; specs/magic-plan.md; specs/BACKLOG.md #83, #84, #85; specs/future-work.md.

The two-element collapse

theorem QuantumInfo.Controlled.agree_off_iff {m : ℕ} {j : Fin m} {p k : Fin m → Fin 2} : (∀ (i : Fin m), i ≠ j → p i = k i) ↔ p = Function.update k j 0 ∨ p = Function.update k j 1

A label agrees with k away from j exactly when it is one of the two labels obtained by setting the j-th qubit.

theorem QuantumInfo.Controlled.sum_collapse_update {m : ℕ} (j : Fin m) (k : Fin m → Fin 2) (f : (Fin m → Fin 2) → ℂ) (hf : ∀ (p : Fin m → Fin 2), (¬∀ (i : Fin m), i ≠ j → p i = k i) → f p = 0) : ∑ p : Fin m → Fin 2, f p = f (Function.update k j 0) + f (Function.update k j 1)

Every sum here collapses to the two labels that agree with k away from the target.

The controlled gate

def QuantumInfo.Controlled.ctrlSet {m : ℕ} (S : Finset (Fin m)) (j : Fin m) (pat : Fin m → Fin 2) (a b c d : ℂ) : Matrix (Fin m → Fin 2) (Fin m → Fin 2) ℂ

The gate controlled on the qubits of S with pattern pat, acting by the 2 × 2 block !![a, b; c, d] on the target qubit j.

Equations

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

theorem QuantumInfo.Controlled.ctrlSet_apply_of_not_agree {m : ℕ} {S : Finset (Fin m)} {j : Fin m} {pat : Fin m → Fin 2} {a b c d : ℂ} {k l : Fin m → Fin 2} (h : ¬∀ (i : Fin m), i ≠ j → k i = l i) : ctrlSet S j pat a b c d k l = 0

theorem QuantumInfo.Controlled.ctrlSet_apply_of_ctrl {m : ℕ} {S : Finset (Fin m)} {j : Fin m} {pat : Fin m → Fin 2} {a b c d : ℂ} {k l : Fin m → Fin 2} (hag : ∀ (i : Fin m), i ≠ j → k i = l i) (hc : ∀ i ∈ S, k i = pat i) : ctrlSet S j pat a b c d k l = MultiControlled.blockEntry (k j) (l j) a b c d

theorem QuantumInfo.Controlled.ctrlSet_apply_of_not_ctrl {m : ℕ} {S : Finset (Fin m)} {j : Fin m} {pat : Fin m → Fin 2} {a b c d : ℂ} {k l : Fin m → Fin 2} (hag : ∀ (i : Fin m), i ≠ j → k i = l i) (hc : ¬∀ i ∈ S, k i = pat i) : ctrlSet S j pat a b c d k l = if k j = l j then 1 else 0

theorem QuantumInfo.Controlled.ctrlSet_one {m : ℕ} (S : Finset (Fin m)) (j : Fin m) (pat : Fin m → Fin 2) : ctrlSet S j pat 1 0 0 1 = 1

theorem QuantumInfo.Controlled.ctrlSet_mul {m : ℕ} {S : Finset (Fin m)} {j : Fin m} {pat : Fin m → Fin 2} (hjS : j ∉ S) (a b c d a' b' c' d' : ℂ) : ctrlSet S j pat a b c d * ctrlSet S j pat a' b' c' d' = ctrlSet S j pat (a * a' + b * c') (a * b' + b * d') (c * a' + d * c') (c * b' + d * d')

★ Controlled gates on a fixed control set, target and pattern multiply blockwise.

theorem QuantumInfo.Controlled.ctrlSet_conjTranspose {m : ℕ} {S : Finset (Fin m)} {j : Fin m} {pat : Fin m → Fin 2} (hjS : j ∉ S) (a b c d : ℂ) : (ctrlSet S j pat a b c d).conjTranspose = ctrlSet S j pat ((starRingEnd ℂ) a) ((starRingEnd ℂ) c) ((starRingEnd ℂ) b) ((starRingEnd ℂ) d)

theorem QuantumInfo.Controlled.ctrlSet_mem_unitaryGroup {m : ℕ} {S : Finset (Fin m)} {j : Fin m} {pat : Fin m → Fin 2} (hjS : j ∉ S) {a b c d : ℂ} (h1 : (starRingEnd ℂ) a * a + (starRingEnd ℂ) c * c = 1) (h2 : (starRingEnd ℂ) b * b + (starRingEnd ℂ) d * d = 1) (h3 : (starRingEnd ℂ) a * b + (starRingEnd ℂ) c * d = 0) (h4 : (starRingEnd ℂ) b * a + (starRingEnd ℂ) d * c = 0) : ctrlSet S j pat a b c d ∈ Matrix.unitaryGroup (Fin m → Fin 2) ℂ

★ A controlled gate is unitary exactly when its block is.

The gate vocabulary

def QuantumInfo.Controlled.singleGate {m : ℕ} (j : Fin m) (a b c d : ℂ) : Matrix (Fin m → Fin 2) (Fin m → Fin 2) ℂ

A single-qubit gate: no controls.

Equations

• QuantumInfo.Controlled.singleGate j a b c d = QuantumInfo.Controlled.ctrlSet ∅ j (fun (x : Fin m) => 0) a b c d

def QuantumInfo.Controlled.xGate {m : ℕ} (j : Fin m) : Matrix (Fin m → Fin 2) (Fin m → Fin 2) ℂ

The single-qubit bit flip on qubit j.

Equations

• QuantumInfo.Controlled.xGate j = QuantumInfo.Controlled.singleGate j 0 1 1 0

def QuantumInfo.Controlled.cnotGate' {m : ℕ} (a b : Fin m) : Matrix (Fin m → Fin 2) (Fin m → Fin 2) ℂ

CNOT with control a and target b: one control qubit.

Equations

• QuantumInfo.Controlled.cnotGate' a b = QuantumInfo.Controlled.ctrlSet {a} b (fun (x : Fin m) => 1) 0 1 1 0

theorem QuantumInfo.Controlled.singleGate_mem_unitaryGroup {m : ℕ} (j : Fin m) {a b c d : ℂ} (h1 : (starRingEnd ℂ) a * a + (starRingEnd ℂ) c * c = 1) (h2 : (starRingEnd ℂ) b * b + (starRingEnd ℂ) d * d = 1) (h3 : (starRingEnd ℂ) a * b + (starRingEnd ℂ) c * d = 0) (h4 : (starRingEnd ℂ) b * a + (starRingEnd ℂ) d * c = 0) : singleGate j a b c d ∈ Matrix.unitaryGroup (Fin m → Fin 2) ℂ

theorem QuantumInfo.Controlled.xGate_mem_unitaryGroup {m : ℕ} (j : Fin m) : xGate j ∈ Matrix.unitaryGroup (Fin m → Fin 2) ℂ

theorem QuantumInfo.Controlled.xGate_mul_self {m : ℕ} (j : Fin m) : xGate j * xGate j = 1

theorem QuantumInfo.Controlled.cnotGate'_mem_unitaryGroup {m : ℕ} (a b : Fin m) (hab : a ≠ b) : cnotGate' a b ∈ Matrix.unitaryGroup (Fin m → Fin 2) ℂ

theorem QuantumInfo.Controlled.ctrlSet_erase_eq_ctrlGate {m : ℕ} (j : Fin m) (pat : Fin m → Fin 2) (a b c d : ℂ) : ctrlSet (Finset.univ.erase j) j pat a b c d = MultiControlled.ctrlGate j pat a b c d

★ The full control set gives the multiply-controlled gate of #71, so the two-level theory of #70 and #71 applies to it verbatim.