Gate time from the spectral arc of the eigenphases

An ordered product U = ∏ₖ exp (−i τₖ Hₖ) (τₖ ≥ 0, Hₖ Hermitian) whose Hamiltonians have spectral half-width ‖Hₖ − cₖ • 1‖ ≤ Ω / 2 satisfies, up to the global phase e^{−i ∑ τₖ cₖ}, V = ∏ₖ exp (−i τₖ (Hₖ − cₖ)), and V moves every unit vector by at most (Ω / 2) ∑ τₖ in the sphere angle sAngle u v = arccos (Re ⟪u, v⟫) (not the projective Fubini–Study angle, which forgets the phase). Consequently every eigenvalue e^{iθ} of V has |θ| ≤ (Ω / 2) ∑ τₖ (representative θ ∈ [−π, π]): all eigenphases of the gate lie in an arc of length Ω ∑ τₖ modulo 2π. This removes the restriction |Δφ| ≤ π of QSL.Gate.gate_time_ge_eigenphase_gap.

This is the finite-dimensional, piecewise-constant version of the classical spectral-arc bound for products of unitaries (Nudel'man–Švarcman 1958; Thompson 1986; Miglioli, arXiv:2310.06331, Thm 4.4 / Cor 4.5). Nelson and Barnes, arXiv:2604.23031, eq. (3) state T ≥ Δφ⋆ / Ω. The proof is elementary: the sphere angle satisfies the triangle inequality (Mathlib's InnerProductGeometry.angle_le_angle_add_angle), is invariant under unitaries, and a Duhamel estimate with N equal pieces and N → ∞ bounds one step.

For the two-qubit gate exp (i π/4 (2 Z⊗I + I⊗Z)) = diag (e^{3iπ/4}, e^{iπ/4}, e^{−iπ/4}, e^{−3iπ/4}) (Nelson–Barnes, Table I) four eigenphases spaced by π/2 do not fit in an arc shorter than 3π/2, so Ω ∑ τₖ ≥ 3π/2.

Main results

• QSL.Gate.sAngle: the sphere angle arccos (Re ⟪u, v⟫)
• QSL.Gate.sAngle_le_sAngle_add_sAngle, QSL.Gate.sAngle_act_act: triangle inequality, invariance under a unitary
• QSL.Gate.sAngle_exp_le: sAngle (exp Y ψ) ψ ≤ ‖Y‖ for skew-Hermitian Y
• QSL.Gate.sAngle_centred_le_time: sAngle (V v) v ≤ (Ω / 2) ∑ τₖ for the centred product V
• QSL.Gate.abs_le_of_eigen: |θ| ≤ (Ω / 2) ∑ τₖ for an eigenphase θ ∈ [−π, π] of V
• QSL.Gate.spectral_arc_le_time: all eigenphases of G fit in an arc of length Ω ∑ τₖ
• QSL.Gate.u4d_time_ge: 3π/2 ≤ Ω ∑ τₖ for diag (e^{3iπ/4}, e^{iπ/4}, e^{−iπ/4}, e^{−3iπ/4})

References

• A. A. Nudel'man, P. A. Švarcman, The spectrum of the product of unitary matrices (Russian), Uspehi Mat. Nauk 13 (1958), no. 6 (84), 111–117 (as cited in Miglioli).
• R. C. Thompson, Proof of a conjectured exponential formula, Linear and Multilinear Algebra 19 (1986), no. 2, 187–197 (as cited in Miglioli).
• M. Miglioli, Geometry of spectral bounds of curves of unitary operators, arXiv:2310.06331, Thm 4.4 and Cor 4.5.
• H. Nelson, E. Barnes, How fast can a quantum gate be? Exact speed limits from geometry, arXiv:2604.23031 (2026), eq. (3) and Table I.

The sphere angle

noncomputable def QSL.Gate.sAngle {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (u v : E) : ℝ

The sphere angle arccos (Re ⟪u, v⟫) between (unit) vectors; unlike fsAngle it keeps the phase.

Equations

• QSL.Gate.sAngle u v = Real.arccos (inner ℂ u v).re

theorem QSL.Gate.sAngle_comm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (u v : E) : sAngle u v = sAngle v u

theorem QSL.Gate.sAngle_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {u : E} (hu : ‖u‖ = 1) : sAngle u u = 0

theorem QSL.Gate.sAngle_le_sAngle_add_sAngle {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {u v w : E} (hu : ‖u‖ = 1) (hv : ‖v‖ = 1) (hw : ‖w‖ = 1) : sAngle u w ≤ sAngle u v + sAngle v w

Triangle inequality for the sphere angle of unit vectors (from Mathlib's InnerProductGeometry.angle_le_angle_add_angle for the underlying real inner product space).

theorem QSL.Gate.sAngle_le_of_norm_sub_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {x y : E} (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) {c : ℝ} (h : ‖x - y‖ ≤ c) : sAngle x y ≤ Real.arccos (1 - c ^ 2 / 2)

Chord bound: unit vectors at distance at most c are at sphere angle at most arccos (1 − c²/2).

Unitary invariance

theorem QSL.Gate.sAngle_act_act {n : Type u_1} [Fintype n] [DecidableEq n] {U : Matrix n n ℂ} (hU : U ∈ Matrix.unitaryGroup n ℂ) (u v : EuclideanSpace ℂ n) : sAngle (TwoQubit.act U u) (TwoQubit.act U v) = sAngle u v

The sphere angle is invariant under a unitary applied to both vectors.

One step: sAngle (exp Y ψ) ψ ≤ ‖Y‖

theorem QSL.Gate.sAngle_exp_le {n : Type u_1} [Fintype n] [DecidableEq n] (Y : Matrix n n ℂ) (hY : Y.conjTranspose = -Y) (ψ : EuclideanSpace ℂ n) (hψ : ‖ψ‖ = 1) : sAngle (TwoQubit.act (NormedSpace.exp Y) ψ) ψ ≤ ‖Y‖

Duhamel step on the sphere. For skew-Hermitian Y and a unit vector ψ, sAngle (exp Y ψ) ψ ≤ ‖Y‖.

The chain

noncomputable def QSL.Gate.centredStep {n : Type u_1} [Fintype n] [DecidableEq n] (s : ℝ × ℝ × Matrix n n ℂ) : Matrix n n ℂ

The centred evolution of one step: exp (−i τ (H − c • 1)).

Equations

• QSL.Gate.centredStep s = NormedSpace.exp ((-↑s.1 * Complex.I) • (s.2.2 - ↑s.2.1 • 1))

theorem QSL.Gate.sAngle_centred_le_time {n : Type u_1} [Fintype n] [DecidableEq n] (Ω : ℝ) (steps : List (ℝ × ℝ × Matrix n n ℂ)) (hτ : ∀ s ∈ steps, 0 ≤ s.1) (hH : ∀ s ∈ steps, s.2.2.IsHermitian) (hΩ : ∀ s ∈ steps, ‖s.2.2 - ↑s.2.1 • 1‖ ≤ Ω / 2) (v : EuclideanSpace ℂ n) (hv : ‖v‖ = 1) : sAngle (TwoQubit.act (List.map centredStep steps).prod v) v ≤ Ω / 2 * (List.map Prod.fst steps).sum

Sphere-angle bound for the centred product. Let V = ∏ₖ exp (−i τₖ (Hₖ − cₖ • 1)) with τₖ ≥ 0, Hₖ Hermitian and ‖Hₖ − cₖ • 1‖ ≤ Ω / 2. Then sAngle (V v) v ≤ (Ω / 2) · ∑ τₖ for every unit vector v.

Eigenphases of the centred product

theorem QSL.Gate.sAngle_eigen {n : Type u_1} [Fintype n] {V : Matrix n n ℂ} {ξ : EuclideanSpace ℂ n} (hξ : ‖ξ‖ = 1) {θ : ℝ} (hθ : |θ| ≤ Real.pi) (hV : TwoQubit.act V ξ = Complex.exp (↑θ * Complex.I) • ξ) : sAngle (TwoQubit.act V ξ) ξ = |θ|

If ξ is a unit eigenvector, V ξ = e^{iθ} ξ, with |θ| ≤ π, then sAngle (V ξ) ξ = |θ|, and by the chain bound |θ| ≤ (Ω / 2) ∑ τₖ.

theorem QSL.Gate.abs_le_of_eigen {n : Type u_1} [Fintype n] [DecidableEq n] (Ω : ℝ) (steps : List (ℝ × ℝ × Matrix n n ℂ)) (hτ : ∀ s ∈ steps, 0 ≤ s.1) (hH : ∀ s ∈ steps, s.2.2.IsHermitian) (hΩ : ∀ s ∈ steps, ‖s.2.2 - ↑s.2.1 • 1‖ ≤ Ω / 2) (ξ : EuclideanSpace ℂ n) (hξ : ‖ξ‖ = 1) {θ : ℝ} (hθ : |θ| ≤ Real.pi) (hV : TwoQubit.act (List.map centredStep steps).prod ξ = Complex.exp (↑θ * Complex.I) • ξ) : |θ| ≤ Ω / 2 * (List.map Prod.fst steps).sum

Eigenphase bound. In the situation of sAngle_centred_le_time, an eigenvalue e^{iθ} of V with unit eigenvector and |θ| ≤ π has |θ| ≤ (Ω / 2) · ∑ τₖ.

Relating U to the centred product

def QSL.Gate.phaseSum {n : Type u_1} (steps : List (ℝ × ℝ × Matrix n n ℂ)) : ℝ

The total centring phase ∑ τₖ cₖ.

Equations

• QSL.Gate.phaseSum steps = (List.map (fun (s : ℝ × ℝ × Matrix n n ℂ) => s.1 * s.2.1) steps).sum

theorem QSL.Gate.spectral_arc_le_time {n : Type u_1} [Fintype n] [DecidableEq n] (Ω : ℝ) (steps : List (ℝ × ℝ × Matrix n n ℂ)) (hτ : ∀ s ∈ steps, 0 ≤ s.1) (hH : ∀ s ∈ steps, s.2.2.IsHermitian) (hΩ : ∀ s ∈ steps, ‖s.2.2 - ↑s.2.1 • 1‖ ≤ Ω / 2) (ω : ℂ) (G : Matrix n n ℂ) (hUG : (List.map (fun (s : ℝ × ℝ × Matrix n n ℂ) => NormedSpace.exp ((-↑s.1 * Complex.I) • s.2.2)) steps).prod = ω • G) {ι : Type u_2} (e : ι → EuclideanSpace ℂ n) (he : ∀ (j : ι), ‖e j‖ = 1) (φ : ι → ℝ) (hG : ∀ (j : ι), TwoQubit.act G (e j) = Complex.exp (↑(φ j) * Complex.I) • e j) : ∃ (β : ℝ), ∀ (j : ι), ∃ (m : ℤ), |φ j - β - 2 * Real.pi * ↑m| ≤ Ω / 2 * (List.map Prod.fst steps).sum

Spectral arc of a product of evolutions (finite-dimensional Nudel'man–Švarcman / Thompson / Miglioli, arXiv:2310.06331, Thm 4.4 / Cor 4.5). Let U = ∏ₖ exp (−i τₖ Hₖ) with τₖ ≥ 0, Hₖ Hermitian and ‖Hₖ − cₖ • 1‖ ≤ Ω / 2, and suppose U = ω • G (global phase ω). If G eⱼ = e^{i φⱼ} eⱼ for unit vectors eⱼ (any family), then there is a centre β such that every eigenphase satisfies |φⱼ − β − 2π mⱼ| ≤ (Ω / 2) · ∑ τₖ for some integer mⱼ: all eigenphases lie in an arc of length Ω ∑ τₖ modulo 2π. No restriction on the size of the eigenphase gaps (cf. gate_time_ge_eigenphase_gap, gaps ≤ π).

The gate exp (i π/4 (2 Z⊗I + I⊗Z)) of Nelson–Barnes

noncomputable def QSL.Gate.u4d : Matrix (Fin 4) (Fin 4) ℂ

The two-qubit gate diag (e^{3iπ/4}, e^{iπ/4}, e^{−iπ/4}, e^{−3iπ/4}) = exp (i π/4 (2 Z⊗I + I⊗Z)) (Nelson–Barnes, arXiv:2604.23031, Table I), with eigenphases 3π/4 − j π/2, j = 0, 1, 2, 3.

Equations

• QSL.Gate.u4d = Matrix.diagonal fun (j : Fin 4) => Complex.exp (↑(3 * Real.pi / 4 - ↑↑j * Real.pi / 2) * Complex.I)

theorem QSL.Gate.u4d_time_ge (Ω : ℝ) (steps : List (ℝ × ℝ × Matrix (Fin 4) (Fin 4) ℂ)) (hτ : ∀ s ∈ steps, 0 ≤ s.1) (hH : ∀ s ∈ steps, s.2.2.IsHermitian) (hΩ : ∀ s ∈ steps, ‖s.2.2 - ↑s.2.1 • 1‖ ≤ Ω / 2) (ω : ℂ) (hUG : (List.map (fun (s : ℝ × ℝ × Matrix (Fin 4) (Fin 4) ℂ) => NormedSpace.exp ((-↑s.1 * Complex.I) • s.2.2)) steps).prod = ω • u4d) : 3 * Real.pi / 2 ≤ Ω * (List.map Prod.fst steps).sum

U₄d needs time 3π / (2 Ω). Any ordered product ∏ₖ exp (−i τₖ Hₖ) (τₖ ≥ 0, Hₖ Hermitian on two qubits, ‖Hₖ − cₖ • 1‖ ≤ Ω / 2) equal to u4d up to a global phase has 3π / 2 ≤ Ω · ∑ τₖ: four eigenphases spaced by π/2 do not fit in an arc shorter than 3π/2 (spectral_arc_le_time). Nelson–Barnes, arXiv:2604.23031, Table I.