The circuit-level threshold: many locations, one union bound, and the level count

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate). BACKLOG #62, its probabilistic half.

Glossary: https://glossary.constraintsurfacedynamics.com/threshold-theorem/ Plain-language, CSD-role and formal statements of the threshold theorem, with this module as the Lean anchor. Kept symmetric by scripts/check-glossary.sh.

CodeCapacityThreshold.lean bounds the failure of one encoded block. A computation is a circuit of many locations, each replaced by a gadget, and it fails when any of them fails. This module is that step: the fault patterns of a circuit of N locations whose level-k gadgets have L fault locations each, the union bound over the circuit, and the count of levels an accuracy demands.

• Fintype (ConcatPat n k) and ★ card_concatPat — the level-k gadget has n ^ k fault locations: its pattern space has 2 ^ (n ^ k) elements. This is the overhead of the recursive simulation, in the only form this file needs;
• circuitMeasure N L ν k — independent faults at every location of every gadget: the product over the N circuit locations of concatMeasure L ν k;
• circuitBad N L k — the circuit fails when some location's level-k gadget is bad;
• ★★ circuitMeasure_circuitBad_le — the circuit-level bound ℙ[circuit fails] ≤ N · (c p)^{2^k} / c with c = C(L, 2): the union bound over the locations on top of the code-capacity recursion;
• ★ exists_level_mul_lt and ★★★ exists_level_circuitMeasure_lt — the threshold at circuit level: below p < 1/c, for every circuit size N and every accuracy ε there is a level k at which the whole circuit fails with probability less than ε;
• ★ mul_codeCapacityBound_lt_of_log_div_lt — the quantitative form: any k with 2^k > log(c ε / N) / log(c p) will do. The right-hand side is a single logarithm, so the level needed grows like log log (N/ε);
• ★★ exists_level_two_pow_le and ★★★ exists_level_overhead_le — the overhead is polylogarithmic: the level k = ⌈log₂ X⌉ + 1 (X the logarithm ratio above, floored at 1) both meets the accuracy and keeps 2^k ≤ 4X, so the gadget's L^k fault locations are at most (4X)^{log₂ L} — a fixed power of a logarithm of N/ε. pow_eq_rpow_logb is the identity L^k = (2^k)^{log₂ L} that turns the doubling parameter into the overhead.

Honest scope

⚠️ This is the accounting, not the fault tolerance. What makes a gadget "bad" is an input to this file, exactly as in CodeCapacityThreshold.lean: the consumer must prove that a gadget with at most one fault does the right thing. For faulty gates on the Steane code that consumer is Empirical/QM/QEC/SteaneFaultyGate.lean, at level one and with an ideal recovery. Faults inside the recovery gadget itself — hence extended rectangles, and with them the Aharonov–Ben-Or simulation theorem — are not here; specs/BACKLOG.md #62 records what is left.

⚠️ The locations of a circuit are indexed by Fin N and nothing here says what they do: there is no circuit datatype, no gate set, no time ordering. The union bound needs none of that, and claiming more would be claiming the simulation theorem.

References: D. Aharonov, M. Ben-Or, Fault-tolerant quantum computation with constant error rate, SIAM J. Comput. 38 (2008), §2; P. Aliferis, D. Gottesman, J. Preskill, Quantum accuracy threshold for concatenated distance-3 codes, Quantum Inf. Comput. 6 (2006); specs/BACKLOG.md #62; specs/steane-plan.md; specs/future-work.md.

@[instance_reducible]

instance instFintypeConcatPat (n k : ℕ) : Fintype (ConcatPat n k)

The pattern space of a level-k gadget is finite.

Equations

• instFintypeConcatPat n 0 = { elems := instFintypeConcatPat._aux_1 n, complete := ⋯ }
• instFintypeConcatPat n k.succ = { elems := instFintypeConcatPat._aux_4 n k (instFintypeConcatPat n k), complete := ⋯ }

theorem card_concatPat (n k : ℕ) : Fintype.card (ConcatPat n k) = 2 ^ n ^ k

★ The level-k gadget has n ^ k fault locations: its pattern space has 2 ^ (n ^ k) elements, each location being faulty or not. This is the overhead of the recursive simulation.

noncomputable def circuitMeasure (N L : ℕ) (ν : MeasureTheory.Measure Bool) [MeasureTheory.IsProbabilityMeasure ν] (k : ℕ) : MeasureTheory.Measure (Fin N → ConcatPat L k)

Independent faults at every location of every gadget: the product over the N locations of a circuit of the level-k gadget noise.

Equations

• circuitMeasure N L ν k = MeasureTheory.Measure.pi fun (x : Fin N) => ↑(concatMeasure L ν k)

def circuitBad (N L k : ℕ) : Set (Fin N → ConcatPat L k)

The circuit fails when some location's gadget is bad.

Equations

• circuitBad N L k = {X : Fin N → ConcatPat L k | ∃ (j : Fin N), isBad L k (X j) = true}

theorem circuitBad_eq_iUnion (N L k : ℕ) : circuitBad N L k = ⋃ (j : Fin N), {X : Fin N → ConcatPat L k | isBad L k (X j) = true}

theorem circuitMeasure_coord (N L : ℕ) (ν : MeasureTheory.Measure Bool) [MeasureTheory.IsProbabilityMeasure ν] (k : ℕ) (j : Fin N) : (circuitMeasure N L ν k) {X : Fin N → ConcatPat L k | isBad L k (X j) = true} = ↑(concatMeasure L ν k) (concatBad L k)

One location's failure has the level-k gadget's probability: a cylinder in one coordinate of a product of probability measures.

theorem circuitMeasure_circuitBad_le (N L : ℕ) (ν : MeasureTheory.Measure Bool) [MeasureTheory.IsProbabilityMeasure ν] {p : ℝ} (hp : 0 ≤ p) (hν : ν {b : Bool | b = true} ≤ ENNReal.ofReal p) (k : ℕ) : (circuitMeasure N L ν k) (circuitBad N L k) ≤ ↑N * ENNReal.ofReal (codeCapacityBound (↑(L.choose 2)) p k)

★★ The circuit-level failure bound. A circuit of N locations, each simulated at level k by a gadget of L fault locations under independent faults of rate at most p, has some bad gadget with probability at most N · (c p)^{2^k} / c, c = C(L, 2): the code-capacity recursion at each location, and the union bound over the locations.

theorem mul_codeCapacityBound_lt_of_log_div_lt {c p ε : ℝ} (hc : 0 < c) (hp : 0 < p) (h : c * p < 1) {N : ℕ} (hN : 0 < N) (hε : 0 < ε) {k : ℕ} (hk : Real.log (c * ε / ↑N) / Real.log (c * p) < 2 ^ k) : ↑N * codeCapacityBound c p k < ε

★ How many levels an accuracy needs: any k whose 2^k exceeds log(c ε / N) / log(c p) brings the circuit bound below ε. Both logarithms are negative below the threshold, so the ratio is positive and a single logarithm — the level grows like log log (N / ε).

theorem exists_level_mul_lt {c p ε : ℝ} (hc : 0 < c) (hp : 0 ≤ p) (h : c * p < 1) (N : ℕ) (hε : 0 < ε) : ∃ (k : ℕ), ↑N * codeCapacityBound c p k < ε

★ The threshold, in the form a circuit designer uses: below p < 1/c every accuracy is reachable at some level, whatever the circuit's size.

theorem exists_level_circuitMeasure_lt (N L : ℕ) (ν : MeasureTheory.Measure Bool) [MeasureTheory.IsProbabilityMeasure ν] {p ε : ℝ} (hp : 0 ≤ p) (hν : ν {b : Bool | b = true} ≤ ENNReal.ofReal p) (hL : 0 < L.choose 2) (h : ↑(L.choose 2) * p < 1) (hε : 0 < ε) : ∃ (k : ℕ), (circuitMeasure N L ν k) (circuitBad N L k) < ENNReal.ofReal ε

★★★ The circuit-level threshold theorem, probabilistic form. Below the threshold p < 1/C(L, 2), for every circuit size N and every accuracy ε there is a concatenation level at which the probability that any of the circuit's N level-k gadgets is bad is less than ε — with the gadgets' fault locations, and hence the overhead, counted by card_concatPat.

theorem pow_eq_rpow_logb {L : ℕ} (hL : 0 < L) (k : ℕ) : ↑L ^ k = (2 ^ k) ^ Real.logb 2 ↑L

The overhead as a power of the doubling parameter: L ^ k = (2 ^ k) ^ (log₂ L).

theorem exists_level_two_pow_le {c p ε : ℝ} (hc : 0 < c) (hp : 0 < p) (h : c * p < 1) {N : ℕ} (hN : 0 < N) (hε : 0 < ε) : ∃ (k : ℕ), ↑N * codeCapacityBound c p k < ε ∧ 2 ^ k ≤ 4 * max 1 (Real.log (c * ε / ↑N) / Real.log (c * p))

★★ The level that meets an accuracy has a doubly-logarithmic doubling parameter. Taking k = ⌈log₂ X⌉ + 1, where X = max 1 (log(cε/N)/log(cp)) is the ratio of mul_codeCapacityBound_lt_of_log_div_lt, both brings the circuit bound below ε and keeps 2 ^ k ≤ 4 X.

theorem exists_level_overhead_le {c p ε : ℝ} (hc : 0 < c) (hp : 0 < p) (h : c * p < 1) {N : ℕ} (hN : 0 < N) (hε : 0 < ε) {L : ℕ} (hL : 0 < L) : ∃ (k : ℕ), ↑N * codeCapacityBound c p k < ε ∧ ↑L ^ k ≤ (4 * max 1 (Real.log (c * ε / ↑N) / Real.log (c * p))) ^ Real.logb 2 ↑L

★★★ The overhead of the recursive simulation is polylogarithmic. At the level that meets the accuracy, a gadget's L ^ k fault locations (card_concatPat) are at most (4 X) ^ (log₂ L), with X a logarithm of N / ε: a fixed power of a logarithm, which is what “polylogarithmic overhead” means in the threshold theorem.