Setting and result
The rotated surface code decoded by minimum-weight perfect matching is a standard model of a fault-tolerant quantum memory. Under circuit-level noise, simulations place its threshold near 0.5–1% [9 , 2 ] , and for the circuit considered here the logical failure curves cross near 5 × 10 − 3 5\times10^{-3} 5 × 1 0 − 3 Remark 11.6 ). But rigorous thresholds are much smaller. The path argument of Dennis, Kitaev, Landahl and Preskill [1 ] gives 1.7 × 10 − 4 1.7\times10^{-4} 1.7 × 1 0 − 4 [3 ] reaches 7.4 × 10 − 4 7.4\times10^{-4} 7.4 × 1 0 − 4 1.04 × 10 − 3 1.04\times10^{-3} 1.04 × 1 0 − 3 2 × 10 − 3 2\times10^{-3} 2 × 1 0 − 3 § 10 ).
Code and circuit
Fix an odd distance d ≥ 3 d\geq3 d ≥ 3
D = { ( x , y ) : x , y ∈ { 1 , 3 , … , 2 d − 1 } } . \mathcal{D}=\{(x,y):x,y\in\{1,3,\ldots,2d-1\}\}. D = {( x , y ) : x , y ∈ { 1 , 3 , … , 2 d − 1 }} . 2020 Mathematics Subject Classification. 81P73; 94B35, 05C38, 68V05.
Key words and phrases. Quantum error correction, surface code, fault tolerance, threshold, minimum-weight perfect matching, circuit-level noise, computer-assisted proof. A point m = ( x , y ) m=(x,y) m = ( x , y ) x , y ∈ { 0 , 2 , … , 2 d } x,y\in\{0,2,\ldots,2d\} x , y ∈ { 0 , 2 , … , 2 d } N ( m ) = { m + ( ± 1 , ± 1 ) } ∩ D N(m)=\{m+(\pm1,\pm1)\}\cap D N ( m ) = { m + ( ± 1 , ± 1 )} ∩ D X X X x / 2 + y / 2 x/2+y/2 x /2 + y /2 Z Z Z m m m ∣ N ( m ) ∣ ≥ 2 \lvert N(m)\rvert\ge2 ∣ N ( m )∣ ≥ 2 x ∈ { 0 , 2 d } x\in\{0,2d\} x ∈ { 0 , 2 d } y ∈ { 0 , 2 d } y\in\{0,2d\} y ∈ { 0 , 2 d } d 2 − 1 d^2-1 d 2 − 1 m m m ∏ q ∈ N ( m ) X q \prod_{q\in N(m)}X_q ∏ q ∈ N ( m ) X q ∏ q ∈ N ( m ) Z q \prod_{q\in N(m)}Z_q ∏ q ∈ N ( m ) Z q
δ X = ( ( 1 , 1 ) , ( − 1 , 1 ) , ( 1 , − 1 ) , ( − 1 , − 1 ) ) , δ Z = ( ( 1 , 1 ) , ( 1 , − 1 ) , ( − 1 , 1 ) , ( − 1 , − 1 ) ) . \delta^X=((1,1),(-1,1),(1,-1),(-1,-1)),\qquad\delta^Z=((1,1),(1,-1),(-1,1),(-1,-1)). δ X = (( 1 , 1 ) , ( − 1 , 1 ) , ( 1 , − 1 ) , ( − 1 , − 1 )) , δ Z = (( 1 , 1 ) , ( 1 , − 1 ) , ( − 1 , 1 ) , ( − 1 , − 1 )) . One round of syndrome extraction consists of eight steps.
(S1) Reset every measure qubit to ∣ 0 ⟩ \lvert0\rangle ∣ 0 ⟩
(S2) Apply H H H
(S3–S6) In step 2 + k 2+k 2 + k k = 1 , … , 4 k=1,\ldots,4 k = 1 , … , 4 CX ( m → m + δ k X ) \operatorname{CX}(m\mathbin{\to}m+\delta^X_k) CX ( m → m + δ k X ) m m m m + δ k X ∈ D m+\delta^X_k\in D m + δ k X ∈ D CX ( m + δ k Z → m ) \operatorname{CX}(m+\delta^Z_k\mathbin{\to}m) CX ( m + δ k Z → m ) m m m m + δ k Z ∈ D m+\delta^Z_k\in D m + δ k Z ∈ D
(S7) Apply H H H
(S8) Measure every measure qubit in the Z Z Z
Each qubit takes part in at most one operation per step. The layout and the four CX layers coincide with those of the circuits surface_code:rotated_memory_x/z generated by Stim [4 ] . The orders δ X \delta^X δ X δ Z \delta^Z δ Z [5 , 2 ] .
In the memory experiment in basis Z Z Z , every data qubit is prepared in ∣ 0 ⟩ \lvert0\rangle ∣ 0 ⟩ 0 , … , T − 1 0,\ldots,T-1 0 , … , T − 1 T ≥ 1 T\ge1 T ≥ 1 Z Z Z s m , r s_{m,r} s m , r m m m r r r f q f_q f q q q q m m m
D m , 0 = s m , 0 , D m , r = s m , r ⊕ s m , r − 1 ( 1 ≤ r ≤ T − 1 ) , D m , T = s m , T − 1 ⊕ ⨁ q ∈ N ( m ) f q . D_{m,0}=s_{m,0},\qquad D_{m,r}=s_{m,r}\oplus s_{m,r-1}\ (1\le r\le T-1),\qquad D_{m,T}=s_{m,T-1}\oplus\bigoplus_{q\in N(m)}f_q. D m , 0 = s m , 0 , D m , r = s m , r ⊕ s m , r − 1 ( 1 ≤ r ≤ T − 1 ) , D m , T = s m , T − 1 ⊕ q ∈ N ( m ) ⨁ f q . We call r r r layer of D m , r D_{m,r} D m , r ⨁ q ∈ D , y ( q ) = 1 f q \bigoplus_{q\in D,\ y(q)=1}f_q ⨁ q ∈ D , y ( q ) = 1 f q Z L Z_L Z L X X X ∣ + ⟩ \lvert+\rangle ∣ + ⟩ X L X_L X L x ( q ) = 1 x(q)=1 x ( q ) = 1 Table 3 , V1).
Table 3. Computer verification for Theorem 1.1 . Lemma 2.3(c) needs only d ≤ 9 d \le9 d ≤ 9 T ≤ 5 T \le5 T ≤ 5
Noise
A location is one of the following. Each location fails independently with probability p p p
A reset or preparation. A failed reset to ∣ 0 ⟩ \lvert0\rangle ∣ 0 ⟩ ∣ + ⟩ \lvert+\rangle ∣ + ⟩ X X X Z Z Z
A measurement. A failed measurement reports the flipped outcome.
An H H H X X X Y Y Y Z Z Z 1 / 3 1/3 1/3
A CX gate. Failure is followed by one of the 15 non-identity two-qubit Paulis, each with probability 1 / 15 1/15 1/15
A qubit is idle in a step if no reset, gate or measurement acts on it. Thus data qubits are idle in steps (S1) (except in round 0), (S2), (S7), (S8) and in each of (S3)–(S6) in which they have no CX partner. Z-type measure qubits are idle in (S2) and (S7) and in the CX steps without a partner, while X-type measure qubits are idle in the CX steps without a partner. A fault outcome is a location together with the Pauli or flip that follows its failure. Its probability is p π ( f ) p\,\pi(f) p π ( f ) π ( f ) ∈ { 1 , 1 3 , 1 15 } \pi(f)\in\{1,\frac{1}{3},\frac{1}{15}\} π ( f ) ∈ { 1 , 3 1 , 15 1 }
Decoding graph and decoder
We describe basis Z Z Z X X X V V V D m , r D_{m,r} D m , r signature σ ( f ) ⊆ V \sigma(f)\subseteq V σ ( f ) ⊆ V f f f f f f ℓ ( f ) ∈ { 0 , 1 } \ell(f)\in\{0,1\} ℓ ( f ) ∈ { 0 , 1 } Lemma 2.1 , ∣ σ ( f ) ∣ ≤ 2 \lvert\sigma(f)\rvert\le2 ∣ σ ( f )∣ ≤ 2 ℓ ( f ) \ell(f) ℓ ( f ) σ ( f ) \sigma(f) σ ( f ) decoding graph G G G V ∪ { b 1 , b 2 } V \cup\{b_1,b_2\} V ∪ { b 1 , b 2 } e ( f ) e(f) e ( f ) e ( f ) = σ ( f ) e(f)=\sigma(f) e ( f ) = σ ( f ) ∣ σ ( f ) ∣ = 2 |\sigma(f)|=2 ∣ σ ( f ) ∣ = 2 e ( f ) = { u , b 1 } e(f)=\{u,b_1\} e ( f ) = { u , b 1 } { u , b 2 } \{u,b_2\} { u , b 2 } σ ( f ) = { u } \sigma(f)=\{u\} σ ( f ) = { u } ℓ ( f ) = 1 \ell(f)=1 ℓ ( f ) = 1 ℓ ( f ) = 0 \ell(f)=0 ℓ ( f ) = 0 e e e
c e = ∑ f : e ( f ) = e π ( f ) , q e = c e p . c_e=\sum_{f:e(f)=e}\pi(f),\qquad q_e=c_ep. c e = f : e ( f ) = e ∑ π ( f ) , q e = c e p . The weights are w e = log ( ( 1 − r e ) / r e ) w_e=\log((1-r_e)/r_e) w e = log (( 1 − r e ) / r e ) r e r_e r e q e ( 1 − q e ) ≤ r e ≤ q e q_e(1-q_e)\le r_e\le q_e q e ( 1 − q e ) ≤ r e ≤ q e r e = q e r_e=q_e r e = q e r e r_e r e e ( f ) = e e(f)=e e ( f ) = e ℓ \ell ℓ c ℓ , e c_{\ell,e} c ℓ , e π ( f ) \pi(f) π ( f ) f f f ℓ \ell ℓ e ( f ) = e e(f)=e e ( f ) = e c ℓ , e c_{\ell,e} c ℓ , e ℓ \ell ℓ profile of e e e ( 1 − ∏ ℓ ( 1 − 2 c ℓ , e p ) ) / 2 (1-\prod_\ell(1-2c_{\ell,e}p))/2 ( 1 − ∏ ℓ ( 1 − 2 c ℓ , e p )) /2 p p p e e e profile weights if r e = ψ ( p , profile of e ) r_e=\psi(p,\text{profile of }e) r e = ψ ( p , profile of e ) ψ \psi ψ p ≤ 2 × 10 − 3 p\le2\times10^{-3} p ≤ 2 × 1 0 − 3 q e q_e q e 154 15 ⋅ 2 × 10 − 3 < 0.021 \frac{154}{15}\cdot2\times10^{-3}<0.021 15 154 ⋅ 2 × 1 0 − 3 < 0.021 Lemma 2.1 ), so all weights are positive.
For a set C C C ∂ C ⊆ V \partial C\subseteq V ∂ C ⊆ V C C C A ⊆ V A\subseteq V A ⊆ V C C C ∂ C = A \partial C=A ∂ C = A ∣ C ∩ δ ( b 1 ) ∣ |C\cap\delta(b_1)| ∣ C ∩ δ ( b 1 ) ∣ δ ( b 1 ) \delta(b_1) δ ( b 1 ) b 1 b_1 b 1 A A A C C C fails if its prediction differs from the actual flip of the logical outcome.
Result
Theorem 1.1. Let d ≥ 3 d\ge3 d ≥ 3 T ≥ 1 T\ge1 T ≥ 1 B ∈ { X , Z } B\in\{X,Z\} B ∈ { X , Z } 0 < p ≤ p ∗ = 1.04 × 10 − 3 0<p\le p_* = 1.04\times10^{-3} 0 < p ≤ p ∗ = 1.04 × 1 0 − 3 λ = 31 p \lambda=31\sqrt{p} λ = 31 p B B B T T T § 1.3 , fails with probability
P f a i l ≤ ( T + 1 ) ( d + 1 ) 2 ⋅ 2 c max p 1 − c max p ⋅ λ d − 1 1 − λ ≤ 0.104 ( T + 1 ) ( d + 1 ) λ d 1 − λ , c max = 154 15 . P_{\mathrm{fail}}\le\frac{(T+1)(d+1)}{2}\cdot2\sqrt{\frac{c_{\max}p}{1-c_{\max}p}}\cdot\frac{\lambda^{d-1}}{1-\lambda}\le0.104(T+1)(d+1)\frac{\lambda^d}{1-\lambda},\qquad c_{\max}=\frac{154}{15}. P fail ≤ 2 ( T + 1 ) ( d + 1 ) ⋅ 2 1 − c m a x p c m a x p ⋅ 1 − λ λ d − 1 ≤ 0.104 ( T + 1 ) ( d + 1 ) 1 − λ λ d , c m a x = 15 154 . We call P f a i l / T P_{\mathrm{fail}}/T P fail / T B B B T + 1 ≤ 2 T T+1\le2T T + 1 ≤ 2 T P f a i l / T ≤ 0.208 ( d + 1 ) λ d / ( 1 − λ ) P_{\mathrm{fail}}/T\le0.208(d+1)\lambda^d/(1-\lambda) P fail / T ≤ 0.208 ( d + 1 ) λ d / ( 1 − λ ) T T T p ≤ p ∗ p\le p_* p ≤ p ∗ λ ≤ 0.99972 \lambda\le0.99972 λ ≤ 0.99972 d d d p = 10 − 3 p=10^{-3} p = 1 0 − 3 λ = 0.98031 \lambda=0.98031 λ = 0.98031 P f a i l / T ≤ 10.6 ( d + 1 ) λ d P_{\mathrm{fail}}/T\le10.6(d+1)\lambda^d P fail / T ≤ 10.6 ( d + 1 ) λ d p = 10 − 4 p=10^{-4} p = 1 0 − 4 0.31 ( d + 1 ) ( 0.31 ) d 0.31(d+1)(0.31)^d 0.31 ( d + 1 ) ( 0.31 ) d P f a i l / T P_{\mathrm{fail}}/T P fail / T d ≥ 3 d\ge3 d ≥ 3 p ≤ 5 × 10 − 4 p\le5\times10^{-4} p ≤ 5 × 1 0 − 4 d ≥ 423 d\ge423 d ≥ 423 p = 10 − 3 p=10^{-3} p = 1 0 − 3 d ≥ 63063 d\ge63063 d ≥ 63063 p = p ∗ p=p_* p = p ∗
Theorem 1.2. In the setting of Theorem 1.1 :
(a) if 0 < p ≤ 1.6 × 10 − 3 0<p\le1.6\times10^{-3} 0 < p ≤ 1.6 × 1 0 − 3 λ = 0.997 ( p / ( 1.6 × 10 − 3 ) ) 21 / 50 \lambda=0.997\left(p/(1.6\times10^{-3})\right)^{21/50} λ = 0.997 ( p / ( 1.6 × 1 0 − 3 ) ) 21/50
P f a i l ≤ 0.032 ( T + 1 ) ( d + 1 ) λ d 1 − λ . P_{\mathrm{fail}}\le0.032(T+1)(d+1)\frac{\lambda^d}{1-\lambda}. P fail ≤ 0.032 ( T + 1 ) ( d + 1 ) 1 − λ λ d . (b) if the weights are profile weights , 0 < p ≤ p ∗ ∗ = 2 × 10 − 3 0<p\le p_{**}=2\times10^{-3} 0 < p ≤ p ∗∗ = 2 × 1 0 − 3 λ = 0.999 ( p / p ∗ ∗ ) 9 / 25 \lambda=0.999\left(p/p_{**}\right)^{9/25} λ = 0.999 ( p / p ∗∗ ) 9/25
P f a i l ≤ 0.061 ( T + 1 ) ( d + 1 ) λ d 1 − λ . P_{\mathrm{fail}}\le0.061(T+1)(d+1)\frac{\lambda^d}{1-\lambda}. P fail ≤ 0.061 ( T + 1 ) ( d + 1 ) 1 − λ λ d . Part (b) implies P f a i l / T ≤ 0.122 ( d + 1 ) λ d / ( 1 − λ ) P_{\mathrm{fail}}/T\le0.122(d+1)\lambda^d/(1-\lambda) P fail / T ≤ 0.122 ( d + 1 ) λ d / ( 1 − λ ) λ < 0.999 \lambda<0.999 λ < 0.999 p ≤ p ∗ ∗ p\le p_{**} p ≤ p ∗∗ p = 10 − 3 p=10^{-3} p = 1 0 − 3 λ < 0.7784 \lambda<0.7784 λ < 0.7784 P f a i l / T P_{\mathrm{fail}}/T P fail / T 0.551 ( d + 1 ) ( 0.7784 ) d 0.551(d+1)(0.7784)^d 0.551 ( d + 1 ) ( 0.7784 ) d d ≥ 5 d\ge5 d ≥ 5 10 − 6 10^{-6} 1 0 − 6 d ≥ 71 d\ge71 d ≥ 71 p = 10 − 3 p=10^{-3} p = 1 0 − 3 λ < 0.8185 \lambda<0.8185 λ < 0.8185
P f a i l / T ≤ 0.353 ( d + 1 ) ( 0.8185 ) d P_{\mathrm{fail}}/T \le0.353\,(d+1)\,(0.8185)^d P fail / T ≤ 0.353 ( d + 1 ) ( 0.8185 ) d p < 1.92 × 10 − 4 p < 1.92 \times10^{-4} p < 1.92 × 1 0 − 4 31 p 31\sqrt{p} 31 p Theorem 1.1 is smaller than that of part (b).
The circuit of § 1.1 has eight steps per round. A common leaner schedule measures and resets the measure qubits in a single step and prepares and measures the X-type ones in the X X X § 7 ). It has fewer idle steps, and the same two arguments yield larger thresholds.
Theorem 1.3. For the lean schedule of Section 7, with the noise model, memory experiments and decoder of Sections 1.2 and 1.3, let d ≥ 3 d \ge3 d ≥ 3 T ≥ 1 T \ge1 T ≥ 1 B ∈ { X , Z } B \in\{X,Z\} B ∈ { X , Z }
(a) If 0 < p ≤ 1.53 × 10 − 3 0 < p \le1.53 \times10^{-3} 0 < p ≤ 1.53 × 1 0 − 3 λ = 25.55 p \lambda= 25.55\sqrt{p} λ = 25.55 p
P f a i l ≤ 0.0985 ( T + 1 ) ( d + 1 ) λ d 1 − λ . P_{\mathrm{fail}} \le0.0985\,(T+1)(d+1)\frac{\lambda^d}{1-\lambda}. P fail ≤ 0.0985 ( T + 1 ) ( d + 1 ) 1 − λ λ d . (b) If 0 < p ≤ 2.4 × 10 − 3 0 < p \le2.4 \times10^{-3} 0 < p ≤ 2.4 × 1 0 − 3 λ = 0.997 ( p / ( 2.4 × 10 − 3 ) ) 21 / 50 \lambda= 0.997\left(p/(2.4 \times10^{-3})\right)^{21/50} λ = 0.997 ( p / ( 2.4 × 1 0 − 3 ) ) 21/50
P f a i l ≤ 0.028 ( T + 1 ) ( d + 1 ) λ d 1 − λ . P_{\mathrm{fail}} \le0.028\,(T+1)(d+1)\frac{\lambda^d}{1-\lambda}. P fail ≤ 0.028 ( T + 1 ) ( d + 1 ) 1 − λ λ d . (c) If the weights are profile weights, 0 < p ≤ 3 × 10 − 3 0 < p \le3 \times10^{-3} 0 < p ≤ 3 × 1 0 − 3 λ = 0.997 ( p / ( 3 × 10 − 3 ) ) 9 / 25 \lambda= 0.997\left(p/(3 \times10^{-3})\right)^{9/25} λ = 0.997 ( p / ( 3 × 1 0 − 3 ) ) 9/25
P f a i l ≤ 0.052 ( T + 1 ) ( d + 1 ) λ d 1 − λ . P_{\mathrm{fail}} \le0.052\,(T+1)(d+1)\frac{\lambda^d}{1-\lambda}. P fail ≤ 0.052 ( T + 1 ) ( d + 1 ) 1 − λ λ d . At p = 10 − 3 p = 10^{-3} p = 1 0 − 3 λ < 0.6714 \lambda< 0.6714 λ < 0.6714 P f a i l / T P_{\mathrm{fail}}/T P fail / T d ≥ 3 d \ge3 d ≥ 3 10 − 6 10^{-6} 1 0 − 6 d ≥ 43 d \ge43 d ≥ 43
§ 8 extends both arguments to error rates that depend on the type of operation (Theorem 8.1 ) and applies them to error models built from the published component error rates of six devices. Three models are certified: those of the Quantinuum Helios and H2 data sheets, and one with the error rates of IBM’s Heron r3 processor ibm_boston on a square grid. However, the models of Google’s and USTC’s processors are not certified. For them, floating-point estimates indicate that no positive potential satisfies the inequalities of Lemma 6.5 with λ < 1 \lambda< 1 λ < 1
Relation to earlier work
Dennis, Kitaev, Landahl and Preskill reduced matching failure to self-avoiding walks and proved a threshold of 1.14% for independent qubit and measurement errors, and of 1.7 × 10 − 4 1.7 \times10^{-4} 1.7 × 1 0 − 4 [1 ] . Fowler proved 7.4 × 10 − 4 7.4 \times10^{-4} 7.4 × 1 0 − 4 [3 ] , using the bound 14 p / 5 14p/5 14 p /5 [9 ] . General threshold theorems for local stochastic noise cover concatenated codes [6 ] and low-density parity-check codes [7 , 8 ] , and finite thresholds have recently been proved for the union-find and greedy decoders of the surface code under circuit-level local stochastic noise [10 ] . We keep the path reduction of [1 ] but replace the path count by the local criterion of § 4 , applied to the exact edge probabilities of the circuit. For Theorem 1.2 we also use the minimality of the correction along the path, beyond the half-weight inequality of [1 ] , and for part (b) a canonical choice among the minimum-weight corrections. For the circuit considered here, Fowler’s argument gives 4.3 × 10 − 4 4.3 \times10^{-4} 4.3 × 1 0 − 4 Remark 11.1 ), so Theorems 1.1 and 1.2 improve the rigorous value for this circuit by factors of about 2.4 and 4.6.
Outline
Section 2 describes the decoding graph: each fault outcome produces one edge, the bulk has twelve edges per node, and the graph has 29 node types in each sector. In Section 3 we reduce failure to weighted paths from b 1 b_1 b 1 b 2 b_2 b 2 [1 ] . We prove the local criterion in Section 4 and combine the pieces into Theorem 1.1 in Section 5. Section 6 proves Theorem 1.2 , Section 7 treats the lean schedule, and Section 8 treats non-uniform error rates. Computer-verified statements carry the mark † and are collected in Table 3 –Table 6 . Section 10 describes the formal proofs in Lean 4.
Table 6. Computer verification for Theorem 8.1 and the error models of Table 2.
The decoding graph
We write G d , T G_{d,T} G d , T d d d T T T height of a detector D m , r D_{m,r} D m , r y y y m m m x x x
Lemma 2.1 (†). For B ∈ { X , Z } B \in\{X,Z\} B ∈ { X , Z } d ≤ 13 d \le13 d ≤ 13 T ≤ 7 T \le7 T ≤ 7
(a) Every fault outcome flips at most two detectors.
(b) Outcomes with the same signature have the same value of ℓ \ell ℓ ℓ ( f ) = 1 \ell(f) = 1 ℓ ( f ) = 1 ∣ σ ( f ) ∣ = 1 |\sigma(f)| = 1 ∣ σ ( f ) ∣ = 1
(c) The edges at b 1 b_1 b 1 b 2 b_2 b 2 2 d − 2 2d - 2 2 d − 2
(d) The heights of the two ends of an edge in V differ by at most 2.
(e) b 1 b_1 b 1 ( T + 1 ) ( d + 1 ) / 2 (T + 1)(d + 1)/2 ( T + 1 ) ( d + 1 ) /2 c e ≤ 154 / 15 c_e \le154/15 c e ≤ 154/15 e e e
Part (a) says that the circuit-level noise decomposes into a graph in each sector. Here each Y Y Y X X X Z Z Z d ≥ 3 d \ge3 d ≥ 3 T ≥ 1 T \ge1 T ≥ 1
The bulk
Let m m m f a r f r o m 0 a n d far from 0 and f a r f r o m 0 an d m + δ k Z m + \delta_k^Z m + δ k Z m m m 2 + k 2 + k 2 + k q q q q ∓ ( 1 , 1 ) q \mp(1,1) q ∓ ( 1 , 1 ) q + ( 1 , − 1 ) q + (1,-1) q + ( 1 , − 1 ) q + ( − 1 , 1 ) q + (-1,1) q + ( − 1 , 1 ) q + ( − 1 , 1 ) q + (-1,1) q + ( − 1 , 1 ) q + ( 1 , − 1 ) q + (1,-1) q + ( 1 , − 1 ) q ∓ ( 1 , 1 ) q \mp(1,1) q ∓ ( 1 , 1 )
Lemma 2.2. In basis Z, a bulk detector v = D m , r v = D_{m,r} v = D m , r ( Δ x , Δ y , Δ r ) (\Delta x, \Delta y, \Delta r) ( Δ x , Δ y , Δ r )
Table 2.2.
In basis X the coefficients are the same, with offsets ± ( 2 , − 2 , 0 ) \pm(2,-2,0) ± ( 2 , − 2 , 0 ) ± ( 0 , 0 , 1 ) \pm(0,0,1) ± ( 0 , 0 , 1 ) ± ( 2 , 2 , 0 ) \pm(2,2,0) ± ( 2 , 2 , 0 ) ± ( 2 , 2 , − 1 ) \pm(2,2,-1) ± ( 2 , 2 , − 1 ) ± ( 2 , − 2 , 1 ) \pm(2,-2,1) ± ( 2 , − 2 , 1 ) ± ( 0 , 4 , − 1 ) \pm(0,4,-1) ± ( 0 , 4 , − 1 )
Proof. We treat basis Z, where only X components matter, and list the outcomes that produce each edge in Table 1, in units of p / 15 p/15 p /15 ∣ + ⟩ |+\rangle ∣ + ⟩ k k k ( k + 1 ) (k + 1) ( k + 1 ) k = 1 k = 1 k = 1 k = 2 k = 2 k = 2 k = 3 k = 3 k = 3
An X on a data qubit q q q q q q r − 1 r - 1 r − 1 r r r r r r ( 2 , 2 , 0 ) (2,2,0) ( 2 , 2 , 0 ) r r r q + ( 1 , 1 ) q + (1,1) q + ( 1 , 1 ) r r r q − ( 1 , 1 ) q - (1,1) q − ( 1 , 1 ) r + 1 r + 1 r + 1 ( − 2 , − 2 , 1 ) (-2,-2,1) ( − 2 , − 2 , 1 ) r − 1 r - 1 r − 1 r r r ( 2 , − 2 , 0 ) (2,-2,0) ( 2 , − 2 , 0 ) ( − 2 , 2 , 1 ) (-2,2,1) ( − 2 , 2 , 1 ) m ′ m' m ′ { m ′ + ( 1 , − 1 ) , m ′ + ( − 1 , − 1 ) } \{m' + (1,-1),m' + (-1,-1)\} { m ′ + ( 1 , − 1 ) , m ′ + ( − 1 , − 1 )} m ′ + ( 2 , 0 ) m' + (2,0) m ′ + ( 2 , 0 ) r r r m ′ + ( − 2 , 0 ) m' + (-2,0) m ′ + ( − 2 , 0 ) r + 1 r + 1 r + 1 m ′ + ( 0 , − 2 ) m' + (0,-2) m ′ + ( 0 , − 2 ) ( − 4 , 0 , 1 ) (-4,0,1) ( − 4 , 0 , 1 ) X X X Z Z Z m m m s m , r s_{m,r} s m , r ( 0 , 0 , 1 ) (0,0,1) ( 0 , 0 , 1 )
The same derivation with Z Z Z X X X
Table 1. Outcomes producing the twelve edges at a bulk detector (basis Z Z Z
Locality and node types
The type of a detector v ∈ V v \in V v ∈ V c e c_e c e e e e v v v b 1 b_1 b 1 b 2 b_2 b 2 b 1 b_1 b 1 b 2 b_2 b 2
Lemma 2.3. Let v = D m , r v = D_{m,r} v = D m , r
(a) If v ∈ σ ( f ) v \in\sigma(f) v ∈ σ ( f ) f f f ℓ ∞ \ell^\infty ℓ ∞ m m m r − 1 r-1 r − 1 r r r T − 1 T-1 T − 1 r = T r = T r = T
(b) The type of v v v ℓ ∞ \ell^\infty ℓ ∞ m m m X X X Z Z Z min ( r , 2 ) \min(r,2) min ( r , 2 ) min ( T − r , 2 ) \min(T-r,2) min ( T − r , 2 )
(c) For all odd d ≥ 3 d \ge3 d ≥ 3 T ≥ 1 T \ge1 T ≥ 1 G d , T G_{d,T} G d , T G d ′ , T ′ G_{d',T'} G d ′ , T ′ d ′ ∈ { 3 , 5 , 7 , 9 } d' \in\{3,5,7,9\} d ′ ∈ { 3 , 5 , 7 , 9 } T ′ ∈ { 1 , … , 5 } T' \in\{1,\ldots,5\} T ′ ∈ { 1 , … , 5 } Lemma 2.1 .
Proof. (a) We use the propagation rules from the proof of Lemma 2.2. In basis Z Z Z X X X X X X Z Z Z X X X q q q CX ( q → m ′ ) \operatorname{CX}(q \to m') CX ( q → m ′ ) Z Z Z m ′ m' m ′ q ∈ N ( m ′ ) q \in N(m') q ∈ N ( m ′ ) m ′ m' m ′ m ′ m' m ′ q q q X X X X X X Z Z Z X X X X X X m ′ m' m ′ N ( m ′ ) N(m') N ( m ′ ) m ′ m' m ′ m ′ m' m ′ X X X ρ \rho ρ s m ′ , ρ ′ s_{m',\rho'} s m ′ , ρ ′ ρ ′ ≥ ρ \rho' \ge\rho ρ ′ ≥ ρ ρ ′ ≥ ρ + 1 \rho' \ge\rho+ 1 ρ ′ ≥ ρ + 1 ρ \rho ρ ρ + 1 \rho+ 1 ρ + 1
(b) By (a), the outcomes with v v v m m m ρ \rho ρ ρ \rho ρ ρ + 1 \rho+ 1 ρ + 1 m m m m m m r − 1 r - 1 r − 1 r r r r + 1 r + 1 r + 1 min ( r , 2 ) \min(r, 2) min ( r , 2 ) min ( T − r , 2 ) \min(T - r, 2) min ( T − r , 2 )
(c) The bulk pattern of qubit positions and measure-qubit types is invariant under the lattice generated by ( 4 , 0 ) (4, 0) ( 4 , 0 ) ( 0 , 4 ) (0, 4) ( 0 , 4 ) ( 2 , 2 ) (2, 2) ( 2 , 2 ) y = 0 y = 0 y = 0 x ≡ 2 ( m o d 4 ) x \equiv2 \pmod{4} x ≡ 2 ( mod 4 ) y = 2 d y = 2d y = 2 d x ≡ 0 x \equiv0 x ≡ 0 x = 0 x = 0 x = 0 y ≡ 0 y \equiv0 y ≡ 0 x = 2 d x = 2d x = 2 d y ≡ 2 ( m o d 4 ) y \equiv2 \pmod{4} y ≡ 2 ( mod 4 ) d d d d d d m m m m m m d ≥ 9 d \ge9 d ≥ 9 G d , T G_{d,T} G d , T G 9 , T G_{9,T} G 9 , T [ 7 , 11 ] [7, 11] [ 7 , 11 ] G 9 G_9 G 9 m m m T ≥ 5 T \ge5 T ≥ 5 ( min ( r , 2 ) , min ( T − r , 2 ) ) (\min(r,2),\min(T-r,2)) ( min ( r , 2 ) , min ( T − r , 2 )) T ′ = 5 T' = 5 T ′ = 5 b 1 b_1 b 1 ρ + 1 \rho+ 1 ρ + 1 ρ \rho ρ ℓ ( f ) \ell(f) ℓ ( f ) X X X b 1 b_1 b 1 b 1 b_1 b 1 ( d + 1 ) / 2 (d + 1)/2 ( d + 1 ) /2
Corollary 2.4 (†). In each basis the detectors of all graphs G d , T G_{d,T} G d , T d ≥ 3 d \ge3 d ≥ 3 T ≥ 1 T \ge1 T ≥ 1
From matching failure to weighted paths
Fix an experiment and let F \mathcal{F} F E E E e e e f ∈ F f \in\mathcal{F} f ∈ F e ( f ) = e e(f) = e e ( f ) = e ∂ E \partial E ∂ E Lemma 2.1 (b) an outcome flips it if and only if its edge ends at b 1 b_1 b 1 ∣ E ∩ δ ( b 1 ) ∣ |E \cap\delta(b_1)| ∣ E ∩ δ ( b 1 ) ∣
Lemma 3.1. If the decoder fails with the minimizer C C C E △ C E \triangle C E △ C b 1 b_1 b 1 b 2 b_2 b 2
Proof. Let R = E △ C R=E\triangle C R = E △ C ∂ C = ∂ E \partial C=\partial E ∂ C = ∂ E R R R ∣ C ∩ δ ( b 1 ) ∣ |C\cap\delta(b_1)| ∣ C ∩ δ ( b 1 ) ∣ ∣ E ∩ δ ( b 1 ) ∣ |E\cap\delta(b_1)| ∣ E ∩ δ ( b 1 ) ∣ b 1 b_1 b 1 R R R R R R 2 ∣ R ∣ 2|R| 2∣ R ∣ b 2 b_2 b 2 ( V ∪ { b 1 , b 2 } , R ) (V\cup\{b_1,b_2\},R) ( V ∪ { b 1 , b 2 } , R ) b 1 b_1 b 1 b 2 b_2 b 2
Lemma 3.2. Every simple path from b 1 b_1 b 1 b 2 b_2 b 2 G d , T G_{d,T} G d , T d d d
Proof. By Lemma 2.1(c,d), the path enters V V V 2 2 2 2 d − 2 2d-2 2 d − 2 V V V 2 2 2 ( 2 d − 4 ) / 2 = d − 2 (2d-4)/2=d-2 ( 2 d − 4 ) /2 = d − 2 V V V
Lemma 3.3. Let γ ⊆ E △ C \gamma\subseteq E\triangle C γ ⊆ E △ C b 1 b_1 b 1 b 2 b_2 b 2 w ( γ ∩ E ) ≥ w ( γ ) / 2 w(\gamma\cap E)\ge w(\gamma)/2 w ( γ ∩ E ) ≥ w ( γ ) /2
Proof. We follow the argument of [1 Sec. 4] . Because the detector boundary of γ \gamma γ C △ γ C\triangle\gamma C △ γ w ( C ) ≤ w ( C △ γ ) = w ( C ) − w ( C ∩ γ ) + w ( γ ∖ C ) w(C)\le w(C\triangle\gamma)=w(C)-w(C\cap\gamma)+w(\gamma\setminus C) w ( C ) ≤ w ( C △ γ ) = w ( C ) − w ( C ∩ γ ) + w ( γ ∖ C ) γ ⊆ E △ C \gamma\subseteq E\triangle C γ ⊆ E △ C γ ∖ C = γ ∩ E \gamma\setminus C=\gamma\cap E γ ∖ C = γ ∩ E w ( C ∩ γ ) = w ( γ ) − w ( γ ∩ E ) w(C\cap\gamma)=w(\gamma)-w(\gamma\cap E) w ( C ∩ γ ) = w ( γ ) − w ( γ ∩ E )
Lemma 3.4. For every set S S S Pr ( S ⊆ E ) ≤ ∏ e ∈ S q e \Pr(S\subseteq E)\le\prod_{e\in S}q_e Pr ( S ⊆ E ) ≤ ∏ e ∈ S q e
Proof. If S ⊆ E S\subseteq E S ⊆ E e ∈ S e\in S e ∈ S f e ∈ F f_e\in\mathcal{F} f e ∈ F e ( f e ) = e e(f_e)=e e ( f e ) = e f e f_e f e
Pr ( S ⊆ E ) ≤ ∑ ( f e ) e ∈ S Pr ( f e ∈ F ∀ e ) ≤ ∑ ( f e ) e ∈ S ∏ e ∈ S p π ( f e ) = ∏ e ∈ S q e . \Pr(S\subseteq E)\le\sum_{(f_e)_{e\in S}}\Pr(f_e\in\mathcal{F}\ \forall e)\le\sum_{(f_e)_{e\in S}}\prod_{e\in S}p\,\pi(f_e)=\prod_{e\in S}q_e. Pr ( S ⊆ E ) ≤ ( f e ) e ∈ S ∑ Pr ( f e ∈ F ∀ e ) ≤ ( f e ) e ∈ S ∑ e ∈ S ∏ p π ( f e ) = e ∈ S ∏ q e . Lemma 3.5. Put a e = 2 q e / ( 1 − q e ) a_e=2\sqrt{q_e}/(1-q_e) a e = 2 q e / ( 1 − q e ) γ \gamma γ
∑ S ⊆ γ , w ( S ) ≥ w ( γ ) / 2 ∏ e ∈ S q e ≤ ∏ e ∈ γ a e . \sum_{\substack{S\subseteq\gamma,\\w(S)\ge w(\gamma)/2}}\prod_{e\in S}q_e\le\prod_{e\in\gamma}a_e. S ⊆ γ , w ( S ) ≥ w ( γ ) /2 ∑ e ∈ S ∏ q e ≤ e ∈ γ ∏ a e . Proof. Each term on the left satisfies w ( S ) − w ( γ ∖ S ) ≥ 0 w(S)-w(\gamma\setminus S)\ge0 w ( S ) − w ( γ ∖ S ) ≥ 0 ∏ e ∈ S q e e ( w ( S ) − w ( γ ∖ S ) ) / 2 \prod_{e\in S}q_e e^{(w(S)-w(\gamma\setminus S))/2} ∏ e ∈ S q e e ( w ( S ) − w ( γ ∖ S )) /2 S ⊆ γ S\subseteq\gamma S ⊆ γ
∏ e ∈ γ ( q e e w e / 2 + e − w e / 2 ) . \prod_{e\in\gamma}\left(q_ee^{w_e/2}+e^{-w_e/2}\right). e ∈ γ ∏ ( q e e w e /2 + e − w e /2 ) . With e w e = ( 1 − r e ) / r e e^{w_e}=(1-r_e)/r_e e w e = ( 1 − r e ) / r e q e ( 1 − q e ) ≤ r e ≤ q e q_e(1-q_e)\le r_e\le q_e q e ( 1 − q e ) ≤ r e ≤ q e
q e 1 − r e r e ≤ q e q e ( 1 − q e ) = q e 1 − q e , r e 1 − r e ≤ q e 1 − q e , q_e\sqrt{\frac{1-r_e}{r_e}}\le\frac{q_e}{\sqrt{q_e(1-q_e)}}=\sqrt{\frac{q_e}{1-q_e}},\qquad
\sqrt{\frac{r_e}{1-r_e}}\le\sqrt{\frac{q_e}{1-q_e}}, q e r e 1 − r e ≤ q e ( 1 − q e ) q e = 1 − q e q e , 1 − r e r e ≤ 1 − q e q e , so each factor is at most a e a_e a e
Proposition 3.6. Let Γ \Gamma Γ b 1 b_1 b 1 b 2 b_2 b 2 G d , T G_{d,T} G d , T P f a i l ≤ ∑ γ ∈ Γ ∏ e ∈ γ a e P_{\mathrm{fail}}\le\sum_{\gamma\in\Gamma}\prod_{e\in\gamma}a_e P fail ≤ ∑ γ ∈ Γ ∏ e ∈ γ a e
Proof. By Lemmas 3.1 and 3.3, failure implies that some γ ∈ Γ \gamma\in\Gamma γ ∈ Γ S = γ ∩ E S=\gamma\cap E S = γ ∩ E S ⊆ E S\subseteq E S ⊆ E w ( S ) ≥ w ( γ ) / 2 w(S)\ge w(\gamma)/2 w ( S ) ≥ w ( γ ) /2 γ \gamma γ S S S
A local criterion for non-backtracking walks
Lemma 4.1. Let G G G V ∪ { b 1 , b 2 } V\cup\{b_1,b_2\} V ∪ { b 1 , b 2 } b 1 b_1 b 1 b 2 b_2 b 2 a e > 0 a_e>0 a e > 0 e e e λ > 0 \lambda>0 λ > 0
Σ ( v ) : = ∑ e ∋ v a e λ + a e ≤ 1 for every v ∈ V . \Sigma(v):=\sum_{e\ni v}\frac{a_e}{\lambda+a_e}\le1\qquad\text{for every }v\in V. Σ ( v ) := e ∋ v ∑ λ + a e a e ≤ 1 for every v ∈ V . where the sum includes edges to b 1 b_1 b 1 b 2 b_2 b 2 κ = λ + max e ∋ b 2 a e \kappa=\lambda+\max_{e\ni b_2}a_e κ = λ + max e ∋ b 2 a e Σ ( b 1 ) = ∑ e ∋ b 1 a e / ( λ + a e ) \Sigma(b_1)=\sum_{e\ni b_1}a_e/(\lambda+a_e) Σ ( b 1 ) = ∑ e ∋ b 1 a e / ( λ + a e ) L ≥ 2 L\ge2 L ≥ 2 b 1 b_1 b 1 b 2 b_2 b 2 L L L
∑ γ ∏ e ∈ γ a e ≤ κ Σ ( b 1 ) λ L − 1 . \sum_{\gamma}\prod_{e\in\gamma}a_e\le\kappa\Sigma(b_1)\lambda^{L-1}. γ ∑ e ∈ γ ∏ a e ≤ κ Σ ( b 1 ) λ L − 1 . Proof. For an oriented edge ε = ( u → v ) \varepsilon=(u\to v) ε = ( u → v ) h ( ε ) = 1 / ( λ + a ε ) h(\varepsilon)=1/(\lambda+a_\varepsilon) h ( ε ) = 1/ ( λ + a ε ) m ≥ 1 m\ge1 m ≥ 1 ( x 0 → x 1 ) (x_0\to x_1) ( x 0 → x 1 ) x 0 ∈ V ∪ { b 1 } x_0\in V\cup\{b_1\} x 0 ∈ V ∪ { b 1 } x 1 ∈ V x_1\in V x 1 ∈ V W m ( x 0 → x 1 ) W_m(x_0\to x_1) W m ( x 0 → x 1 ) ∏ i = 1 m a x i x i + 1 \prod_{i=1}^{m}a_{x_i x_{i+1}} ∏ i = 1 m a x i x i + 1 x 1 , x 2 , … , x m + 1 x_1,x_2,\ldots,x_{m+1} x 1 , x 2 , … , x m + 1 x m + 1 = b 2 x_{m+1}=b_2 x m + 1 = b 2 x 2 , … , x m ∈ V x_2,\ldots,x_m\in V x 2 , … , x m ∈ V x i + 1 ≠ x i − 1 x_{i+1}\ne x_{i-1} x i + 1 = x i − 1 1 ≤ i ≤ m 1\le i\le m 1 ≤ i ≤ m m m m
W m ( x 0 → x 1 ) ≤ κ λ m h ( x 0 → x 1 ) . (1) W_m(x_0\to x_1)\le\kappa\lambda^m h(x_0\to x_1). \tag*{(1)} W m ( x 0 → x 1 ) ≤ κ λ m h ( x 0 → x 1 ) . (1) Because the edge { x 0 , x 1 } \{x_0,x_1\} { x 0 , x 1 } a x 0 x 1 / ( λ + a x 0 x 1 ) a_{x_0x_1}/(\lambda+a_{x_0x_1}) a x 0 x 1 / ( λ + a x 0 x 1 ) Σ ( x 1 ) \Sigma(x_1) Σ ( x 1 )
∑ e ∋ x 1 , e ≠ { x 0 , x 1 } a e λ + a e ≤ 1 − a x 0 x 1 λ + a x 0 x 1 = λ h ( x 0 → x 1 ) . (2) \sum_{\substack{e\ni x_1,\,e\ne\{x_0,x_1\}}}\frac{a_e}{\lambda+a_e}\le1-\frac{a_{x_0x_1}}{\lambda+a_{x_0x_1}}=\lambda h(x_0\to x_1). \tag*{(2)} e ∋ x 1 , e = { x 0 , x 1 } ∑ λ + a e a e ≤ 1 − λ + a x 0 x 1 a x 0 x 1 = λh ( x 0 → x 1 ) . (2) For m = 1 m=1 m = 1 W 1 ( x 0 → x 1 ) = a x 1 b 2 W_1(x_0\to x_1)=a_{x_1b_2} W 1 ( x 0 → x 1 ) = a x 1 b 2 x 1 x_1 x 1 b 2 b_2 b 2 0 0 0 a x 1 b 2 = ( λ + a x 1 b 2 ) ⋅ a x 1 b 2 / ( λ + a x 1 b 2 ) ≤ κ a x 1 b 2 / ( λ + a x 1 b 2 ) a_{x_1b_2}=(\lambda+a_{x_1b_2})\cdot a_{x_1b_2}/(\lambda+a_{x_1b_2})\le\kappa a_{x_1b_2}/(\lambda+a_{x_1b_2}) a x 1 b 2 = ( λ + a x 1 b 2 ) ⋅ a x 1 b 2 / ( λ + a x 1 b 2 ) ≤ κ a x 1 b 2 / ( λ + a x 1 b 2 ) m ≥ 2 m\ge2 m ≥ 2
W m ( x 0 → x 1 ) = ∑ x 2 ∈ V ∖ { x 0 } x 2 ∼ x 1 a x 1 x 2 W m − 1 ( x 1 → x 2 ) ≤ κ λ m − 1 ∑ x 2 a x 1 x 2 λ + a x 1 x 2 ≤ κ λ m h ( x 0 → x 1 ) , W_m(x_0\to x_1)=\sum_{\substack{x_2\in V\setminus\{x_0\}\\x_2\sim x_1}}a_{x_1x_2}W_{m-1}(x_1\to x_2)\le\kappa\lambda^{m-1}\sum_{x_2}\frac{a_{x_1x_2}}{\lambda+a_{x_1x_2}}\le\kappa\lambda^m h(x_0\to x_1), W m ( x 0 → x 1 ) = x 2 ∈ V ∖ { x 0 } x 2 ∼ x 1 ∑ a x 1 x 2 W m − 1 ( x 1 → x 2 ) ≤ κ λ m − 1 x 2 ∑ λ + a x 1 x 2 a x 1 x 2 ≤ κ λ m h ( x 0 → x 1 ) , by induction and (4.2). A simple path b 1 , x 1 , … , x L − 1 , b 2 b_1,x_1,\ldots,x_{L-1},b_2 b 1 , x 1 , … , x L − 1 , b 2 ∑ x 1 ∼ b 1 a b 1 x 1 W L − 1 ( b 1 → x 1 ) ≤ κ λ L − 1 Σ ( b 1 ) \sum_{x_1\sim b_1}a_{b_1x_1}W_{L-1}(b_1\to x_1)\le\kappa\lambda^{L-1}\Sigma(b_1) ∑ x 1 ∼ b 1 a b 1 x 1 W L − 1 ( b 1 → x 1 ) ≤ κ λ L − 1 Σ ( b 1 )
On the k k k a e = a a_e=a a e = a k a / ( λ + a ) ≤ 1 ka/(\lambda+a)\le1 k a / ( λ + a ) ≤ 1 λ ≥ ( k − 1 ) a \lambda\ge(k-1)a λ ≥ ( k − 1 ) a { a e } \{a_e\} { a e } Σ ≡ 1 \Sigma\equiv1 Σ ≡ 1 h h h λ \lambda λ
Proof of Theorem 1.1
The criterion holds at every detector
Let λ = 31 p \lambda=31\sqrt{p} λ = 31 p a e = p α e ( p ) a_e=\sqrt{p}\,\alpha_e(p) a e = p α e ( p ) α e ( p ) = 2 c e / ( 1 − c e p ) \alpha_e(p)=2\sqrt{c_e}/(1-c_ep) α e ( p ) = 2 c e / ( 1 − c e p )
Σ ( v ) = ∑ e ∋ v α e ( p ) 31 + α e ( p ) , \Sigma(v)=\sum_{e\ni v}\frac{\alpha_e(p)}{31+\alpha_e(p)}, Σ ( v ) = e ∋ v ∑ 31 + α e ( p ) α e ( p ) , which increases with p p p Σ ( v ) ≤ 1 \Sigma(v)\le1 Σ ( v ) ≤ 1 p = p ∗ p=p_* p = p ∗ 31 p ∗ = 0.999719 … ≥ 0.9997 31\sqrt{p_*}=0.999719\ldots\ge0.9997 31 p ∗ = 0.999719 … ≥ 0.9997 Σ ( v ) \Sigma(v) Σ ( v ) λ \lambda λ
∑ e ∋ v a e 0.9997 + a e ≤ 1 at p = p ∗ . (3) \sum_{e\ni v}\frac{a_e}{0.9997+a_e}\le1\qquad\text{at }p=p_*. \tag*{(3)} e ∋ v ∑ 0.9997 + a e a e ≤ 1 at p = p ∗ . (3) By Corollary 2.4 we need to check only 29 types per basis. For the bulk type of Lemma 2.2 the computation is short:
Table 1 (PDF p. 9).
and the weighted sum is 0.999409. The other 28 types satisfy (5.1) with left side at most 0.9629† . We list the values for all types in Appendix § 14 . The check is done in exact rational arithmetic, with rational upper bounds for the square roots (Table 3 , V6).
Assembly
We first check that the graph G d , T G_{d,T} G d , T Lemma 4.1 . Each edge comes from a nonempty signature, which contains a detector, so there is no edge between b 1 b_1 b 1 b 2 b_2 b 2 b 1 b_1 b 1 Proposition 3.6 , Lemma 3.2 and Lemma 4.1 , we obtain
P f a i l ≤ ∑ L ≥ d κ Σ ( b 1 ) λ L − 1 = κ Σ ( b 1 ) λ d − 1 1 − λ . P_{\mathrm{fail}} \le\sum_{L \ge d} \kappa\,\Sigma(b_1)\,\lambda^{L-1} = \kappa\,\Sigma(b_1)\frac{\lambda^{d-1}}{1-\lambda}. P fail ≤ L ≥ d ∑ κ Σ ( b 1 ) λ L − 1 = κ Σ ( b 1 ) 1 − λ λ d − 1 . Let a max = 2 c max p / ( 1 − c max p ) a_{\max}=2\sqrt{c_{\max}p}/(1-c_{\max}p) a m a x = 2 c m a x p / ( 1 − c m a x p ) Lemma 2.1 (e), κ ≤ λ + a max \kappa\le\lambda+a_{\max} κ ≤ λ + a m a x Σ ( b 1 ) \Sigma(b_1) Σ ( b 1 ) a max / ( λ + a max ) a_{\max}/(\lambda+a_{\max}) a m a x / ( λ + a m a x ) κ Σ ( b 1 ) ≤ ( T + 1 ) ( d + 1 ) 2 a max \kappa\,\Sigma(b_1)\le\frac{(T+1)(d+1)}{2}a_{\max} κ Σ ( b 1 ) ≤ 2 ( T + 1 ) ( d + 1 ) a m a x p ≤ p ∗ p\le p_* p ≤ p ∗ 1 − c max p ≥ 0.98932 1-c_{\max}p\ge0.98932 1 − c m a x p ≥ 0.98932 a max ≤ 6.4429 p a_{\max}\le6.4429\sqrt{p} a m a x ≤ 6.4429 p
P f a i l ≤ ( T + 1 ) ( d + 1 ) 2 ⋅ 6.4429 p ⋅ λ d − 1 1 − λ = 6.4429 62 ( T + 1 ) ( d + 1 ) λ d 1 − λ ≤ 0.104 ( T + 1 ) ( d + 1 ) λ d 1 − λ . \begin{aligned}
P_{\mathrm{fail}}\le\frac{(T+1)(d+1)}{2}\cdot6.4429\sqrt{p}\cdot\frac{\lambda^{d-1}}{1-\lambda} \\
&= \frac{6.4429}{62}(T+1)(d+1)\frac{\lambda^d}{1-\lambda}\le0.104(T+1)(d+1)\frac{\lambda^d}{1-\lambda}.
\end{aligned} P fail ≤ 2 ( T + 1 ) ( d + 1 ) ⋅ 6.4429 p ⋅ 1 − λ λ d − 1 = 62 6.4429 ( T + 1 ) ( d + 1 ) 1 − λ λ d ≤ 0.104 ( T + 1 ) ( d + 1 ) 1 − λ λ d . Proof of Theorem 1.2
In the proof of Theorem 1.1 we sum over all ways of labelling the edges of a path as errors or corrections, although most of these labellings cannot occur. Indeed, the correction edges on a stretch of the failure path belong to a minimum-weight correction. Their weight is therefore at most that of the error edges on the stretch plus any detour between its ends, and at most that of any set of edges with the same boundary. We turn these two inequalities into local exclusion rules (Definition 6.2 ) and count only the labelled paths that obey them. For profile weights a third rule uses the freedom in the choice of the minimizer: among the minimizers for which the decoder fails we take one that minimizes a fixed linear functional, and such a minimizer cannot turn a corner around which an equally heavy route of smaller value exists. These rules are the main new ingredient of the proof. For part (a) we fix p ∗ ∗ = 1 / 625 p_{**}=1/625 p ∗∗ = 1/625 s = 21 / 50 s=21/50 s = 21/50 p ∗ ∗ = 1 / 500 p_{**}=1/500 p ∗∗ = 1/500 s = 9 / 25 s=9/25 s = 9/25
Windows
For a path or walk P P P c ( P ) = ∏ e ∈ P c e c(P)=\prod_{e\in P}c_e c ( P ) = ∏ e ∈ P c e G / B G/B G / B G G G b 1 b_1 b 1 b 2 b_2 b 2 B B B C C C γ ⊆ E △ C \gamma\subseteq E\mathbin{\triangle}C γ ⊆ E △ C Lemma 3.1 . A window is a sub-path σ \sigma σ γ \gamma γ σ C = σ ∩ C \sigma_C=\sigma\cap C σ C = σ ∩ C σ E = σ ∩ E \sigma_E=\sigma\cap E σ E = σ ∩ E σ \sigma σ σ C \sigma_C σ C σ E \sigma_E σ E
Lemma 6.1. (a) For every window σ \sigma σ P ′ P' P ′ G / B G/B G / B σ \sigma σ w ( σ C ) − w ( σ E ) ≤ w ( P ′ ) w(\sigma_C)-w(\sigma_E)\le w(P') w ( σ C ) − w ( σ E ) ≤ w ( P ′ )
(b) For every X ⊆ C X\subseteq C X ⊆ C P ′ P' P ′ G / B G/B G / B X X X w ( X ) ≤ w ( P ′ ) w(X)\le w(P') w ( X ) ≤ w ( P ′ )
Proof. (a) The set C ′ = C △ σ △ P ′ C'=C\mathbin{\triangle}\sigma\mathbin{\triangle}P' C ′ = C △ σ △ P ′ ∂ C ′ = ∂ C \partial C'=\partial C ∂ C ′ = ∂ C C △ σ = ( C ∖ σ C ) ∪ σ E C\mathbin{\triangle}\sigma=(C\setminus\sigma_C)\cup\sigma_E C △ σ = ( C ∖ σ C ) ∪ σ E w ( C ′ ) ≤ w ( C ) − w ( σ C ) + w ( σ E ) + w ( P ′ ) w(C')\le w(C)-w(\sigma_C)+w(\sigma_E)+w(P') w ( C ′ ) ≤ w ( C ) − w ( σ C ) + w ( σ E ) + w ( P ′ ) w ( C ) ≤ w ( C ′ ) w(C)\le w(C') w ( C ) ≤ w ( C ′ )
(b) Similarly, the set C ′ = C △ X △ P ′ C'=C\mathbin{\triangle}X\mathbin{\triangle}P' C ′ = C △ X △ P ′ ∂ C ′ = ∂ C \partial C'=\partial C ∂ C ′ = ∂ C w ( C ′ ) ≤ w ( C ) − w ( X ) + w ( P ′ ) w(C')\le w(C)-w(X)+w(P') w ( C ′ ) ≤ w ( C ) − w ( X ) + w ( P ′ ) w ( C ) ≤ w ( C ′ ) w(C)\le w(C') w ( C ) ≤ w ( C ′ )
For a detector D m , r D_{m,r} D m , r m = ( x , y ) m=(x,y) m = ( x , y ) ϕ ( D m , r ) = x + 9 y + 81 r \phi(D_{m,r})=x+9y+81r ϕ ( D m , r ) = x + 9 y + 81 r C C C Φ ( C ) \Phi(C) Φ ( C ) ϕ ( u ) + ϕ ( v ) \phi(u)+\phi(v) ϕ ( u ) + ϕ ( v ) { u , v } \{u,v\} { u , v } C C C u , v ∈ V u,v\in V u , v ∈ V
A labelled window is a path σ = ( v 0 , … , v m ) \sigma=(v_0,\ldots,v_m) σ = ( v 0 , … , v m ) G G G 2 ≤ m ≤ 4 2\le m\le4 2 ≤ m ≤ 4 n C n_C n C n E n_E n E σ C \sigma_C σ C σ E \sigma_E σ E T ( σ ) T(\sigma) T ( σ ) σ C \sigma_C σ C head of σ \sigma σ v m − 1 v_{m-1} v m − 1 ball of a detector v v v v v v σ \sigma σ admissible walk for σ \sigma σ G / B G/B G / B b 1 b_1 b 1 b 2 b_2 b 2 B B B B B B
Definition 6.2. A labelled window σ \sigma σ excluded if it satisfies one of the following conditions.
(M) There is an admissible walk P ′ P' P ′ v 0 v_0 v 0 v m v_m v m h ′ h' h ′ v 0 , v m ∈ { b 1 , b 2 } v_0,v_m\in\{b_1,b_2\} v 0 , v m ∈ { b 1 , b 2 } k = n C − n E − h ′ ≥ 0 k=n_C-n_E-h'\ge0 k = n C − n E − h ′ ≥ 0
( 1 p ∗ ∗ ) k c ( σ E ) c ( P ′ ) c ( σ C ) > ∏ e ∈ σ C 1 1 − c e p ∗ ∗ ⋅ ( 1 1 − c max p ∗ ∗ ) h ′ . (4) \left(\frac{1}{p_{\ast\ast}}\right)^k \frac{c(\sigma_E)c(P')}{c(\sigma_C)}
>
\prod_{e\in\sigma_C}\frac{1}{1-c_e p_{\ast\ast}}\cdot
\left(\frac{1}{1-c_{\max}p_{\ast\ast}}\right)^{h'}. \tag*{(4)} ( p ∗∗ 1 ) k c ( σ C ) c ( σ E ) c ( P ′ ) > e ∈ σ C ∏ 1 − c e p ∗∗ 1 ⋅ ( 1 − c m a x p ∗∗ 1 ) h ′ . (4) (J) There are admissible walks, each from a vertex of T ( σ ) T(\sigma) T ( σ ) T ( σ ) T(\sigma) T ( σ ) B B B T ( σ ) T(\sigma) T ( σ ) P ′ P' P ′ h ′ h' h ′ k = n C − h ′ ≥ 0 k=n_C-h'\ge0 k = n C − h ′ ≥ 0
( 1 p ∗ ∗ ) k c ( P ′ ) c ( σ C ) > ∏ e ∈ σ C 1 1 − c e p ∗ ∗ ⋅ ( 1 1 − c max p ∗ ∗ ) h ′ . (5) \left(\frac{1}{p_{\ast\ast}}\right)^k \frac{c(P')}{c(\sigma_C)}
>
\prod_{e\in\sigma_C}\frac{1}{1-c_e p_{\ast\ast}}\cdot
\left(\frac{1}{1-c_{\max}p_{\ast\ast}}\right)^{h'}. \tag*{(5)} ( p ∗∗ 1 ) k c ( σ C ) c ( P ′ ) > e ∈ σ C ∏ 1 − c e p ∗∗ 1 ⋅ ( 1 − c m a x p ∗∗ 1 ) h ′ . (5) If T ( σ ) T(\sigma) T ( σ ) P ′ P' P ′
(S) (Only for Theorems 1.2(b) and 1.3(c).) The window has m = 2 m=2 m = 2 u = v 0 u=v_0 u = v 0 b = v 1 b=v_1 b = v 1 w = v 2 w=v_2 w = v 2 x ∉ { u , b , w } x\notin\{u,b,w\} x ∈ / { u , b , w } u u u w w w ϕ ( x ) < ϕ ( b ) \phi(x)<\phi(b) ϕ ( x ) < ϕ ( b ) u x ux ux x w xw x w u b ub u b b w bw b w
Rule (M) compares the window with an alternative route between its ends. Rule (J) compares its correction edges with a re-pairing of their endpoints. Rule (S) compares the corner u , b , w u,b,w u , b , w u , x , w u,x,w u , x , w x x x b b b
Lemma 6.3. (a) Let p ≤ p ∗ ∗ p\le p_{\ast\ast} p ≤ p ∗∗ C C C γ ∩ E \gamma\cap E γ ∩ E γ ∩ C \gamma\cap C γ ∩ C γ \gamma γ
(b) Let p ≤ p ∗ ∗ p\le p_{\ast\ast} p ≤ p ∗∗ C ∗ C^* C ∗ Φ \Phi Φ γ ⊆ E △ C ∗ \gamma\subseteq E\triangle C^* γ ⊆ E △ C ∗ γ \gamma γ
Proof. (a) Suppose that a window σ \sigma σ γ \gamma γ P ′ P' P ′ P ′ ′ P'' P ′′ P ′ P' P ′ w ( P ′ ′ ) ≤ w ( P ′ ) w(P'')\le w(P') w ( P ′′ ) ≤ w ( P ′ ) ϵ e = − ln ( 1 − q e ) \epsilon_e=-\ln(1-q_e) ϵ e = − ln ( 1 − q e ) q e ( 1 − q e ) ≤ r e ≤ q e q_e(1-q_e)\le r_e\le q_e q e ( 1 − q e ) ≤ r e ≤ q e ∣ w e + ln q e ∣ ≤ ϵ e \lvert w_e+\ln q_e\rvert\le\epsilon_e ∣ w e + ln q e ∣ ≤ ϵ e ϵ e \epsilon_e ϵ e e ∈ P ′ e\in P' e ∈ P ′ − ln ( 1 − c max p ) -\ln(1-c_{\max}p) − ln ( 1 − c m a x p )
Under (M), P ′ ′ P'' P ′′ σ \sigma σ b 1 b_1 b 1 b 2 b_2 b 2 B B B
w ( σ C ) − w ( σ E ) − w ( P ′ ) ≥ k ln 1 p + ln c ( σ E ) c ( P ′ ) c ( σ C ) − ∑ e ∈ σ ϵ e − ∑ e ∈ P ′ ϵ e . w(\sigma_C)-w(\sigma_E)-w(P')
\ge
k\ln\frac{1}{p}
+\ln\frac{c(\sigma_E)c(P')}{c(\sigma_C)}
-\sum_{e\in\sigma}\epsilon_e
-\sum_{e\in P'}\epsilon_e. w ( σ C ) − w ( σ E ) − w ( P ′ ) ≥ k ln p 1 + ln c ( σ C ) c ( σ E ) c ( P ′ ) − e ∈ σ ∑ ϵ e − e ∈ P ′ ∑ ϵ e . At p = p ∗ ∗ p=p_{\ast\ast} p = p ∗∗ p p p k ≥ 0 k\ge0 k ≥ 0 ϵ e \epsilon_e ϵ e w ( σ C ) − w ( σ E ) > w ( P ′ ′ ) w(\sigma_C)-w(\sigma_E)>w(P'') w ( σ C ) − w ( σ E ) > w ( P ′′ )
Under (J), each vertex of T ( σ ) T(\sigma) T ( σ ) P ′ ′ P'' P ′′ T ( σ ) T(\sigma) T ( σ ) σ C \sigma_C σ C σ E \sigma_E σ E w ( σ C ) > w ( P ′ ′ ) w(\sigma_C)>w(P'') w ( σ C ) > w ( P ′′ ) X = σ C X=\sigma_C X = σ C ( u , b , w ) (u,b,w) ( u , b , w ) γ \gamma γ x x x Q Q Q u b ub u b b w bw b w w x wx w x x u xu xu u b ub u b b w bw b w C ∗ C^* C ∗ C ′ = C ∗ △ Q C'=C^*\mathbin{\triangle} Q C ′ = C ∗ △ Q ∂ C ′ = ∂ C ∗ \partial C'=\partial C^* ∂ C ′ = ∂ C ∗ Q Q Q b 1 b_1 b 1 C ′ C' C ′ C ∗ C^* C ∗ w ( u x ) + w ( x w ) = w ( u b ) + w ( b w ) w(ux)+w(xw)=w(ub)+w(bw) w ( ux ) + w ( x w ) = w ( u b ) + w ( b w ) u x ux ux x w xw x w C ∗ C^* C ∗ w ( C ′ ) = w ( C ∗ ) w(C')=w(C^*) w ( C ′ ) = w ( C ∗ ) C ′ C' C ′ Φ ( C ′ ) − Φ ( C ∗ ) = 2 ( ϕ ( x ) − ϕ ( b ) ) < 0 \Phi(C')-\Phi(C^*)=2(\phi(x)-\phi(b))<0 Φ ( C ′ ) − Φ ( C ∗ ) = 2 ( ϕ ( x ) − ϕ ( b )) < 0 C ∗ C^* C ∗ x w xw x w C ∗ C^* C ∗ w ( C ′ ) = w ( C ∗ ) − w ( u b ) − w ( b w ) − w ( x w ) + w ( u x ) = w ( C ∗ ) − 2 w ( x w ) w(C')=w(C^*)-w(ub)-w(bw)-w(xw)+w(ux)=w(C^*)-2w(xw) w ( C ′ ) = w ( C ∗ ) − w ( u b ) − w ( b w ) − w ( x w ) + w ( ux ) = w ( C ∗ ) − 2 w ( x w ) w ( C ′ ) = w ( C ∗ ) − w ( Q ) w(C')=w(C^*)-w(Q) w ( C ′ ) = w ( C ∗ ) − w ( Q ) w ( C ′ ) < w ( C ∗ ) w(C')<w(C^*) w ( C ′ ) < w ( C ∗ ) C ∗ C^* C ∗
For example, for a window made of C-edges only, k ≥ 0 k\geq0 k ≥ 0
Labelled paths
A labelled path is a simple path b 1 = v 0 , v 1 , … , v L = b 2 b_1=v_0,v_1,\ldots,v_L=b_2 b 1 = v 0 , v 1 , … , v L = b 2 G G G
ω ( γ ) = ∏ E - e d g e s q e 1 − s ( 1 − q e ) − s ∏ C - e d g e s ( q e 1 − q e ) s , \omega(\gamma)=\prod_{\mathrm{E\text{-}edges}}q_e^{1-s}(1-q_e)^{-s}\prod_{\mathrm{C\text{-}edges}}\left(\frac{q_e}{1-q_e}\right)^s, ω ( γ ) = E - edges ∏ q e 1 − s ( 1 − q e ) − s C - edges ∏ ( 1 − q e q e ) s , and we write ω ( e , l ) \omega(e,l) ω ( e , l ) e e e l l l
Proposition 6.4. For every p ≤ p ∗ ∗ p\leq p_{**} p ≤ p ∗∗ P f a i l P_{\mathrm{fail}} P fail
Proof. Suppose the decoder fails. For part (a) let C C C C = C ∗ C=C^* C = C ∗ Lemma 6.3 (b). In both cases the decoder fails with C C C γ ⊆ E △ C \gamma\subseteq E\mathbin{\triangle}C γ ⊆ E △ C Lemma 3.1 , and label the edges of γ ∩ E \gamma\cap E γ ∩ E γ ∩ C \gamma\cap C γ ∩ C Lemma 6.3 no sub-path of γ \gamma γ γ \gamma γ S S S S ⊆ E S\subseteq E S ⊆ E Lemma 3.3 , w ( S ) ≥ w ( γ ∖ S ) w(S)\geq w(\gamma\setminus S) w ( S ) ≥ w ( γ ∖ S ) Lemma 3.4 , P f a i l P_{\mathrm{fail}} P fail ∏ e ∈ γ q e \prod_{e\in\gamma}q_e ∏ e ∈ γ q e Lemma 3.5 , we have ∏ e ∈ γ q e ≤ ∏ e ∈ S q e e s w e ∏ e ∈ γ ∖ S e − s w e \prod_{e\in\gamma}q_e\leq\prod_{e\in S}q_e e^{s w_e}\prod_{e\in\gamma\setminus S}e^{-s w_e} ∏ e ∈ γ q e ≤ ∏ e ∈ S q e e s w e ∏ e ∈ γ ∖ S e − s w e q e ( 1 − q e ) ≤ r e ≤ q e q_e(1-q_e)\leq r_e\leq q_e q e ( 1 − q e ) ≤ r e ≤ q e q e e s w e ≤ q e 1 − s ( 1 − q e ) − s q_e e^{s w_e}\leq q_e^{1-s}(1-q_e)^{-s} q e e s w e ≤ q e 1 − s ( 1 − q e ) − s e − s w e ≤ ( q e / ( 1 − q e ) ) s e^{-s w_e}\leq(q_e/(1-q_e))^s e − s w e ≤ ( q e / ( 1 − q e ) ) s
A criterion with memory
A state is a path v 0 , v 1 , v 2 , v 3 v_0,v_1,v_2,v_3 v 0 , v 1 , v 2 , v 3 v 1 , v 2 , v 3 ∈ V v_1,v_2,v_3\in V v 1 , v 2 , v 3 ∈ V v 0 ∈ V ∪ { b 1 } v_0\in V\cup\{b_1\} v 0 ∈ V ∪ { b 1 } l 1 l 2 l 3 l_1l_2l_3 l 1 l 2 l 3 successors are the states ( v 1 , v 2 , v 3 , v 4 ; l 2 l 3 l 4 ) (v_1,v_2,v_3,v_4;l_2l_3l_4) ( v 1 , v 2 , v 3 , v 4 ; l 2 l 3 l 4 ) v 4 ∈ V ∖ { v 0 , v 1 , v 2 } v_4\in V\setminus\{v_0,v_1,v_2\} v 4 ∈ V ∖ { v 0 , v 1 , v 2 } terminal moves are the edges { v 3 , b 2 } \{v_3,b_2\} { v 3 , b 2 } l 4 l_4 l 4 ( v 2 , v 3 , v 4 ) (v_2,v_3,v_4) ( v 2 , v 3 , v 4 ) ( v 1 , … , v 4 ) (v_1,\ldots,v_4) ( v 1 , … , v 4 ) ( v 0 , … , v 4 ) (v_0,\ldots,v_4) ( v 0 , … , v 4 ) l 3 l 4 l_3l_4 l 3 l 4 l 2 l 3 l 4 l_2l_3l_4 l 2 l 3 l 4 l 1 ⋯ l 4 l_1\cdots l_4 l 1 ⋯ l 4 v 4 = b 2 v_4=b_2 v 4 = b 2 v 3 v_3 v 3
Lemma 6.5. Let λ > 0 \lambda>0 λ > 0 H H H positive number to every state. Suppose that every state σ = ( v 0 , v 1 , v 2 , v 3 ; l 1 l 2 l 3 ) \sigma=(v_0,v_1,v_2,v_3;l_1l_2l_3) σ = ( v 0 , v 1 , v 2 , v 3 ; l 1 l 2 l 3 )
∑ s u c c e s s o r s ω ( v 3 v 4 , l 4 ) H ( v 1 , v 2 , v 3 , v 4 ; l 2 l 3 l 4 ) + ∑ t e r m i n a l m o v e s ω ( v 3 b 2 , l 4 ) ≤ λ H ( σ ) . (6) \sum_{\mathrm{successors}}\omega(v_3v_4,l_4)H(v_1,v_2,v_3,v_4;l_2l_3l_4)+\sum_{\mathrm{terminal\ moves}}\omega(v_3b_2,l_4)\leq\lambda H(\sigma). \tag*{(6)} successors ∑ ω ( v 3 v 4 , l 4 ) H ( v 1 , v 2 , v 3 , v 4 ; l 2 l 3 l 4 ) + terminal moves ∑ ω ( v 3 b 2 , l 4 ) ≤ λ H ( σ ) . (6) Then for every L ≥ 4 L\geq4 L ≥ 4 L L L
λ L − 3 ∑ ω ( b 1 v 1 , l 1 ) ω ( v 1 v 2 , l 2 ) ω ( v 2 v 3 , l 3 ) H ( b 1 , v 1 , v 2 , v 3 ; l 1 l 2 l 3 ) , \lambda^{L-3}\sum\omega(b_1v_1,l_1)\omega(v_1v_2,l_2)\omega(v_2v_3,l_3)H(b_1,v_1,v_2,v_3;l_1l_2l_3), λ L − 3 ∑ ω ( b 1 v 1 , l 1 ) ω ( v 1 v 2 , l 2 ) ω ( v 2 v 3 , l 3 ) H ( b 1 , v 1 , v 2 , v 3 ; l 1 l 2 l 3 ) , where the sum runs over the states with v 0 = b 1 v_0=b_1 v 0 = b 1
Proof. For a state σ \sigma σ m ≥ 1 m\ge1 m ≥ 1 W m ( σ ) W_m(\sigma) W m ( σ ) m m m σ \sigma σ W 1 ( σ ) W_1(\sigma) W 1 ( σ ) W 1 ( σ ) ≤ λ H ( σ ) W_1(\sigma)\le\lambda H(\sigma) W 1 ( σ ) ≤ λ H ( σ ) m ≥ 2 m\ge2 m ≥ 2
W m ( σ ) = ∑ successors ω ( v 3 v 4 , l 4 ) W m − 1 ( v 1 , v 2 , v 3 , v 4 ; l 2 l 3 l 4 ) ≤ λ m H ( σ ) . W_m(\sigma)=\sum_{\text{successors}}\omega(v_3v_4,l_4)W_{m-1}(v_1,v_2,v_3,v_4;l_2l_3l_4)\le\lambda^m H(\sigma). W m ( σ ) = successors ∑ ω ( v 3 v 4 , l 4 ) W m − 1 ( v 1 , v 2 , v 3 , v 4 ; l 2 l 3 l 4 ) ≤ λ m H ( σ ) . A labelled path b 1 , v 1 , … , v L b_1,v_1,\ldots,v_L b 1 , v 1 , … , v L ( b 1 , v 1 , v 2 , v 3 ; l 1 l 2 l 3 ) (b_1,v_1,v_2,v_3;l_1l_2l_3) ( b 1 , v 1 , v 2 , v 3 ; l 1 l 2 l 3 ) v i + 1 ∉ { v i − 2 , v i − 1 , v i } v_{i+1}\notin\{v_{i-2},v_{i-1},v_i\} v i + 1 ∈ / { v i − 2 , v i − 1 , v i } v i + 1 v_{i+1} v i + 1 L L L ∑ ω ( b 1 v 1 , l 1 ) ω ( v 1 v 2 , l 2 ) ω ( v 2 v 3 , l 3 ) W L − 3 ( b 1 , v 1 , v 2 , v 3 ; l 1 l 2 l 3 ) \sum\omega(b_1v_1,l_1)\omega(v_1v_2,l_2)\omega(v_2v_3,l_3)W_{L-3}(b_1,v_1,v_2,v_3;l_1l_2l_3) ∑ ω ( b 1 v 1 , l 1 ) ω ( v 1 v 2 , l 2 ) ω ( v 2 v 3 , l 3 ) W L − 3 ( b 1 , v 1 , v 2 , v 3 ; l 1 l 2 l 3 )
Classes and locality
The certificate assigns the same potential to states with the same class and the same labels. Here the class of ( v 0 , v 1 , v 2 , v 3 ; l 1 l 2 l 3 ) (v_0,v_1,v_2,v_3;l_1l_2l_3) ( v 0 , v 1 , v 2 , v 3 ; l 1 l 2 l 3 ) v 0 v_0 v 0 b 1 b_1 b 1 v 1 v_1 v 1 v 2 v_2 v 2 v 3 v_3 v 3 v 1 − v 0 v_1-v_0 v 1 − v 0 v 2 − v 1 v_2-v_1 v 2 − v 1 v 3 − v 2 v_3-v_2 v 3 − v 2 λ \lambda λ v v v u − v u-v u − v u u u u u u v v v
Lemma 6.6. The rows of the states ( v 0 , v 1 , v 2 , v 3 ; l 1 l 2 l 3 ) (v_0,v_1,v_2,v_3;l_1l_2l_3) ( v 0 , v 1 , v 2 , v 3 ; l 1 l 2 l 3 ) v 3 v_3 v 3 v 3 v_3 v 3 ω ( b 1 v 1 , l 1 ) ω ( v 1 v 2 , l 2 ) ω ( v 2 v 3 , l 3 ) H ( b 1 , v 1 , v 2 , v 3 ; l 1 l 2 l 3 ) \omega(b_1v_1,l_1)\omega(v_1v_2,l_2)\omega(v_2v_3,l_3)H(b_1,v_1,v_2,v_3;l_1l_2l_3) ω ( b 1 v 1 , l 1 ) ω ( v 1 v 2 , l 2 ) ω ( v 2 v 3 , l 3 ) H ( b 1 , v 1 , v 2 , v 3 ; l 1 l 2 l 3 ) v 1 v_1 v 1 b 1 b_1 b 1 v 1 v_1 v 1 G d , T G_{d,T} G d , T G d ′ , T ′ G_{d',T'} G d ′ , T ′ d ′ ≤ 25 d'\le25 d ′ ≤ 25 T ′ ≤ 13 T'\le13 T ′ ≤ 13
Proof. The vertices of a state ending at v 3 v_3 v 3 v 3 v_3 v 3 v 3 v_3 v 3 v 3 v_3 v 3 v v v v v v v † v^\dagger v † v 2 ∼ v 1 v_2\sim v_1 v 2 ∼ v 1 v 3 ∼ v 2 v_3\sim v_2 v 3 ∼ v 2
A chain of at most four edges between detectors changes each coordinate by at most 16 and the layer by at most 4. By Lemma 2.3(b), the typed ball of v 3 v_3 v 3 ℓ ∞ \ell^\infty ℓ ∞ v 3 v_3 v 3 X X X Z Z Z min ( r , 6 ) \min(r,6) min ( r , 6 ) min ( T − r , 6 ) \min(T-r,6) min ( T − r , 6 ) r r r v 3 v_3 v 3 G 25 G_{25} G 25 T ′ = 13 T'=13 T ′ = 13
Proof of Theorem 1.2
Put λ 0 = 997 / 1000 \lambda_0=997/1000 λ 0 = 997/1000 λ 0 = 999 / 1000 \lambda_0=999/1000 λ 0 = 999/1000 d ≤ 25 d\le25 d ≤ 25 T ≤ 13 T\le13 T ≤ 13 1 Lemma 6.6 these are all the rows of all graphs G d , T G_{d,T} G d , T h h h l 1 l 2 l 3 l_1l_2l_3 l 1 l 2 l 3 H = h / 10 15 H=h/10^{15} H = h /1 0 15 p = p ∗ ∗ p=p_{**} p = p ∗∗ λ = λ 0 \lambda=\lambda_0 λ = λ 0 ω ( e , l ) \omega(e,l) ω ( e , l ) 1 Table 4 ). Let p ≤ p ∗ ∗ p\le p_{**} p ≤ p ∗∗ ρ = ( p / p ∗ ∗ ) s \rho=(p/p_{**})^s ρ = ( p / p ∗∗ ) s ω ( e , l ) ( p ) ≤ ρ ω ( e , l ) ( p ∗ ∗ ) \omega(e,l)(p) \le\rho\omega(e,l)(p_{**}) ω ( e , l ) ( p ) ≤ ρ ω ( e , l ) ( p ∗∗ ) ( p / p ∗ ∗ ) 1 − s ≤ ρ (p/p_{**})^{1-s} \le\rho ( p / p ∗∗ ) 1 − s ≤ ρ ( 1 − q e ) − 1 (1-q_e)^{-1} ( 1 − q e ) − 1 p p p Lemma 6.3 (a), and rule (S) does not depend on p p p p p p λ p = λ 0 ρ \lambda_p=\lambda_0\rho λ p = λ 0 ρ K K K Lemma 6.6 at p ∗ ∗ p_{**} p ∗∗ v 1 v_1 v 1 b 1 † b_1^\dagger b 1 † K 3 K_3 K 3 ω ( b 1 v 1 , l 1 ) ω ( v 1 v 2 , l 2 ) ω ( v 2 b 2 , l 3 ) \omega(b_1v_1,l_1)\omega(v_1v_2,l_2)\omega(v_2b_2,l_3) ω ( b 1 v 1 , l 1 ) ω ( v 1 v 2 , l 2 ) ω ( v 2 b 2 , l 3 ) b 1 , v 1 , v 2 , b 2 b_1,v_1,v_2,b_2 b 1 , v 1 , v 2 , b 2 v 1 v_1 v 1 d = 3 d=3 d = 3 K = 0.031062 … K=0.031062\ldots K = 0.031062 … K 3 = 0.032106 … K_3=0.032106\ldots K 3 = 0.032106 … K = 0.056229 … K=0.056229\ldots K = 0.056229 … K 3 = 0.064013 … K_3=0.064013\ldots K 3 = 0.064013 … Lemma 3.2 we obtain
Table 4. Computer verification for Theorem 1.2 . Rows S1–S5 concern part (a). Lemma 6.6 needs d ≤ 25 d \le25 d ≤ 25 T ≤ 13 T \le13 T ≤ 13
P f a i l ≤ ∣ N ( b 1 ) ∣ ( ρ 3 K 3 [ d = 3 ] + ∑ L ≥ max ( d , 4 ) λ p L − 3 ρ 3 K ) ≤ ρ 3 ∣ N ( b 1 ) ∣ ( K + K 3 ) λ p d − 3 1 − λ p . P_{\mathrm{fail}} \leq\lvert N(b_1)\rvert\left(\rho^3K_3[d=3]+\sum_{L\geq\max(d,4)}\lambda_p^{L-3}\rho^3K\right)\leq\rho^3\lvert N(b_1)\rvert(K+K_3)\frac{\lambda_p^{d-3}}{1-\lambda_p}. P fail ≤ ∣ N ( b 1 )∣ ρ 3 K 3 [ d = 3 ] + L ≥ m a x ( d , 4 ) ∑ λ p L − 3 ρ 3 K ≤ ρ 3 ∣ N ( b 1 )∣ ( K + K 3 ) 1 − λ p λ p d − 3 . Recall that ∣ N ( b 1 ) ∣ = ( T + 1 ) ( d + 1 ) / 2 \lvert N(b_1)\rvert=(T+1)(d+1)/2 ∣ N ( b 1 )∣ = ( T + 1 ) ( d + 1 ) /2 Lemma 2.1 (e). With ρ = λ p / λ 0 \rho=\lambda_p/\lambda_0 ρ = λ p / λ 0 ( K + K 3 ) ( T + 1 ) ( d + 1 ) λ p d / ( 2 λ 0 3 ( 1 − λ p ) ) (K+K_3)(T+1)(d+1)\lambda_p^d/(2\lambda_0^3(1-\lambda_p)) ( K + K 3 ) ( T + 1 ) ( d + 1 ) λ p d / ( 2 λ 0 3 ( 1 − λ p )) ( K + K 3 ) / ( 2 λ 0 3 ) (K+K_3)/(2\lambda_0^3) ( K + K 3 ) / ( 2 λ 0 3 ) 0.032 0.032 0.032 0.061 0.061 0.061
The lean schedule
In the lean schedule all measure qubits and data qubits are prepared in a first step, the Z-type measure qubits in ∣ 0 ⟩ \lvert0\rangle ∣ 0 ⟩ ∣ + ⟩ \lvert+\rangle ∣ + ⟩ § 1.1 and one more step. In it each Z-type measure qubit is measured in the Z basis and reset to ∣ 0 ⟩ \lvert0\rangle ∣ 0 ⟩ ∣ + ⟩ \lvert+\rangle ∣ + ⟩ § 1.2 applies to these locations, the measurement and the reset in this step failing independently, each with probability p p p
§ 2 carries over with the following changes{sup}†. Each fault outcome again flips at most two detectors, and Lemma 2.1 holds with c max = 94 / 15 c_{\max}=94/15 c m a x = 94/15 15 c e 15c_e 15 c e ± ( 0 , 0 , 1 ) \pm(0,0,1) ± ( 0 , 0 , 1 ) ± ( 2 , − 2 , 0 ) \pm(2,-2,0) ± ( 2 , − 2 , 0 ) ± ( 2 , 2 , 0 ) \pm(2,2,0) ± ( 2 , 2 , 0 ) ± ( 2 , 2 , − 1 ) \pm(2,2,-1) ± ( 2 , 2 , − 1 ) ± ( 2 , − 2 , − 1 ) \pm(2,-2,-1) ± ( 2 , − 2 , − 1 ) ± ( 4 , 0 , − 1 ) \pm(4,0,-1) ± ( 4 , 0 , − 1 ) 6.6 , which use only the layout, the CX orders and this structure of the rounds, apply verbatim. All edges again change each coordinate by at most 4 and the layer by at most 1.
Proof of Theorem 1.3. (a) As in § 5 , with λ = 25.55 p \lambda=25.55\sqrt{p} λ = 25.55 p p = 1.53 × 10 − 3 p=1.53\times10^{-3} p = 1.53 × 1 0 − 3 25.55 p ≥ 0.9993 25.55\sqrt{p}\geq0.9993 25.55 p ≥ 0.9993 0.9997 0.9997 0.9997 0.9993 0.9993 0.9993 0.99794 0.99794 0.99794 0.95318 0.95318 0.95318 c max = 94 / 15 c_{\max}=94/15 c m a x = 94/15 § 5 then leads to the prefactor c max / ( 1 − c max p ) / 25.55 ≤ 0.0985 \sqrt{c_{\max}/(1-c_{\max}p)}/25.55\leq0.0985 c m a x / ( 1 − c m a x p ) /25.55 ≤ 0.0985
(b) As in § 6 , with p ∗ ∗ = 3 / 1250 p_{**}=3/1250 p ∗∗ = 3/1250 s = 21 / 50 s=21/50 s = 21/50 c max = 94 / 15 c_{\max}=94/15 c m a x = 94/15 d ≤ 25 d\leq25 d ≤ 25 T ≤ 13 T\leq13 T ≤ 13 d ≤ 15 d\leq15 d ≤ 15 T ≤ 7 T\leq7 T ≤ 7 λ = 997 / 1000 \lambda=997/1000 λ = 997/1000 K = 0.026464 … K=0.026464\ldots K = 0.026464 … K 3 = 0.028384 … K_3=0.028384\ldots K 3 = 0.028384 … ( K + K 3 ) / ( 2 ⋅ 0.997 3 ) ≤ 0.028 s u p † (K+K_3)/(2\cdot0.997^3)\leq0.028{sup}\dagger ( K + K 3 ) / ( 2 ⋅ 0.99 7 3 ) ≤ 0.028 s u p †
(c) As in part (b) of Theorem 1.2 , with p ∗ ∗ = 3 / 1000 p_{**}=3/1000 p ∗∗ = 3/1000 s = 9 / 25 s=9/25 s = 9/25 λ 0 = 997 / 1000 \lambda_0=997/1000 λ 0 = 997/1000 c max = 94 / 15 c_{\max}=94/15 c m a x = 94/15 d ≤ 25 d\leq25 d ≤ 25 T ≤ 13 T\leq13 T ≤ 13 λ = 997 / 1000 \lambda=997/1000 λ = 997/1000 K = 0.045261 … K=0.045261\ldots K = 0.045261 … K 3 = 0.057416 … K_3=0.057416\ldots K 3 = 0.057416 … ( K + K 3 ) / ( 2 ⋅ 0.997 3 ) ≤ 0.052 s u p † (K+K_3)/(2\cdot0.997^3)\leq0.052{sup}\dagger ( K + K 3 ) / ( 2 ⋅ 0.99 7 3 ) ≤ 0.052 s u p †
Non-uniform error rates
In a real device the gates, measurements and idle steps fail at different rates. To model this, we sort the locations of the circuit of Section 1.1 into seven categories: resets and preparations; measurements; H H H θ \theta θ θ k \theta_k θ k k k k
q e ( θ ) = ∑ k c e , k θ k , q_e(\theta)=\sum_k c_{e,k}\theta_k, q e ( θ ) = k ∑ c e , k θ k , where c e , k c_{e,k} c e , k π ( f ) \pi(f) π ( f ) f f f e ( f ) = e e(f)=e e ( f ) = e k k k ∑ k c e , k = c e \sum_k c_{e,k}=c_e ∑ k c e , k = c e θ \theta θ q e ( θ ) q_e(\theta) q e ( θ ) c e p c_ep c e p c e , k c_{e,k} c e , k 1
Theorem 8.1. Let θ \theta θ max e q e ( θ ) < 1 / 2 \max_e q_e(\theta)<1/2 max e q e ( θ ) < 1/2 t θ t\theta tθ 0 < t ≤ 1 0<t\leq1 0 < t ≤ 1
(a) Suppose that ∑ e ∋ v a e / ( λ + a e ) ≤ 1 \sum_{e\ni v}a_e/(\lambda+a_e)\leq1 ∑ e ∋ v a e / ( λ + a e ) ≤ 1 v v v a e = 2 q e ( θ ) / ( 1 − q e ( θ ) ) a_e=2\sqrt{q_e(\theta)}/(1-q_e(\theta)) a e = 2 q e ( θ ) / ( 1 − q e ( θ )) λ < 1 \lambda<1 λ < 1
P f a i l ≤ ( T + 1 ) ( d + 1 ) 2 ⋅ a max λ ⋅ ( λ t ) d 1 − λ t . P_{\mathrm{fail}}\leq\frac{(T+1)(d+1)}{2}\cdot\frac{a_{\max}}{\lambda}\cdot\frac{(\lambda\sqrt{t})^d}{1-\lambda\sqrt{t}}. P fail ≤ 2 ( T + 1 ) ( d + 1 ) ⋅ λ a m a x ⋅ 1 − λ t ( λ t ) d . where a max a_{\max} a m a x a e a_e a e b 1 b_1 b 1 b 2 b_2 b 2
(b) Let q ( P ) = ∏ e ∈ P q e ( θ ) q(P)=\prod_{e\in P}q_e(\theta) q ( P ) = ∏ e ∈ P q e ( θ ) q max = max e q e ( θ ) q_{\max}=\max_e q_e(\theta) q m a x = max e q e ( θ )
q ( σ E ) q ( P ′ ) q ( σ C ) > ∏ e ∈ σ 1 1 − q e ( θ ) ⋅ ( 1 1 − q max ) h ′ (7) \frac{q(\sigma_E)q(P')}{q(\sigma_C)}
>
\prod_{e\in\sigma}
\frac{1}{1-q_e(\theta)}
\cdot
\left(\frac{1}{1-q_{\max}}\right)^{h'} \tag*{(7)} q ( σ C ) q ( σ E ) q ( P ′ ) > e ∈ σ ∏ 1 − q e ( θ ) 1 ⋅ ( 1 − q m a x 1 ) h ′ (7) and (6.2) by
q ( P ′ ) q ( σ C ) > ∏ e ∈ σ C 1 1 − q e ( θ ) ⋅ ( 1 1 − q max ) h ′ (8) \frac{q(P')}{q(\sigma_C)}
>
\prod_{e\in\sigma_C}
\frac{1}{1-q_e(\theta)}
\cdot
\left(\frac{1}{1-q_{\max}}\right)^{h'} \tag*{(8)} q ( σ C ) q ( P ′ ) > e ∈ σ C ∏ 1 − q e ( θ ) 1 ⋅ ( 1 − q m a x 1 ) h ′ (8) keeping the conditions k ≥ 0 k\geq0 k ≥ 0 ω ( e , l ) \omega(e,l) ω ( e , l ) q e ( θ ) q_e(\theta) q e ( θ ) 0 < s ≤ 1 / 2 0<s\leq1/2 0 < s ≤ 1/2 λ < 1 \lambda<1 λ < 1 K K K K 3 K_3 K 3
P f a i l ≤ ( T + 1 ) ( d + 1 ) 2 ⋅ K + K 3 λ 3 ⋅ ( λ t s ) d 1 − λ t s . P_{\mathrm{fail}}\leq\frac{(T+1)(d+1)}{2}\cdot\frac{K+K_3}{\lambda^3}\cdot\frac{(\lambda t s)^d}{1-\lambda t s}. P fail ≤ 2 ( T + 1 ) ( d + 1 ) ⋅ λ 3 K + K 3 ⋅ 1 − λ t s ( λ t s ) d . (c) For a location ℓ \ell ℓ k k k c ℓ , e ( θ ) c_{\ell,e}(\theta) c ℓ , e ( θ ) θ k π ( f ) \theta_k\pi(f) θ k π ( f ) f f f ℓ \ell ℓ e ( f ) = e e(f)=e e ( f ) = e c ℓ , e ( θ ) c_{\ell,e}(\theta) c ℓ , e ( θ ) e e e θ \theta θ r e r_e r e t t t λ < 1 \lambda<1 λ < 1
Proof. (a) For the rates t θ t\theta tθ a e a_e a e t a e \sqrt{t}a_e t a e 1 − t q e ( θ ) ≥ 1 − q e ( θ ) 1-tq_e(\theta)\geq1-q_e(\theta) 1 − t q e ( θ ) ≥ 1 − q e ( θ ) x / ( λ t + x ) x/(\lambda\sqrt{t}+x) x / ( λ t + x ) x x x λ t \lambda\sqrt{t} λ t λ \lambda λ t a max \sqrt{t}a_{\max} t a m a x a max a_{\max} a m a x
(b) Lemma 6.3(a) holds for the rates t θ t\theta tθ k ln ( 1 / t ) + ln ( q ( σ E ) q ( P ′ ) / q ( σ C ) ) k\ln(1/t)+\ln(q(\sigma_E)q(P')/q(\sigma_C)) k ln ( 1/ t ) + ln ( q ( σ E ) q ( P ′ ) / q ( σ C )) k ln ( 1 / t ) + ln ( q ( P ′ ) / q ( σ C ) ) k\ln(1/t)+\ln(q(P')/q(\sigma_C)) k ln ( 1/ t ) + ln ( q ( P ′ ) / q ( σ C )) k ≥ 0 k\geq0 k ≥ 0 ω ( e , l ) ( t θ ) ≤ t s ω ( e , l ) ( θ ) \omega(e,l)(t\theta) \le t^{s}\omega(e,l)(\theta) ω ( e , l ) ( tθ ) ≤ t s ω ( e , l ) ( θ ) t 1 − s ≤ t s t^{1-s} \le t^{s} t 1 − s ≤ t s s ≤ 1 / 2 s \le1/2 s ≤ 1/2 t θ t\theta tθ λ t s \lambda t^{s} λ t s λ \lambda λ t 3 s t^{3s} t 3 s θ \theta θ ρ = t s \rho= t^{s} ρ = t s
(c) The profiles at t θ t\theta tθ t t t θ \theta θ t t t C ∗ C^* C ∗
Table 2 lists error models built from published component error rates of six devices, mapped onto the seven categories. Errors reported as average infidelities r r r 3 r / 2 3r/2 3 r /2 5 r / 4 5r/4 5 r /4 s = 43 / 100 s = 43/100 s = 43/100
Quantinuum Helios:
P f a i l ≤ 0.033 ( T + 1 ) ( d + 1 ) λ d 1 − λ , λ = 0.75 t 43 / 100 P_{\mathrm{fail}} \le0.033\,(T+1)(d+1)\frac{\lambda^{d}}{1-\lambda},\qquad\lambda= 0.75t^{43/100} P fail ≤ 0.033 ( T + 1 ) ( d + 1 ) 1 − λ λ d , λ = 0.75 t 43/100 Quantinuum H2:
P f a i l ≤ 0.022 ( T + 1 ) ( d + 1 ) λ d 1 − λ , λ = 0.715 t 43 / 100 P_{\mathrm{fail}} \le0.022\,(T+1)(d+1)\frac{\lambda^{d}}{1-\lambda},\qquad\lambda= 0.715t^{43/100} P fail ≤ 0.022 ( T + 1 ) ( d + 1 ) 1 − λ λ d , λ = 0.715 t 43/100 IBM Heron r3, square grid:
P f a i l ≤ 0.023 ( T + 1 ) ( d + 1 ) λ d 1 − λ , λ = 0.97 t 43 / 100 P_{\mathrm{fail}} \le0.023\,(T+1)(d+1)\frac{\lambda^{d}}{1-\lambda},\qquad\lambda= 0.97t^{43/100} P fail ≤ 0.023 ( T + 1 ) ( d + 1 ) 1 − λ λ d , λ = 0.97 t 43/100 for their rates scaled by any t ≤ 1 t \le1 t ≤ 1 s = 19 / 50 s = 19/50 s = 19/50
Quantinuum Helios:
P f a i l ≤ 0.058 ( T + 1 ) ( d + 1 ) λ d 1 − λ , λ = 0.675 t 19 / 50 P_{\mathrm{fail}} \le0.058\,(T+1)(d+1)\frac{\lambda^{d}}{1-\lambda},\qquad\lambda= 0.675t^{19/50} P fail ≤ 0.058 ( T + 1 ) ( d + 1 ) 1 − λ λ d , λ = 0.675 t 19/50 Quantinuum H2:
P f a i l ≤ 0.039 ( T + 1 ) ( d + 1 ) λ d 1 − λ , λ = 0.643 t 19 / 50 P_{\mathrm{fail}} \le0.039\,(T+1)(d+1)\frac{\lambda^{d}}{1-\lambda},\qquad\lambda= 0.643t^{19/50} P fail ≤ 0.039 ( T + 1 ) ( d + 1 ) 1 − λ λ d , λ = 0.643 t 19/50 IBM Heron r3, square grid:
P f a i l ≤ 0.039 ( T + 1 ) ( d + 1 ) λ d 1 − λ , λ = 0.873 t 19 / 50 P_{\mathrm{fail}} \le0.039\,(T+1)(d+1)\frac{\lambda^{d}}{1-\lambda},\qquad\lambda= 0.873t^{19/50} P fail ≤ 0.039 ( T + 1 ) ( d + 1 ) 1 − λ λ d , λ = 0.873 t 19/50 Part (a) also certifies Helios and H2, but it fails at λ = 1 \lambda= 1 λ = 1
Computer verification
Table 3 lists the computations behind the statements marked{sup}†. We compute the fault table by forward propagation of Pauli frames, independently of Stim’s detector-error-model code, and keep each Pauli outcome of each location with its exact probability. Over the full range there are 1,924,076 outcomes. The circuit file also declares the detectors of the other type, but the decoding graph of each sector ignores them. All comparisons in V6 use exact rational arithmetic. One run of the accompanying script performs all checks in the table and passes only if all of them hold.
Table 4 lists the checks behind Theorem 1.2. Two further scripts, one for each part, regenerate the rows of all instances with d ≤ 25 d \le25 d ≤ 25 T ≤ 13 T \le13 T ≤ 13 h h h d ≤ 9 d \le9 d ≤ 9 T ≤ 5 T \le5 T ≤ 5 § 8 . Classes are named by 64-bit hashes of the types and offsets they record. A collision would merge two classes, but this can only make the system of rows harder to satisfy. Three further steps are not used in the proof: the iteration on the system of rows that found the potentials, and two tests of the exclusions. For the first test, let w e + = ln q e − ln ( 1 − q e ) w_e^{+} = \ln q_e - \ln(1-q_e) w e + = ln q e − ln ( 1 − q e ) w e − = − ln q e + ln ( 1 − q e ) w_e^{-} = -\ln q_e + \ln(1-q_e) w e − = − ln q e + ln ( 1 − q e ) p ∗ ∗ p_{**} p ∗∗ G / B G/B G / B w + w^{+} w + σ \sigma σ w − ( σ C ) − w + ( σ E ) w^{-}(\sigma_C) - w^{+}(\sigma_E) w − ( σ C ) − w + ( σ E ) σ C \sigma_C σ C w − ( σ C ) w^{-}(\sigma_C) w − ( σ C ) d ≤ 9 d \le9 d ≤ 9 T ≤ 5 T \le5 T ≤ 5 p ∗ ∗ = 1 / 625 p_{**} = 1/625 p ∗∗ = 1/625 p ∗ ∗ = 1 / 500 p_{**} = 1/500 p ∗∗ = 1/500 d ≤ 9 d \le9 d ≤ 9 T ≤ 5 T \le5 T ≤ 5
The checks behind Theorem 1.3 (Table 5 ) are those of Table 3 and Table 4 , run on the lean schedule with its own certificates. The Dijkstra test of the exclusions finds no failure among the 23.6 million excluded windows of the 40 instances with d ≤ 9 d \le9 d ≤ 9 T ≤ 5 T \le5 T ≤ 5 p ∗ ∗ = 3 / 1250 p_{**} = 3/1250 p ∗∗ = 3/1250 p ∗ ∗ = 3 / 1000 p_{**} = 3/1000 p ∗∗ = 3/1000
Table 5. Computer verification for Theorem 1.3.
For § 8 , a further script runs the checks H1–H4 of Table 6 on the error models of Table 2 . For H4 it runs the script of rows S1–S5 with the edge probabilities q e ( θ ) q_e(\theta) q e ( θ ) Table 4 for ( d , T ) = ( 5 , 3 ) (d,T) = (5,3) ( d , T ) = ( 5 , 3 ) ( 7 , 4 ) (7,4) ( 7 , 4 ) ( 9 , 5 ) (9,5) ( 9 , 5 )
Table 2. Error models (Pauli error probabilities per location) and the rates λ \lambda λ Theorem 8.1 at t = 1 t = 1 t = 1 s = 43 / 100 s = 43/100 s = 43/100 s = 19 / 50 s = 19/50 s = 19/50 d ≤ 15 d \le15 d ≤ 15 T ≤ 7 T \le7 T ≤ 7 s ∈ { 0.40 , 0.43 , 0.45 } s \in\{0.40, 0.43, 0.45\} s ∈ { 0.40 , 0.43 , 0.45 } s s s [11 Table S4] , with the CZ crosstalk and leakage rows added to the CX rate, and the leakage-heating row added to the data-idle error during measurement and reset, which is split over steps (S1) and (S8). Willow: mean simultaneous randomized-benchmarking errors of the spec sheet. Zuchongzhi 3.2: cross-entropy-benchmarking errors of the 97-qubit region, used as reported. Assumptions: the rates in the column “idle” for the IBM, Google and USTC models (for the Google models estimated from coherence times); the reset rates and the (S1) and (S8) idle rates of the IBM and USTC models; for Willow, the reset and data-idle rates of the 72-qubit budget; and for both Google models, the split of the data-idle error over (S1) and (S8).
Formal verification in Lean 4
We prove the theorems of this paper in the proof assistant Lean 4 (version 4.35.0-rc3), using the Mathlib library (commit c55e6e78). A proof assistant checks every step of a proof against a small set of logical rules; the part of Lean that performs this check is its kernel . The formal development defines the circuit, the noise, the memory experiment and the decoder of § 1 , and derives the bounds of the theorems from these definitions. It contains about 25,100 lines written by hand, together with generated data files (node types, certificates) and generated check files. Each theorem is proved in two versions: in the kernel version every computation is checked by the kernel, and in the native version the large computations are evaluated outside the kernel, which takes far less time. In this section we state what is proved, what has to be trusted, and how to reproduce the verification.
What is modelled
The circuit and the experiment. The layout of the rotated surface code, the eight steps of a round, the noise locations with their outcomes and the probabilities p π ( f ) p\mathop{\pi}(f) p π ( f ) § 1.1 and § 1.2 . We define the effect of the faults by Pauli-frame propagation: a CX gate copies an X component from its control to its target and a Z component from its target to its control, an H gate exchanges the two components, and a reset clears both. For any set of faults, at most one outcome per location, this determines the recorded measurement outcomes, the detectors D m , r D_{m,r} D m , r § 1.1 and the flip of the logical outcome. The formal development proves that these are the parities of the single-fault values, so they agree with the signatures σ ( f ) \sigma(f) σ ( f ) ℓ ( f ) \ell(f) ℓ ( f ) § 1.3 .
The decoder and the failure probability. Here the decoding graph and the weights are those of § 1.3 , for any numbers r e r_e r e q e ( 1 − q e ) ≤ r e ≤ q e q_e(1-q_e) \le r_e \le q_e q e ( 1 − q e ) ≤ r e ≤ q e P f a i l P_{\mathrm{fail}} P fail C C C ∂ C \partial C ∂ C
Profile weights. The profile of an edge and profile weights are those of § 1.3 : for a location ℓ \ell ℓ c ℓ , e c_{\ell,e} c ℓ , e π ( f ) \pi(f) π ( f ) f f f ℓ \ell ℓ e ( f ) = e e(f)=e e ( f ) = e e e e c ℓ , e c_{\ell,e} c ℓ , e ℓ \ell ℓ r e r_e r e p p p e e e § 1.3 are profile weights. The theorems that use rule (S) are stated for profile weights.
The lean schedule. We model the lean schedule of § 7 by its own Pauli-frame semantics: a preparation step, then per round four CX steps and a fused measure-and-reset step, in which the X-type measure qubits are measured in the X basis. Its noise locations are those of § 7 , including the reset failures after the last measurement. The development proves that every lean location changes the measurement outcomes and the final data values exactly as the corresponding location of the eight-step circuit restricted to the lean locations, and that the reset failures after the last measurement change nothing. Hence the lean experiment has the failure probability of the restricted eight-step circuit, and the formal theorems are about the lean schedule itself.
Non-uniform rates. A rate vector θ \theta θ § 8 the failure probability θ k \theta_k θ k 0 < t ≤ 1 0 < t \le1 0 < t ≤ 1
What is proved
Table 7 lists the formal theorems. Each holds for all odd d ≥ 3 d \ge3 d ≥ 3 T ≥ 1 T \ge1 T ≥ 1 Theorems 1.1 , 1.2 , 1.3 and 8.1 , written for the failure probability defined above.
Table 7. The formal theorems, and for each of their two versions the number of axioms it depends on besides the three standard ones. “Kernel”: every computation is checked by Lean’s kernel. “Native”: the large computation is evaluated outside the kernel, by compiled code or by Lean’s interpreter; each such evaluation enters the proof as one axiom (see the text). The standard axioms are propositional extensionality, the axiom of choice and quotient soundness.
What has to be trusted
A Lean proof can rely on axioms, which the kernel accepts without proof. Lean reports, for every theorem, the axioms it depends on. Every theorem of Table 7 depends on three standard axioms of Lean’s foundations (propositional extensionality, the axiom of choice and the soundness of quotients). The kernel versions depend on nothing else.
The native versions also depend on axioms of a second kind, one for each large computation. For such a computation Lean evaluates the Boolean test outside the kernel, with compiled code or with its interpreter, and records the outcome “true” as an axiom naming the test. Trusting these axioms means trusting, in addition to the kernel, Lean’s compiler, interpreter and runtime, the C compiler that builds the precompiled modules, and the assumption that the loaded libraries were built from the checked sources. The kernel itself already relies on the GMP library for arithmetic on large natural numbers. The computations are: the checks of Theorem 1.1 at representative detectors, which by Lemma 2.3(c) lie in instances with d ≤ 9 d \le9 d ≤ 9 T ≤ 5 T \le5 T ≤ 5 Theorem 1.1 .
In the kernel versions the kernel checks the same facts, in reformulated forms whose soundness is proved, split into generated files that are checked one per process: the rows and start sums at the 13,658 heads for each of the ten certificates (3,330 files), the coverage of the typed balls for the five models (107 files), the type tables (550 files), and the factor bounds and the search trees that hold the typed balls and the potentials. As in the native versions, the exclusion witnesses come from an untrusted search and are checked exactly. A further file compares the statement of each kernel theorem of Theorems 1.2 to 8.1 with the statement of its native version, and the two are identical; the two versions of Theorem 1.1 are stated by the same source text.
The certificates are read from the files of the supplement; the formal data files record the SHA-256 hash of each certificate file. Programs outside Lean generate the node types, the tables, the heads and the other auxiliary data from which the checks start. Because every item they produce is checked inside Lean, an error in them can only make a check fail. The search for exclusion witnesses is likewise untrusted: the rows accept a window as excluded only after the witness found by the search passes an exact check whose soundness is proved.
Two cross-checks support the model without being part of the proof. The node types computed in Lean coincide, as strings including all coefficients, with the node types of the accompanying programs for all five models (the eight-step circuit, the lean schedule built by those programs from its own circuit description through Stim, and the three non-uniform models). All five models have the same 13,658 typed balls on the range of Lemma 6.6 .
Cost
Table 8 lists the measured cost of the checks. Each check runs as a separate Lean process.
Table 8. Cost of the formal checks: number of files, sum over the files of the time per process, and the largest memory of one process. The remaining files, which combine the checks and state the theorems of the native versions and of Theorem 1.1, take about one minute in total and up to 4.0 GiB, and the comparison of the statements takes 5 s and 16.2 GiB.
Reproduction
The formal development is part of the supplement, with a README that lists the commands. First, the definitions and proofs build with Lean’s build tool. Then the scripts below compile the check files, each in its own Lean process and, except for Theorem 1.1, with the precompiled computational modules (QECComp) loaded. Finally the files that combine the checks and state the theorems are compiled, and each prints the axioms of its theorems:
lake build QEC QECComp
scripts/run_checks.sh # Theorem 1.1, kernel
scripts/run_final.sh # Theorem 1.1, native
scripts/run_checks8.sh # Theorem 1.2(a)
for X in L He Hl H2; do # Theorems 1.3(b), 8.1(b)
scripts/run_checksW.sh $X
done
scripts/run_finalW.sh # parts (a), theorem files
for X in S8 SL SHe SHl SH2; do # 1.2(b), 1.3(c), 8.1(c)
scripts/run_checksS.sh $X
done
scripts/run_finalS.sh # profile tables, theorem filesAfter these commands, one script builds the kernel versions of Theorems 1.2 to 8.1 in stages, one file per process; the README lists the stages and the numbers of parallel jobs. A final file, gen/kernel/StmtV3.lean, compares their statements with those of the native versions and prints their axioms.
Table 9 maps the parts of this paper to the files of the development.
Table 9. Where the parts of the paper are formalized.
Remarks
the heavier boundary edges are taken into account. Two changes account for the improvement to 1.04 × 10 − 3 1.04 \times10^{-3} 1.04 × 1 0 − 3 2 q e 2\sqrt{q_e} 2 q e 2 q max 2\sqrt{q_{\max}} 2 q m a x Lemma 4.1 replaces the factor 11 by an exact count of the twelve unequal edges at each node. At the bulk node with λ = 1 \lambda= 1 λ = 1 p = 1.0419 × 10 − 3 p = 1.0419 \times10^{-3} p = 1.0419 × 1 0 − 3 p = 1.0420 × 10 − 3 p = 1.0420 \times10^{-3} p = 1.0420 × 1 0 − 3 1.042 × 10 − 3 1.042 \times10^{-3} 1.042 × 1 0 − 3 p → 0 p \to0 p → 0 Σ = 1 \Sigma= 1 Σ = 1 λ = Λ p \lambda= \Lambda\sqrt{p} λ = Λ p Λ = 30.929 \Lambda= 30.929 Λ = 30.929 ∑ e 2 c e / ( Λ + 2 c e ) = 1 \sum_e 2\sqrt{c_e}/(\Lambda+ 2\sqrt{c_e}) = 1 ∑ e 2 c e / ( Λ + 2 c e ) = 1 8.7 × 10 − 4 8.7 \times10^{-4} 8.7 × 1 0 − 4
Remark 11.2 (Limits of the certificate). Consider the rows of § 6 computed from the instances with d ≤ 15 d \le15 d ≤ 15 T ≤ 7 T \le7 T ≤ 7 p p p p = 1.6 × 10 − 3 p = 1.6 \times10^{-3} p = 1.6 × 1 0 − 3 s = 0.42 s = 0.42 s = 0.42 p = 2 × 10 − 3 p = 2 \times10^{-3} p = 2 × 1 0 − 3 s = 0.36 s = 0.36 s = 0.36 s s s p = 1.62 × 10 − 3 p = 1.62 \times10^{-3} p = 1.62 × 1 0 − 3 p = 2.05 × 10 − 3 p = 2.05 \times10^{-3} p = 2.05 × 1 0 − 3 2.47 × 10 − 3 2.47 \times10^{-3} 2.47 × 1 0 − 3 3.05 × 10 − 3 3.05 \times10^{-3} 3.05 × 1 0 − 3 s s s [18 ] . Since the full range of d d d T T T 1.6185 × 10 − 3 1.6185 \times10^{-3} 1.6185 × 1 0 − 3 1.6936 × 10 − 3 1.6936 \times10^{-3} 1.6936 × 1 0 − 3 Φ \Phi Φ p p p
Remark 11.3 (Limits of arguments by increasing events). Call a set of outcomes failing if, when exactly these outcomes occur, some minimizer makes the decoder fail. An event is increasing if it is preserved when outcomes are added. All bounds in this paper bound P f a i l P_{\mathrm{fail}} P fail U U U U U U U U U X X X ∂ X \partial X ∂ X γ \gamma γ Lemma 3.1 , then γ \ C \gamma\mathbin{\backslash} C γ \ C γ \ E \gamma\mathbin{\backslash} E γ \ E U U U γ \gamma γ b 1 b_1 b 1 b 2 b_2 b 2 E ′ E' E ′ γ \ E ′ \gamma\mathbin{\backslash} E' γ \ E ′ ∂ E ′ \partial E' ∂ E ′
We estimated Pr ( U ) \Pr(U) Pr ( U ) T = d T = d T = d U U U U U U d ≤ 9 d \le9 d ≤ 9 p ≤ 4.25 × 10 − 3 p \le4.25 \times10^{-3} p ≤ 4.25 × 1 0 − 3 d = 11 d = 11 d = 11 p = 4 × 10 − 3 p = 4 \times10^{-3} p = 4 × 1 0 − 3 § 1.1 and d = 5 , 7 , 9 , 11 d = 5,7,9,11 d = 5 , 7 , 9 , 11 Pr ( U ) \Pr(U) Pr ( U ) d d d p = 3.5 × 10 − 3 p = 3.5 \times10^{-3} p = 3.5 × 1 0 − 3 d d d p = 5 × 10 − 3 p = 5 \times10^{-3} p = 5 × 1 0 − 3 p = 4 × 10 − 3 p = 4 \times10^{-3} p = 4 × 1 0 − 3 p = 4.25 × 10 − 3 p = 4.25 \times10^{-3} p = 4.25 × 1 0 − 3 d = 7 d = 7 d = 7 d = 11 d = 11 d = 11 d d d 6 × 10 − 3 6 \times10^{-3} 6 × 1 0 − 3 d = 5 d = 5 d = 5 d = 7 d = 7 d = 7 7 × 10 − 3 7 \times10^{-3} 7 × 1 0 − 3 U U U 3.5 × 10 − 3 3.5 \times10^{-3} 3.5 × 1 0 − 3 5 × 10 − 3 5 \times10^{-3} 5 × 1 0 − 3 4 × 10 − 3 4 \times10^{-3} 4 × 1 0 − 3 Pr ( U ) \Pr(U) Pr ( U )
d = 3 , 5 , 7 d = 3, 5, 7 d = 3 , 5 , 7 d = 7 d = 7 d = 7 [11 ] , and the model reproduces them at t ≈ 1.1 t \approx1.1 t ≈ 1.1 U U U
Code and data
The programs, the certificates, the formal proofs and the outputs of all checks in Table 3 –Table 6 are archived at https://doi.org/10.5281/zenodo.23498518.
Generative AI tools were used to find and prove the results, to write the programs and the formal proofs, and to draft the text.
Node types
Each line gives one type: an example detector ( x , y , r ) (x, y, r) ( x , y , r ) G 9 , 5 G_{9,5} G 9 , 5 G 9 , 5 G_{9,5} G 9 , 5 15 c e 15c_{\mathrm{e}} 15 c e ♭ \flat ♭ b 1 b_1 b 1 ♯ \sharp ♯ b 2 b_2 b 2 (3) , that is Σ \Sigma Σ p = p ∗ p = p_* p = p ∗ λ = 0.9997 \lambda= 0.9997 λ = 0.9997
Table 10. Node types in basis Z Z Z
Table 11. Node types in basis X X X
References
ORCID: https://orcid.org/0000-0003-4668-3639
