The 15-to-1 distillation bound and its recursion

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #78, part (d) of R-004 (specs/magic-plan.md, "The split"); closes R-004.

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

The fifteen injections (BACKLOG #66–#67) leave independent Z-errors of rate p on the encoded magic state: the error pattern e ∈ 𝔽₂¹⁵ is distributed by the product measure patternMeasure ν of fifteen copies of a Bernoulli ν with ν {1} = p. The X-checks accept exactly the undetected patterns (BACKLOG #77), and an accepted pattern is wrong exactly when its weight is odd.

• patternMeasure_singleton — μ {e} = p^{|e|} (1 − p)^{15 − |e|};
• acceptSet, wrongSet; ★ measure_acceptSet_ge — acceptance ≥ (1 − p)^{15} (the zero pattern is accepted); ★ measure_wrongSet_le — accepted-and-wrong ≤ 35 p³ + 2¹¹ p⁵ (an accepted wrong pattern has odd weight ≥ 3: exactly 35 of weight 3, at most 2¹¹ of weight ≥ 5, the counts of BACKLOG #75 transported through the definitional bridge);
• ★★ distillation_error_le — the conditional error of one round: P(output wrong | accept) ≤ (35 p³ + 2¹¹ p⁵) / (1 − p)^{15} — Bravyi–Kitaev's 35 p³ at leading order; ★ distillation_error_le_ninety — for p ≤ 1/20 the bound is at most 90 p³;
• distillIter p k — the recursion p ↦ 90 p³; ★ distillIter_le, ★★ tendsto_distillIter — below p ≤ 1/20 the iterated error rate tends to 0 (as p (90 p²)^k, a crude but valid envelope of the triple-exponential decay).

Honest scope

⚠️ The recursion iterates the one-round bound under the standard modelling assumption that the output errors of one round are again independent Z-errors of the bounded rate; the threshold p ≤ 1/20 is a convenient sufficient condition, not Bravyi–Kitaev's exact fixed point ≈ 0.141. The explicit decoding circuit is BACKLOG #79.

References: S. Bravyi, A. Kitaev, PRA 71 (2005) 022316 §IV; specs/magic-plan.md; specs/BACKLOG.md #78; specs/future-work.md.

Transport of the counts from ReedMuller15.lean

theorem QuantumInfo.ReedMuller15.wt_eq_weight (e : Fin 15 → Fin 2) : wt e = ReedMuller15.weight e

theorem QuantumInfo.ReedMuller15.wt_ne_one_of_undetected {e : Fin 15 → Fin 2} (he : syndromeF e = 0) : wt e ≠ 1

theorem QuantumInfo.ReedMuller15.wt_ne_two_of_undetected {e : Fin 15 → Fin 2} (he : syndromeF e = 0) : wt e ≠ 2

theorem QuantumInfo.ReedMuller15.card_undetected_wt_three : {e : Fin 15 → Fin 2 | syndromeF e = 0 ∧ wt e = 3}.card = 35

Exactly 35 undetected patterns of weight 3 (BACKLOG #75, on Fin 2 labels).

theorem QuantumInfo.ReedMuller15.card_undetectedF : {e : Fin 15 → Fin 2 | syndromeF e = 0}.card = 2 ^ 11

2¹¹ undetected patterns (BACKLOG #75, on Fin 2 labels).

The pattern measure

@[reducible, inline]

noncomputable abbrev QuantumInfo.ReedMuller15.patternMeasure (ν : MeasureTheory.Measure (Fin 2)) : MeasureTheory.Measure (Fin 15 → Fin 2)

Fifteen independent copies of the single-qubit error law ν.

Equations

• QuantumInfo.ReedMuller15.patternMeasure ν = MeasureTheory.Measure.pi fun (x : Fin 15) => ν

theorem QuantumInfo.ReedMuller15.measure_zero_eq (ν : MeasureTheory.Measure (Fin 2)) [MeasureTheory.IsProbabilityMeasure ν] {p : ℝ} (hp0 : 0 ≤ p) (hν : ν {1} = ENNReal.ofReal p) : ν {0} = ENNReal.ofReal (1 - p)

theorem QuantumInfo.ReedMuller15.patternMeasure_singleton (ν : MeasureTheory.Measure (Fin 2)) [MeasureTheory.IsProbabilityMeasure ν] {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hν : ν {1} = ENNReal.ofReal p) (e : Fin 15 → Fin 2) : (patternMeasure ν) {e} = ENNReal.ofReal (p ^ wt e * (1 - p) ^ (15 - wt e))

μ {e} = p^{|e|} (1 − p)^{15 − |e|}.

def QuantumInfo.ReedMuller15.acceptSet : Set (Fin 15 → Fin 2)

The accepted patterns: zero syndrome.

Equations

• QuantumInfo.ReedMuller15.acceptSet = {e : Fin 15 → Fin 2 | QuantumInfo.ReedMuller15.syndromeF e = 0}

def QuantumInfo.ReedMuller15.wrongSet : Set (Fin 15 → Fin 2)

The accepted and wrong patterns: zero syndrome and odd parity.

Equations

• QuantumInfo.ReedMuller15.wrongSet = {e : Fin 15 → Fin 2 | QuantumInfo.ReedMuller15.syndromeF e = 0 ∧ QuantumInfo.ReedMuller15.parity e = 1}

theorem QuantumInfo.ReedMuller15.acceptSet_eq : acceptSet = ↑{e : Fin 15 → Fin 2 | syndromeF e = 0}

theorem QuantumInfo.ReedMuller15.measurableSet_acceptSet : MeasurableSet acceptSet

theorem QuantumInfo.ReedMuller15.wt_zero : wt 0 = 0

theorem QuantumInfo.ReedMuller15.measure_acceptSet_ge (ν : MeasureTheory.Measure (Fin 2)) [MeasureTheory.IsProbabilityMeasure ν] {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hν : ν {1} = ENNReal.ofReal p) : ENNReal.ofReal ((1 - p) ^ 15) ≤ (patternMeasure ν) acceptSet

★ Acceptance probability at least (1 − p)^{15}: the zero pattern is accepted.

theorem QuantumInfo.ReedMuller15.singleton_le_pow_wt (ν : MeasureTheory.Measure (Fin 2)) [MeasureTheory.IsProbabilityMeasure ν] {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hν : ν {1} = ENNReal.ofReal p) (e : Fin 15 → Fin 2) : (patternMeasure ν) {e} ≤ ENNReal.ofReal (p ^ wt e)

theorem QuantumInfo.ReedMuller15.measure_wrongSet_le (ν : MeasureTheory.Measure (Fin 2)) [MeasureTheory.IsProbabilityMeasure ν] {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hν : ν {1} = ENNReal.ofReal p) : (patternMeasure ν) wrongSet ≤ ENNReal.ofReal (35 * p ^ 3 + 2 ^ 11 * p ^ 5)

★ Accepted-and-wrong probability at most 35 p³ + 2¹¹ p⁵.

The conditional error of one round

theorem QuantumInfo.ReedMuller15.acceptSet_inter : acceptSet ∩ {e : Fin 15 → Fin 2 | parity e = 1} = wrongSet

theorem QuantumInfo.ReedMuller15.distillation_error_le (ν : MeasureTheory.Measure (Fin 2)) [MeasureTheory.IsProbabilityMeasure ν] {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p < 1) (hν : ν {1} = ENNReal.ofReal p) : (patternMeasure ν)[{e : Fin 15 → Fin 2 | parity e = 1} | acceptSet] ≤ ENNReal.ofReal ((35 * p ^ 3 + 2 ^ 11 * p ^ 5) / (1 - p) ^ 15)

★★ The 15-to-1 distillation bound: conditional on acceptance, the output is wrong with probability at most (35 p³ + 2¹¹ p⁵) / (1 − p)^{15} — Bravyi–Kitaev's 35 p³ at leading order.

theorem QuantumInfo.ReedMuller15.bound_le_ninety {p : ℝ} (hp0 : 0 ≤ p) (hp : p ≤ 1 / 20) : (35 * p ^ 3 + 2 ^ 11 * p ^ 5) / (1 - p) ^ 15 ≤ 90 * p ^ 3

For p ≤ 1/20 the one-round bound is at most 90 p³.

theorem QuantumInfo.ReedMuller15.distillation_error_le_ninety (ν : MeasureTheory.Measure (Fin 2)) [MeasureTheory.IsProbabilityMeasure ν] {p : ℝ} (hp0 : 0 ≤ p) (hp : p ≤ 1 / 20) (hν : ν {1} = ENNReal.ofReal p) : (patternMeasure ν)[{e : Fin 15 → Fin 2 | parity e = 1} | acceptSet] ≤ ENNReal.ofReal (90 * p ^ 3)

★ One round for p ≤ 1/20: the conditional error is at most 90 p³.

The recursion

def QuantumInfo.ReedMuller15.distillIter (p : ℝ) : ℕ → ℝ

The iterated error rate: p₀ = p, p_{k+1} = 90 p_k³.

Equations

• QuantumInfo.ReedMuller15.distillIter p 0 = p
• QuantumInfo.ReedMuller15.distillIter p k.succ = 90 * QuantumInfo.ReedMuller15.distillIter p k ^ 3

theorem QuantumInfo.ReedMuller15.distillIter_zero (p : ℝ) : distillIter p 0 = p

theorem QuantumInfo.ReedMuller15.distillIter_succ (p : ℝ) (k : ℕ) : distillIter p (k + 1) = 90 * distillIter p k ^ 3

theorem QuantumInfo.ReedMuller15.distillIter_le {p : ℝ} (hp0 : 0 ≤ p) (hp : p ≤ 1 / 20) (k : ℕ) : 0 ≤ distillIter p k ∧ distillIter p k ≤ p ∧ distillIter p k ≤ p * (90 * p ^ 2) ^ k

★ For p ≤ 1/20: 0 ≤ p_k ≤ p (90 p²)^k and p_k ≤ p.

theorem QuantumInfo.ReedMuller15.tendsto_distillIter {p : ℝ} (hp0 : 0 ≤ p) (hp : p ≤ 1 / 20) : Filter.Tendsto (distillIter p) Filter.atTop (nhds 0)

★★ The distillation threshold, in the form the chain claims: below p ≤ 1/20 the iterated error rate tends to 0.