Composing corrected gadgets along a circuit

Category: 1-Mathlib (CSD-free; staged for upstream).

BACKLOG #62's threshold programme has per-gadget theorems — a faulty transversal gate, Hadamard, logical X̄/Z̄ or two-block CNOT is corrected by one recovery channel — and the probabilistic accounting over a circuit's locations. What it did not have is the step between them: a circuit, and the statement that correcting each gadget in turn reproduces the ideal circuit. This module is that step, abstractly:

• IsCodeState P ρ — the state is supported in the code space of the projector P;
• IsCorrectedStep P ideal step — the two conditions a gadget must meet to be composable: step (a faulty gadget followed by its recovery) returns the ideal gadget's output on code states, and the ideal gadget keeps code states in the code space. The second is the one that is easy to forget and does all the work in the induction: it is what hands the next gadget the hypothesis it needs;
• Circuit, idealRun, correctedRun — a circuit is a list of gadgets, each given by its ideal action and by the corrected step that implements it; the head acts first;
• ★ isCodeState_idealRun — the ideal run stays in the code space, gadget by gadget;
• ★★★ correctedRun_eq_idealRun — the composition theorem: a circuit whose every gadget is faulty and whose every fault is corrected computes exactly what the ideal circuit computes, on any code state.

The abstraction is deliberate. step is an arbitrary map on density operators, so it does not care whether the recovery is an ideal channel or itself a faulty circuit: when #62(c) makes the recovery gadget faulty, the same theorem applies to the new steps with no restatement.

Honest scope

⚠️ This is the deterministic half. Nothing here counts faults or assigns them probabilities: the hypothesis is that every gadget's fault is corrected, and the conclusion is exact equality. The probability that a circuit's fault pattern is correctable is Probability/CircuitThreshold.lean (#62(a)), and joining the two — one statement with a probability and an exact output — is #62(d2).

⚠️ No level reduction. A corrected step is a single level-1 object; the recursive simulation, where a level-k gadget is a level-(k−1) circuit, is not here (#62(d2)). Nor is there any claim that a given gadget set is universal or that a circuit computes anything in particular: idealRun is whatever the list says it is.

References: D. Aharonov, M. Ben-Or, Fault-tolerant quantum computation with constant error rate, SIAM J. Comput. 38 (2008) 1207 §§9–11 (rectangles and the simulation theorem); Probability/CircuitThreshold.lean; specs/BACKLOG.md #62.

Code states and corrected steps

def QuantumInfo.IsCodeState {n : Type u_1} [Fintype n] (P ρ : Matrix n n ℂ) : Prop

A state supported in the code space of the projector P.

Equations

• QuantumInfo.IsCodeState P ρ = (ρ = P * ρ * P)

structure QuantumInfo.IsCorrectedStep {n : Type u_1} [Fintype n] (P : Matrix n n ℂ) (ideal step : Matrix n n ℂ → Matrix n n ℂ) : Prop

A corrected step: step — think of a faulty gadget followed by its recovery — agrees with the ideal gadget on code states, and the ideal gadget keeps code states in the code space. The two conditions together are exactly what makes a circuit of such steps compose: the second is what hands the next gadget the hypothesis it needs.

• recovers (ρ : Matrix n n ℂ) : IsCodeState P ρ → step ρ = ideal ρ

  On a code state the step returns the ideal gadget's output.

• preserves (ρ : Matrix n n ℂ) : IsCodeState P ρ → IsCodeState P (ideal ρ)

  The ideal gadget keeps code states in the code space.

Circuits

@[reducible, inline]

abbrev QuantumInfo.Circuit (n : Type u_2) : Type u_2

A circuit: a list of gadgets, each given by its ideal action and by the corrected step that implements it. The head of the list acts first.

Equations

• QuantumInfo.Circuit n = List ((Matrix n n ℂ → Matrix n n ℂ) × (Matrix n n ℂ → Matrix n n ℂ))

def QuantumInfo.runMaps {n : Type u_1} (steps : List (Matrix n n ℂ → Matrix n n ℂ)) (ρ : Matrix n n ℂ) : Matrix n n ℂ

Running a list of maps, the head first.

Equations

• QuantumInfo.runMaps steps ρ = List.foldl (fun (σ : Matrix n n ℂ) (S : Matrix n n ℂ → Matrix n n ℂ) => S σ) ρ steps

@[simp]

theorem QuantumInfo.runMaps_nil {n : Type u_1} (ρ : Matrix n n ℂ) : runMaps [] ρ = ρ

@[simp]

theorem QuantumInfo.runMaps_cons {n : Type u_1} (S : Matrix n n ℂ → Matrix n n ℂ) (steps : List (Matrix n n ℂ → Matrix n n ℂ)) (ρ : Matrix n n ℂ) : runMaps (S :: steps) ρ = runMaps steps (S ρ)

def QuantumInfo.idealRun {n : Type u_1} (c : Circuit n) (ρ : Matrix n n ℂ) : Matrix n n ℂ

The circuit's ideal action: every gadget acting ideally.

Equations

• QuantumInfo.idealRun c ρ = QuantumInfo.runMaps (List.map Prod.fst c) ρ

def QuantumInfo.correctedRun {n : Type u_1} (c : Circuit n) (ρ : Matrix n n ℂ) : Matrix n n ℂ

The circuit as actually run: every gadget faulty, every fault corrected.

Equations

• QuantumInfo.correctedRun c ρ = QuantumInfo.runMaps (List.map Prod.snd c) ρ

@[simp]

theorem QuantumInfo.idealRun_nil {n : Type u_1} (ρ : Matrix n n ℂ) : idealRun [] ρ = ρ

@[simp]

theorem QuantumInfo.correctedRun_nil {n : Type u_1} (ρ : Matrix n n ℂ) : correctedRun [] ρ = ρ

@[simp]

theorem QuantumInfo.idealRun_cons {n : Type u_1} (g : (Matrix n n ℂ → Matrix n n ℂ) × (Matrix n n ℂ → Matrix n n ℂ)) (c : Circuit n) (ρ : Matrix n n ℂ) : idealRun (g :: c) ρ = idealRun c (g.1 ρ)

@[simp]

theorem QuantumInfo.correctedRun_cons {n : Type u_1} (g : (Matrix n n ℂ → Matrix n n ℂ) × (Matrix n n ℂ → Matrix n n ℂ)) (c : Circuit n) (ρ : Matrix n n ℂ) : correctedRun (g :: c) ρ = correctedRun c (g.2 ρ)

def QuantumInfo.IsCorrectedCircuit {n : Type u_1} [Fintype n] (P : Matrix n n ℂ) (c : Circuit n) : Prop

A circuit all of whose gadgets are corrected steps for the code P.

Equations

• QuantumInfo.IsCorrectedCircuit P c = ∀ g ∈ c, QuantumInfo.IsCorrectedStep P g.1 g.2

theorem QuantumInfo.isCorrectedCircuit_nil {n : Type u_1} [Fintype n] (P : Matrix n n ℂ) : IsCorrectedCircuit P []

theorem QuantumInfo.IsCorrectedCircuit.tail {n : Type u_1} [Fintype n] {P : Matrix n n ℂ} {g : (Matrix n n ℂ → Matrix n n ℂ) × (Matrix n n ℂ → Matrix n n ℂ)} {c : Circuit n} (h : IsCorrectedCircuit P (g :: c)) : IsCorrectedCircuit P c

theorem QuantumInfo.IsCorrectedCircuit.head {n : Type u_1} [Fintype n] {P : Matrix n n ℂ} {g : (Matrix n n ℂ → Matrix n n ℂ) × (Matrix n n ℂ → Matrix n n ℂ)} {c : Circuit n} (h : IsCorrectedCircuit P (g :: c)) : IsCorrectedStep P g.1 g.2

theorem QuantumInfo.isCodeState_idealRun {n : Type u_1} [Fintype n] {P : Matrix n n ℂ} {c : Circuit n} (hc : IsCorrectedCircuit P c) {ρ : Matrix n n ℂ} (hρ : IsCodeState P ρ) : IsCodeState P (idealRun c ρ)

★ The ideal run stays in the code space, gadget by gadget.

theorem QuantumInfo.correctedRun_eq_idealRun {n : Type u_1} [Fintype n] {P : Matrix n n ℂ} {c : Circuit n} (hc : IsCorrectedCircuit P c) {ρ : Matrix n n ℂ} (hρ : IsCodeState P ρ) : correctedRun c ρ = idealRun c ρ

★★★ The composition theorem: a circuit whose every gadget is faulty and whose every fault is corrected computes exactly what the ideal circuit computes, on any code state. The induction is the whole content: each corrected step returns the ideal output, and the ideal output is again a code state, so the next gadget's hypothesis is available. Nothing here is special to a code or to a gadget set — which is the point: when the recovery itself becomes a faulty circuit, the same theorem applies to the new steps.

theorem QuantumInfo.isCorrectedCircuit_replicate {n : Type u_1} [Fintype n] {P : Matrix n n ℂ} {g : (Matrix n n ℂ → Matrix n n ℂ) × (Matrix n n ℂ → Matrix n n ℂ)} (h : IsCorrectedStep P g.1 g.2) (k : ℕ) : IsCorrectedCircuit P (List.replicate k g)

A circuit of copies of one corrected gadget is corrected.