Empirical/QM/QEC: the bit-flip channel as the environment marginal of a joint unitary

Category: 3-Local (QM-validity companion of BitFlipChannel.lean).

The bit-flip channel Φ(ρ) = (1 − p) ρ + p X ρ X has a concrete Stinespring dilation: the joint unitary U_p = CX · (I ⊗ R_p) on system ⊗ environment (an environment qubit rotated by R_p |0⟩ = √(1−p) |0⟩ + √p |1⟩, then a flip of the system controlled by the environment), with the environment ready in |0⟩:

`U_p (ψ ⊗ |0⟩) = √(1−p) ψ ⊗ |0⟩ + √p (Xψ) ⊗ |1⟩`.

• flipRotation, controlledFlip, bitFlipUnitary — the pieces and U_p; bitFlipUnitary_conjTranspose_mul — unitarity;
• krausBlock_bitFlipUnitary_embedEnv — the environment blocks of U_p · (· ⊗ |0⟩) are exactly the bit-flip Kraus operators {√(1−p) I, √p X};
• ★ stinespringChannel_bitFlipUnitary — the bit-flip channel IS the Stinespring channel of U_p with a ready environment, as channels (equal Kraus families).

Consumer: Empirical/CSD/QEC/ThreeQubit.lean, where U_p lifted to a Σ-flow produces the bit-flip channel on the density operators of preparations (W11 of specs/qit-chain-scoping.md).

The bit-flip channel as the environment marginal of a joint unitary

noncomputable def CSD.Empirical.QM.QEC.flipRotation (p : ℝ) : Matrix (Fin 2) (Fin 2) ℂ

The real rotation R_p with R_p |0⟩ = √(1−p) |0⟩ + √p |1⟩ on the environment qubit.

Equations

• CSD.Empirical.QM.QEC.flipRotation p = !![↑√(1 - p), -↑√p; ↑√p, ↑√(1 - p)]

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

The controlled flip CX with the environment as control: applies X to the system when the environment is |1⟩. Index (system, environment).

Equations

• CSD.Empirical.QM.QEC.controlledFlip = Matrix.of fun (q r : Fin 2 × Fin 2) => if q.2 = r.2 then if q.2 = 1 then CSD.Empirical.QM.QEC.pX q.1 r.1 else 1 q.1 r.1 else 0

noncomputable def CSD.Empirical.QM.QEC.bitFlipUnitary (p : ℝ) : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ

The bit-flip joint unitary U_p = CX · (I ⊗ R_p): rotate the environment, then flip the system conditioned on it. U_p (ψ ⊗ |0⟩) = √(1−p) ψ ⊗ |0⟩ + √p (Xψ) ⊗ |1⟩.

Equations

• CSD.Empirical.QM.QEC.bitFlipUnitary p = CSD.Empirical.QM.QEC.controlledFlip * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 (CSD.Empirical.QM.QEC.flipRotation p)

theorem CSD.Empirical.QM.QEC.flipRotation_conjTranspose_mul (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) : (flipRotation p).conjTranspose * flipRotation p = 1

theorem CSD.Empirical.QM.QEC.controlledFlip_conjTranspose_mul : controlledFlip.conjTranspose * controlledFlip = 1

theorem CSD.Empirical.QM.QEC.bitFlipUnitary_conjTranspose_mul (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) : (bitFlipUnitary p).conjTranspose * bitFlipUnitary p = 1

U_p is unitary.

theorem CSD.Empirical.QM.QEC.krausBlock_bitFlipUnitary_embedEnv (p : ℝ) (i : Fin 2) : QuantumInfo.krausBlock (bitFlipUnitary p * LF2.embedEnv (Fin 2) (EuclideanSpace.single 0 1)) i = ↑√(![1 - p, p] i) • ![1, pX] i

The environment blocks of U_p · (· ⊗ |0⟩) are the bit-flip Kraus operators {√(1−p) I, √p X}.

theorem CSD.Empirical.QM.QEC.stinespringChannel_bitFlipUnitary (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) : LF2.stinespringChannel (bitFlipUnitary p) ⋯ (EuclideanSpace.single 0 1) stinespringChannel_bitFlipUnitary._proof_1 = bitFlipChannel p hp0 hp1

★ The bit-flip channel is the Stinespring channel of U_p with a ready environment, as channels (equal Kraus families).