Certified Speed-Limit Diagnostics for Deployed Superconducting Quantum Processors

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 π 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.287 and 1/3 of the qubit-only exchange time (refined bound, explicit construction); 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. Companion site (blueprint): https://karlesmarin.github.io/blueprints/qsl-diagnostics/