Blueprint

🗺️ Map of Certified Speed-Limit Diagnostics for Deployed Superconducting Quantum Processors

🏷️ Quantum speed limits · superconducting-qubit gate calibration
54 results ✅ 8 entirely in Lean ◐ 11 partly in Lean ✅ 2 in Isabelle 💻 36 checked by a program written proof only (a result can carry several tags)

Dependencies in the written proof: an arrow A → B means that this proof of B uses A. Every result rests on its written proof; the tags record what was checked besides, and each statement's “Evidence & scope” block says how far. The colour of a box is its strongest tag, in the order above; the tags in the box give the rest. Boxes with a thick border are the main results; click a box to read the statement.

cluster_0 Introduction cluster_1 Certified Bounds cluster_2 Data and Conventions cluster_3 Single-Qubit Gates cluster_4 Two-Qubit Gates cluster_5 Time Series 2021–2025 cluster_6 How Far the Model Allows cluster_7 Application: A Chip-to-Chip State Transfer cluster_8 What the Certificate Does and Does Not Guarantee cluster_9 Reproducibility cluster_10 Conclusion i:abstract Remark Abstract the abstract: 11.3× at full amplitude, ≈ 2× at the drive IBM uses, gates ≈ 10× faster than the median within each device’s full amplitude, 4.22× for two qubits, a CZ between 0.295 and 0.331 of the qubit-only time (version 3) i:claims Remark §I what the paper claims: five contributions (the fifth in version 2), and no new physics b:table Remark Table I Table I: the certified statements used in the paper (Lean 4, commit 42f307b) and their status in the literature ◐ part in Lean b:zz Theorem §II-A Zieliński–Zych: π^α ≤ 2M_α τ^α for every α > 0 ✅ Lean · Isabelle b:ml Theorem §II-A Margolus–Levitin: π ≤ 2⟨E⟩τ for a state that becomes orthogonal at τ ✅ Lean b:twolevel Theorem §II-A two-level drive: τ ≥ π/Ωₘax for every pulse shape; a fixed-axis π pulse has speed-limit ratio exactly 1 ◐ part in Lean b:mt Theorem §II-A Mandelstam–Tamm, L¹ form: 1 ≤ D₁τ ≤ ΔE·τ ✅ Lean b:ent Theorem §II-B entangling time in any local dimension: arccos λ ≤ J·Στₖ ✅ Lean b:bell Corollary §II-B a Bell vector needs J·Στₖ ≥ π/4, in any local dimension d ≥ 2 ✅ Lean b:tight Proposition §II-B the bound is attained: H = J·Z⊗X reaches a Bell vector in time π/(4J) ✅ Lean q:gap Observation §IV-A X gates last a median 11.30 times their two- level speed limit at full drive amplitude 💻 program b:twolevel->q:gap r:lower Proposition §VII-A a lower bound for any number of levels: T ≥ π/Ωₘax, and in the trace metric T ≥ 2 arcsin(1−e)/Ωₘax; for r ≤ 0.2 the times found are 6 % above it 💻 program b:twolevel->r:lower b:ent->b:bell b:chord Theorem §II-B the earlier chord-distance version: J·Στₖ ≥ √(2−√2) ≈ 0.7654 ✅ Lean r:cz Observation §VII-B CZ with the second transmon level: error 2·10⁻⁸ at T = 0.55/J with local controls ≤ 10J, i.e. 0.35 of the qubit-only time and 5 % above the construction π/(6J) ◐ part in Lean · 💻 program b:ent->r:cz r:czconstr Observation §VII-B explicit CZ construction: fast twirling of one transmon keeps (J/2)Q⊗Q, the code in the extreme eigenvectors of Q gives (3J/2)Z⊗Z and a CZ in π/(6J) = 0.5236/J; so π/(8J) ≤ T_* ≤ π/(6J), and with the refined bound (next nodes) 0.4511/J ≤ T_* ≤ π/(6J) ◐ part in Lean · 💻 program b:ent->r:czconstr r:czrefined Observation §VII-B a refined CZ bound: T_* ≥ 0.4511/J (a comparator- trajectory argument; the 97/32 lemma is certified in Lean), so 0.4511/J ≤ T_* ≤ π/(6J) = 0.5236/J and T_*(2·10⁻⁸) ≥ 0.4510/J ◐ part in Lean · 💻 program b:ent->r:czrefined r:asymptotic Observation §VII-B larger local dimension: the construction gives a CZ in π/(2Jλd²), the entangling-time theorem gives π/(4Jκd); the ratio 2κd/λd² is 2, 1.33, 1.27, 1.20, 1.09, 1.05 for d = 2, 3, 4, 5, 10, 20 and tends to 1 ◐ part in Lean · 💻 program b:ent->r:asymptotic r:heis Observation §VII-B Heisenberg coupling and ancillas: the smallest largest-Schmidt- coefficient is exactly cos(2T) up to the Bell time π/8 (an analytic witness) ◐ part in Lean · 💻 program b:ent->r:heis b:bell->b:tight b:cnot Corollary §II-B any CNOT, or gate locally equivalent to it (ECR), on the qubit subspace of two d-level systems needs J·T ≥ π/4 ◐ part in Lean · 💻 program b:approx Theorem §II-B robust bounds: a Bell vector to fidelity 1−ε needs J·Στₖ ≥ π/4 − arcsin √ε; a two-level transfer needs Ωₘax T ≥ 2 arccos √ε ✅ Lean b:bell->b:approx t:certified Observation §V-C against our certified constants the median ratio is 8.7 (chord) or 8.4 (sharp π/4), twice the literature one ◐ part in Lean · 💻 program b:bell->t:certified b:chord->t:certified t:controls Observation §V-C numerical controls of the certified bound: 0 violations in 20 000 and 3000 trials 💻 program b:chord->t:controls d:conv Observation §III-C the drive convention is c = 1: IBM’s calibrated π pulse rotates by 1.148 π with c = 1 (2.296 π with c = 2) 💻 program r:choi Observation §VII-B a gate bound by the Choi state: T_*(e) ≥ [π/4 − arccos(1−e)]/(2J), so 0.392599/J ≤ T_*(2·10⁻⁸) ≤ 0.55/J (sharpened to 0.4510/J in r:czrefined); exact Bell preparation is a different, easier task ◐ part in Lean · 💻 program b:approx->r:choi v:floor Observation §VIII certified floor: T ≥ π/(2√2 g) for the relay, from the any-dimension speed limit with ‖H‖ ≤ √2 g ◐ part in Lean b:approx->v:floor d:identity Observation §III-C the residual is explained: omegad·|amp|·Aᵣec = π on all 777 qubits to 1.2·10⁻⁷; the ratio of the two areas tends to 1/(1−e⁻²) = 1.15652 💻 program d:conv->d:identity d:derived Observation §III-C omegad is not an independent measurement: IBM derives it from the π-pulse calibration 💻 program d:conv->d:derived d:falsifier Observation §III-D the pre-registered falsifier fired on 254 qubits of three backends with placeholder-like values, which are excluded 💻 program d:conv->q:gap q:cap Observation §IV-C IBM’s design rule: the calibrated peak Rabi frequency is about 0.09 of the anharmonicity (0.0907, or 0.078 with the normalized peak) 💻 program d:conv->q:cap q:decomp Observation §IV-C what sets the duration: the gap factors into a pulse shape (≈ 2.16 = 1.87 × 1/(1−e⁻²)) and an amplitude reserve (≈ 5) d:identity->q:decomp q:hyp Observation §IV-B pre-registered rivals: H1 rejected at full amplitude (depends on the waveform reading at the drive used), H3 excluded, H2 without support 💻 program d:derived->q:hyp q:gap->q:decomp q:gap->q:hyp s:table Observation §VI single-qubit ratio frozen near 11 from 2021 to 2025; two-qubit ratio 2.78 → 4.26 💻 program q:gap->s:table r:law Observation §VII-A optimal control: shortest X time found ≈ max(π/Ωₘax, 1.1·2π/|δ|), a speed-limit branch and a leakage- dominated branch 💻 program q:gap->r:law c:summary Remark §XI conclusion: 11.3× at full amplitude and ≈ 2× at the drive used; X gates ≈ 10× faster than the median within the full amplitude (4.8 ns at rfull); 4.22× for two qubits; a CZ between the refined bound 0.4511/J and the construction π/(6J) q:gap->c:summary q:perqubit Observation §IV-C per-qubit durations under the cap would gain only ×1.09; cairo runs above the cap 💻 program r:ibm Observation §VII-A for IBM’s |δ| ≈ 2.07 rad/ns: the fastest pulse found takes ≈ 16 ns at its own cap (35.6 ns is ≈ 2.2 times that); at r = 1 the 4-level search finds 3.3 ns, but that value is truncation-dependent 💻 program q:decomp->r:ibm q:cap->q:perqubit t:pairs Observation §V-A 1758 coupled pairs in 43 backends: median jq = 0.01268 rad/ns, median gate 548 ns 💻 program t:gap Observation §V-B ECR/CX gates last a median 4.22 times the CNOT-class bound π/(2jq) 💻 program t:pairs->t:gap t:cr Observation §V-D cross resonance against its first-order formula: median θ/(π/2) = 1.109; Ω_CR/Δ ≈ 0.45 💻 program t:pairs->t:cr t:gap->t:certified t:gap->s:table t:gap->c:summary t:certified->r:cz r:cr Observation §VII-B cross resonance: the fastest CNOT found is ≈ 1.2 times slower at IBM’s drive fraction 0.45 than at 0.7 💻 program t:cr->r:cr s:duration Observation §VI the two-qubit ratio grew because gates got longer, not because the coupling changed 💻 program s:table->s:duration s:lesson Observation §VI a pooled effect (p = 0.0017) vanished under a stratified control (p = 0.90): consistent with confounding by epoch 💻 program s:error Observation §VI lengthening does not lower the error: Spearman +0.13 (p = 0.23); it falls in only 31 % of lengthened pairs 💻 program s:duration->s:error s:error->s:lesson r:law->r:ibm r:trunc Observation §VII-A truncation: the 4-level pulse at r = 1 degrades to 5.5–7.2·10⁻⁴ with 5 to 12 levels; a 6-level pulse at T = 7.0/|δ| (3.4 ns) reaches 4.0·10⁻⁶ there and 3.6·10⁻⁶ with 8 and 12 levels 💻 program r:rfull Observation §VII-A the full amplitude |D| = 1 is rfull = omegad/|δ|, median 0.351; at r = 0.351 an X of 4.8 ns exists (bound 4.3 ns): the median gate is 10–11 times the model minimum, a 35.6 ns Falcon gate 7.4–8.3 times 💻 program r:ibm->r:trunc r:ibm->c:summary r:trunc->r:rfull r:cz->c:summary r:czconstr->r:cz r:czv3 Observation §VII-B version 3: two copies give T_* ≥ π/(√46 J) = 0.4632/J; a closed excursion through |mm⟩, certified in interval arithmetic, gives T_* ≤ 0.520023/J; so the CZ lies between 0.295 and 0.331 of the qubit-only time 💻 program r:czconstr->r:asymptotic r:choi->r:cz r:choi->r:czrefined r:czrefined->r:czv3 v:link Remark §VIII the IBM chip-to-chip transfer: 80 cm coax, one standing mode, g/2π = 8–9 MHz, Tg = 256–312 ns, F = 98.86–99.29 % 💻 program v:gaps Remark Table VII Table VII: the IBM transfers last 5.8–7.9× the single-mode minimal time (4.1–5.6× sequential, 11.6–15.9× the certified floor); the 126 ns target would still be 2.9–3.2× 💻 program v:optimum Observation §VIII the single-mode minimal time is π/(√2 g) (Boscain–Chambrion–Charlot 2005); its lower half gT ≥ π/√2 is machine-checked in Isabelle ✅ Isabelle · 💻 program v:floor->v:optimum v:coherence Observation §VIII at the minimal time the coherence error of the optimal protocol is 0.13–0.26 % (master equation), 4–6× below the measured errors; IBM’s additive model gives less (0.09–0.17 %): exact for relaxation, not for dephasing; one protocol, not a floor 💻 program v:caveats Remark §VIII caveats: many cable modes (the bounds then hold with the collective norm G), g is the maximal coupling, IBM’s fidelity and error model, Markovian dephasing at the Ramsey rate v:gaps->v:coherence h:scope Remark §IX the certified objects are the inequalities, not the gaps; the bounds not in Lean and the truncation are listed x:repro Remark §X every number traces to a script of the companion package, linked from this blueprint 💻 program c:ack Remark §XI conflict of interest and the use of AI assistants

What the paper contributes

Two kinds of results, kept apart on this map. Certified inequalities (green, linked to Lean): the Margolus–Levitin bound, an $L^1$ form of Mandelstam–Tamm, the Zieliński–Zych family for every exponent $\alpha>0$, time-dependent two-level bounds, and an entangling-time bound $J\,T\ge\arccos\lambda$ in arbitrary local dimension (a Bell state needs $J\,T\ge\pi/4$, attained; robust versions with state infidelity $\varepsilon$). Diagnostics on deployed hardware (grey, with the program that computes each number): how far the calibrated gates of IBM superconducting processors are from those bounds, from public, version-pinned calibration snapshots.

  • Single-qubit $X$ gates last a median $11.30$ times their two-level speed limit $\pi/\Omega_{\max}$ (1646 qubits, 41 backends), a ratio frozen near $11$ from 2021 to 2025.
  • Two-qubit ECR/CX gates last a median $4.22$ times the known CNOT-class bound $\pi/(2j_q)$; the ratio grew from $2.78$ (2021) to $4.26$ (2025) because gates got longer, not because couplings got weaker.
  • Calibrated drives sit at fixed fractions of an energy splitting: $\Omega_{\rm peak}\approx0.09|\delta|$ (one qubit), $\Omega_{\rm CR}\approx0.45\Delta$ (two).
  • The drive-strength convention is fixed by IBM's calibrated $\pi$ pulses; the $\approx15\%$ residual is explained by the pulse normalization: $\texttt{omegad}\cdot|\mathrm{amp}|\cdot A_{\rm rec}=\pi$ on all 777 qubits to $1.2\cdot10^{-7}$, and the residual tends to $1/(1-e^{-2})=1.15652$.
  • At the drive IBM actually uses the $X$ gate is within about $2$ of the square-pulse limit (shape factor $1.87$, or $2.16$ with Qiskit's peak normalization); the $11.3$ is against full drive amplitude, which IBM does not use.
  • Optimal control on IBM's own transmon model finds feasible $X$ gates of $\approx16$ ns at IBM's amplitude cap and $4.8$ ns at its full amplitude (minimum at least $4.3$ ns): $7.4$–$8.3$ times faster than the archived $35.6$ ns within the same amplitude budget; $\approx3.4$ ns needs three times that amplitude (numerical witnesses, not physical floors; the 6-level pulse is converged to 12 levels). The fit $\max(\pi/\Omega_{\max},\,\sim1.1\cdot2\pi/|\delta|)$ is empirical, not a theorem; $T\ge\pi/\Omega_{\max}$ (and $2\arcsin(1-e)/\Omega_{\max}$ in the trace metric) holds for any number of levels.
  • With the second transmon level the minimal CZ time lies between $0.295$ and $0.331$ of the qubit-only time: $0.4632/J\le T_*\le0.5200/J$ (version~3: a two-copy bound and a certified protocol; before, $0.4511/J\le T_*\le\pi/(6J)$; the certified norm bound is $\pi/(8J)$); optimal control reaches error $2\cdot10^{-8}$ at $0.55/J$ ($0.35$), and for the same task $0.4510/J\le T_*(2\cdot10^{-8})\le0.55/J$. In larger local dimension the construction and the entangling-time theorem approach each other (ratio $\to1$, certified in Lean).

The paper claims no new physics: the speed limits are classical, the two-qubit constants are known for qubits, and the transmon model is IBM's. The entangling-time bound is, for qubits, a known corollary of Dür et al. and Vidal–Hammerer–Cirac, new only as a machine-checked, any-dimension assembly. This blueprint is built from a draft: the paper's own open items are shown where they matter.

🚀 Start here: Observation §IV-A: X gates last a median 11.30 times their two-level speed limit at full drive amplitude.

Main results:

  • Theorem §II-A: Zieliński–Zych: π^α ≤ 2M_α τ^α for every α > 0
  • Theorem §II-B: entangling time in any local dimension: arccos λ ≤ J·Στₖ
  • Corollary §II-B: a Bell vector needs J·Στₖ ≥ π/4, in any local dimension d ≥ 2
  • Observation §III-C: the drive convention is c = 1: IBM’s calibrated π pulse rotates by 1.148 π with c = 1 (2.296 π with c = 2)
  • Observation §IV-A: X gates last a median 11.30 times their two-level speed limit at full drive amplitude
  • Observation §V-B: ECR/CX gates last a median 4.22 times the CNOT-class bound π/(2jq)
  • Observation §VI: single-qubit ratio frozen near 11 from 2021 to 2025; two-qubit ratio 2.78 → 4.26
  • Observation §VII-A: optimal control: shortest X time found ≈ max(π/Ωₘax, 1.1·2π/|δ|), a speed-limit branch and a leakage-dominated branch
  • Observation §VII-B: CZ with the second transmon level: error 2·10⁻⁸ at T = 0.55/J with local controls ≤ 10J, i.e. 0.35 of the qubit-only time and 5 % above the construction π/(6J)

🧭 Fields: where the paper lives and what it connects

Tools taken from other branches

What the results serve

  • Gate design on superconducting processors ← how far calibrated gates are from the physical limit, and which fractions of the energy splittings the calibrations use — §IV-A, §V-B, §IV-C, §V-D
  • Reproducible hardware benchmarking ← version-pinned public calibration snapshots as a citable source, and a stratified control against confounding by epoch — §VI, §VI