Empirical/QM: syndrome-conditioned recovery as one channel #

Category: 3-Local. QM-validity layer (matrix algebra over the K2 Channel layer, no CSD content); companion of ThreeQubit.lean and BitFlipChannel.lean.

ThreeQubit.lean proves the bit-flip code corrects each single error branch by branch: the syndrome identifies Xⱼ, and Xⱼ undoes it. The operational statement of error correction is stronger: a single CPTP map — measure the syndrome, then apply the correction the outcome names — returns every code state, mixed or pure, from the mixed post-error state. This file builds that channel and proves it.

codeProj — the projector onto the codespace span{|000⟩, |111⟩}, as |000⟩⟨000| + |111⟩⟨111| (kron3 of the qubit projectors q0, q1; the kron3 linearity of ErrorDiscretization.lean);
errorOp — the four errors {I, X₁, X₂, X₃}; syndromeProj k = Eₖ P₀ Eₖ — the projector onto the k-th error subspace Eₖ · C. ★ syndromeProj_mul_syndromeProj (the four are pairwise orthogonal projectors) and ★ sum_syndromeProj (they sum to 1): the syndrome is a projective measurement on the register;
syndromeProj_errorOp_logical, syndromeProj_errorOp_logical_of_ne — the errored codeword Eₖ ψ_L lies in the k-th syndrome subspace and in no other;
recoveryChannel — the syndrome-conditioned recovery, a Channel with Kraus operators Eₖ Pₖ ("if the syndrome is k, apply Eₖ"); trace preservation is ∑ₖ Pₖ = 1;
singleFlipChannel q — the mixed single-error channel ρ ↦ ∑ₖ qₖ Eₖ ρ Eₖ for any weights qₖ ≥ 0, ∑ qₖ = 1 (the discretised error, all four branches at once);
★★ recoveryChannel_apply_singleFlipChannel_apply — recovery is exact on the code, as one channel on the mixed state: for every operator ρ supported on the codespace (P₀ ρ P₀ = ρ, in particular every mixed code state), R (N_q ρ) = ρ; and comp_recoveryChannel_singleFlipChannel_apply, the same for the composite channel R ∘ N_q of ChannelComp.lean.

The proof is the Knill–Laflamme mechanism in its simplest instance: Pⱼ Eₖ P₀ = δⱼₖ Pₖ Eₖ (the error Eₖ carries the code onto the k-th syndrome subspace and nowhere else), so the double Kraus sum collapses to its diagonal, and on the diagonal Eₖ Pₖ Eₖ = P₀.

What is not here: errors outside the single-flip set (two flips are miscorrected — the code's distance is 3). The independent-noise channel (bit-flip_p)^{⊗3}, whose double- and triple-flip branches the code mis-corrects into the logical flip, is IndependentNoise.lean (recoveryChannel_apply_indepFlipChannel_apply: the 3p² − 2p³ residual); singleFlipChannel is its correctable part with free weights.

Source #

Shor 1995, Phys. Rev. A 52, R2493; Knill–Laflamme 1997, Phys. Rev. A 55, 900 (the correction conditions; the recovery channel ∑ₖ Eₖ Pₖ · Pₖ Eₖᴴ).

Empirical/QM: syndrome-conditioned recovery as one channel #

Source #

The qubit projectors, the code projector, the errors #

The syndrome projectors: a projective measurement on the register #

The errored codewords lie in their syndrome subspaces #

The recovery channel and the single-error channel #

The Knill–Laflamme collapse #