\documentclass[11pt]{amsart}
\pdfsuppressptexinfo=-1
\usepackage[margin=1.1in]{geometry}
\usepackage{amsmath,amssymb,amsthm,mathtools}
\usepackage{booktabs,enumitem,array}
\usepackage[hidelinks]{hyperref}
\hypersetup{pdftitle={A matching threshold of 2e-3 for the rotated surface code under circuit-level noise},pdfauthor={Tejasvi Singh Tomar}}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}
\numberwithin{equation}{section}
\setlength{\emergencystretch}{2em}

\newcommand{\Pfail}{P_{\mathrm{fail}}}
\newcommand{\pst}{p_\ast}
\newcommand{\dX}{\delta^{X}}
\newcommand{\dZ}{\delta^{Z}}
\newcommand{\cD}{\mathcal{D}}
\newcommand{\cF}{\mathcal{F}}
\newcommand{\ver}{\textsuperscript{\dag}}

\begin{document}

\title[Matching threshold for the rotated surface code]{A matching threshold of $2\times10^{-3}$ for the rotated surface code under circuit-level noise}
\author{Tejasvi Singh Tomar}
\renewcommand{\urladdrname}{{\itshape ORCID}}
\urladdr{\href{https://orcid.org/0000-0003-4668-3639}{https://orcid.org/0000-0003-4668-3639}}
\date{20 October 2026}
\subjclass[2020]{81P73; 94B35, 05C38, 68V05}
\keywords{Quantum error correction, surface code, fault tolerance, threshold, minimum-weight perfect matching, circuit-level noise, computer-assisted proof}

\begin{abstract}
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.
\end{abstract}

\maketitle

\section{Setting and result}\label{sec:setting}

The rotated surface code decoded by minimum-weight perfect matching is a standard model of a fault-tolerant quantum memory. Under circuit-level noise, simulations place its threshold near $0.5$--$1\%$ \cite{WFH11,FMMC12}, and for the circuit considered here the logical failure curves cross near $5\times10^{-3}$ (Remark~\ref{rem:numerical}). But rigorous thresholds are much smaller. The path argument of Dennis, Kitaev, Landahl and Preskill \cite{DKLP02} gives $1.7\times10^{-4}$, and Fowler's refinement \cite{Fow12} reaches $7.4\times10^{-4}$, each for its own circuit and noise model. For the standard syndrome-extraction circuit we prove $1.04\times10^{-3}$ in closed form and $2\times10^{-3}$ with a computer-verified certificate, by a local criterion for weighted non-backtracking walks and by the minimality of the correction along the failure path. All theorems are also proved in the proof assistant Lean~4, with all computations checked by its kernel (Section~\ref{sec:lean4}).

\subsection{Code and circuit}\label{sec:circuit}
Fix an odd distance $d\ge3$. The data qubits sit at the points of
\[
\cD=\{(x,y): x,y\in\{1,3,\dots,2d-1\}\}.
\]
A point $m=(x,y)$ with $x,y\in\{0,2,\dots,2d\}$ has the diagonal neighbourhood $N(m)=\{m+(\pm1,\pm1)\}\cap\cD$. It has \emph{X type} if $x/2+y/2$ is odd and \emph{Z type} otherwise. The measure qubits are the points $m$ with $|N(m)|\ge2$, excluding X-type points with $x\in\{0,2d\}$ and Z-type points with $y\in\{0,2d\}$. There are $d^2-1$ of them. An X-type (Z-type) measure qubit $m$ measures the stabilizer $\prod_{q\in N(m)}X_q$ ($\prod_{q\in N(m)}Z_q$). Write
\[
\dX=\bigl((1,1),(-1,1),(1,-1),(-1,-1)\bigr),\qquad \dZ=\bigl((1,1),(1,-1),(-1,1),(-1,-1)\bigr).
\]
One round of syndrome extraction consists of eight steps.
\begin{enumerate}[label=\textup{(S\arabic*)},leftmargin=3em]
\item Reset every measure qubit to $|0\rangle$.
\item Apply $H$ to every X-type measure qubit.
\item[(S3--S6)] In step $2+k$, $k=1,\dots,4$, apply $\mathrm{CX}(m\to m+\dX_k)$ for each X-type $m$ with $m+\dX_k\in\cD$, and $\mathrm{CX}(m+\dZ_k\to m)$ for each Z-type $m$ with $m+\dZ_k\in\cD$.
\setcounter{enumi}{6}
\item Apply $H$ to every X-type measure qubit.
\item Measure every measure qubit in the $Z$ basis.
\end{enumerate}
Each qubit takes part in at most one operation per step. The layout and the four CX layers coincide with those of the circuits \texttt{surface\_code:rotated\_memory\_x/z} generated by Stim \cite{Gid21}. The orders $\dX$ and $\dZ$ are the standard ones that orient hook errors perpendicular to the logical operator they could shorten \cite{TS14,FMMC12}.

In the \emph{memory experiment in basis $Z$}, every data qubit is prepared in $|0\rangle$ in step (S1) of round $0$. Rounds $0,\dots,T-1$ follow, for some $T\ge1$, and then all data qubits are measured in the $Z$ basis. Let $s_{m,r}$ be the outcome of $m$ in round $r$ and $f_q$ the final outcome of $q$. For every Z-type $m$ the \emph{detectors} are
\[
D_{m,0}=s_{m,0},\qquad D_{m,r}=s_{m,r}\oplus s_{m,r-1}\ (1\le r\le T-1),\qquad D_{m,T}=s_{m,T-1}\oplus\bigoplus_{q\in N(m)}f_q .
\]
We call $r$ the \emph{layer} of $D_{m,r}$. The logical outcome is $\bigoplus_{q\in\cD,\,y(q)=1}f_q$, the value of $Z_L$ on the bottom row. The experiment in basis $X$ is the same with $|+\rangle$, $X$-basis final measurements, X-type detectors and $X_L$ on the left column $x(q)=1$. Without noise all detectors and the logical outcome equal $0$ (Table~\ref{tab:verify}, V1).

\subsection{Noise}\label{sec:noise}
A \emph{location} is one of the following. Each location fails independently with probability $p$.
\begin{itemize}[leftmargin=2em]
\item A reset or preparation. A failed reset to $|0\rangle$ (preparation of $|+\rangle$) is followed by $X$ (by $Z$).
\item A measurement. A failed measurement reports the flipped outcome.
\item An $H$ gate, or a qubit that is idle during a step. Failure is followed by $X$, $Y$ or $Z$, each with probability $1/3$.
\item A CX gate. Failure is followed by one of the $15$ non-identity two-qubit Paulis, each with probability $1/15$.
\end{itemize}
A qubit is idle in a step if no reset, gate or measurement acts on it. Thus data qubits are idle in steps (S1) (except in round $0$), (S2), (S7), (S8) and in each of (S3)--(S6) in which they have no CX partner. Z-type measure qubits are idle in (S2) and (S7) and in the CX steps without a partner, while X-type measure qubits are idle in the CX steps without a partner. A \emph{fault outcome} is a location together with the Pauli or flip that follows its failure. Its probability is $p\,\pi(f)$ with $\pi(f)\in\{1,\tfrac13,\tfrac1{15}\}$.

\subsection{Decoding graph and decoder}\label{sec:decoder}
We describe basis $Z$. Basis $X$ is the same with the roles of the two types exchanged. Let $V$ be the set of detectors $D_{m,r}$. The \emph{signature} $\sigma(f)\subseteq V$ of a fault outcome $f$ is the set of detectors that change when $f$ is the only failure, and $\ell(f)\in\{0,1\}$ records whether the logical outcome changes. By Lemma~\ref{lem:graphlike}, $|\sigma(f)|\le2$, and $\ell(f)$ depends only on $\sigma(f)$. The \emph{decoding graph} $G$ has vertex set $V\cup\{b_1,b_2\}$ and one edge $e(f)$ for each nonempty signature: $e(f)=\sigma(f)$ if $|\sigma(f)|=2$, and $e(f)=\{u,b_1\}$ or $\{u,b_2\}$ if $\sigma(f)=\{u\}$ and $\ell(f)=1$ or $\ell(f)=0$, respectively. For an edge $e$ put
\[
c_e=\sum_{f:\,e(f)=e}\pi(f),\qquad q_e=c_e\,p .
\]
The weights are $w_e=\log\bigl((1-r_e)/r_e\bigr)$ for numbers $r_e$ with $q_e(1-q_e)\le r_e\le q_e$. Two choices are common: $r_e=q_e$, and $r_e$ equal to the probability that an odd number of outcomes with $e(f)=e$ occur. The second lies in this range by the Bonferroni inequality. For a location $\ell$ let $c_{\ell,e}$ be the sum of $\pi(f)$ over the outcomes $f$ of $\ell$ with $e(f)=e$. We call the multiset of the nonzero numbers $c_{\ell,e}$, over all locations $\ell$, the \emph{profile} of $e$. Because the outcomes of a location exclude each other, the second choice equals $\bigl(1-\prod_\ell(1-2c_{\ell,e}p)\bigr)/2$. Thus both choices depend only on $p$ and on the profile of $e$. We call weights as above \emph{profile weights} if $r_e=\psi(p,\text{profile of }e)$ for one function $\psi$. For $p\le2\times10^{-3}$ each $q_e$ is at most $\tfrac{154}{15}\cdot2\times10^{-3}<0.021$ (Lemma~\ref{lem:graphlike}), so all weights are positive.

For a set $C$ of edges let $\partial C\subseteq V$ be the set of detectors of odd degree in $C$. Given the set $\mathcal A\subseteq V$ of detectors that equal $1$, the decoder returns a set $C$ of minimum weight with $\partial C=\mathcal A$, and it predicts that the logical outcome was flipped if and only if $|C\cap\delta(b_1)|$ is odd, where $\delta(b_1)$ is the set of edges at $b_1$. A minimum-weight perfect matching of $\mathcal A$, with boundary copies and shortest-path distances, yields such a set as the symmetric difference of its paths. We prove the results below for every minimizer $C$. The decoder \emph{fails} if its prediction differs from the actual flip of the logical outcome.

\subsection{Result}
\begin{theorem}\label{thm:main}
Let $d\ge3$ be odd, $T\ge1$, $B\in\{X,Z\}$ and $0<p\le\pst=1.04\times10^{-3}$. Put $\lambda=31\sqrt p$. The memory experiment in basis $B$ with $T$ rounds, decoded as in Section~\ref{sec:decoder}, fails with probability
\[
\Pfail\le \frac{(T+1)(d+1)}{2}\cdot 2\sqrt{\frac{c_{\max}\,p}{1-c_{\max}\,p}}\cdot\frac{\lambda^{d-1}}{1-\lambda}
\le 0.104\,(T+1)(d+1)\,\frac{\lambda^{d}}{1-\lambda},\qquad c_{\max}=\tfrac{154}{15}.
\]
\end{theorem}

We call $\Pfail/T$ the logical error rate per round of the memory experiment in basis $B$. Since $T+1\le2T$, it obeys $\Pfail/T\le0.208\,(d+1)\lambda^d/(1-\lambda)$ uniformly in $T$. For $p\le\pst$ we have $\lambda\le0.99972$, so this decays exponentially in $d$. For example, at $p=10^{-3}$, where $\lambda=0.98031$, the bound reads $\Pfail/T\le10.6\,(d+1)\,\lambda^d$, and at $p=10^{-4}$ it reads $0.31\,(d+1)\,(0.31)^d$. The bound on $\Pfail/T$ is below $1$ for all $d\ge3$ when $p\le5\times10^{-4}$, for $d\ge423$ when $p=10^{-3}$, but only for $d\ge63063$ when $p=\pst$.

\begin{theorem}\label{thm:refined}
In the setting of Theorem~\ref{thm:main}:
\begin{enumerate}[label=\textup{(\alph*)}]
\item if $0<p\le1.6\times10^{-3}$ and $\lambda=0.997\,\bigl(p/(1.6\times10^{-3})\bigr)^{21/50}$, then
\[
\Pfail\le 0.032\,(T+1)(d+1)\,\frac{\lambda^{d}}{1-\lambda};
\]
\item if the weights are profile weights, $0<p\le p_{\ast\ast}=2\times10^{-3}$ and $\lambda=0.999\,(p/p_{\ast\ast})^{9/25}$, then
\[
\Pfail\le 0.061\,(T+1)(d+1)\,\frac{\lambda^{d}}{1-\lambda}.
\]
\end{enumerate}
\end{theorem}

Part (b) implies $\Pfail/T\le0.122\,(d+1)\lambda^d/(1-\lambda)$, and $\lambda\le0.999$ for $p\le p_{\ast\ast}$. At $p=10^{-3}$ we have $\lambda<0.7784$, and the bound on $\Pfail/T$ is at most $0.551\,(d+1)\,(0.7784)^d$, which is below $1$ for all $d\ge5$ and below $10^{-6}$ for $d\ge71$. Part (a), at $p=10^{-3}$, gives $\lambda<0.8185$ and $\Pfail/T\le0.353\,(d+1)\,(0.8185)^d$. But for $p<1.92\times10^{-4}$ the rate $31\sqrt p$ of Theorem~\ref{thm:main} is smaller than that of part (b).

The circuit of Section~\ref{sec:circuit} has eight steps per round. A common leaner schedule measures and resets the measure qubits in a single step and prepares and measures the X-type ones in the $X$ basis directly (Section~\ref{sec:lean}). It has fewer idle steps, and the same two arguments yield larger thresholds.

\begin{theorem}\label{thm:lean}
For the lean schedule of Section~\ref{sec:lean}, with the noise model, memory experiments and decoder of Sections~\ref{sec:noise} and~\ref{sec:decoder}, let $d\ge3$ be odd, $T\ge1$ and $B\in\{X,Z\}$.
\begin{enumerate}[label=\textup{(\alph*)}]
\item If $0<p\le1.53\times10^{-3}$ and $\lambda=25.55\sqrt p$, then
\[
\Pfail\le0.0985\,(T+1)(d+1)\,\frac{\lambda^d}{1-\lambda}.
\]
\item If $0<p\le2.4\times10^{-3}$ and $\lambda=0.997\,\bigl(p/(2.4\times10^{-3})\bigr)^{21/50}$, then
\[
\Pfail\le0.028\,(T+1)(d+1)\,\frac{\lambda^d}{1-\lambda}.
\]
\item If the weights are profile weights, $0<p\le3\times10^{-3}$ and $\lambda=0.997\,\bigl(p/(3\times10^{-3})\bigr)^{9/25}$, then
\[
\Pfail\le0.052\,(T+1)(d+1)\,\frac{\lambda^d}{1-\lambda}.
\]
\end{enumerate}
\end{theorem}

At $p=10^{-3}$, part (c) gives $\lambda<0.6714$, and the bound on $\Pfail/T$ is below $0.39$ for all $d\ge3$ and below $10^{-6}$ for $d\ge43$.

Section~\ref{sec:hetero} extends both arguments to error rates that depend on the type of operation (Theorem~\ref{thm:hetero}) and applies them to error models built from the published component error rates of six devices. Three models are certified: those of the Quantinuum Helios and H2 data sheets, and one with the error rates of IBM's Heron~r3 processor ibm\_boston on a square grid. However, the models of Google's and USTC's processors are not certified. For them, floating-point estimates indicate that no positive potential satisfies the inequalities of Lemma~\ref{lem:memory} with $\lambda<1$.

\subsection*{Relation to earlier work}
Dennis, Kitaev, Landahl and Preskill reduced matching failure to self-avoiding walks and proved a threshold of $1.14\%$ for independent qubit and measurement errors, and of $1.7\times10^{-4}$ per qubit and time step for the toric code with a CNOT syndrome-extraction circuit and worst-case Pauli faults, assuming that classical decoding takes one time step \cite{DKLP02}. Fowler proved $7.4\times10^{-4}$ for the planar code with nearest-neighbour circuits and unit weights \cite{Fow12}, using the bound $14p/5$ on line probabilities of the circuits of \cite{WFH11}. General threshold theorems for local stochastic noise cover concatenated codes \cite{AGP06} and low-density parity-check codes \cite{KP13,Got14}, and finite thresholds have recently been proved for the union-find and greedy decoders of the surface code under circuit-level local stochastic noise \cite{YLY26}. We keep the path reduction of \cite{DKLP02} but replace the path count by the local criterion of Section~\ref{sec:criterion}, applied to the exact edge probabilities of the circuit. For Theorem~\ref{thm:refined} we also use the minimality of the correction along the path, beyond the half-weight inequality of \cite{DKLP02}, and for part (b) a canonical choice among the minimum-weight corrections. For the circuit considered here, Fowler's argument gives $4.3\times10^{-4}$ (Remark~\ref{rem:fowler}), so Theorems~\ref{thm:main} and~\ref{thm:refined} improve the rigorous value for this circuit by factors of about $2.4$ and $4.6$.

\subsection*{Outline}
Section~\ref{sec:graph} describes the decoding graph: each fault outcome produces one edge, the bulk has twelve edges per node, and the graph has $29$ node types in each sector. In Section~\ref{sec:paths} we reduce failure to weighted paths from $b_1$ to $b_2$, following \cite{DKLP02}. We prove the local criterion in Section~\ref{sec:criterion} and combine the pieces into Theorem~\ref{thm:main} in Section~\ref{sec:proof}. Section~\ref{sec:refined} proves Theorem~\ref{thm:refined}, Section~\ref{sec:lean} treats the lean schedule, and Section~\ref{sec:hetero} treats non-uniform error rates. Computer-verified statements carry the mark ${}^\dagger$ and are collected in Tables~\ref{tab:verify}--\ref{tab:verify4}. Section~\ref{sec:lean4} describes the formal proofs in Lean~4.

\section{The decoding graph}\label{sec:graph}

We write $G_{d,T}$ for the decoding graph of the experiment with distance $d$ and $T$ rounds, in basis $Z$ or $X$. The \emph{height} of a detector $D_{m,r}$ is the second coordinate $y$ of $m$ in basis $Z$ and the first coordinate $x$ in basis $X$.

\begin{lemma}[\ver]\label{lem:graphlike}
For $B\in\{X,Z\}$, odd $d\le13$ and $T\le7$ the following hold.
\begin{enumerate}[label=\textup{(\alph*)}]
\item Every fault outcome flips at most two detectors.
\item Outcomes with the same signature have the same value of $\ell$, and $\ell(f)=1$ only if $|\sigma(f)|=1$.
\item The edges at $b_1$ join it to detectors of height $2$, and the edges at $b_2$ join it to detectors of height $2d-2$. No detector is adjacent to both.
\item The heights of the two ends of an edge in $V$ differ by at most $2$.
\item $b_1$ has exactly $(T+1)(d+1)/2$ neighbours, and $c_e\le154/15$ for every edge $e$.
\end{enumerate}
\end{lemma}

Part (a) says that the circuit-level noise decomposes into a graph in each sector. Here each $Y$ component splits into its $X$ part, seen by Z-type detectors, and its $Z$ part, seen by X-type detectors. Lemma~\ref{lem:locality} below will show that Lemma~\ref{lem:graphlike} holds for all odd $d\ge3$ and all $T\ge1$.

\subsection{The bulk}
Let $m$ be a Z-type measure qubit far from the boundary and $1\le r\le T-1$ far from $0$ and $T$. Then the data qubit $m+\dZ_k$ meets $m$ in step $2+k$. There are two kinds of data qubits. A data qubit $q$ of kind~A has Z-type neighbours $q\mp(1,1)$, which it meets in steps (S3) and (S6), and X-type neighbours $q+(1,-1)$, $q+(-1,1)$, which it meets in (S4) and (S5). A data qubit of kind~B has Z-type neighbours $q+(-1,1)$, $q+(1,-1)$, met in (S4) and (S5), and X-type neighbours $q\mp(1,1)$, met in (S3) and (S6).

\begin{lemma}\label{lem:bulk}
In basis $Z$, a bulk detector $v=D_{m,r}$ has exactly twelve edges. Their other ends, written as offsets $(\Delta x,\Delta y,\Delta r)$, and their coefficients are
\[
\begin{array}{c|cccccc}
\text{offset} & \pm(2,-2,0) & \pm(0,0,1) & \pm(2,2,0) & \pm(2,2,-1) & \pm(2,-2,-1) & \pm(4,0,-1)\\\hline
15\,c_e & 72 & 66 & 48 & 16 & 8 & 8
\end{array}
\]
In basis $X$ the coefficients are the same, with offsets $\pm(2,-2,0)$, $\pm(0,0,1)$, $\pm(2,2,0)$, $\pm(2,2,-1)$, $\pm(2,-2,1)$ and $\pm(0,4,-1)$.
\end{lemma}

\begin{proof}
We treat basis $Z$, where only $X$ components matter, and list the outcomes that produce each edge in Table~\ref{tab:bulk}, in units of $p/15$. Three propagation rules determine the list. First, a CX copies an $X$ on its control to its target. Second, an $X$ on the target of a CX is not copied. Third, an $X$ on an X-type measure qubit before its first CX acts trivially, because that qubit is in $|+\rangle$ at that point. By the first rule, an $X$ on such a qubit between its $k$-th and $(k+1)$-st CX is copied onto its remaining data qubits. For $k=1$ this equals an $X$ on its first data qubit, for $k=2$ it is the hook pair, and for $k=3$ it is an $X$ on its last data qubit.

An $X$ on a data qubit $q$ changes the next outcome of each Z-type neighbour that has not yet met $q$ in the current round, and the outcome in the next round of each neighbour that has. Hence an $X$ on a kind-A qubit between (S6) of round $r-1$ and (S3) of round $r$ flips its two neighbours in layer $r$, and it produces the edge with offset $(2,2,0)$. An $X$ between (S3) and (S6) of round $r$ flips $q+(1,1)$ in layer $r$ and $q-(1,1)$ in layer $r+1$, and it gives the offset $(-2,-2,1)$. Similarly, for kind~B the windows are (S5) of round $r-1$ to (S4) of round $r$, with offset $(2,-2,0)$, and (S4) to (S5), with offset $(-2,2,1)$. The hook pair of an X-type measure qubit $m'$ is $\{m'+(1,-1),m'+(-1,-1)\}$. It flips $m'+(2,0)$ in layer $r$ and $m'+(-2,0)$ in layer $r+1$, while the flips of $m'+(0,-2)$ cancel, which leads to the offset $(-4,0,1)$. Finally, an $X$ on the Z-type qubit $m$ after its reset changes $s_{m,r}$ only, which gives the offset $(0,0,1)$. Applying these rules to all locations in the neighbourhood, we obtain the entries of Table~\ref{tab:bulk}. For a CX we record which of the $15$ outcomes contribute, as pairs (control part, target part).

The same derivation with $Z$ components yields the offsets and coefficients stated for basis $X$.
\end{proof}

\begin{table}[ht]
\centering\small
\begin{tabular}{@{}l>{\raggedright\arraybackslash}p{0.66\textwidth}r@{}}
\toprule
edge & contributing outcomes (units of $p/15$) & $15c_e$\\
\midrule
$(0,0,\pm1)$ & reset flip $15$; idle in (S2) $10$; each of the $4$ CX: $(I/Z,X/Y)$ on (data, $m$) $4$; idle in (S7) $10$; measurement flip $15$ & $66$\\
$\pm(2,2,0)$ & kind A, $q$: CX in (S6) of round $r-1$, $(X/Y,I/Z)$ $4$; idles in (S7), (S8), (S1), (S2) $4\times10$; CX in (S3), $(X/Y,X/Y)$ $4$ & $48$\\
$\pm(2,-2,0)$ & kind B, $q$: CX in (S5) of round $r-1$, $(X/Y,I/Z)$ $4$; X-type $q+(1,1)$ in (S5) of round $r-1$, $(X/Y,I/Z)$ $4$; its CX onto $q$ in (S6), $X/Y$ on $q$ $8$; idles $4\times10$; X-type $q-(1,1)$: CX onto $q$ in (S3), $(I/Z,X/Y)$ and $(X/Y,I/Z)$ $8$, its CX in (S4), $(X/Y,X/Y)$ $4$; CX $q\to q+(-1,1)$ in (S4), $(X/Y,X/Y)$ $4$ & $72$\\
$\pm(2,2,-1)$ & kind A, $q$ between (S3) and (S6): CX in (S3) $(X/Y,I/Z)$ $4$; CX onto $q$ in (S4) and (S5), $(I/Z,X/Y)$ $4+4$; CX in (S6) $(X/Y,X/Y)$ $4$ & $16$\\
$\pm(2,-2,-1)$ & kind B, $q$ between (S4) and (S5): CX in (S4) $(X/Y,I/Z)$ $4$; CX in (S5) $(X/Y,X/Y)$ $4$ & $8$\\
$\pm(4,0,-1)$ & X-type $m'$ after (S4): its CX in (S4) $(X/Y,I/Z)$ $4$; its CX in (S5) $(X/Y,X/Y)$ $4$ & $8$\\
\bottomrule
\end{tabular}
\caption{Outcomes producing the twelve edges at a bulk detector (basis $Z$, Lemma~\ref{lem:bulk}). The kind-A and kind-B qubits are the data qubits shared by the two ends of the edge.}
\label{tab:bulk}
\end{table}

\subsection{Locality and node types}
The \emph{type} of a detector $v\in V$ is the multiset of pairs (offset of the other end, $c_e$) over the edges $e$ at $v$, where an edge to $b_1$ or $b_2$ is recorded with the label $b_1$ or $b_2$ in place of the offset.

\begin{lemma}\label{lem:locality}
Let $v=D_{m,r}$.
\begin{enumerate}[label=\textup{(\alph*)}]
\item If $v\in\sigma(f)$, then $f$ acts on a qubit at $\ell^\infty$-distance at most $2$ from $m$, in round $r-1$ or $r$ \textup{(}in round $T-1$ or in the final measurement if $r=T$\textup{)}.
\item The type of $v$ is determined by the positions of the qubits at $\ell^\infty$-distance at most $6$ from $m$ and the X or Z types of the measure qubits among them, by $\min(r,2)$ and by $\min(T-r,2)$.
\item For all odd $d\ge3$ and all $T\ge1$, every detector of $G_{d,T}$ has the type of a detector of $G_{d',T'}$ for some $d'\in\{3,5,7,9\}$ and $T'\in\{1,\dots,5\}$. The same reduction applies to the statements of Lemma~\ref{lem:graphlike}.
\end{enumerate}
\end{lemma}

\begin{proof}
(a) We use the propagation rules from the proof of Lemma~\ref{lem:bulk}. In basis $Z$ only $X$ components matter, and basis $X$ is the same with $Z$ components and the roles of the two types of measure qubits exchanged. An $X$ on a data qubit $q$ is copied by the gate $\mathrm{CX}(q\to m')$ onto each Z-type measure qubit $m'$ with $q\in N(m')$, where it flips the outcome of $m'$ and is removed by the next reset of $m'$. It is copied nowhere else, because $q$ is the target of its CX gates with X-type measure qubits. An $X$ on a Z-type measure qubit flips its outcome and is removed by the next reset, whereas an $X$ on an X-type measure qubit $m'$ is copied onto the data qubits of $N(m')$ that $m'$ meets later in the same round. The latter does not change the outcome of $m'$, and it is removed by the next reset. Hence the propagated $X$ part of a single-qubit outcome lies, on data qubits, within distance $1$ of the faulty qubit, and the detectors it flips lie within distance $2$ of it. A two-qubit outcome is the product of its two factors, and detector values are linear in the Pauli frame. In time, a measure qubit is reset at the start of each round, and a data error that is present from round $\rho$ on changes $s_{m',\rho'}$ for all $\rho'\ge\rho$ or for all $\rho'\ge\rho+1$, so it flips layers $\rho$ and $\rho+1$ only. The final layer compares the last round with the data measurement, which sees the same error.

(b) By (a), the outcomes with $v$ in their signature act within distance $2$ of $m$, so their CX partners lie within distance $3$. By the rules in (a), the signature and the logical effect of such an outcome in round $\rho$ are determined by the steps at which CX gates act, in rounds $\rho$ and $\rho+1$, on its qubits, on the data qubits within distance $1$ of them and on the measure qubits adjacent to those. Hence all of these qubits lie within distance $5$ of $m$. Which gates act on a qubit, and in which step, depends only on which of its diagonal neighbours exist, and these lie within distance $6$ of $m$. Whether round $r-1$ is round $0$, and whether layer $r$ or $r+1$ is the final one, is recorded by $\min(r,2)$ and $\min(T-r,2)$.

(c) The bulk pattern of qubit positions and measure-qubit types is invariant under the lattice generated by $(4,0)$, $(0,4)$ and $(2,2)$, and the measure qubits of each of the two types form a single coset of it. Along the side $y=0$ the X-type measure qubits sit at $x\equiv2\pmod4$, along $y=2d$ at $x\equiv0$, along $x=0$ the Z-type ones sit at $y\equiv0$ and along $x=2d$ at $y\equiv2\pmod 4$. For odd $d$ this pattern, measured from the nearest corner, does not depend on $d$. Hence, for a detector in a given basis, the configuration within distance $6$ of $m$ is determined by the distances from $m$ to the four sides, truncated at $7$. If $d\ge9$, each quadruple of truncated distances that occurs in $G_{d,T}$ also occurs in $G_{9,T}$. Indeed, the range $[7,11]$ of coordinates at distance at least $7$ from both opposite sides of $G_9$ contains the even coordinates $8$ and $10$, one of each residue modulo $4$, so the parity condition that makes $m$ X-type or Z-type can be met there. Likewise, for $T\ge5$ the layer data $(\min(r,2),\min(T-r,2))$ of all layers occur for $T'=5$. Part (b) then implies the claim for the types of detectors. The statements of Lemma~\ref{lem:graphlike} concern single outcomes, edges and the neighbours of $b_1$, and they reduce in the same way. For the logical effect, after round $\rho+1$ the propagated frame of an outcome in round $\rho$ no longer changes on the data qubits, so $\ell(f)$ is the parity of its $X$ part on the bottom row at that time, which is again determined locally. An outcome with empty signature is handled in the same way, with the configuration around the outcome in place of the configuration around a detector. Finally, the number of neighbours of $b_1$ is a sum over detectors. By the types, a detector is adjacent to $b_1$ exactly when it has height $2$, and each layer has $(d+1)/2$ detectors of height $2$.
\end{proof}

\begin{corollary}[\ver]\label{cor:types}
In each basis the detectors of all graphs $G_{d,T}$, $d\ge3$ odd and $T\ge1$, have exactly $29$ types. They are listed in Appendix~\ref{app:types}.
\end{corollary}

\section{From matching failure to weighted paths}\label{sec:paths}

Fix an experiment and let $\cF$ be the set of fault outcomes that occur. At most one outcome occurs per location. Let $E$ be the set of edges $e$ such that the number of $f\in\cF$ with $e(f)=e$ is odd. Since detector values are linear in the Pauli frame, the set of detectors equal to $1$ is $\partial E$. The logical outcome is linear in the Pauli frame as well, and by Lemma~\ref{lem:graphlike}(b) an outcome flips it if and only if its edge ends at $b_1$. Therefore the logical outcome flips if and only if $|E\cap\delta(b_1)|$ is odd.

\begin{lemma}\label{lem:path}
If the decoder fails with the minimizer $C$, then $E\triangle C$ contains a simple path from $b_1$ to $b_2$.
\end{lemma}

\begin{proof}
Let $R=E\triangle C$. Since $\partial C=\partial E$, each detector has even degree in $R$. Failure means that $|C\cap\delta(b_1)|$ and $|E\cap\delta(b_1)|$ have different parity, so $b_1$ has odd degree in $R$. As the degrees in $R$ sum to $2|R|$, the vertex $b_2$ has odd degree as well. In each connected component of $(V\cup\{b_1,b_2\},R)$ the number of odd-degree vertices is even. Hence $b_1$ and $b_2$ lie in the same component, and that component contains a simple path between them.
\end{proof}

\begin{lemma}\label{lem:length}
Every simple path from $b_1$ to $b_2$ in $G_{d,T}$ has at least $d$ edges.
\end{lemma}

\begin{proof}
By Lemma~\ref{lem:graphlike}(c,d), the path enters $V$ at height $2$, leaves it from height $2d-2$, and each of its edges inside $V$ changes the height by at most $2$. Thus it has at least $(2d-4)/2=d-2$ edges inside $V$, and two edges at the boundary vertices.
\end{proof}

\begin{lemma}\label{lem:half}
Let $\gamma\subseteq E\triangle C$ be a simple path from $b_1$ to $b_2$. Then $w(\gamma\cap E)\ge w(\gamma)/2$.
\end{lemma}

\begin{proof}
We follow the argument of \cite[Sec.~4]{DKLP02}. Because the detector boundary of $\gamma$ is empty, $C\triangle\gamma$ is also a valid output, and $w(C)\le w(C\triangle\gamma)=w(C)-w(C\cap\gamma)+w(\gamma\setminus C)$. Since $\gamma\subseteq E\triangle C$, we have $\gamma\setminus C=\gamma\cap E$ and $w(C\cap\gamma)=w(\gamma)-w(\gamma\cap E)$.
\end{proof}

\begin{lemma}\label{lem:prob}
For every set $S$ of edges, $\Pr(S\subseteq E)\le\prod_{e\in S}q_e$.
\end{lemma}

\begin{proof}
If $S\subseteq E$, then for each $e\in S$ some $f_e\in\cF$ has $e(f_e)=e$. The $f_e$ are distinct, because each outcome has one edge. Two distinct outcomes at the same location never occur together, while outcomes at distinct locations are independent. Hence
\[
\Pr(S\subseteq E)\le\sum_{(f_e)_{e\in S}}\Pr(f_e\in\cF\ \forall e)\le\sum_{(f_e)_{e\in S}}\ \prod_{e\in S}p\,\pi(f_e)=\prod_{e\in S}q_e.\qedhere
\]
\end{proof}

\begin{lemma}\label{lem:tilt}
Put $a_e=2\sqrt{q_e/(1-q_e)}$. For every path $\gamma$,
\[
\sum_{S\subseteq\gamma,\ w(S)\ge w(\gamma)/2}\ \prod_{e\in S}q_e\ \le\ \prod_{e\in\gamma}a_e .
\]
\end{lemma}

\begin{proof}
Each term on the left satisfies $w(S)-w(\gamma\setminus S)\ge0$, so it is at most $\prod_{e\in S}q_e\,e^{(w(S)-w(\gamma\setminus S))/2}$. Summing this over all $S\subseteq\gamma$, we obtain $\prod_{e\in\gamma}\bigl(q_e e^{w_e/2}+e^{-w_e/2}\bigr)$. With $e^{w_e}=(1-r_e)/r_e$ and $q_e(1-q_e)\le r_e\le q_e$ we get
\[
q_e\sqrt{\frac{1-r_e}{r_e}}\le\frac{q_e}{\sqrt{q_e(1-q_e)}}=\sqrt{\frac{q_e}{1-q_e}},\qquad \sqrt{\frac{r_e}{1-r_e}}\le\sqrt{\frac{q_e}{1-q_e}},
\]
so each factor is at most $a_e$.
\end{proof}

\begin{proposition}\label{prop:sum}
Let $\Gamma$ be the set of simple paths from $b_1$ to $b_2$ in $G_{d,T}$. Then $\Pfail\le\sum_{\gamma\in\Gamma}\prod_{e\in\gamma}a_e$.
\end{proposition}

\begin{proof}
By Lemmas~\ref{lem:path} and~\ref{lem:half}, failure implies that some $\gamma\in\Gamma$ and $S=\gamma\cap E$ satisfy $S\subseteq E$ and $w(S)\ge w(\gamma)/2$. We apply the union bound over $\gamma$ and $S$, then Lemmas~\ref{lem:prob} and~\ref{lem:tilt}.
\end{proof}

\section{A local criterion for non-backtracking walks}\label{sec:criterion}

\begin{lemma}\label{lem:criterion}
Let $G$ be a finite graph with vertex set $V\cup\{b_1,b_2\}$, without an edge between $b_1$ and $b_2$, and let $a_e>0$ for each edge $e$. Let $\lambda>0$ and suppose that
\[
\Sigma(v):=\sum_{e\ni v}\frac{a_e}{\lambda+a_e}\le1\qquad\text{for every }v\in V,
\]
where the sum includes edges to $b_1$ and $b_2$. Put $\kappa=\lambda+\max_{e\ni b_2}a_e$ and $\Sigma(b_1)=\sum_{e\ni b_1}a_e/(\lambda+a_e)$. Then for every $L\ge2$ the simple paths from $b_1$ to $b_2$ with $L$ edges satisfy
\[
\sum_{\gamma}\ \prod_{e\in\gamma}a_e\ \le\ \kappa\,\Sigma(b_1)\,\lambda^{L-1}.
\]
\end{lemma}

\begin{proof}
For an oriented edge $\varepsilon=(u\to v)$ put $h(\varepsilon)=1/(\lambda+a_\varepsilon)$. For $m\ge1$ and an oriented edge $(x_0\to x_1)$ with $x_0\in V\cup\{b_1\}$ and $x_1\in V$, let $W_m(x_0\to x_1)$ be the sum of $\prod_{i=1}^{m}a_{x_ix_{i+1}}$ over all walks $x_1,x_2,\dots,x_{m+1}$ with $x_{m+1}=b_2$, $x_2,\dots,x_m\in V$, consecutive vertices adjacent and $x_{i+1}\ne x_{i-1}$ for $1\le i\le m$. We show by induction on $m$ that
\begin{equation}\label{eq:induction}
W_m(x_0\to x_1)\le\kappa\,\lambda^{m}\,h(x_0\to x_1).
\end{equation}
Because the edge $\{x_0,x_1\}$ contributes $a_{x_0x_1}/(\lambda+a_{x_0x_1})$ to $\Sigma(x_1)$, the hypothesis implies
\begin{equation}\label{eq:local}
\sum_{e\ni x_1,\ e\ne\{x_0,x_1\}}\frac{a_e}{\lambda+a_e}\le1-\frac{a_{x_0x_1}}{\lambda+a_{x_0x_1}}=\lambda\,h(x_0\to x_1).
\end{equation}
For $m=1$, $W_1(x_0\to x_1)=a_{x_1b_2}$ if $x_1$ is adjacent to $b_2$ and $0$ otherwise. Since $a_{x_1b_2}=(\lambda+a_{x_1b_2})\cdot a_{x_1b_2}/(\lambda+a_{x_1b_2})\le\kappa\,a_{x_1b_2}/(\lambda+a_{x_1b_2})$, \eqref{eq:induction} follows from \eqref{eq:local}. For $m\ge2$,
\[
W_m(x_0\to x_1)=\sum_{\substack{x_2\in V\setminus\{x_0\}\\ x_2\sim x_1}}a_{x_1x_2}W_{m-1}(x_1\to x_2)\le\kappa\lambda^{m-1}\sum_{x_2}\frac{a_{x_1x_2}}{\lambda+a_{x_1x_2}}\le\kappa\lambda^{m}h(x_0\to x_1),
\]
by induction and \eqref{eq:local}. A simple path $b_1,x_1,\dots,x_{L-1},b_2$ is a walk of this kind, so the sum in the lemma is at most $\sum_{x_1\sim b_1}a_{b_1x_1}W_{L-1}(b_1\to x_1)\le\kappa\lambda^{L-1}\Sigma(b_1)$.
\end{proof}

On the $k$-regular tree with all $a_e=a$ the criterion reads $ka/(\lambda+a)\le1$, that is $\lambda\ge(k-1)a$. Since this is the exact growth rate of non-backtracking walks there, the criterion is sharp on trees. On a lattice with unequal edges it gives the growth rate of weighted non-backtracking walks exactly: if all nodes have the same multiset $\{a_e\}$ and $\Sigma\equiv1$, then $h$ is a positive eigenvector of the weighted non-backtracking operator with eigenvalue $\lambda$.

\section{Proof of Theorem~\ref{thm:main}}\label{sec:proof}

\subsection{The criterion holds at every detector}
Let $\lambda=31\sqrt p$ and write $a_e=\sqrt p\,\alpha_e(p)$ with $\alpha_e(p)=2\sqrt{c_e/(1-c_ep)}$. Then
\[
\Sigma(v)=\sum_{e\ni v}\frac{\alpha_e(p)}{31+\alpha_e(p)},
\]
which increases with $p$. Thus it suffices to check $\Sigma(v)\le1$ at $p=\pst$. There $31\sqrt{\pst}=0.999719\ldots\ge0.9997$, and $\Sigma(v)$ decreases in $\lambda$, so it suffices to check
\begin{equation}\label{eq:check}
\sum_{e\ni v}\frac{a_e}{0.9997+a_e}\le1\qquad\text{at }p=\pst .
\end{equation}
By Corollary~\ref{cor:types} we need to check only $29$ types per basis. For the bulk type of Lemma~\ref{lem:bulk} the computation is short:
\[
\begin{array}{c|ccccc}
15\,c_e & 72 & 66 & 48 & 16 & 8\\
\text{multiplicity} & 2 & 2 & 2 & 2 & 4\\\hline
a_e & 0.141662 & 0.135603 & 0.115570 & 0.066650 & 0.047116\\
a_e/(0.9997+a_e) & 0.124117 & 0.119442 & 0.103625 & 0.062503 & 0.045009
\end{array}
\]
and the weighted sum is $0.999409$. The other $28$ types satisfy \eqref{eq:check} with left side at most $0.9629$${}^\dagger$. We list the values for all types in Appendix~\ref{app:types}. The check is done in exact rational arithmetic, with rational upper bounds for the square roots (Table~\ref{tab:verify}, V6).

\subsection{Assembly}
We first check that the graph $G_{d,T}$ satisfies the hypotheses of Lemma~\ref{lem:criterion}. Each edge comes from a nonempty signature, which contains a detector, so there is no edge between $b_1$ and $b_2$. Since there is one edge per signature, there are no parallel edges, and the number of edges at $b_1$ equals the number of its neighbours. Combining Proposition~\ref{prop:sum}, Lemma~\ref{lem:length} and Lemma~\ref{lem:criterion}, we obtain
\[
\Pfail\le\sum_{L\ge d}\kappa\,\Sigma(b_1)\,\lambda^{L-1}=\kappa\,\Sigma(b_1)\frac{\lambda^{d-1}}{1-\lambda}.
\]
Let $a_{\max}=2\sqrt{c_{\max}p/(1-c_{\max}p)}$. By Lemma~\ref{lem:graphlike}(e), $\kappa\le\lambda+a_{\max}$ and each term of $\Sigma(b_1)$ is at most $a_{\max}/(\lambda+a_{\max})$, so $\kappa\,\Sigma(b_1)\le\tfrac{(T+1)(d+1)}{2}\,a_{\max}$. This is the first bound of the theorem. For $p\le\pst$ we have $1-c_{\max}p\ge0.98932$ and $a_{\max}\le6.4429\sqrt p$, so
\begin{align*}
\Pfail&\le\frac{(T+1)(d+1)}{2}\cdot6.4429\sqrt p\cdot\frac{\lambda^{d-1}}{1-\lambda}\\
&=\frac{6.4429}{62}\,(T+1)(d+1)\frac{\lambda^{d}}{1-\lambda}\le0.104\,(T+1)(d+1)\frac{\lambda^d}{1-\lambda}.\qquad\qed
\end{align*}

\section{Proof of Theorem~\ref{thm:refined}}\label{sec:refined}

In the proof of Theorem~\ref{thm:main} we sum over all ways of labelling the edges of a path as errors or corrections, although most of these labellings cannot occur. Indeed, the correction edges on a stretch of the failure path belong to a minimum-weight correction. Their weight is therefore at most that of the error edges on the stretch plus any detour between its ends, and at most that of any set of edges with the same boundary. We turn these two inequalities into local exclusion rules (Definition~\ref{def:excluded}) and count only the labelled paths that obey them. For profile weights a third rule uses the freedom in the choice of the minimizer: among the minimizers for which the decoder fails we take one that minimizes a fixed linear functional, and such a minimizer cannot turn a corner around which an equally heavy route of smaller value exists. These rules are the main new ingredient of the proof. For part (a) we fix $p_{\ast\ast}=1/625$ and the tilt $s=21/50$, and for part (b) $p_{\ast\ast}=1/500$ and $s=9/25$.

\subsection{Windows}
For a path or walk $P$ we write $c(P)=\prod_{e\in P}c_e$, with multiplicity, and $G/B$ for the graph obtained from $G$ by identifying $b_1$ and $b_2$ to a single vertex $B$. Let $C$ be a minimizer and $\gamma\subseteq E\triangle C$ the path of Lemma~\ref{lem:path}. A \emph{window} is a sub-path $\sigma$ of $\gamma$. We write $\sigma_C=\sigma\cap C$ and $\sigma_E=\sigma\cap E$, so that $\sigma$ is the disjoint union of $\sigma_C$ and $\sigma_E$.

\begin{lemma}\label{lem:window}
\begin{enumerate}[label=\textup{(\alph*)}]
\item For every window $\sigma$ and every set $P'$ of edges of $G/B$ with the same detector boundary as $\sigma$, $w(\sigma_C)-w(\sigma_E)\le w(P')$.
\item For every $X\subseteq C$ and every set $P'$ of edges of $G/B$ with the same detector boundary as $X$, $w(X)\le w(P')$.
\end{enumerate}
\end{lemma}

\begin{proof}
(a) The set $C'=C\triangle\sigma\triangle P'$ satisfies $\partial C'=\partial C$. Since $C\triangle\sigma=(C\setminus\sigma_C)\cup\sigma_E$, we have $w(C')\le w(C)-w(\sigma_C)+w(\sigma_E)+w(P')$, and $w(C)\le w(C')$.

(b) Similarly, the set $C'=C\triangle X\triangle P'$ satisfies $\partial C'=\partial C$ and $w(C')\le w(C)-w(X)+w(P')$, and $w(C)\le w(C')$.
\end{proof}

For a detector $D_{m,r}$ with $m=(x,y)$ put $\phi(D_{m,r})=x+9y+81r$, and for a set $C$ of edges let $\Phi(C)$ be the sum of $\phi(u)+\phi(v)$ over the edges $\{u,v\}$ of $C$ with $u,v\in V$.

A \emph{labelled window} is a path $\sigma=(v_0,\dots,v_m)$ in $G$ with $2\le m\le4$ and a label $\mathsf E$ or $\mathsf C$ on each edge. We write $n_C$ and $n_E$ for the numbers of its $\mathsf C$- and $\mathsf E$-edges, $\sigma_C$ and $\sigma_E$ for the sets of these edges, and $T(\sigma)$ for the set of detectors of odd degree in $\sigma_C$. The \emph{head} of $\sigma$ is $v_{m-1}$. The \emph{ball} of a detector $v$ is the set of detectors joined to $v$ by a chain of at most four edges between detectors. Since the detectors of $\sigma$ lie within three such edges of its head, they belong to the ball of the head. An \emph{admissible walk} for $\sigma$ is a walk in $G/B$, with $b_1$ and $b_2$ read as $B$, that visits $B$ at most once and whose detectors all lie in the ball of the head.

\begin{definition}\label{def:excluded}
A labelled window $\sigma$ is \emph{excluded} if it satisfies one of the following conditions.
\begin{enumerate}[leftmargin=2.8em]
\item[\textup{(M)}] There is an admissible walk $P'$ from $v_0$ to $v_m$ with $h'$ edges, empty if $v_0,v_m\in\{b_1,b_2\}$, such that $k=n_C-n_E-h'\ge0$ and
\begin{equation}\label{eq:excluded}
\Bigl(\frac{1}{p_{\ast\ast}}\Bigr)^{k}\frac{c(\sigma_E)\,c(P')}{c(\sigma_C)}>\prod_{e\in\sigma}\frac{1}{1-c_e\,p_{\ast\ast}}\cdot\Bigl(\frac{1}{1-c_{\max}\,p_{\ast\ast}}\Bigr)^{h'}.
\end{equation}
\item[\textup{(J)}] There are admissible walks, each from a vertex of $T(\sigma)$ to another vertex of $T(\sigma)$ or to $B$, such that each vertex of $T(\sigma)$ is an end of exactly one of them, their union $P'$ has $h'$ edges counted with multiplicity, $k=n_C-h'\ge0$ and
\begin{equation}\label{eq:excludedJ}
\Bigl(\frac{1}{p_{\ast\ast}}\Bigr)^{k}\frac{c(P')}{c(\sigma_C)}>\prod_{e\in\sigma_C}\frac{1}{1-c_e\,p_{\ast\ast}}\cdot\Bigl(\frac{1}{1-c_{\max}\,p_{\ast\ast}}\Bigr)^{h'}.
\end{equation}
If $T(\sigma)$ is empty, $P'$ is empty.
\item[\textup{(S)}] (Only for Theorems~\ref{thm:refined}(b) and~\ref{thm:lean}(c).) The window has $m=2$, its vertices $u=v_0$, $b=v_1$ and $w=v_2$ are detectors, both of its edges carry the label $\mathsf C$, and some detector $x\notin\{u,b,w\}$ is adjacent to $u$ and to $w$, with $\phi(x)<\phi(b)$, such that the profiles of $ux$ and $xw$ are those of $ub$ and $bw$, in some order.
\end{enumerate}
\end{definition}

Rule (M) compares the window with an alternative route between its ends. Rule (J) compares its correction edges with a re-pairing of their endpoints. Rule (S) compares the corner $u,b,w$ with the opposite corner $u,x,w$ of a square. Restricting the walks to the ball of the head keeps (M) and (J) local, and the detector $x$ of (S) lies within two edges of the head $b$ (Lemma~\ref{lem:locality2}). Because dropping walks only drops exclusions, any restriction of this kind would do.

\begin{lemma}\label{lem:excluded}
\begin{enumerate}[label=\textup{(\alph*)}]
\item Let $p\le p_{\ast\ast}$, let the weights be as in Section~\ref{sec:decoder}, and let $C$ be a minimizer. Label the edges of $\gamma\cap E$ by $\mathsf E$ and those of $\gamma\cap C$ by $\mathsf C$. Then no window of $\gamma$, with these labels, is excluded by (M) or (J).
\item Let $p\le p_{\ast\ast}$, let the weights be profile weights and suppose that the decoder fails. Let $C^\ast$ be a minimizer for which the decoder fails, with the smallest value of $\Phi$ among these minimizers, and label the path $\gamma\subseteq E\triangle C^\ast$ as in (a). Then no window of $\gamma$ is excluded by (S).
\end{enumerate}
\end{lemma}

\begin{proof}
(a) Suppose that a window $\sigma$ of $\gamma$ is excluded, and let $P'$ be the walk or the union of walks of Definition~\ref{def:excluded}. Let $P''$ be the set of edges that $P'$ uses an odd number of times, so that $w(P'')\le w(P')$. Put $\varepsilon_e=-\ln(1-q_e)$. Since $q_e(1-q_e)\le r_e\le q_e$, each weight satisfies $|w_e+\ln q_e|\le\varepsilon_e$, and each $\varepsilon_e$ with $e\in P'$ is at most $-\ln(1-c_{\max}p)$.

Under (M), $P''$ has the same detector boundary as $\sigma$, because $b_1$, $b_2$ and $B$ are not detectors, and we have
\[
w(\sigma_C)-w(\sigma_E)-w(P')\ge k\ln\frac1p+\ln\frac{c(\sigma_E)\,c(P')}{c(\sigma_C)}-\sum_{e\in\sigma}\varepsilon_e-\sum_{e\in P'}\varepsilon_e .
\]
At $p=p_{\ast\ast}$ the right side is positive by \eqref{eq:excluded}. As $p$ decreases, the first term does not decrease, because $k\ge0$, and each $\varepsilon_e$ decreases, so the right side stays positive. Hence $w(\sigma_C)-w(\sigma_E)>w(P'')$, which contradicts Lemma~\ref{lem:window}(a).

Under (J), each vertex of $T(\sigma)$ is an end of exactly one walk, so $P''$ has the detector boundary $T(\sigma)$ of $\sigma_C$. The same estimate without the terms of $\sigma_E$, and with \eqref{eq:excludedJ} in place of \eqref{eq:excluded}, shows that $w(\sigma_C)>w(P'')$, which contradicts Lemma~\ref{lem:window}(b) for $X=\sigma_C$.

(b) Suppose that the window $(u,b,w)$ of $\gamma$ is excluded by (S), with the detector $x$, and let $Q$ be the cycle with the edges $ub$, $bw$, $wx$ and $xu$. The edges $ub$ and $bw$ belong to $C^\ast$. The set $C'=C^\ast\triangle Q$ satisfies $\partial C'=\partial C^\ast$, and since $Q$ has no edge at $b_1$, the decoder predicts the same logical flip with $C'$ as with $C^\ast$. Since profile weights agree on edges with the same profile, $w(ux)+w(xw)=w(ub)+w(bw)$. If neither $ux$ nor $xw$ belongs to $C^\ast$, then $w(C')=w(C^\ast)$, so $C'$ is a minimizer for which the decoder fails, and $\Phi(C')-\Phi(C^\ast)=2\bigl(\phi(x)-\phi(b)\bigr)<0$, which contradicts the choice of $C^\ast$. If exactly one of them, say $xw$, belongs to $C^\ast$, then $w(C')=w(C^\ast)-w(ub)-w(bw)-w(xw)+w(ux)=w(C^\ast)-2w(xw)$, and if both do, then $w(C')=w(C^\ast)-w(Q)$. In both cases $w(C')<w(C^\ast)$, which contradicts the minimality of $C^\ast$.
\end{proof}

For example, for a window made of $\mathsf C$-edges only, $k\ge0$ says that the alternative has at most as many edges as the window. For mixed windows, rule (M) uses the $\mathsf E$-edges as well: the correction edges of a window weigh at most as much as its error edges together with any alternative. Rule (J) uses only the correction edges, but it can re-pair the ends of two separate runs of them.

\subsection{Labelled paths}
A \emph{labelled path} is a simple path $b_1=v_0,v_1,\dots,v_L=b_2$ in $G$ with a label $\mathsf E$ or $\mathsf C$ on each edge, none of whose sub-paths with $2$, $3$ or $4$ edges is, with its labels, an excluded window. Its weight is
\[
\omega(\gamma)=\prod_{\mathsf E\text{-edges}}q_e^{1-s}(1-q_e)^{-s}\prod_{\mathsf C\text{-edges}}\Bigl(\frac{q_e}{1-q_e}\Bigr)^{s},
\]
and we write $\omega(e,l)$ for the factor of an edge $e$ with label $l$.

\begin{proposition}\label{prop:labelled}
For every $p\le p_{\ast\ast}$, $\Pfail$ is at most the total weight of all labelled paths, provided that for part (b) the weights are profile weights.
\end{proposition}

\begin{proof}
Suppose the decoder fails. For part (a) let $C$ be the minimizer that it returns, and for part (b) let $C=C^\ast$ be the minimizer of Lemma~\ref{lem:excluded}(b). In both cases the decoder fails with $C$. Let $\gamma\subseteq E\triangle C$ be the path of Lemma~\ref{lem:path}, and label the edges of $\gamma\cap E$ by $\mathsf E$ and those of $\gamma\cap C$ by $\mathsf C$. By Lemma~\ref{lem:excluded} no sub-path of $\gamma$ with at most four edges is, with these labels, an excluded window, so $\gamma$ with these labels is a labelled path. Its set $S$ of $\mathsf E$-edges satisfies $S\subseteq E$ and, by Lemma~\ref{lem:half}, $w(S)\ge w(\gamma\setminus S)$. By the union bound and Lemma~\ref{lem:prob}, $\Pfail$ is at most the sum of $\prod_{e\in S}q_e$ over labelled paths. As in the proof of Lemma~\ref{lem:tilt}, we have $\prod_{e\in S}q_e\le\prod_{e\in S}q_ee^{sw_e}\prod_{e\in\gamma\setminus S}e^{-sw_e}$. Because $q_e(1-q_e)\le r_e\le q_e$, we have $q_ee^{sw_e}\le q_e^{1-s}(1-q_e)^{-s}$ and $e^{-sw_e}\le(q_e/(1-q_e))^{s}$.
\end{proof}

\subsection{A criterion with memory}
A \emph{state} is a path $v_0,v_1,v_2,v_3$ of distinct vertices with $v_1,v_2,v_3\in V$ and $v_0\in V\cup\{b_1\}$, together with labels $l_1l_2l_3$ of its three edges. Its \emph{successors} are the states $(v_1,v_2,v_3,v_4;l_2l_3l_4)$ with $v_4\in V\setminus\{v_0,v_1,v_2\}$, and its \emph{terminal moves} are the edges $\{v_3,b_2\}$ with a label $l_4$. In both cases we require that none of the windows $(v_2,v_3,v_4)$, $(v_1,\dots,v_4)$ and $(v_0,\dots,v_4)$, with the labels $l_3l_4$, $l_2l_3l_4$ and $l_1\cdots l_4$, is excluded, where $v_4=b_2$ for terminal moves. These three windows have the head $v_3$.

\begin{lemma}\label{lem:memory}
Let $\lambda>0$, and let $H$ assign a positive number to every state. Suppose that every state $\sigma=(v_0,v_1,v_2,v_3;l_1l_2l_3)$ satisfies
\begin{equation}\label{eq:row}
\sum_{\text{successors}}\omega(v_3v_4,l_4)\,H(v_1,v_2,v_3,v_4;l_2l_3l_4)+\sum_{\text{terminal moves}}\omega(v_3b_2,l_4)\le\lambda\,H(\sigma).
\end{equation}
Then for every $L\ge4$ the labelled paths with $L$ edges have total weight at most
\[
\lambda^{L-3}\sum\omega(b_1v_1,l_1)\,\omega(v_1v_2,l_2)\,\omega(v_2v_3,l_3)\,H(b_1,v_1,v_2,v_3;l_1l_2l_3),
\]
where the sum runs over the states with $v_0=b_1$.
\end{lemma}

\begin{proof}
For a state $\sigma$ and $m\ge1$ let $W_m(\sigma)$ be the total weight of the sequences of $m$ edges that continue $\sigma$ by successors and end with a terminal move, the weight being the product of the factors of the new edges. Then $W_1(\sigma)$ is the terminal sum in \eqref{eq:row}, so $W_1(\sigma)\le\lambda H(\sigma)$, and for $m\ge2$, by induction,
\[
W_m(\sigma)=\sum_{\text{successors}}\omega(v_3v_4,l_4)\,W_{m-1}(v_1,v_2,v_3,v_4;l_2l_3l_4)\le\lambda^{m}H(\sigma).
\]
A labelled path $b_1,v_1,\dots,v_L$ begins with the state $(b_1,v_1,v_2,v_3;l_1l_2l_3)$, and each quadruple of consecutive vertices is a successor of the previous one. Indeed $v_{i+1}\notin\{v_{i-2},v_{i-1},v_i\}$ because the path is simple, and the windows ending at $v_{i+1}$ are not excluded because the path is labelled. Hence the labelled paths with $L$ edges have total weight at most $\sum\omega(b_1v_1,l_1)\,\omega(v_1v_2,l_2)\,\omega(v_2v_3,l_3)\,W_{L-3}(b_1,v_1,v_2,v_3;l_1l_2l_3)$.
\end{proof}

\subsection{Classes and locality}
The certificate assigns the same potential to states with the same \emph{class} and the same labels. Here the class of $(v_0,v_1,v_2,v_3;l_1l_2l_3)$ records the types of $v_0$ (or the label $b_1$), $v_1$, $v_2$ and $v_3$ and the offsets $v_1-v_0$, $v_2-v_1$ and $v_3-v_2$. We call the inequality \eqref{eq:row}, written in terms of classes, labels and edge coefficients, the \emph{row} of the state. The \emph{growth rate} of a set of rows is the infimum of the $\lambda$ for which some positive potential satisfies all of them. The \emph{typed ball} of a detector $v$ is the set of pairs (offset $u-v$, type of $u$) over the detectors $u$ in the ball of $v$.

\begin{lemma}\label{lem:locality2}
The rows of the states $(v_0,v_1,v_2,v_3;l_1l_2l_3)$ with a given last vertex $v_3$ are determined by the typed ball of $v_3$. The sum of $\omega(b_1v_1,l_1)\,\omega(v_1v_2,l_2)\,\omega(v_2v_3,l_3)\,H(b_1,v_1,v_2,v_3;l_1l_2l_3)$ over the states with a given neighbour $v_1$ of $b_1$ is determined by the typed ball of $v_1$. Every typed ball of every graph $G_{d,T}$ occurs in some $G_{d',T'}$ with $d'\le25$ and $T'\le13$.
\end{lemma}

\begin{proof}
The vertices of a state ending at $v_3$ and of its successors lie within three edges of $v_3$, and their classes and the coefficients of the edges involved are read from types and offsets. Since the windows tested in these rows have the head $v_3$, the exclusion tests use only walks whose detectors lie in the ball of $v_3$, the edges among these detectors and their boundary edges, all of which the types record. Rule (S) uses a detector within two edges of the head and the profiles of four edges between detectors of the ball. The profiles of the edges at a detector $v$ are determined by the same local data as its type in Lemma~\ref{lem:locality}(b), because the outcomes with $v$ in their signature and their locations are, and they are in fact determined by the type of $v$${}^\dagger$. So the types record these profiles as well. The start sums involve $v_2\sim v_1$, $v_3\sim v_2$ and no exclusions.

A chain of at most four edges between detectors changes each coordinate by at most $16$ and the layer by at most $4$. By Lemma~\ref{lem:locality}(b), the typed ball of $v_3$ is therefore determined by the positions of the qubits within $\ell^\infty$-distance $22$ of $v_3$ and the X or Z types of the measure qubits among them, by $\min(r,6)$ and by $\min(T-r,6)$, where $r$ is the layer of $v_3$. The last statement follows as in Lemma~\ref{lem:locality}(c), with $6$ replaced by $22$ and $2$ by $6$. Indeed, the even coordinates of $G_{25}$ at distance at least $23$ from both opposite sides are $24$ and $26$, one of each residue modulo $4$, and the layer data of every layer occur for $T'=13$.
\end{proof}

\subsection{Proof of Theorem~\ref{thm:refined}}
Put $\lambda_0=997/1000$ for part (a) and $\lambda_0=999/1000$ for part (b). The instances with $d\le25$ and $T\le13$ have $2{,}546{,}882$ distinct rows for part (a) and $2{,}545{,}552$ for part (b)${}^\dagger$, and by Lemma~\ref{lem:locality2} these are all the rows of all graphs $G_{d,T}$. Each of the two certificates assigns a positive integer $h$ to each of the $953{,}120$ pairs of a class and a label sequence $l_1l_2l_3$ that occur, and we put $H=h/10^{15}$. All rows hold in exact integer arithmetic at $p=p_{\ast\ast}$ with $\lambda=\lambda_0$, when each factor $\omega(e,l)$ is replaced by a rational upper bound computed with integer roots of order $50$ for part (a) and $25$ for part (b)${}^\dagger$ (Table~\ref{tab:verify2}). Let $p\le p_{\ast\ast}$ and $\rho=(p/p_{\ast\ast})^{s}$. Then each factor satisfies $\omega(e,l)(p)\le\rho\,\omega(e,l)(p_{\ast\ast})$, because $(p/p_{\ast\ast})^{1-s}\le\rho$ and $(1-q_e)^{-1}$ decreases as $p$ decreases. Windows excluded by (M) or (J) stay excluded by Lemma~\ref{lem:excluded}(a), and rule (S) does not depend on $p$. Hence all rows hold at $p$ with $\lambda_p=\lambda_0\rho$. Let $K$ be an upper bound, computed with the same rational bounds of the factors, for the start sums of Lemma~\ref{lem:locality2} at $p_{\ast\ast}$ over all neighbours $v_1$ of $b_1$${}^\dagger$. Let $K_3$ be an upper bound of the same kind for the sums of $\omega(b_1v_1,l_1)\,\omega(v_1v_2,l_2)\,\omega(v_2b_2,l_3)$ over the paths $b_1,v_1,v_2,b_2$ with a given $v_1$ and all labels${}^\dagger$; such paths exist only for $d=3$. For part (a) $K=0.031062\ldots$ and $K_3=0.032106\ldots$, and for part (b) $K=0.056229\ldots$ and $K_3=0.064013\ldots$. From Proposition~\ref{prop:labelled}, Lemma~\ref{lem:memory} and Lemma~\ref{lem:length} we obtain
\[
\Pfail\le|N(b_1)|\Bigl(\rho^{3}K_3\,[d=3]+\sum_{L\ge\max(d,4)}\lambda_p^{L-3}\rho^{3}K\Bigr)\le\rho^{3}\,|N(b_1)|\,(K+K_3)\,\frac{\lambda_p^{d-3}}{1-\lambda_p}.
\]
Recall that $|N(b_1)|=(T+1)(d+1)/2$ by Lemma~\ref{lem:graphlike}(e). With $\rho=\lambda_p/\lambda_0$ the right side equals $(K+K_3)(T+1)(d+1)\lambda_p^{d}/(2\lambda_0^3(1-\lambda_p))$, and $(K+K_3)/(2\lambda_0^3)$ is at most $0.032$ for part (a) and $0.061$ for part (b). \qed

\section{The lean schedule}\label{sec:lean}
In the lean schedule all measure qubits and data qubits are prepared in a first step, the Z-type measure qubits in $|0\rangle$ and the X-type ones in $|+\rangle$. Each round then consists of the steps (S3)--(S6) of Section~\ref{sec:circuit} and one more step. In it each Z-type measure qubit is measured in the $Z$ basis and reset to $|0\rangle$, each X-type measure qubit is measured in the $X$ basis and reset to $|+\rangle$, and the data qubits are idle. The noise model of Section~\ref{sec:noise} applies to these locations, the measurement and the reset in this step failing independently, each with probability $p$. The detectors, the logical outcomes and the decoder are as before.

Section~\ref{sec:graph} carries over with the following changes${}^\dagger$. Each fault outcome again flips at most two detectors, and Lemma~\ref{lem:graphlike} holds with $c_{\max}=94/15$. In the bulk of basis $Z$, the coefficients $15c_e$ of the edges with offsets $\pm(0,0,1)$, $\pm(2,-2,0)$, $\pm(2,2,0)$, $\pm(2,2,-1)$, $\pm(2,-2,-1)$ and $\pm(4,0,-1)$ are $46$, $42$, $18$, $16$, $8$ and $8$, against $66$, $72$, $48$, $16$, $8$ and $8$ in Lemma~\ref{lem:bulk}. The difference comes from the three idle steps per round of the data qubits and the two of the Z-type measure qubits that the lean schedule does not have. There are again $29$ node types per basis. We count the reset in the measure-and-reset step, and the first step, as the start of the next round. With this convention a measure qubit is again reset at the start of each round, and the proofs of Lemmas~\ref{lem:locality} and~\ref{lem:locality2}, which use only the layout, the CX orders and this structure of the rounds, apply verbatim. All edges again change each coordinate by at most $4$ and the layer by at most $1$.

\begin{proof}[Proof of Theorem~\ref{thm:lean}]
(a) As in Section~\ref{sec:proof}, with $\lambda=25.55\sqrt p$. At $p=1.53\times10^{-3}$ we have $25.55\sqrt p\ge0.9993$, and the criterion \eqref{eq:check}, with $0.9997$ replaced by $0.9993$, holds for all types, with largest left side $0.99794$ at the bulk type and $0.95318$ for the others${}^\dagger$. With $c_{\max}=94/15$, the assembly of Section~\ref{sec:proof} then leads to the prefactor $\sqrt{c_{\max}/(1-c_{\max}p)}/25.55\le0.0985$.

(b) As in Section~\ref{sec:refined}, with $p_{\ast\ast}=3/1250$, $s=21/50$ and $c_{\max}=94/15$ in Definition~\ref{def:excluded}. The instances with $d\le25$ and $T\le13$ have $2{,}548{,}765$ distinct rows, all of which already occur for $d\le15$ and $T\le7$. A certificate with positive integers on the $953{,}120$ pairs of a class and a label sequence satisfies all rows in exact arithmetic with $\lambda=997/1000$, and the start constants are $K=0.026464\ldots$ and $K_3=0.028384\ldots$, with $(K+K_3)/(2\cdot0.997^3)\le0.028$${}^\dagger$.

(c) As in part (b) of Theorem~\ref{thm:refined}, with $p_{\ast\ast}=3/1000$, $s=9/25$, $\lambda_0=997/1000$ and $c_{\max}=94/15$. The instances with $d\le25$ and $T\le13$ have $2{,}547{,}432$ distinct rows. Again, a certificate on the same $953{,}120$ pairs satisfies all rows in exact arithmetic with $\lambda=997/1000$, and the start constants are $K=0.045261\ldots$ and $K_3=0.057416\ldots$, with $(K+K_3)/(2\cdot0.997^3)\le0.052$${}^\dagger$.
\end{proof}

\section{Non-uniform error rates}\label{sec:hetero}
In a real device the gates, measurements and idle steps fail at different rates. To model this, we sort the locations of the circuit of Section~\ref{sec:circuit} into seven categories: resets and preparations; measurements; $H$ gates; CX gates; qubits idle in steps (S2)--(S7); data qubits idle in step (S1); data qubits idle in step (S8). A \emph{rate vector} $\theta$ assigns a failure probability $\theta_k$ to the locations of category $k$, with the failure outcomes of Section~\ref{sec:noise}. The probability of an edge becomes
\[
q_e(\theta)=\sum_k c_{e,k}\,\theta_k ,
\]
where $c_{e,k}$ is the sum of $\pi(f)$ over the outcomes $f$ with $e(f)=e$ at locations of category $k$, so that $\sum_kc_{e,k}=c_e$. The graph, the signatures and the logical effects do not depend on $\theta$, and Sections~\ref{sec:graph} and~\ref{sec:paths} hold with $q_e(\theta)$ in place of $c_ep$. The types, which now record the coefficients $c_{e,k}$, are again $29$ per basis, and Lemma~\ref{lem:locality} holds with the same proof${}^\dagger$.

\begin{theorem}\label{thm:hetero}
Let $\theta$ be a rate vector with $\max_eq_e(\theta)<1/2$, and consider the memory experiment with rates $t\theta$ for some $0<t\le1$.
\begin{enumerate}[label=\textup{(\alph*)}]
\item Suppose that $\sum_{e\ni v}a_e/(\lambda+a_e)\le1$ at every detector $v$, where $a_e=2\sqrt{q_e(\theta)/(1-q_e(\theta))}$ and $\lambda<1$. Then
\[
\Pfail\le\frac{(T+1)(d+1)}{2}\cdot\frac{a_{\max}}{\lambda}\cdot\frac{(\lambda\sqrt t)^{d}}{1-\lambda\sqrt t},
\]
where $a_{\max}$ is the largest $a_e$ over the edges at $b_1$ and $b_2$.
\item Let $q(P)=\prod_{e\in P}q_e(\theta)$, with multiplicity, and $q_{\max}=\max_eq_e(\theta)$. In Definition~\ref{def:excluded}, replace \eqref{eq:excluded} by
\begin{equation}\label{eq:excluded-theta}
\frac{q(\sigma_E)\,q(P')}{q(\sigma_C)}>\prod_{e\in\sigma}\frac{1}{1-q_e(\theta)}\cdot\Bigl(\frac{1}{1-q_{\max}}\Bigr)^{h'}
\end{equation}
and \eqref{eq:excludedJ} by
\begin{equation}\label{eq:excludedJ-theta}
\frac{q(P')}{q(\sigma_C)}>\prod_{e\in\sigma_C}\frac{1}{1-q_e(\theta)}\cdot\Bigl(\frac{1}{1-q_{\max}}\Bigr)^{h'},
\end{equation}
keeping the conditions $k\ge0$, and define labelled paths, states and rows as in Section~\ref{sec:refined} with the windows excluded by these two rules, with the factors $\omega(e,l)$ evaluated at $q_e(\theta)$ and with a tilt $0<s\le1/2$. Suppose that a positive potential satisfies all rows with some $\lambda<1$, and let $K$ and $K_3$ be the largest start sums, as in Section~\ref{sec:refined}. Then
\[
\Pfail\le\frac{(T+1)(d+1)}{2}\cdot\frac{K+K_3}{\lambda^{3}}\cdot\frac{(\lambda t^{s})^{d}}{1-\lambda t^{s}}.
\]
\item For a location $\ell$ of category $k$ let $c_{\ell,e}(\theta)$ be the sum of $\theta_k\pi(f)$ over the outcomes $f$ of $\ell$ with $e(f)=e$, and call the multiset of the nonzero numbers $c_{\ell,e}(\theta)$ the profile of $e$ at $\theta$. Suppose that $r_e$ is a function of $t$ and of this profile, and add rule (S) of Definition~\ref{def:excluded}, with these profiles, to the two rules of part (b). If a positive potential satisfies all rows with some $\lambda<1$, then the bound of part (b) holds with the start sums of these rows.
\end{enumerate}
\end{theorem}

\begin{proof}
(a) For the rates $t\theta$ each $a_e$ is at most $\sqrt t\,a_e$, because $1-tq_e(\theta)\ge1-q_e(\theta)$. Since $x/(\lambda\sqrt t+x)$ increases in $x$, the criterion holds with $\lambda\sqrt t$ in place of $\lambda$. The bound then follows from the assembly of Section~\ref{sec:proof}, with $\sqrt t\,a_{\max}$ in place of $a_{\max}$.

(b) Lemma~\ref{lem:excluded}(a) holds for the rates $t\theta$, with \eqref{eq:excluded-theta} and \eqref{eq:excludedJ-theta} in place of \eqref{eq:excluded} and \eqref{eq:excludedJ}. In its proof the first two terms of the lower bound become $k\ln(1/t)+\ln(q(\sigma_E)q(P')/q(\sigma_C))$ under (M) and $k\ln(1/t)+\ln(q(P')/q(\sigma_C))$ under (J), and $k\ge0$. Similarly, Lemma~\ref{lem:locality2} holds with the same proof. Each factor satisfies $\omega(e,l)(t\theta)\le t^{s}\,\omega(e,l)(\theta)$, because $t^{1-s}\le t^{s}$ for $s\le1/2$. Hence all rows hold for the rates $t\theta$ with $\lambda t^{s}$ in place of $\lambda$, and every start sum is at most $t^{3s}$ times its value at $\theta$. With $\rho=t^{s}$, the assembly of Section~\ref{sec:refined} yields the bound.

(c) The profiles at $t\theta$ are $t$ times those at $\theta$, so rule (S) does not depend on $t$, and Lemma~\ref{lem:excluded}(b) holds with the same proof: profile weights agree on edges with the same profile. The proof of part (b) then applies with the rows of part (c), and Proposition~\ref{prop:labelled} uses the minimizer $C^\ast$ of Lemma~\ref{lem:excluded}(b).
\end{proof}

Table~\ref{tab:chips} lists error models built from published component error rates of six devices, mapped onto the seven categories. Errors reported as average infidelities $r$, including the memory errors of the Quantinuum data sheets, are converted to Pauli error probabilities $3r/2$ (one qubit) and $5r/4$ (two qubits). Errors reported as Pauli errors, and the cross-entropy-benchmarking errors of Zuchongzhi~3.2, are used as they are. Readout and SPAM errors are used as measurement flip probabilities, and the SPAM errors of Helios and H2 also as reset failure probabilities. Rates that a source does not report are assumptions, listed with the sources in the accompanying files. The models are idealizations: they assume independent stochastic Pauli noise on the circuit of Section~\ref{sec:circuit}, whereas the devices use other native gates and schedules and also suffer leakage and correlated or coherent errors. Thus Theorem~\ref{thm:hetero} applies to the stated models, not to the devices. Part (b), with $s=43/100$, certifies three models:
\begin{align*}
&\text{Quantinuum Helios:}&&\Pfail\le0.033\,(T+1)(d+1)\,\lambda^d/(1-\lambda),&&\lambda=0.75\,t^{43/100},\\
&\text{Quantinuum H2:}&&\Pfail\le0.022\,(T+1)(d+1)\,\lambda^d/(1-\lambda),&&\lambda=0.715\,t^{43/100},\\
&\text{IBM Heron r3, square grid:}&&\Pfail\le0.023\,(T+1)(d+1)\,\lambda^d/(1-\lambda),&&\lambda=0.97\,t^{43/100},
\end{align*}
for their rates scaled by any $t\le1$. For profile weights, part (c) with $s=19/50$ improves these to
\begin{align*}
&\text{Quantinuum Helios:}&&\Pfail\le0.058\,(T+1)(d+1)\,\lambda^d/(1-\lambda),&&\lambda=0.675\,t^{19/50},\\
&\text{Quantinuum H2:}&&\Pfail\le0.039\,(T+1)(d+1)\,\lambda^d/(1-\lambda),&&\lambda=0.643\,t^{19/50},\\
&\text{IBM Heron r3, square grid:}&&\Pfail\le0.039\,(T+1)(d+1)\,\lambda^d/(1-\lambda),&&\lambda=0.873\,t^{19/50}.
\end{align*}
Part (a) also certifies Helios and H2, but it fails at $\lambda=1$ for the other four models${}^\dagger$. For the models of Google's and USTC's processors, floating-point estimates of the growth rate of the rows are $1.39$, $1.45$ and $1.52$ for part (b) and $1.25$, $1.30$ and $1.36$ for part (c).

\begin{table}[ht]
\centering\scriptsize\setlength{\tabcolsep}{4pt}
\begin{tabular}{@{}lcccccccccc@{}}
\toprule
model & CX & $H$ & meas. & reset & idle & idle (S1) & idle (S8) & (a) & (b) & (c)\\
\midrule
Helios \cite{QHelios} & 1e-3 & 4.5e-5 & 5e-4 & 5e-4 & 9e-4 & 9e-4 & 9e-4 & $0.9325^\dagger$ & $0.75^\dagger$ & $0.675^\dagger$\\
H2 \cite{QH2} & 1.25e-3 & 4.5e-5 & 1e-3 & 1e-3 & 3e-4 & 3e-4 & 3e-4 & $0.8957^\dagger$ & $0.715^\dagger$ & $0.643^\dagger$\\
Heron r3 \cite{IBMQ} & 1.9375e-3 & 2.76e-4 & 3.48e-3 & 2e-3 & 1e-4 & 1e-3 & 2e-3 & $(1.212)$ & $0.97^\dagger$ & $0.873^\dagger$\\
Google 72q \cite{GQAI24} & 3.55e-3 & 6.2e-4 & 8e-3 & 1.5e-3 & 3.7e-4 & 3e-3 & 6.25e-3 & $(1.741)$ & $(1.393)$ & $(1.249)$\\
Willow \cite{GWillow} & 4.125e-3 & 5.25e-4 & 7.7e-3 & 1.5e-3 & 3.7e-4 & 3e-3 & 6.25e-3 & $(1.813)$ & $(1.445)$ & $(1.295)$\\
Zuchongzhi 3.2 \cite{USTC26} & 5.5e-3 & 8.5e-4 & 9.5e-3 & 1.5e-3 & 3e-4 & 1.5e-3 & 3.5e-3 & $(1.915)$ & $(1.516)$ & $(1.360)$\\
\bottomrule
\end{tabular}
\caption{Error models (Pauli error probabilities per location) and the rates $\lambda$ of parts (a), (b) and (c) of Theorem~\ref{thm:hetero} at $t=1$. Daggered values are certified exactly, those of (b) with $s=43/100$ and those of (c) with $s=19/50$. Values in parentheses are not certificates: in column (a) they are floating-point roots of the criterion, and in columns (b) and (c) floating-point growth rates of the rows, computed from the instances with $d\le15$ and $T\le7$, the smallest over $s\in\{0.40,0.43,0.45\}$ for (b) and over a grid of $s$ between $0.30$ and $0.44$ for (c). Helios and H2: typical values of the data sheets. Heron r3: medians of ibm\_boston on 2026-10-18, placed on a square grid, which the device does not have. Google 72q: the error budget of the 72-qubit processor in \cite[Table S4]{GQAI24}, with the CZ crosstalk and leakage rows added to the CX rate, and the leakage-heating row added to the data-idle error during measurement and reset, which is split over steps (S1) and (S8). Willow: mean simultaneous randomized-benchmarking errors of the spec sheet. Zuchongzhi 3.2: cross-entropy-benchmarking errors of the $97$-qubit region, used as reported. Assumptions: the rates in the column ``idle'' for the IBM, Google and USTC models (for the Google models estimated from coherence times); the reset rates and the (S1) and (S8) idle rates of the IBM and USTC models; for Willow, the reset and data-idle rates of the 72-qubit budget; and for both Google models, the split of the data-idle error over (S1) and (S8).}
\label{tab:chips}
\end{table}

\section{Computer verification}\label{sec:verification}

Table~\ref{tab:verify} lists the computations behind the statements marked ${}^\dagger$. We compute the fault table by forward propagation of Pauli frames, independently of Stim's detector-error-model code, and keep each Pauli outcome of each location with its exact probability. Over the full range there are $1{,}924{,}076$ outcomes. The circuit file also declares the detectors of the other type, but the decoding graph of each sector ignores them. All comparisons in V6 use exact rational arithmetic. One run of the accompanying script performs all checks in the table and passes only if all of them hold.

\begin{table}[ht]
\centering\small
\begin{tabular}{@{}l>{\raggedright\arraybackslash}p{0.62\textwidth}l@{}}
\toprule
& check & range\\
\midrule
V1 & noiseless circuit: all detectors and the logical outcome are deterministic, with value $0$ & $d\le13$, $T\le7$\\
V2 & fault table: each outcome, injected alone into Stim's Pauli-frame simulator, gives the signature and logical effect computed here; the set of signatures equals that of Stim's detector error model; the outcome probabilities of each location sum to $1$; the coefficients $c_e$ agree with Stim's edge probabilities at $p=10^{-7}$ to $2\times10^{-6}$ relative & $d\le13$, $T\le7$\\
V3 & Lemma~\ref{lem:graphlike}(a,b) & $d\le13$, $T\le7$\\
V4 & Lemma~\ref{lem:graphlike}(c,d,e) & $d\le13$, $T\le7$\\
V5 & exactly $29$ types per basis; all occur already for $d\le9$, $T\le5$; the set of types is the same for all $d\ge9$, $T\ge5$ in range (Lemma~\ref{lem:locality}) & $d\le13$, $T\le7$\\
V6 & criterion \eqref{eq:check} for all types at $p=\pst$, $\lambda=0.9997$, and at $p=10^{-3}$, $\lambda=0.98$; the unique maximum is the bulk type; the second largest value at $\pst$ is at most $0.9629$ & all $29+29$ types\\
\bottomrule
\end{tabular}
\caption{Computer verification for Theorem~\ref{thm:main}. Lemma~\ref{lem:locality}(c) needs only $d\le9$ and $T\le5$.}
\label{tab:verify}
\end{table}

Table~\ref{tab:verify2} lists the checks behind Theorem~\ref{thm:refined}. Two further scripts, one for each part, regenerate the rows of all instances with $d\le25$ and $T\le13$ and check them against the two certificates, each of which lists $953{,}120$ integers $h$. By Lemma~\ref{lem:locality2} the rows at a detector depend only on its typed ball, so each script computes the rows at one detector for each distinct typed ball of the range, which we call the heads; balls are compared as full tuples. The rows are generated by a C++ program with exact integer arithmetic. A Python implementation of the same rules produces the same rows at all detectors of five test instances with $d\le9$ and $T\le5$, and of two instances with the rates of Section~\ref{sec:hetero}. Classes are named by $64$-bit hashes of the types and offsets they record. A collision would merge two classes, but this can only make the system of rows harder to satisfy. Three further steps are not used in the proof: the iteration on the system of rows that found the potentials, and two tests of the exclusions. For the first test, let $w^{+}_e=-\ln q_e-\ln(1-q_e)$ and $w^{-}_e=-\ln q_e+\ln(1-q_e)$ be the upper and lower bounds of the weights at $p_{\ast\ast}$. For each excluded window, Dijkstra's algorithm on $G/B$ with the weights $w^{+}$ finds an edge set with the same detector boundary as $\sigma$ that is lighter than $w^{-}(\sigma_C)-w^{+}(\sigma_E)$, or an edge set with the same detector boundary as $\sigma_C$ that is lighter than $w^{-}(\sigma_C)$. The test covers all $23.7$ million excluded windows of the instances with $d\le9$ and $T\le5$, with no failure, both at $p_{\ast\ast}=1/625$ and at $p_{\ast\ast}=1/500$. The second test recomputes every exclusion by rule (S) from the decoding graph, with the profiles read from the fault table, and checks that the two pairs of edges have the same profiles. For $d\le9$ and $T\le5$ it confirms all $18{,}720$ such windows for each schedule and finds no window that the rule misses.

\begin{table}[ht]
\centering\small
\begin{tabular}{@{}l>{\raggedright\arraybackslash}p{0.62\textwidth}l@{}}
\toprule
& check & range\\
\midrule
S1 & parameters of the certificate: $p_{\ast\ast}=1/625$, $\lambda=997/1000$, $s=21/50$ & \\
S2 & rows of all instances: $2{,}546{,}882$ distinct rows, all of which already occur for $d\le15$, $T\le7$; $13{,}658$ distinct typed balls; $29$ node types per basis, with injective identifiers; largest coefficient $c_{\max}=154/15$ & $d\le25$, $T\le13$\\
S3 & every class in a row, as head or successor, has a positive potential in the certificate & all rows\\
S4 & every row holds in exact integer arithmetic at $p_{\ast\ast}$ and $\lambda=997/1000$, with rational upper bounds of the factors $\omega$; largest ratio of the two sides $0.99900$ & all rows\\
S5 & start constants $K=0.031062\ldots$ and $K_3=0.032106\ldots$, with $(K+K_3)/(2\cdot0.997^3)\le0.032$ & all neighbours of $b_1$\\
S6 & part (b), as S1--S5: $p_{\ast\ast}=1/500$, $\lambda=999/1000$, $s=9/25$, rules (M), (J) and (S); the profile of each edge at a detector is determined by the type of the detector; $2{,}545{,}552$ distinct rows; positive potentials; all rows exact, largest ratio $0.99900$; $K=0.056229\ldots$, $K_3=0.064013\ldots$, $(K+K_3)/(2\cdot0.999^3)\le0.061$ & $d\le25$, $T\le13$\\
\bottomrule
\end{tabular}
\caption{Computer verification for Theorem~\ref{thm:refined}. Rows S1--S5 concern part (a). Lemma~\ref{lem:locality2} needs $d\le25$ and $T\le13$.}
\label{tab:verify2}
\end{table}

The checks behind Theorem~\ref{thm:lean} (Table~\ref{tab:verify3}) are those of Tables~\ref{tab:verify} and~\ref{tab:verify2}, run on the lean schedule with its own certificates. The Dijkstra test of the exclusions finds no failure among the $23.6$ million excluded windows of the $40$ instances with $d\le9$ and $T\le5$ at $p_{\ast\ast}=3/1250$, nor among the $23.5$ million at $p_{\ast\ast}=3/1000$.

\begin{table}[ht]
\centering\small
\begin{tabular}{@{}l>{\raggedright\arraybackslash}p{0.62\textwidth}l@{}}
\toprule
& check & range\\
\midrule
L1 & as V1--V5: deterministic noiseless values $0$; fault table equal to Stim's outcome by outcome and in first-order coefficients; Lemma~\ref{lem:graphlike} with $c_{\max}=94/15$; $29$ types per basis, stable for $d\ge9$, $T\ge5$ & $d\le13$, $T\le7$\\
L2 & as V6: criterion at $p=1.53\times10^{-3}$, $\lambda=0.9993\le25.55\sqrt p$; largest left side $0.99794$ (bulk), second $0.95318$ & all $29+29$ types\\
L3 & as S1--S5: $p_{\ast\ast}=3/1250$, $s=21/50$; $2{,}548{,}765$ rows, all present for $d\le15$, $T\le7$; positive potentials; all rows exact at $\lambda=997/1000$, largest ratio $0.99799$; $K=0.026464\ldots$, $K_3=0.028384\ldots$, $(K+K_3)/(2\cdot0.997^3)\le0.028$ & $d\le25$, $T\le13$\\
L4 & as S6: $p_{\ast\ast}=3/1000$, $s=9/25$, rules (M), (J) and (S); $2{,}547{,}432$ rows; positive potentials; all rows exact at $\lambda=997/1000$, largest ratio $0.99900$; $K=0.045261\ldots$, $K_3=0.057416\ldots$, $(K+K_3)/(2\cdot0.997^3)\le0.052$ & $d\le25$, $T\le13$\\
\bottomrule
\end{tabular}
\caption{Computer verification for Theorem~\ref{thm:lean}.}
\label{tab:verify3}
\end{table}

For Section~\ref{sec:hetero}, a further script runs the checks H1--H4 of Table~\ref{tab:verify4} on the error models of Table~\ref{tab:chips}. For H4 it runs the script of rows S1--S5 with the edge probabilities $q_e(\theta)$, written as integers over a common denominator, in place of the coefficients, and check H5 runs the script of row S6 in the same way. As a test, with uniform rates this code gives the rows of the code of Table~\ref{tab:verify2} for $(d,T)=(5,3)$, $(7,4)$ and $(9,5)$, after renaming the classes and rescaling the numerators of the edges.

\begin{table}[ht]
\centering\small
\begin{tabular}{@{}l>{\raggedright\arraybackslash}p{0.62\textwidth}l@{}}
\toprule
& check & range\\
\midrule
H1 & every location has one of the seven categories; with equal rates the coefficients $c_{e,k}$ add up to $c_e$ & $d\le9$, $T\le5$\\
H2 & category-resolved types: $29$ per basis, all present for $d=9$, $T=5$, and the same set for all $d\ge9$, $T\ge5$ in range & $d\le13$, $T\le7$\\
H3 & part (a) holds exactly for Helios at $\lambda=0.9325$ and for H2 at $\lambda=0.8957$; for the other four models its left side exceeds $1$ at $\lambda=1$ for some type & all $29+29$ types\\
H4 & part (b) for Helios, H2 and Heron r3, with $s=43/100$, as S1--S5: $q_{\max}$ recomputed, and every edge probability of the range at most $q_{\max}$; $2{,}546{,}246$, $2{,}546{,}404$ and $2{,}546{,}625$ distinct rows; positive potentials; all rows exact at $\lambda=3/4$, $143/200$ and $97/100$; $(K+K_3)/(2\lambda^3)\le0.033$, $0.022$ and $0.023$ & $d\le25$, $T\le13$\\
H5 & part (c) for Helios, H2 and Heron r3, with $s=19/50$, as S6, with the profiles at the model rates: $2{,}544{,}853$, $2{,}545{,}240$ and $2{,}545{,}179$ distinct rows; positive potentials; all rows exact at $\lambda=27/40$, $643/1000$ and $873/1000$; $(K+K_3)/(2\lambda^3)\le0.058$, $0.039$ and $0.039$ & $d\le25$, $T\le13$\\
\bottomrule
\end{tabular}
\caption{Computer verification for Theorem~\ref{thm:hetero} and the error models of Table~\ref{tab:chips}.}
\label{tab:verify4}
\end{table}

\section{Formal verification in Lean 4}\label{sec:lean4}

We prove the theorems of this paper in the proof assistant Lean~4 (version 4.35.0-rc3), using the Mathlib library
(commit \texttt{c55e6e78}). A \emph{proof assistant} checks every step of a proof against a small set of logical rules;
the part of Lean that performs this check is its \emph{kernel}. The formal development defines the circuit, the noise,
the memory experiment and the decoder of Section~\ref{sec:setting}, and derives the bounds of the theorems from these
definitions. It contains about 25{,}100 lines written by hand, together with generated data files (node types,
certificates) and generated check files. Each theorem is proved in two versions: in the \emph{kernel} version every
computation is checked by the kernel, and in the \emph{native} version the large computations are evaluated outside the
kernel, which takes far less time. In this section we state what is proved, what has to be trusted, and how to
reproduce the verification.

\subsection{What is modelled}

\emph{The circuit and the experiment.} The layout of the rotated surface code, the eight steps of a round, the noise
locations with their outcomes and the probabilities $p\,\pi(f)$ are those of Sections~\ref{sec:circuit}
and~\ref{sec:noise}. We define the effect of the faults by Pauli-frame propagation: a CX gate copies an $X$ component
from its control to its target and a $Z$ component from its target to its control, an $H$ gate exchanges the two
components, and a reset clears both. For any set of faults, at most one outcome per location, this determines the
recorded measurement outcomes, the detectors $D_{m,r}$ of Section~\ref{sec:circuit} and the flip of the logical
outcome. The formal development proves that these are the parities of the single-fault values, so they agree with the
signatures $\sigma(f)$ and the logical effects $\ell(f)$ of Section~\ref{sec:decoder}.

\emph{The decoder and the failure probability.} Here the decoding graph and the weights are those of
Section~\ref{sec:decoder}, for any numbers $r_e$ with $q_e(1-q_e)\le r_e\le q_e$; this range contains both common
choices. The failure probability $\Pfail$ is the probability, under the product distribution of the faults, that some
set $C$ of minimum weight with $\partial C$ equal to the observed detectors predicts the logical flip wrongly. Hence a bound
on this probability holds for every rule that selects a minimizer.

\emph{Profile weights.} The profile of an edge and profile weights are those of Section~\ref{sec:decoder}: for a location $\ell$, $c_{\ell,e}$ is the sum of $\pi(f)$ over the outcomes $f$ of $\ell$ with $e(f)=e$, the \emph{profile} of $e$ is the multiset of the nonzero numbers $c_{\ell,e}$ over all locations $\ell$, and the weights are \emph{profile weights} if $r_e$ is a function of $p$ and the profile of $e$. Note that both choices of Section~\ref{sec:decoder} are profile weights. The theorems that use rule (S) are stated for profile weights.

\emph{The lean schedule.} We model the lean schedule of Section~\ref{sec:lean} by its own Pauli-frame semantics: a
preparation step, then per round four CX steps and a fused measure-and-reset step, in which the X-type measure qubits
are measured in the $X$ basis. Its noise locations are those of Section~\ref{sec:lean}, including the reset failures
after the last measurement. The development proves that every lean location changes the measurement outcomes and the
final data values exactly as the corresponding location of the eight-step circuit restricted to the lean locations,
and that the reset failures after the last measurement change nothing. Hence the lean experiment has the failure
probability of the restricted eight-step circuit, and the formal theorems are about the lean schedule itself.

\emph{Non-uniform rates.} A rate vector $\theta$ assigns to each of the seven categories of Section~\ref{sec:hetero}
the failure probability $\theta_k$, and the outcomes of a failed location are uniform. The formal theorems are stated
for the three certified models, whose rates are those of the accompanying files, scaled by any $0<t\le1$.

\subsection{What is proved}

Table~\ref{tab:lean-thms} lists the formal theorems. Each holds for all odd $d\ge3$, all $T\ge1$ and both bases, with
the constants of the corresponding theorem of this paper. Their statements are the inequalities of
Theorems~\ref{thm:main}, \ref{thm:refined}, \ref{thm:lean} and~\ref{thm:hetero}, written for the failure probability
defined above.

\begin{table}[ht]
\centering
\small
\begin{tabular}{p{0.32\textwidth}p{0.36\textwidth}cc}
\toprule
Statement & Range and constants & Kernel & Native \\
\midrule
Thm~\ref{thm:main} & $p\le1.04\times10^{-3}$, both bounds & none & 61 \\
Thm~\ref{thm:refined}(a) & $p\le1.6\times10^{-3}$, $0.032$ & none & 131 \\
Thm~\ref{thm:refined}(b) & $p\le2\times10^{-3}$, $0.061$ & none & 132 \\
Thm~\ref{thm:lean}(a) & $p\le1.53\times10^{-3}$, $0.0985$ & none & 63 \\
Thm~\ref{thm:lean}(b) & $p\le2.4\times10^{-3}$, $0.028$ & none & 132 \\
Thm~\ref{thm:lean}(c) & $p\le3\times10^{-3}$, $0.052$ & none & 132 \\
Thm~\ref{thm:hetero}(a), Helios, H2 & $\lambda=0.9325$, $0.8957$ & none & 63 each \\
Thm~\ref{thm:hetero}(b), Heron, Helios, H2 & $0.023$, $0.033$, $0.022$ & none & 132 each \\
Thm~\ref{thm:hetero}(c), Heron, Helios, H2 & $0.039$, $0.058$, $0.039$ & none & 132 each \\
\bottomrule
\end{tabular}
\caption{The formal theorems, and for each of their two versions the number of axioms it depends on besides the three
standard ones. ``Kernel'': every computation is checked by Lean's kernel. ``Native'': the large computations are
evaluated outside the kernel, by compiled code or by Lean's interpreter; each such evaluation enters the proof as one
axiom (see the text). The standard axioms are propositional extensionality, the axiom of choice and quotient
soundness.}
\label{tab:lean-thms}
\end{table}

\subsection{What has to be trusted}

A Lean proof can rely on axioms, which the kernel accepts without proof. Lean reports, for every theorem, the axioms it
depends on. Every theorem of Table~\ref{tab:lean-thms} depends on three standard axioms of Lean's foundations
(propositional extensionality, the axiom of choice and the soundness of quotients). The kernel versions depend on
nothing else.

The native versions also depend on axioms of a second kind, one for each large computation. For such a computation
Lean evaluates the Boolean test outside the kernel, with compiled code or with its interpreter, and records the outcome
``true'' as an axiom naming the test. Trusting these axioms means trusting, in addition to the kernel, Lean's compiler,
interpreter and runtime, the C compiler that builds the precompiled modules, and the assumption that the loaded
libraries were built from the checked sources. The kernel itself already relies on the GMP library for arithmetic on
large natural numbers. The computations are: the checks of
Theorem~\ref{thm:main} at representative detectors, which by Lemma~\ref{lem:locality}(c) lie in instances with $d\le9$
and $T\le5$ (60 tests: the signatures of all fault outcomes near these detectors, and their node types); the type table of the circuit, with the edge profiles for rule (S); the coverage of all typed balls by the heads, and the number of heads; the rows and the start sums
at the 13{,}658 heads (40 tests); the rational upper bounds of the factors; the bound on the numerators; and the criterion for the
node types, used by parts~(a) and by the native version of Theorem~\ref{thm:main}.

In the kernel versions the kernel checks the same facts, in reformulated forms whose soundness is proved, split into
generated files that are checked one per process: the rows and start sums at the 13{,}658 heads for each of the ten certificates (3{,}330 files), the
coverage of the typed balls for the five models (107 files), the type tables (550 files), and the factor bounds and the
search trees that hold the typed balls and the potentials. As in the native versions, the exclusion witnesses come from an untrusted search and are
checked exactly. A further file compares the statement of each kernel theorem of Theorems~\ref{thm:refined}
to~\ref{thm:hetero} with the statement of its native version, and the two are identical; the two versions of
Theorem~\ref{thm:main} are stated by the same source text.

The certificates are read from the files of the supplement; the formal data files record the SHA-256 hash of
each certificate file. Programs outside Lean generate the node types, the tables, the heads and the other auxiliary data from which the
checks start. Because every item they produce is checked inside Lean, an error in them can only make a check fail. The
search for exclusion witnesses is likewise untrusted: the rows accept a window as excluded only after the witness found
by the search passes an exact check whose soundness is proved.

Two cross-checks support the model without being part of the proof. The node types computed in Lean coincide, as
strings including all coefficients, with the node types of the accompanying programs for all five models (the
eight-step circuit, the lean schedule built by those programs from its own circuit description through Stim, and the
three non-uniform models). All five models have the same 13{,}658 typed balls on the range of
Lemma~\ref{lem:locality2}.

\subsection{Cost}

Table~\ref{tab:lean-cost} lists the measured cost of the checks. Each check runs as a separate Lean process.

\begin{table}[ht]
\centering
\small
\begin{tabular}{lrrr}
\toprule
Checks & Files & Time & Memory \\
\midrule
Thm~\ref{thm:main}, kernel & 390 & 1.9 h & 13.0 GiB \\
Thm~\ref{thm:main}, native & 10 & 0.07 h & 3.5 GiB \\
Thm~\ref{thm:refined}(a), native & 71 & 1.5 h & 3.5 GiB \\
Thm~\ref{thm:refined}(b), native & 43 & 2.0 h & 3.6 GiB \\
Thm~\ref{thm:lean}(b), native & 71 & 1.7 h & 3.6 GiB \\
Thm~\ref{thm:lean}(c), native & 43 & 2.2 h & 3.6 GiB \\
Thm~\ref{thm:hetero}(b), three models, native & 213 & 6.6 h & 3.6 GiB \\
Thm~\ref{thm:hetero}(c), three models, native & 129 & 6.1 h & 3.6 GiB \\
Criteria of parts (a) of Thms~\ref{thm:lean} and~\ref{thm:hetero}, both versions & 6 & under 1 min & 3.7 GiB \\
Kernel versions: rows at the heads, ten certificates & 3{,}330 & 550 h & 6.9 GiB \\
Kernel versions: coverage, five models & 107 & 41 h & 9.9 GiB \\
Kernel versions: type tables & 550 & 12 h & 10.0 GiB \\
Kernel versions: search trees, factor bounds, other files & 790 & 1.1 h & 8.7 GiB \\
\bottomrule
\end{tabular}
\caption{Cost of the formal checks: number of files, sum over the files of the time per process, and the largest memory
of one process. The remaining files, which combine the checks and state the theorems of the native versions and of
Theorem~\ref{thm:main}, take about one minute in total and up to 4.0 GiB, and the comparison of the statements takes
5 s and 16.2 GiB.}
\label{tab:lean-cost}
\end{table}

\subsection{Reproduction}

The formal development is part of the supplement, with a README that lists the commands. First, the definitions and proofs
build with Lean's build tool. Then the scripts below compile the check files, each in its own Lean process and, except for
Theorem~\ref{thm:main}, with the precompiled computational modules (\texttt{QECComp}) loaded. Finally the files that combine the checks and state the theorems are compiled, and each prints the axioms
of its theorems:
\begin{verbatim}
lake build QEC QECComp
scripts/run_checks.sh     # Theorem 1.1, kernel
scripts/run_final.sh      # Theorem 1.1, native
scripts/run_checks8.sh    # Theorem 1.2(a)
for X in L He Hl H2; do   # Theorems 1.3(b), 8.1(b)
  scripts/run_checksW.sh $X
done
scripts/run_finalW.sh     # parts (a), theorem files
for X in S8 SL SHe SHl SH2; do   # 1.2(b), 1.3(c), 8.1(c)
  scripts/run_checksS.sh $X
done
scripts/run_finalS.sh     # profile tables, theorem files
\end{verbatim}
After these commands, one script builds the kernel versions of Theorems~\ref{thm:refined} to~\ref{thm:hetero} in
stages, one file per process; the README lists the stages and the numbers of parallel jobs. A final file,
\texttt{gen/kernel/StmtV3.lean}, compares their statements with those of the native versions and prints their axioms.

Table~\ref{tab:lean-files} maps the parts of this paper to the files of the development.

\begin{table}[ht]
\centering
\small
\begin{tabular}{p{0.42\textwidth}p{0.52\textwidth}}
\toprule
Part of the paper & File and main names \\
\midrule
Circuit, noise, frames (§\ref{sec:circuit}, §\ref{sec:noise}) & \texttt{QEC/Circuit/Frame.lean}, \texttt{Fault.lean}, \texttt{Instance.lean} (\texttt{circ}) \\
Experiment with many faults, $\Pfail$ & \texttt{QEC/Circuit/Experiment2.lean}, \texttt{Final.lean} (\texttt{PfailExp}) \\
Decoder, Lemma~\ref{lem:path}, Proposition~\ref{prop:sum}, Lemma~\ref{lem:criterion} & \texttt{QEC/Decoder/Reduction.lean}, \texttt{QEC/Graph/} \\
Theorem~\ref{thm:main} & \texttt{QEC/Thm11/Main.lean}, \texttt{QEC/Checks/Thm11V3.lean} (\texttt{thm11\_circuit\_kernel}), \texttt{QEC/ChecksN/Thm11V2.lean} (\texttt{thm11\_circuit\_native}) \\
Definition~\ref{def:excluded}, Lemma~\ref{lem:excluded}, Proposition~\ref{prop:labelled}, Lemma~\ref{lem:memory} & \texttt{QEC/Refined/Excl.lean}, \texttt{Labelled.lean}, \texttt{Memory.lean}, \texttt{Assembly.lean} \\
Rule (S) and the canonical minimizer & \texttt{QEC/Refined/ExclS.lean} (\texttt{not\_exclS}, \texttt{pfail\_le\_labelledS}), \texttt{ProfileS.lean} \\
Typed balls, rows, coverage (generic) & \texttt{QEC/Refined/Ball.lean}, \texttt{Witness.lean}, \texttt{RowsSem.lean}, \texttt{StartSem.lean}, \texttt{Cover.lean}, \texttt{Generic.lean} \\
Computational core & \texttt{QECComp/Basic.lean}, \texttt{Rows.lean}, \texttt{Cover.lean} \\
Theorem~\ref{thm:refined} & \texttt{QEC/Refined/Thm12.lean}, \texttt{QEC/ChecksN8/Thm12V2.lean} (\texttt{thm12\_circuit\_native}) \\
The lean schedule (§\ref{sec:lean}) & \texttt{QEC/Refined/Specs.lean} (\texttt{WL}), \texttt{LeanSem.lean} (\texttt{PfailLean}, \texttt{PfailLean\_eq}) \\
Theorem~\ref{thm:lean} & \texttt{QEC/ChecksNW/Thm13aV2.lean} (\texttt{thm13a\_lean\_native}), \texttt{Thm13bV2.lean} (\texttt{thm13b\_lean\_native}) \\
Non-uniform rates (§\ref{sec:hetero}) & \texttt{QEC/Refined/Weighted.lean}, \texttt{Specs.lean}, \texttt{Rates.lean} \\
Theorem~\ref{thm:hetero} & \texttt{QEC/ChecksNW/Thm81aV2.lean}, \texttt{Thm81bV2.lean} (\texttt{thm81b\_heron\_native} etc.) \\
Profile-weight theorems & \texttt{QEC/Refined/ThmS.lean}, \texttt{QEC/ChecksNS/Thm12bV2.lean} (\texttt{thm12b\_circuit\_native}), \texttt{Thm13cV2.lean} (\texttt{thm13c\_lean\_native}), \texttt{Thm81cV2.lean} (\texttt{thm81c\_heron\_native} etc.); rule (S) in the rows: \texttt{QECComp/RowsS.lean}, \texttt{QEC/Refined/RowsSemS.lean}, \texttt{GenericS.lean} \\
Kernel versions of Theorems~\ref{thm:refined}--\ref{thm:hetero} & \texttt{QECKernel/Fin/} (\texttt{thm12\_circuit\_kernel} etc.), \texttt{QECKernel/Bound.lean}, \texttt{BoundS.lean}, \texttt{AssemblyK.lean}; rule (S) in the kernel rows: \texttt{QECKernel/HeadsS.lean}; statement check: \texttt{gen/kernel/StmtV3.lean} \\
\bottomrule
\end{tabular}
\caption{Where the parts of the paper are formalized.}
\label{tab:lean-files}
\end{table}

\section{Remarks}\label{sec:remarks}

\begin{remark}[Comparison with \cite{Fow12}]\label{rem:fowler}
Fowler's argument uses unit weights, bounds the number of non-backtracking paths of length $m$ by $3n^2\,11^{m-1}$ and bounds each line probability by the largest one, for which it takes the value $14p/5$ of the circuits of \cite{WFH11}. In the circuit considered here the largest bulk coefficient is $72/15$, so that argument gives at most $1/(484\cdot\tfrac{72}{15})=4.3\times10^{-4}$, before the heavier boundary edges are taken into account. Two changes account for the improvement to $1.04\times10^{-3}$. First, log-likelihood weights let each edge contribute $2\sqrt{q_e}$ instead of $2\sqrt{q_{\max}}$. Second, the criterion of Lemma~\ref{lem:criterion} replaces the factor $11$ by an exact count of the twelve unequal edges at each node. At the bulk node with $\lambda=1$ the left side of the criterion is below $1$ at $p=1.0419\times10^{-3}$ but above $1$ at $p=1.0420\times10^{-3}$, so the method cannot reach beyond $1.042\times10^{-3}$. As $p\to0$ the bulk root of $\Sigma=1$ is $\lambda=\Lambda\sqrt p$ with $\Lambda=30.929$, the solution of $\sum_e2\sqrt{c_e}/(\Lambda+2\sqrt{c_e})=1$ over the bulk coefficients. With unit weights the same method gives $8.7\times10^{-4}$ in the bulk.
\end{remark}

\begin{remark}[Limits of the certificate]
Consider the rows of Section~\ref{sec:refined} computed from the instances with $d\le15$ and $T\le7$, with the exclusions at each $p$. Their growth rate is $0.99407$ at $p=1.6\times10^{-3}$ for the rules of part (a) with $s=0.42$, and $0.99744$ to $0.99751$ at $p=2\times10^{-3}$ for the rules of part (b) with $s=0.36$. But for every tilt $s$ it is above $1$ at $p=1.62\times10^{-3}$ for the rules of part (a) and at $p=2.05\times10^{-3}$ for those of part (b); for the lean schedule the same holds at $2.47\times10^{-3}$ and at $3.05\times10^{-3}$. These statements rest on lower and upper Collatz--Wielandt bounds computed in floating point on a grid of tilts, together with the log-convexity of the growth rate in $s$ \cite{Kin61}. Since the full range of $d$ and $T$ only adds rows, certificates of these kinds, with any tilt, cannot reach these values. Longer windows raise these values only slowly: on the bulk lattice, without boundaries, the rules of part (a) reach growth rate $1$ at $1.6185\times10^{-3}$ with windows of four edges and at $1.6936\times10^{-3}$ with windows of five edges. Rule (S) extends to runs of three or four correction edges: such a run can be excluded if an edge-disjoint route between its ends uses only edges between detectors, has the same multiset of profiles and has a smaller value of $\Phi$. This excludes more windows but leaves the growth rates at the values of $p$ above unchanged to five digits.
\end{remark}

\begin{remark}[Limits of arguments by increasing events]\label{rem:increasing}
Call a set of outcomes \emph{failing} if, when exactly these outcomes occur, some minimizer makes the decoder fail. An event is \emph{increasing} if it is preserved when outcomes are added. All bounds in this paper bound $\Pfail$ by the probability of an increasing event that contains the failing sets, and so does any bound obtained by counting paths, clusters or witnesses with a union bound. Rule (S) does not change this, because it too depends only on the labels and the graph. Every such event contains the event $U$ that some subset of the occurring outcomes is failing, and $U$ is itself increasing. Lemma~\ref{lem:window}(b) describes $U$: every subset $X$ of a minimizer has minimum weight among the sets with boundary $\partial X$. Hence if the decoder fails and $\gamma$ is the path of Lemma~\ref{lem:path}, then $\gamma\cap C$ is a minimizer for the error $\gamma\cap E$, which is produced by a subset of the occurring outcomes, and with this minimizer the decoder fails on that error alone. So $U$ occurs if and only if some simple path $\gamma$ from $b_1$ to $b_2$ contains a set $E'$ of edges, each produced by an occurring outcome, such that $\gamma\setminus E'$ has minimum weight among the sets with boundary $\partial E'$.

We estimated $\Pr(U)$ by Monte Carlo sampling for the memory experiment with $T=d$, deciding $U$ in each sample by integer programming. Samples that the program did not resolve within its round or time limit count as not in $U$, so the estimates are lower bounds; the share of such samples is below $1\%$ for $d\le9$ at $p\le4.25\times10^{-3}$ and about $3\%$ at $d=11$ and $p=4\times10^{-3}$. These estimates are not rigorous. For the circuit of Section~\ref{sec:circuit} and $d=5,7,9,11$, with $800$ to $2{,}550$ samples per point, $\Pr(U)$ decreases with $d$ at $p=3.5\times10^{-3}$ but increases with $d$ at $p=5\times10^{-3}$. At $p=4\times10^{-3}$ the four estimates agree within their statistical errors, at about $0.044$, and at $p=4.25\times10^{-3}$ they rise slightly from $d=7$ to $d=11$, by less than their statistical errors. For the lean schedule the estimates are roughly constant in $d$ at $6\times10^{-3}$ and increase from $d=5$ to $d=7$ at $7\times10^{-3}$. The threshold of $U$ for the 8-step circuit therefore lies between $3.5\times10^{-3}$ and $5\times10^{-3}$, probably near $4\times10^{-3}$, and no argument of this kind can prove a threshold above it. Where $\Pr(U)$ no longer decays but matching still succeeds, failing sets are present but are undone by the other outcomes, and a proof there would need an argument that is not monotone in the faults.
\end{remark}

\begin{remark}[Other schedules]
Each of the following modifications produces a circuit whose fault outcomes have the signatures and probabilities of a subset of our outcomes: deleting noise locations; merging (S8) with (S1) of the next round into a single measure-and-reset step; and preparing and measuring the X-type measure qubits in the $X$ basis directly, without (S2) and (S7). For such a circuit each coefficient is at most the corresponding $c_e$, so its edge weights $a_e$ are smaller, and Theorem~\ref{thm:main} holds for it with the same constants. In particular, the noisy circuits \texttt{surface\_code:rotated\_memory\_x/z} generated by Stim with all noise parameters equal to $p$ are of this kind. Theorem~\ref{thm:refined}, however, does not transfer in this way, because its exclusions compare coefficients of alternative paths, and these change when noise locations are removed. For the lean schedule, Theorem~\ref{thm:lean} provides sharper bounds.
\end{remark}

\begin{remark}[Weights]
Theorems~\ref{thm:main}--\ref{thm:lean} assume $q_e(1-q_e)\le r_e\le q_e$, and Theorems~\ref{thm:refined}(b) and~\ref{thm:lean}(c) also assume profile weights. Stim's detector error model replaces each depolarizing location by independent mechanisms. If these are projected to a sector and the mechanisms that produce the same edge are combined as independent events, then $1-2r_e=\prod_\ell(1-x_\ell)^{k_\ell/m_\ell}$, where $k_\ell$ outcomes of $\ell$ produce $e$, and $(x_\ell,m_\ell)$ is $(16p/15,8)$, $(4p/3,2)$ or $(2p,1)$ for two-qubit, single-qubit and flip locations. In our circuits $c_{\ell,e}$ determines $k_\ell$ and the kind of $\ell$, so these are profile weights, and for $d\le13$, $T\le7$ and $p\le3\times10^{-3}$ they lie in this range for both schedules. The heuristic decomposition of Stim's detector error model sometimes splits an outcome whose signature in the sector is $\{u,v\}$ into the two boundary edges at $u$ and $v$. This changes some edge probabilities by factors up to $2$, and a matching decoder built on that decomposition is not covered. But the canonical decomposition used here sends the $X$ part and the $Z$ part of each outcome to its unique edge in each sector.
\end{remark}

\begin{remark}[Numerical threshold]\label{rem:numerical}
We simulated this circuit with $d$ rounds and decoded it by matching on the decoding graph of Section~\ref{sec:decoder} with $r_e=q_e$, using PyMatching and $2\times10^5$ samples per point. The logical failure curves for $d=3,5,7,9$ cross near $p\approx5\times10^{-3}$. The rigorous values $p_{\ast\ast}=2\times10^{-3}$ and $\pst$ are thus smaller than this crossing by factors of about $2.5$ and $5$. For the lean schedule the curves cross near $p\approx8\times10^{-3}$, about $2.7$ times the value $3\times10^{-3}$ of Theorem~\ref{thm:lean}(c).
\end{remark}

\begin{remark}[Google's Willow schedule]\label{rem:willow}
Google's surface-code experiments on the Willow processor \cite{GQAI24} use a different circuit: the ZXXZ variant of the code, CZ gates conjugated by Hadamard gates, an echo pulse on all qubits in the middle of each round, and a fused measure-and-reset step. We built this circuit with the noise of Section~\ref{sec:noise} at the Willow rates of Table~\ref{tab:chips}, all multiplied by a factor $t$: CZ gates get the CX rate, Hadamard gates and echo pulses the $H$ rate, and the data qubits, idle during measurement and reset, the rates of steps (S8) and (S1). With the same noise rules, the circuits published with \cite{GData24} for $d=3,5,7$ in basis $X$ and $d=7$ in basis $Z$, with ten rounds, produce the same detector error model after three changes that do not alter it: the initial reset made explicit, the random Pauli layer at the start removed, and two consecutive resets merged. For $d\le15$ the decoding graph is graph-like in each sector, with twelve edges at each bulk node, and each bulk coefficient is at least the corresponding one of Lemma~\ref{lem:bulk}. Monte Carlo estimates, which are not rigorous, place the crossing of the logical failure curves at $t\approx1.39$. But the estimates of $\Pr(U)$, lower bounds as in Remark~\ref{rem:increasing} from $1{,}900$ to $8{,}000$ samples per point, decrease with $d$ at $t=0.9$ and stop decreasing between $t=0.9$ and $t=1$. We also decoded the detection events measured on the device \cite{GData24} with the decoder of Section~\ref{sec:decoder} for this circuit, separately in each sector. The resulting logical error rates per cycle, geometric means over patches and bases, are $9.9\times10^{-3}$, $6.6\times10^{-3}$ and $4.3\times10^{-3}$ for $d=3,5,7$, between $2.5$ and $3$ times what Google's decoders reach at $d=7$ \cite{GQAI24}, and the model reproduces them at $t\approx1.1$. For this decoder and in this model, the device thus operates at or above the threshold of $U$, where no argument by increasing events applies, while matching still suppresses errors.
\end{remark}

\section*{Code and data}
The programs, the certificates, the formal proofs and the outputs of all checks in Tables~\ref{tab:verify}--\ref{tab:verify4} are archived at \url{https://doi.org/10.5281/zenodo.23498518}.

\section*{Use of AI tools}
Generative AI tools were used to find and prove the results, to write the programs and the formal proofs, and to draft the text.

\appendix
\section{Node types}\label{app:types}
Each line gives one type: an example detector $(x,y,r)$ in $G_{9,5}$, the number of detectors of this type in $G_{9,5}$, the degree, the coefficients $15c_e$ of its edges (a superscript $\flat$ marks the edge to $b_1$ and $\sharp$ the edge to $b_2$), and the left side of \eqref{eq:check}, that is $\Sigma$ at $p=\pst$ and $\lambda=0.9997$, rounded up to four decimals. The first row is the bulk type.

\begin{table}[h!]\centering\scriptsize
\begin{tabular}{@{}llll r@{}}
\toprule
$(x,y,r)$ & \# & deg & $\{15c_e\}$ & $\Sigma$\\
\midrule
$(4,4,1)$ & 72 & 12 & $\{72,72,66,66,48,48,16,16,8,8,8,8\}$ & 0.9995 \\
$(2,6,1)$ & 12 & 11 & $\{72,70,66,66,48,48,22,16,8,8,8\}$ & 0.9629 \\
$(16,4,1)$ & 12 & 11 & $\{72,70,66,66,48,48,22,16,8,8,8\}$ & 0.9629 \\
$(4,16,1)$ & 12 & 9 & $\{148^{\sharp},72,66,66,48,16,8,8,8\}$ & 0.8334 \\
$(6,2,1)$ & 12 & 9 & $\{148^{\flat},72,66,66,48,16,8,8,8\}$ & 0.8334 \\
$(2,2,1)$ & 4 & 8 & $\{154^{\flat},70,66,66,48,16,8,8\}$ & 0.7897 \\
$(16,16,1)$ & 4 & 8 & $\{154^{\sharp},70,66,66,48,16,8,8\}$ & 0.7897 \\
$(4,4,5)$ & 21 & 8 & $\{66,51,51,39,39,16,8,8\}$ & 0.6737 \\
$(0,4,1)$ & 12 & 7 & $\{78,78,70,48,22,8,8\}$ & 0.6459 \\
$(18,6,1)$ & 12 & 7 & $\{78,78,70,48,22,8,8\}$ & 0.6459 \\
$(16,4,5)$ & 3 & 7 & $\{66,51,49,39,39,22,8\}$ & 0.6368 \\
$(4,4,0)$ & 21 & 8 & $\{66,41,41,29,29,16,8,8\}$ & 0.6298 \\
$(0,16,1)$ & 4 & 6 & $\{78,78,72^{\sharp},70,8,8\}$ & 0.5939 \\
$(18,2,1)$ & 4 & 6 & $\{78,78,72^{\flat},70,8,8\}$ & 0.5939 \\
$(2,6,0)$ & 3 & 7 & $\{66,41,39,29,29,22,8\}$ & 0.5927 \\
$(2,2,5)$ & 4 & 6 & $\{100^{\flat},66,51,39,16,8\}$ & 0.5711 \\
$(4,16,5)$ & 3 & 6 & $\{108^{\sharp},66,51,39,8,8\}$ & 0.5584 \\
$(4,16,0)$ & 4 & 6 & $\{80^{\sharp},66,41,29,16,8\}$ & 0.5359 \\
$(6,2,0)$ & 3 & 6 & $\{88^{\flat},66,41,29,8,8\}$ & 0.5239 \\
$(16,16,5)$ & 1 & 5 & $\{114^{\sharp},66,49,39,8\}$ & 0.5149 \\
$(0,4,5)$ & 3 & 6 & $\{78,51,39,22,8,8\}$ & 0.4920 \\
$(2,2,0)$ & 1 & 5 & $\{94^{\flat},66,39,29,8\}$ & 0.4807 \\
$(18,6,0)$ & 3 & 6 & $\{78,41,29,22,8,8\}$ & 0.4701 \\
$(0,16,5)$ & 1 & 5 & $\{78,63^{\sharp},51,8,8\}$ & 0.4421 \\
$(18,2,0)$ & 1 & 5 & $\{78,53^{\flat},41,8,8\}$ & 0.4235 \\
$(18,2,5)$ & 1 & 3 & $\{78,49,39^{\flat}\}$ & 0.3275 \\
$(18,6,5)$ & 3 & 3 & $\{78,49,39\}$ & 0.3275 \\
$(0,4,0)$ & 3 & 3 & $\{78,39,29\}$ & 0.3053 \\
$(0,16,0)$ & 1 & 3 & $\{78,39,29^{\sharp}\}$ & 0.3053 \\
\bottomrule
\end{tabular}
\caption{Node types in basis $Z$.}
\end{table}

\begin{table}[h!]\centering\scriptsize
\begin{tabular}{@{}llll r@{}}
\toprule
$(x,y,r)$ & \# & deg & $\{15c_e\}$ & $\Sigma$\\
\midrule
$(6,4,1)$ & 72 & 12 & $\{72,72,66,66,48,48,16,16,8,8,8,8\}$ & 0.9995 \\
$(4,2,1)$ & 12 & 11 & $\{72,70,66,66,48,48,22,16,8,8,8\}$ & 0.9629 \\
$(6,16,1)$ & 12 & 11 & $\{72,70,66,66,48,48,22,16,8,8,8\}$ & 0.9629 \\
$(2,4,1)$ & 12 & 9 & $\{148^{\flat},72,66,66,48,16,8,8,8\}$ & 0.8334 \\
$(16,6,1)$ & 12 & 9 & $\{148^{\sharp},72,66,66,48,16,8,8,8\}$ & 0.8334 \\
$(2,16,1)$ & 4 & 8 & $\{146^{\flat},72,66,66,48,22,8,8\}$ & 0.7975 \\
$(16,2,1)$ & 4 & 8 & $\{146^{\sharp},72,66,66,48,22,8,8\}$ & 0.7975 \\
$(4,2,5)$ & 21 & 8 & $\{66,51,51,39,39,16,8,8\}$ & 0.6737 \\
$(4,18,1)$ & 12 & 7 & $\{78,78,70,48,22,8,8\}$ & 0.6459 \\
$(6,0,1)$ & 12 & 7 & $\{78,78,70,48,22,8,8\}$ & 0.6459 \\
$(6,16,5)$ & 3 & 7 & $\{66,51,49,39,39,22,8\}$ & 0.6368 \\
$(6,4,0)$ & 21 & 8 & $\{66,41,41,29,29,16,8,8\}$ & 0.6298 \\
$(2,0,1)$ & 4 & 6 & $\{80^{\flat},78,78,48,22,8\}$ & 0.6083 \\
$(16,18,1)$ & 4 & 6 & $\{80^{\sharp},78,78,48,22,8\}$ & 0.6083 \\
$(4,2,0)$ & 3 & 7 & $\{66,41,39,29,29,22,8\}$ & 0.5927 \\
$(2,4,5)$ & 3 & 6 & $\{100^{\flat},66,51,39,16,8\}$ & 0.5711 \\
$(16,2,5)$ & 4 & 6 & $\{108^{\sharp},66,51,39,8,8\}$ & 0.5584 \\
$(16,6,0)$ & 3 & 6 & $\{80^{\sharp},66,41,29,16,8\}$ & 0.5359 \\
$(2,16,5)$ & 1 & 5 & $\{98^{\flat},66,51,39,22\}$ & 0.5348 \\
$(2,4,0)$ & 4 & 6 & $\{88^{\flat},66,41,29,8,8\}$ & 0.5239 \\
$(16,2,0)$ & 1 & 5 & $\{78^{\sharp},66,41,29,22\}$ & 0.4995 \\
$(6,0,5)$ & 3 & 6 & $\{78,51,39,22,8,8\}$ & 0.4920 \\
$(4,18,0)$ & 3 & 6 & $\{78,41,29,22,8,8\}$ & 0.4701 \\
$(2,0,5)$ & 1 & 5 & $\{78,61^{\flat},39,22,8\}$ & 0.4558 \\
$(16,18,0)$ & 1 & 5 & $\{78,51^{\sharp},29,22,8\}$ & 0.4350 \\
$(4,18,5)$ & 3 & 3 & $\{78,49,39\}$ & 0.3275 \\
$(16,18,5)$ & 1 & 3 & $\{78,49^{\sharp},39\}$ & 0.3275 \\
$(2,0,0)$ & 1 & 3 & $\{78,39^{\flat},29\}$ & 0.3053 \\
$(6,0,0)$ & 3 & 3 & $\{78,39,29\}$ & 0.3053 \\
\bottomrule
\end{tabular}
\caption{Node types in basis $X$.}
\end{table}

\clearpage
\begin{thebibliography}{10}
\bibitem{DKLP02} E.~Dennis, A.~Kitaev, A.~Landahl and J.~Preskill, \emph{Topological quantum memory}, J. Math. Phys. \textbf{43} (2002), 4452--4505.
\bibitem{FMMC12} A.~G.~Fowler, M.~Mariantoni, J.~M.~Martinis and A.~N.~Cleland, \emph{Surface codes: Towards practical large-scale quantum computation}, Phys. Rev. A \textbf{86} (2012), 032324.
\bibitem{Fow12} A.~G.~Fowler, \emph{Proof of finite surface code threshold for matching}, Phys. Rev. Lett. \textbf{109} (2012), 180502.
\bibitem{Gid21} C.~Gidney, \emph{Stim: a fast stabilizer circuit simulator}, Quantum \textbf{5} (2021), 497.
\bibitem{TS14} Y.~Tomita and K.~M.~Svore, \emph{Low-distance surface codes under realistic quantum noise}, Phys. Rev. A \textbf{90} (2014), 062320.
\bibitem{AGP06} P.~Aliferis, D.~Gottesman and J.~Preskill, \emph{Quantum accuracy threshold for concatenated distance-3 codes}, Quantum Inf. Comput. \textbf{6} (2006), 97--165.
\bibitem{KP13} A.~A.~Kovalev and L.~P.~Pryadko, \emph{Fault tolerance of quantum low-density parity check codes with sublinear distance scaling}, Phys. Rev. A \textbf{87} (2013), 020304(R).
\bibitem{Got14} D.~Gottesman, \emph{Fault-tolerant quantum computation with constant overhead}, arXiv:1310.2984.
\bibitem{WFH11} D.~S.~Wang, A.~G.~Fowler and L.~C.~L.~Hollenberg, \emph{Surface code quantum computing with error rates over 1\%}, Phys. Rev. A \textbf{83} (2011), 020302(R).
\bibitem{YLY26} S.~Yoshida, E.~Lake and H.~Yamasaki, \emph{Proof of a finite threshold for the union-find decoder}, arXiv:2602.20238.
\bibitem{GQAI24} Google Quantum AI and Collaborators, \emph{Quantum error correction below the surface code threshold}, arXiv:2408.13687.
\bibitem{USTC26} K.~Zhang, Z.~Yi, S.~Guo et al., \emph{Learning to decode in parallel: self-coordinating neural network for real-time quantum error correction}, arXiv:2601.09921, Table 2.
\bibitem{QHelios} Quantinuum, \emph{Quantinuum Helios product data sheet}, version 1.2, June 9, 2026, Table 1.
\bibitem{QH2} Quantinuum, \emph{System Model H2 product data sheet}, version 4.00, September 17, 2025, Table 1.
\bibitem{GWillow} Google Quantum AI, \emph{Willow spec sheet}, December 9, 2024.
\bibitem{GData24} Google Quantum AI, \emph{Data for ``Quantum error correction below the surface code threshold''}, Zenodo (2024), \url{https://doi.org/10.5281/zenodo.13273331}.
\bibitem{IBMQ} IBM Quantum Platform, calibration data of the processor ibm\_boston (Heron r3), read on October 18, 2026.
\bibitem{Kin61} J.~F.~C.~Kingman, \emph{A convexity property of positive matrices}, Quart. J. Math. Oxford \textbf{12} (1961), 283--284.
\end{thebibliography}

\end{document}