The commutator decomposition: a small rotation is a commutator of two √ε rotations

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate). BACKLOG #114, the third brick of #74's split.

#112 proved that a commutator of two near-identity unitaries is quadratically nearer the identity. This file proves the converse direction the Solovay–Kitaev recursion needs: a rotation by a small angle is such a commutator, with both factors O(√ε) from the identity. Together the two make the iteration contract.

Everything runs on the quaternion product su2_mul, so the matrix work is real algebra.

What is proved

• ★★★ exists_commutator_of_det_one — the target: every determinant-one unitary is a group commutator of two unitaries within √2·√‖U - 1‖ of the identity, with the commutator exact. Read with #112's contraction, that is the Solovay-Kitaev step in both directions. The two factors are themselves determinant one (SU2Rotation.axisRot_det, det_conj_of_mem_unitary), which the construction always produced and the statement records since #116 — that is what lets the Solovay-Kitaev recursion re-enter itself on them;
• ★★ norm_su2_sub_one — the distance to the identity is √(2 - 2w), where w is the scalar part: star M * M is a scalar for M = su2 w x y z - 1, so the C*-identity ‖M‖² = ‖M⋆M‖ gives the norm with no eigenvalue computation. For a rotation this is ★ norm_axisRot_sub_one;
• ★★★ skComm_eq — the exact commutator identity: for V the rotation by φ about x̂ and W the rotation by φ about ŷ, V W V⋆ W⋆ = su2 (1 - 2s⁴) (2cs³) (-2cs³) (2c²s²) with c = cos(φ/2), s = sin(φ/2). The scalar part is the angle relation — quartic in s, hence quadratic in the angle — and the rest is the axis, which depends on φ;
• ★★ norm_skComm_sub_one = 2sin²(φ/2), ★★★ norm_skV_sub_one_le — the √2·√ε bound — and ★★★ exists_skComm_norm_eq: every distance in [0, 2] is realised exactly, at factor angle 2 arcsin √(ε/2);
• ★★ exists_su2_of_det_one — the su2 parametrisation is onto the determinant-one unitaries (the surjectivity #113 found missing): for det U = 1 the inverse is the adjugate and for a unitary it is the adjoint, so comparing them forces U 1 1 = conj (U 0 0) and U 1 0 = -conj (U 0 1), which is exactly the shape su2 has;
• ★★ su2_conj_pure — conjugating by a π-rotation reflects the axis, v ↦ 2(m̂·v)m̂ - v, and ★★ bisector_reflect — the bisector reflection swaps two vectors of equal length, so the axis can be moved anywhere except to its exact opposite. ★ star_groupCommutator disposes of that last case: the opposite axis belongs to the adjoint of the commutator, which is the same pair in the other order — no perpendicular-vector construction is needed anywhere;
• ★★ norm_conj_sub_one and ★★ conj_groupCommutator — the transport: conjugation changes no distance to the identity, and a conjugate of a commutator is the commutator of the conjugates.

Honest scope

⚠️ V and W are unitaries, not gate words. The commutator is exact and the factors are rotations; nothing here expresses them in a generating set. That is the division of labour the algorithm needs — the net (#113) supplies words, the recursion (#115) approximates these factors by them — and it means this row alone implies no gate count.

⚠️ Determinant one, and 2 × 2. A general unitary needs a phase, exactly as in #81; nothing is claimed for U(2) modulo phase here, and nothing in higher dimension.

⚠️ The constant is √2, and it is not claimed optimal. It comes from sin(φ/4) ≤ sin(φ/2) = √(sin(θ/4)), which is lossy by design: the Solovay-Kitaev exponent does not depend on it.

⚠️ The factor bound needs 0 ≤ φ ≤ π for the standard pair, which is where the sign analysis (2c + 1)(c - 1) ≤ 0 holds; exists_skComm_norm_eq only ever produces angles in that range.

References: C. Dawson, M. Nielsen, The Solovay-Kitaev algorithm, Quantum Inf. Comput. 6 (2006) 81, §4 (the group-commutator decomposition); M. Nielsen, I. Chuang, Quantum Computation and Quantum Information, Appendix 3; SU2Rotation.lean (#80, su2, su2_mul, axisRot), GroupCommutator.lean (#112); specs/BACKLOG.md #114, #74, #112, #113, #115, #116.

The quaternion conjugate, and the distance to the identity

theorem QuantumInfo.SU2.su2_star (w x y z : ℝ) : star (su2 w x y z) = su2 w (-x) (-y) (-z)

theorem QuantumInfo.SU2.su2_star_mul_self {w x y z : ℝ} (hu : w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = 1) : star (su2 w x y z) * su2 w x y z = 1

theorem QuantumInfo.SU2.su2_add_star (w x y z : ℝ) : su2 w x y z + star (su2 w x y z) = ↑(2 * w) • 1

theorem QuantumInfo.SU2.star_su2_sub_one_mul_self {w x y z : ℝ} (hu : w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = 1) : star (su2 w x y z - 1) * (su2 w x y z - 1) = ↑(2 - 2 * w) • 1

theorem QuantumInfo.SU2.norm_su2_sub_one {w x y z : ℝ} (hu : w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = 1) : ‖su2 w x y z - 1‖ = √(2 - 2 * w)

★★ The distance to the identity is √(2 − 2w), with w the scalar part. star M * M is a scalar multiple of 1, so the C*-identity ‖M‖² = ‖M⋆M‖ settles the norm without computing any eigenvalue.

theorem QuantumInfo.SU2.norm_axisRot_sub_one {a b c : ℝ} (hu : a ^ 2 + b ^ 2 + c ^ 2 = 1) (θ : ℝ) : ‖axisRot a b c θ - 1‖ = √(2 - 2 * Real.cos (θ / 2))

★ The distance from a rotation to the identity.

The commutator of two rotations about orthogonal axes

noncomputable def QuantumInfo.SU2.skV (φ : ℝ) : Matrix (Fin 2) (Fin 2) ℂ

The first factor of the standard pair: rotation by φ about x̂.

Equations

• QuantumInfo.SU2.skV φ = QuantumInfo.SU2.axisRot 1 0 0 φ

noncomputable def QuantumInfo.SU2.skW (φ : ℝ) : Matrix (Fin 2) (Fin 2) ℂ

The second factor of the standard pair: rotation by φ about ŷ.

Equations

• QuantumInfo.SU2.skW φ = QuantumInfo.SU2.axisRot 0 1 0 φ

noncomputable def QuantumInfo.SU2.skComm (φ : ℝ) : Matrix (Fin 2) (Fin 2) ℂ

The group commutator of the standard pair. star is the inverse here, both factors being unit quaternions.

Equations

• QuantumInfo.SU2.skComm φ = QuantumInfo.SU2.skV φ * QuantumInfo.SU2.skW φ * star (QuantumInfo.SU2.skV φ) * star (QuantumInfo.SU2.skW φ)

theorem QuantumInfo.SU2.skComm_eq (φ : ℝ) : skComm φ = su2 (1 - 2 * Real.sin (φ / 2) ^ 4) (2 * Real.cos (φ / 2) * Real.sin (φ / 2) ^ 3) (-(2 * Real.cos (φ / 2) * Real.sin (φ / 2) ^ 3)) (2 * Real.cos (φ / 2) ^ 2 * Real.sin (φ / 2) ^ 2)

★★★ The exact commutator identity. With c = cos(φ/2) and s = sin(φ/2), the commutator of the two standard rotations is the unit quaternion (1 - 2s⁴, 2cs³, -2cs³, 2c²s²).

The scalar part 1 - 2s⁴ is the angle relation — quartic in s, hence quadratic in the angle — and the three vector components are the axis, which depends on φ and is not x̂, ŷ or their cross product. Only su2_mul is used: the matrix work is quaternion algebra.

theorem QuantumInfo.SU2.skComm_unit (φ : ℝ) : (1 - 2 * Real.sin (φ / 2) ^ 4) ^ 2 + (2 * Real.cos (φ / 2) * Real.sin (φ / 2) ^ 3) ^ 2 + (-(2 * Real.cos (φ / 2) * Real.sin (φ / 2) ^ 3)) ^ 2 + (2 * Real.cos (φ / 2) ^ 2 * Real.sin (φ / 2) ^ 2) ^ 2 = 1

The commutator is a unit quaternion.

theorem QuantumInfo.SU2.norm_skComm_sub_one (φ : ℝ) : ‖skComm φ - 1‖ = 2 * Real.sin (φ / 2) ^ 2

★★ The commutator's distance to the identity is 2sin²(φ/2) — quadratic in the factors' angle, which is #112's contraction seen from the other side.

theorem QuantumInfo.SU2.norm_skV_sub_one (φ : ℝ) : ‖skV φ - 1‖ = √(2 - 2 * Real.cos (φ / 2))

The factors' distance to the identity.

theorem QuantumInfo.SU2.norm_skW_sub_one (φ : ℝ) : ‖skW φ - 1‖ = √(2 - 2 * Real.cos (φ / 2))

The square-root bound

theorem QuantumInfo.SU2.norm_skV_sub_one_le {φ : ℝ} (h0 : 0 ≤ φ) (hpi : φ ≤ Real.pi) : ‖skV φ - 1‖ ≤ √2 * √‖skComm φ - 1‖

★★★ The factors are within √2·√ε of the identity, where ε is the commutator's own distance. This is the half of Solovay-Kitaev that #112 does not give: not only is a commutator of small things smaller, but the factors needed to produce a given smallness are only square-root large.

theorem QuantumInfo.SU2.norm_skW_sub_one_le {φ : ℝ} (h0 : 0 ≤ φ) (hpi : φ ≤ Real.pi) : ‖skW φ - 1‖ ≤ √2 * √‖skComm φ - 1‖

theorem QuantumInfo.SU2.exists_skComm_norm_eq {ε : ℝ} (h0 : 0 ≤ ε) (h2 : ε ≤ 2) : ∃ (φ : ℝ), 0 ≤ φ ∧ φ ≤ Real.pi ∧ ‖skComm φ - 1‖ = ε ∧ ‖skV φ - 1‖ ≤ √2 * √ε ∧ ‖skW φ - 1‖ ≤ √2 * √ε

★★★ Every distance in [0, 2] is realised by an exact commutator whose factors are √2·√ε-close to the identity. The accuracy is attained exactly, not approached: the factors' angle is 2 arcsin √(ε/2).

Every determinant-one unitary is a unit quaternion

theorem QuantumInfo.SU2.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 w x y z

★★ The su2 parametrisation is onto the determinant-one unitaries. For det U = 1 the inverse is the adjugate, and for a unitary it is the adjoint, so comparing the two gives U 1 1 = conj (U 0 0) and U 1 0 = -conj (U 0 1) — which is exactly the shape su2 has.

This is the surjectivity #113 found missing.

Moving the axis: conjugation by a π-rotation reflects it

theorem QuantumInfo.SU2.su2_conj_pure {m₁ m₂ m₃ : ℝ} (hm : m₁ ^ 2 + m₂ ^ 2 + m₃ ^ 2 = 1) (w x y z : ℝ) : su2 0 m₁ m₂ m₃ * su2 w x y z * star (su2 0 m₁ m₂ m₃) = su2 w (2 * (m₁ * x + m₂ * y + m₃ * z) * m₁ - x) (2 * (m₁ * x + m₂ * y + m₃ * z) * m₂ - y) (2 * (m₁ * x + m₂ * y + m₃ * z) * m₃ - z)

★★ Conjugating by a π-rotation about m̂ reflects the vector part in m̂, fixing the scalar part: v ↦ 2(m̂·v)m̂ − v. The π-rotation about m̂ is the pure unit quaternion su2 0 m₁ m₂ m₃, and this is the whole conjugacy engine: a reflection in the bisector of two axes swaps them.

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

A unit quaternion is a unitary matrix.

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

theorem QuantumInfo.SU2.bisector_reflect {p₁ p₂ p₃ n₁ n₂ n₃ ρ : ℝ} (hp : p₁ ^ 2 + p₂ ^ 2 + p₃ ^ 2 = ρ) (hn : n₁ ^ 2 + n₂ ^ 2 + n₃ ^ 2 = ρ) (hsum : 0 < (p₁ + n₁) ^ 2 + (p₂ + n₂) ^ 2 + (p₃ + n₃) ^ 2) : ∃ (m₁ : ℝ) (m₂ : ℝ) (m₃ : ℝ), m₁ ^ 2 + m₂ ^ 2 + m₃ ^ 2 = 1 ∧ 2 * (m₁ * p₁ + m₂ * p₂ + m₃ * p₃) * m₁ - p₁ = n₁ ∧ 2 * (m₁ * p₁ + m₂ * p₂ + m₃ * p₃) * m₂ - p₂ = n₂ ∧ 2 * (m₁ * p₁ + m₂ * p₂ + m₃ * p₃) * m₃ - p₃ = n₃

★★ The bisector reflection swaps two vectors of equal length. No normalisation is needed: the same bisector works at any common length, which is what keeps the assembly free of axis arithmetic. The hypothesis is exactly that the two are not opposite.

Transport along a unitary conjugation

theorem QuantumInfo.SU2.norm_conj_sub_one {E : Type u_1} [NormedRing E] [StarRing E] [CStarRing E] {S : E} (hS : S ∈ unitary E) (K : E) : ‖S * K * star S - 1‖ = ‖K - 1‖

★★ Conjugating by a unitary changes no distance to the identity.

theorem QuantumInfo.SU2.conj_groupCommutator {E : Type u_1} [Monoid E] [StarMul E] {S : E} (hS : S ∈ unitary E) (V W : E) : S * V * star S * (S * W * star S) * star (S * V * star S) * star (S * W * star S) = S * (V * W * star V * star W) * star S

★★ A conjugate of a commutator is the commutator of the conjugates, so a decomposition at one axis transports to every unitary conjugate of it — and by norm_conj_sub_one the factors keep their distances. This is the consumer for the missing same-angle conjugacy step.

theorem QuantumInfo.SU2.star_groupCommutator {E : Type u_1} [Monoid E] [StarMul E] (V W : E) : star (V * W * star V * star W) = W * V * star W * star V

★ The adjoint of a group commutator is the commutator of the same pair, swapped. This is what removes the antipodal case from the axis argument: an axis opposite the standard commutator's belongs to its adjoint, which is the same two factors in the other order.

The theorem: every determinant-one unitary is such a commutator

theorem QuantumInfo.SU2.det_conj_of_mem_unitary {S : Matrix (Fin 2) (Fin 2) ℂ} (hS : S ∈ unitary (Matrix (Fin 2) (Fin 2) ℂ)) (X : Matrix (Fin 2) (Fin 2) ℂ) : (S * X * star S).det = X.det

Conjugation by a unitary leaves the determinant alone.

theorem QuantumInfo.SU2.exists_commutator_of_det_one {U : Matrix (Fin 2) (Fin 2) ℂ} (hU : U ∈ unitary (Matrix (Fin 2) (Fin 2) ℂ)) (hdet : U.det = 1) : ∃ (V : Matrix (Fin 2) (Fin 2) ℂ) (W : Matrix (Fin 2) (Fin 2) ℂ), V ∈ unitary (Matrix (Fin 2) (Fin 2) ℂ) ∧ W ∈ unitary (Matrix (Fin 2) (Fin 2) ℂ) ∧ V.det = 1 ∧ W.det = 1 ∧ U = V * W * star V * star W ∧ ‖V - 1‖ ≤ √2 * √‖U - 1‖ ∧ ‖W - 1‖ ≤ √2 * √‖U - 1‖

★★★ #114's target: every determinant-one unitary is a group commutator of two unitaries that are only square-root far from the identity.

‖V - 1‖, ‖W - 1‖ ≤ √2·√‖U - 1‖, with the commutator exact. Read with #112's contraction this is the Solovay-Kitaev step in both directions: the commutator of two δ-close unitaries is 2δ²-close, and every ε-close unitary is the commutator of two √(2ε)-close ones.

The proof assembles the file: exists_su2_of_det_one writes U as a unit quaternion; exists_skComm_norm_eq produces a standard-pair commutator at exactly the same distance, hence (by norm_su2_sub_one) with the same scalar part; the vector parts then have the same length, so bisector_reflect and su2_conj_pure rotate one onto the other unless they are opposite — and in that case U is the adjoint of the commutator, which is the same pair in the other order.