Recursive error suppression $e_k \le (cp)^{2^k}/c$

Proved

ThresholdTheorem.concatenated_error_recursion

by Lucas · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

fault-tolerancequantum-computingquantum-error-correction

Recursive error suppression. Let $c>0$ and let $(e_k)_{k\ge0}$ be non-negative reals with $e_0\le p$ and

e_{k+1}\;\le\;c\,e_k^{2}\qquad(k\ge 0).

Then for every $k$ ,

e_k\;\le\;\frac{(c\,p)^{2^k}}{c}.

Here $e_k$ plays the role of the failure probability of a level- $k$ encoded gate. When $p<1/c$ the bound decreases doubly exponentially in the number of levels, which is the source of the threshold $p_{\mathrm{th}}=1/c$ .

Preamble

import Mathlib
import Definitions.Def_threshold_theorem_noise_model

open ThresholdTheorem

Formal statement

namespace ThresholdTheorem
theorem concatenated_error_recursion (c p : ℝ) (hc : 0 < c) (e : ℕ → ℝ)
    (he0 : e 0 ≤ p) (hnn : ∀ k, 0 ≤ e k) (hrec : ∀ k, e (k + 1) ≤ c * e k ^ 2) (k : ℕ) :
    e k ≤ (c * p) ^ (2 ^ k) / c := by sorry
end ThresholdTheorem

Source

Wikipedia, "Threshold theorem" (revision oldid=1360742213, https://en.wikipedia.org/w/index.php?title=Threshold_theorem&oldid=1360742213), section "Explanation"; the boxed statement is quoted there from M. A. Nielsen and I. L. Chuang, Quantum Computation and Quantum Information, 10th anniversary ed., Cambridge University Press, p. 481.

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Recursive error suppression ek≤(cp)2k/ce_k \le (cp)^{2^k}/cek​≤(cp)2k/c

Recursive error suppression $e_k \le (cp)^{2^k}/c$