A matching threshold of 2×10⁻³ for the rotated surface code under circuit-level noise

We consider the rotated surface code of odd distance $d$ with its standard syndrome-extraction circuit, under circuit-level depolarizing noise in which every gate, idle step, preparation and measurement fails independently with probability $p$, decoded by minimum-weight perfect matching with the log-likelihood weights of single faults. We prove that a memory experiment with $T$ rounds fails with probability at most $0.061\,(T+1)(d+1)\,\lambda^{d}/(1-\lambda)$, where $\lambda=0.999\,(p/p_{\ast\ast})^{9/25}$, for every $p\le p_{\ast\ast}=2\times10^{-3}$. Hence the logical error rate per round decays exponentially in $d$ for all $p\le p_{\ast\ast}$. Earlier rigorous thresholds for matching on surface-code circuits are $1.7\times10^{-4}$, due to Dennis, Kitaev, Landahl and Preskill, and $7.4\times10^{-4}$, due to Fowler. We keep their reduction of a failure to a weighted self-avoiding path in the decoding graph, but bound these paths by a local criterion for non-backtracking walks, which gives the threshold $1.04\times10^{-3}$ in closed form. To reach $2\times10^{-3}$ we use the minimality of the correction along the path, for a canonical choice among the minimum-weight corrections: labellings of short stretches of the path into error and correction edges that contradict this minimality are excluded, and the remaining labelled walks are counted with a potential function that is checked in exact arithmetic. For a leaner schedule with fused measure-and-reset steps the two arguments give $1.53\times10^{-3}$ and $3\times10^{-3}$, respectively. With error rates that depend on the type of operation, they certify exponential decay for error models built from the published component error rates of Quantinuum's Helios and H2 and of IBM's Heron r3 processor ibm_boston, mapped onto this circuit. All theorems are also proved in the proof assistant Lean 4, with all computations checked by its kernel. Any argument that bounds the failure probability by the probability of an increasing event, ours included, is limited by the smallest such event that contains all failures, and Monte Carlo estimates place the threshold of this event near $4\times10^{-3}$ for this circuit.