Empirical/QM/QEC: the bit-flip error channel

Category: 3-Local.

The honest error model behind the three-qubit bit-flip code (ThreeQubit.lean): a single-qubit error is not a coherent rotation but a CPTP channel — decoherence from interaction with the environment. The canonical bit-flip channel is

Φ(ρ) = (1 − p) ρ + p · X ρ X,

a mixedUnitaryChannel with Kraus operators {√(1−p) · I, √p · X} (channels phase C4 of specs/channels-plan.md). With probability p the qubit suffers an X (bit-flip) error; with probability 1 − p it is left alone.

This is the "error = decoherence" statement made precise: the error is the environment-averaged image of the joint system-environment flow (the channel's Stinespring dilation, QuantumInfo.Channel.stinespringIsom). The correction — syndrome measurement and recovery — is the discrete X₁/X₂/X₃ recovery of ThreeQubit.lean; closing the loop to a measurement-conditioned update is LF5 work.

@[simp]

theorem CSD.Empirical.QM.QEC.pX_conjTranspose : pX.conjTranspose = pX

The Pauli X is self-adjoint.

theorem CSD.Empirical.QM.QEC.pX_unitary : pX.conjTranspose * pX = 1

The Pauli X is unitary: Xᴴ X = 1.

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

The single-qubit bit-flip channel Φ(ρ) = (1−p) ρ + p · X ρ X, the canonical decoherence / error model for a qubit: a mixedUnitaryChannel over {I, X} with probabilities {1−p, p} (Kraus {√(1−p) I, √p X}).

Equations

• CSD.Empirical.QM.QEC.bitFlipChannel p hp0 hp1 = QuantumInfo.Channel.mixedUnitaryChannel ![1, CSD.Empirical.QM.QEC.pX] CSD.Empirical.QM.QEC.bitFlipChannel._proof_1 ![1 - p, p] ⋯ ⋯

theorem CSD.Empirical.QM.QEC.bitFlipChannel_apply (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (ρ : Matrix (Fin 2) (Fin 2) ℂ) : (bitFlipChannel p hp0 hp1).apply ρ = ↑(1 - p) • ρ + ↑p • (pX * ρ * pX)

The bit-flip channel acts as advertised: Φ(ρ) = (1−p) ρ + p · X ρ X. The decoherence reading of a single-qubit error.