The z-y-z Euler decomposition of a 2 × 2 unitary, and the ABC identity

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #84, part (e2) of R-005 (specs/magic-plan.md, "The split"); the piece #81 and #85 share.

Nielsen–Chuang Theorem 4.1: every 2 × 2 unitary is a phase times a product of three rotations about the z, y and z axes — ★★ exists_euler. The proof is the textbook trigonometry, with one economy: passing to determinant one first (★★ exists_euler_of_det_one) leaves only two entries to match, because a determinant-one unitary is !![a, -star b; b, star a] (adjugate_entries, from Uᴴ = adjugate U). Writing a and b in polar form then gives the three angles outright, γ = 2 arccos ‖a‖, β = arg b - arg a, δ = -arg a - arg b, with no case split: where a column degenerates the matching entry is killed by cos (γ/2) = ‖a‖ = 0 or sin (γ/2) = ‖b‖ = 0, and Complex.norm_mul_exp_arg_mul_I holds at 0 too.

Then Nielsen–Chuang Corollary 4.2, the ABC identity: ★ abc_identity and ★ abc_prod_eq_one exhibit A, B, C with A X B X C = R_z(β) R_y(γ) R_z(δ) and A B C = 1, so ★★ exists_abc writes any 2 × 2 unitary as e^{iα} · A X B X C with A B C = 1. That is the form a controlled gate needs: the Xs become the two CNOTs of a one-control circuit, since the control bit 0 leaves A B C = 1 and the control bit 1 inserts them.

• expI, expI_add, star_expI, polar, polar_star — the unit circle written additively;
• rzMat, ryMat (SU2.axisRot about z and y), rzMat_eq, ryMat_eq, rzMat_mul, ryMat_mul, and their unitarity through the new SU2.su2_mem_unitaryGroup, SU2.axisRot_mem_unitaryGroup;
• xMat, xMat_mul_self, xMat_conj_rzMat, xMat_conj_ryMat, xMat_conj_mul — conjugation by X negates both angles, and distributes over products;
• ★ rz_ry_rz_eq — the Euler product as an explicit matrix;
• normSq_col_zero, adjugate_entries — what unitarity and det = 1 give;
• ★★ exists_euler_of_det_one, ★★ exists_euler, ★ abc_prod_eq_one, ★ abc_identity, ★★ exists_abc;
• SU2.axisRot_det, expI_smul_mem_unitaryGroup, exists_su2_of_det_one, exists_axisRot_of_det_one, exists_sqrt_of_det_one, rz_ry_rz_det and ★★ exists_sqrt — every 2 × 2 unitary has a unitary square root, through the axis–angle form of its determinant-one part.

Honest scope

⚠️ This file is 2 × 2 matrices only. The circuit-level statement — that the one-control gate ctrlSet {a} j of #83 is a product of two CNOTs and single-qubit gates — is CsdLean4/Mathlib/QuantumInfo/ControlledSingle.lean, which turns exists_abc into that product. ⚠️ expI t is Complex.exp (t * I), kept as a definition only to keep the entries of the rotation matrices readable; upstream it would be Circle.exp t. Nothing here needs the circle group.

References: M. A. Nielsen, I. L. Chuang, Quantum Computation and Quantum Information Theorem 4.1 and Corollary 4.2 (§4.2, §4.3); CsdLean4/Mathlib/QuantumInfo/SU2Rotation.lean for the axis–angle layer; specs/magic-plan.md; specs/BACKLOG.md #84, #81, #85; specs/future-work.md.

Unitarity of the quaternion matrices

The 2 × 2 layer of SU2Rotation.lean gains the three facts this file needs: a unit quaternion is a unitary matrix.

theorem QuantumInfo.SU2.su2_conjTranspose (w x y z : ℝ) : (su2 w x y z).conjTranspose = su2 w (-x) (-y) (-z)

theorem QuantumInfo.SU2.su2_mem_unitaryGroup {w x y z : ℝ} (h : w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = 1) : su2 w x y z ∈ Matrix.unitaryGroup (Fin 2) ℂ

A unit quaternion is a unitary matrix.

theorem QuantumInfo.SU2.axisRot_mem_unitaryGroup {a b c : ℝ} (hu : a ^ 2 + b ^ 2 + c ^ 2 = 1) (θ : ℝ) : axisRot a b c θ ∈ Matrix.unitaryGroup (Fin 2) ℂ

A rotation about a unit axis is unitary.

The unit circle, written additively

noncomputable def QuantumInfo.Euler.expI (t : ℝ) : ℂ

expI t = e^{it}. A definition only so that the entries of the rotation matrices below read as phases; upstream this is Circle.exp t.

Equations

• QuantumInfo.Euler.expI t = Complex.exp (↑t * Complex.I)

@[simp]

theorem QuantumInfo.Euler.expI_zero : expI 0 = 1

theorem QuantumInfo.Euler.expI_add (s t : ℝ) : expI (s + t) = expI s * expI t

theorem QuantumInfo.Euler.expI_eq (t : ℝ) : expI t = ↑(Real.cos t) + Complex.I * ↑(Real.sin t)

@[simp]

theorem QuantumInfo.Euler.star_expI (t : ℝ) : star (expI t) = expI (-t)

@[simp]

theorem QuantumInfo.Euler.expI_mul_neg (t : ℝ) : expI t * expI (-t) = 1

theorem QuantumInfo.Euler.polar (z : ℂ) : ↑‖z‖ * expI z.arg = z

The polar form of a complex number: z = ‖z‖ e^{i arg z}, at z = 0 too.

theorem QuantumInfo.Euler.polar_star (z : ℂ) : ↑‖z‖ * expI (-z.arg) = star z

The polar form of the conjugate.

The two rotations and the bit flip

noncomputable def QuantumInfo.Euler.rzMat (β : ℝ) : Matrix (Fin 2) (Fin 2) ℂ

R_z(β): the rotation by β about the z axis, diag (e^{-iβ/2}, e^{iβ/2}).

Equations

• QuantumInfo.Euler.rzMat β = QuantumInfo.SU2.axisRot 0 0 1 β

noncomputable def QuantumInfo.Euler.ryMat (γ : ℝ) : Matrix (Fin 2) (Fin 2) ℂ

R_y(γ): the rotation by γ about the y axis, the real rotation matrix.

Equations

• QuantumInfo.Euler.ryMat γ = QuantumInfo.SU2.axisRot 0 1 0 γ

def QuantumInfo.Euler.xMat : Matrix (Fin 2) (Fin 2) ℂ

The 2 × 2 bit flip (X, the first Pauli matrix).

Equations

• QuantumInfo.Euler.xMat = !![0, 1; 1, 0]

theorem QuantumInfo.Euler.rzMat_eq (β : ℝ) : rzMat β = !![expI (-(β / 2)), 0; 0, expI (β / 2)]

theorem QuantumInfo.Euler.ryMat_eq (γ : ℝ) : ryMat γ = !![↑(Real.cos (γ / 2)), -↑(Real.sin (γ / 2)); ↑(Real.sin (γ / 2)), ↑(Real.cos (γ / 2))]

theorem QuantumInfo.Euler.rzMat_mul (s t : ℝ) : rzMat s * rzMat t = rzMat (s + t)

theorem QuantumInfo.Euler.ryMat_mul (s t : ℝ) : ryMat s * ryMat t = ryMat (s + t)

@[simp]

theorem QuantumInfo.Euler.rzMat_zero : rzMat 0 = 1

@[simp]

theorem QuantumInfo.Euler.ryMat_zero : ryMat 0 = 1

theorem QuantumInfo.Euler.rzMat_mem_unitaryGroup (β : ℝ) : rzMat β ∈ Matrix.unitaryGroup (Fin 2) ℂ

theorem QuantumInfo.Euler.ryMat_mem_unitaryGroup (γ : ℝ) : ryMat γ ∈ Matrix.unitaryGroup (Fin 2) ℂ

theorem QuantumInfo.Euler.xMat_mem_unitaryGroup : xMat ∈ Matrix.unitaryGroup (Fin 2) ℂ

@[simp]

theorem QuantumInfo.Euler.xMat_mul_self : xMat * xMat = 1

theorem QuantumInfo.Euler.xMat_conj_rzMat (β : ℝ) : xMat * rzMat β * xMat = rzMat (-β)

Conjugating by X negates a z rotation: X R_z(β) X = R_z(-β).

theorem QuantumInfo.Euler.xMat_conj_ryMat (γ : ℝ) : xMat * ryMat γ * xMat = ryMat (-γ)

Conjugating by X negates a y rotation: X R_y(γ) X = R_y(-γ).

theorem QuantumInfo.Euler.xMat_conj_mul (M N : Matrix (Fin 2) (Fin 2) ℂ) : xMat * M * xMat * (xMat * N * xMat) = xMat * (M * N) * xMat

Conjugation by X is multiplicative.

The Euler product

theorem QuantumInfo.Euler.rz_ry_rz_eq (β γ δ : ℝ) : rzMat β * ryMat γ * rzMat δ = !![expI (-((β + δ) / 2)) * ↑(Real.cos (γ / 2)), -(expI (-((β - δ) / 2)) * ↑(Real.sin (γ / 2))); expI ((β - δ) / 2) * ↑(Real.sin (γ / 2)), expI ((β + δ) / 2) * ↑(Real.cos (γ / 2))]

★ The z-y-z product as an explicit matrix (Nielsen–Chuang (4.12)).

What unitarity gives

theorem QuantumInfo.Euler.normSq_col_zero {U : Matrix (Fin 2) (Fin 2) ℂ} (hU : U ∈ Matrix.unitaryGroup (Fin 2) ℂ) : ‖U 0 0‖ ^ 2 + ‖U 1 0‖ ^ 2 = 1

The first column of a unitary matrix is a unit vector.

theorem QuantumInfo.Euler.adjugate_entries {U : Matrix (Fin 2) (Fin 2) ℂ} (hU : U ∈ Matrix.unitaryGroup (Fin 2) ℂ) (hdet : U.det = 1) : U 1 1 = star (U 0 0) ∧ U 0 1 = -star (U 1 0)

A determinant-one unitary is !![a, -star b; b, star a], because Uᴴ is its adjugate.

The Euler decomposition

theorem QuantumInfo.Euler.exists_euler_of_det_one {U : Matrix (Fin 2) (Fin 2) ℂ} (hU : U ∈ Matrix.unitaryGroup (Fin 2) ℂ) (hdet : U.det = 1) : ∃ (β : ℝ) (γ : ℝ) (δ : ℝ), U = rzMat β * ryMat γ * rzMat δ

★★ The z-y-z Euler decomposition in SU(2): a determinant-one 2 × 2 unitary is R_z(β) R_y(γ) R_z(δ). Half of Nielsen–Chuang Theorem 4.1, and the half that carries the trigonometry: passing to determinant one leaves only two entries to match.

theorem QuantumInfo.Euler.exists_euler {U : Matrix (Fin 2) (Fin 2) ℂ} (hU : U ∈ Matrix.unitaryGroup (Fin 2) ℂ) : ∃ (α : ℝ) (β : ℝ) (γ : ℝ) (δ : ℝ), U = expI α • (rzMat β * ryMat γ * rzMat δ)

★★ Nielsen–Chuang Theorem 4.1: every 2 × 2 unitary is a phase times a z-y-z product of rotations.

The ABC identity

theorem QuantumInfo.Euler.abc_prod_eq_one (β γ δ : ℝ) : rzMat β * ryMat (γ / 2) * (ryMat (-(γ / 2)) * rzMat (-((δ + β) / 2))) * rzMat ((δ - β) / 2) = 1

★ The three factors of Nielsen–Chuang Corollary 4.2 multiply to 1.

theorem QuantumInfo.Euler.abc_identity (β γ δ : ℝ) : rzMat β * ryMat (γ / 2) * xMat * (ryMat (-(γ / 2)) * rzMat (-((δ + β) / 2))) * xMat * rzMat ((δ - β) / 2) = rzMat β * ryMat γ * rzMat δ

★ The ABC identity (Nielsen–Chuang Corollary 4.2): inserting the two Xs turns the product of the three factors into the Euler product.

theorem QuantumInfo.Euler.exists_abc {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 ∧ U = expI α • (A * xMat * B * xMat * C)

★★ Every 2 × 2 unitary is e^{iα} A X B X C with A B C = 1 — the form a controlled gate needs: on the control bit 0 the two Xs are absent and the target gets A B C = 1, on the control bit 1 they are present and it gets e^{-iα} U.

Axis–angle form and square roots

Two consequences of the decomposition that the control-count recursion of #85 and the density argument of #81 both need: a determinant-one unitary is a rotation about some unit axis, and every 2 × 2 unitary has a unitary square root.

theorem QuantumInfo.Euler.expI_smul_mem_unitaryGroup (t : ℝ) {U : Matrix (Fin 2) (Fin 2) ℂ} (hU : U ∈ Matrix.unitaryGroup (Fin 2) ℂ) : expI t • U ∈ Matrix.unitaryGroup (Fin 2) ℂ

A unimodular scalar multiple of a unitary is unitary.

theorem QuantumInfo.Euler.exists_su2_of_det_one {U : Matrix (Fin 2) (Fin 2) ℂ} (hU : U ∈ Matrix.unitaryGroup (Fin 2) ℂ) (hdet : U.det = 1) : ∃ (w : ℝ) (x : ℝ) (y : ℝ) (z : ℝ), w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = 1 ∧ U = SU2.su2 w x y z

A determinant-one unitary is a unit quaternion.

theorem QuantumInfo.Euler.exists_axisRot_of_det_one {U : Matrix (Fin 2) (Fin 2) ℂ} (hU : U ∈ Matrix.unitaryGroup (Fin 2) ℂ) (hdet : U.det = 1) : ∃ (a : ℝ) (b : ℝ) (c : ℝ) (θ : ℝ), a ^ 2 + b ^ 2 + c ^ 2 = 1 ∧ U = SU2.axisRot a b c θ

A determinant-one unitary is a rotation about a unit axis.

theorem QuantumInfo.Euler.exists_sqrt_of_det_one {U : Matrix (Fin 2) (Fin 2) ℂ} (hU : U ∈ Matrix.unitaryGroup (Fin 2) ℂ) (hdet : U.det = 1) : ∃ V ∈ Matrix.unitaryGroup (Fin 2) ℂ, V.det = 1 ∧ V * V = U

A determinant-one unitary has a determinant-one unitary square root.

theorem QuantumInfo.Euler.rz_ry_rz_det (β γ δ : ℝ) : (rzMat β * ryMat γ * rzMat δ).det = 1

theorem QuantumInfo.Euler.exists_sqrt {U : Matrix (Fin 2) (Fin 2) ℂ} (hU : U ∈ Matrix.unitaryGroup (Fin 2) ℂ) : ∃ V ∈ Matrix.unitaryGroup (Fin 2) ℂ, V * V = U

★★ Every 2 × 2 unitary has a unitary square root. The control-count recursion of #85 consumes this: C^k(U) is built from C^{k-1} of a square root of U.