The Zieliński–Zych speed limits and their limit α → 0

For a discrete spectral measure with populations p n ≥ 0, ∑ p n = 1, energies E n ≥ E₀ and fractional moment M_α = ∑ p n (E n − E₀)^α, if the autocorrelation ∑ p n e^{−i E n τ} vanishes at τ ≥ 0, then π^α ≤ 2 M_α τ^α, that is τ ≥ π / (2 M_α)^{1/α} (ħ = 1; Zieliński–Zych, Phys. Rev. A 74, 034301 (2006), Eq. (10)). The inequality x^α − π^α/2 + (π^α/2) cos x + α π^{α−1} sin x ≥ 0 behind it, stated without proof by Zieliński and Zych (who assert it for all α > 0), is proved here for every α > 0 (the case α = 1 is Margolus–Levitin): for 0 < α ≤ 1 by a harmonic-mean bound on t^α, for α ≥ 1 by Bernoulli plus the split tan(u) versus 2α/π. E₀ only needs to bound from below the energies that carry population. When the lowest populated level E 0 = E₀ carries p 0 and the others lie strictly above it, M_α → 1 − p 0 as α → 0⁺, so the bound tends to +∞ when 1/2 < p 0 < 1 and to 0 when p 0 < 1/2: in that limit the family reduces to the dominant-population criterion.

Main results

• QSL.zz_inequality: x^α − π^α/2 + (π^α/2) cos x + α π^{α−1} sin x ≥ 0 for 0 < α ≤ 1, x ≥ 0
• QSL.zielinski_zych: orthogonality at τ forces π^α ≤ 2 M_α τ^α (0 < α ≤ 1)
• QSL.zielinski_zych_time: the same as τ ≥ π / (2 M_α)^{1/α}
• QSL.zz_inequality_of_one_le: the same inequality for α ≥ 1, x ≥ 0
• QSL.zz_inequality_all: the same inequality for every α > 0, x ≥ 0
• QSL.zielinski_zych_all: π^α ≤ 2 M_α τ^α for every α > 0
• QSL.zielinski_zych_time_all: τ ≥ π / (2 M_α)^{1/α} for every α > 0
• QSL.tendsto_fractionalMoment: M_α → 1 − p 0 as α → 0⁺
• QSL.zz_bound_tendsto_atTop: the bound tends to +∞ as α → 0⁺ when 1/2 < p 0 < 1
• QSL.zz_bound_tendsto_zero: the bound tends to 0 as α → 0⁺ when p 0 < 1/2

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, thm:clock.

Elementary trigonometric bounds

Power bounds

The normalized inequality

theorem QSL.zz_inequality {α x : ℝ} (hα : 0 < α) (hα1 : α ≤ 1) (hx : 0 ≤ x) : 0 ≤ x ^ α - Real.pi ^ α / 2 + Real.pi ^ α / 2 * Real.cos x + α * Real.pi ^ (α - 1) * Real.sin x

The Zieliński–Zych inequality (their Eq. (9)): for 0 < α ≤ 1 and x ≥ 0, x^α - π^α/2 + (π^α/2) cos x + α π^{α-1} sin x ≥ 0, with equality at x = 0 and x = π.

The case α ≥ 1

Normalising t = x / π, the inequality reads F(t) = t^α - sin²(π t / 2) + (α/π) sin (π t) ≥ 0. For t ≥ 1 Bernoulli gives t^α ≥ 1 + α (t - 1) and u - sin u ≥ 0. For 0 ≤ t ≤ 1 put u = π (1 - t) / 2 ∈ [0, π/2]. If π cos u ≤ 2 α sin u, dropping t^α leaves cos u (2 α sin u - π cos u) / π ≥ 0. Otherwise Bernoulli leaves (π sin² u - 2 α (u - sin u cos u)) / π, which is ≥ 0 because 2 α sin u ≤ π cos u and u cos u ≤ sin u (u ≤ tan u).

theorem QSL.zz_inequality_of_one_le {α x : ℝ} (hα : 1 ≤ α) (hx : 0 ≤ x) : 0 ≤ x ^ α - Real.pi ^ α / 2 + Real.pi ^ α / 2 * Real.cos x + α * Real.pi ^ (α - 1) * Real.sin x

The Zieliński–Zych inequality for α ≥ 1 (asserted without proof in their paper).

theorem QSL.zz_inequality_all {α x : ℝ} (hα : 0 < α) (hx : 0 ≤ x) : 0 ≤ x ^ α - Real.pi ^ α / 2 + Real.pi ^ α / 2 * Real.cos x + α * Real.pi ^ (α - 1) * Real.sin x

The Zieliński–Zych inequality for every α > 0.

theorem QSL.zielinski_zych_all {p E : ℕ → ℝ} {E₀ α M τ : ℝ} (hα : 0 < α) (hp : ∀ (n : ℕ), 0 ≤ p n) (hE : ∀ (n : ℕ), E₀ ≤ E n) (hτ : 0 ≤ τ) (hsum : HasSum p 1) (hM : HasSum (fun (n : ℕ) => p n * (E n - E₀) ^ α) M) (hRe : HasSum (fun (n : ℕ) => p n * Real.cos (E n * τ)) 0) (hIm : HasSum (fun (n : ℕ) => p n * Real.sin (E n * τ)) 0) : Real.pi ^ α ≤ 2 * M * τ ^ α

The Zieliński–Zych speed limit for every α > 0 (their Eq. (10), ℏ = 1).

theorem QSL.zielinski_zych_time_all {p E : ℕ → ℝ} {E₀ α M τ : ℝ} (hα : 0 < α) (hp : ∀ (n : ℕ), 0 ≤ p n) (hE : ∀ (n : ℕ), E₀ ≤ E n) (hτ : 0 ≤ τ) (hsum : HasSum p 1) (hM : HasSum (fun (n : ℕ) => p n * (E n - E₀) ^ α) M) (hRe : HasSum (fun (n : ℕ) => p n * Real.cos (E n * τ)) 0) (hIm : HasSum (fun (n : ℕ) => p n * Real.sin (E n * τ)) 0) : Real.pi / (2 * M) ^ (1 / α) ≤ τ

The same bound as a lower bound on the time, for every α > 0.

theorem QSL.zielinski_zych {p E : ℕ → ℝ} {E₀ α M τ : ℝ} (hα : 0 < α) (hα1 : α ≤ 1) (hp : ∀ (n : ℕ), 0 ≤ p n) (hE : ∀ (n : ℕ), E₀ ≤ E n) (hτ : 0 ≤ τ) (hsum : HasSum p 1) (hM : HasSum (fun (n : ℕ) => p n * (E n - E₀) ^ α) M) (hRe : HasSum (fun (n : ℕ) => p n * Real.cos (E n * τ)) 0) (hIm : HasSum (fun (n : ℕ) => p n * Real.sin (E n * τ)) 0) : Real.pi ^ α ≤ 2 * M * τ ^ α

The Zieliński–Zych speed limit (their Eq. (10), ℏ = 1): if the autocorrelation of a normalized population distribution with energies E n ≥ E₀ vanishes at τ ≥ 0, then π^α ≤ 2 M_α τ^α with M_α = ∑ p n (E n - E₀)^α.

theorem QSL.zielinski_zych_time {p E : ℕ → ℝ} {E₀ α M τ : ℝ} (hα : 0 < α) (hα1 : α ≤ 1) (hp : ∀ (n : ℕ), 0 ≤ p n) (hE : ∀ (n : ℕ), E₀ ≤ E n) (hτ : 0 ≤ τ) (hsum : HasSum p 1) (hM : HasSum (fun (n : ℕ) => p n * (E n - E₀) ^ α) M) (hRe : HasSum (fun (n : ℕ) => p n * Real.cos (E n * τ)) 0) (hIm : HasSum (fun (n : ℕ) => p n * Real.sin (E n * τ)) 0) : Real.pi / (2 * M) ^ (1 / α) ≤ τ

The same bound as a lower bound on the time: π / (2 M_α)^{1/α} ≤ τ.

theorem QSL.tendsto_fractionalMoment {p E : ℕ → ℝ} {E₀ α₀ : ℝ} (hp : ∀ (n : ℕ), 0 ≤ p n) (hsum : HasSum p 1) (h0 : E 0 = E₀) (hE : ∀ (n : ℕ), n ≠ 0 → E₀ < E n) (hα₀ : 0 < α₀) (hmom : Summable fun (n : ℕ) => p n * (E n - E₀) ^ α₀) : Filter.Tendsto (fun (α : ℝ) => ∑' (n : ℕ), p n * (E n - E₀) ^ α) (nhdsWithin 0 (Set.Ioi 0)) (nhds (1 - p 0))

The fractional moments tend to 1 - p 0. If the level 0 is the lowest populated one (E 0 = E₀ and E n > E₀ for n ≠ 0) and some moment of order α₀ > 0 is finite, then ∑ p n (E n - E₀)^α → 1 - p 0 as α → 0⁺.

theorem QSL.zz_bound_tendsto_atTop {p E : ℕ → ℝ} {E₀ α₀ : ℝ} (hp : ∀ (n : ℕ), 0 ≤ p n) (hsum : HasSum p 1) (h0 : E 0 = E₀) (hE : ∀ (n : ℕ), n ≠ 0 → E₀ < E n) (hα₀ : 0 < α₀) (hmom : Summable fun (n : ℕ) => p n * (E n - E₀) ^ α₀) (hhalf : 1 / 2 < p 0) (hone : p 0 < 1) : Filter.Tendsto (fun (α : ℝ) => Real.pi / (2 * ∑' (n : ℕ), p n * (E n - E₀) ^ α) ^ (1 / α)) (nhdsWithin 0 (Set.Ioi 0)) Filter.atTop

A dominant lowest level makes the Zieliński–Zych bound diverge: if 1/2 < p 0 < 1, then π / (2 M_α)^{1/α} → +∞ as α → 0⁺, so the family certifies that the state never becomes orthogonal.

theorem QSL.zz_bound_tendsto_zero {p E : ℕ → ℝ} {E₀ α₀ : ℝ} (hp : ∀ (n : ℕ), 0 ≤ p n) (hsum : HasSum p 1) (h0 : E 0 = E₀) (hE : ∀ (n : ℕ), n ≠ 0 → E₀ < E n) (hα₀ : 0 < α₀) (hmom : Summable fun (n : ℕ) => p n * (E n - E₀) ^ α₀) (hhalf : p 0 < 1 / 2) : Filter.Tendsto (fun (α : ℝ) => Real.pi / (2 * ∑' (n : ℕ), p n * (E n - E₀) ^ α) ^ (1 / α)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Without a dominant lowest level the bound collapses: if p 0 < 1/2, then π / (2 M_α)^{1/α} → 0 as α → 0⁺.