Documentation

Formalizations.Physics.QuantumMechanics.SpeedLimit.GateEigenphases

Gate-time lower bound from the eigenphase gap #

A gate G is implemented, up to a global phase, by an ordered product U = ∏ₖ exp (−i τₖ Hₖ) of piecewise constant evolutions (τₖ ≥ 0, Hₖ Hermitian, ħ = 1) whose Hamiltonians have spectral half-width at most Ω / 2, i.e. ‖Hₖ − cₖ • 1‖ ≤ Ω / 2 for real cₖ. Then the total time is at least Δφ / Ω, where Δφ is the gap between two eigenphases of G on orthonormal eigenvectors.

Nelson and Barnes, How fast can a quantum gate be? Exact speed limits from geometry, arXiv:2604.23031 (2026), eq. (3), state the general bound T ≥ Δφ⋆ / Ω_max. This file gives an elementary proof via the shifted Mandelstam–Tamm bound (Duhamel estimate of QSL.Qudit.fsAngle_exp_add_exp_le plus the triangle inequality of the Fubini–Study angle), and only for gaps Δφ ≤ π. Nothing is claimed here about gaps larger than π; the full range is in Formalizations.Physics.QuantumMechanics.SpeedLimit.SpectralArc (sphere angle, spectral arc).

For the two-qubit controlled-Z gate diag (1, 1, 1, −1) the eigenphases 0 and π give T ≥ π / Ω, matching T⋆ (CZ) = π / Ω of Nelson–Barnes (Table I).

Main results #

References #

source
theorem QSL.Gate.fsAngle_le_time_halfWidth {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) :
Qudit.fsAngle (TwoQubit.act (List.map (fun (s : ℝ × ℝ × Matrix n n ℂ) => NormedSpace.exp ((-↑s.1 * Complex.I) • s.2.2)) steps).prod v) v ≤ Ω / 2 * (List.map Prod.fst steps).sum

Mandelstam–Tamm bound for a product of evolutions. If U = ∏ₖ exp (−i τₖ Hₖ) with τₖ ≥ 0, Hₖ Hermitian and ‖Hₖ − cₖ • 1‖ ≤ Ω / 2 for real cₖ, then every unit vector v satisfies fsAngle (U v) v ≤ (Ω / 2) · ∑ τₖ.

source
theorem QSL.Gate.gate_time_ge_eigenphase_gap {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) (ej ek : EuclideanSpace ℂ n) (hj : ‖ej‖ = 1) (hk : ‖ek‖ = 1) (hjk : inner ℂ ej ek = 0) (φj φk : ℝ) (hGj : TwoQubit.act G ej = Complex.exp (↑φj * Complex.I) • ej) (hGk : TwoQubit.act G ek = Complex.exp (↑φk * Complex.I) • ek) (hgap : |φj - φk| ≤ Real.pi) :
|φj - φk| ≤ Ω * (List.map Prod.fst steps).sum

Gate time from the eigenphase gap (gaps ≤ π only). Let U = ∏ₖ exp (−i τₖ Hₖ) with τₖ ≥ 0, Hₖ Hermitian, ‖Hₖ − cₖ • 1‖ ≤ Ω / 2, and suppose U = ω • G for a complex scalar ω (global phase). If G eⱼ = e^{i φⱼ} eⱼ and G eₖ = e^{i φₖ} eₖ for orthonormal eⱼ, eₖ with |φⱼ − φₖ| ≤ π, then |φⱼ − φₖ| ≤ Ω · ∑ τₖ. Cf. Nelson–Barnes, arXiv:2604.23031, eq. (3); this is an elementary proof for gaps ≤ π.

source
def QSL.Gate.cz :
Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ

The controlled-Z gate diag (1, 1, 1, −1) on two qubits.

Equations
Instances For
    source
    theorem QSL.Gate.cz_time_ge (Ω : ℝ) (steps : List (ℝ × ℝ × Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ)) (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 2 × Fin 2) (Fin 2 × Fin 2) ℂ) => NormedSpace.exp ((-↑s.1 * Complex.I) • s.2.2)) steps).prod = ω • cz) :
    Real.pi ≤ Ω * (List.map Prod.fst steps).sum

    CZ needs time π / Ω. Any ordered product ∏ₖ exp (−i τₖ Hₖ) (τₖ ≥ 0, Hₖ Hermitian on two qubits, ‖Hₖ − cₖ • 1‖ ≤ Ω / 2) equal to the controlled-Z gate up to a global phase has π ≤ Ω · ∑ τₖ. The eigenphases of CZ on e₀₀ and e₁₁ are 0 and π. This matches T⋆ (CZ) = π / Ω of Nelson–Barnes, arXiv:2604.23031, Table I.