A lower bound on the duration of an entangling two-qubit gate

Two qubits, ℂ² ⊗ ℂ² with basis indexed by Fin 2 × Fin 2, evolve under a Hamiltonian L + H, where L = A ⊗ 1 + 1 ⊗ B is an arbitrary local (piecewise constant) control and H is a Hermitian interaction of operator norm at most J (ħ = 1). The Bell vector Φ = (e₀₀ + e₁₁)/√2 is at L2-distance at least √(2 − √2) from every product vector, since |⟨Φ, a ⊗ b⟩| ≤ 1/√2. Local unitaries preserve product vectors, so a gate that sends a product vector to Φ is at operator distance at least √(2 − √2) from every local unitary A ⊗ B. A Duhamel estimate ‖exp (X + Y) − exp X‖ ≤ ‖Y‖ for skew-Hermitian X, Y shows that each step exp (−i τ (L + H)) is within τ ‖H‖ of the local unitary exp (−i τ L), and telescoping over the steps gives √(2 − √2) ≤ J · ∑ τₖ: the total time ∑ τₖ is at least √(2 − √2) / J.

Matrices are over ℂ with the L2 operator norm (Matrix.Norms.L2Operator); vectors live in EuclideanSpace ℂ (Fin 2 × Fin 2).

Main results

• QSL.TwoQubit.norm_inner_bell_prodVec_le: ‖⟪Φ, a ⊗ b⟫‖ ≤ 1/√2 for unit a, b
• QSL.TwoQubit.sqrt_two_sub_sqrt_two_le_norm_bell_sub_prodVec: √(2 − √2) ≤ ‖Φ − a ⊗ b‖ for unit a, b
• QSL.TwoQubit.sqrt_two_sub_sqrt_two_le_norm_sub_kronecker: if G maps a unit product vector to Φ, then √(2 − √2) ≤ ‖G − A ⊗ₖ B‖ for all unitary A, B
• QSL.TwoQubit.norm_exp_add_sub_exp_le: ‖exp (X + Y) − exp X‖ ≤ ‖Y‖ for skew-Hermitian X, Y
• QSL.TwoQubit.entangling_time_lower_bound: a controlled evolution ∏ exp (−i τₖ (Lₖ + H)) with ‖H‖ ≤ J that sends a unit product vector to Φ satisfies √(2 − √2) ≤ J · ∑ τₖ

References

• C. Marín, The Clock That Never Ticks: a machine-checked path from the dilogarithm to quantum speed limits in Lean 4, Zenodo (2026), doi:10.5281/zenodo.20675271.

@[reducible, inline]

abbrev QSL.TwoQubit.Vec2 : Type

Qubit vectors.

Equations

• QSL.TwoQubit.Vec2 = EuclideanSpace ℂ (Fin 2)

@[reducible, inline]

abbrev QSL.TwoQubit.Vec4 : Type

Two-qubit vectors.

Equations

• QSL.TwoQubit.Vec4 = EuclideanSpace ℂ (Fin 2 × Fin 2)

@[reducible, inline]

abbrev QSL.TwoQubit.Mat2 : Type

Single-qubit operators.

Equations

• QSL.TwoQubit.Mat2 = Matrix (Fin 2) (Fin 2) ℂ

@[reducible, inline]

abbrev QSL.TwoQubit.Mat4 : Type

Two-qubit operators.

Equations

• QSL.TwoQubit.Mat4 = Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ

def QSL.TwoQubit.prodVec (a b : Vec2) : Vec4

The product vector (a ⊗ b) (i, j) = a i * b j.

Equations

• QSL.TwoQubit.prodVec a b = WithLp.toLp 2 fun (p : Fin 2 × Fin 2) => a.ofLp p.1 * b.ofLp p.2

noncomputable def QSL.TwoQubit.bell : Vec4

The Bell vector Φ = (e₀₀ + e₁₁)/√2.

Equations

• QSL.TwoQubit.bell = WithLp.toLp 2 fun (p : Fin 2 × Fin 2) => if p.1 = p.2 then ↑(√2)⁻¹ else 0

def QSL.TwoQubit.act {n : Type u_1} [Fintype n] (M : Matrix n n ℂ) (v : EuclideanSpace ℂ n) : EuclideanSpace ℂ n

Action of a matrix on a Euclidean vector.

Equations

• QSL.TwoQubit.act M v = WithLp.toLp 2 (M.mulVec v.ofLp)

theorem QSL.TwoQubit.norm_inner_bell_prodVec_le (a b : Vec2) (ha : ‖a‖ = 1) (hb : ‖b‖ = 1) : ‖inner ℂ bell (prodVec a b)‖ ≤ (√2)⁻¹

(1) Bell overlap: ‖⟪Φ, a ⊗ b⟫‖ ≤ 1/√2 for unit vectors a, b ∈ ℂ².

theorem QSL.TwoQubit.sqrt_two_sub_sqrt_two_le_norm_bell_sub_prodVec (a b : Vec2) (ha : ‖a‖ = 1) (hb : ‖b‖ = 1) : √(2 - √2) ≤ ‖bell - prodVec a b‖

(2) Distance: √(2 − √2) ≤ ‖Φ − a ⊗ b‖ for unit vectors a, b ∈ ℂ².

theorem QSL.TwoQubit.sqrt_two_sub_sqrt_two_le_norm_sub_kronecker (G : Mat4) (a b : Vec2) (ha : ‖a‖ = 1) (hb : ‖b‖ = 1) (hG : act G (prodVec a b) = bell) (A B : Mat2) (hA : A ∈ Matrix.unitaryGroup (Fin 2) ℂ) (hB : B ∈ Matrix.unitaryGroup (Fin 2) ℂ) : √(2 - √2) ≤ ‖G - Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A B‖

(3) Entangling gates are far from local gates: if G maps a unit product vector to Φ, then √(2 − √2) ≤ ‖G − A ⊗ₖ B‖ for all unitary 2 × 2 matrices A, B.

Exponentials of skew-Hermitian matrices and the Duhamel estimate

theorem QSL.TwoQubit.norm_exp_add_sub_exp_le {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] (X Y : Matrix n n ℂ) (hX : X.conjTranspose = -X) (hY : Y.conjTranspose = -Y) : ‖NormedSpace.exp (X + Y) - NormedSpace.exp X‖ ≤ ‖Y‖

(4) Duhamel step: for skew-Hermitian X, Y, ‖exp (X + Y) − exp X‖ ≤ ‖Y‖.

Local evolutions and the main theorem

theorem QSL.TwoQubit.entangling_time_lower_bound (H : Mat4) (hH : Matrix.IsHermitian H) (J : ℝ) (hJ : ‖H‖ ≤ J) (steps : List (ℝ × Mat2 × Mat2)) (hτ : ∀ s ∈ steps, 0 ≤ s.1) (hA : ∀ s ∈ steps, Matrix.IsHermitian s.2.1) (hB : ∀ s ∈ steps, Matrix.IsHermitian s.2.2) (a b : Vec2) (ha : ‖a‖ = 1) (hb : ‖b‖ = 1) (hU : act (List.map (fun (s : ℝ × Mat2 × Mat2) => NormedSpace.exp ((-↑s.1 * Complex.I) • (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) s.2.1 1 + Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 s.2.2 + H))) steps).prod (prodVec a b) = bell) : √(2 - √2) ≤ J * (List.map Prod.fst steps).sum

(5) Main theorem. Let H be a Hermitian interaction with ‖H‖ ≤ J and let U = ∏ₖ exp (−i τₖ (Aₖ ⊗ 1 + 1 ⊗ Bₖ + H)) (an ordered product over the list steps of triples (τₖ, Aₖ, Bₖ), τₖ ≥ 0, Aₖ, Bₖ Hermitian) be a controlled evolution with arbitrary local controls. If U maps a unit product vector a ⊗ b to the Bell vector Φ, then √(2 − √2) ≤ J · ∑ τₖ.