Empirical/QM: independent bit-flip noise on the three-qubit code, and its residual failure

Category: 3-Local. QM-validity layer (matrix algebra over the K2 Channel layer; no CSD content). BACKLOG #52, the QM half.

SyndromeRecovery.lean corrects the single-error mixture ∑ₖ qₖ Eₖ ρ Eₖ exactly. The physical noise is different: each of the three qubits flips independently with probability p, so all eight flip patterns occur, the two- and three-flip patterns with total weight 3p² − 2p³, and those the code mis-corrects into the logical flip X̄ = X ⊗ X ⊗ X. This file states the channel and the exact outcome of syndrome recovery on it:

• flipOp x = X^{x₁} ⊗ X^{x₂} ⊗ X^{x₃} for a pattern x : Fin 2 × Fin 2 × Fin 2, with weight indepWeight p x = ∏ᵢ (p if xᵢ = 1 else 1 − p) (sum_indepWeight: they sum to 1);
• indepFlipChannel p — the mixed-unitary channel of that family (Channel.mixedUnitaryChannel), so ControlledDilation.lean gives it as the Stinespring channel of one joint unitary on register ⊗ ℂ⁸;
• flipOp_eq — every pattern is a single error times 1 (weight ≤ 1) or times X̄ (weight ≥ 2), the syndrome reading of the pattern; recoveryChannel_apply_flipOp — recovery returns ρ on the first and X̄ ρ X̄ on the second;
• ★★ recoveryChannel_apply_indepFlipChannel_apply — on the code, R (N_p ρ) = (1 − p_fail) ρ + p_fail X̄ ρ X̄ with p_fail = 3p² − 2p³: the recovered state is the input with probability 1 − 3p² + 2p³ and the logically flipped input otherwise (failProb_lt_of_lt_half: p_fail < p for 0 < p < 1/2, the code helps exactly below p = 1/2).

Empirical/CSD/QEC/IndependentNoiseFlow.lean reads the joint unitary as a Σ-flow.

Source

Nielsen–Chuang §10.1.1 (the three-qubit bit-flip code, the 3p² − 2p³ failure probability).

Flip patterns, their operators and their weights

@[reducible, inline]

abbrev CSD.Empirical.QM.QEC.FlipPattern : Type

A flip pattern: which of the three qubits flip (1) or not (0).

Equations

• CSD.Empirical.QM.QEC.FlipPattern = (Fin 2 × Fin 2 × Fin 2)

noncomputable def CSD.Empirical.QM.QEC.flipMat : Fin 2 → Matrix (Fin 2) (Fin 2) ℂ

flipMat 0 = 1, flipMat 1 = X.

Equations

• CSD.Empirical.QM.QEC.flipMat = ![1, CSD.Empirical.QM.QEC.pX]

@[simp]

theorem CSD.Empirical.QM.QEC.flipMat_zero : flipMat 0 = 1

@[simp]

theorem CSD.Empirical.QM.QEC.flipMat_one : flipMat 1 = pX

theorem CSD.Empirical.QM.QEC.flipMat_mul_self (x : Fin 2) : flipMat x * flipMat x = 1

theorem CSD.Empirical.QM.QEC.flipMat_conjTranspose (x : Fin 2) : (flipMat x).conjTranspose = flipMat x

noncomputable def CSD.Empirical.QM.QEC.flipOp (x : FlipPattern) : Matrix (Fin 2 × Fin 2 × Fin 2) (Fin 2 × Fin 2 × Fin 2) ℂ

The pattern error X^{x₁} ⊗ X^{x₂} ⊗ X^{x₃}.

Equations

• CSD.Empirical.QM.QEC.flipOp x = CSD.Empirical.QM.QEC.kron3 (CSD.Empirical.QM.QEC.flipMat x.1) (CSD.Empirical.QM.QEC.flipMat x.2.1) (CSD.Empirical.QM.QEC.flipMat x.2.2)

theorem CSD.Empirical.QM.QEC.kron3_one : kron3 1 1 1 = 1

theorem CSD.Empirical.QM.QEC.flipOp_mul_self (x : FlipPattern) : flipOp x * flipOp x = 1

theorem CSD.Empirical.QM.QEC.flipOp_conjTranspose (x : FlipPattern) : (flipOp x).conjTranspose = flipOp x

theorem CSD.Empirical.QM.QEC.flipOp_conjTranspose_mul_self (x : FlipPattern) : (flipOp x).conjTranspose * flipOp x = 1

noncomputable def CSD.Empirical.QM.QEC.bitWeight (p : ℝ) : Fin 2 → ℝ

The weight of one qubit's outcome: 1 − p for no flip, p for a flip.

Equations

• CSD.Empirical.QM.QEC.bitWeight p = ![1 - p, p]

@[simp]

theorem CSD.Empirical.QM.QEC.bitWeight_zero (p : ℝ) : bitWeight p 0 = 1 - p

@[simp]

theorem CSD.Empirical.QM.QEC.bitWeight_one (p : ℝ) : bitWeight p 1 = p

noncomputable def CSD.Empirical.QM.QEC.indepWeight (p : ℝ) (x : FlipPattern) : ℝ

The weight of a pattern under independent flips: the product over the three qubits.

Equations

• CSD.Empirical.QM.QEC.indepWeight p x = CSD.Empirical.QM.QEC.bitWeight p x.1 * CSD.Empirical.QM.QEC.bitWeight p x.2.1 * CSD.Empirical.QM.QEC.bitWeight p x.2.2

theorem CSD.Empirical.QM.QEC.bitWeight_nonneg {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (x : Fin 2) : 0 ≤ bitWeight p x

theorem CSD.Empirical.QM.QEC.indepWeight_nonneg {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (x : FlipPattern) : 0 ≤ indepWeight p x

theorem CSD.Empirical.QM.QEC.sum_indepWeight (p : ℝ) : ∑ x : FlipPattern, indepWeight p x = 1

The pattern weights sum to 1: ((1 − p) + p)³ = 1.

The independent bit-flip channel

noncomputable def CSD.Empirical.QM.QEC.indepFlipChannel (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) : QuantumInfo.Channel (Fin 2 × Fin 2 × Fin 2) (Fin 2 × Fin 2 × Fin 2) FlipPattern

The independent bit-flip channel on the register: each qubit flips independently with probability p; ρ ↦ ∑ₓ w_p(x) Xˣ ρ Xˣ.

Equations

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

theorem CSD.Empirical.QM.QEC.indepFlipChannel_apply (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (ρ : Matrix (Fin 2 × Fin 2 × Fin 2) (Fin 2 × Fin 2 × Fin 2) ℂ) : (indepFlipChannel p hp0 hp1).apply ρ = ∑ x : FlipPattern, ↑(indepWeight p x) • (flipOp x * ρ * flipOp x)

The logical flip, and how each pattern reads to the syndrome

noncomputable def CSD.Empirical.QM.QEC.logicalX : Matrix (Fin 2 × Fin 2 × Fin 2) (Fin 2 × Fin 2 × Fin 2) ℂ

The logical bit-flip X̄ = X ⊗ X ⊗ X, which swaps |000⟩ and |111⟩.

Equations

• CSD.Empirical.QM.QEC.logicalX = CSD.Empirical.QM.QEC.kron3 CSD.Empirical.QM.QEC.pX CSD.Empirical.QM.QEC.pX CSD.Empirical.QM.QEC.pX

theorem CSD.Empirical.QM.QEC.logicalX_mul_self : logicalX * logicalX = 1

theorem CSD.Empirical.QM.QEC.logicalX_conjTranspose : logicalX.conjTranspose = logicalX

theorem CSD.Empirical.QM.QEC.pX_mul_q0 : pX * q0 = q1 * pX

theorem CSD.Empirical.QM.QEC.pX_mul_q1 : pX * q1 = q0 * pX

theorem CSD.Empirical.QM.QEC.logicalX_mul_codeProj : logicalX * codeProj = codeProj * logicalX

The logical flip preserves the code space: X̄ P₀ = P₀ X̄.

theorem CSD.Empirical.QM.QEC.codeProj_mul_logicalX : codeProj * logicalX = logicalX * codeProj

theorem CSD.Empirical.QM.QEC.codeProj_conj_logicalX (ρ : Matrix (Fin 2 × Fin 2 × Fin 2) (Fin 2 × Fin 2 × Fin 2) ℂ) (hρ : codeProj * ρ * codeProj = ρ) : codeProj * (logicalX * ρ * logicalX) * codeProj = logicalX * ρ * logicalX

X̄ ρ X̄ is code-supported when ρ is.

theorem CSD.Empirical.QM.QEC.errorOp_mul_logicalX (k : Fin 4) : errorOp k * logicalX = logicalX * errorOp k

Every single error commutes with the logical flip.

def CSD.Empirical.QM.QEC.flipCount (x : FlipPattern) : ℕ

The number of flipped qubits in a pattern.

Equations

• CSD.Empirical.QM.QEC.flipCount x = ↑x.1 + ↑x.2.1 + ↑x.2.2

def CSD.Empirical.QM.QEC.singleIdx (x : FlipPattern) : Fin 4

The single-error label the syndrome assigns to a pattern: the flipped qubit for weight one, the unflipped qubit for weight two (the code mis-corrects it), 0 for weights zero and three.

Equations

• CSD.Empirical.QM.QEC.singleIdx x = ![![![0, 3], ![2, 1]], ![![1, 2], ![3, 0]]] x.1 x.2.1 x.2.2

theorem CSD.Empirical.QM.QEC.flipOp_eq (x : FlipPattern) : flipOp x = errorOp (singleIdx x) * if flipCount x ≤ 1 then 1 else logicalX

How the syndrome reads a pattern: Xˣ = E_{k(x)} for weight ≤ 1 and Xˣ = E_{k(x)} X̄ for weight ≥ 2.

Recovery, pattern by pattern

theorem CSD.Empirical.QM.QEC.recoveryChannel_apply_errorOp (k : Fin 4) (ρ : Matrix (Fin 2 × Fin 2 × Fin 2) (Fin 2 × Fin 2 × Fin 2) ℂ) (hρ : codeProj * ρ * codeProj = ρ) : recoveryChannel.apply (errorOp k * ρ * errorOp k) = ρ

Recovery undoes any single error on a code-supported operator.

theorem CSD.Empirical.QM.QEC.recoveryChannel_apply_flipOp (x : FlipPattern) (ρ : Matrix (Fin 2 × Fin 2 × Fin 2) (Fin 2 × Fin 2 × Fin 2) ℂ) (hρ : codeProj * ρ * codeProj = ρ) : recoveryChannel.apply (flipOp x * ρ * flipOp x) = if flipCount x ≤ 1 then ρ else logicalX * ρ * logicalX

Recovery on one pattern: the input for weight ≤ 1, the logically flipped input for weight ≥ 2.

The failure probability

noncomputable def CSD.Empirical.QM.QEC.failProb (p : ℝ) : ℝ

The logical failure probability of the three-qubit code under independent flips: 3p² − 2p³, the weight of the patterns with at least two flips.

Equations

• CSD.Empirical.QM.QEC.failProb p = 3 * p ^ 2 - 2 * p ^ 3

theorem CSD.Empirical.QM.QEC.failProb_lt_of_lt_half {p : ℝ} (hp0 : 0 < p) (hp : p < 1 / 2) : failProb p < p

The code helps exactly below p = 1/2: p_fail < p for 0 < p < 1/2.

theorem CSD.Empirical.QM.QEC.recoveryChannel_apply_indepFlipChannel_apply (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (ρ : Matrix (Fin 2 × Fin 2 × Fin 2) (Fin 2 × Fin 2 × Fin 2) ℂ) (hρ : codeProj * ρ * codeProj = ρ) : recoveryChannel.apply ((indepFlipChannel p hp0 hp1).apply ρ) = ↑(1 - failProb p) • ρ + ↑(failProb p) • (logicalX * ρ * logicalX)

★★ Syndrome recovery on independent bit-flip noise, on the code: for every code-supported ρ (P₀ ρ P₀ = ρ), R (N_p ρ) = (1 − p_fail) ρ + p_fail X̄ ρ X̄ with p_fail = 3p² − 2p³ — the recovered state is the input with probability 1 − 3p² + 2p³ and the logically flipped input otherwise.