Level reduction, and the probabilistic join

Category: 1-Mathlib (CSD-free). BACKLOG #97, split out of #62 (d2) — the last of that row's remainder.

Three things were deliberately left out of #94, #95 and #96, and they are what this file supplies: the recursion (a level-k gadget is a level-(k−1) circuit), the fault count, and the join of the deterministic and probabilistic halves into one statement.

The deterministic half is #62 (d1)'s ★★★ correctedRun_eq_idealRun; the arithmetic half is #51's codeCapacityBound with ★★ concatMeasure_concatBad_le, the code-capacity recursion on error patterns. Neither is re-proved here. What is new is the lifting, the union bound, and the step from "the good event has large probability" to "the output is exactly the ideal one with large probability".

Level reduction

• ★★★ isCorrectedStep_correctedRun — a corrected circuit is a corrected step one level up: if every gadget of c is corrected and idealRun c is the gadget the next level wants, then correctedRun c is a corrected step for it. The preserves half comes free from isCodeState_idealRun, so no extra hypothesis is needed;
• IsCorrectedAtLevel P k ideal impl — the recursive simulation: at level 0 a corrected step, and at level k + 1 the corrected run of a circuit whose gadgets are corrected at level k;
• ★★★ isCorrectedStep_of_isCorrectedAtLevel — correctness at every level follows from correctness at level 0, by induction on the tower. This is the recursion the threshold theorem runs on, and with it ★★★ correctedRun_eq_idealRun_of_level: a circuit of level-k gadgets computes the ideal circuit's output.

The probabilistic join

• ★★★ one_sub_le_measure_output_eq — the join, with no measurability hypotheses at all: if the output is the ideal one on every pattern that makes no gadget bad, and each gadget is bad with probability at most q, then the output is ideal with probability at least 1 − N · q. Subadditivity does all the work — 1 ≤ μ s + μ sᶜ holds for arbitrary sets — so nothing has to be shown measurable;

• ConcatPat-valued circuit patterns, circuitMeasure, and ★ circuitMeasure_coord, the one-coordinate marginal of the product (which does need measurability, supplied by ★ measurableSet_of_concatPat: every set of patterns is measurable, since the pattern spaces are finite with measurable singletons);

• ★★★ one_sub_le_measure_output_eq_concat — the row's statement: for a circuit of N level-k concatenated gadgets under independent noise of rate at most p,

  μ {output = ideal} ≥ 1 − N · (C(n,2) · p)^(2^k) / C(n,2),
  

  which is 1 − N (cp)^{2^k}/c with c = C(n, 2). The deterministic input is the hypothesis that a pattern making no gadget bad gives the ideal output — exactly what #96's good extended rectangles and isCorrectedStep_of_isCorrectedAtLevel deliver;

• ★★ tendsto_one_sub_codeCapacityBound — and below threshold the bound tends to 1 as the level grows, from #51's tendsto_codeCapacityBound.

Honest scope

⚠️ The deterministic input is a hypothesis, and this file does not discharge it. hgood says a pattern with no bad gadget yields the ideal output. For a concrete code that is what #96's rectangles plus the level recursion above give — but no concrete gadget set is plugged in here, so nothing below is a threshold theorem for the Steane code. The row's statement is proved with its deterministic premise named, not assumed away.

⚠️ "Bad" is a pattern predicate, not a physical fault model. isBad counts two-or-more bad sub-blocks recursively; nothing here derives it from a circuit's fault locations, and the correspondence between a gadget's faults and a ConcatPat is not constructed. The locality assumption — that a gadget's failure depends only on its own block's pattern — is built into the product measure and is a modelling choice, visible in the statement as the independence of circuitMeasure.

⚠️ Independent noise. circuitMeasure is a product across gadgets and across blocks. Correlated noise is outside everything below, and so is any adversarial or non-Markovian model.

⚠️ No gate counts and no overhead. N is the number of gadgets, given; nothing bounds the circuit size needed to simulate a given computation, and no polylogarithmic-overhead claim is made or implied. That is the part of a threshold theorem this file does not touch.

⚠️ The constant is C(n, 2), from the two-or-more union bound. It is not claimed sharp, and no optimised threshold value follows from it.

⚠️ Maps, not channels, as in #62 (d1) and #96: no positivity or trace preservation is imposed anywhere, so "output" means the value of a map on a matrix.

References

Mathlib/QuantumInfo/FaultTolerantComposition.lean (#62 (d1)); Mathlib/QuantumInfo/ExtendedRectangle.lean (#96); Mathlib/Probability/CodeCapacityThreshold.lean (#51, codeCapacityBound, concatMeasure_concatBad_le); specs/BACKLOG.md #97, #96, #95, #94, #86, #62, #51; specs/future-work.md.

Level reduction

theorem QuantumInfo.isCorrectedStep_correctedRun {m : Type u_1} [Fintype m] {P : Matrix m m ℂ} {c : Circuit m} {ideal : Matrix m m ℂ → Matrix m m ℂ} (hc : IsCorrectedCircuit P c) (hideal : ∀ (ρ : Matrix m m ℂ), IsCodeState P ρ → idealRun c ρ = ideal ρ) : IsCorrectedStep P ideal (correctedRun c)

★★★ A corrected circuit is a corrected step one level up. The hypothesis is only that the circuit's ideal run is the gadget the next level wants; preserves then comes free from isCodeState_idealRun. This is the lifting the recursive simulation runs on.

def QuantumInfo.IsCorrectedAtLevel {m : Type u_1} [Fintype m] (P : Matrix m m ℂ) : ℕ → (Matrix m m ℂ → Matrix m m ℂ) → (Matrix m m ℂ → Matrix m m ℂ) → Prop

The recursive simulation. At level 0 a gadget is a corrected step; at level k + 1 it is the corrected run of a circuit whose gadgets are corrected at level k.

Equations

• One or more equations did not get rendered due to their size.
• QuantumInfo.IsCorrectedAtLevel P 0 x✝¹ x✝ = QuantumInfo.IsCorrectedStep P x✝¹ x✝

theorem QuantumInfo.isCorrectedStep_of_isCorrectedAtLevel {m : Type u_1} [Fintype m] {P : Matrix m m ℂ} (k : ℕ) (ideal impl : Matrix m m ℂ → Matrix m m ℂ) : IsCorrectedAtLevel P k ideal impl → IsCorrectedStep P ideal impl

★★★ Correctness at every level follows from correctness at level 0. The induction over the tower: each level's circuit is corrected because its gadgets are, and then the level above is a corrected step by isCorrectedStep_correctedRun.

theorem QuantumInfo.correctedRun_eq_idealRun_of_level {m : Type u_1} [Fintype m] {P : Matrix m m ℂ} {c : Circuit m} {k : ℕ} (hc : ∀ g ∈ c, IsCorrectedAtLevel P k g.1 g.2) {ρ : Matrix m m ℂ} (hρ : IsCodeState P ρ) : correctedRun c ρ = idealRun c ρ

★★★ A circuit of level-k gadgets computes the ideal circuit's output.

The join: a large good event gives a correct output

theorem QuantumInfo.one_sub_le_measure_output_eq {Ω : Type u_1} {β : Type u_2} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {N : ℕ} (Bad : Fin N → Set Ω) {out : Ω → β} {ideal : β} (hgood : ∀ (ω : Ω), (∀ (j : Fin N), ω ∉ Bad j) → out ω = ideal) {q : ENNReal} (hq : ∀ (j : Fin N), μ (Bad j) ≤ q) : 1 - ↑N * q ≤ μ {ω : Ω | out ω = ideal}

★★★ The probabilistic join. If the output is the ideal one whenever no gadget is bad, and each of the N gadgets is bad with probability at most q, then the output is ideal with probability at least 1 − N · q.

⚠️ No measurability hypotheses: subadditivity gives 1 ≤ μ s + μ sᶜ for arbitrary sets, and monotonicity does the rest.

The concatenated instance

@[instance_reducible]

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

Equations

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

instance QuantumInfo.instMeasurableSingletonClassConcatPat (n k : ℕ) : MeasurableSingletonClass (ConcatPat n k)

theorem QuantumInfo.measurableSet_of_concatPat (n k : ℕ) (S : Set (ConcatPat n k)) : MeasurableSet S

★ Every set of patterns is measurable: the pattern spaces are finite and have measurable singletons.

@[reducible, inline]

abbrev QuantumInfo.CircuitPat (N n k : ℕ) : Type

The fault patterns of a circuit of N gadgets, each a level-k concatenated block.

Equations

• QuantumInfo.CircuitPat N n k = (Fin N → ConcatPat n k)

noncomputable def QuantumInfo.circuitMeasure (N n : ℕ) (ν : MeasureTheory.Measure Bool) [MeasureTheory.IsProbabilityMeasure ν] (k : ℕ) : MeasureTheory.Measure (CircuitPat N n k)

Independent noise across the gadgets of the circuit. ⚠️ Independence is a modelling choice, and it is visible here.

Equations

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

instance QuantumInfo.instIsProbabilityMeasureCircuitMeasure (N n : ℕ) (ν : MeasureTheory.Measure Bool) [MeasureTheory.IsProbabilityMeasure ν] (k : ℕ) : MeasureTheory.IsProbabilityMeasure (circuitMeasure N n ν k)

theorem QuantumInfo.circuitMeasure_coord (N n : ℕ) (ν : MeasureTheory.Measure Bool) [MeasureTheory.IsProbabilityMeasure ν] (k : ℕ) (j : Fin N) (S : Set (ConcatPat n k)) : (circuitMeasure N n ν k) {ω : CircuitPat N n k | ω j ∈ S} = ↑(concatMeasure n ν k) S

★ The one-coordinate marginal of the circuit's noise is one gadget's noise.

theorem QuantumInfo.one_sub_le_measure_output_eq_concat {β : Type u_1} {N n k : ℕ} (ν : MeasureTheory.Measure Bool) [MeasureTheory.IsProbabilityMeasure ν] {p : ℝ} (hp : 0 ≤ p) (hν : ν {b : Bool | b = true} ≤ ENNReal.ofReal p) {out : CircuitPat N n k → β} {ideal : β} (hgood : ∀ (ω : CircuitPat N n k), (∀ (j : Fin N), isBad n k (ω j) = false) → out ω = ideal) : 1 - ↑N * ENNReal.ofReal (codeCapacityBound (↑(n.choose 2)) p k) ≤ (circuitMeasure N n ν k) {ω : CircuitPat N n k | out ω = ideal}

★★★ The threshold statement. For a circuit of N gadgets, each a level-k concatenated block under independent noise of rate at most p, the output is exactly the ideal one with probability at least

1 − N · (C(n,2) · p)^(2^k) / C(n,2),

which is the row's 1 − N (cp)^{2^k}/c. The deterministic premise hgood — a pattern with no bad gadget gives the ideal output — is what #96's good extended rectangles and isCorrectedStep_of_isCorrectedAtLevel supply for a concrete gadget set; it is named here, not assumed away.

theorem QuantumInfo.tendsto_one_sub_codeCapacityBound {n N : ℕ} {p : ℝ} (hc : 0 < ↑(n.choose 2)) (hp : 0 ≤ p) (h : ↑(n.choose 2) * p < 1) : Filter.Tendsto (fun (k : ℕ) => 1 - ↑N * ENNReal.ofReal (codeCapacityBound (↑(n.choose 2)) p k)) Filter.atTop (nhds 1)

★★ Below threshold the bound tends to 1. With C(n,2) · p < 1, raising the concatenation level drives the failure probability to 0, so the output is ideal with probability tending to 1. From #51's tendsto_codeCapacityBound; the limit is of the bound, not of the measure.