The concatenated Steane code: the quantum recovery at level k

Category: 3-Local (Empirical, QM twin). BACKLOG #86, the second half of #61: the quantum statement at every level of concatenation, where SteaneThreshold.lean (#51) had it at level one and the pattern recursion (concatMeasure_concatBad_le) at every level.

One level up, over any register

concatEnc W = blockKron (fun _ => W) * steaneEnc puts seven W-encoded blocks under one Steane layer; it is an isometry when W is (concatEnc_conjTranspose_mul). The engine is ★★ exists_concatEnc_step: if a pair of block-wise errors acts as a scalar on the encoded qubit of every block but at most two named ones, it acts as a scalar one level up. The good blocks give their scalars, and the tensor of the two remaining logical operators is scalar because the Steane code has distance three (exists_steaneEnc_blockKron in SteaneEncoder.lean). Two blocks, not one: the Knill–Laflamme condition is a condition on pairs of errors, and each error of the pair may spend its one arbitrary block somewhere else.

The tower

cLabel is the label space (cLabel 0 = Fin 2, cLabel (k+1) = Fin 7 → cLabel k, literally recursive, with its Fintype/DecidableEq by recursion), cEnc the encoder, cProj the code projector, and cFam/cErr the error family: a level-k error in every block and optionally one block carrying an arbitrary operator, addressed by a matrix unit. Then

• ★★★ encoderKL_cErr: Knill–Laflamme at every level, in the encoder form of Mathlib/QuantumInfo/KnillLaflamme.lean — cEnc kᴴ Eᵢᴴ Eⱼ cEnc k = γ • 1. The induction is the step above, with the two named blocks the arbitrary blocks of the two errors;
• ★★★ exists_cErr_recovery: one recovery channel per level for that family.

The patterns, and the failure bound

PatErr k x E says E is an error of the pattern x: a tensor over the tree with the identity at every unhit leaf and an arbitrary operator at every hit one. isBad 7 k x = false — at most one bad sub-block at every level — is the good event of the code-capacity recursion, and

• ★★ patErr_mem_span: every good pattern's errors lie in the span of the family. The good blocks are spans by induction, the one bad block is a combination of matrix units (Matrix.matrix_eq_sum_single), and blockKron is multilinear (blockKron_sum_smul), so the tensor expands over exactly cErr (k + 1);
• ★★★ exists_concat_recovery: the recovery returns the code state up to a scalar for every good pattern, through #61's span step (exists_smul_recovery_apply_of_eq_lin_comb);
• ★★★ exists_concat_recovery_unitary: for a unitary error the scalar is 1 (smul_eq_one_of_unitary: the error and the channel both preserve the trace), so the level-k code restores every code state exactly from every good pattern. What it says nothing about is concatBad 7 k (good_eq_compl_concatBad), whose probability under independent noise of rate p is at most (21 p)^{2^k}/21 (steane_concatBad_le) — the encoded failure bound at every level.

Honest scope

⚠️ Code capacity still: the noise is on the data qubits, the recovery is applied once, and the gates of the encoder and of the recovery are perfect. Faulty gates, error propagation and extended rectangles are BACKLOG #62, deliberately not claimed. ⚠️ The recovery is a Knill–Laflamme channel, not the block-by-block decoder a compiler would run: what is proved is that a correcting channel exists at every level (and is the one exists_recovery_of_encoderKL builds), not that the hierarchical decoder is optimal or efficient. ⚠️ The scalar of exists_concat_recovery is existential, as in #61: for a non-unitary error the recovery returns the code state with a weight, and nothing here normalises it. ⚠️ ρ.trace ≠ 0 in the unitary statement is what turns "up to a scalar" into "exactly"; a density operator has trace one, so it is no restriction in use. ⚠️ The family cErr addresses its one arbitrary block by matrix units, a spanning set, not by Paulis. That is enough for the span argument and avoids Pauli bookkeeping at every level; the price is that the family is larger than it needs to be.

Source

A. Steane, Error correcting codes in quantum theory, PRL 77 (1996); E. Knill, R. Laflamme, W. Zurek, Science 279 (1998) 342 (concatenation and the threshold); M. Nielsen, I. Chuang, §10.6.1; Mathlib/QuantumInfo/BlockKron.lean, Mathlib/QuantumInfo/KnillLaflamme.lean (the encoder form and the span step), Empirical/QM/QEC/SteaneEncoder.lean, Empirical/QM/QEC/SteaneArbitrary.lean (#61), Empirical/QM/QEC/SteaneThreshold.lean (#51), Mathlib/Probability/CodeCapacityThreshold.lean; specs/BACKLOG.md #86; specs/steane-plan.md; specs/future-work.md.

One level up

noncomputable def CSD.Empirical.QM.QEC.Steane.concatEnc {L : Type u_1} (W : Matrix L (Fin 2) ℂ) : Matrix (Fin 7 → L) (Fin 2) ℂ

One level up: seven blocks, each carrying the encoder W, then the Steane encoder on the seven encoded qubits.

Equations

• CSD.Empirical.QM.QEC.Steane.concatEnc W = (QuantumInfo.blockKron fun (x : Fin 7) => W) * CSD.Empirical.QM.QEC.Steane.steaneEnc

theorem CSD.Empirical.QM.QEC.Steane.concatEnc_conjTranspose_mul {L : Type u_1} [Fintype L] {W : Matrix L (Fin 2) ℂ} (hW : W.conjTranspose * W = 1) : (concatEnc W).conjTranspose * concatEnc W = 1

The level-up encoder is an isometry if W is.

theorem CSD.Empirical.QM.QEC.Steane.exists_concatEnc_step {L : Type u_1} [Fintype L] {W : Matrix L (Fin 2) ℂ} (b₀ b₁ : Fin 7) (A A' : Fin 7 → Matrix L L ℂ) (h : ∀ (b : Fin 7), b ≠ b₀ → b ≠ b₁ → ∃ (γ : ℂ), W.conjTranspose * (A b).conjTranspose * A' b * W = γ • 1) : ∃ (δ : ℂ), (concatEnc W).conjTranspose * (QuantumInfo.blockKron A).conjTranspose * QuantumInfo.blockKron A' * concatEnc W = δ • 1

★★ The induction step. A pair of block-wise errors whose logical actions are scalars on every block but at most two named ones acts as a scalar on the qubit encoded one level up: the good blocks contribute their scalars and the tensor of the remaining logical operators is scalar by the Steane code's distance (exists_steaneEnc_blockKron).

The tower of concatenated registers

def CSD.Empirical.QM.QEC.Steane.cLabel : ℕ → Type

The label space of the level-k concatenated register: one qubit at level 0, seven blocks of the previous level after that.

Equations

• CSD.Empirical.QM.QEC.Steane.cLabel 0 = Fin 2
• CSD.Empirical.QM.QEC.Steane.cLabel k.succ = (Fin 7 → CSD.Empirical.QM.QEC.Steane.cLabel k)

@[instance_reducible]

instance CSD.Empirical.QM.QEC.Steane.instFintypeCLabel (k : ℕ) : Fintype (cLabel k)

Equations

• CSD.Empirical.QM.QEC.Steane.instFintypeCLabel 0 = { elems := CSD.Empirical.QM.QEC.Steane.instFintypeCLabel._aux_1, complete := CSD.Empirical.QM.QEC.Steane.instFintypeCLabel._proof_3 }
• CSD.Empirical.QM.QEC.Steane.instFintypeCLabel k.succ = { elems := CSD.Empirical.QM.QEC.Steane.instFintypeCLabel._aux_4 k (CSD.Empirical.QM.QEC.Steane.instFintypeCLabel k), complete := ⋯ }

@[instance_reducible]

instance CSD.Empirical.QM.QEC.Steane.instDecidableEqCLabel (k : ℕ) : DecidableEq (cLabel k)

Equations

• CSD.Empirical.QM.QEC.Steane.instDecidableEqCLabel 0 = CSD.Empirical.QM.QEC.Steane.instDecidableEqCLabel._aux_1
• CSD.Empirical.QM.QEC.Steane.instDecidableEqCLabel k.succ = CSD.Empirical.QM.QEC.Steane.instDecidableEqCLabel._aux_3 k (CSD.Empirical.QM.QEC.Steane.instDecidableEqCLabel k)

noncomputable def CSD.Empirical.QM.QEC.Steane.cEnc (k : ℕ) : Matrix (cLabel k) (Fin 2) ℂ

The encoder of the level-k concatenated code: nothing at level 0, one more Steane layer at every step.

Equations

• CSD.Empirical.QM.QEC.Steane.cEnc 0 = 1
• CSD.Empirical.QM.QEC.Steane.cEnc k.succ = CSD.Empirical.QM.QEC.Steane.concatEnc (CSD.Empirical.QM.QEC.Steane.cEnc k)

noncomputable def CSD.Empirical.QM.QEC.Steane.cProj (k : ℕ) : Matrix (cLabel k) (cLabel k) ℂ

The code projector of the level-k code.

Equations

• CSD.Empirical.QM.QEC.Steane.cProj k = CSD.Empirical.QM.QEC.Steane.cEnc k * (CSD.Empirical.QM.QEC.Steane.cEnc k).conjTranspose

theorem CSD.Empirical.QM.QEC.Steane.cEnc_zero : cEnc 0 = 1

theorem CSD.Empirical.QM.QEC.Steane.cEnc_conjTranspose_mul (k : ℕ) : (cEnc k).conjTranspose * cEnc k = 1

theorem CSD.Empirical.QM.QEC.Steane.isCodeProjector_cProj (k : ℕ) : QuantumInfo.IsCodeProjector (cProj k)

The error family of the level-k code

def CSD.Empirical.QM.QEC.Steane.cFam : ℕ → Type

The index of the level-k error family: at level k + 1, a level-k error in every block and optionally one block carrying an arbitrary operator, addressed by a matrix unit.

Equations

• CSD.Empirical.QM.QEC.Steane.cFam 0 = Unit
• CSD.Empirical.QM.QEC.Steane.cFam k.succ = ((Fin 7 → CSD.Empirical.QM.QEC.Steane.cFam k) × Option (Fin 7 × CSD.Empirical.QM.QEC.Steane.cLabel k × CSD.Empirical.QM.QEC.Steane.cLabel k))

@[instance_reducible]

instance CSD.Empirical.QM.QEC.Steane.instFintypeCFam (k : ℕ) : Fintype (cFam k)

Equations

• CSD.Empirical.QM.QEC.Steane.instFintypeCFam 0 = { elems := CSD.Empirical.QM.QEC.Steane.instFintypeCFam._aux_1, complete := CSD.Empirical.QM.QEC.Steane.instFintypeCFam._proof_3 }
• CSD.Empirical.QM.QEC.Steane.instFintypeCFam k.succ = { elems := CSD.Empirical.QM.QEC.Steane.instFintypeCFam._aux_4 k (CSD.Empirical.QM.QEC.Steane.instFintypeCFam k), complete := ⋯ }

@[instance_reducible]

instance CSD.Empirical.QM.QEC.Steane.instDecidableEqCFam (k : ℕ) : DecidableEq (cFam k)

Equations

• CSD.Empirical.QM.QEC.Steane.instDecidableEqCFam 0 = CSD.Empirical.QM.QEC.Steane.instDecidableEqCFam._aux_1
• CSD.Empirical.QM.QEC.Steane.instDecidableEqCFam k.succ = CSD.Empirical.QM.QEC.Steane.instDecidableEqCFam._aux_3 k (CSD.Empirical.QM.QEC.Steane.instDecidableEqCFam k)

noncomputable def CSD.Empirical.QM.QEC.Steane.cErr (k : ℕ) : cFam k → Matrix (cLabel k) (cLabel k) ℂ

The level-k error family.

Equations

• CSD.Empirical.QM.QEC.Steane.cErr 0 x_2 = 1
• CSD.Empirical.QM.QEC.Steane.cErr k.succ (g, none) = QuantumInfo.blockKron fun (b : Fin 7) => CSD.Empirical.QM.QEC.Steane.cErr k (g b)
• CSD.Empirical.QM.QEC.Steane.cErr k.succ (g, some (b₀, u, v)) = QuantumInfo.blockKron fun (b : Fin 7) => if b = b₀ then Matrix.single u v 1 else CSD.Empirical.QM.QEC.Steane.cErr k (g b)

theorem CSD.Empirical.QM.QEC.Steane.cErr_zero (i : cFam 0) : cErr 0 i = 1

noncomputable def CSD.Empirical.QM.QEC.Steane.cBlocks (k : ℕ) (i : cFam (k + 1)) (b : Fin 7) : Matrix (cLabel k) (cLabel k) ℂ

The blocks of a level-(k + 1) family member.

Equations

• One or more equations did not get rendered due to their size.

def CSD.Empirical.QM.QEC.Steane.cBadPos (k : ℕ) (i : cFam (k + 1)) : Fin 7

The block a level-(k + 1) family member may treat as arbitrary.

Equations

• CSD.Empirical.QM.QEC.Steane.cBadPos k i = match i.2 with | none => 0 | some (b₀, fst, snd) => b₀

theorem CSD.Empirical.QM.QEC.Steane.cErr_succ (k : ℕ) (i : cFam (k + 1)) : cErr (k + 1) i = QuantumInfo.blockKron (cBlocks k i)

theorem CSD.Empirical.QM.QEC.Steane.exists_cBlocks_eq (k : ℕ) (i : cFam (k + 1)) {b : Fin 7} (hb : b ≠ cBadPos k i) : ∃ (f : cFam k), cBlocks k i b = cErr k f

Away from its one arbitrary block, a family member carries a level-k family error.

theorem CSD.Empirical.QM.QEC.Steane.encoderKL_cErr (k : ℕ) : QuantumInfo.EncoderKL (cEnc k) (cErr k)

★★★ Knill–Laflamme at every level, in encoder form. Every pair of the level-k family acts on the encoded qubit as a scalar: the good blocks by induction, the one arbitrary block of each error by the Steane code's distance.

theorem CSD.Empirical.QM.QEC.Steane.exists_cErr_recovery (k : ℕ) : ∃ (c : Matrix (cFam k) (cFam k) ℂ) (R : QuantumInfo.Channel (cLabel k) (cLabel k) (Option (cFam k))), ∀ (ρ : Matrix (cLabel k) (cLabel k) ℂ), ρ = cProj k * ρ * cProj k → ∀ (i j : cFam k), R.apply (cErr k i * ρ * (cErr k j).conjTranspose) = c j i • ρ

★★★ The recovery of the level-k concatenated code. One channel corrects the whole family: a level-k error in every block and one arbitrary block at every level.

The errors of a pattern

def CSD.Empirical.QM.QEC.Steane.PatErr (k : ℕ) : ConcatPat 7 k → Matrix (cLabel k) (cLabel k) ℂ → Prop

The errors of an error pattern: at level 0 the identity unless the qubit is hit, and at level k + 1 a tensor over the blocks whose factors are errors of the sub-patterns. The operators at the hit leaves are arbitrary — this is the error set the code capacity argument counts.

Equations

• One or more equations did not get rendered due to their size.
• CSD.Empirical.QM.QEC.Steane.PatErr 0 x_3 E = (x_3 = false → E = 1)

theorem CSD.Empirical.QM.QEC.Steane.patErr_zero {x : ConcatPat 7 0} {E : Matrix (cLabel 0) (cLabel 0) ℂ} : PatErr 0 x E ↔ x = false → E = 1

theorem CSD.Empirical.QM.QEC.Steane.patErr_succ {k : ℕ} {x : ConcatPat 7 (k + 1)} {E : Matrix (cLabel (k + 1)) (cLabel (k + 1)) ℂ} : PatErr (k + 1) x E ↔ ∃ (N : Fin 7 → Matrix (cLabel k) (cLabel k) ℂ), E = QuantumInfo.blockKron N ∧ ∀ (b : Fin 7), PatErr k (x b) (N b)

def CSD.Empirical.QM.QEC.Steane.cIdOne (k : ℕ) : cFam k

A filler index of the level-k family: the identity error.

Equations

• CSD.Empirical.QM.QEC.Steane.cIdOne 0 = ()
• CSD.Empirical.QM.QEC.Steane.cIdOne k.succ = (fun (x : Fin 7) => CSD.Empirical.QM.QEC.Steane.cIdOne k, none)

noncomputable def CSD.Empirical.QM.QEC.Steane.cSpanFam (k : ℕ) : cFam k ⊕ cLabel k × cLabel k → Matrix (cLabel k) (cLabel k) ℂ

The per-block spanning family of the span argument: the level-k family for the good blocks, and the matrix units for the one block treated as arbitrary.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CSD.Empirical.QM.QEC.Steane.cSpanCoef (k : ℕ) (b₀ : Fin 7) (a : Fin 7 → cFam k → ℂ) (X : Matrix (cLabel k) (cLabel k) ℂ) (b : Fin 7) : cFam k ⊕ cLabel k × cLabel k → ℂ

The coefficients of the span argument: the good blocks use the coefficients the induction gives, the one arbitrary block the entries of its own operator.

Equations

• One or more equations did not get rendered due to their size.

theorem CSD.Empirical.QM.QEC.Steane.patErr_mem_span (k : ℕ) (x : ConcatPat 7 k) : isBad 7 k x = false → ∀ (E : Matrix (cLabel k) (cLabel k) ℂ), PatErr k x E → E ∈ Submodule.span ℂ (Set.range (cErr k))

★★ Every good pattern's errors lie in the span of the family. A pattern with at most one bad sub-block at every level: the good blocks are in the span of the level-k family by induction, the one bad block carries an arbitrary operator and so a combination of matrix units, and blockKron is multilinear — so the tensor expands over exactly the family cErr (k + 1).

The concatenated quantum recovery

theorem CSD.Empirical.QM.QEC.Steane.good_eq_compl_concatBad (k : ℕ) : {x : ConcatPat 7 k | isBad 7 k x = false} = (concatBad 7 k)ᶜ

The good patterns are the complement of concatBad, whose probability steane_concatBad_le bounds by (21 p)^{2^k}/21.

theorem CSD.Empirical.QM.QEC.Steane.exists_concat_recovery (k : ℕ) : ∃ (R : QuantumInfo.Channel (cLabel k) (cLabel k) (Option (cFam k))), ∀ (x : ConcatPat 7 k), isBad 7 k x = false → ∀ (E : Matrix (cLabel k) (cLabel k) ℂ), PatErr k x E → ∃ (γ : ℂ), ∀ (ρ : Matrix (cLabel k) (cLabel k) ℂ), ρ = cProj k * ρ * cProj k → R.apply (E * ρ * E.conjTranspose) = γ • ρ

★★★ The concatenated quantum recovery, up to a scalar. At every level one channel serves every good pattern: for a pattern with at most one bad sub-block at every level, and arbitrary operators on the hit leaves, the recovery returns the code state up to a scalar.

theorem CSD.Empirical.QM.QEC.Steane.exists_concat_recovery_unitary (k : ℕ) : ∃ (R : QuantumInfo.Channel (cLabel k) (cLabel k) (Option (cFam k))), ∀ (x : ConcatPat 7 k), isBad 7 k x = false → ∀ (E : Matrix (cLabel k) (cLabel k) ℂ), PatErr k x E → E.conjTranspose * E = 1 → ∀ (ρ : Matrix (cLabel k) (cLabel k) ℂ), ρ = cProj k * ρ * cProj k → ρ.trace ≠ 0 → R.apply (E * ρ * E.conjTranspose) = ρ

★★★ The concatenated quantum recovery, exactly. For a unitary error the scalar is 1: the level-k code restores every code state from every good pattern of unitary errors. The patterns for which this says nothing are concatBad 7 k, whose probability under independent noise of rate p is at most (21 p)^{2^k}/21 (steane_concatBad_le, good_eq_compl_concatBad) — so the quantum statement holds at every level, where the chain's document had it at level one.