The code-capacity threshold: independent errors, two or more, and concatenation

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate). BACKLOG #51 (row 14's part (c)), the probabilistic core of the code-capacity threshold argument.

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

A distance-3 code corrects any single error, so an encoded block fails only when two or more of its n qubits are hit. Under independent noise of rate p that happens with probability at most C(n, 2) p² (the union bound over pairs). Concatenating the code k times replaces p by c p² at each level (c = C(n, 2)), giving (c p)^{2^k} / c, which is below p once c p ≤ 1 and tends to 0 once c p < 1: the threshold p < 1/c.

• ★ measure_pi_two_or_more_le — under the product of n copies of a probability measure, the patterns with two or more coordinates in a set of measure ≤ q have measure ≤ C(n, 2) q²;
• codeCapacityBound — the recursion p ↦ c p²; codeCapacityBound_eq — the closed form (c p)^{2^k} / c; codeCapacityBound_le — below p when c p ≤ 1; ★ tendsto_codeCapacityBound — the threshold: the bound tends to 0 when c p < 1;
• ConcatPat, concatMeasure, concatBad — the error patterns of a k-fold concatenated n-block code under independent noise, with the bad patterns (an error at level 0; two or more bad sub-blocks at level k + 1), and ★★ concatMeasure_concatBad_le — the code-capacity recursion: the bad patterns at level k have probability at most codeCapacityBound c p k.

The quantum half — that a block whose pattern is not bad is restored by the recovery — is the consumer's (Empirical/QM/QEC/SteaneThreshold.lean for the Steane code at level 1). References: E. Knill, R. Laflamme, W. Zurek, Resilient quantum computation, Science 279 (1998); D. Aharonov, M. Ben-Or, Fault-tolerant quantum computation with constant error rate, SIAM J. Comput. 38 (2008), §2 (the code-capacity recursion); specs/BACKLOG.md #51; specs/steane-plan.md.

theorem measure_pi_two_or_more_le {ι : Type u_1} {α : Type u_2} [Fintype ι] [MeasurableSpace α] (ν : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure ν] (P : α → Prop) [DecidablePred P] {q : ENNReal} (hP : ν {a : α | P a} ≤ q) : (MeasureTheory.Measure.pi fun (x : ι) => ν) {x : ι → α | 2 ≤ {i : ι | P (x i)}.card} ≤ ↑((Fintype.card ι).choose 2) * q ^ 2

★ Two or more of n independent events of probability ≤ q occur with probability ≤ C(n, 2) q²: under the product of n copies of a probability measure ν, the patterns with at least two coordinates satisfying P have measure at most C(n, 2) · q² when ν {P} ≤ q (the union bound over the pairs of coordinates, each pair cylinder having measure ν {P}²).

def codeCapacityBound (c p : ℝ) : ℕ → ℝ

The code-capacity recursion: p ↦ c p², iterated k times from p.

Equations

• codeCapacityBound c p 0 = p
• codeCapacityBound c p k.succ = c * codeCapacityBound c p k ^ 2

theorem codeCapacityBound_zero (c p : ℝ) : codeCapacityBound c p 0 = p

theorem codeCapacityBound_succ (c p : ℝ) (k : ℕ) : codeCapacityBound c p (k + 1) = c * codeCapacityBound c p k ^ 2

theorem codeCapacityBound_nonneg {c p : ℝ} (hc : 0 ≤ c) (hp : 0 ≤ p) (k : ℕ) : 0 ≤ codeCapacityBound c p k

theorem codeCapacityBound_eq {c : ℝ} (hc : 0 < c) (p : ℝ) (k : ℕ) : codeCapacityBound c p k = (c * p) ^ 2 ^ k / c

The closed form of the recursion: k levels give (c p)^{2^k} / c.

theorem codeCapacityBound_le {c p : ℝ} (hc : 0 < c) (hp : 0 ≤ p) (h : c * p ≤ 1) (k : ℕ) : codeCapacityBound c p k ≤ p

Below the threshold c p ≤ 1, every level is at most p.

theorem tendsto_codeCapacityBound {c p : ℝ} (hc : 0 < c) (hp : 0 ≤ p) (h : c * p < 1) : Filter.Tendsto (codeCapacityBound c p) Filter.atTop (nhds 0)

★ The threshold: below p < 1/c the concatenated failure bound tends to 0.

def ConcatPat (n : ℕ) : ℕ → Type

Error patterns of a k-fold concatenated n-block code: level 0 is one qubit (true = an error), level k + 1 is n blocks of level k.

Equations

• ConcatPat n 0 = Bool
• ConcatPat n k.succ = (Fin n → ConcatPat n k)

@[instance_reducible]

instance instMeasurableSpaceConcatPat (n k : ℕ) : MeasurableSpace (ConcatPat n k)

Equations

• instMeasurableSpaceConcatPat n 0 = instMeasurableSpaceConcatPat._aux_1 n
• instMeasurableSpaceConcatPat n k.succ = MeasurableSpace.pi

noncomputable def concatMeasure (n : ℕ) (ν : MeasureTheory.Measure Bool) [MeasureTheory.IsProbabilityMeasure ν] (k : ℕ) : { μ : MeasureTheory.Measure (ConcatPat n k) // MeasureTheory.IsProbabilityMeasure μ }

The independent noise on k-level patterns: ν on each qubit, the product across blocks, bundled with its probability-measure proof (which the next product needs).

Equations

• concatMeasure n ν 0 = ⟨ν, inst✝⟩
• concatMeasure n ν k.succ = ⟨MeasureTheory.Measure.pi fun (x : Fin n) => ↑(concatMeasure n ν k), ⋯⟩

def isBad (n k : ℕ) : ConcatPat n k → Bool

The bad patterns, as a Boolean test: an error at level 0; two or more bad sub-blocks at level k + 1.

Equations

• isBad n 0 = fun (b : ConcatPat n 0) => b
• isBad n k.succ = fun (x : ConcatPat n (k + 1)) => decide (2 ≤ {i : Fin n | isBad n k (x i) = true}.card)

def concatBad (n k : ℕ) : Set (ConcatPat n k)

The set of bad patterns at level k.

Equations

• concatBad n k = {x : ConcatPat n k | isBad n k x = true}

theorem concatBad_zero (n : ℕ) : concatBad n 0 = {b : Bool | b = true}

theorem concatBad_succ (n k : ℕ) : concatBad n (k + 1) = {x : Fin n → ConcatPat n k | 2 ≤ {i : Fin n | isBad n k (x i) = true}.card}

theorem concatMeasure_concatBad_le (n : ℕ) (ν : MeasureTheory.Measure Bool) [MeasureTheory.IsProbabilityMeasure ν] {p : ℝ} (hp : 0 ≤ p) (hν : ν {b : Bool | b = true} ≤ ENNReal.ofReal p) (k : ℕ) : ↑(concatMeasure n ν k) (concatBad n k) ≤ ENNReal.ofReal (codeCapacityBound (↑(n.choose 2)) p k)

★★ The code-capacity recursion on error patterns. Under independent noise with per-qubit error probability at most p, the bad patterns of the k-fold concatenated n-block code have probability at most codeCapacityBound (C(n, 2)) p k = (C(n, 2) p)^{2^k} / C(n, 2).