\documentclass[11pt]{amsart} \pdfsuppressptexinfo=-1 \usepackage[margin=1.1in]{geometry} \usepackage{amsmath,amssymb,amsthm,mathtools} \usepackage{booktabs,enumitem,array} \usepackage{tikz} \usepackage[hidelinks]{hyperref} \hypersetup{pdftitle={Certified lower bounds on the optimal-decoding threshold of the surface code},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}} \newcommand{\PML}{P_{\mathrm{ML}}} \newcommand{\PMW}{P_{\mathrm{MW}}} \newcommand{\TV}{\operatorname{TV}} \newcommand{\Long}{\mathrm{Long}} \newcommand{\cut}{\mathrm{cut}} \newcommand{\inter}{\mathrm{int}} \newcommand{\core}{\mathrm{core}} \newcommand{\eL}{\varepsilon_{\mathrm{L}}} \newcommand{\eps}{\varepsilon} \newcommand{\Ctop}{C_{\mathrm{top}}} \newcommand{\bad}{\mathrm{bad}} \newcommand{\Gbot}{G_{\mathrm{bot}}} \newcommand{\Gtop}{G_{\mathrm{top}}} \newcommand{\Sbot}{S_{\mathrm{bot}}} \newcommand{\Stop}{S_{\mathrm{top}}} \newcommand{\Ut}{\tilde U_0} \newcommand{\Tt}{\tilde T} \begin{document} \title[Lower bounds on the surface-code threshold]{Certified lower bounds on the optimal-decoding threshold of the surface code} \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{November 2026} \subjclass[2020]{81P73; 94B35, 82B44, 62F25, 68V20} \keywords{Quantum error correction, surface code, toric code, threshold, maximum-likelihood decoding, minimum-weight matching, random-bond Ising model, Nishimori line, statistical certificate, computer-assisted proof, Lean} \begin{abstract} Under independent bit flips, rigorous lower bounds on the threshold of the surface code from earlier work stay below $0.04$, while numerical estimates place the optimal threshold near $0.109$. By counting labelled failure paths with exact transfer-matrix certificates, we prove without sampling that every minimum-weight decoder has threshold at least $0.0465$ on the planar and rotated codes. We then give statistical certificates that, with confidence $1-10^{-9}$ each, the optimal threshold of the planar code is at least $0.103$ under bit flips and at least $0.02$ under phenomenological noise. Each statistical certificate bounds the failure probability of an auxiliary decoder that divides the code into blocks and corrects each block using a window around it; optimal decoding does at least as well, so the bound also holds for optimal decoding. A deterministic lemma shows that the auxiliary decoder fails only if bad blocks, in which the window corrections leave a defect or a long residual path, form a sparse hierarchy that joins the two rough boundaries. This gives an explicit bound once every block is bad with probability below a limit, about $4\times10^{-4}$ under bit flips, and a pre-registered Monte Carlo experiment bounds these probabilities. The confidence rests on a binomial model of the counts of bad blocks and on two tested properties of each decoding program. All these results are proved in the proof assistant Lean~4, the statistical ones with the binomial model and the two properties as hypotheses. \end{abstract} \maketitle \section{Introduction}\label{sec:intro} The surface code \cite{Kit03,DKLP02} stores a logical qubit reliably as long as the physical error rate stays below a threshold. In the simplest setting, code capacity, each qubit suffers a bit flip independently with probability $p$ and the syndrome is measured without error. Decoding one error sector is then a problem on a planar graph. For optimal decoding, which picks the most likely logical class given the syndrome, this problem is the random-bond Ising model on the Nishimori line \cite{Nis81,DKLP02}, and the optimal threshold is believed to be the Nishimori point, estimated numerically as $0.10917(3)$ \cite{PPV09}. Minimum-weight matching, the standard efficient decoder, has a threshold near $0.1031$ in simulations \cite{WHP03}. Rigorous lower bounds are much smaller. Dennis, Kitaev, Landahl and Preskill \cite{DKLP02} showed that minimum-weight decoding, and hence optimal decoding, succeeds with probability tending to one for $p$ below a constant, which their argument puts at $0.0373$. For the toric code, a decoding failure produces a homologically nontrivial cycle on which at least half of the edges are errors, and the expected number of such cycles decays for these $p$. The value $0.0373$ uses a numerical estimate of the connective constant $\mu$ of self-avoiding walks on the square lattice; with the proven bound $\mu\le2.662343$ \cite{Cou22} the same argument gives $0.0366$. To our knowledge, no larger rigorous code-capacity threshold has been published for either decoder. Other rigorous bounds, from a recent method for general local noise channels \cite{KM26} and from the bounds for low-density parity-check codes of \cite{DKP15} (see also \cite{KP13}), are lower. Table~\ref{tab:prior} collects these values, together with those for measurement errors at the same rate as qubit errors. \begin{table}[ht] \centering \small \begin{tabular}{@{}>{\raggedright\arraybackslash}p{0.36\textwidth}>{\raggedright\arraybackslash}p{0.27\textwidth}>{\raggedright\arraybackslash}p{0.27\textwidth}@{}} \toprule & bit flips & bit flips and measurement errors \\ \midrule numerical estimate, optimal decoding & $0.10917(3)$ \cite{PPV09} & about $0.033$ \cite{OAIM04} \\ numerical estimate, matching & $0.1031$ \cite{WHP03} & $0.0293(2)$ \cite{WHP03} \\ earlier rigorous bound, minimum weight (hence optimal) & $0.0366$ \cite{Cou22,DKLP02} & $0.0112$ \cite{DKLP02,PT00} \\ earlier rigorous bounds, other methods & $0.034$ \cite{KM26}; about $0.029$ for the toric code \cite{DKP15} & \\ this paper, minimum weight (hence optimal) & $0.0465$ (Theorems~\ref{thm:planar}--\ref{thm:toric}) & $0.016$ (Theorem~\ref{thm:phenom}) \\ this paper, optimal, statistical & $0.103$ (Theorem~\ref{thm:ml}) & $0.02$ (Theorem~\ref{thm:d1}) \\ \bottomrule \end{tabular} \caption{Thresholds of the surface code under independent noise. The earlier rigorous bounds in the third row are those of the argument of \cite{DKLP02} with the proven bounds $2.662343$ \cite{Cou22} and $4.739$ \cite{PT00} on the connective constants of self-avoiding walks on the square and the cubic lattice; with numerical estimates of these constants, the authors of \cite{DKLP02} report $0.0373$ and $0.0114$. The value $0.0465$ is for the planar and rotated codes; for the toric code we prove $0.046$. The statistical results hold with the confidence of Section~\ref{sec:conf}.} \label{tab:prior} \end{table} On the side of statistical mechanics, Horiguchi and Morita extended the Peierls argument to the $\pm J$ model on the square lattice and showed that a ferromagnetic phase exists when the fraction of antiferromagnetic bonds is below $1-0.97394\approx0.026$ \cite{HM82}. Rigorous results on phase transitions along the Nishimori line in finite dimensions remain scarce \cite{OO26}; for continuous spins in three dimensions see \cite{GS22}. Numerically, the phase boundary of the square-lattice model is reentrant below the Nishimori point \cite{AH04,PPV09}, so the matching threshold lies below the optimal one. Reentrance has been proved, with computer assistance, for a decorated square lattice with independent $\pm J$ couplings \cite{Pei26}. Thresholds proved for renormalization-group and cellular-automaton decoders are many orders of magnitude smaller \cite{BH11,KuP19}. Under circuit-level noise, the path argument gives $1.7\times10^{-4}$ for the circuit model of \cite{DKLP02}, matching thresholds of $7.4\times10^{-4}$ \cite{Fow12} and $2\times10^{-3}$ \cite{Tom26} have been proved, each for its own circuit and noise model, and the union-find and greedy decoders are known to have finite thresholds \cite{YLY26}. Critical points have been certified statistically in percolation. The method of Balister, Bollob\'as and Walters \cite{BBW05} turns Monte Carlo estimates into confidence intervals with exactly computed error probabilities, and it gives intervals of width at most $5\times10^{-4}$ at confidence $99.9999\%$ for the site and bond percolation thresholds of the eleven Archimedean lattices \cite{RW07}. We are not aware of a comparable certificate for an error-correction threshold. \subsection{Results} Without sampling, every minimum-weight decoder, and hence maximum-likelihood decoding, has threshold at least $0.0465$ on the planar and rotated codes and at least $0.046$ on the toric code (Theorems~\ref{thm:planar}--\ref{thm:toric}). Under phenomenological noise, in which data qubits and syndrome bits fail independently with the same probability, every minimum-weight decoder of the planar code has threshold at least $0.016$ (Theorem~\ref{thm:phenom}). With sampling, maximum-likelihood decoding of the planar code has threshold at least $0.103$ under independent bit flips (Theorem~\ref{thm:ml}) and at least $0.02$ under phenomenological noise (Theorem~\ref{thm:d1}). These two are statistical results. They hold with the confidence defined in Section~\ref{sec:conf}, which is based on registered Monte Carlo experiments, on a binomial model of their counts and on two tested properties of the decoding programs. For Theorem~\ref{thm:ml}, the registration required one test of these properties to be run at the registered block and window size before the launch, but this test was run only after the analysis (Section~\ref{sec:cert-exp}). The bounds of these two theorems become useful only at distances of order $10^{5}$. Table~\ref{tab:prior} compares these thresholds with earlier ones, and Section~\ref{sec:results} states all results with their constants. \subsection{Methods}\label{sec:intro-methods} The argument of \cite{DKLP02} bounds the failure probability by the probability of an increasing event, one that is preserved when errors are added: the presence of a long path on which at least half of the edges are errors. Every argument that applies a union bound to paths, clusters or other sets that the error must contain does the same, and for matching, Monte Carlo estimates suggest that no such argument reaches $p=0.093$ (Section~\ref{sec:disc-mono}). The sampling-free bounds stay in this class of arguments and push it further by exact counting; the statistical certificates leave it. For the sampling-free bounds (Section~\ref{sec:count}) we fix a failing minimum-weight correction $C^\ast$ that minimizes a linear tie-break functional. Its symmetric difference with the error contains a path between the rough boundaries whose edges are labelled as errors or corrections. Exchanging a short stretch of the path for a geodesic, or its correction edges for a shortest pairing of their odd-degree checks, gives another failing correction (Figure~\ref{fig:path}); since $C^\ast$ has least weight and, among failing minimizers, least functional, many labelled stretches cannot occur. The remaining labelled walks are counted by a transfer matrix with finite memory, and an integer potential that satisfies every row of the matrix certifies that their growth rate is below one for label weights that bound the probability of each walk (Section~\ref{cnt:count}). For the certificate of Theorem~\ref{thm:ml} we bound optimal decoding by an auxiliary decoder. It divides the code into square blocks (Figure~\ref{fig:blocks}). For each block it computes a minimum-weight correction on a window around the block, with edge weights given by the marginals of the window posterior, and keeps the edges that the block owns. A block is bad if the combined first-stage correction leaves a defect in it or a residual path from it to $\ell_\infty$ distance $L$; adding errors can remove both, so this event is not increasing. A deterministic lemma (Section~\ref{sec:cert-lemma}) shows that a failure of the decoder forces a sparse hierarchy of bad blocks, which gives an explicit bound on the failure probability once blocks are bad with probability below a limit, about $4\times10^{-4}$ for the block and window sizes of Theorem~\ref{thm:ml} (Appendix~\ref{s1:sec:numbers}). Under the two tested properties of the program (Section~\ref{sec:conf}), whether a block is bad depends only on the errors near it, and blocks in equivalent positions are bad with the same probability, so only one number per kind of block has to be bounded. Monte Carlo sampling bounds these numbers with exact binomial confidence bounds, in the manner of the percolation certificates mentioned above. Optimal decoding does at least as well as the auxiliary decoder, and the failure probability of optimal decoding is non-decreasing in $p$ and in the width and non-increasing in the distance (Section~\ref{sec:reduction}), so the bound at a single value of $p$, for codes made of whole blocks, gives a threshold. Sections~\ref{sec:phenom} and~\ref{sec:cert-meas} carry both methods over to phenomenological noise, on its three-dimensional decoding graph. All theorems of Section~\ref{sec:setting} are proved in Lean~4 \cite{dMU21} with Mathlib \cite{mathlib20} (Section~\ref{sec:lean}), with the conditions of Theorems~\ref{thm:ml} and~\ref{thm:d1} taken as hypotheses; Section~\ref{sec:lean-trust} lists what the formal proofs do not cover. \subsection{Organization} Section~\ref{sec:setting} defines the codes and decoders, states the main results, explains the confidence statement and reduces Theorem~\ref{thm:ml} to a bound for the auxiliary decoder. Section~\ref{sec:count} proves the sampling-free bounds for bit flips and Section~\ref{sec:phenom} the sampling-free bound for measurement errors. Section~\ref{sec:cert} describes the auxiliary decoder, proves the deterministic bound and reports the two certificates. Section~\ref{sec:lean} describes the formal proofs, and Section~\ref{sec:discussion} discusses the limits of these methods. Appendix~\ref{app:proof} proves Theorem~\ref{thm:cert} in full. Two supplements accompany the paper (see Code and data): the records of the experiments and of the formal checks, and the proof of a criterion for a threshold of optimal decoding in terms of quantities of a single finite window, which Section~\ref{sec:disc-stat} states informally. \section{Setting and main results}\label{sec:setting} \subsection{Decoding graphs}\label{sec:graphs} All results concern one error sector of a surface code under independent errors, so they are statements about a decoding graph. A \emph{decoding graph} $G$ has a set $V$ of checks, in some cases two boundary vertices $b_1,b_2$ that carry no parity constraint, and a finite set of edges, the error locations; an edge between a check and a boundary vertex is a \emph{half-edge}. Under independent noise of strength $p$, the error $E$ contains each edge independently with probability $p$. The syndrome $\partial E\subseteq V$ is the set of checks of odd degree in $E$. A \emph{correction} is a set $C$ of edges with $\partial C=\partial E$. If $G$ has boundary vertices, $C$ \emph{fails} when $|C\cap\delta(b_1)|$ and $|E\cap\delta(b_1)|$ have different parity, where $\delta(b_1)$ is the set of half-edges at $b_1$; in particular, $E\oplus C$ then contains a path from $b_1$ to $b_2$. For the toric code, $C$ fails when $E\oplus C$ is homologically nontrivial. We use the following graphs; the rotated code and the toric code are written in coordinates in Section~\ref{sec:count}. \begin{enumerate}[label=(\alph*),leftmargin=2em] \item The \emph{planar code} $\mathcal P_{d,w}$ of distance $d\ge2$ and width $w\ge1$: checks $(x,y)$ with $0\le x\le w-1$ and $0\le y\le d-2$, an edge between any two checks at Euclidean distance $1$, and a half-edge from each check $(x,0)$ to $b_1$ and from each check $(x,d-2)$ to $b_2$. The bottom and top sides are rough and the left and right sides smooth. For $w=d$ this is one error sector of the unrotated planar code of distance $d$; under independent $X$ and $Z$ errors the other sector is the same graph rotated by a right angle, so for square codes the statements below apply to it by symmetry. \item The \emph{rotated code} $\mathcal R_d$ of odd distance $d$: the checks are the $X$ checks of the rotated surface code with $d^2$ qubits, and the errors are $Z$ errors. Each qubit is an edge between the two $X$ checks that contain it; a qubit that lies in only one $X$ check is a half-edge to $b_1$ or to $b_2$, according to the rough side on which it lies. \item The \emph{toric code} $\mathcal T_m$ of side $m$: checks $\mathbb Z_m^2$, each joined to its right and upper neighbour. \item The \emph{phenomenological graph} $\mathcal Q_{d,w,T}$ of the planar code with $T\ge0$ noisy rounds of syndrome measurement and a final perfect round: vertices $(t,x,y)$ with $0\le t\le T$, $0\le x\le w-1$ and $0\le y\le d-2$, an edge between any two vertices at distance $1$ (space-like edges are data errors, time-like edges are errors of syndrome bits), and half-edges from $(t,x,0)$ to $b_1$ and from $(t,x,d-2)$ to $b_2$. Every edge has the same probability $p$, so data qubits and syndrome bits fail at the same rate. \end{enumerate} \subsection{Decoders}\label{sec:decoders} A \emph{decoder} maps each syndrome to a logical class, possibly at random; it fails on $E$ when it outputs a class other than that of $E$. The \emph{maximum-likelihood} (ML) decoder outputs a class of largest posterior probability given the syndrome; it minimizes the failure probability among all decoders, randomized ones included. We write $\PML(G,p)$ for its failure probability. A \emph{minimum-weight decoder} outputs a correction of least size $|C|$. Our counting bounds concern \[ \PMW(G,p)=\Pr\bigl(\text{some correction of least size fails}\bigr), \] so they hold for every rule of breaking ties. Every minimum-weight decoder with a fixed tie rule is a decoder, so $\PML(G,p)\le\PMW(G,p)$. A decoder has threshold at least $p_\ast$ on a family of codes if its failure probability tends to zero as $d\to\infty$ for every $p0$, then for every $p\in[0,0.103]$ the probability $\PML(\mathcal P_{d,w},p)$ tends to $0$ and is at most $e^{-(d-1)/70400}$ for all large $d$. Hence the optimal threshold of the planar code under independent bit flips is at least $0.103$. \end{theorem} For $n_x=n_y=n$, as for $w=d-1=nL$, the right side of \eqref{eq:ml} is below $0.1$ from $n=1379$ and below $10^{-3}$ from $n=1700$, that is, from distance $485{,}409$ and $598{,}401$. For square codes, $w=d$, we have $n_x=n_y+1$, and the two values of $n_y$ are the same, $1379$ and $1700$. These are the constants of the Lean proof; sharper constants are given in Remark~\ref{rem:sharper}. \begin{theorem}[optimal decoding with measurement errors at $p=0.02$]\label{thm:d1} Let $L=35$ be the block side of the registered program of Section~\ref{sec:cert-meas}. For $w\ge1$, $T\ge0$ and $d\ge5L+1$ put $n_x=\max(5,\lceil w/L\rceil)$, $n_t=\max(5,\lceil (T+1)/L\rceil)$ and $n_y=\lfloor (d-1)/L\rfloor$. With confidence $1-10^{-9}$, under the conditions \textup{(V6)}, \textup{(Hcov)} and \textup{(Bin)} for this program (Section~\ref{sec:conf}), the following holds: for every $p\in[0,0.02]$, every $w\ge1$, every $T\ge0$ and every $d\ge5L+1$, \begin{equation}\label{eq:d1} \PML(\mathcal Q_{d,w,T},p)\le 804\,n_tn_x\,e^{-0.1008\,(n_y-47)}+5.11\times10^{6}\,n_tn_x\,e^{-0.007\,(n_y-47)} . \end{equation} In particular, under these conditions and with this confidence, if $w\ge1$ and $T$ are functions of $d$ that grow subexponentially, that is, $w\,e^{-cd}\to0$ and $T\,e^{-cd}\to0$ as $d\to\infty$ for every $c>0$, then for every $p\in[0,0.02]$ the probability $\PML(\mathcal Q_{d,w,T},p)$ tends to $0$ and is at most $e^{-(d-1)/28000}$ for all large $d$. Hence the optimal threshold of the planar code under phenomenological noise is at least $0.02$. \end{theorem} For $n_t=n_x=n_y=n$, as for $T+1=w=d-1=nL$, the right side of \eqref{eq:d1} is below $0.1$ from $n=5018$ and below $10^{-3}$ from $n=5713$, that is, from distance $175{,}631$ and $199{,}956$. As for Theorem~\ref{thm:ml}, these constants come from the Lean proof; they are not optimized. \subsection{The confidence statement}\label{sec:conf} Theorem~\ref{thm:ml} rests on a fixed program, the first stage of the auxiliary decoder of Section~\ref{sec:cert}, and on a random experiment that was registered before it ran. The bound \eqref{eq:ml} is a deterministic statement $S$. The Lean proof derives $S$ from (V6), (Hcov) and the hypothesis that seven unknown numbers $\varepsilon_t$ are at most $3.29\times10^{-4}$, where $\varepsilon_t$ is the probability that a reference block of type $t\in\{L0,L1,L2,\mathrm{bulk},R2,R1,R0\}$ is bad under independent bit flips at $p=0.103$ (Section~\ref{sec:cert-exp}). The experiment is sequential. The samples of each type are drawn in a fixed order, and each type is examined at three looks, after its first $n_1=125{,}040$, $n_2=187{,}560$ and $n_3=250{,}080$ samples. A type is accepted at the first look $j$ at which at most $c_j$ of these $n_j$ samples are bad, where $(c_1,c_2,c_3)=(7,19,32)$, and its sampling stops there. The experiment accepts if every type is accepted at one of its looks. \begin{definition}\label{def:conf} A statement $S$ holds \emph{with confidence $1-\delta$} for a registered experiment if the experiment accepted and $\Pr(\text{the experiment accepts and } S \text{ is false})\le\delta$, where the probability is over the randomness of the experiment. \end{definition} The conditions are the following. \begin{enumerate}[label=(\textup{\arabic*}),leftmargin=2em] \item[(V6)] The first stage of the decoder reads only the syndrome: for every code size and every block, its output on the block depends on the error only through the syndrome in the window of the block. \item[(Hcov)] The first stage commutes with translations: if a code is embedded in a larger one at an offset by whole blocks, with the sides that a block touches aligned, then the larger code's output on the image of a block is the image of the smaller code's output on the block, for every syndrome. \item[(Bin)] For each type $t$ and each look $j$, the number of bad samples among the first $n_j$ samples of type $t$ has the binomial law with parameters $n_j$ and $\varepsilon_t$. \end{enumerate} Conditions (V6) and (Hcov) are properties of the registered program. The validations V2, V4 and V6 of Section~\ref{sec:cert-exp} tested them and found no mismatch. V6 at the registered geometry $(352,527)$ ran only after the analysis, although the registration required it before the first sample (Section~\ref{sec:cert-exp}). Table~\ref{tab:conditions} lists, for both certificates, what supports each condition and when it was tested. Validations are finite tests, so (V6) and (Hcov) remain validated hypotheses about the registered program, not proved facts. Condition (Bin) treats the pseudo-random numbers as independent uniform draws; it holds if the bad indicators of the samples of each type, in their fixed order, are independent and each equal to $1$ with probability $\varepsilon_t$. The rounding of the flip probability is handled on paper, outside the formal proof. The sampler compares a uniform number in binary arithmetic with the floating-point number nearest to $0.103$, so its flip probability exceeds $0.103$ by less than $10^{-16}$. A sample uses fewer than $8.92\times10^{6}$ edges, so each $\varepsilon_t$ changes by less than $9.9\times10^{-10}$. This change is far inside the margins of the acceptance rule. Each threshold $c_j$ is the largest count whose exact one-sided Clopper--Pearson upper bound~\cite{CP34} for $\varepsilon_t$ at level $10^{-9}/3$, from $n_j$ samples, is at most $3.29\times10^{-4}$, and the largest of these three bounds is $3.2632\times10^{-4}$, rounded up. So a type passes a given look with probability at most $10^{-9}/3$ whenever its bad probability is at least $3.2632\times10^{-4}$, and at the flip probability of the sampler a type with $\varepsilon_t>3.29\times10^{-4}$ is bad with probability above $3.29\times10^{-4}-9.9\times10^{-10}>3.2632\times10^{-4}$. Condition (Bin) also identifies the blocks sampled by the experiment with the reference blocks (Section~\ref{sec:cert-exp}); each sampled block lies in a patch of the code that contains all edges on which its bad event depends. Only the marginal law of each count at each look enters. The experiment accepted (Table~\ref{tab:cert-counts}). Under (V6), (Hcov) and (Bin), if $S$ is false, then some type $t^\ast$, determined by the unknown numbers $\varepsilon_t$, has $\varepsilon_{t^\ast}>3.29\times10^{-4}$, and the experiment can accept only if $t^\ast$ is accepted at one of its three looks; by the previous paragraph this has probability at most $3\cdot10^{-9}/3=10^{-9}$. This is the confidence $1-10^{-9}$ of Theorem~\ref{thm:ml}. The level $10^{-9}$ is not divided among the seven types: the experiment accepts only if every type is accepted, that is, it rejects the union of the seven hypotheses $\varepsilon_t>3.29\times10^{-4}$ only if it rejects each of them, and such an intersection--union test has the level of its component tests~\cite{Ber82}. The exact sum of the three binomial tail probabilities at $3.29\times10^{-4}$ is $4.78\times10^{-10}$. The confidence $1-10^{-9}$ is that of a single experiment: no other experiment was registered for this statement, and during the run the counts were read only by an automated step that took each look and reported its decision and nothing else (Section~\ref{sec:cert-exp}). Section~\ref{sec:cert-exp} also lists every certificate experiment registered for this paper or its earlier versions, with a bound for all of them together. \begin{remark}[sharper constants]\label{rem:sharper} For each type, the exact one-sided Clopper--Pearson upper bound for $\varepsilon_t$ at level $10^{-9}/3$, at the look that accepted the type, is at most $3.13149\times10^{-4}$ (rounded up; the largest is that of the bulk type, accepted at the first look with $7$ bad samples). So all seven bounds are below $\hat\varepsilon=3.1315\times10^{-4}$, with a margin larger than the effect of the rounding of the flip probability. With confidence $1-10^{-9}$, all seven true probabilities are at most $\hat\varepsilon$: if the largest of them exceeded $\hat\varepsilon$, the type that attains it would exceed its own bound, and for a fixed type this happens at one of its three looks with probability at most $3\cdot10^{-9}/3$. Evaluating the bound of Section~\ref{sec:cert} at $\hat\varepsilon$ in place of $3.29\times10^{-4}$, with the level parameter $a_1=16$ that minimizes the bound there, as the registration prescribes, gives \[ \PML(\mathcal P_{d,w},p)\le 544\,n_x\,e^{-0.1666\,(n_y-40)}+1.70\times10^{5}\,n_x\,e^{-0.0296\,(n_y-40)} \] under the same conditions and with the same confidence $1-10^{-9}$. For $n_x=n_y=n$ it is below $0.1$ from $n=749$ and below $10^{-3}$ from $n=911$, that is, from distance $263{,}649$ and $320{,}673$; for square codes the two values of $n_y$ are the same, $749$ and $911$. This bound depends on the numerical evaluation of Appendix~\ref{s1:sec:numbers}, which Lean does not check (Section~\ref{sec:lean-trust}). \end{remark} Theorem~\ref{thm:d1} rests in the same way on a second registered experiment, with the program of Section~\ref{sec:cert-meas}. Its blocks are cubes of side $L=35$ in the coordinates $(t,x,y)$ of $\mathcal Q_{d,w,T}$, and its window radius is $R=34$. For this program, (V6) and (Hcov) are the statements above, with translations by whole blocks in each of the three directions. Condition (Bin) says that for each of the $25$ block types $t$ the number of bad samples has the binomial law with parameters $n=3\times10^{6}$ and $\varepsilon_t$, where $\varepsilon_t$ is the probability that the reference block of type $t$ is bad at $p=0.02$; as above, it also identifies the sampled blocks with the reference blocks. The experiment accepts if no type has more than $14$ bad samples. Under (V6), (Hcov) and (Bin), if some $\varepsilon_t>1.85\times10^{-5}$ then the probability of acceptance is at most $10^{-9}$, and otherwise \eqref{eq:d1} holds. The experiment accepted (Table~\ref{tab:cert-meas}), which gives the confidence $1-10^{-9}$ of Theorem~\ref{thm:d1}. Its validations of (V6) and (Hcov) at the registered radius ran only after the analysis (Table~\ref{tab:conditions}). The flip probability of its sampler exceeds $0.02$ by less than $1.8\times10^{-17}$, which changes each $\varepsilon_t$ by less than $3\times10^{-10}$. A type passes with probability at most $4\times10^{-11}$ whenever its bad probability is at least the Clopper--Pearson bound at $k=14$, and this bound lies more than $10^{-7}$ below $1.85\times10^{-5}$. So this rounding does not affect the confidence either. \begin{table}[ht] \centering \small \begin{tabular}{@{}>{\raggedright\arraybackslash}p{0.11\textwidth}p{0.41\textwidth}p{0.41\textwidth}@{}} \toprule condition & certificate at $p=0.103$ ($L=352$, $R=527$) & certificate at $p=0.02$ ($L=35$, $R=34$) \\ \midrule (V6) & V6 at $(L,R)=(8,11)$, $(16,23)$ and $(24,35)$ before the registration; at the registered $(352,527)$ only after the analysis, although the registration required it before the first sample (Section~\ref{sec:cert-exp}) & V6 at $(9,4)$ before the registration; at $R=L-1$ only after the analysis, at $(9,8)$ and $(35,34)$ \\ (Hcov) & the window-local design (Section~\ref{sec:cert-decoder}); V2 and V4 at $(8,11)$, $(16,23)$ and $(24,35)$ before the registration & V2 and V4 at $(9,4)$ before the registration; at $R=L-1$ only after the analysis, at $(9,8)$ and $(35,34)$ \\ (Bin) & fixed looks, fresh seeds, every sample up to the accepting look counted in the fixed order; samples identified with the reference blocks by construction and by V4 & fixed $n$, fresh seeds, every sample counted; samples identified with the reference blocks by construction and by V4 \\ the program & V1, also at the registered geometry before the first sample, V3 and V5; identical records of the implementations of the run at the registered geometry (Section~\ref{sec:cert-exp}) & V1 at the registered geometry, V3 at $(9,4)$ \\ \bottomrule \end{tabular} \caption{The conditions of the two certificates and the validations that support them (Section~\ref{sec:cert-exp}); pairs $(L,R)$ give the block side and the window radius. No validation had a mismatch. Sections~R.1 and~R.2 of the records supplement give every run with its number of comparisons.} \label{tab:conditions} \end{table} \subsection{From the auxiliary decoder to optimal decoding}\label{sec:reduction} In Section~\ref{sec:cert} we bound the failure probability of an auxiliary decoder at $p=0.103$ on codes made of whole blocks, $\mathcal P_{n_yL+1,\,n_xL}$ with $n_x\ge6$ and $n_y\ge41$, by the right side of \eqref{eq:ml}, under the same conditions and with the same confidence. The first stage of this decoder is the registered program; its later stages are minimum-weight corrections with edge weights in $[0.98,1.02]$. The Lean proof of Theorem~\ref{thm:ml} takes unit weights there, so it has no hypothesis on them; this is allowed because only $\PML$ is bounded, the experiment measures only the first stage, and every such auxiliary decoder bounds $\PML$. Theorem~\ref{thm:ml} follows from this bound, the optimality of ML decoding and the next two lemmas, which hold for every code size. \begin{lemma}[monotonicity in $p$]\label{lem:monoq} For $0\le p\le p'\le\tfrac12$, $\PML(\mathcal P_{d,w},p)\le\PML(\mathcal P_{d,w},p')$. \end{lemma} \begin{proof} If $p=\tfrac12$ there is nothing to prove. Otherwise let $N$ contain each edge independently with probability $r=(p'-p)/(1-2p)\in[0,\tfrac12]$, independently of $E$. Then $E'=E\oplus N$ contains each edge independently with probability $p(1-r)+(1-p)r=p'$. Consider the randomized decoder that, given $\partial E$, draws $N$, applies the ML decoder for $p'$ to the syndrome $\partial E\oplus\partial N=\partial E'$, and adds the class of $N$ to its output. Since the class of $E'$ is the class of $E$ plus the class of $N$, this decoder fails exactly when the ML decoder for $p'$ fails on $E'$. Its failure probability is therefore $\PML(\mathcal P_{d,w},p')$, and the ML decoder for $p$ does at least as well. \end{proof} \begin{proposition}[monotonicity in the size]\label{prop:monosize} For fixed $p\in[0,1]$, $\PML(\mathcal P_{d,w},p)$ is non-increasing in $d$ and non-decreasing in $w$. \end{proposition} \begin{proof} From $d$ to $d+1$: the checks of $\mathcal P_{d,w}$ are the checks of $\mathcal P_{d+1,w}$ in rows $0,\dots,d-2$. Read the vertical edges of $\mathcal P_{d+1,w}$ between rows $d-2$ and $d-1$ as the half-edges of $\mathcal P_{d,w}$ at its top side. The restriction of an error of $\mathcal P_{d+1,w}$ to these edges and to the edges below them is an independent error of $\mathcal P_{d,w}$, with the same class, since the class is the parity at $b_1$, and its syndrome is the syndrome of the large code in rows $0,\dots,d-2$. Any decoder of $\mathcal P_{d,w}$ therefore gives a decoder of $\mathcal P_{d+1,w}$ with the same failure probability, and ML decoding of $\mathcal P_{d+1,w}$ does at least as well. From $w$ to $w+1$: a decoder of $\mathcal P_{d,w}$ draws an independent error $N$ on the edges of $\mathcal P_{d,w+1}$ that are not edges of $\mathcal P_{d,w}$, that is, the vertical edges and half-edges of column $w$ and the horizontal edges between columns $w-1$ and $w$. From $\partial E$ and $N$ it computes the syndrome of $E\cup N$ in $\mathcal P_{d,w+1}$, applies ML decoding of $\mathcal P_{d,w+1}$ and adds the class of $N$, the parity of its half-edges at $b_1$. It fails exactly when ML decoding of $\mathcal P_{d,w+1}$ fails on $E\cup N$, an independent error of $\mathcal P_{d,w+1}$. Hence $\PML(\mathcal P_{d,w},p)\le\PML(\mathcal P_{d,w+1},p)$. \end{proof} \begin{proof}[Proof of Theorem~\ref{thm:ml}] Let $0\le p\le0.103$, $w\ge1$ and $d\ge41L+1$, and let $n_x,n_y$ be as in the theorem, so that $n_x\ge6$, $n_y\ge41$, $w\le n_xL$ and $d\ge n_yL+1$. Lemma~\ref{lem:monoq} and Proposition~\ref{prop:monosize} give \[ \PML(\mathcal P_{d,w},p)\le\PML(\mathcal P_{d,w},0.103)\le\PML(\mathcal P_{n_yL+1,\,n_xL},0.103). \] The last probability is at most the failure probability of the auxiliary decoder on $\mathcal P_{n_yL+1,\,n_xL}$ at $p=0.103$, and by Section~\ref{sec:cert} this is at most the right side of \eqref{eq:ml}. For the last statement, $n_y\ge(d-1)/L-1$ and $0.015/L\ge1/35200$ give $e^{-0.10(n_y-40)}\le e^{-0.015(n_y-40)}\le e^{0.615-(d-1)/35200}$, so the right side of \eqref{eq:ml} is at most $3.81\times10^{4}\,e^{0.615}\,n_x\,e^{-(d-1)/35200}$. If $w$ grows subexponentially in $d$, so does $n_x\le\max(6,w/L+1)$, and this is at most $e^{-(d-1)/70400}$ for all large $d$. \end{proof} \section{Sampling-free bounds}\label{sec:count} In this section we prove Theorems~\ref{thm:planar}, \ref{thm:rotated} and~\ref{thm:toric} by the scheme outlined in Section~\ref{sec:intro-methods}. Two features are specific to this section: the smooth sides of the rotated code, which are not parallel to the lattice axes, and the seam of the tie-break on the torus. \subsection{Coordinates}\label{cnt:coord} All three decoding graphs consist of points of $\mathbb Z^2$, or of $\mathbb Z_m^2$, joined by unit steps, together with half-edges. We write $|u-v|$ for the $\ell^1$ distance, and a lattice path between $u$ and $v$ with $|u-v|$ steps is a \emph{geodesic}. Each half-edge is regarded as the unit step from its check to an \emph{outer point}, a lattice point outside the graph, as follows. \emph{Planar code.} For the check $(x',y')$ of $\mathcal P_{d,w}$ in Section~\ref{sec:graphs} we write $(x,y)=(y',x')$. The checks are then the points of the box $B=[0,d-2]\times[0,w-1]$, each check $(0,y)$ has a half-edge to $b_1$ with outer point $(-1,y)$, and each check $(d-2,y)$ has a half-edge to $b_2$ with outer point $(d-1,y)$. These are the coordinates of the Lean statements, which write $n_x=d-1$ and $n_y=w$. \emph{Rotated code.} The $d^2$ data qubits of $\mathcal R_d$ sit at the points $(a,b)$ with $0\le a,b\le d-1$. For $0\le i,j\le d-2$ the plaquette with corners $(i,j)$, $(i+1,j)$, $(i,j+1)$, $(i+1,j+1)$ carries an $X$ check when $i+j$ is even. The weight-two $X$ checks act on the qubits $(i,0),(i+1,0)$ for odd $i$ and on $(i,d-1),(i+1,d-1)$ for even $i$, $0\le i\le d-2$; we place them at the positions $(i,-1)$ and $(i,d-1)$. The $X$ check at position $(i,j)$ gets the lattice coordinates $(x,y)=\bigl((i+j)/2,(i-j)/2\bigr)$, so that $x+y=i$ and $x-y=j$. Then: \begin{enumerate}[label=(\alph*),leftmargin=2em] \item the checks are exactly the lattice points of $R_d=\{(x,y)\in\mathbb Z^2: 0\le x+y\le d-2,\ -1\le x-y\le d-1\}$; \item two checks share a qubit if and only if they are lattice neighbours, and then they share exactly one; \item the qubits that lie in only one $X$ check are the half-edges. At each check $z$ they correspond one-to-one to the unit steps $e$ for which $z+e$ lies beyond one of the \emph{rough lines} $x+y=-1$ and $x+y=d-1$ and inside the \emph{smooth range} $-1\le x-y\le d-1$; the outer point of the half-edge is $z+e$. The half-edges across $x+y=-1$ are the qubits of the column $a=0$ and join $b_1$; those across $x+y=d-1$ are the qubits of the column $a=d-1$ and join $b_2$. There are $d$ of each. \end{enumerate} These facts follow from the definitions. We also checked them by explicit construction for $d\le21$, and the Lean development identifies the failure probability of the rotated code with that of this graph (Section~\ref{sec:lean-count}). A check can have two half-edges to the same boundary vertex; they are different edges. We call the lines $x-y=-1$ and $x-y=d-1$ the bottom and the top \emph{smooth sides}, and $h(z)=(d-1)-(x-y)$ the \emph{height} of a point $z=(x,y)$ below the top side. \emph{Toric code.} We write the checks of $\mathcal T_m$ as $(x,y)$ with $x,y\in\{0,\dots,m-1\}$; each check is joined to $(x\pm1,y)$ and $(x,y\pm1)$, modulo $m$. \subsection{Tie-break, failure paths and exclusion rules}\label{cnt:rules} For the planar and the rotated code let $\phi(x,y)=x+9y$. For the toric code let $\phi(x,y)=x$, the representative in $\{0,\dots,m-1\}$; this is a function on $\mathbb Z_m^2$, which jumps across the \emph{seam} between the columns $m-1$ and $0$. For a set $S$ of edges let $\Phi(S)$ be the sum of $\phi(u)+\phi(v)$ over the edges $\{u,v\}$ of $S$, where a half-edge contributes its check and its outer point. Suppose that some correction of least size fails, and let $C^\ast$ be one with the least value of $\Phi$ among the failing corrections of least size. The set $E\oplus C^\ast$ has even degree at every check. For the planar and the rotated code it has odd degree at $b_1$ and at $b_2$, so it contains a simple path $\gamma$ from $b_1$ to $b_2$. Its first and last edges are half-edges, and its \emph{interior} $\gamma'$, the path without them, joins a check on the side of $b_1$ to a check on the side of $b_2$. So $\gamma'$ has at least $d-2$ edges: in $\mathcal P_{d,w}$ the coordinate $x$ runs from $0$ to $d-2$, and in $\mathcal R_d$ every step changes $x+y$ by $\pm1$, from $0$ to $d-2$. For the toric code $E\oplus C^\ast$ is not null-homologous, so it contains a simple cycle $\gamma$ that is not null-homologous, and $\gamma$ has at least $m$ edges; we put $\gamma'=\gamma$. In all cases $C^\ast\oplus\gamma$ is a correction, so $|\gamma\cap E|\ge|\gamma\cap C^\ast|$ because $C^\ast$ has least size. We label the edges of $\gamma$ in $E$ by $\mathsf E$ and those in $C^\ast$ by $\mathsf C$; every edge of $\gamma$ gets exactly one label. A \emph{window} is a sub-path $\sigma$ of $\gamma'$ between two checks $u\ne v$. We write $n_E$ and $n_C$ for the numbers of its labels, $\sigma_E$ and $\sigma_C$ for its sets of $\mathsf E$- and $\mathsf C$-edges, and $T_\sigma$ for the set of checks of odd degree in $\sigma_C$. An \emph{alternative} to a set $S$ of edges is a set $A$ of edges of the graph with the same checks of odd degree as $S$, such that $A$ has an even number of half-edges at $b_1$ (planar and rotated code), respectively such that $|S|+|A|0$ and raises the point between them by $2$ in $\xi$. Suppose that the least value $l$ of $\xi$ on $P$ is below $\min(\xi(a),\xi(b),c-1)$. At the first point of $P$ with $\xi=l$, the path arrives by a step $s_2$ and leaves by a step $s_1$, from a point at level $l+1\le c-1$; the exchange keeps the path at $\xi\le c$ and lowers $\Phi$, a contradiction. Without the constraint the same exchange applies at every level, and the canonical geodesic is the unique geodesic of least $\Phi$. \end{proof} For a window $\sigma$ let $\xi_\sigma$ be the least value of $\xi$ on its points. The points of $\sigma$ lie in $R_d$, so $\xi_\sigma\ge-1$, and since consecutive points differ by $1$ in $\xi$ and all satisfy $\xi\le d-1$, also $\xi_\sigma\le d-2$. The tests for $\mathcal R_d$ use, for each pair of checks of the window, a geodesic of least $\Phi$ among those whose points have height $h\ge0$, that is, $\xi\le c=d-1$; in (iii) and (iv) these are taken over the pairs of a least-length matching. By Lemma~\ref{cnt:lem-band} and $\xi_\sigma\le d-2$, every such geodesic stays at $\xi\ge\xi_\sigma\ge-1$, inside the smooth range. Lemma~\ref{cnt:lem-rough} turns it, or the union of the matching geodesics, into an edge set $A$ of $\mathcal R_d$ with no more edges. If $A$ has fewer edges, the window violates (i) or (iii) for the alternative $A$; otherwise $\Phi(A)$ equals the $\Phi$ of the geodesics. In both cases a window that fails a test violates Lemma~\ref{cnt:lem-rules}. This holds for every $d$. The tests of a window depend on its position only through the ceiling $\xi\le d-1$. A geodesic between two points $a,b$ of a window rises at most $|a-b|\le M$ above $\max(\xi(a),\xi(b))$, where $M$ bounds the number of edges of the windows we test. So if all points of a window have height at least $M$, the ceiling does not bind, and the tests are those of the planar code (all lattice geodesics). \emph{Toric code.} The windows we test have at most $M$ edges, and every alternative used has at most $M$ edges, with $2M4M^2$. \end{lemma} \begin{proof} For $m>2M$ the window and its alternatives do not wrap around the torus, and their points have offsets within $M$ of the offset of the first point of the window. Only (ii) and (iv), and the choice of a geodesic or matching of least $\Phi$, compare values of $\Phi$, and each comparison is between two edge sets with the same number of edges, at most $2M$ in total, hence at most $4M$ endpoints. Each side equals $mN+Q$, where $N$ counts its endpoints at negative offsets and $Q$ is the sum of the offsets of its endpoints. The difference is $m\,\Delta N+\Delta Q$; $\Delta N$ does not depend on $m$, and $\Delta Q$ does not change if all offsets are shifted by the same amount, so measuring them from the first point of the window gives $|\Delta Q|\le4M\cdot M0$, the rows in $B$ follow. \end{proof} So one certificate for the bulk system covers every box; no boundary types occur. \subsection{The certificate}\label{phen:cert} The certificate is a positive integer potential for the bulk system with $M=8$: $5{,}263{,}174$ states and $44{,}599{,}560$ transitions, $p_\ast=2/125$, $X=231/50$, $\lambda=499/500$, potentials at most $2^{32}$. As in Section~\ref{cnt:cert}, every row \eqref{phen:row} is checked in exact integer arithmetic. The largest ratio of the two sides of \eqref{phen:row} is $0.997805$ (the Perron root of the system is $0.995809$), and the start sum $K_0=(\omega_E+\omega_C)^2\sum_s\omega(s)H(s)/\min H$ is at most $1.2827$. \begin{proof}[Proof of Theorem~\ref{thm:phenom}] By Lemma~\ref{phen:lem-rules} and the counting above, $\PMW(\mathcal Q_{d,w,T},p)$ is at most the total weight of the labelled paths from $b_1$ to $b_2$ whose windows satisfy the lemma. As in the proof of Theorem~\ref{thm:planar}, bound the two half-edges of each path, summed over their labels, by $\omega_E+\omega_C$ each. The interior of the path starts at one of the $w(T+1)$ checks of the rows $y=0$ and has at least $d-2$ edges. With the certificate, Lemma~\ref{phen:lem-box} gives at $p=p_\ast=2/125$ \[ \PMW(\mathcal Q_{d,w,T},p)\le w(T+1)K_0\sum_{\ell\ge d-2}\lambda^{\ell-7}\le(T+1)\,w\cdot1.2827\cdot \frac{\lambda^{d-9}}{1-\lambda}. \] The condition $d\ge9$ makes the interior at least $7$ steps long, so that it begins with a state. For $p] (11,6.6) -- (16,6.6); \node[fill=white,inner sep=1pt] at (13.5,5.9) {$R$}; \draw[<->] (-0.5,-1.1) -- (3.5,-1.1); \node[anchor=north] at (1.5,-1.2) {$L$}; \end{tikzpicture} \caption{The auxiliary decoder of Section~\ref{sec:cert-decoder} on a part of a code far from its sides, with block side $L=4$ and window radius $R=5$, given by the formula $R=\tfrac32L-1$ of the registered program of Section~\ref{sec:cert-exp}; dots are checks and thin lines bound the blocks. The window $W_c$ of block $c$ (dashed) consists of the checks within $\ell_\infty$ distance $R$ of $c$; it reaches beyond $N_1(c)$ (thick), the nine blocks at block distance at most~$1$ from $c$. Stage~1 computes a correction for each block from the syndrome in its window and keeps the edges that the block owns; the kept edges form $C_0$. A block is bad if the residual syndrome has a check in it (flagged; filled dots) or if a path of $F=E\oplus C_0$ (red edges) inside $N_1(c)$ joins it to a check at $\ell_\infty$ distance at least $L$ (long; the loop through $c$ reaches distance $L$ from $c$ and makes $c$ long, but it stays within distance $32R$. With \[ D=4+\lfloor 2R/L\rfloor , \] the bad events of any set of blocks with pairwise distances at least $D$ are therefore independent; $D=5$ for $R=L-1$, and $D=6$ for $L\le R<\tfrac32L$. \paragraph{Types.} Since $R0$, which depend only on $\varepsilon$, $D$, $a_0$, $a_1$, the weight ratio $\kappa=1.05$ and $L$, and do not increase with $L$, such that for all $n_x$ as in Section~\ref{sec:cert-decoder} and all $n_y>H_0$ \[ \Pr\bigl(\text{the decoder fails on }\mathcal P_{n_yL+1,\,n_xL}\bigr)\le C_1\,n_x\,e^{-s_1(n_y-H_0)}+C_2\,n_x\,e^{-s_2(n_y-H_0)} . \] \end{theorem} In the instance $(\varepsilon,a_0,a_1)=(3.29\times10^{-4},5,16)$ with $L\le R<\tfrac32L$, so that $g=2$, $D=6$ and $H_0=40$, the bound holds for every $L\ge2$, $n_x\ge6$ and $n_y\ge41$ with \[ C_1=36,\quad s_1=0.10,\quad C_2=3.8\times10^{4},\quad s_2=0.015, \] the constants of \eqref{eq:ml}. The Lean proof establishes the bound with these constants (Section~\ref{sec:lean-ml}), and Appendix~\ref{s1:sec:numbers} compares them with the numerical evaluation. At the same $(\varepsilon,a_0,a_1)$ and for every $L\ge192$, the numerical evaluation of the series in Appendix~\ref{s1:sec:numbers} gives the sharper bound $5.35\times10^{2}\,n_x\,e^{-0.161(n_y-40)}+1.39\times10^{5}\,n_x\,e^{-0.025(n_y-40)}$, and at the certified level $\hat\varepsilon$ it gives the constants of Remark~\ref{rem:sharper}. The proof is given in full in Appendix~\ref{app:proof}; its idea is as follows. Call the components of the bad blocks under adjacency at distance at most $a_0$ the \emph{clusters}. A path of $F$ that starts in a good block $c$ ends before it reaches distance $L$ from $c$, since otherwise $c$ would be long. Hence every component of $F$ meets at most one cluster, and the residual defects, which lie in flagged blocks, lie in clusters. Group the clusters into \emph{families} linked by level-1 components. If the decoder fails, then either the part of $E\oplus C$ attached to a single family has odd parity at both boundary vertices, or the top stage joins a chain of families from one rough side to the other. Parity inside interior clusters forces witnesses, flagged blocks far apart within a cluster or a family, and keeps consecutive families of a chain more than $a_1$ apart; an exchange argument bounds the total weight of the top-stage paths of a chain by the distances between the entry and exit defects within its families, since otherwise re-pairing would lower the weight of the top stage. Among the bad blocks of a cluster, a greedy selection keeps blocks at mutual distance at least $D$, which by $(\mathrm H_\varepsilon)$ are all bad with probability at most $\varepsilon$ to the number of blocks. Counting the two alternatives with exponential tilts then gives two geometric series, and hence the two terms of the bound. \subsection{The certificate at \texorpdfstring{$p=0.103$}{p = 0.103}}\label{sec:cert-exp} In the code of $7\times7$ blocks, $\mathcal P_{7L+1,\,7L}$, the blocks $(a,3)$ with $a=0,\dots,6$ are the \emph{reference blocks} of the types $L0$, $L1$, $L2$, bulk, $R2$, $R1$, $R0$, and $\varepsilon_t$ is the probability that the reference block of type $t$ is bad at $p=0.103$. A sample of type $t$ draws independent flips on a \emph{patch}, which consists of the checks within $\ell_\infty$ distance $R+1$ of $N_1(c)$ and all edges between them; for the types other than bulk the patch is clipped at the smooth side. The sample then runs stage~1 on the windows of the blocks of $N_1(c)$, nine of them, or six for the types $L0$ and $R0$, and evaluates Definition~\ref{def:cert-bad}. Every edge that the bad event depends on lies in the patch, so a sample is bad with probability $\varepsilon_t$; this identification is part of (Bin). The level $3.29\times10^{-4}$ was fixed before the calibration runs described next, together with the constants of \eqref{eq:ml}, which Lean proves at this level. The block side and the number of samples were chosen before the registration, by a rule applied to two calibration runs of the bulk type at $p=0.103$ with $R=\tfrac32L-1$, whose seeds are disjoint from those of the experiment. The first calibration run had ten block sides from $96$ to $384$, with $1.2\times10^{5}$ samples at each of the three largest; the second had $1.2\times10^{5}$ samples at each of $L=352$, $384$ and $416$. The rule was frozen together with the design of the second run, before that run started. It fits a model of the rate of flagged blocks as a function of $L$ to the flag counts of both runs, takes the rate of long blocks at each $L$ from the second run alone, and selects, among block sides from $352$ to $440$ and sizes of $2\times10^{5}$, $2.5\times10^{5}$ and $3\times10^{5}$ samples per type, the cheapest design whose probability of failing the acceptance rule, estimated from the posterior law of these rates under each of two models of the flag rate, is at most $0.07$. It selected $L=352$ and $n=2\times10^{5}$, with an estimated probability of failing of $0.061$. An earlier version of the rule had fitted the rate of long blocks over the ten block sides of the first run, and this fit failed its goodness-of-fit test; the choice to keep the flag counts of the first run and to drop its counts of long blocks was made after that run had been read. These choices affect only the cost of the experiment and its chance of failing, not its validity, since every sample of the experiment was drawn after the registration, with fresh seeds. The registration was frozen before the first sample was drawn. It fixes the program: $p=0.103$, $L=352$, $R=527$, the posterior weights \eqref{eq:cert-weights} on every edge of every window with their tie term and clipping, the marginal computation of Section~\ref{sec:cert-marg}, and the matching implementation at a fixed version. It fixes the later stages, with $a_0=5$ and $a_1=16$, and the rule that the sharper constants of Remark~\ref{rem:sharper} use the admissible $a_1$ that minimizes the bound at the certified level. It fixes the experiment as follows. The samples of each type are drawn in chunks of $40$, with seeds derived from the type, the index of the chunk and entropy drawn at the freeze, and they are ordered by chunk. The looks are at $n_1=125{,}040$, $n_2=187{,}560$ and $n_3=250{,}080$ samples, that is, after $3{,}126$, $4{,}689$ and $6{,}252$ chunks; here $n_3=160\lceil1.25\,n/160\rceil$ for the selected $n=2\times10^{5}$, $n_1=n_3/2$ and $n_2=3n_3/4$. A look counts the bad samples among the first $n_j$ samples of the type, and it is taken only when all of them are complete, so the order in which samples finish cannot affect it. A type is accepted at the first look $j$ with at most $c_j$ bad samples, $(c_1,c_2,c_3)=(7,19,32)$, and no sample of an accepted type beyond its accepting look is counted. Each $c_j$ is the largest count whose exact one-sided Clopper--Pearson upper bound for $\varepsilon_t$ at level $10^{-9}/3$, from $n_j$ samples, is at most $3.29\times10^{-4}$: these bounds are $3.1315\times10^{-4}$, $3.2483\times10^{-4}$ and $3.2632\times10^{-4}$ at $c_j$, rounded up, and $3.2919\times10^{-4}$, $3.3369\times10^{-4}$ and $3.3240\times10^{-4}$ at $c_j+1$, rounded down. A type fails as soon as more than $c_3$ samples of an initial segment of its order, made of complete chunks, are bad, since then no look can accept it, and one failed type ends the experiment without acceptance. A sample whose decoding makes no progress for $3600$\,s is decoded again in a new process, and it is counted as bad if it again makes no progress within $2700$\,s. The command of the analysis was written down before the run started. The calibration rule had selected the size $n$ for a single look with acceptance at $k_t\le21$, a threshold that divides the level $10^{-9}$ among the seven types. Before the second calibration run was analysed, the registration replaced the single look by the sequential design above, in which each type is tested at the full level (Section~\ref{sec:conf}) and which, by the estimates of the registration, is less likely to fail than the single look. By the method of Section~\ref{sec:cert-marg}, the program computes the same quantities as the program of the certificate at $p=0.102$ in the previous version of this paper, but at the values of $p$, $L$ and $R$ of this certificate. The present implementation differs from the earlier one in three ways, each of which, by construction, leaves the output unchanged bit for bit: the program and its marginal computation are organized to use less memory and time; the matching library is built with a change that removes a rare slow path without changing any step of the matching; and the windows of a sample are computed in three threads. Before the registration, at the registered geometry, the $21$ samples of V1 below gave identical outputs with and without these changes, and three full samples of each type gave identical records with and without the threads. Six validations test the registered program. Each uses its own random inputs, and none reads a certificate sample. V6 compares the stage-1 outputs, matching weights and flags of all nine windows for errors with the same syndrome: $E$; $E\oplus S$, for plaquette boundaries $S$ inside the windows; $E\oplus S\oplus\Gamma$, for a relative cycle $\Gamma$ across them; and the canonical chain of the syndrome. It tests (V6) directly. V2 compares stage-1 outputs, in block coordinates, for errors that are periodic with period $L$. V4 compares the block events of the sampler with the full decoder on planar codes of $8\times8$ blocks, for all seven types. V2 and V4 test (Hcov) and the identification of samples with reference blocks. V1 (two runs of the program on the same samples), V3 (an independent implementation of the marginals and the matching) and V5 (exact transfer-matrix marginals) test the implementation. All six passed before the registration was frozen, on blocks of side $8$, $16$ and $24$ with window radius $R=\tfrac32L-1$, the formula of the registered program, and V1 passed again at the registered geometry $(352,527)$, also before the registration. Table~\ref{tab:conditions} gives the outcomes, and Table~R.1 of the records supplement lists every run. The run deviated from the registration in one respect. The registration made the launch conditional on four checks: V6 at the registered geometry $(352,527)$ and three gates. The first gate compares the records of the driver program that ran the samples with those of a reference driver. The second checks that a chunk resumed in a new process gives the same records as one decoded without interruption. The third checks, on an instance known to be slow, that the selected matching implementation does not stall in a stage-1 window solve on a sample where the reference implementation finishes; this gate decides which implementation may be used. None of the four ran before the launch. V6 at $(352,527)$ ran after the analysis, on the frozen program with the registered inputs. Its pass rule, written down before V6 gave any result, required $21$ of $21$ comparisons without a mismatch, and a failure would have withdrawn the certificate. V6 passed. Since V6 tests a property of the program and not of the samples, running V6 after the analysis tests the same property as running it at the registered time; for V6, only the timing departs from the registration. What the three gates guard against is covered by checks that ran before the launch, by the records of the run and by the replays of the bad samples, and the three gates themselves passed after the analysis (Section~R.1). The run took place on 7 November 2026, on $20$ machines. An automated step took each look as soon as its samples were complete and reported only its decision; the counts themselves were read only after the last decision. Table~\ref{tab:cert-counts} shows the result. Five types were accepted at the first look; $L2$ and $R1$, with $9$ and $10$ bad samples among their first $n_1$ samples, were accepted at the second. So the experiment accepted, and by Sections~\ref{sec:conf} and~\ref{sec:reduction} this gives Theorem~\ref{thm:ml}. No sample stalled, and the failure condition never applied. The largest upper bound at an accepting look, that of the bulk type, gives the level $\hat\varepsilon$ of Remark~\ref{rem:sharper}. Each of the $42$ bad samples among the counted ones was decoded again from its seed on a machine that had produced none of them, with records identical apart from the time and memory fields. For the $4{,}120$ counted samples whose full first-stage data the registration required to be stored, the flags and long paths were recomputed from these data with identical results (Section~R.1). \begin{table}[ht] \centering \begin{tabular}{@{}lcrrrc@{}} \toprule type & look & $n$ & bad samples $k_t$ & $c_j$ & upper bound for $\varepsilon_t$ \\ \midrule $L0$ & $1$ & $125040$ & $2$ & $7$ & $2.228\times10^{-4}$ \\ $L1$ & $1$ & $125040$ & $4$ & $7$ & $2.617\times10^{-4}$ \\ $L2$ & $2$ & $187560$ & $10$ & $19$ & $2.401\times10^{-4}$ \\ bulk & $1$ & $125040$ & $7$ & $7$ & $3.132\times10^{-4}$ \\ $R2$ & $1$ & $125040$ & $3$ & $7$ & $2.429\times10^{-4}$ \\ $R1$ & $2$ & $187560$ & $12$ & $19$ & $2.599\times10^{-4}$ \\ $R0$ & $1$ & $125040$ & $4$ & $7$ & $2.617\times10^{-4}$ \\ \bottomrule \end{tabular} \caption{The certificate at $p=0.103$, $L=352$, $R=527$: for each type, the look that accepted it, the number $n$ of samples counted there, the number $k_t$ of bad samples among them and the threshold $c_j$ of that look. The last column is the exact one-sided Clopper--Pearson upper bound at level $10^{-9}/3$, rounded up. At the first look, $L2$ had $9$ and $R1$ had $10$ bad samples among $125{,}040$.} \label{tab:cert-counts} \end{table} \paragraph{Registered experiments.} Table~\ref{tab:family} lists every certificate experiment registered for this paper or its earlier versions, each with its outcome. The second registration at $p=0.100$ was conditional: it was to be run only if, when the machines of the first registration became free, the first had not passed all its types. It was never run. Registrations that were replaced before any sample was drawn under them, and so were never run, are not listed; three of them, at $p=0.100$, had been time-stamped. Each listed registration bounds by $10^{-9}$ the probability that it accepts while its statement is false, under the conditions of its own program. Over all $k=5$ of them, whether or not they were run, the probability that at least one accepted a false statement is at most $5\times10^{-9}$ under the conditions of all five programs; this holds whatever rule selects the statements that are reported and however the experiments depend on each other. Since Theorem~\ref{thm:ml} covers every $p\le0.103$, it implies the threshold statements of the two earlier accepted certificates for bit flips. The registrations and records of the experiments at $p=0.100$ and $p=0.102$ are in earlier versions of the fourth record listed in Code and data. \begin{table}[ht] \centering \small \begin{tabular}{@{}l>{\raggedright\arraybackslash}p{0.14\textwidth}lc>{\raggedright\arraybackslash}p{0.27\textwidth}>{\raggedright\arraybackslash}p{0.13\textwidth}@{}} \toprule registered & $p$ & $(L,R)$ & types & acceptance & outcome \\ \midrule 26 Oct 2026 & $0.100$ & $(280,279)$ & $5$ & $k_t\le18$ of $1.2\times10^{5}$; level $5\times10^{-4}$ & accepted \\ 26 Oct 2026 & $0.02$, measurement errors & $(35,34)$ & $25$ & $k_t\le14$ of $3\times10^{6}$; level $1.85\times10^{-5}$ & accepted, Theorem~\ref{thm:d1} \\ 26 Oct 2026 & $0.100$, conditional & $(304,303)$ & $5$ & $k_t\le18$ of $1.2\times10^{5}$; level $5\times10^{-4}$ & not run \\ 30 Oct 2026 & $0.102$ & $(280,419)$ & $7$ & $k_t\le17$ of $2\times10^{5}$; level $3\times10^{-4}$ & accepted \\ 7 Nov 2026 & $0.103$ & $(352,527)$ & $7$ & three looks; level $3.29\times10^{-4}$ & accepted, Theorem~\ref{thm:ml} \\ \bottomrule \end{tabular} \caption{The certificate experiments registered for this paper or its earlier versions, each designed for confidence $1-10^{-9}$. Pairs $(L,R)$ give the block side and the window radius; the level is the bound on the bad-block probabilities that acceptance certifies. Registrations replaced before any sample was drawn under them are not listed.} \label{tab:family} \end{table} \subsection{The certificate under measurement errors}\label{sec:cert-meas} Theorem~\ref{thm:d1} uses a certificate of the same kind on the phenomenological graph. The codes are $\mathcal Q_{n_yL+1,\,n_xL,\,n_tL-1}$ with $n_x,n_t,n_y\ge5$, whose checks form the box $[0,n_tL)\times[0,n_xL)\times[0,n_yL)$ in the coordinates $(t,x,y)$. The blocks are cubes of side $L=35$, and the window of a block is the set of checks at $\ell_\infty$ distance at most $R=34$ from it. Distances between blocks are $\ell_\infty$ distances of their indices, so $N_1(c)$ has at most $27$ blocks. Only the sides $y=0$ and $y=n_yL-1$ carry half-edges; the two sides in $x$ and the first and last layers in $t$ behave like smooth sides. Every weight is $1$. For each block, stage~1 computes a minimum-weight correction of the syndrome in the block's window on the graph of the window. In this graph, every check with a neighbour outside the window has one edge to a boundary vertex. Stage~1 uses a matching program at a fixed version with a fixed order of nodes and edges, and it keeps the edges owned by the block. Levels $0$ and $1$, with $a_0=4$ and $a_1=20$, and the top stage are as in Section~\ref{sec:cert-decoder}. A block is bad if it is flagged or long, as in Definition~\ref{def:cert-bad}, and the bad events of blocks at pairwise distances at least $D=5$ are independent. Outside the declared rows $0$, $1$, $n_y-2$, $n_y-1$, a block has one of $25$ types. Its block column gives one of $L0$, $L1$, bulk, $R1$, $R0$, as in Section~\ref{sec:cert-lemma}, and its block layer in time gives one of $B0$, $B1$, bulk, $E1$, $E0$, defined in the same way. The deterministic lemma and the counting of Theorem~\ref{thm:cert} have three-dimensional analogues, with $D=5$, $a_0=4$, $a_1=20$, $H_0=47$ and $\kappa=1$, since all weights are equal. Lean proves them in full, for the decoder whose later stages use any minimum-weight corrections for these unit weights. If every type is bad with probability at most $\varepsilon^\ast=1.85\times10^{-5}$, the decoder fails on $\mathcal Q_{n_yL+1,\,n_xL,\,n_tL-1}$ with probability at most the right side of \eqref{eq:d1}; the rates $0.1008$ and $0.007$ there are the tilts of the two counts. Lemma~\ref{lem:monoq} and Proposition~\ref{prop:monosize} hold for $\mathcal Q_{d,w,T}$ with the same proofs, where a new layer, together with the time-like edges into it, is added like a new column. As in the proof of Theorem~\ref{thm:ml}, these lemmas and the optimality of ML decoding turn the bound for codes made of whole blocks into \eqref{eq:d1} for all $d\ge5L+1$, $w\ge1$ and $T\ge0$. When $w$ and $T$ grow subexponentially in $d$, so does $n_tn_x$, while the exponentials of \eqref{eq:d1} decay at least like $e^{-(d-1)/5000}$; this gives the last statement of Theorem~\ref{thm:d1}. As in Section~\ref{sec:cert-exp}, no sample was drawn before the registration was frozen; this registration fixes the program described above, the level $\varepsilon^\ast$ and a joint design. Each of $N=3\times10^{6}$ simulations draws independent flips at $p=0.02$ on a patch of $5\times5\times3$ blocks (in $x$, $t$ and $y$) with their windows and a margin. It runs stage~1 on the $75$ windows and evaluates the bad events of the $25$ blocks of the middle block row, one of each type. The seeds are derived from fresh entropy; every simulation is counted, and there is no stopping rule. The experiment accepts if $k_t\le14$ for every type $t$. Equivalently, for every type the exact one-sided Clopper--Pearson upper bound for $\varepsilon_t$ at level $4\times10^{-11}=10^{-9}/25$ is at most $\varepsilon^\ast$. Before the registration, V1 ran at the registered geometry. Also before the registration, V2, V3, V4 and V6 of Section~\ref{sec:cert-exp}, adapted to three dimensions, ran at $(L,R)=(9,4)$, not at the registered radius $R=L-1$. V2, V4 and V6 ran at $R=L-1$ only after the analysis, at $(L,R)=(9,8)$ and at the registered $(35,34)$. The outcomes are in Table~\ref{tab:conditions}, with the individual runs in Section~R.2 of the records supplement. Table~\ref{tab:cert-meas} shows the counts. There were $32$ bad samples, all flagged and none long, and at most $4$ of any type, so the experiment accepted. The largest exact Clopper--Pearson upper bound at level $4\times10^{-11}$, that of the count $4$, is $1.1706\times10^{-5}$, rounded up. \begin{table}[ht] \centering \begin{tabular}{@{}lccccc@{}} \toprule & $L0$ & $L1$ & bulk & $R1$ & $R0$ \\ \midrule $B0$ & $0$ & $0$ & $3$ & $3$ & $0$ \\ $B1$ & $2$ & $1$ & $1$ & $1$ & $2$ \\ bulk & $2$ & $1$ & $1$ & $2$ & $0$ \\ $E1$ & $1$ & $0$ & $0$ & $2$ & $2$ \\ $E0$ & $0$ & $4$ & $1$ & $2$ & $1$ \\ \bottomrule \end{tabular} \caption{The certificate under measurement errors at $p=0.02$, $L=35$, $R=34$: the number of bad samples among the $3\times10^{6}$ samples of each type, by block layer in time (rows) and block column (columns). Every count is at most $14$.} \label{tab:cert-meas} \end{table} \section{Formal verification in Lean 4}\label{sec:lean} The theorems of Section~\ref{sec:setting} are also proved in the proof assistant Lean~4, with the Mathlib library; Table~\ref{tab:results} lists the formal theorems. A proof assistant checks every step of a proof against the rules of its logic, and the part of Lean that performs this check is its kernel. \begin{table}[t] \centering \small \begin{tabular}{@{}p{0.09\textwidth}>{\raggedright\arraybackslash}p{0.22\textwidth}>{\raggedright\arraybackslash}p{0.39\textwidth}l@{}} \toprule result & content & Lean theorems & checked by \\ \midrule Thm.~\ref{thm:planar} & $0.0465$ & \texttt{planar\_A10\_kernel}, \texttt{planar\_A10\_kernel\_ML} & kernel \\ & same statement & \texttt{planar\_A}, \texttt{planar\_A\_ML} & compiled evaluation \\ Thm.~\ref{thm:rotated} & $0.0465$ & \texttt{rotated\_B\_kernel}, \texttt{rotated\_B\_kernel\_ML} & kernel \\ & same statement & \texttt{rotated\_B}, \texttt{rotated\_B\_ML} & compiled evaluation \\ Thm.~\ref{thm:toric} & $0.046$ & \texttt{toric\_A'\_10\_kernel}, \texttt{toric\_A'\_10\_kernel\_ML} & kernel \\ & same statement & \texttt{toric\_A'\_10}, \texttt{toric\_A'\_10\_ML} & compiled evaluation \\ & $0.045$ & \texttt{toric\_A'\_kernel}, \texttt{toric\_A'\_kernel\_ML} & kernel \\ & same statement & \texttt{toric\_A'}, \texttt{toric\_A'\_ML} & compiled evaluation \\ Thm.~\ref{thm:phenom} & $0.016$ & \texttt{phenom\_D2M8\_kernel}, \texttt{phenom\_D2M8\_kernel\_ML} & kernel \\ & same statement & \texttt{phenom\_D2}, \texttt{phenom\_D2\_ML} & compiled evaluation \\ Thm.~\ref{thm:ml} & bound \eqref{eq:ml} and threshold & \texttt{theoremB\_q103\_main}, \texttt{pMLPlanar\_tendsto\_zero\_subexp\_q103}, \texttt{pMLPlanar\_exp\_decay\_subexp\_q103} & kernel \\ & confidence statements & \texttt{theoremB\_certified\_q103}, \texttt{threshold\_q103\_certified}, through \texttt{S3Fam.certified\_seqK\_iut} & kernel \\ & counts of Table~\ref{tab:cert-counts} and the rule & \texttt{cp\_accept\_q103\_j}$j$ and \texttt{cp\_reject\_q103\_j}$j$ for $j=1,2,3$, \texttt{cp\_q103}, \texttt{obs\_accept\_q103}, \texttt{obs\_first\_q103}, \texttt{obs\_cp\_q103}, and \texttt{cp\_upper\_q103\_}$t$, \texttt{cp\_tight\_q103\_}$t$ for $t=$ \texttt{L0}, \texttt{L1\_R0}, \texttt{L2}, \texttt{bulk}, \texttt{R2}, \texttt{R1} & kernel \\ & the confidence statements for the observed counts & \texttt{theoremB\_certified\_q103\_obs}, \texttt{threshold\_q103\_certified\_obs} & kernel \\ Thm.~\ref{thm:cert} & the instance with $D=6$ & \texttt{S3Fam.h2d\_E329} & kernel \\ Prop.~\ref{prop:cert-valid} & validity of the decoder & \texttt{S3Geom.S3dec\_valid} & kernel \\ Thm.~\ref{thm:d1} & bound \eqref{eq:d1} & \texttt{d1B\_num}, through \texttt{fail\_bound\_prog3} & kernel \\ & threshold & \texttt{pML3\_tendsto\_zero\_subexp}, \texttt{pML3\_exp\_decay\_subexp} & kernel \\ & confidence statements & \texttt{d1B\_certified}, \texttt{threshold\_d1\_general\_certified} & kernel \\ & counts of Table~\ref{tab:cert-meas} and the rule & \texttt{d1\_accept}, \texttt{d1\_rule\_tail}, \texttt{d1\_cp\_upper\_k4}, \texttt{d1\_cp\_tight\_k4} & kernel \\ \bottomrule \end{tabular} \caption{The main results and their formal proofs. Names ending in \texttt{\_ML} are the statements for $\PML$. ``Kernel'' means that every step, including every finite computation, is checked by Lean's kernel; ``compiled evaluation'' means that the certificate checks are run as compiled code inside Lean (Section~\ref{sec:lean-count}).} \label{tab:results} \end{table} \subsection{The sampling-free bounds}\label{sec:lean-count} The Lean statements of Theorems~\ref{thm:planar}--\ref{thm:phenom} concern the decoding graphs of Section~\ref{sec:graphs}, which are defined in Lean from their checks and edges. In Lean, $\mathcal P_{d,w}$ is the box $[0,d-1)\times[0,w)$ of checks with half-edges at the two ends of the first coordinate; the Lean statements write $n_x=d-1$ and $n_y=w$, so the exponent $n_x-10$ in Lean is the exponent $d-11$ of Theorem~\ref{thm:planar}. The phenomenological graph $\mathcal Q_{d,w,T}$ is the box $[0,T+1)\times[0,w)\times[0,d-1)$ with half-edges at the two ends of the last coordinate. The rotated code is defined by the positions of its $d^2$ qubits and of its $X$ checks, and the logical class of an error is the parity of its flips on the first column; a Lean lemma identifies its failure probability with that of the graph used in the proof. The toric code $\mathcal T_m$ has the checks $\mathbb Z_m^2$, and a correction fails when $E\oplus C$ crosses one of the two seams of the torus an odd number of times. In Lean, $\PMW$ is the probability that some correction of least size fails, and $\PML$ is the least failure probability of a map from syndromes to logical classes; a randomized decoder is a mixture of such maps, so it does no better. Each theorem has a version for $\PMW$ and one for $\PML$; the second follows from the first and $\PML\le\PMW$. The constants and rates are those of Section~\ref{sec:results}, entered as exact rationals, for example $398.91=39891/100$ and $0.998=499/500$. The statements have no hypotheses beyond the ranges of $p$ and of the size. \paragraph{The general argument.} Each proof consists of a general argument, proved once for each family of graphs, and a finite check of a certificate. The general argument has four parts: the probability estimates (independence of the edges, the union bound over failure paths, and the change of measure from $p_\ast$ to $p$), a decoder lemma, a counting lemma, and the soundness of the checks. The decoder lemma states that if some correction of least size fails, then a failing correction of least size with the least value of the tie-breaking potential $\Phi$ exists; $E\oplus C$ then contains a path between the two boundaries (for the toric code, a cycle that is not null-homologous), and no window of this path can be replaced by a witness that passes the check, which covers the exclusion rules of Section~\ref{sec:count} in one statement. The counting lemma turns the row inequalities of a potential into a bound on the weighted number of legal labelled walks of each length. The soundness theorems derive the hypotheses of the counting lemma from the Boolean checks of a certificate. For the rotated code the walk carries its height below the top side while it is near that side, and for the toric code its offset from the seam of $\Phi$ while it is near the seam; a translation lemma shows that the checks of states far from the seam do not depend on the offset, so the far states are checked at a single offset. \paragraph{Certificates.} A certificate lists the states of the walk, that is, its last $K$ steps with their labels (for the rotated and the toric code also the height or the offset near the boundary or the seam), gives each state a positive integer potential, and fixes $p_\ast$, $\lambda$ and the constant of the bound. The check functions verify, for every listed state, that the weighted sum of the potentials of its legal successors is at most $\lambda$ times its own potential and that every successor that is not listed ends in an excluded window; they verify that every legal start of a walk is listed or excluded, and they bound the start sum by the stated constant. An excluded window counts only if a witness for it passes the witness check. Hence neither the search that finds the witnesses nor the certificate files need to be trusted: a wrong value can only make a check fail. Tables~\ref{cnt:tab-cert} and~\ref{phen:tab} give the sizes of the certificates. \paragraph{Compiled evaluation and the kernel.} A generator turns the certificate files into Lean data modules and writes the sha256 of each input file into the module. The checks are then evaluated in one of two ways. With compiled evaluation, the check functions are compiled to machine code and run through \texttt{native\_decide}; each call adds one axiom, which \texttt{\#print axioms} lists, and the compiler and the runtime join the trusted base. On the kernel route, the certificate is a binary search tree whose nodes hold a state, its potential and the successors that the certificate claims to be excluded; the check functions recurse on this tree, and every check is reduced by the kernel (\texttt{decide +kernel}), which adds no axiom. The checks are split into pieces of moderate size (ranges of rows or subtrees, and prefixes of the start walks), each piece is a separate theorem, and lemmas proved once combine the pieces. The planar, the rotated, the phenomenological and the two toric bounds are proved in both ways from the same certificates, with identical statements (Table~\ref{tab:results}). The Lean sources also contain kernel-checked bounds from two smaller certificates, for the planar code at $p\le0.045$ with $d\ge9$ and for the phenomenological graph at $p\le0.0155$ with $d\ge7$, with $157{,}618$ and $72{,}294$ states. The data modules can be regenerated from the certificate files, whose sha256 they record; the reproduction manifest lists the input files of each theorem with their hashes. For the kernel certificates these include the transition or hint files, from which the generator reads the windows that the certificate claims to be excluded. Section~R.3 of the records supplement gives the cost of the checks behind Table~\ref{tab:results} and lists how many such axioms each compiled-evaluation theorem uses besides the standard ones (Section~\ref{sec:lean-trust}). \subsection{The certified threshold}\label{sec:lean-ml} The development defines the planar code $\mathcal P_{d,w}$ of Section~\ref{sec:graphs}, in which every edge, half-edges included, is flipped independently with probability $p$. It defines the class of an error, the parity of its half-edges at $b_1$, and the failure probability $\PML(\mathcal P_{d,w},p)$ of a decoder that maps each syndrome to a class of largest probability; every tie rule gives the same value. The auxiliary decoder of Section~\ref{sec:cert} is defined on every code size, with block side $L$ and window radius $R$; $n_x=\max(6,\lceil w/L\rceil)$ and $n_y=\lfloor (d-1)/L\rfloor$ are as in Theorem~\ref{thm:ml}. The probabilities $\varepsilon_t$ that the reference blocks are bad are defined from the first stage of the decoder on a code of $7\times7$ blocks, as in Section~\ref{sec:cert-exp}. Let the first stage have block side $L\ge2$ and window radius $L\le R<\tfrac32L$, so that $D=6$, and let it satisfy (V6) and (Hcov). Lean derives the bound \eqref{eq:ml} of Theorem~\ref{thm:ml} from the hypothesis that $\varepsilon_t\le3.29\times10^{-4}$ for the seven types. From the bound it derives the threshold statement for every width $w\ge1$ that grows subexponentially in $d$, in particular for every width bounded by a polynomial in $d$: for every $p\in[0,0.103]$, the optimal failure probability tends to $0$ and is at most $e^{-(d-1)/(200L)}$ for all large $d$, that is, $e^{-(d-1)/70400}$ at $L=352$. The proof bounds $\PML$ by the failure probability of the auxiliary decoder, using Lemma~\ref{lem:monoq} and Proposition~\ref{prop:monosize}, which are also proved in Lean. The per-block hypothesis $(\mathrm H_\varepsilon)$ follows from three facts: from (V6), through the independence of blocks at block distance at least~$6$; from (Hcov), through the equality of the bad probabilities of blocks of the same type, for every $n_x\ge6$; and from the bounds on the $\varepsilon_t$. Lean proves Theorem~\ref{thm:cert} in the instance described after that theorem, $(\varepsilon,a_0,a_1)=(3.29\times10^{-4},5,16)$ with $D=6$, for every $L\ge2$ and every first stage, with weights in $[0.98,1.02]$ on the edges and in $[0,1.02]$ on the half-edges in the later stages, and with both terms of \eqref{eq:ml} and the constants shown; Theorem~\ref{thm:ml} uses it with unit weights (Section~\ref{sec:reduction}). The deterministic part of this proof is proved for every $g=\lfloor R/L\rfloor+1$, with $a_0\ge\max(2,D-1)$ and $a_1\ge a_0$, and so is the reduction, by (Hcov), to the $2g+3$ reference blocks for every $n_x\ge2g+2$. The experiment enters through (Bin). Lean proves the confidence statement of Section~\ref{sec:conf} for a sequential design with any finite set of looks: if the threshold $c_j$ of each look satisfies $F(c_j;n_j,3.29\times10^{-4})\le\alpha$, where $F$ is the binomial lower tail, then under (Bin) either the bound holds or the probability that every type is accepted at some look is at most $\alpha$ times the number of looks. It proves this both for the bound and for the threshold statement, with one acceptance event for all widths, and it does not assume a bound on the $\varepsilon_t$. For the registered looks the kernel checks $F(c_j;n_j,3.29\times10^{-4})\le10^{-9}/32R$, which holds for $n\ge4+\lfloor2R/L\rfloor$, and disjoint edge sets carry independent errors. \end{proof} If every block of type $t$ is bad with probability $\eps_t$, then $(\mathrm H_\eps)$ holds with $\eps=\max_t\eps_t$, by Lemma~\ref{s1:lem:dep}. \subsection{The deterministic lemma}\label{s1:sec:det} From now on, $a_0\ge D-1$, $a_1\ge a_0$, $a_1\ge2D-2$, and $a_1$ is even. (The condition $a_1\ge a_0$ is used only in the strip argument below.) The declared rows are $0,\dots,g$ and $n_y-g-1,\dots,n_y-1$. Since $R\ge(g-1)L$, we have $D\ge2g+2$; hence $a_0\ge2g+1$, so that $\lceil a_0/2\rceil\ge g+1$, and $h_s=a_1/2+1\ge D>g$ for the strip depth $h_s$ used below. Besides the declared rows, this is all that the proof uses about $g$. The lemmas of this section carry the letters (A), (B), (C), (W) and (X) of the outline of the proof of Theorem~\ref{thm:cert}. \paragraph{Clusters.} With the blocks of the declared rows counted as bad, the \emph{clusters} are the components of the bad blocks (declared or not) under adjacency at distance at most $a_0$. Distinct clusters are at distance at least $a_0+1\ge D$. $\Gbot$ and $\Gtop$ are the clusters that contain the declared rows at the bottom and at the top (possibly the same cluster). Every other cluster is \emph{interior}; its blocks lie in the rows $g+1+a_0,\dots,n_y-g-2-a_0$. \begin{lemma}[A]\label{s1:lem:A} Take the components of $F$ on the checks (a half-edge belongs to the component of its check; $b_1$ and $b_2$ join nothing). A component of $F$ that meets no bad block has no odd check and lies within distance $L-1$ of each block it meets. Every component of $F$ meets at most one cluster. \end{lemma} \begin{proof} Let $c$ be a good block. Then $c$ is in the rows $g+1,\dots,n_y-g-2$, and no path of $F$ from a check of $c$ reaches $\ell_\infty$ distance $L$ from $c$: every edge changes each coordinate by at most $1$, so the first check of such a path at distance at least $L$ from $c$ is at distance exactly $L$, and the path up to that check lies in $N_1(c)$, which would make $c$ long. (Since $c$ is in rows $g+1,\dots,n_y-g-2$ and $g\ge1$, the blocks of $N_1(c)$ contain no check of row $0$ or $H-1$, so the path meets no half-edge before that check.) The odd checks of $F$ are the residual defects, which lie in flagged, hence bad, blocks; so a component meeting no bad block has none. Suppose a component meets two clusters $K_1\ne K_2$. A path in it from $K_1$ to $K_2$ leaves $K_1$ into a block $c'$ adjacent to $K_1$, which is good because $a_0\ge1$. The whole component then lies within distance $L-1$ of $c'$, so it meets only blocks within distance $1$ of $c'$; in particular $K_2$ has a block within distance $1$ of $c'$, hence within distance $2\le a_0$ of $K_1$, a contradiction. \end{proof} Since flagged blocks are bad and the level-0 adjacency equals the cluster adjacency, every level-0 component lies in one cluster. Two clusters are \emph{linked} if a level-1 component (resolved or not) meets both, and the \emph{families} are the classes of clusters under the equivalence generated by linking. For a family $\cF$ let $Y_\cF$ be the sum of the components of $F$ that meet $\cF$ and of the corrections $C_K$ of the resolved components inside $\cF$. \begin{lemma}[B, decomposition]\label{s1:lem:B} $\partial Y_\cF=\Omega\cap\cF$ for every family, and \[ E\oplus C=\Bigl(\sum_{\text{components of $F$ meeting no bad block}}\Bigr)\oplus\bigoplus_\cF Y_\cF\oplus\Ctop . \] The components of $F$ that meet no bad block are closed and do not change the class. \end{lemma} \begin{proof} $E\oplus C=F\oplus\bigoplus_KC_K\oplus\Ctop$, and $F$ is the sum of its components; by Lemma~\ref{s1:lem:A}, each component meeting a bad block meets exactly one cluster, hence one family. The components of $F$ meeting $\cF$ have as odd checks the residual defects in the flagged blocks of $\cF$, and each resolved $C_K$ inside $\cF$ has odd checks $\cD'\cap K$. Every flagged block of $\cF$ is resolved exactly once, or its residual belongs to $\Omega$; this gives $\partial Y_\cF=\Omega\cap\cF$. A component meeting no bad block has no odd check and lies within distance $L-1$ of a good block, so it touches no half-edge and its height is less than $3L\le H$; it is therefore a cycle of checks with no half-edge, which does not change the parity at $b_1$. \end{proof} \begin{lemma}[C, failure path]\label{s1:lem:C} If the decoder fails, then one of the following holds: \begin{enumerate}[label=(T\arabic*),leftmargin=2.5em] \item some family $\cF$ has $Y_\cF$ with odd degree at both $b_1$ and $b_2$; \item there is a sequence $b_1\to\cF_1\to\dots\to\cF_m\to b_2$ of distinct families in which consecutive families are joined by paths of $\Ctop$, and the first (last) link is a path of $\Ctop$ from $b_1$ (to $b_2$) or an odd degree of $Y_{\cF_1}$ at $b_1$ (of $Y_{\cF_m}$ at $b_2$). \end{enumerate} \end{lemma} \begin{proof} Decompose $\Ctop$ into paths that pair the checks of $\Omega$ with each other or with a boundary vertex, and form the multigraph whose vertices are the families and $b_1,b_2$: it has an edge for each such path (between the families, or the family and boundary vertex, containing its ends) and an edge $\cF b_i$ whenever $Y_\cF$ has odd degree at $b_i$. By the handshake lemma for $Y_\cF$ and Lemma~\ref{s1:lem:B}, every family vertex has even degree. If the decoder fails, $E\oplus C$ has odd degree at $b_1$, and by Lemma~\ref{s1:lem:B} so has $b_1$ in the multigraph; hence $b_1$ and $b_2$ lie in one component of the multigraph, and a simple path joins them. If this path is $b_1\to\cF\to b_2$ and both of its edges are odd degrees of $Y_\cF$, this is case (T1); otherwise the path is as in (T2). (A minimum-weight $\Ctop$ contains no path between two boundary vertices, since weights are positive.) \end{proof} \begin{lemma}[W, parity witnesses]\label{s1:lem:W} \leavevmode \begin{enumerate}[label=(W\arabic*),leftmargin=2.8em,start=0] \item An odd level-0 component $K$ in an interior cluster has, in the same cluster, a flagged block at distance at least $a_0+1$ from $K$. \item Let $K_1$ be an odd level-1 component such that every cluster meeting $K_1$ is interior. Then one of these clusters contains a flagged block of another level-1 component, at distance at least $a_1+1$ from $K_1$. \end{enumerate} \begin{enumerate}[label=(R),leftmargin=2.8em] \item Every check of $\Omega$ lies in a flagged block of an odd level-0 component whose blocks belong to an odd level-1 component. Consequently, a path of $\Ctop$ between two different families of a (T2) chain joins blocks at distance at least $a_1+1$. \end{enumerate} \end{lemma} \begin{proof} The components of $F$ that meet an interior cluster reach no rough side, since the cluster's blocks lie in the rows $g+1+a_0,\dots,n_y-g-2-a_0$ and the components stay within distance $L-1$ of good blocks outside it. Their odd checks are the residual defects in the cluster's flagged blocks, so the number of these defects is even. For (W0): $|\cD'\cap K|$ is odd, so the cluster has residual defects outside $K$, that is, in another level-0 component, which is at distance at least $a_0+1$ from $K$. For (W1), add to the components of $F$ meeting an interior cluster the resolved level-0 corrections inside it; the odd checks of the sum are the residual defects of the cluster's odd level-0 components, again an even number. Summing over the clusters that meet $K_1$, all interior by assumption, the total number of such defects is even, while $K_1$ contains an odd number of them; so some cluster has level-1 residual outside $K_1$, that is, in a flagged block of another level-1 component, at distance at least $a_1+1$ from $K_1$. (R) holds by the construction of $\Omega$. Blocks of distinct level-1 components are more than $a_1$ apart, and the two ends of a path of $\Ctop$ between different families lie in different level-1 components, because a level-1 component lies in a single family. \end{proof} \paragraph{Strips and the sub-path of a chain.} Put $h_s=a_1/2+1$. The bottom strip $\Sbot$ is the set of block rows $\le h_s$, the top strip $\Stop$ the set of rows $\ge n_y-1-h_s$. A \emph{bottom (top) strip family} is a family with a block in $\Sbot$ ($\Stop$); a family containing $\Gbot$ is a bottom strip family. A family $\cF$ with $Y_\cF$ of odd degree at $b_1$ is also a bottom strip family: a half-edge of $Y_\cF$ at $b_1$ lies in a component of $F$ meeting block row $0$, whose blocks are declared and belong to $\Gbot$, or in a correction $C_K$ whose region reaches row $0$, so that $K$ has a block within $\max(\lceil a_0/2\rceil,a_1/2)\le h_s$ rows of row $0$. The same holds at the top. On a (T2) chain, let $\cF_0$ be the last bottom strip family ($b_1$ if there is none) and $\cF_{m+1}$ the first top strip family after it ($b_2$ if there is none); the families $\cF_1,\dots,\cF_m$ between them are \emph{intermediate}. If $\cF_0$ is also a top strip family, it has blocks in both strips; this case is counted with (T1) in Section~\ref{s1:sec:bound}, so we assume $\cF_0\ne\cF_{m+1}$ there. An intermediate family contains no block of the strips and hence, since $g0$ and $s\ge0$ let \[ t(v)=e^{\lambda\kappa|v|_1+s\,v_y},\qquad \Tt_0=\sum_{v\in S_0}t(v),\qquad \Tt_1=\sum_{v\in S_1}t(v), \] where $v_y$ is the signed row component of $v$. Define \begin{gather*} U_0=\eps T_0,\quad \Ut=\eps\Tt_0,\quad \tilde Q=\eps T_0+\frac{\Ut}{1-\Ut},\quad \tilde V=\eps\Tt_1\tilde Q,\quad V_0=\eps T_1\Bigl(\eps T_0+\frac{U_0}{1-U_0}\Bigr),\\ W_0=\frac1{1-\Ut},\qquad B_0=\frac1{1-U_0},\qquad Q_m=\bigl((1-\Ut)^{-2}-1\bigr)B_0+\eps T_0+B_0-1 . \end{gather*} For $a,c\ge0$ let $M_{a,c}=\sum_{x:\,|x|_\infty\ge\sigma_w}\bigl(w^{*a}*\mathbf 1_{S_0}^{*c}\bigr)(x)$, where $w=\mathbf 1_{S_0}\,t$ and $*$ is convolution on $\mathbb Z^2$: it counts tree paths with $a$ tilted and then $c$ untilted steps in $S_0$ that end at $\ell_\infty$ distance at least $\sigma_w$. Put \[ \mathrm{Wit}_{\mathrm{on}}=W_0\sum_{a,c\ge0}\eps^{a+c}M_{a,c},\qquad \mathrm{Wit}_{\mathrm{off}}=\sum_{c\ge1}\eps^cM_{0,c}\big|_{\lambda=s=0}, \] $\mathrm{off}=(1+\kappa)D\nu$, and \[ \Phi=e^{\lambda\,\mathrm{off}}\,\eps\,\Bigl[\mathrm{Wit}_{\mathrm{on}}+\frac{Q_m\,\eps T_1\,\mathrm{Wit}_{\mathrm{off}}}{1-V_0}\Bigr](1-\tilde V)^{-2},\qquad J=\sum_{\Delta\in\mathbb Z^2,\,|\Delta|_\infty\ge\sigma_w}e^{-\lambda|\Delta|_1+s\Delta_y},\qquad r=J\,\Phi . \] $J$ is finite if and only if $s<\lambda$. For the spanning case let $T_1(s)=\sum_{v\in S_1}e^{sv_y}$, $U_0(s)=\eps\sum_{v\in S_0}e^{sv_y}$ and \[ V_1(s)=\eps T_1(s)\Bigl(\eps T_0+\frac{U_0(s)}{1-U_0(s)}\Bigr). \] \subsubsection{The theorem} \begin{theorem}\label{s1:thm:main} Let $L\ge2$, $0\le R<\tfrac32L$, $D=4+\lfloor2R/L\rfloor$, $a_0\ge D-1$, and let $a_1$ be even with $a_1\ge a_0$ and $a_1\ge2D-2$; put $h_s=a_1/2+1$ and $H_0=2h_s+A_1+1=2a_1+D+2$. Assume $(\mathrm H_\eps)$. \begin{enumerate}[label=(\alph*),leftmargin=2em] \item If $V_1(0)<0.9$, then with $s_1=\sup\{s\ge0:V_1(s)\le0.9,\ U_0(s)\le0.9\}$, \[ \Pr(\mathrm{T1},\text{ or (T2) with }\cF_0=\cF_{m+1})\le C_1\,n_x\,e^{-s_1(n_y-H_0)},\qquad C_1=\frac{(h_s+1)\,W_1\,(1+\eps T_1(s_1)W_1)}{1-V_1(s_1)}, \] where $W_1=1/(1-U_0(s_1))$. \item If at some $0\le s<\lambda$ we have $\Ut<1$, $\tilde V<1$, $V_0<1$ and $r<1$, then \[ \Pr(\mathrm{T2},\ \cF_0\ne\cF_{m+1})\le C_2\,n_x\,e^{-s(n_y-H_0)},\qquad C_2=\frac{4(h_s+1)\,G_{\mathrm{bot}}\,J\,E_{\mathrm{top}}\,e^{\lambda c_{\mathrm{ends}}}}{1-r}, \] where $G_{\mathrm{bot}}=W_0/(1-\tilde V)$, $E_{\mathrm{top}}=\eps W_0(1+\eps\Tt_1W_0)/(1-\tilde V)$ and $c_{\mathrm{ends}}=D\nu+\kappa D\nu+\kappa\nu+\kappa(2h_s+A_1)+2.04\,\kappa/L$. \end{enumerate} Consequently, the failure probability of the decoder on $\mathcal P_{n_yL+1,n_xL}$ is at most $C_1n_xe^{-s_1(n_y-H_0)}+C_2n_xe^{-s_2(n_y-H_0)}$ with $s_2=s$. \end{theorem} This is Theorem~\ref{thm:cert} with explicit constants; the constants depend on $L$ only through the last term of $c_{\mathrm{ends}}$, which decreases in $L$. The rest of this section proves it. Throughout, a \emph{configuration} is an error $E$, and every sum over block tuples counts each tuple once; tuples that cannot arise only add nonnegative terms. \subsubsection{Routes through a family}\label{s1:sec:routes} Fix a family $\cF$ of a (T2) chain, with entry check $u$ and exit check $v$ (for $\cF_0$ only an exit, for $\cF_{m+1}$ only an entry). Join two clusters of $\cF$ if some level-1 component has odd level-0 components $o$ in one and $o'$ in the other at distance at most $a_1$. This graph on the clusters of $\cF$ is connected, because each level-1 component is $a_1$-connected and each odd level-0 component lies in one cluster. Take a simple path $c_0=\mathcal C(u),\dots,c_t=\mathcal C(v)$ in it, where $\mathcal C(x)$ is the cluster containing $\beta(x)$, and for each step a pair $(o,o')$ at distance at most $a_1$ with blocks $b_o\in o$ and $b_{o'}\in o'$ at distance at most $a_1$. Root $c_0$ at $\beta(u)$ and $c_{j+1}$ at $b_{o'}$, and select blocks as in Lemma~\ref{s1:lem:select}. The \emph{route} of $\cF$ is the sequence of selected blocks formed by the tree path in $c_j$ from its root to the selected block $s_j$ that covers $b_o$ (in-cluster steps in $S_0$), the \emph{link} $s_j\to\mathrm{root}(c_{j+1})$, and so on, ending in $c_t$ with the tree path from its root to the selected block $\sigma(\cF)$ that covers $\beta(v)$. A link has length at least $a_0+1\ge D$ (the clusters are distinct) and at most $(D-1)+a_1=A_1$, so its step lies in $S_1$. \emph{Leaves.} Every root is a block of an odd level-0 component: $\beta(u)$ by (R), and $b_{o'}$ because $o'$ belongs to a level-1 component. In an interior cluster, by (W0) and Lemma~\ref{s1:lem:select}(ii) the cluster has at least two selected blocks. For every route cluster whose route part is its root alone, other than the cluster $\mathcal C^*$ below, add one tree neighbour of the root (a \emph{leaf}, with displacement in $S_0$, not on the route). \emph{Witness.} Let $K_j$ and $K'_j$ be the level-1 components of the links that enter and leave $c_j$, with $K_0=K(u)$ and $K'_t=K(v)$, the level-1 components of $u$ and $v$. \begin{itemize}[leftmargin=2em] \item[($\alpha$)] If $K_j\ne K'_j$ for some $j$, put $\mathcal C^*=c_j$ and $e^*=\mathrm{root}(c_j)$, a block of $K_j$. The block $b_o$ of the leaving link (or $\beta(v)$ if $j=t$) belongs to $K'_j$, so it is at distance at least $a_1+1$ from $e^*$, and the selected block $b'$ that covers it satisfies $|b'-e^*|_\infty\ge a_1+1-(D-1)=\sigma_w$. \item[($\alpha'$)] Otherwise every link belongs to $K=K(u)=K(v)$, which is odd because it carries the residual check $u$, and by (W1) a cluster $\mathcal C^*$ meeting $K$ contains a block of a level-1 component $K'\ne K$. If $\mathcal C^*$ is a route cluster, its root $e^*$ is a block of $K$, and the selected block $b'$ covering the block of $K'$ satisfies $|b'-e^*|_\infty\ge\sigma_w$. \item[($\beta$)] If $\mathcal C^*$ is not a route cluster, follow a chain of odd level-0 components of $K$ from a route cluster $\mathcal C_x$ to $\mathcal C^*$, shortened so that the clusters after $\mathcal C_x$ are distinct and off the route, and root each of them at the block reached by the link into it (an \emph{excursion}); again $e^*=\mathrm{root}(\mathcal C^*)$ is a block of $K$ and $|b'-e^*|_\infty\ge\sigma_w$. \end{itemize} In all cases the tree path $\pi$ in $\mathcal C^*$ from $e^*$ to $b'$ has at least one step, so $\mathcal C^*$ needs no leaf. The \emph{skeleton} of $\cF$ consists of the route, the leaves, $\pi$ and, in case ($\beta$), the excursion: the tree path in $\mathcal C_x$ from a route block to the start of the first excursion link, the excursion links, and the excursion clusters with their own leaves. All skeleton blocks are distinct selected blocks, so by Lemma~\ref{s1:lem:select} and $(\mathrm H_\eps)$ the probability that all of them are bad is at most $\eps$ to the number of them. (The skeleton of an intermediate family contains no declared block.) \subsubsection{Proof of part (a)} Let $\cF$ be a family with blocks in both strips; this covers (T1), where some $Y_\cF$ has odd degree at $b_1$ and at $b_2$, and the case $\cF_0=\cF_{m+1}$. Take, as in Section~\ref{s1:sec:routes}, a route through the clusters of $\cF$ from a block in $\Sbot$ or in a declared bottom row to a block in $\Stop$ or in a declared top row, with leaves on the link-entered clusters. If $\cF$ contains $\Gbot$, choose the route to start at a declared block of $\Gbot$; this is possible because the graph on the clusters of $\cF$ is connected, and then the route, a simple path in that graph, never returns to $\Gbot$. Cut it at the last block $b_s$ that lies in $\Sbot$ or in a declared row and at the first later block that lies in $\Stop$ or in a declared row; the counted part runs from $b_s$ to the block $b_e$ before that cut. There are at most $(h_s+1)\,n_x$ choices for $b_s$, which is not counted with a factor $\eps$; every later route block and every leaf is bad, selected and not declared. Every later link enters an interior cluster, which has (W0), except possibly one link into the non-declared part of $\Gtop$, whose target may lack (W0). The block $b_e$ is within $A_1$ rows of a block of $\Stop$ or of a declared row, so the signed row progress from $b_s$ to $b_e$ is at least $(n_y-1-h_s-A_1)-h_s=n_y-H_0$. Multiplying the indicator by $e^{s(\text{progress}-(n_y-H_0))}\ge1$ and distributing $e^{s\,\text{progress}}$ over the steps gives, summed over all counted routes, \[ (h_s+1)\,n_x\cdot W_1\cdot\sum_{k\ge0}V_1(s)^k\cdot(1+\eps T_1(s)W_1)\cdot e^{-s(n_y-H_0)}, \] since the in-cluster steps from $b_s$ contribute $\sum_kU_0(s)^k=W_1$, each link into an interior cluster contributes $\eps T_1(s)$ times $\eps T_0$ (root with a leaf, the route staying at the root) plus $U_0(s)/(1-U_0(s))$ (one or more route steps), which is $V_1(s)$, and the one exceptional link contributes at most $1+\eps T_1(s)W_1$. At $s=s_1$ this is $C_1n_xe^{-s_1(n_y-H_0)}$. \subsubsection{The counting lemma for intermediate families} \begin{lemma}\label{s1:lem:T2} Let $\cF_1,\dots,\cF_m$ be the intermediate families of a (T2) chain, $D'_i=\mathrm{root}(\cF_{i+1})-\sigma(\cF_i)$ the jump displacements ($0\le i\le m$, with $\sigma(\cF_0)$ the block of $\cF_0$'s route that covers $\beta(v_0)$) and $R_i=\sigma(\cF_i)-\mathrm{root}(\cF_i)$ the route displacements ($1\le i\le m$). Then: \begin{enumerate}[label=(\roman*),leftmargin=2em] \item $|D'_i|_\infty\ge\sigma_w$ for every jump; \item $\sum_{i=0}^m|D'_i|_1\le\kappa\sum_{i=1}^m|R_i|_1+m\,\mathrm{off}+c_{\mathrm{ends}}+\kappa\,\rho_{\mathrm{bot}}+\kappa\,\rho_{\mathrm{top}}$, where $\rho_{\mathrm{bot}}$ and $\rho_{\mathrm{top}}$ are the $\ell_1$ lengths, in blocks, of the end routes of Section~\ref{s1:sec:ends}; \item summed over all skeletons of $\cF_1,\dots,\cF_m$ and all landing roots, with the weight $\eps$ per skeleton block, $e^{\lambda\kappa|v|_1+sv_y}$ per route step $v$, and $e^{-\lambda|D'|_1+sD'_y}$ per jump, each intermediate family contributes at most $\Phi$ and each jump at most $J$. \end{enumerate} \end{lemma} \begin{proof} (i) By (R), $v_i$ and $u_{i+1}$ lie in odd level-0 components of odd level-1 components, in $\cF_i$ and $\cF_{i+1}$; a level-1 component lies in one family, so these level-1 components differ, and blocks of different level-1 components are at distance at least $a_1+1$. Since $|\sigma(\cF_i)-\beta(v_i)|_\infty\le D-1$, we get $|D'_i|_\infty\ge a_1+1-(D-1)=\sigma_w$. (ii) By Section~\ref{s1:sec:metric}, the path $P_i$ weighs at least $0.98\,L\,(|D'_i|_1-D\nu)$: the root of $\cF_{i+1}$ is $\beta(u_{i+1})$, and $\sigma(\cF_i)$ is within $D-1$ of $\beta(v_i)$, which costs $(D-1)\nu$, plus $\nu$ for the offsets of the checks in their blocks. Likewise $d(u_i,v_i)\le1.02\,L\,(|R_i|_1+D\nu)$. Inserting these and the end bounds of Section~\ref{s1:sec:ends} into Lemma~\ref{s1:lem:X} and dividing by $0.98\,L$ gives (ii), since $1.02/0.98\le\kappa$ and $\mathrm{off}=(1+\kappa)D\nu$. (iii) For every configuration in (T2) choose one skeleton for each intermediate family as in Section~\ref{s1:sec:routes}. On that configuration (ii) holds for the data of the chosen skeletons, so \[ 1\le\exp\Bigl(\lambda\Bigl(\kappa\sum_i|R_i|_1+m\,\mathrm{off}+c_{\mathrm{ends}}+\kappa\rho_{\mathrm{bot}}+\kappa\rho_{\mathrm{top}}-\sum_i|D'_i|_1\Bigr)\Bigr), \] and $|R_i|_1$ is at most the sum of the $\ell_1$ norms of the route steps of $\cF_i$. The signed row progress of the block path from $b_s$ to $b_e$ (Section~\ref{s1:sec:ends}) is the sum of the row components of all route steps and jumps, in-block offsets telescoping, and it is at least $n_y-H_0$; so also $1\le e^{s(\text{progress}-(n_y-H_0))}$. Taking expectations and the union over skeletons, the probability is at most the sum, over all skeleton tuples, of the product of these factors and $\eps$ per skeleton block. The sum factorizes. Per jump, the landing root of $\cF_{i+1}$ ranges over the $\Delta=D'_i$ with $|\Delta|_\infty\ge\sigma_w$: factor $J$. Per family in cases ($\alpha$), ($\alpha'$): the route clusters $c_0,\dots,c_t$, one of which is $\mathcal C^*$. Each link contributes $\eps\Tt_1$ (its target block and its tilted step), and each route cluster other than $\mathcal C^*$ contributes $\tilde Q$: either the root with a leaf ($\eps T_0$, the route staying at the root) or $k\ge1$ tilted route steps ($\Ut^k$). $\mathcal C^*$ contributes $\mathrm{Wit}_{\mathrm{on}}$: its route part from $e^*$ shares an initial segment of $a$ tilted steps with $\pi$, $\pi$ continues with $c$ untilted steps and ends at distance at least $\sigma_w$ from $e^*$ (the count $M_{a,c}$), and the rest of the route part from the branching block contributes $W_0$. The position of $\mathcal C^*$ among the $t+1$ route clusters gives $\sum_t(t+1)\tilde V^t=(1-\tilde V)^{-2}$, and the landing root gives $\eps$. In case ($\beta$), the marked route cluster $\mathcal C_x$ contributes $Q_m$: a route part with $k\ge1$ steps, $k+1$ choices of the branching block and the excursion's in-cluster walk ($B_0$), or the root with a leaf and an empty excursion walk ($\eps T_0$), or a non-empty excursion walk from the root ($B_0-1$); the excursion links are untilted ($\eps T_1$ each), the excursion clusters contribute $\sum_jV_0^j=(1-V_0)^{-1}$, and $\mathcal C^*$ contributes $\mathrm{Wit}_{\mathrm{off}}$ through $\pi$ from its root. Together with $e^{\lambda\,\mathrm{off}}$ per family this gives at most $\Phi$ per intermediate family. \end{proof} \subsubsection{The ends, and proof of part (b)}\label{s1:sec:ends} Assume $\cF_0\ne\cF_{m+1}$, and first that both are strip families. \emph{Bottom end.} Choose a route in $\cF_0$ that ends at the selected block $\sigma(\cF_0)$ covering $\beta(v_0)$ and that starts in a declared row of $\Gbot$, if $\cF_0$ contains $\Gbot$ (the tree path of $\Gbot$ from a declared block, then links into interior clusters; the route never returns to $\Gbot$), and otherwise at a block of $\Sbot$. Let $b_s$ be the last block of the route that is declared or lies in $\Sbot$. There are at most $(h_s+1)\,n_x$ positions for $b_s$, each with weight at most $1$; every later route block has its factor $\eps$, and every later link enters an interior cluster, which has (W0). The route from $b_s$ therefore contributes at most $G_{\mathrm{bot}}=W_0/(1-\tilde V)$. Its length $\rho_{\mathrm{bot}}=|\sigma(\cF_0)-b_s|_1$ enters (ii) above through \[ d(v_0,b_1)\le1.02\,L\,\bigl(\rho_{\mathrm{bot}}+D\nu\bigr)+1.02\,\bigl(h_sL+1.02\bigr), \] a path from $v_0$ to a check of $b_s$, then straight down at most $h_sL$ rows, then a half-edge of weight at most $1.02$. Divided by $0.98\,L$, with $1.02/0.98\le\kappa$, the last term gives $\kappa h_s+1.02\,\kappa/L$; the two ends together give the term $2.04\,\kappa/L$ of $c_{\mathrm{ends}}$. \emph{Top end.} The route of $\cF_{m+1}$ starts at the landing root $\beta(u_{m+1})$, which has its factor $\eps$ (it is never declared), and stops before the first block that is declared or lies in $\Stop$; let $b_e$ be its last block. It may enter the non-declared part of $\Gtop$ once by a link whose target lacks (W0), with weight $\eps\Tt_1$ instead of $\tilde V$, and then continues by in-cluster steps; so it contributes at most $E_{\mathrm{top}}=\eps W_0(1+\eps\Tt_1W_0)/(1-\tilde V)$. Both of its ends are selected blocks, and $b_e$ lies within $h_s+A_1$ block rows of the top row, so with $\rho_{\mathrm{top}}=|b_e-\beta(u_{m+1})|_1$, \[ d(u_{m+1},b_2)\le1.02\,L\,\bigl(\rho_{\mathrm{top}}+\nu\bigr)+1.02\,\bigl((h_s+A_1)L+1.02\bigr). \] \emph{Assembly.} The chain from $\cF_0$ to $\cF_{m+1}$ has $m$ intermediate families and $m+1$ jumps; the extra jump adds $D\nu$ in (ii). Adding the two end bounds, divided by $0.98\,L$, gives the constant $c_{\mathrm{ends}}=D\nu+\kappa D\nu+\kappa\nu+\kappa(2h_s+A_1)+2.04\,\kappa/L$ of the theorem. The signed row progress from $b_s$ (row at most $h_s$) to $b_e$ (row at least $n_y-1-h_s-A_1$) is at least $n_y-H_0$. By Lemma~\ref{s1:lem:T2}(iii), the probability of a (T2) chain with strip families at both ends is at most \[ (h_s+1)\,n_x\cdot G_{\mathrm{bot}}\cdot J\sum_{m\ge0}r^m\cdot E_{\mathrm{top}}\cdot e^{\lambda c_{\mathrm{ends}}}\cdot e^{-s(n_y-H_0)} . \] If $\cF_0=b_1$ or $\cF_{m+1}=b_2$, the chain starts or ends with a path of $\Ctop$ to the boundary. The landing sum of such a boundary match over the $n_x$ block columns is dominated by the corresponding strip factor $(h_s+1)\,n_x\,G_{\mathrm{bot}}\,J$, respectively $J\,E_{\mathrm{top}}$, and a factor $4$ covers the four variants. With $\sum_mr^m=(1-r)^{-1}$ this is $C_2\,n_x\,e^{-s(n_y-H_0)}$. This proves part (b), and with part (a) and Lemma~\ref{s1:lem:C} the theorem. \subsection{Evaluation of the constants}\label{s1:sec:numbers} \paragraph{Method.} All counts are exact integers: $T_0$, $T_1$ and the sums over $S_0$ and $S_1$ are finite sums. The witness counts $M_{a,c}$ for $a+c\le9$ are computed by discrete Fourier convolution on a grid large enough that no wrap-around occurs, which reproduces the direct convolution up to rounding; the remaining terms with $a+c\ge10$ are bounded by the sum over all walks, $\sum_{n\ge10}\sum_{a=0}^n\Ut^{\,a}U_0^{\,n-a}$. The landing sum has the closed form \[ J=\frac{1+x}{1-x}\Bigl(1+\frac{y_+}{1-y_+}+\frac{y_-}{1-y_-}\Bigr)-\sum_{|\Delta|_\infty<\sigma_w}e^{-\lambda|\Delta|_1+s\Delta_y},\qquad x=e^{-\lambda},\ y_\pm=e^{-(\lambda\mp s)}, \] valid for $s<\lambda$. In the numerical evaluation the offset is taken as $\mathrm{off}+\kappa/2$, which only increases $r$. For given $\eps$, the rate $s$ of part (b) is the largest $s$ (by bisection) for which $\min_\lambda r(\lambda,s)\le0.9$ over a geometric grid of $\lambda$, possibly multiplied by a fixed fraction in $\{1,0.9,0.8,0.7,0.6\}$ chosen to minimize the code size at which the bound drops below $0.1$; then $\lambda$ is the minimizer at that $s$. The rate $s_1$ of part (a) is found by bisection. All arithmetic is in double precision. The stated constants are rounded: rates down, prefactors up, so that the stated bound is implied by the computed one. \paragraph{Convergence limits.} For $D=6$, $a_0=5$, $a_1=16$ and $\kappa=1.05$, one has $T_0=320$, $T_1=1728$, $\sigma_w=12$, $h_s=9$ and $H_0=40$. The spanning term converges ($V_1(0)\le0.9$) for $\eps\le8.301\times10^{-4}$, and the chain term ($\min_\lambda r(\lambda,0)\le0.9$) for $\eps\le3.982\times10^{-4}$. For comparison, with $D=5$, $a_0=4$ and $a_1=12$, which serve window radii $\tfrac12L\le R