A two-level unitary on qubits is a Gray-code sandwich of multiply-controlled gates

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #71, part (d) of R-005 (specs/magic-plan.md, "The split").

On the computational basis Fin m → Fin 2 of m qubits, a multiply-controlled gate ctrlGate j pat a b c d acts by the 2 × 2 block !![a, b; c, d] on qubit j of those basis labels that agree with pat away from j, and as the identity on every other label. The bridge to the two-level matrices of TwoLevel.lean is exact: ★ ctrlGate_eq_twoLevelMat identifies it with the two-level matrix on the adjacent pair pat[j ↦ 0], pat[j ↦ 1]. So a multiply-controlled X (ctrlGate j pat 0 1 1 0) is the transposition of two labels differing in one bit.

Nielsen–Chuang §4.5.2: a two-level unitary on labels u ≠ v becomes a multiply-controlled gate once u is walked to a neighbour of v along a Gray code, each step being a multiply-controlled X. Here the Gray code is the recursion itself: flip one differing bit, conjugate, and the differing set shrinks by one.

• swapMat u v — the transposition of two labels; swapMat_apply (its entries are the permutation's), swapMat_mul_self, swapMat_mem_unitaryGroup;
• ★ swapMat_conj_apply — conjugating by a transposition relabels: (S V S) k l = V (swap u v k) (swap u v l), hence ★ idOutside_swapMat_conj;
• Adjacent u v, diffSet, adjacent_iff_diffSet_card_eq_one;
• ctrlGate, ★ ctrlGate_eq_twoLevelMat, ctrlGate_mem_unitaryGroup, ★ exists_ctrlGate_of_adjacent — a two-level matrix on an adjacent pair is a multiply-controlled gate;
• IsMultiCtrlX, IsMultiCtrlGate;
• ★★ exists_multiCtrl_sandwich — every two-level unitary on qubits is L · W · L⁻¹ with L a list of multiply-controlled Xs and W a single multiply-controlled gate; ★ exists_multiCtrl_list — the same as one flat product, the form #72 consumes.

Honest scope

⚠️ Existence and structure, no gate counts: the Gray walk here flips the differing bits in the order the recursion picks them, and L.length is the Hamming distance minus one, but no optimality or circuit-size claim is made (the two-level count of #70 is #82, landed 2026-09-28 as exists_twoLevel_prod_length, and says nothing about this file's Gray walk; efficiency overall is #74, kept not claimed). Decomposing a multiply-controlled gate into CNOTs and single-qubit gates is #72.

References: M. A. Nielsen, I. L. Chuang, Quantum Computation and Quantum Information §4.5.2; specs/magic-plan.md; specs/BACKLOG.md #71; specs/future-work.md.

Transpositions of basis labels

noncomputable def QuantumInfo.MultiControlled.swapMat {m : ℕ} (u v : Fin m → Fin 2) : Matrix (Fin m → Fin 2) (Fin m → Fin 2) ℂ

The transposition of two basis labels, as a matrix.

Equations

• QuantumInfo.MultiControlled.swapMat u v = QuantumInfo.TwoLevel.twoLevelMat u v 0 1 1 0

theorem QuantumInfo.MultiControlled.swapMat_mem_unitaryGroup {m : ℕ} {u v : Fin m → Fin 2} (huv : u ≠ v) : swapMat u v ∈ Matrix.unitaryGroup (Fin m → Fin 2) ℂ

theorem QuantumInfo.MultiControlled.isTwoLevel_swapMat {m : ℕ} {u v : Fin m → Fin 2} (huv : u ≠ v) : TwoLevel.IsTwoLevel (swapMat u v)

theorem QuantumInfo.MultiControlled.swapMat_mul_self {m : ℕ} {u v : Fin m → Fin 2} (huv : u ≠ v) : swapMat u v * swapMat u v = 1

theorem QuantumInfo.MultiControlled.swapMat_apply {m : ℕ} {u v : Fin m → Fin 2} (huv : u ≠ v) (k l : Fin m → Fin 2) : swapMat u v k l = if k = (Equiv.swap u v) l then 1 else 0

The entries of the transposition matrix are those of the permutation.

theorem QuantumInfo.MultiControlled.swapMat_conj_apply {m : ℕ} {u v : Fin m → Fin 2} (huv : u ≠ v) (V : Matrix (Fin m → Fin 2) (Fin m → Fin 2) ℂ) (k l : Fin m → Fin 2) : (swapMat u v * V * swapMat u v) k l = V ((Equiv.swap u v) k) ((Equiv.swap u v) l)

★ Conjugating by a transposition relabels the matrix.

theorem QuantumInfo.MultiControlled.idOutside_swapMat_conj {m : ℕ} {u u' v : Fin m → Fin 2} (huu' : u ≠ u') (hvu' : v ≠ u') {V : Matrix (Fin m → Fin 2) (Fin m → Fin 2) ℂ} (hid : TwoLevel.IdOutside {u, v} V) : TwoLevel.IdOutside {u', v} (swapMat u u' * V * swapMat u u')

★ Conjugating a two-level matrix by a transposition moves its block to the swapped pair.

Adjacent labels

def QuantumInfo.MultiControlled.diffSet {m : ℕ} (u v : Fin m → Fin 2) : Finset (Fin m)

The set of qubits where two labels differ.

Equations

• QuantumInfo.MultiControlled.diffSet u v = {i : Fin m | u i ≠ v i}

theorem QuantumInfo.MultiControlled.mem_diffSet {m : ℕ} {u v : Fin m → Fin 2} {i : Fin m} : i ∈ diffSet u v ↔ u i ≠ v i

theorem QuantumInfo.MultiControlled.diffSet_eq_empty_iff {m : ℕ} {u v : Fin m → Fin 2} : diffSet u v = ∅ ↔ u = v

def QuantumInfo.MultiControlled.Adjacent {m : ℕ} (u v : Fin m → Fin 2) : Prop

Two labels are adjacent when they differ in exactly one qubit.

Equations

• QuantumInfo.MultiControlled.Adjacent u v = ∃ (j : Fin m), u j ≠ v j ∧ ∀ (i : Fin m), i ≠ j → u i = v i

theorem QuantumInfo.MultiControlled.adjacent_of_diffSet_card_eq_one {m : ℕ} {u v : Fin m → Fin 2} (h : (diffSet u v).card = 1) : Adjacent u v

Multiply-controlled gates

def QuantumInfo.MultiControlled.blockEntry (x y : Fin 2) (a b c d : ℂ) : ℂ

The 2 × 2 block entry selected by a pair of bits.

Equations

• QuantumInfo.MultiControlled.blockEntry x y a b c d = if x = 0 then if y = 0 then a else b else if y = 0 then c else d

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

The multiply-controlled gate: the 2 × 2 block !![a, b; c, d] applied to qubit j of the basis labels agreeing with pat away from j, the identity on all other labels.

Equations

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

theorem QuantumInfo.MultiControlled.eq_update_iff {m : ℕ} {k pat : Fin m → Fin 2} {j : Fin m} {x : Fin 2} : k = Function.update pat j x ↔ (∀ (i : Fin m), i ≠ j → k i = pat i) ∧ k j = x

theorem QuantumInfo.MultiControlled.update_ne_update {m : ℕ} {pat : Fin m → Fin 2} {j : Fin m} : Function.update pat j 0 ≠ Function.update pat j 1

theorem QuantumInfo.MultiControlled.ctrlGate_eq_twoLevelMat {m : ℕ} (j : Fin m) (pat : Fin m → Fin 2) (a b c d : ℂ) : ctrlGate j pat a b c d = TwoLevel.twoLevelMat (Function.update pat j 0) (Function.update pat j 1) a b c d

★ A multiply-controlled gate is the two-level matrix on the adjacent pair it acts on.

theorem QuantumInfo.MultiControlled.ctrlGate_mem_unitaryGroup {m : ℕ} (j : Fin m) (pat : Fin m → Fin 2) {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) : ctrlGate j pat a b c d ∈ Matrix.unitaryGroup (Fin m → Fin 2) ℂ

def QuantumInfo.MultiControlled.IsMultiCtrlX {m : ℕ} (X : Matrix (Fin m → Fin 2) (Fin m → Fin 2) ℂ) : Prop

A multiply-controlled X: the transposition of two labels differing in one qubit.

Equations

• QuantumInfo.MultiControlled.IsMultiCtrlX X = ∃ (j : Fin m) (pat : Fin m → Fin 2), X = QuantumInfo.MultiControlled.ctrlGate j pat 0 1 1 0

def QuantumInfo.MultiControlled.IsMultiCtrlGate {m : ℕ} (W : Matrix (Fin m → Fin 2) (Fin m → Fin 2) ℂ) : Prop

A multiply-controlled single-qubit gate.

Equations

• QuantumInfo.MultiControlled.IsMultiCtrlGate W = ∃ (j : Fin m) (pat : Fin m → Fin 2) (a : ℂ) (b : ℂ) (c : ℂ) (d : ℂ), W = QuantumInfo.MultiControlled.ctrlGate j pat a b c d

theorem QuantumInfo.MultiControlled.twoLevelMat_swap_block {m : ℕ} {u v : Fin m → Fin 2} (huv : u ≠ v) (a b c d : ℂ) : TwoLevel.twoLevelMat u v a b c d = TwoLevel.twoLevelMat v u d c b a

theorem QuantumInfo.MultiControlled.Adjacent.ne {m : ℕ} {u v : Fin m → Fin 2} (h : Adjacent u v) : u ≠ v

theorem QuantumInfo.MultiControlled.adjacent_eq_update {m : ℕ} {u v : Fin m → Fin 2} (hadj : Adjacent u v) : ∃ (j : Fin m), u = Function.update u j 0 ∧ v = Function.update u j 1 ∨ v = Function.update u j 0 ∧ u = Function.update u j 1

For adjacent labels the pair is the multiply-controlled gate's pair, in one of two orders.

theorem QuantumInfo.MultiControlled.exists_ctrlGate_of_adjacent {m : ℕ} {u v : Fin m → Fin 2} (hadj : Adjacent u v) (a b c d : ℂ) : IsMultiCtrlGate (TwoLevel.twoLevelMat u v a b c d)

★ A two-level matrix on an adjacent pair is a multiply-controlled gate.

theorem QuantumInfo.MultiControlled.isMultiCtrlX_swapMat {m : ℕ} {u v : Fin m → Fin 2} (hadj : Adjacent u v) : IsMultiCtrlX (swapMat u v)

★ The transposition of two adjacent labels is a multiply-controlled X.

theorem QuantumInfo.MultiControlled.isMultiCtrlX_mem_unitaryGroup {m : ℕ} {X : Matrix (Fin m → Fin 2) (Fin m → Fin 2) ℂ} (hX : IsMultiCtrlX X) : X ∈ Matrix.unitaryGroup (Fin m → Fin 2) ℂ

The Gray-code decomposition

theorem QuantumInfo.MultiControlled.reverse_prod_mul_prod_of_self_inverse {m : ℕ} (L : List (Matrix (Fin m → Fin 2) (Fin m → Fin 2) ℂ)) (h : ∀ X ∈ L, X * X = 1) : L.reverse.prod * L.prod = 1

theorem QuantumInfo.MultiControlled.exists_multiCtrl_sandwich_aux {m : ℕ} (N : ℕ) (u v : Fin m → Fin 2) (V : Matrix (Fin m → Fin 2) (Fin m → Fin 2) ℂ) : (diffSet u v).card ≤ N → u ≠ v → TwoLevel.IdOutside {u, v} V → ∃ (L : List (Matrix (Fin m → Fin 2) (Fin m → Fin 2) ℂ)) (W : Matrix (Fin m → Fin 2) (Fin m → Fin 2) ℂ), (∀ X ∈ L, IsMultiCtrlX X ∧ X * X = 1) ∧ IsMultiCtrlGate W ∧ V = L.prod * W * L.reverse.prod

The recursion: walking one differing qubit at a time.

theorem QuantumInfo.MultiControlled.exists_multiCtrl_sandwich {m : ℕ} {u v : Fin m → Fin 2} (huv : u ≠ v) {V : Matrix (Fin m → Fin 2) (Fin m → Fin 2) ℂ} (hid : TwoLevel.IdOutside {u, v} V) : ∃ (L : List (Matrix (Fin m → Fin 2) (Fin m → Fin 2) ℂ)) (W : Matrix (Fin m → Fin 2) (Fin m → Fin 2) ℂ), (∀ X ∈ L, IsMultiCtrlX X ∧ X * X = 1) ∧ IsMultiCtrlGate W ∧ V = L.prod * W * L.reverse.prod ∧ (V ∈ Matrix.unitaryGroup (Fin m → Fin 2) ℂ → W ∈ Matrix.unitaryGroup (Fin m → Fin 2) ℂ)

★★ Every two-level matrix on qubits is a Gray-code sandwich: a list of multiply-controlled Xs, one multiply-controlled single-qubit gate, and the list again (each factor being its own inverse). If the matrix is unitary so is the gate.

theorem QuantumInfo.MultiControlled.exists_multiCtrl_list {m : ℕ} {u v : Fin m → Fin 2} (huv : u ≠ v) {V : Matrix (Fin m → Fin 2) (Fin m → Fin 2) ℂ} (hid : TwoLevel.IdOutside {u, v} V) : ∃ (L : List (Matrix (Fin m → Fin 2) (Fin m → Fin 2) ℂ)), (∀ X ∈ L, IsMultiCtrlX X ∨ IsMultiCtrlGate X) ∧ L.prod = V

★ The flat form: a two-level matrix on qubits is a product of multiply-controlled gates — the shape BACKLOG #72 consumes.