Clifford+T is universal: dense in U(2ⁿ) modulo phase

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #73, part (f) of R-005, which it closes: the last residue of the quantum-computing chain that had a Lean shape.

Glossary: https://glossary.constraintsurfacedynamics.com/clifford-t/ Plain-language, CSD-role and formal statements of Clifford+T universality, with this module as the Lean anchor. Kept symmetric by scripts/check-glossary.sh.

★★ exists_phase_mem_cliffordTmLim: every unitary on m ≥ 1 qubits becomes a limit of Clifford+T circuits after multiplication by a single global phase. The file assembles the whole chain and supplies the three joints it was missing.

The exact product (★★ mem_closure_elementary): every unitary on m qubits is a finite, exact product of CNOTs and single-qubit gates. That is #70's two-level decomposition, then #71's Gray-code sandwich, then #85's control-count recursion. The joint is ★ block_mem_unitaryGroup_of_ctrlSetOf, the converse of ctrlSet_mem_unitaryGroup: the earlier rows deliver a controlled gate known to be unitary, while #85 asks for its 2 × 2 block to be unitary, and the block's unitarity follows by evaluating the relation UᴴU = 1 at the labels that differ only on the target, where the sum collapses to two terms.

The lift. Sending a 2 × 2 gate to the m-qubit gate on one qubit is a monoid homomorphism (gateOfHom) and continuous (continuous_gateOf), so it carries the closure of the one-qubit Clifford+T words into the closure of the m-qubit circuits (★ gateOf_mem_cliffordTmLim). The step that makes "modulo phase" survive is gateOf_smul: a phase on the block is a global phase on the gate, because the gate is the block tensored with the identity, so scalars pull straight out. Were that false the phases of #81 would become relative phases and the argument would not close.

The phases add. The gates that become limits after one global phase are themselves a submonoid (phaseLim), so the exact product of elementary gates inherits a single phase, the sum of the factors' phases, without any bookkeeping over lists.

• ★ ctrlSetOf_eq_of_block, ★ block_mem_unitaryGroup_of_ctrlSetOf, block_mem_unitaryGroup_of_ctrlGate;
• isMultiCtrlX_mem_closure, isMultiCtrlGate_mem_closure, ★ twoLevel_mem_closure, ★★ mem_closure_elementary;
• gateOf_eq_ctrlSetOf, gateOf_apply_of_agree, gateOf_apply_of_not_agree, gateOf_one, gateOf_mul, gateOf_add, gateOf_smul, gateOfHom, continuous_gateOf;
• cliffordTGates, cliffordTm, cliffordTmLim, cliffordTm_le_lim, isClosed_cliffordTmLim, ★ gateOf_mem_cliffordTmLim;
• smul_mul_smul_eq, phaseLim, mem_phaseLim_iff, elementary_le_phaseLim, ★★ exists_phase_mem_cliffordTmLim.

Honest scope

⚠️ Density, not exactness, and no gate counts. The statement is membership in a topological closure: for every unitary and every accuracy there is a Clifford+T circuit that close, which is what gate synthesis needs, and all that is true of a countable gate set. How the circuit's length grows as the accuracy tightens is Solovay–Kitaev, BACKLOG #74, deliberately not claimed. ⚠️ m ≥ 1. The m = 0 case is the scalars and carries no gates. ⚠️ The single-qubit factors of the exact product are genuine U(2) elements; it is only after the approximation step that everything is Clifford+T. The two statements are kept separate on purpose.

References: M. A. Nielsen, I. L. Chuang, Quantum Computation and Quantum Information §4.5 (Theorem 4.1 through §4.5.3); C. M. Dawson, M. A. Nielsen, quant-ph/0505030; CsdLean4/Mathlib/LinearAlgebra/Matrix/TwoLevel.lean (#70), CsdLean4/Mathlib/QuantumInfo/MultiControlled.lean (#71), ControlRecursion.lean (#85) and CliffordTDensity.lean (#81); specs/magic-plan.md; specs/BACKLOG.md #73; specs/residues.tsv R-005; specs/future-work.md.

A unitary controlled gate has a unitary block

The decompositions of #70 and #71 deliver a controlled gate and the knowledge that it is unitary; #85 asks for its 2 × 2 block to be unitary. This is the missing converse of ctrlSet_mem_unitaryGroup: evaluate the unitarity relation at the labels that differ only on the target.

theorem QuantumInfo.Controlled.ctrlSetOf_eq_of_block {m : ℕ} {S : Finset (Fin m)} {j : Fin m} {pat : Fin m → Fin 2} (a b c d : ℂ) : ctrlSetOf S j pat !![a, b; c, d] = ctrlSet S j pat a b c d

theorem QuantumInfo.Controlled.block_mem_unitaryGroup_of_ctrlSetOf {m : ℕ} {S : Finset (Fin m)} {j : Fin m} (hjS : j ∉ S) (pat : Fin m → Fin 2) {M : Matrix (Fin 2) (Fin 2) ℂ} (h : ctrlSetOf S j pat M ∈ Matrix.unitaryGroup (Fin m → Fin 2) ℂ) : M ∈ Matrix.unitaryGroup (Fin 2) ℂ

★ A controlled gate is unitary only if its block is.

theorem QuantumInfo.Controlled.block_mem_unitaryGroup_of_ctrlGate {m : ℕ} {j : Fin m} {pat : Fin m → Fin 2} {a b c d : ℂ} (h : MultiControlled.ctrlGate j pat a b c d ∈ Matrix.unitaryGroup (Fin m → Fin 2) ℂ) : !![a, b; c, d] ∈ Matrix.unitaryGroup (Fin 2) ℂ

Every unitary is an exact product of CNOTs and single-qubit gates

theorem QuantumInfo.Controlled.isMultiCtrlX_mem_closure {m : ℕ} {X : Matrix (Fin m → Fin 2) (Fin m → Fin 2) ℂ} (hX : MultiControlled.IsMultiCtrlX X) : X ∈ Submonoid.closure (elementary m)

theorem QuantumInfo.Controlled.isMultiCtrlGate_mem_closure {m : ℕ} {W : Matrix (Fin m → Fin 2) (Fin m → Fin 2) ℂ} (hW : MultiControlled.IsMultiCtrlGate W) (hWu : W ∈ Matrix.unitaryGroup (Fin m → Fin 2) ℂ) : W ∈ Submonoid.closure (elementary m)

theorem QuantumInfo.Controlled.twoLevel_mem_closure {m : ℕ} {V : Matrix (Fin m → Fin 2) (Fin m → Fin 2) ℂ} (hV : TwoLevel.IsTwoLevel V) (hVu : V ∈ Matrix.unitaryGroup (Fin m → Fin 2) ℂ) : V ∈ Submonoid.closure (elementary m)

★ A two-level unitary is a product of CNOTs and single-qubit gates: #71's Gray-code sandwich fed into #85.

theorem QuantumInfo.Controlled.mem_closure_elementary {m : ℕ} (hm : 0 < m) {U : Matrix (Fin m → Fin 2) (Fin m → Fin 2) ℂ} (hU : U ∈ Matrix.unitaryGroup (Fin m → Fin 2) ℂ) : U ∈ Submonoid.closure (elementary m)

★★ Every unitary on m qubits is an exact product of CNOTs and single-qubit gates — the two-level decomposition of #70, the Gray-code sandwich of #71 and the control-count recursion of #85, composed.

Lifting a single-qubit gate to m qubits

theorem QuantumInfo.Controlled.gateOf_eq_ctrlSetOf {m : ℕ} (j : Fin m) (M : Matrix (Fin 2) (Fin 2) ℂ) : gateOf j M = ctrlSetOf ∅ j (fun (x : Fin m) => 0) M

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

theorem QuantumInfo.Controlled.gateOf_apply_of_not_agree {m : ℕ} {j : Fin m} {k l : Fin m → Fin 2} (hag : ¬∀ (i : Fin m), i ≠ j → k i = l i) (M : Matrix (Fin 2) (Fin 2) ℂ) : gateOf j M k l = 0

theorem QuantumInfo.Controlled.gateOf_one {m : ℕ} (j : Fin m) : gateOf j 1 = 1

theorem QuantumInfo.Controlled.gateOf_mul {m : ℕ} (j : Fin m) (M N : Matrix (Fin 2) (Fin 2) ℂ) : gateOf j (M * N) = gateOf j M * gateOf j N

theorem QuantumInfo.Controlled.gateOf_add {m : ℕ} (j : Fin m) (M N : Matrix (Fin 2) (Fin 2) ℂ) : gateOf j (M + N) = gateOf j M + gateOf j N

theorem QuantumInfo.Controlled.gateOf_smul {m : ℕ} (j : Fin m) (c : ℂ) (M : Matrix (Fin 2) (Fin 2) ℂ) : gateOf j (c • M) = c • gateOf j M

A phase on the block is a global phase on the gate — the step that makes "modulo phase" survive the lift, because the gate is the block tensored with the identity.

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

Lifting a single-qubit gate to m qubits is a monoid homomorphism.

Equations

• QuantumInfo.Controlled.gateOfHom j = { toFun := QuantumInfo.Controlled.gateOf j, map_one' := ⋯, map_mul' := ⋯ }

theorem QuantumInfo.Controlled.continuous_gateOf {m : ℕ} (j : Fin m) : Continuous fun (M : Matrix (Fin 2) (Fin 2) ℂ) => gateOf j M

Clifford+T on m qubits

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

The Clifford+T gate set on m qubits: H and T on any qubit, CNOT on any ordered pair.

Equations

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

noncomputable def QuantumInfo.Controlled.cliffordTm (m : ℕ) : Submonoid (Matrix (Fin m → Fin 2) (Fin m → Fin 2) ℂ)

The monoid of Clifford+T circuits on m qubits.

Equations

• QuantumInfo.Controlled.cliffordTm m = Submonoid.closure (QuantumInfo.Controlled.cliffordTGates m)

noncomputable def QuantumInfo.Controlled.cliffordTmLim (m : ℕ) : Submonoid (Matrix (Fin m → Fin 2) (Fin m → Fin 2) ℂ)

The limits of Clifford+T circuits on m qubits: a closed submonoid.

Equations

• QuantumInfo.Controlled.cliffordTmLim m = (QuantumInfo.Controlled.cliffordTm m).topologicalClosure

theorem QuantumInfo.Controlled.cliffordTm_le_lim {m : ℕ} : cliffordTm m ≤ cliffordTmLim m

theorem QuantumInfo.Controlled.isClosed_cliffordTmLim {m : ℕ} : IsClosed ↑(cliffordTmLim m)

theorem QuantumInfo.Controlled.gateOf_mem_cliffordTmLim {m : ℕ} (j : Fin m) {M : Matrix (Fin 2) (Fin 2) ℂ} (hM : M ∈ SU2.cliffordTLim) : gateOf j M ∈ cliffordTmLim m

★ The one-qubit density transfers to m qubits: lifting is a continuous homomorphism, so it carries the closure of the one-qubit words into the closure of the m-qubit circuits.

Clifford+T is dense in U(2ⁿ) modulo phase

theorem QuantumInfo.Controlled.smul_mul_smul_eq {m : ℕ} (c d : ℂ) (A B : Matrix (Fin m → Fin 2) (Fin m → Fin 2) ℂ) : (c * d) • (A * B) = c • A * d • B

noncomputable def QuantumInfo.Controlled.phaseLim (m : ℕ) : Submonoid (Matrix (Fin m → Fin 2) (Fin m → Fin 2) ℂ)

The gates that become limits of Clifford+T circuits after one global phase. They form a submonoid, which is what lets the phases of the factors add up.

Equations

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

theorem QuantumInfo.Controlled.mem_phaseLim_iff {m : ℕ} {g : Matrix (Fin m → Fin 2) (Fin m → Fin 2) ℂ} : g ∈ phaseLim m ↔ ∃ (φ : ℝ), Euler.expI φ • g ∈ cliffordTmLim m

theorem QuantumInfo.Controlled.elementary_le_phaseLim {m : ℕ} : elementary m ⊆ ↑(phaseLim m)

theorem QuantumInfo.Controlled.exists_phase_mem_cliffordTmLim {m : ℕ} (hm : 0 < m) {U : Matrix (Fin m → Fin 2) (Fin m → Fin 2) ℂ} (hU : U ∈ Matrix.unitaryGroup (Fin m → Fin 2) ℂ) : ∃ (φ : ℝ), Euler.expI φ • U ∈ cliffordTmLim m

★★ Clifford+T is universal: dense in U(2ⁿ) modulo phase. Every unitary on m ≥ 1 qubits becomes a limit of Clifford+T circuits after multiplication by a single global phase. This is the statement R-005 asked for, and it closes it.