The entangling time of a bounded interaction in any local dimension

Two quantum systems with finite index types ι and κ (arbitrary local dimensions, ancillas included) evolve under A ⊗ 1 + 1 ⊗ B + H, where the local part is an arbitrary piecewise constant control and H is a Hermitian interaction with ‖H‖ ≤ J (ħ = 1). We measure distances between unit vectors with the Fubini–Study angle arccos ‖⟪u, v⟫‖, which satisfies the triangle inequality and is invariant under unitaries. A Duhamel estimate, split into N equal pieces and letting N → ∞, shows that the angle between exp (X + Y) ψ and exp X ψ is at most ‖Y‖ for skew-Hermitian X, Y. Chaining over the steps of the control, the final state of an evolution started at a product vector lies within angle J · ∑ τₖ of a product vector. Hence, if every unit product vector has overlap at most λ with the target state, arccos λ ≤ J · ∑ τₖ. For the two-level Bell vector (e₀₀ + e₁₁)/√2 inside qudits of any dimension d ≥ 2, λ = 1/√2, so the total time is at least π / (4 J); this is exact (attained by J · Z ⊗ X for qubits).

This sharpens QSL.TwoQubit.entangling_time_lower_bound, whose chord bound is √(2 − √2).

Main results

• QSL.Qudit.fsAngle_le_fsAngle_add_fsAngle: triangle inequality for the Fubini–Study angle
• QSL.Qudit.fsAngle_act_act: invariance under a unitary matrix
• QSL.Qudit.fsAngle_exp_add_exp_le: fsAngle (exp (X + Y) ψ) (exp X ψ) ≤ ‖Y‖ for skew-Hermitian X, Y and unit ψ
• QSL.Qudit.arccos_le_entangling_time: arccos λ ≤ J · ∑ τₖ for any target whose overlap with unit product vectors is at most λ
• QSL.Qudit.pi_div_four_le_entangling_time, QSL.Qudit.pi_div_four_le_entangling_time_fin: preparing a two-level Bell vector from a product vector takes J · ∑ τₖ ≥ π / 4
• QSL.Qudit.entangling_time_tight: the bound is attained (H = J · Z ⊗ X, one step of length π / (4 J))

References

• W. Dür, G. Vidal, J. I. Cirac, N. Linden, S. Popescu, Entanglement capabilities of nonlocal Hamiltonians, Phys. Rev. Lett. 87 (2001) 137901.
• G. Vidal, K. Hammerer, J. I. Cirac, Interaction cost of nonlocal gates, Phys. Rev. Lett. 88 (2002) 237902.
• B. Basyildiz, C. Jameson, Z. Gong, Speed limits of two-qubit gates with qudits, arXiv:2312.09218.
• Ł. Rudnicki, Quantum speed limit helps interpret geometric measure of entanglement, Phys. Rev. A 104 (2021) 032417, arXiv:2107.11877.
• 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.

The Fubini–Study angle

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

The Fubini–Study angle arccos ‖⟪u, v⟫‖ between (unit) vectors.

Equations

• QSL.Qudit.fsAngle u v = Real.arccos ‖inner ℂ u v‖

theorem QSL.Qudit.fsAngle_nonneg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (u v : E) : 0 ≤ fsAngle u v

theorem QSL.Qudit.fsAngle_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {u : E} (hu : ‖u‖ = 1) : fsAngle u u = 0

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

(A) Triangle inequality for the Fubini–Study angle of unit vectors.

theorem QSL.Qudit.fsAngle_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) : fsAngle x y ≤ Real.arccos (1 - c ^ 2 / 2)

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

theorem QSL.Qudit.arccos_one_sub_le {c : ℝ} (hc0 : 0 ≤ c) (hc : c < 2) : Real.arccos (1 - c ^ 2 / 2) ≤ c / √(1 - c ^ 2 / 4)

arccos (1 − c²/2) = 2 arcsin (c/2) ≤ c / √(1 − c²/4) for 0 ≤ c < 2.

Unitary matrices acting on Euclidean vectors

theorem QSL.Qudit.act_mul {n : Type u_1} [Fintype n] (M N : Matrix n n ℂ) (v : EuclideanSpace ℂ n) : TwoQubit.act (M * N) v = TwoQubit.act M (TwoQubit.act N v)

theorem QSL.Qudit.act_one {n : Type u_1} [Fintype n] [DecidableEq n] (v : EuclideanSpace ℂ n) : TwoQubit.act 1 v = v

theorem QSL.Qudit.act_sub {n : Type u_1} [Fintype n] (M N : Matrix n n ℂ) (v : EuclideanSpace ℂ n) : TwoQubit.act (M - N) v = TwoQubit.act M v - TwoQubit.act N v

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

theorem QSL.Qudit.norm_act_of_mem {n : Type u_1} [Fintype n] [DecidableEq n] {U : Matrix n n ℂ} (hU : U ∈ Matrix.unitaryGroup n ℂ) (v : EuclideanSpace ℂ n) : ‖TwoQubit.act U v‖ = ‖v‖

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

(A') The Fubini–Study angle is invariant under a unitary applied to both vectors.

theorem QSL.Qudit.exp_mem_unitaryGroup {n : Type u_1} [Fintype n] [DecidableEq n] (Z : Matrix n n ℂ) (hZ : Z.conjTranspose = -Z) : NormedSpace.exp Z ∈ Matrix.unitaryGroup n ℂ

theorem QSL.Qudit.fsAngle_exp_add_exp_le {n : Type u_1} [Fintype n] [DecidableEq n] (X Y : Matrix n n ℂ) (hX : X.conjTranspose = -X) (hY : Y.conjTranspose = -Y) (ψ : EuclideanSpace ℂ n) (hψ : ‖ψ‖ = 1) : fsAngle (TwoQubit.act (NormedSpace.exp (X + Y)) ψ) (TwoQubit.act (NormedSpace.exp X) ψ) ≤ ‖Y‖

(B) Step bound: for skew-Hermitian X, Y and a unit vector ψ, the Fubini–Study angle between exp (X + Y) ψ and exp X ψ is at most ‖Y‖.

Bipartite systems with arbitrary local dimensions

def QSL.Qudit.prodVec {ι : Type u_1} {κ : Type u_2} (a : EuclideanSpace ℂ ι) (b : EuclideanSpace ℂ κ) : EuclideanSpace ℂ (ι × κ)

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

Equations

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

theorem QSL.Qudit.norm_prodVec {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (a : EuclideanSpace ℂ ι) (b : EuclideanSpace ℂ κ) : ‖prodVec a b‖ = ‖a‖ * ‖b‖

theorem QSL.Qudit.act_kronecker_prodVec {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (A : Matrix ι ι ℂ) (B : Matrix κ κ ℂ) (a : EuclideanSpace ℂ ι) (b : EuclideanSpace ℂ κ) : TwoQubit.act (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A B) (prodVec a b) = prodVec (TwoQubit.act A a) (TwoQubit.act B b)

theorem QSL.Qudit.exp_local {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (A : Matrix ι ι ℂ) (B : Matrix κ κ ℂ) : NormedSpace.exp (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A 1 + Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 B) = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (NormedSpace.exp A) (NormedSpace.exp B)

exp (A ⊗ 1 + 1 ⊗ B) = exp A ⊗ exp B.

theorem QSL.Qudit.arccos_le_entangling_time {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (H : Matrix (ι × κ) (ι × κ) ℂ) (hH : H.IsHermitian) (J : ℝ) (hJ : ‖H‖ ≤ J) (steps : List (ℝ × Matrix ι ι ℂ × Matrix κ κ ℂ)) (hτ : ∀ s ∈ steps, 0 ≤ s.1) (hA : ∀ s ∈ steps, s.2.1.IsHermitian) (hB : ∀ s ∈ steps, s.2.2.IsHermitian) (a : EuclideanSpace ℂ ι) (b : EuclideanSpace ℂ κ) (ha : ‖a‖ = 1) (hb : ‖b‖ = 1) (Φ : EuclideanSpace ℂ (ι × κ)) (hU : TwoQubit.act (List.map (fun (s : ℝ × Matrix ι ι ℂ × Matrix κ κ ℂ) => 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) = Φ) (lam : ℝ) (hlam : ∀ (x : EuclideanSpace ℂ ι) (y : EuclideanSpace ℂ κ), ‖x‖ = 1 → ‖y‖ = 1 → ‖inner ℂ Φ (prodVec x y)‖ ≤ lam) : Real.arccos lam ≤ J * (List.map Prod.fst steps).sum

(C) General entangling-time bound, any local dimensions. Let H be a Hermitian interaction with ‖H‖ ≤ J, and U = ∏ₖ exp (−i τₖ (Aₖ ⊗ 1 + 1 ⊗ Bₖ + H)) (ordered product over steps, τₖ ≥ 0, Aₖ, Bₖ Hermitian). If U maps the unit product vector a ⊗ b to Φ, and every unit product vector has overlap at most λ with Φ, then arccos λ ≤ J · ∑ τₖ.

noncomputable def QSL.Qudit.bellPair {ι : Type u_1} {κ : Type u_2} [DecidableEq ι] [DecidableEq κ] (i₀ i₁ : ι) (j₀ j₁ : κ) : EuclideanSpace ℂ (ι × κ)

The two-level Bell vector (e_{i₀ j₀} + e_{i₁ j₁}) / √2.

Equations

• QSL.Qudit.bellPair i₀ i₁ j₀ j₁ = ↑(√2)⁻¹ • (EuclideanSpace.single (i₀, j₀) 1 + EuclideanSpace.single (i₁, j₁) 1)

theorem QSL.Qudit.norm_inner_bellPair_prodVec_le {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] {i₀ i₁ : ι} {j₀ j₁ : κ} (hi : i₀ ≠ i₁) (hj : j₀ ≠ j₁) (a : EuclideanSpace ℂ ι) (b : EuclideanSpace ℂ κ) (ha : ‖a‖ = 1) (hb : ‖b‖ = 1) : ‖inner ℂ (bellPair i₀ i₁ j₀ j₁) (prodVec a b)‖ ≤ (√2)⁻¹

Overlap of the two-level Bell vector with unit product vectors: at most 1/√2.

theorem QSL.Qudit.arccos_inv_sqrt_two : Real.arccos (√2)⁻¹ = Real.pi / 4

theorem QSL.Qudit.pi_div_four_le_entangling_time {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (H : Matrix (ι × κ) (ι × κ) ℂ) (hH : H.IsHermitian) (J : ℝ) (hJ : ‖H‖ ≤ J) (steps : List (ℝ × Matrix ι ι ℂ × Matrix κ κ ℂ)) (hτ : ∀ s ∈ steps, 0 ≤ s.1) (hA : ∀ s ∈ steps, s.2.1.IsHermitian) (hB : ∀ s ∈ steps, s.2.2.IsHermitian) (a : EuclideanSpace ℂ ι) (b : EuclideanSpace ℂ κ) (ha : ‖a‖ = 1) (hb : ‖b‖ = 1) {i₀ i₁ : ι} {j₀ j₁ : κ} (hi : i₀ ≠ i₁) (hj : j₀ ≠ j₁) (hU : TwoQubit.act (List.map (fun (s : ℝ × Matrix ι ι ℂ × Matrix κ κ ℂ) => 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) = bellPair i₀ i₁ j₀ j₁) : Real.pi / 4 ≤ J * (List.map Prod.fst steps).sum

(D) Preparing a two-level Bell vector (e_{i₀ j₀} + e_{i₁ j₁}) / √2 from a unit product vector with a bounded interaction ‖H‖ ≤ J and arbitrary local controls takes J · ∑ τₖ ≥ π / 4, in any local dimensions.

theorem QSL.Qudit.pi_div_four_le_entangling_time_fin (d : ℕ) (hd : 2 ≤ d) (H : Matrix (Fin d × Fin d) (Fin d × Fin d) ℂ) (hH : H.IsHermitian) (J : ℝ) (hJ : ‖H‖ ≤ J) (steps : List (ℝ × Matrix (Fin d) (Fin d) ℂ × Matrix (Fin d) (Fin d) ℂ)) (hτ : ∀ s ∈ steps, 0 ≤ s.1) (hA : ∀ s ∈ steps, s.2.1.IsHermitian) (hB : ∀ s ∈ steps, s.2.2.IsHermitian) (a b : EuclideanSpace ℂ (Fin d)) (ha : ‖a‖ = 1) (hb : ‖b‖ = 1) (hU : TwoQubit.act (List.map (fun (s : ℝ × Matrix (Fin d) (Fin d) ℂ × Matrix (Fin d) (Fin d) ℂ) => 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) = bellPair ⟨0, ⋯⟩ ⟨1, ⋯⟩ ⟨0, ⋯⟩ ⟨1, ⋯⟩) : Real.pi / 4 ≤ J * (List.map Prod.fst steps).sum

(D, qudits) For two qudits of dimension d ≥ 2, preparing (e₀₀ + e₁₁)/√2 from a unit product vector takes J · ∑ τₖ ≥ π / 4.

Tightness: J · Z ⊗ X reaches the Bell vector at J · τ = π / 4

theorem QSL.Qudit.entangling_time_tight (J : ℝ) (hJ : 0 < J) : ∃ (H : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ) (steps : List (ℝ × Matrix (Fin 2) (Fin 2) ℂ × Matrix (Fin 2) (Fin 2) ℂ)) (a : EuclideanSpace ℂ (Fin 2)) (b : EuclideanSpace ℂ (Fin 2)), H.IsHermitian ∧ ‖H‖ ≤ J ∧ (∀ s ∈ steps, 0 ≤ s.1) ∧ (∀ s ∈ steps, s.2.1.IsHermitian) ∧ (∀ s ∈ steps, s.2.2.IsHermitian) ∧ ‖a‖ = 1 ∧ ‖b‖ = 1 ∧ TwoQubit.act (List.map (fun (s : ℝ × Matrix (Fin 2) (Fin 2) ℂ × Matrix (Fin 2) (Fin 2) ℂ) => 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) = bellPair 0 1 0 1 ∧ J * (List.map Prod.fst steps).sum = Real.pi / 4

(E) Tightness: for two qubits, H = J · Z ⊗ X and one step of length π / (4 J) with no local control map the unit product vector ((1, −i)/√2) ⊗ ((1, i)/√2) to the Bell vector, so the bound π / 4 ≤ J · ∑ τₖ of pi_div_four_le_entangling_time is attained.