Every unitary matrix is a product of two-level unitaries

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

Glossary: https://glossary.constraintsurfacedynamics.com/two-level-unitary/ Plain-language, CSD-role and formal statements of two-level unitaries, with this module as the Lean anchor. Kept symmetric by scripts/check-glossary.sh.

A matrix is two-level when it agrees with the identity outside a {i, j} × {i, j} block (IsTwoLevel, through the predicate IdOutside s for a general index set). Nielsen–Chuang §4.5.1: every unitary is a product of two-level unitaries, and at most d(d − 1)/2 of them suffice. The proof here is Givens elimination, organised as an induction on the support:

• IdOutside, ★ IdOutside.mul, IdOutside.mono, IdOutside.eq_one, IsTwoLevel;
• twoLevelMat i j a b c d — the identity with the 2 × 2 block !![a, b; c, d] at (i, j); ★ twoLevelMat_mul (composition is 2 × 2 matrix multiplication), twoLevelMat_conjTranspose, twoLevelMat_one, ★ twoLevelMat_mem_unitaryGroup (unitary exactly when the block is), and the action on a vector (twoLevelMat_mulVec_apply_*);
• givensMat i j v — the Givens rotation in the (i, j) plane that kills the j-component of v (★ givensMat_mulVec_apply_snd, and givensMat_mulVec_apply_fst for the value it accumulates);
• ★★ exists_clear_column — a product of two-level unitaries kills any prescribed set of components of a vector, leaving the rest untouched, one factor per component cleared, and with the pivot accumulating the norm of the cleared block;
• ★★ exists_twoLevel_prod — every unitary is a product of two-level unitaries (for an index type with at least two elements), via exists_twoLevel_prod_of_idOutside by induction on the support;
• ★★★ exists_twoLevel_prod_length — Nielsen–Chuang's count: at most d(d − 1)/2 factors (BACKLOG #82). Not one factor is spent on a phase: the pivot of an elimination round holds the norm of the column it has just cleared, a nonnegative real, which for a unitary is exactly 1, so the row and column come out of the round already in the form the induction needs. The bookkeeping is Pascal's rule, (m − 1) + Nat.choose (m − 1) 2 = Nat.choose m 2, with isTwoLevel_of_idOutside_card_le_two as the base case: on a block of at most two indices the matrix is two-level.

Honest scope

⚠️ The count is an upper bound — which is all Nielsen–Chuang §4.5.1 asserts. No matching lower bound is proved: nothing here says that d(d − 1)/2 factors are necessary. And it counts two-level factors, not elementary gates: the CNOT-and-single-qubit-gate count of a unitary is the efficiency row BACKLOG #74, kept not claimed. exists_twoLevel_prod is retained alongside the counted version because its consumers (the Clifford+T density of #71–#73) need no count.

References: M. A. Nielsen, I. L. Chuang, Quantum Computation and Quantum Information §4.5.1; G. H. Golub, C. F. Van Loan, Matrix Computations §5.1 (Givens rotations); specs/magic-plan.md; specs/BACKLOG.md #70, #82; specs/future-work.md.

Agreeing with the identity outside a block

def QuantumInfo.TwoLevel.IdOutside {n : Type u_1} [DecidableEq n] (s : Finset n) (U : Matrix n n ℂ) : Prop

U agrees with the identity outside the block s × s.

Equations

• QuantumInfo.TwoLevel.IdOutside s U = ∀ (k l : n), k ∉ s ∨ l ∉ s → U k l = if k = l then 1 else 0

theorem QuantumInfo.TwoLevel.IdOutside.one {n : Type u_1} [DecidableEq n] (s : Finset n) : IdOutside s 1

theorem QuantumInfo.TwoLevel.IdOutside.mono {n : Type u_1} [DecidableEq n] {s t : Finset n} {U : Matrix n n ℂ} (hst : s ⊆ t) (h : IdOutside s U) : IdOutside t U

theorem QuantumInfo.TwoLevel.IdOutside.mul {n : Type u_1} [Fintype n] [DecidableEq n] {s : Finset n} {U V : Matrix n n ℂ} (hU : IdOutside s U) (hV : IdOutside s V) : IdOutside s (U * V)

Outside its block a matrix has a single nonzero entry in each row and column, so the sum defining a product collapses.

theorem QuantumInfo.TwoLevel.IdOutside.eq_one {n : Type u_1} [DecidableEq n] {U : Matrix n n ℂ} (h : IdOutside ∅ U) : U = 1

theorem QuantumInfo.TwoLevel.IdOutside.list_prod {n : Type u_1} [Fintype n] [DecidableEq n] {s : Finset n} {L : List (Matrix n n ℂ)} (h : ∀ V ∈ L, IdOutside s V) : IdOutside s L.prod

def QuantumInfo.TwoLevel.IsTwoLevel {n : Type u_1} [DecidableEq n] (U : Matrix n n ℂ) : Prop

A two-level matrix agrees with the identity outside a {i, j} × {i, j} block.

Equations

• QuantumInfo.TwoLevel.IsTwoLevel U = ∃ (i : n) (j : n), i ≠ j ∧ QuantumInfo.TwoLevel.IdOutside {i, j} U

The two-level matrices

def QuantumInfo.TwoLevel.twoLevelMat {n : Type u_1} [DecidableEq n] (i j : n) (a b c d : ℂ) : Matrix n n ℂ

The identity with the 2 × 2 block !![a, b; c, d] inserted in the rows and columns i and j.

Equations

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

@[simp]

theorem QuantumInfo.TwoLevel.twoLevelMat_apply_fst_fst {n : Type u_1} [DecidableEq n] {i j : n} {a b c d : ℂ} : twoLevelMat i j a b c d i i = a

@[simp]

theorem QuantumInfo.TwoLevel.twoLevelMat_apply_fst_snd {n : Type u_1} [DecidableEq n] {i j : n} {a b c d : ℂ} (hij : i ≠ j) : twoLevelMat i j a b c d i j = b

@[simp]

theorem QuantumInfo.TwoLevel.twoLevelMat_apply_snd_fst {n : Type u_1} [DecidableEq n] {i j : n} {a b c d : ℂ} (hij : i ≠ j) : twoLevelMat i j a b c d j i = c

@[simp]

theorem QuantumInfo.TwoLevel.twoLevelMat_apply_snd_snd {n : Type u_1} [DecidableEq n] {i j : n} {a b c d : ℂ} (hij : i ≠ j) : twoLevelMat i j a b c d j j = d

theorem QuantumInfo.TwoLevel.twoLevelMat_apply_of_row_ne {n : Type u_1} [DecidableEq n] {i j : n} {a b c d : ℂ} {k : n} (hki : k ≠ i) (hkj : k ≠ j) (l : n) : twoLevelMat i j a b c d k l = if k = l then 1 else 0

theorem QuantumInfo.TwoLevel.twoLevelMat_apply_of_col_ne {n : Type u_1} [DecidableEq n] {i j : n} {a b c d : ℂ} {k l : n} (hli : l ≠ i) (hlj : l ≠ j) : twoLevelMat i j a b c d k l = if k = l then 1 else 0

theorem QuantumInfo.TwoLevel.idOutside_twoLevelMat {n : Type u_1} [DecidableEq n] {i j : n} {a b c d : ℂ} : IdOutside {i, j} (twoLevelMat i j a b c d)

theorem QuantumInfo.TwoLevel.isTwoLevel_twoLevelMat {n : Type u_1} [DecidableEq n] {i j : n} {a b c d : ℂ} (hij : i ≠ j) : IsTwoLevel (twoLevelMat i j a b c d)

theorem QuantumInfo.TwoLevel.twoLevelMat_one {n : Type u_1} [DecidableEq n] {i j : n} (hij : i ≠ j) : twoLevelMat i j 1 0 0 1 = 1

theorem QuantumInfo.TwoLevel.sum_eq_pair {n : Type u_1} [Fintype n] [DecidableEq n] {i j : n} (hij : i ≠ j) (f : n → ℂ) (h : ∀ (m : n), m ≠ i → m ≠ j → f m = 0) : ∑ m : n, f m = f i + f j

A sum over the index type whose summand vanishes off {i, j}.

theorem QuantumInfo.TwoLevel.mul_apply_of_idOutside_pair {n : Type u_1} [Fintype n] [DecidableEq n] {i j : n} (hij : i ≠ j) (U V : Matrix n n ℂ) (hU : IdOutside {i, j} U) (k l : n) : (U * V) k l = if k = i ∨ k = j then U k i * V i l + U k j * V j l else V k l

Multiplying by a matrix supported in the {i, j} block collapses the sum: rows outside the block are copied, rows inside it combine only the i-th and j-th rows of the other factor.

theorem QuantumInfo.TwoLevel.twoLevelMat_mul {n : Type u_1} [Fintype n] [DecidableEq n] {i j : n} (hij : i ≠ j) (a b c d a' b' c' d' : ℂ) : twoLevelMat i j a b c d * twoLevelMat i j a' b' c' d' = twoLevelMat i j (a * a' + b * c') (a * b' + b * d') (c * a' + d * c') (c * b' + d * d')

★ Composition of two-level matrices in the same block is 2 × 2 matrix multiplication.

theorem QuantumInfo.TwoLevel.twoLevelMat_conjTranspose {n : Type u_1} [DecidableEq n] {i j : n} (hij : i ≠ j) (a b c d : ℂ) : (twoLevelMat i j a b c d).conjTranspose = twoLevelMat i j ((starRingEnd ℂ) a) ((starRingEnd ℂ) c) ((starRingEnd ℂ) b) ((starRingEnd ℂ) d)

theorem QuantumInfo.TwoLevel.twoLevelMat_mem_unitaryGroup {n : Type u_1} [Fintype n] [DecidableEq n] {i j : n} (hij : i ≠ j) {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) : twoLevelMat i j a b c d ∈ Matrix.unitaryGroup n ℂ

★ A two-level matrix is unitary exactly when its 2 × 2 block is: the columns must be orthonormal.

The action on a vector

theorem QuantumInfo.TwoLevel.twoLevelMat_mulVec_apply_fst {n : Type u_1} [Fintype n] [DecidableEq n] {i j : n} {a b c d : ℂ} (hij : i ≠ j) (v : n → ℂ) : (twoLevelMat i j a b c d).mulVec v i = a * v i + b * v j

theorem QuantumInfo.TwoLevel.twoLevelMat_mulVec_apply_snd {n : Type u_1} [Fintype n] [DecidableEq n] {i j : n} {a b c d : ℂ} (hij : i ≠ j) (v : n → ℂ) : (twoLevelMat i j a b c d).mulVec v j = c * v i + d * v j

theorem QuantumInfo.TwoLevel.twoLevelMat_mulVec_apply_of_ne {n : Type u_1} [Fintype n] [DecidableEq n] {i j : n} {a b c d : ℂ} {k : n} (hki : k ≠ i) (hkj : k ≠ j) (v : n → ℂ) : (twoLevelMat i j a b c d).mulVec v k = v k

The Givens rotation

noncomputable def QuantumInfo.TwoLevel.givensMat {n : Type u_1} [DecidableEq n] (i j : n) (v : n → ℂ) : Matrix n n ℂ

The Givens rotation in the (i, j) plane that kills the j-component of v.

Equations

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

theorem QuantumInfo.TwoLevel.isTwoLevel_givensMat {n : Type u_1} [DecidableEq n] {i j : n} (hij : i ≠ j) (v : n → ℂ) : IsTwoLevel (givensMat i j v)

theorem QuantumInfo.TwoLevel.idOutside_givensMat {n : Type u_1} [DecidableEq n] {i j : n} (v : n → ℂ) : IdOutside {i, j} (givensMat i j v)

theorem QuantumInfo.TwoLevel.normSq_add_nonneg {n : Type u_1} {i j : n} (v : n → ℂ) : 0 ≤ Complex.normSq (v i) + Complex.normSq (v j)

theorem QuantumInfo.TwoLevel.sqrt_normSq_ne_zero {n : Type u_1} {i j : n} (v : n → ℂ) (h : Complex.normSq (v i) + Complex.normSq (v j) ≠ 0) : ↑√(Complex.normSq (v i) + Complex.normSq (v j)) ≠ 0

In the nonzero case the radius is a nonzero complex number.

theorem QuantumInfo.TwoLevel.sq_sqrt_normSq {n : Type u_1} {i j : n} (v : n → ℂ) : ↑√(Complex.normSq (v i) + Complex.normSq (v j)) ^ 2 = ↑(Complex.normSq (v i)) + ↑(Complex.normSq (v j))

The radius squares to the sum of the two squared moduli.

theorem QuantumInfo.TwoLevel.conj_sqrt_normSq {n : Type u_1} {i j : n} (v : n → ℂ) : (starRingEnd ℂ) ↑√(Complex.normSq (v i) + Complex.normSq (v j)) = ↑√(Complex.normSq (v i) + Complex.normSq (v j))

theorem QuantumInfo.TwoLevel.givensMat_mem_unitaryGroup {n : Type u_1} [Fintype n] [DecidableEq n] {i j : n} (v : n → ℂ) (hij : i ≠ j) : givensMat i j v ∈ Matrix.unitaryGroup n ℂ

theorem QuantumInfo.TwoLevel.givensMat_mulVec_apply_snd {n : Type u_1} [Fintype n] [DecidableEq n] {i j : n} (v : n → ℂ) (hij : i ≠ j) : (givensMat i j v).mulVec v j = 0

★ The Givens rotation kills the j-component.

theorem QuantumInfo.TwoLevel.givensMat_mulVec_apply_fst {n : Type u_1} [Fintype n] [DecidableEq n] {i j : n} (v : n → ℂ) (hij : i ≠ j) : (givensMat i j v).mulVec v i = ↑√(Complex.normSq (v i) + Complex.normSq (v j))

The i-component accumulates the radius.

theorem QuantumInfo.TwoLevel.givensMat_mulVec_apply_of_ne {n : Type u_1} [Fintype n] [DecidableEq n] {i j : n} (v : n → ℂ) {k : n} (hki : k ≠ i) (hkj : k ≠ j) : (givensMat i j v).mulVec v k = v k

Clearing the components of a vector

theorem QuantumInfo.TwoLevel.exists_clear_column {n : Type u_1} [Fintype n] [DecidableEq n] (i : n) (s : Finset n) (his : i ∉ s) (v : n → ℂ) : ∃ (L : List (Matrix n n ℂ)), (∀ V ∈ L, IsTwoLevel V ∧ V ∈ Matrix.unitaryGroup n ℂ ∧ IdOutside (insert i s) V) ∧ L.length = s.card ∧ (∀ k ∈ s, L.prod.mulVec v k = 0) ∧ (∀ (k : n), k ≠ i → k ∉ s → L.prod.mulVec v k = v k) ∧ Complex.normSq (L.prod.mulVec v i) = ∑ k ∈ insert i s, Complex.normSq (v k) ∧ (s.Nonempty → L.prod.mulVec v i = ↑√(∑ k ∈ insert i s, Complex.normSq (v k)))

★★ A product of two-level unitaries kills any prescribed set of components of a vector, leaving every other component except the i-th untouched — one factor per component cleared, and with the i-th component accumulating the norm of the block. That the accumulated value is a nonnegative real is what makes the Nielsen–Chuang count tight: the pivot needs no separate phase-fixing factor.

The decomposition

theorem QuantumInfo.TwoLevel.unitaryGroup_list_prod_mem {n : Type u_1} [Fintype n] [DecidableEq n] {L : List (Matrix n n ℂ)} (h : ∀ V ∈ L, V ∈ Matrix.unitaryGroup n ℂ) : L.prod ∈ Matrix.unitaryGroup n ℂ

theorem QuantumInfo.TwoLevel.IsTwoLevel.conjTranspose {n : Type u_1} [DecidableEq n] {U : Matrix n n ℂ} (h : IsTwoLevel U) : IsTwoLevel U.conjTranspose

The conjugate transpose of a two-level matrix is two-level in the same block.

theorem QuantumInfo.TwoLevel.reverse_map_conjTranspose_prod_mul {n : Type u_1} [Fintype n] [DecidableEq n] (L : List (Matrix n n ℂ)) (h : ∀ V ∈ L, V ∈ Matrix.unitaryGroup n ℂ) : (List.map (fun (V : Matrix n n ℂ) => V.conjTranspose) L).reverse.prod * L.prod = 1

The reversed list of adjoints inverts the product of a list of unitaries.

theorem QuantumInfo.TwoLevel.row_eq_of_col_eq {n : Type u_1} [Fintype n] [DecidableEq n] {U : Matrix n n ℂ} (hU : U ∈ Matrix.unitaryGroup n ℂ) (i : n) (hcol : ∀ (k : n), k ≠ i → U k i = 0) : (starRingEnd ℂ) (U i i) * U i i = 1 ∧ ∀ (l : n), l ≠ i → U i l = 0

The column of a unitary matrix that has been cleared to a multiple of a basis vector has that multiple of modulus one, and the corresponding row is cleared too.

theorem QuantumInfo.TwoLevel.sum_normSq_col {n : Type u_1} [Fintype n] [DecidableEq n] {U : Matrix n n ℂ} (hU : U ∈ Matrix.unitaryGroup n ℂ) (i : n) : ∑ k : n, Complex.normSq (U k i) = 1

The squared modulus of the i-th column of a unitary is 1.

theorem QuantumInfo.TwoLevel.isTwoLevel_of_idOutside_card_le_two {n : Type u_1} [Fintype n] [DecidableEq n] (hcard : 1 < Fintype.card n) {s : Finset n} (hs : s.card ≤ 2) (hne : s.Nonempty) {U : Matrix n n ℂ} (hid : IdOutside s U) : IsTwoLevel U

A unitary that is the identity outside a block of at most two indices is two-level.

theorem QuantumInfo.TwoLevel.exists_twoLevel_prod_of_idOutside {n : Type u_1} [Fintype n] [DecidableEq n] (hcard : 1 < Fintype.card n) (s : Finset n) (U : Matrix n n ℂ) : U ∈ Matrix.unitaryGroup n ℂ → IdOutside s U → ∃ (L : List (Matrix n n ℂ)), (∀ V ∈ L, IsTwoLevel V ∧ V ∈ Matrix.unitaryGroup n ℂ) ∧ L.prod = U ∧ L.length ≤ (max s.card 2).choose 2

The Nielsen–Chuang count. The decomposition, by induction on the support: a unitary that is the identity outside a block of m indices is a product of at most (max m 2).choose 2 two-level unitaries — m(m − 1)/2 once m ≥ 2, the max covering only the degenerate one-index case, where the matrix is a bare phase and costs one factor.

theorem QuantumInfo.TwoLevel.exists_twoLevel_prod {n : Type u_1} [Fintype n] [DecidableEq n] (hcard : 1 < Fintype.card n) (U : Matrix n n ℂ) (hU : U ∈ Matrix.unitaryGroup n ℂ) : ∃ (L : List (Matrix n n ℂ)), (∀ V ∈ L, IsTwoLevel V ∧ V ∈ Matrix.unitaryGroup n ℂ) ∧ L.prod = U

★★ Every unitary matrix is a product of two-level unitaries (Nielsen–Chuang §4.5.1), for an index type with at least two elements.

theorem QuantumInfo.TwoLevel.exists_twoLevel_prod_length {n : Type u_1} [Fintype n] [DecidableEq n] (hcard : 1 < Fintype.card n) (U : Matrix n n ℂ) (hU : U ∈ Matrix.unitaryGroup n ℂ) : ∃ (L : List (Matrix n n ℂ)), (∀ V ∈ L, IsTwoLevel V ∧ V ∈ Matrix.unitaryGroup n ℂ) ∧ L.prod = U ∧ L.length ≤ Fintype.card n * (Fintype.card n - 1) / 2

★★★ The Nielsen–Chuang bound: d(d − 1)/2 two-level factors suffice. Every d × d unitary (d ≥ 2) is a product of at most d(d − 1)/2 two-level unitaries — the count of §4.5.1, tight for d = 2. The construction is Givens elimination, and the reason no factor is wasted on phases is exists_clear_column: the pivot accumulates the norm of the column, which for a unitary is exactly 1.