One control: C¹(U) from two CNOTs and single-qubit gates

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #84, part (e2) of R-005 (specs/magic-plan.md, "The split"), the circuit half; the 2 × 2 half is EulerDecomposition.lean.

Nielsen–Chuang Figure 4.6: a gate with one control is a product of two CNOTs and four single-qubit gates — ★★ ctrlOf_eq_circuit. The mechanism is the ABC identity of EulerDecomposition.lean: on the control bit 0 the two CNOTs act trivially and the target sees A B C = 1, on the control bit 1 they each insert an X and it sees e^{iα} A X B X C = U.

The proof needs one piece of gate algebra, and that piece is the content of this file. ctrlChoice is the family of gates that apply the 2 × 2 block M b to the target when the control carries the bit b. It is closed under products, blockwise in each branch separately (★★ ctrlChoice_mul), and it contains every gate the circuit uses:

• a single-qubit gate on the target is ctrlChoice with a constant family (gateOf_eq_ctrlChoice);
• a diagonal single-qubit gate on the control is ctrlChoice with scalar branches (★ diagGate_eq_ctrlChoice) — the one place the control qubit is addressed;
• CNOT is ctrlChoice with branches 1 and X (cnotGate'_eq_ctrlChoice);
• the one-control gate itself is ctrlChoice with branches 1 and U (ctrlOf_eq_ctrlChoice).

So the whole circuit collapses to one ctrlChoice, and the identity is checked one control bit at a time. gateOf and ctrlOf are #83's singleGate and ctrlSet {a} j addressed by a 2 × 2 matrix instead of four scalars (blockEntry_eq_apply is the bridge).

• ctrlChoice, ctrlChoice_apply_of_agree, ctrlChoice_apply_of_not_agree, ctrlChoice_one, ★★ ctrlChoice_mul;
• blockEntry_eq_apply, gateOf, ctrlOf, unitary_entries, gateOf_mem_unitaryGroup, ctrlOf_mem_unitaryGroup;
• gateOf_eq_ctrlChoice, diagGate_apply, ctrlChoice_diag_apply, ★ diagGate_eq_ctrlChoice, cnotGate'_eq_ctrlChoice, ★ ctrlOf_eq_ctrlChoice;
• ★★ ctrlOf_eq_circuit.

Honest scope

⚠️ One control. The control-count recursion (C^k(U) from C^{k-1}(√U)) and the pattern normalisation that frees the control values are BACKLOG #85; ctrlChoice_mul is the algebra they will be stated in.

References: M. A. Nielsen, I. L. Chuang, Quantum Computation and Quantum Information §4.3 (Figure 4.6 and Corollary 4.2); CsdLean4/Mathlib/QuantumInfo/ControlledGate.lean for the gate vocabulary; specs/magic-plan.md; specs/BACKLOG.md #84, #85; specs/future-work.md.

The one-control gate family

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

The gate that applies the 2 × 2 block M b to the target qubit j of those basis labels whose control qubit a carries the bit b.

Equations

• QuantumInfo.Controlled.ctrlChoice a j M k l = if ∀ (i : Fin m), i ≠ j → k i = l i then M (k a) (k j) (l j) else 0

theorem QuantumInfo.Controlled.ctrlChoice_apply_of_agree {m : ℕ} {a j : Fin m} {M : Fin 2 → Matrix (Fin 2) (Fin 2) ℂ} {k l : Fin m → Fin 2} (hag : ∀ (i : Fin m), i ≠ j → k i = l i) : ctrlChoice a j M k l = M (k a) (k j) (l j)

theorem QuantumInfo.Controlled.ctrlChoice_apply_of_not_agree {m : ℕ} {a j : Fin m} {M : Fin 2 → Matrix (Fin 2) (Fin 2) ℂ} {k l : Fin m → Fin 2} (h : ¬∀ (i : Fin m), i ≠ j → k i = l i) : ctrlChoice a j M k l = 0

theorem QuantumInfo.Controlled.ctrlChoice_one {m : ℕ} (a j : Fin m) : (ctrlChoice a j fun (x : Fin 2) => 1) = 1

theorem QuantumInfo.Controlled.ctrlChoice_mul {m : ℕ} {a j : Fin m} (haj : a ≠ j) (M N : Fin 2 → Matrix (Fin 2) (Fin 2) ℂ) : ctrlChoice a j M * ctrlChoice a j N = ctrlChoice a j fun (b : Fin 2) => M b * N b

★★ One-control gates multiply blockwise, in each branch separately. The control bit is untouched by both factors, so the two branches never mix: this is the algebra every circuit identity with one control is checked in.

The vocabulary of #83, addressed by a 2 × 2 matrix

theorem QuantumInfo.Controlled.blockEntry_eq_apply (p q : Fin 2) (x y z w : ℂ) : MultiControlled.blockEntry p q x y z w = !![x, y; z, w] p q

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

The single-qubit gate on j given by a 2 × 2 matrix.

Equations

• QuantumInfo.Controlled.gateOf j M = QuantumInfo.Controlled.singleGate j (M 0 0) (M 0 1) (M 1 0) (M 1 1)

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

The gate M on qubit j controlled by qubit a.

Equations

• QuantumInfo.Controlled.ctrlOf a j M = QuantumInfo.Controlled.ctrlSet {a} j (fun (x : Fin m) => 1) (M 0 0) (M 0 1) (M 1 0) (M 1 1)

theorem QuantumInfo.Controlled.unitary_entries {M : Matrix (Fin 2) (Fin 2) ℂ} (hM : M ∈ Matrix.unitaryGroup (Fin 2) ℂ) : (starRingEnd ℂ) (M 0 0) * M 0 0 + (starRingEnd ℂ) (M 1 0) * M 1 0 = 1 ∧ (starRingEnd ℂ) (M 0 1) * M 0 1 + (starRingEnd ℂ) (M 1 1) * M 1 1 = 1 ∧ (starRingEnd ℂ) (M 0 0) * M 0 1 + (starRingEnd ℂ) (M 1 0) * M 1 1 = 0 ∧ (starRingEnd ℂ) (M 0 1) * M 0 0 + (starRingEnd ℂ) (M 1 1) * M 1 0 = 0

Unitarity of a 2 × 2 matrix, entry by entry — the form #83's gates ask for.

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

theorem QuantumInfo.Controlled.ctrlOf_mem_unitaryGroup {m : ℕ} {a j : Fin m} (haj : a ≠ j) {M : Matrix (Fin 2) (Fin 2) ℂ} (hM : M ∈ Matrix.unitaryGroup (Fin 2) ℂ) : ctrlOf a j M ∈ Matrix.unitaryGroup (Fin m → Fin 2) ℂ

Every gate of the circuit is a ctrlChoice

theorem QuantumInfo.Controlled.gateOf_eq_ctrlChoice {m : ℕ} {a j : Fin m} (M : Matrix (Fin 2) (Fin 2) ℂ) : gateOf j M = ctrlChoice a j fun (x : Fin 2) => M

theorem QuantumInfo.Controlled.diagGate_apply {m : ℕ} {a : Fin m} (p q : ℂ) (k l : Fin m → Fin 2) : singleGate a p 0 0 q k l = if k = l then if k a = 0 then p else q else 0

A diagonal single-qubit gate is diagonal on basis labels, with the value read off the qubit it acts on.

theorem QuantumInfo.Controlled.ctrlChoice_diag_apply {m : ℕ} {a j : Fin m} (p q : ℂ) (k l : Fin m → Fin 2) : ctrlChoice a j (fun (b : Fin 2) => if b = 0 then p • 1 else q • 1) k l = if k = l then if k a = 0 then p else q else 0

The same shape for the one-control gate whose branches are scalars.

theorem QuantumInfo.Controlled.diagGate_eq_ctrlChoice {m : ℕ} {a j : Fin m} (p q : ℂ) : singleGate a p 0 0 q = ctrlChoice a j fun (b : Fin 2) => if b = 0 then p • 1 else q • 1

★ A diagonal single-qubit gate on the control qubit is a one-control gate with scalar branches. This is the only place the control qubit is addressed directly, and it is how the global phase of the ABC identity enters the circuit.

theorem QuantumInfo.Controlled.ctrlOf_eq_ctrlChoice {m : ℕ} {a j : Fin m} (M : Matrix (Fin 2) (Fin 2) ℂ) : ctrlOf a j M = ctrlChoice a j fun (b : Fin 2) => if b = 0 then 1 else M

theorem QuantumInfo.Controlled.cnotGate'_eq_ctrlChoice {m : ℕ} (a j : Fin m) : cnotGate' a j = ctrlChoice a j fun (b : Fin 2) => if b = 0 then 1 else Euler.xMat

The circuit

theorem QuantumInfo.Controlled.ctrlOf_eq_circuit {m : ℕ} {a j : Fin m} (haj : a ≠ j) {U : Matrix (Fin 2) (Fin 2) ℂ} (hU : U ∈ Matrix.unitaryGroup (Fin 2) ℂ) : ∃ (α : ℝ) (A : Matrix (Fin 2) (Fin 2) ℂ) (B : Matrix (Fin 2) (Fin 2) ℂ) (C : Matrix (Fin 2) (Fin 2) ℂ), A ∈ Matrix.unitaryGroup (Fin 2) ℂ ∧ B ∈ Matrix.unitaryGroup (Fin 2) ℂ ∧ C ∈ Matrix.unitaryGroup (Fin 2) ℂ ∧ A * B * C = 1 ∧ ctrlOf a j U = singleGate a 1 0 0 (Euler.expI α) * gateOf j A * cnotGate' a j * gateOf j B * cnotGate' a j * gateOf j C

★★ A gate with one control is a product of two CNOTs and four single-qubit gates (Nielsen–Chuang Figure 4.6). The phase of the ABC identity rides on the control line as the diagonal gate diag (1, e^{iα}); the control bit 0 leaves the target A B C = 1, and the control bit 1 inserts the two Xs, leaving it e^{iα} A X B X C = U.