- Boxes
- definitions
- Ellipses
- theorems and lemmas
- Blue border
- the statement of this result is ready to be formalized; all prerequisites are done
- Orange border
- the statement of this result is not ready to be formalized; the blueprint needs more work
- Blue background
- the proof of this result is ready to be formalized; all prerequisites are done
- Green border
- the statement of this result is formalized
- Green background
- the proof of this result is formalized
- Dark green background
- the proof of this result and all its ancestors are formalized
- Dark green border
- this is in Mathlib
If the evolution maps a product vector to a state whose overlap with the Bell vector satisfies \(|\langle \mathrm{Bell},\Phi \rangle |^2\ge 1-\varepsilon \), then \(J\sum _k\tau _k\ge \pi /4-\arcsin \sqrt\varepsilon \). For a two-level transfer with infidelity at most \(\varepsilon \), \(\Omega _{\max }T\ge 2\arccos \sqrt\varepsilon \).
CNOT maps \(|{+}\rangle |0\rangle \) to the Bell state, so any implementation of CNOT on the qubit subspace of two \(d\)-level systems needs \(J\, T\ge \pi /4\), with \(J\) the norm of the interaction on the full \(d\)-level space. The same holds for every gate only locally equivalent to CNOT, such as IBM’s echoed cross-resonance (ECR): such a gate maps some product vector to \((P\otimes Q)\) applied to a Bell vector, local unitaries do not change the overlap with product vectors, and so \(J\, T\ge \pi /4\).
Two systems with finite index types (arbitrary local dimensions, ancillas included) evolve under \(\prod _k\exp [-i\tau _k(A_k\otimes 1+1\otimes B_k+H)]\), with \(A_k,B_k\) Hermitian and unbounded (piecewise-constant local control), \(\tau _k\ge 0\), and a constant Hermitian interaction \(H\) with \(\| H\| \le J\) (operator norm). If the evolution maps a unit product vector to \(\Phi \), and every unit product vector has overlap at most \(\lambda \) with \(\Phi \), then \(\arccos \lambda \le J\sum _k\tau _k\).
If \(S(\tau )=0\) at \(\tau \ge 0\), then \(1\le D_1\tau \) with \(D_1=\sum _n p_n|E_n-\bar E|\); and \(1\le \Delta E\, \tau \). The full MT constant \(\tau \ge \pi /(2\Delta E)\) is not proved in the development.
Certified statements used in this paper (Lean 4, commit 42f307b; theorem names with prefix QSL.) and their status in the literature.
margolus_levitin: \(\pi \le 2\langle E\rangle \tau \). Status: classical (Margolus–Levitin).
mandelstam_tamm_L1, _weak: \(1\le D_1\tau \le \Delta E\, \tau \). Status: weak form of Mandelstam–Tamm.
zielinski_zych_all: \(\pi ^\alpha \le 2M_\alpha \tau ^\alpha \), all \(\alpha {\gt}0\). Status: stated in Zieliński–Zych; key inequality unproved there.
Qudit.arccos_le_entangling_time: \(\arccos \lambda \le J\sum \tau _k\). Status: corollary of Basyildiz–Jameson–Gong and Rudnicki.
Qudit.pi_div_four_le_entangling_time_fin: Bell: \(J\sum \tau _k\ge \pi /4\), any \(d\). Status: \(d=2\): Dür et al., Vidal–Hammerer–Cirac.
Qudit.entangling_time_tight: attained by \(J\, Z\otimes X\). Status: \(d=2\): Dür et al., Vidal–Hammerer–Cirac.
Qudit.pi_div_four_le_entangling_time_local, _shift_local: same for \((P\otimes Q)\, \)Bell (ECR). Status: corollary.
TwoQubit.entangling_time_lower_bound: chord form, constant \(\sqrt{2-\sqrt2}\). Status: weaker earlier version.
Qudit.arccos_le_entangling_time_shift: \(\| H\| \to \| H-c\mathbb 1\| \). Status: corollary; \(d=2\): Dür et al.
Qudit.pi_div_eight_le_heisenberg_time: Heisenberg Bell: \(T\ge \pi /8\). Status: \(d=2\), no ancilla: Dür et al.
Gate.fsAngle_le_time_halfWidth: angle \(\le (\Omega _{\max }/2)\, T\), piecewise \(H(t)\). Status: standard (shifted MT).
FixedAxis.mandelstam_tamm_integral_eq_solution: \(\int \Delta E=\arccos |\langle \psi _0|\psi _T\rangle |\), fixed axis. Status: equality case of Mandelstam–Tamm.
Qudit.pi_div_four_sub_le_entangling_time_approx: Bell to fidelity \(1-\varepsilon \): \(J\sum \tau _k\ge \pi /4-\arcsin \sqrt\varepsilon \). Status: robust corollary; formalized here.
Gate.two_arccos_sqrt_le_time_approx: transfer to fidelity \(1-\varepsilon \): \(\Omega _{\max }T\ge 2\arccos \sqrt\varepsilon \). Status: two-level; tight.
Exchange.exchange_norm_ge, _le, ratio_tendsto_one: \(\lambda _d^2/2\le \kappa _d\le 2(d-1)\); \(2\kappa _d/\lambda _d^2\to 1\). Status: not found in the sources read.
Exchange.refined_cz_lemma: \(\tfrac 14\mathrm{Tr}[(P_A\otimes P_B)H_c^2]\le \tfrac {97}{32}J^2\), rank-2 codes, \(d=3\). Status: lemma of the refined CZ bound.
- QSL.margolus_levitin
- QSL.mandelstam_tamm_L1
- QSL.mandelstam_tamm_weak
- QSL.zielinski_zych_all
- QSL.Qudit.arccos_le_entangling_time
- QSL.Qudit.pi_div_four_le_entangling_time_fin
- QSL.Qudit.entangling_time_tight
- QSL.Qudit.pi_div_four_le_entangling_time_local
- QSL.Qudit.pi_div_four_le_entangling_time_shift_local
- QSL.TwoQubit.entangling_time_lower_bound
- QSL.Qudit.arccos_le_entangling_time_shift
- QSL.Qudit.pi_div_eight_le_heisenberg_time
- QSL.Gate.fsAngle_le_time_halfWidth
- QSL.FixedAxis.mandelstam_tamm_integral_eq_solution
- QSL.Qudit.pi_div_four_sub_le_entangling_time_approx
- QSL.Gate.two_arccos_sqrt_le_time_approx
- QSL.Exchange.exchange_norm_ge
- QSL.Exchange.exchange_norm_le
- QSL.Exchange.ratio_tendsto_one
- QSL.Exchange.refined_cz_lemma
For a two-level system driven at constant Rabi frequency \(\Omega \), ML gives \(\tau \ge \pi /\Omega \) for \(|0\rangle \to |1\rangle \), saturated by a square \(\pi \) pulse. For a time-dependent drive two further statements are certified. (i) Any piecewise-constant evolution whose Hamiltonians satisfy \(\| H_k-c_k\mathbb 1\| \le \Omega _{\max }/2\) for some real \(c_k\) moves any state by a Fubini–Study angle at most \((\Omega _{\max }/2)\, T\); hence \(|0\rangle \to |1\rangle \) needs \(T\ge \pi /\Omega _{\max }\) for every pulse shape. (ii) For a fixed-axis drive \(H(t)=f(t)\, \sigma _x/2\) with \(f\ge 0\) and \(\int f\le \pi \), starting from \(|0\rangle \), the generalized MT bound \(\int \Delta E\, dt\ge \arccos |\langle \psi _0|\psi _T\rangle |\) holds with equality: every fixed-axis \(\pi \) pulse has speed-limit ratio exactly \(1\), whatever its shape. It does not extend to DRAG pulses.
If \(S(\tau )=0\) at \(\tau \ge 0\), with \(E_n\ge E_0\) on populated levels and \(M_\alpha =\sum _n p_n(E_n-E_0)^\alpha \), then \(\pi ^\alpha \le 2M_\alpha \tau ^\alpha \) for every \(\alpha {\gt}0\). The auxiliary inequality \(x^\alpha -\pi ^\alpha /2+(\pi ^\alpha /2)\cos x+\alpha \pi ^{\alpha -1}\sin x\ge 0\) (\(x\ge 0\)) is stated without proof in the original paper for all \(\alpha {\gt}0\); Lean proves it for \(0{\lt}\alpha \le 1\) and for \(\alpha \ge 1\).
The author declares no conflict of interest. This work received no funding. Use of AI tools. This work was carried out with an AI assistant. The author checked all statements, proofs and computations and takes full responsibility for the content.
On public calibration snapshots of pre-Heron IBM processors (mainly Falcon and Eagle), single-qubit gates run at a median \(11.3\times \) their two-level speed limit at full drive amplitude, a ratio within about \(5\% \) of \(11.3\) in every year from 2021 to 2025. That denominator is an amplitude IBM does not use: it runs the drive at about a tenth of the anharmonicity, and at that drive its pulses are about \(2\) times the square-pulse limit (the shape factor \(1.87\), or \(2.16\) with Qiskit’s peak normalization) and can be shortened by at most \(2.18\) (nominal peak) or \(1.89\) (edge-subtracted peak) at the same peak drive; the remaining \(\approx 5\) is amplitude headroom, a design choice. Optimal control on IBM’s model finds \(\approx 16\) ns \(X\) gates at IBM’s own amplitude cap and \(4.8\) ns at its full amplitude (where the minimum is at least \(4.3\) ns): within the same amplitude budget the model admits gates about \(10\) times faster than the median gate (\(7.4\)–\(8.3\) times for a \(35.6\) ns Falcon gate); \(\approx 3.4\) ns needs three times that amplitude. These are feasible times in an idealized model, not physical floors. Two-qubit gates run at a median \(4.22\times \) the known qubit-subspace CNOT-class bound \(\pi /(2j_q)\); in the snapshots that ratio rose from \(2.78\) to \(4.26\) between 2021 and 2025 as gates got longer, not monotonically and coinciding with the change from Falcon CX to Eagle ECR, while the archived couplings did not change. The current Heron generation (CZ \(\approx 68\)–\(70\) ns) is not covered. The inequalities of Table I are machine-checked, including an any-dimension entangling-time bound that is new only as a certified assembly of known pieces. On the model, optimal control finds a cross-resonance CNOT \(\approx 1.2\) times faster at drive fraction \(0.7\) than at IBM’s \(0.45\), and, with the second transmon level, a CZ (error \(2\cdot 10^{-8}\)) in \(0.35\) of the qubit-only exchange time with local controls of at most \(10J\); both are feasible times found, not proven minima. The open questions are the true minimum between the two-copy bound \(0.4632/J\) and the certified protocol \(0.5200/J\) (version 3) (in \(d\)-level transmons the gap between the entangling bound and the construction closes as \(d\to \infty \), a limit certified in Lean), and a certified bound that joins the speed-limit and leakage branches of Eq. (1), for which we have no result. The same diagnostic applied to IBM’s chip-to-chip state transfer (version 2) places it at \(5.8\)–\(7.9\) times the single-mode minimal time \(\pi /(\sqrt2\, g)\), whose lower bound is machine-checked in Isabelle, with a coherence error at that time four to six times below the measured errors; this is the error of one protocol, not a floor.
The factor \(c\) is not documented in the snapshots. We fixed it before computing any gap, with the pre-specified rival H3 (“a different convention, factor \(2\) or \(2\pi \)”). The independent datum is the calibrated \(X\) pulse itself: its rotation angle must be \(\pi \). Across the 32 backends with pulse definitions, \(\texttt{omegad}\cdot |\mathrm{amp}|\cdot \mathrm{area}=1.148\, \pi \) with \(c=1\) and \(2.296\, \pi \) with \(c=2\) (median, with a simple discretization of the area). We adopt \(c=1\): the conventions with a factor \(2\) or \(2\pi \) are excluded. The residual \(\approx 1.15\) has an exact explanation in the pulse normalization (next node).
For equal \(\sigma \), the product \(\texttt{omegad}\cdot \mathrm{amp}\) is identical to 9 digits across 27 backends. Hence omegad is not an independent measurement; IBM derives it from the \(\pi \)-pulse calibration. Any correlation between gate duration and omegad is therefore partly circular.
The pre-registered falsifier was a ratio \(\tau _X/\tau _{\rm QSL}{\lt}1\) on any qubit, impossible for an exact \(X\) under a correct convention (an approximate gate with trace error \(e\) allows down to \((2/\pi )\arcsin (1-e)\), i.e. \(0.991\) for \(e=10^{-4}\)). It fired: 254 qubits came out faster than their own limit. They belong to the snapshots of brussels, prague and strasbourg, whose sample time \(dt\ge 1\) ns differs from that of every other snapshot (\(0.22\) ns) and suggests placeholder values (we have no documentation of their provenance); these backends are excluded, as are qubits reporting zero anharmonicity; the exclusion was decided after the falsifier fired, and we report it as such. Controls: a hand computation on armonk reproduces the script (ratio \(2.631\)), and changing the unit of omegad moves the median by exactly \(2\pi \). One time-series snapshot (toronto, 2021-03-15, median two-qubit duration 6315 ns, ratio \(\sim 40\)) is an outlier, probably a degraded calibration; it is kept in the time-series table, and removing it changes the 2021 two-qubit median from \(2.78\) to \(2.74\) (toronto_sensibilidad.py).
The residual \(\approx 1.15\) has an exact explanation in the pulse normalization. With \(g(x)=\exp [-(x-N/2)^2/(2\sigma ^2)]\), \(N=4\sigma \) and \(S=\sum _{n=0}^{N-1}g(n+\tfrac 12)\), let \(A_{\rm rec}=dt\, [S-N\, g(-\tfrac 12)]\) be the area of the sampled Gaussian with the edge value subtracted but without renormalizing the peak, and \(A_Q=dt\, [S-N\, g(-1)]/[1-g(-1)]\) the area of Qiskit’s lifted Gaussian. Then \(\texttt{omegad}\cdot |\mathrm{amp}|\cdot A_{\rm rec}=\pi \) on all 777 qubits with pulse definitions, to \(1.2\cdot 10^{-7}\); the residual is \(A_Q/A_{\rm rec}\), which tends to \(1/(1-e^{-2})=1.15652\) and reproduces, without fitting, both the width dependence of a simple discretization (\(1.1428\), \(1.1482\), \(1.1523\) for \(\sigma =24,40,80\)) and the values \(1.1552\)–\(1.1565\) of Qiskit’s convention. The check covers all qubits. So omegad is consistent with a drive whose peak is \((1-e^{-2})|\mathrm{amp}|\) in units of omegad; under Qiskit’s normalization the model would over-rotate by \(1.1565\). The snapshots do not say which waveform reaches the qubit. The full-amplitude ratio below uses omegad only and does not depend on this; the peak-drive figures do, and we give both readings.
The certified objects are the inequalities, not the gaps. The theorems of Table I are machine-checked for all inputs satisfying their hypotheses. Each reported gap is a computation on vendor data; its trust rests on the controls of Section III, not on a proof. The model is IBM’s, not a measurement. Every speed limit is evaluated in IBM’s Duffing model with the RWA. If the model misdescribes a device, the gap inherits the error. omegad is derived. It comes from the \(\pi \)-pulse calibration, and a factor \(1/(1-e^{-2})\) separates the area with which omegad was derived from Qiskit’s normalized pulse; which of the two waveforms reaches the qubit is not in the snapshots. The single-qubit gaps carry this uncertainty, and duration–omegad correlations are partly circular. Hypotheses of the two-qubit theorem. The Lean theorem assumes a constant interaction of bounded norm and piecewise-constant local controls, with a product initial state. Applying it to IBM gates assumes that the drives act locally and that the static coupling is the only interaction (no classical crosstalk). The single-qubit time-dependent bound and the ECR corollary are stated in Lean for piecewise-constant controls; a continuous pulse is covered only as a limit of such controls, which is not formalized. The norm \(\| H_{\rm int}\| =j_q\) holds only in the qubit subspace, and \(j_q\) itself is a model value repeated across dates. Bounds that are not in Lean. The literature gate bound \(\pi /(2j_q)\) behind the headline \(4.22\), its application to real durations (our inference), the multilevel single-qubit bound \(T\ge \pi /\Omega _{\max }\) and its trace-metric version (proved in the text), the instantiation with references, the time argument of the refined CZ bound \(0.4511/J\) (its \(97/32\) lemma is in Lean) and the CZ construction are not formalized (Lean certifies \(\pi /(8J)\)). Truncation. The single-qubit times found with 4 levels at \(r\ge 0.8\) are not converged in the number of levels; the converged fastest gate, \(\approx 3.4\) ns, comes from a 6-level search checked up to 12 levels. Effective cross-resonance models. The CR check uses effective Hamiltonians (first order, third order, and a static numerical block diagonalization); none is a time-dependent simulation of the calibrated pulse sequence with echoes and cancellation tones. Coarse optimal control. The optimal-control tables come from coarse grids (time steps, 8–10 piecewise-constant segments, finitely many random starts), without noise; the times reported are feasible times found, i.e. upper bounds on the minimum, and a time at which no gate was found proves nothing. Snapshots, not live data; no hardware validation. All data are dated snapshots. We have run nothing on hardware: IBM has been withdrawing pulse-level access, so the feasible times found in Section VII are model predictions. Black-box timing on live hardware is nevertheless feasible: gate-time amplification, which reads gate durations from job wall-time, could validate the snapshot durations used here. We have not done so.
How far are deployed quantum gates from the fastest evolution quantum mechanics allows? We answer for pre-Heron IBM processors, mainly Falcon and Eagle, using public, version-pinned calibration snapshots and inequalities whose proofs are machine-checked in Lean 4. Heron snapshots lack a Hamiltonian. For single-qubit gates, with the drive-strength convention fixed by IBM’s calibrated \(\pi \) pulses, the \(X\) gate lasts a median \(11.3\) times the two-level speed limit at full drive amplitude (1646 qubits, 41 backends). Most of this gap is a design choice: IBM drives at about a tenth of the anharmonicity, and at that drive its pulses are about \(2\) times the square-pulse limit. Within each device’s full amplitude, optimal control on IBM’s model gives gates about \(10\) times faster than the median. For two-qubit gates (1758 coupled pairs, 43 backends), the known qubit-subspace minimal time of controlled-NOT-class gates under exchange coupling (literature) gives a median ratio \(4.22\); across the snapshots it rose, not monotonically, from \(2.78\) (2021) to \(4.26\) (2025) as gates got longer, coinciding with the change from Falcon to Eagle. With the second level and fast arbitrary local control, the minimal time of a controlled-Z gate with ideal local control lies between \(0.295\) and \(0.331\) of the qubit-only exchange time (a two-copy bound and a certified explicit protocol, version 3); bounded local control reaches \(0.35\). We also formalize an entangling-time bound in arbitrary local dimension, known for qubits and new only as a machine-checked assembly. Applied to IBM’s chip-to-chip state transfer (version 2), the same diagnostic places the transfers at \(5.8\)–\(7.9\) times the single-mode minimal time, whose lower bound is machine-checked in Isabelle, and the coherence error of the fastest protocol four to six times below the measured errors. The contribution is a reproducible diagnostic built on the machine-checked inequalities, with explicit guarantees.
This paper contributes five things. (1) Certified bounds. The inequalities listed in Table I are proved in Lean 4 in the public development (the two-qubit gate bound \(\pi /(2j_q)\) behind the headline \(4.22\) is taken from the literature and is not among them): Margolus–Levitin, an \(L^1\) form of Mandelstam–Tamm, the Zieliński–Zych family for every exponent \(\alpha {\gt}0\) (whose key auxiliary inequality the original paper states without proof), a time-dependent single-qubit bound with its equality case for fixed-axis pulses and its finite-tolerance version, an entangling-time bound in arbitrary local dimension with its shifted, locally equivalent (ECR) and finite-tolerance versions (Section II), and, for the CZ in \(d\)-level transmons, the norm bounds behind its asymptotic tightness and the key lemma of the refined bound (Section VII). (2) A convention fixed by independent data. The drive-strength parameter is pinned by IBM’s calibrated \(\pi \) pulses through an exact pulse-area identity that holds on all 777 qubits with pulse definitions, up to which of two pulse normalizations reaches the qubit, which also reveals that it is derived from calibration rather than measured independently (Section III). (3) A sweep of deployed hardware: single-qubit gates on 1646 qubits, two-qubit gates on 1758 pairs, and a 2021–2025 time series (Sections IV–VI); for the single-qubit sweep, a falsifier and three rival hypotheses were written before the analysis, and we report their fate. (4) Feasible times found by optimal control on the vendor’s own model, bracketed by lower bounds (certified, or proved in the text) and, for the CZ, by an explicit construction, which in \(d\)-level transmons approaches the entangling-time bound as \(d\to \infty \) at fixed interaction norm, with ideal local control (Section VII). (5) An application beyond gates (version 2): IBM’s chip-to-chip state transfer runs at \(5.8\)–\(7.9\) times the single-mode minimal time, whose lower bound we machine-check in Isabelle; the master equation of the optimal protocol puts its coherence error four to six times below the measured errors (Section VIII). We claim no new physics: the speed limits are classical, the two-qubit constants are known for qubits, and the transmon model is IBM’s. The exceptions are mathematical: the \(d\)-level quadrature code for the CZ and its asymptotic tightness were not found in the sources we read (Section VII). To our knowledge no prior work applies a proof-assistant-certified QSL to public calibration data with a per-gate gap; a search that finds nothing does not prove novelty. Section IX states what the certificate covers.
The calibrated peak Rabi frequency sits at a nearly fixed fraction of the anharmonicity: over 750 qubits, \(\Omega _{\rm peak}/|\delta |\) has median \(0.0907\) and 10th–90th percentile \([0.0607,0.0992]\), i.e. a cap near \(0.1\), taking the peak as \(\texttt{omegad}\, |\mathrm{amp}|\); with the peak \((1-e^{-2})\, \texttt{omegad}\, |\mathrm{amp}|\) consistent with omegad the median is \(0.078\). We read this as IBM’s design rule, not a physical limit.
Writing \(\tau _X/\tau _{\rm QSL}=\mathrm{duration}\cdot dt\cdot \texttt{omegad}/\pi \), the gap factors into \(\approx 2.16\)—the duration over \(A_{\rm rec}\), i.e. the pulse-shape factor \(1.87\) (a \(4\sigma \) Gaussian with its edge removed against a square pulse of the same peak) times the normalization \(1/(1-e^{-2})\)—times \(1/\mathrm{amp}\approx 5\). Since \(\texttt{omegad}\cdot |\mathrm{amp}|\cdot A_{\rm rec}=\pi \), the ratio is exactly \(\tau _X/\tau _{\rm QSL}=\mathrm{duration}\cdot dt/(|\mathrm{amp}|A_{\rm rec})\approx 2.16/|\mathrm{amp}|\): with a nearly fixed envelope, the spread of the ratio is the spread of the calibrated amplitudes (IBM calibrates the \(\pi \) pulse at \(\mathrm{amp}\approx 0.2\): an amplitude reserve). Neither the speed limit nor the anharmonicity fixes the duration; engineering choices do: a duration fixed in samples per backend and a low amplitude. The headline with its denominators. The median \(11.3\) is measured against \(\pi /\Omega _{\max }\) with \(\Omega _{\max }=\texttt{omegad}\), the drive at full amplitude \(|D|=1\). The calibrated peak drive is \(\Omega _{\rm peak}\approx 0.09|\delta |\); the factor \(\approx 5\) between that drive and full amplitude is headroom chosen by design, and at the drive actually used the gap is the shape factor \(1.87\) if the peak is \((1-e^{-2})\, \texttt{omegad}\, |\mathrm{amp}|\), or \(\approx 2.16\) if it is \(\texttt{omegad}\, |\mathrm{amp}|\). Optimal control on IBM’s own model (Table V) bounds the gain at the same peak drive: since \(T\ge 2\arcsin (1-e)/\Omega _{\rm peak}\), a gate with \(T\Omega _{\rm peak}/\pi =R_{\rm peak}\) can be shortened by at most \(R_{\rm peak}/0.991\), i.e. \(2.18\) with the nominal peak or \(1.89\) with the edge-subtracted one (at the slightly higher cap \(r=0.1\) the fastest pulse found, \(\approx 16\) ns against \(35.6\) ns, gives \(2.2\)); and, within the full amplitude, a median gate of \(11.3\, \tau _{\rm QSL}\) against a minimum between \(0.99\, \tau _{\rm QSL}\) (bound) and \(1.12\, \tau _{\rm QSL}\) (found at the median \(r_{\rm full}=0.351\)), i.e. about \(10\)–\(11\) times; for the Falcon example (\(35.6\) ns) at that amplitude, \(7.4\)–\(8.3\) times. A gate of \(\approx 3.4\) ns needs about three times that amplitude. In short: IBM runs the drive at about a tenth of the anharmonicity; at that drive its pulses are about \(2\) times the square-pulse limit at that drive and can be shortened by at most \(2.2\) at the same peak drive; within the full amplitude the model admits gates about \(10\) times faster than the median. The figure \(11.3\) should not be read as “gates are \(11\) times slower than possible”; those \(\approx 10\times \) are a model prediction.
Over 41 backends and 1646 qubits, the \(X\) gate lasts a median \(\tau _X/\tau _{\rm QSL}=11.30\) times its two-level speed limit at full drive amplitude (\(|D|=1\), \(\tau _{\rm QSL}=\pi /\texttt{omegad}\)), 5th–95th percentile \([7.19,15.54]\), minimum \(2.37\). The \(\sqrt X\) gate has the same duration and half the rotation, so its median ratio is \(22.61\). Qubits of one backend share a duration, so they are not independent: the median of the 41 per-backend medians is \(11.37\), and a bootstrap that resamples whole backends gives a \(95\% \) interval \([11.02,11.65]\) for the median. Against the leakage time scale \(2\pi /|\delta |\), the \(X\) gate lasts a median \(15.45\) periods \([10.90,18.70]\). IBM does not drive at that amplitude: the next nodes separate the part of the gap set by the drive actually used from the part set by amplitude headroom.
Before computing we wrote three rivals with predicted ranges: H1, amplitude-limited gates at \(1\)–\(2\times \) the limit; H2, leakage-limited gates, \(\tau _X\propto 1/|\delta |\), ratio \(2\)–\(6\), uncorrelated with omegad; H3, a convention artefact. Outcome: H1 is rejected against the full-amplitude limit (the gates are at \(\approx 11\times \)); against the peak drive actually used the ratio is \(\approx 2.16\), just above H1’s range, which did not specify the drive; with the peak \((1-e^{-2})|\mathrm{amp}|\) consistent with omegad it is \(1.87\), inside that range, so this comparison depends on the reading, while the full-amplitude one does not; H2 has no support (\(R^2\) of \(\log \tau _X\) on \(\log (1/|\delta |)\) is \(0.087\), and the gates last \(\approx 15\) leakage periods); the factor-\(2\) and factor-\(2\pi \) conventions of H3 are excluded by the \(\pi \)-pulse check, and the remaining \(15\% \) is the lifted-Gaussian normalization. The \(R^2\) on \(\log (1/\texttt{omegad})\) is \(0.692\) (shuffled control \(0.001\)), but because omegad is derived from the same pulse’s amplitude and width this is partly circular and is not independent physical evidence.
Since all qubits of a backend share one duration, one may ask how much would be gained by giving each qubit the shortest duration compatible with that cap (\(c=0.099\), the observed 90th percentile), keeping the pulse shape (750 qubits on 31 backends). The median per-qubit gain is only \(\times 1.09\) (\(\times 1.07\) if a layer waits for its slowest qubit): the cap binds almost every qubit alike. The backend cairo is a natural experiment: its common \(X\) duration is \(21.3\) ns where the cap would require a median of \(31.6\) ns, i.e. it runs at a drive fraction near \(0.15\), and works.
The same construction works for \(d\)-level transmons: encoding each qubit in the two extreme eigenvectors of \(Q_d=b+b^\dagger \) (eigenvalues \(\pm \lambda _d\), with \(\lambda _d/\sqrt2\) the largest zero of the Hermite polynomial \(H_d\)) gives a CZ in interaction time \(\pi /(2J\lambda _d^2)\), while the entangling-time theorem gives \(\pi /(4J\kappa _d)\) with \(\kappa _d=\| b^\dagger \otimes b+b\otimes b^\dagger \| \). The ratio of the two bounds is \(2\kappa _d/\lambda _d^2\): \(2\), \(1.33\), \(1.27\), \(1.20\), \(1.09\), \(1.05\) for \(d=2,3,4,5,10,20\), and it tends to \(1\). This is certified in Lean: \(\lambda _d^2/2\le \kappa _d\le 2(d-1)\) (QSL.Exchange.exchange_norm_ge, QSL.Exchange.exchange_norm_le), \(\lambda _d\ge 2(1-1/m)\sqrt{d-m}\) for the largest eigenvalue (QSL.Exchange.lamMax_ge), and \(2\kappa _d/\lambda _d^2\to 1\) (QSL.Exchange.ratio_tendsto_one); the rate is \(O(d^{-2/3})\) by the asymptotics of the largest Hermite zero (DLMF 18.16.17, not formalized). At a fixed interaction norm \(\| H_c\| =J\kappa _d\), the CZ time of the construction therefore approaches the Bell-preparation bound: the entangling-time bound becomes tight for the whole gate as \(d\to \infty \), with ideal local control. The averaging step is an instance of the no-overhead simulation framework of Wocjan, Rötteler, Janzing and Beth (2002); the quadrature code and the asymptotic tightness were not found in the sources we read.
For a gate with error \(e\), add a two-level reference to each transmon and start from the product (across \(AA'{:}BB'\)) of two local maximally entangled states: the overlap of the resulting state with the one produced by CZ is exactly \(|\mathrm{Tr}(CZ^\dagger PUP)|/4=1-e\), leakage included, and the CZ state has Schmidt coefficients \((1/\sqrt2,1/\sqrt2)\) across that cut, while the references leave \(\| H_c\| =2J\) unchanged. The tolerance version of the theorem (with \(\varepsilon =1-(1-e)^2\)) then gives \(T_*(e)\ge [\pi /4-\arccos (1-e)]/(2J)\) (this instantiation with references is ours, not formalized). Preparing the single output \(CZ|{+}{+}\rangle \) is a much easier task: local operations map \(|{+}{+}\rangle \) to \(|12\rangle \), on \(\{ |12\rangle ,|21\rangle \} \) the coupling acts as \(2J\sigma _x\), and local operations map the result back, so the state-preparation bound is attained exactly: it is a valid but weak bound for the gate. The norm-based bound is sharpened in the next node: \(0.4510/J\le T_*(2\cdot 10^{-8})\le 0.55/J\).
We optimized a CNOT on two 3-level transmons with a cross-resonance drive bounded by \(|\Omega _{\rm CR}|\le r\Delta \) at IBM median parameters (\(J/\Delta =0.0176\), \(\delta /\Delta =-2.7\), 10 segments). In units of the exchange time \(\pi /(2J)\) the shortest feasible times found (error \({\lt}10^{-3}\), upper bounds on the minimum) are \(3.27\) (\(r=0.25\)), \(1.82\) (\(r=0.45\), IBM’s calibrated fraction) and \(1.50\) (\(r=0.7\)). Since a larger cap admits every pulse of a smaller one, \(1.50\) is also feasible for every \(r\ge 0.7\); independent searches at \(r=1.0\) and \(1.5\) returned longer times, a failure of the local search, which we confirmed by re-expressing the \(r=0.7\) pulse under the larger caps (identical error) and continuing from it to shorter times, which did not reach \(10^{-3}\) down to \(1.2\). The searches use coarse time grids and few random starts; a repeated run at \(r=0.7\), \(T=1.50\) reached only \(1.2\cdot 10^{-3}\). What the data support is that at IBM’s fraction the fastest CNOT found is \(\approx 1.2\) times slower than at \(r=0.7\); they do not establish an optimum in \(r\).
Two 3-level transmons with a fixed exchange coupling \(J(b_1^\dagger b_2+{\rm h.c.})\) and fast local control (any Hermitian \(A_k\), \(B_k\) on each transmon, 8 piecewise-constant segments, exact gradients). The target is CZ on the qubit subspace with no leakage; the action outside it is free. Every solution is recomputed independently in float64. As a control, the qubit-only search reproduces the known time \(\pi /(2J)\) (a gate at \(\pi /(2J)\), none at \(0.89\, \pi /(2J)\)). Write \(T_*\) for the minimal time of an exact CZ with ideal (unbounded, instantaneous) local control, and \(T_*(e)\) for the minimal time of a CZ with error at most \(e\) in the trace metric used throughout. With local controls of at most \(10J\) during the gate (plus instantaneous local unitaries before and after), a CZ is realized to error \(\le 2\cdot 10^{-8}\) (leakage \(\le 4\cdot 10^{-8}\)) at \(T=0.55/J\), i.e. at \(0.35\) of the qubit-only time and \(5\% \) above the construction. At \(T=0.45/J\) and \(0.50/J\), relaxing the cap to \(20J\), \(40J\) or none did not improve the solutions found (\(\approx 5\cdot 10^{-3}\) and \(\approx 4\cdot 10^{-4}\)); this does not identify what limits them, and none was found at \(0.50/J\). For the same task and metric, \(0.4510/J\le T_*(2\cdot 10^{-8})\le 0.55/J\); the bound also shows that no protocol reaches \(e\le 2\cdot 10^{-8}\) at \(T=0.45/J\) (it needs \(e\ge 1.9\cdot 10^{-6}\) there), consistent with the \(5\cdot 10^{-3}\) found. The solutions populate the second level: up to \(60\% \) of the population of a computational input leaves the qubit subspace during the gate. Each code state of the construction has population \(1/3\) in \(|2\rangle \), so each encoded basis input has \(5/9\approx 56\% \) outside the qubit subspace (superpositions range from \(0\) to \(8/9\)); together with the \(\sqrt2\)-enhanced elements \(\langle 20|H_c|11\rangle \), \(\langle 02|H_c|11\rangle \) identified for CNOT and iSWAP, this suggests a mechanism for our solutions that we have not isolated. For the qutrit CZ, \(CZ_3|k,l\rangle =e^{2\pi ikl/3}|k,l\rangle \), with a capacitive coupling and drive cap \(40g\), the optimal-control time reported by Basyildiz, Gong and Ashhab is close to the qubit limit. That is a different gate: on the qubit subspace it is \(\mathrm{diag}(1,1,1,e^{2\pi i/3})\), not \(\mathrm{diag}(1,1,1,-1)\), and coupling and controls differ, so the two times are not comparable.
CZ maps \(|{+}{+}\rangle \) to a maximally entangled state, so the entangling-time theorem with \(\| H_c\| =2J\) (\(d=3\)) gives \(T_*\ge \pi /(8J)=0.393/J\). An explicit construction gives an upper bound. Writing \(H_c=\tfrac J2(Q\otimes Q+\Pi \otimes \Pi )\) with \(Q=b+b^\dagger \) and \(\Pi =i(b^\dagger -b)\), fast conjugations of one transmon by \(W=V_Q\, \mathrm{diag}(1,e^{2\pi i/3},e^{4\pi i/3})V_Q^\dagger \) (\(V_Q\) diagonalizing \(Q\)) average \(\Pi \otimes \Pi \) away and keep \(\tfrac J2Q\otimes Q\); encoding each qubit in the two extreme eigenvectors of \(Q\) (eigenvalues \(\pm \sqrt3\)) gives \(\tfrac {3J}{2}Z\otimes Z\), hence a CZ (up to local phases) in interaction time \(\pi /(6J)=0.5236/J\), in the limit of arbitrarily fast local operations So \(\pi /(8J)\le T_*\le \pi /(6J)\); the lower bound is sharpened to \(0.4511/J\) in the next nodes (the construction is then within \(16\% \) of the bound).
The gate bound itself can be sharpened, because the gate must act coherently on all logical inputs (the lemma is certified in Lean as QSL.Exchange.refined_cz_lemma, with its equality case, and checked numerically in cota_cz_refinada.py; the time argument built on it is not formalized). Let \(L(t)\) apply the same local controls as \(U(t)\) but without \(H_c\), and \(z(t)=U(t)^\dagger L(t)|\Omega _0\rangle \) with \(|\Omega _0\rangle \) the reference-extended product state above. Then \(\dot z=iU^\dagger H_cL|\Omega _0\rangle \), whose Fubini–Study speed is the spread of \(H_c\) in \(L(t)|\Omega _0\rangle \); that state has physical reduced state \((P_A\otimes P_B)/4\) with \(P_A,P_B\) rank-2 projectors, and for any such projectors \(\tfrac 14\mathrm{Tr}[(P_A\otimes P_B)H_c^2]\le \tfrac {97}{32}J^2\) (equality at \(P=\mathbb 1-|v\rangle \langle v|\), \(|v\rangle =\sqrt{7/8}|0\rangle +\sqrt{1/8}|2\rangle \)). Since \(L(T)|\Omega _0\rangle \) is a product across \(AA'{:}BB'\) and the CZ state is at Fubini–Study distance at least \(\pi /4\) from every product, \(T_*(e)\ge [\pi /4-\arccos (1-e)]/(J\sqrt{97/32})\), i.e. \(T_*\ge 0.4511/J\) and \(T_*(2\cdot 10^{-8})\ge 0.4510/J\), \(15\% \) above the norm bound. With ideal local control, \(0.4511/J\le T_*\le \pi /(6J)=0.5236/J\) (the upper value as a limit of finite protocols); the construction is within \(16\% \) of the bound. Preparing one Bell state and implementing the whole CZ therefore have different minimal times in this model.
Version 3: both ends improved. Apply two identical copies of a protocol to \(\chi _0=\psi ^-_{A_1A_2}\otimes \psi ^-_{B_1B_2}\), the singlets of the qubit subspace. Local controls preserve the symmetric and antisymmetric subspaces of each pair, and the copies are exchanged by a symmetry, so the state stays in \(\wedge ^2\otimes \wedge ^2\oplus \mathrm{Sym}^2\otimes \mathrm{Sym}^2\); an exact CZ must carry it from the first sector to the second, at a rate at most \(\| K\| \), with \(K\) the block of \(H_c^{(1)}+H_c^{(2)}\) between them. In exact arithmetic \(\| K\| ^2=\tfrac {23}{2}J^2\), so \(T_*\ge \pi /(\sqrt{46}\, J)=0.4632/J\). In the other direction, the average of 18 local conjugates of \(H_c\) keeps, besides \(\tfrac J2Q\otimes Q\), a three-state block \(\{ |\ell \ell \rangle ,|mm\rangle ,|hh\rangle \} \) in the eigenbasis of \(Q=b+b^\dagger \); with a local detuning of \(|m\rangle \) the block returns exactly at \(T_2=3\pi /\big(2(1+\sqrt{65})J\big)=0.5200016/J\) and the code undergoes a CZ up to local phases. A second-order product of 64 steps followed by an exact correction is certified by a Krawczyk test in interval arithmetic, \(T_*\le 0.520023/J\) (two negative controls are rejected). Hence \(0.4632/J\le T_*\le 0.5200/J\), between \(0.295\) and \(0.331\) of the qubit-only time.
For \(H=XX+YY+ZZ\) and fast local control, the smallest largest-Schmidt-coefficient found from a product state at time \(T\) is \(\lambda (T)=\cos (2T)\) to \(10^{-13}\) without ancillas and to \(10^{-8}\) with one ancilla qubit per side, up to the Bell time \(\pi /8\). The same identity \(\lambda (T)=\cos (wT)\), with \(w\) the spectral half-width, holds for Ising \(ZZ\) and \(XY\) couplings with and without ancillas (errors \(\le 3\cdot 10^{-7}\)). The norm bound gives rate \(\| H\| =3\); the identity says the right rate is the spectral half-width \((E_{\max }-E_{\min })/2=2\). This is a certified corollary: since \(H-c\mathbb 1\) differs from \(H\) by \(c\mathbb 1\), which can be absorbed in the local control, \(\arccos \lambda \le T\, \| H-c\mathbb 1\| \) for every real \(c\); for Heisenberg \(\| H+\mathbb 1\| =2\) (because \(H+\mathbb 1=2\, \mathrm{SWAP}\)), whence \(T\ge \pi /8\). An explicit trajectory reaches the bound: \(e^{-iHT}|01\rangle =e^{iT}[\cos (2T)|01\rangle -i\sin (2T)|10\rangle ]\), whose largest Schmidt coefficient is \(\cos (2T)\) for \(T\le \pi /8\). Local ancillas do not change the spectrum of the coupling and so cannot lower this bound.
For IBM’s typical \(|\delta |\approx 2.07\) rad/ns, the fastest pulse found at IBM’s own cap \(r=0.1\) takes \(\approx 16\) ns, against \(35.6\) ns for Falcon single-qubit gates (e.g. jakarta): a factor \(\approx 2.2\) at that cap, which is slightly above the calibrated peak drive (median \(0.091\)). At \(r=1\) the 4-level search finds \(T=6.9/|\delta |\) (\(3.3\) ns), but the truncation matters at this drive (next node). At IBM’s cap the 4-level pulse is unaffected by more levels (\(\eta _4=0.01\)). As an independent point of comparison, a \(4.16\) ns single-qubit pulse on a superconducting transmon, with \(99.76\% \) fidelity and \(0.044\% \) leakage, has been demonstrated by optimal control (Werninghaus et al.); its elementary pulses are \(\pm X/2\) and \(\pm Y/2\) characterized by Clifford-based protocols, a different task from our simulated \(X\) gate, so it gives context, not validation. Limits: the time grid is coarse, the search is local, and there is no noise or line distortion in the model.
We ran optimal control on a 4-level Duffing transmon in units \(|\delta |=1\), with a piecewise-constant complex drive bounded by \(|\Omega |\le r|\delta |\), and searched, on a grid of times, for the shortest time at which an \(X\) gate with error \({\lt}10^{-4}\) including leakage is found. The two-level control returns \(T=\pi /\Omega _{\max }\) exactly. The results follow \(T_{\rm found}\approx \max \! \big(\pi /\Omega _{\max },\ \sim 1.1\cdot 2\pi /|\delta |\big)\), a speed-limit branch for \(r\lesssim 0.3\) and a leakage-dominated branch for \(r\gtrsim 0.8\). This is an empirical fit to a coarse grid, not a theorem; it misses the values found at \(r=0.3\)–\(0.5\) by \(13\)–\(16\% \), where neither branch dominates. The entries are feasible times found, i.e. upper bounds on the true minimum: a larger cap admits every pulse of a smaller one, so the true minimum cannot increase with \(r\), and the value at \(r=1.5\) above that at \(r=1.0\) shows that the search is local. Shortest time found (units \(|\delta |=1\); ratio to \(\pi /\Omega _{\max }\)): \(r=0.1\): \(33.0\) (\(1.05\)); \(0.2\): \(16.5\) (\(1.05\)); \(0.3\): \(12.0\) (\(1.15\)); \(0.5\): \(8.2\) (\(1.30\)); \(0.8\): \(7.1\); \(1.0\): \(6.9\); \(1.5\): \(7.3\).
A lower bound holds for any number of levels. With \(H(t)=H_{\rm diag}(t)+\tfrac 12(u\, b^\dagger +u^*b)\), \(|u|\le \Omega _{\max }\), and \(p_0=|a_0|^2\) the population of \(|0\rangle \), the only way out of \(|0\rangle \) is through \(|1\rangle \), so \(|\dot p_0|\le |u|\, |a_0||a_1|\le |u|\sqrt{p_0(1-p_0)}\) and the angle \(\theta =\arccos \sqrt{p_0}\) obeys \(|\dot\theta |\le |u|/2\). An \(X\) gate takes \(\theta \) from \(0\) to \(\pi /2\), hence \(T\ge \pi /\Omega _{\max }\) for any truncation; with a transfer fidelity \(|\langle 1|\psi _T\rangle |^2\ge 1-\varepsilon \), \(T\ge 2\arccos \sqrt\varepsilon /\Omega _{\max }\). (This short proof is ours and not formalized; the two-level case is QSL.Gate.two_arccos_sqrt_le_time_approx.) In the trace metric of Table V the same argument bounds \(|U_{10}|,|U_{01}|\le \sin (\Omega _{\max }T/2)\) for \(T\le \pi /\Omega _{\max }\), so an error \(e\) needs \(T\ge 2\arcsin (1-e)/\Omega _{\max }\); for \(r\le 0.2\) the times found are \(6\% \) above it (\(e=10^{-4}\)), so there the minimum is known to \(6\% \); at IBM’s cap (\(\Omega _{\max }=0.1|\delta |\), \(|\delta |=2.07\) rad/ns) the archived \(35.6\) ns lies between \(2.2\) and \(2.4\) times the true minimum (bound \(15.0\) ns for that tolerance, pulse found \(15.9\) ns).
The drive fraction \(r=1\) is not available in the analysed snapshots: the full amplitude \(|D|=1\) corresponds to \(r_{\rm full}=\texttt{omegad}/|\delta |\), median \(0.351\) (\(5\)th–\(95\)th percentile \([0.24,0.61]\)). At \(r=0.351\) a 6-level search finds an \(X\) at \(T=10.0/|\delta |=4.8\) ns with \(1-F=2.8\cdot 10^{-8}\), unchanged with 12 levels, while the bound above gives \(T\ge 8.87/|\delta |=4.3\) ns; so within the amplitude budget of the median device a \(35.6\) ns Falcon gate is \(7.4\) times the fastest gate found and at most \(8.3\) times the bound, i.e. \(7.4\)–\(8.3\) times the minimum of the model, and the median gate (\(11.3\, \tau _{\rm QSL}\), with \(\tau _{\rm QSL}=8.95/|\delta |\) at \(r=0.351\)) is \(10\)–\(11\) times.
At \(r=1\) the 4-level search finds \(T=6.9/|\delta |\) (\(3.3\) ns), but the truncation matters at this drive: the 4-level pulse at \(T=7.0/|\delta |\) keeps \(1-F=7\cdot 10^{-9}\) in 4 levels but degrades to \(5.5\)–\(7.2\cdot 10^{-4}\) with 5 to 12, and the Duhamel bound on the distance to a larger model, \(\eta _4=\int |u|\, \| \langle 3|U P\| \, dt=0.55\), does not certify it. A pulse optimized with 6 levels at the same time reaches \(1-F=4.0\cdot 10^{-6}\) there and \(3.6\cdot 10^{-6}\) with 8 and 12 levels, so a gate of \(\approx 3.4\) ns (\(T=7.0/|\delta |\)), more than ten times shorter than IBM’s, survives in the converged model; it is a numerical witness in an idealized model, not a physical floor. The table entries for \(r\ge 0.8\) are 4-level values and are not converged in the number of levels.
The ratio grew from \(2.78\) (2021) to \(4.26\) (2025). The coupling did not change: \(g/2\pi \approx 1.9\)–\(2.1\) MHz in every processor family, and within a processor \(j_q\) is identical at every date—a model value carried over, not re-measured. The change is the duration: Eagle ECR gates (median 562 ns) against Falcon CX gates (\(\approx 377\) ns), and recalibrations lengthen gates and never shorten them in the examples examined (bogota \(366\to 544\) ns, perth \(380\to 491\) ns, lagos \(299\to 452\) ns). The trend describes the snapshots in the series, which are all pre-Heron: it reflects the transition from Falcon CX to Eagle ECR gates, not the whole fleet. The current Heron generation, with CZ gates of \(\approx 68\)–\(70\) ns (\(68\) ns median in our torino snapshot; \(70\) ns measured on ibm_torino by Ishida and Hasegawa), is not in the series, because its snapshots carry no Hamiltonian.
Across the 80 snapshots with two-qubit durations and errors, Spearman’s correlation between median two-qubit duration and median gate error is \(+0.13\) (\(p=0.23\)). For the same pair lengthened between two dates (71 cases), the error rises (median change in \(\log \) error \(+0.21\); it falls in only \(31\% \)); for pairs shortened (40 cases) it falls. These comparisons are observational: other calibration changes and drift happen at the same dates.
We then asked whether lengthened pairs had worse qubits. Pooled across dates, \(T_1\) of lengthened pairs fell more than that of unchanged pairs (Mann–Whitney \(p=0.0017\)). Under a stratified control (same backend, same dates; 18 strata, 84 lengthened pairs) the effect vanished (Wilcoxon \(p=0.90\) for \(T_1\), \(p=0.99\) for \(T_2\)); a pooled frequency-shift effect (\(p=4\cdot 10^{-12}\)) vanished likewise. The pooled effects are consistent with confounding by epoch: lengthenings concentrate in backends and periods in which the whole chip’s \(T_1\) fell. We retracted the reading that lengthened pairs had degraded qubits: after controlling for backend and date the data do not support pair-specific degradation. This does not show what does drive lengthening. Any cross-date effect in calibration snapshots should be tested stratified by backend and date before it is read.
Median gaps by year (56 usable snapshots, 41 backends). Two-qubit ratio against \(\pi /(2j_q)\). Single qubit \(\tau _X/\tau _{\rm QSL}\): \(11.28\) (2021), \(11.32\) (2022), \(11.21\) (2023), \(11.10\) (2024), \(11.87\) (2025). Two qubits \(\tau _{2q}/(\pi /2j_q)\): \(2.78\), \(2.64\), \(4.32\), \(3.89\), \(4.26\). The ratio stays at \(\approx 11\) over five years for a single qubit: a design constant. For two qubits it grew from \(2.78\) (2021) to \(4.26\) (2025). Snapshots per year: \(27\), \(4\), \(2\), \(16\), \(7\); the 2022 and 2023 medians rest on 4 and 2 snapshots respectively. One time-series snapshot (toronto, 2021-03-15, median two-qubit duration 6315 ns, ratio \(\sim 40\)) is kept in the table; removing it changes the 2021 two-qubit median from \(2.78\) to \(2.74\) and the single-qubit one not at all.
Against our certified chord constant \(\sqrt{2-\sqrt2}/j_q\) the median ratio is \(8.7\); the sharp Lean constant \(\pi /4\) lowers it by \(2.6\% \) to \(8.4\), and since \(\pi /(4j_q)\) is exactly half of \(\pi /(2j_q)\) the certified ratio is exactly twice the literature ratio. Both are correct; they bound different tasks. Both assume \(\| H_{\rm int}\| =j_q\), i.e. the qubit subspace. With the second transmon level the norm grows to \(2j_q\), the certified time bound halves to \(\pi /(8j_q)\) and the certified ratio doubles to \(\approx 16.9\): the bound becomes weaker, which says nothing about how much of that room is reachable. Our \(\pi /(8j_q)\) for \(d=3\) is not tight; Section VII sharpens it to \(0.4511/j_q\) for the CZ.
Numerical controls of the certified bound: the Duhamel inequality has \(0\) violations in \(20\, 000\) random pairs, with maximum ratio \(0.99998\) (the constant \(1\) is sharp), and the bound has \(0\) violations in \(3000\) evolutions with random local control.
IBM’s CX is built from echoed cross-resonance (CR) pulses. To first order the CR drive of amplitude \(\Omega \) on the control, at detuning \(\Delta \), produces a \(ZX\) rate \(\nu _{ZX}=-(J\Omega /\Delta )\, \delta _c/(\delta _c+\Delta )\), and a CNOT needs \(\theta _{ZX}=\nu _{ZX}t_{\rm CR}=\pi /2\). On 1212 calibrated CX gates in 29 backends the median of \(\theta /(\pi /2)\) is \(1.109\), 10th–90th percentile \([0.870,1.472]\), with \(59\% \) in \([0.8,1.2]\). The median lies \(11\% \) above the target, with a wide spread. The calibrated drive sits at a nearly fixed fraction of the detuning: \(|\Omega _{\rm CR}/\Delta |\) has median \(0.451\). The two gaps share one pattern: the control runs at a fixed fraction of an energy splitting it must not excite—\(\Omega _{\rm peak}\approx 0.09|\delta |\) for one qubit, \(\Omega _{\rm CR}\approx 0.45\Delta \) for two. The calibrated drives lie outside the stated range of the perturbative expansion (\(53\% \) of the gates have \(\Omega /2\pi {\gt}50\) MHz); with the third-order term the median falls to \(0.898\) (\([0.659,1.105]\)), and a numerical block diagonalization gives \(0.967\) (\([0.795,1.159]\), \(81\% \) in \([0.8,1.2]\)). Flipping the sign of \(\Delta \) moves the median away from 1 (\(0.664\)), as a control should. One convention is unresolved: the Qiskit control channel of the pair \((c,t)\) is weighted by the drive strength of the target, whereas we use that of the control; with the former the first-order median is \(1.089\).
In the qubit subspace the IBM coupling is \(j_q(\sigma ^+_i\sigma ^-_j+\mathrm{h.c.})=(j_q/2)(XX+YY)\), of operator norm \(j_q\). Literature bound for the gate. With unbounded local control, no leakage, and an \(XY\) coupling, the minimal time of a CNOT-class gate (CNOT, CZ, ECR) is \(\pi /(2j_q)\). This follows from Howard et al., Appendix C, and from the majorization theory of Vidal–Hammerer–Cirac. The detuning is a local term absorbed by the unbounded local control, and bounded drives are a subset of unbounded ones, so within the qubit subspace the real duration cannot beat it [our inference, not stated in that form in the sources]. Our certified bound for state preparation. The Lean theorem bounds the time to create a Bell state from a product state: \(\pi /(4J)\), attainable. A full CNOT on an \(XY\) coupling needs twice that, which is why the literature bound is the stronger one for gates. Ours is the one that is machine-checked, and it survives extra transmon levels: with \(|2\rangle \) included the norm of the exchange term grows (\(\| a^\dagger b+ab^\dagger \| =1,2,3.4641\) for \(d=2,3,4\)), and the CNOT bound becomes \(\pi /(4J)\) with that larger \(J\). With leakage levels allowed, the only rigorous constant in the literature is for iSWAP; for CNOT/ECR with \(|2\rangle \) no constant was found in the sources read. Ours, \(\pi /(8j_q)\) for \(d=3\), is not known to be tight. Against the literature bound the median ECR/CX lasts \(4.22\) times its limit.
From the snapshots we extract every coupled pair with a coupling \(j_q\) in the Hamiltonian variables and a calibrated two-qubit gate: 1758 pairs in 43 backends (1019 ECR, 739 CX). The median coupling is \(j_q=0.01268\) rad/ns (\(g/2\pi \approx 2.0\) MHz), the median detuning \(115\) MHz (\(\approx 60\, j_q\)), and the median gate duration \(548\) ns (5th–95th percentile \([277,698]\) ns).
(i) The cable has many modes (free spectral range \(\approx 150\) MHz, \(g/{\rm FSR}\approx 0.05\)–\(0.06\) by the authors’ figures); protocols that use several modes are not covered by the single-mode optimum, and for them the certified floor and the Isabelle bound \(\pi /(\sqrt2\, G)\) hold with the collective coupling norm \(G\) of each end, which is not reported. (ii) \(g\) is the maximal coupling; the ratios measure the distance to what that maximum allows, not to the waveforms used. (iii) The reported fidelity and the error model are IBM’s; the occupations \(\tfrac 12\)–\(\tfrac 12\) are IBM’s assumption, and for the qubits we use, as IBM does, the shorter coherence time of each pair. (iv) The master equation takes dephasing as Markovian at the rate set by the Ramsey \(T_2\); low-frequency noise would change the dephasing terms.
By IBM’s own error model most of the measured error is coherence at these durations. At the optimum, with the same coherence times, the coherence error of the optimal protocol is \(0.13\)–\(0.26\% \) (master equation, checked against an independent integrator), four to six times below the measured errors. The additive model of Eq. (2) evaluated with the occupations of the optimal protocol gives less, \(0.09\)–\(0.17\% \): it is exact for relaxation but not for pure dephasing while the excitation is shared between elements. This is the coherence error of one admissible protocol, not a floor: a slower protocol can lose less (with lossless cable and lossy qubits the sequential protocol, at twice the duration, has a smaller error), and a floor would need an inequality valid for every control.
Since \(\| H(t)\| =(|g_1|^2+|g_2|^2)^{1/2}\le \sqrt2\, g\) and the transfer \(|A\rangle \to |B\rangle \) needs a Fubini–Study angle \(\pi /2\), the bound QSL.Gate.fsAngle_le_time_halfWidth of Section II (with shift \(c=0\); it holds in any dimension) gives \(T\ge \pi /(2\sqrt2\, g)\) for piecewise-constant couplings of any phase. It is certified and not tight.
IBM chip-to-chip transfers against the single-mode optimum \(\pi /(\sqrt2\, g)\), for \(g/2\pi =8\) and \(9\) MHz (\(44.2\) and \(39.3\) ns). Q240–Q247: \(T_g=312\) ns, \(T_g/T_{\min }=7.06\)–\(7.94\), error \(0.71\% \), coherence at \(T_g\) (IBM’s model) \(0.63\% \), coherence at \(T_{\min }\) \(0.13\)–\(0.15\% \). Q241–Q246: \(296\) ns, \(6.70\)–\(7.53\), \(1.13\% \), \(0.87\% \), \(0.23\)–\(0.26\% \). Q242–Q245: \(256\) ns, \(5.79\)–\(6.52\), \(1.01\% \), \(0.61\% \), \(0.16\)–\(0.18\% \). Q243–Q244: \(312\) ns, \(7.06\)–\(7.94\), \(1.14\% \), \(0.94\% \), \(0.22\)–\(0.24\% \). The ratios are ratios to the optimum of the single-mode model with the published maximal couplings; they do not show that the device admits a speed-up by that factor at the same fidelity. The transfers last \(5.8\)–\(7.9\) times the single-mode optimum, \(4.1\)–\(5.6\) times the sequential time and \(11.6\)–\(15.9\) times the certified floor. The \(126\) ns that the authors give as a target would still be \(2.9\)–\(3.2\) times the optimum.
The same diagnostic applies to operations other than gates. Sundaresan et al. transfer a qubit state between two 120-qubit processors through an \(80\) cm aluminium coaxial link (an “L-coupler”), relaying the excitation through one standing mode of the cable. They report the maximal qubit–mode coupling, \(g/2\pi =8\)–\(9\) MHz (their Fig. 1f), the transfer duration \(T_g\) and the fidelity of each of four links (their Extended Data Table 2), and the coherence times of qubits and cable modes (Extended Data Tables 1 and 2). The coupling waveforms are not published. Model. In the single-excitation subspace, with the rotating-wave approximation and one resonant mode, the relay is a three-level problem on \(|A\rangle \) (first qubit), \(|C\rangle \) (cable mode), \(|B\rangle \) (second qubit): \(H(t)=g_1(t)\, (|A\rangle \langle C|+{\rm h.c.})+g_2(t)\, (|C\rangle \langle B|+{\rm h.c.})\) with complex \(g_i(t)\), \(|g_i(t)|\le g\) and \(g=2\pi \times (g/2\pi )\).
For this model the minimal time is \(\pi /(\sqrt2\, g)\), reached with both couplings constant and at their maximum: the isotropic case of Theorem 1 of Boscain, Chambrion and Charlot. The lower half, \(gT\ge \pi /\sqrt2\), is machine-checked in Isabelle/HOL (Relay_Minimal_Time.relay_minimal_time, entry Quantum_Speed_Limits) for the amplitudes \(x=|a_A|\), \(z=|a_B|\), which satisfy \(|\dot x|,|\dot z|\le g\sqrt{1-x^2-z^2}\) away from a countable set of times; the proof uses an explicit calibration function, and the reduction from the Schrödinger equation to these inequalities is in the text, not in Isabelle. We also reproduced the optimum numerically with piecewise-constant controls, real and complex: no control found reaches full transfer for \(gT{\lt}\pi /\sqrt2\). With these couplings the excitation spends a quarter of the time in the cable (\(\int _0^T|c(t)|^2dt=T/4\)). The sequential protocol (two swaps) takes \(\pi /g\).
All scripts and data are in the companion package of the blueprint, https://karlesmarin.github.io/blueprints/qsl-diagnostics/companion/ (Apache 2.0): convencion.py (three-level check of the drive convention), pulsos_x.py and identidad_omegad.py, identidad_calibracion.py (convention from calibrated \(\pi \) pulses), barrido.py (single-qubit sweep, barrido.csv), pares.py (two-qubit pairs, pares.csv), cruce_formulas.py (CR and peak-Rabi checks), serie_temporal.py, serie_porque.py, duracion_error.py (time series, serie.csv), degradacion.py and frecuencia_degradados.py (stratified controls), mejora_por_cubit.py (per-qubit durations), mediana_por_backend.py (backend-weighted median, clustered bootstrap), toronto_sensibilidad.py (outlier sensitivity), control_dos_cubits.py and cnot_m3.py (numerical controls of the certified bounds), grape_1q.py, grape_cr.py and grape_cr_continuacion.py (monotonicity check), grape_cz_torch.py with its independent check verificar_cz.py, grape_bell_torch.py, grape_anchura.py, poblacion_cz.py (optimal control), fuentes/cruce_mg2020.py (higher-order CR check), cruces_area_cz.py (pulse-area identity, CZ construction) and truncacion_1q.py (truncation check), tercera_revision.py (gate-metric bounds, \(r_{\rm full}\)), cota_cz_refinada.py (refined CZ bound). Data: qiskit-ibm-runtime 0.51.0 and qiskit-terra 0.24.1 fake-backend snapshots (Apache 2.0), copied in datos/ and datos_serie/. The Lean sources are at https://github.com/karlesmarin/formalizations, commit 42f307b. The calibrated pulses (qiskit-terra 0.24.1) are copied in datos_pulsos/; a self-check rebuilds barrido.csv inside the package and compares it with the archived file. A companion blueprint, https://karlesmarin.github.io/blueprints/qsl-diagnostics/, maps each claim of this paper to its Lean theorem or script. Its laboratories run in the reader’s browser on the reader’s own values: Figs. 1–4 redrawn live; the fixed-axis equality on the Bloch sphere for any envelope; the certified floors of Section II for a list of the reader’s own gates (diagnose your device), which fires the falsifier of Section III on any gate below its floor; and the \(d\)-level CZ bounds of Section VII. Each result can be downloaded as CSV or shared as a link with its inputs. For Section VIII (version 2): relevo/datos/ibm_2610.29986.toml (the published values, each with its table), relevo/cocientes.py, relevo/diag_relevo.py, relevo/lindblad_relevo.py with its independent check relevo/lindblad_rk4.py, relevo/suelo_lindblad.py, relevo/comparar_modelos.py, relevo/falsar_v198.py, relevo/tiempo_minimo.py and relevo/heya_satd.py, which reproduces the published Lindblad simulation of an IBM SATD transfer as a validation of the simulator. The Isabelle sources of Quantum_Speed_Limits are in the same package.