Empirical/QM: the register's single-error channel as a joint unitary with an environment

Category: 3-Local. QM-validity layer (the register-level companion of BitFlipDilation.lean; matrix algebra over the K2 Channel / Stinespring layer, no CSD content).

BitFlipDilation.lean realises the one-qubit bit-flip channel as the environment marginal of a joint unitary on qubit ⊗ qubit. This file does the same for the three-qubit register and its mixed single-error channel singleFlipChannel q (SyndromeRecovery.lean), as the instance e = Fin 4, E = errorOp of the generic controlled-error dilation of ControlledDilation.lean (BACKLOG #52): the environment is a four-level "which-error" register, and

• errorVec q = ∑ₖ √qₖ eₖ is the unit environment vector carrying the error weights;
• errorRotation q is a unitary on the environment with R e₀ = errorVec q, obtained from Matrix.UnitaryGroup.exists_unitary_single_eq (a unitary with a prescribed first column);
• controlledError = blockDiagonal errorOp applies Eₖ to the register when the environment is eₖ — the controlled error, unitary because each Eₖ is;
• registerUnitary q = controlledError · (1 ⊗ R_q), so U_q (ψ ⊗ e₀) = ∑ₖ √qₖ (Eₖ ψ) ⊗ eₖ;
• krausBlock_registerUnitary_embedEnv — the environment blocks of U_q (· ⊗ e₀) are exactly the Kraus operators √qₖ Eₖ, and ★ stinespringChannel_registerUnitary — the single-error channel is the Stinespring channel of U_q with a ready environment, as channels.

Every statement is the generic one specialised (singleFlipChannel_eq_mixedUnitaryChannel is rfl); the names are kept for the consumers (Empirical/CSD/QEC/RegisterFlow.lean reads U_q as a Σ-flow on register ⊗ environment).

Source

Stinespring 1955; Nielsen–Chuang §8.2.3 (environmental models of noise), §10.1 (the three-qubit bit-flip code).

theorem CSD.Empirical.QM.QEC.errorOp_conjTranspose_mul_self (k : Fin 4) : (errorOp k).conjTranspose * errorOp k = 1

Each error Eₖ ∈ {I, X₁, X₂, X₃} is unitary.

The environment side: weights as a unit vector, and a unitary reaching it

noncomputable def CSD.Empirical.QM.QEC.errorVec (q : Fin 4 → ℝ) : EuclideanSpace ℂ (Fin 4)

The environment amplitude vector ∑ₖ √qₖ eₖ.

Equations

• CSD.Empirical.QM.QEC.errorVec q = CSD.Empirical.QM.QEC.weightVec q

@[simp]

theorem CSD.Empirical.QM.QEC.errorVec_apply (q : Fin 4 → ℝ) (k : Fin 4) : (errorVec q).ofLp k = ↑√(q k)

theorem CSD.Empirical.QM.QEC.norm_errorVec (q : Fin 4 → ℝ) (hq0 : ∀ (k : Fin 4), 0 ≤ q k) (hq1 : ∑ k : Fin 4, q k = 1) : ‖errorVec q‖ = 1

noncomputable def CSD.Empirical.QM.QEC.errorRotation (q : Fin 4 → ℝ) (hq0 : ∀ (k : Fin 4), 0 ≤ q k) (hq1 : ∑ k : Fin 4, q k = 1) : Matrix (Fin 4) (Fin 4) ℂ

A unitary on the environment taking the ready vector e₀ to errorVec q.

Equations

• CSD.Empirical.QM.QEC.errorRotation q hq0 hq1 = CSD.Empirical.QM.QEC.weightRotation q hq0 hq1 0

theorem CSD.Empirical.QM.QEC.errorRotation_apply_single (q : Fin 4 → ℝ) (hq0 : ∀ (k : Fin 4), 0 ≤ q k) (hq1 : ∑ k : Fin 4, q k = 1) : (Matrix.toEuclideanLin (errorRotation q hq0 hq1)) (EuclideanSpace.single 0 1) = errorVec q

theorem CSD.Empirical.QM.QEC.errorRotation_conjTranspose_mul (q : Fin 4 → ℝ) (hq0 : ∀ (k : Fin 4), 0 ≤ q k) (hq1 : ∑ k : Fin 4, q k = 1) : (errorRotation q hq0 hq1).conjTranspose * errorRotation q hq0 hq1 = 1

theorem CSD.Empirical.QM.QEC.errorRotation_apply_zero (q : Fin 4 → ℝ) (hq0 : ∀ (k : Fin 4), 0 ≤ q k) (hq1 : ∑ k : Fin 4, q k = 1) (l : Fin 4) : errorRotation q hq0 hq1 l 0 = ↑√(q l)

The first column of the rotation is the weight vector: R l 0 = √qₗ.

The controlled error and the joint unitary

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

The controlled error: apply Eₖ to the register when the environment is eₖ. Index (register, environment).

Equations

• CSD.Empirical.QM.QEC.controlledError = Matrix.blockDiagonal CSD.Empirical.QM.QEC.errorOp

theorem CSD.Empirical.QM.QEC.controlledError_conjTranspose_mul : controlledError.conjTranspose * controlledError = 1

noncomputable def CSD.Empirical.QM.QEC.registerUnitary (q : Fin 4 → ℝ) (hq0 : ∀ (k : Fin 4), 0 ≤ q k) (hq1 : ∑ k : Fin 4, q k = 1) : Matrix ((Fin 2 × Fin 2 × Fin 2) × Fin 4) ((Fin 2 × Fin 2 × Fin 2) × Fin 4) ℂ

The register's joint unitary U_q = controlledError · (1 ⊗ R_q): rotate the environment into the weight vector, then apply the error the environment names. U_q (ψ ⊗ e₀) = ∑ₖ √qₖ (Eₖ ψ) ⊗ eₖ.

Equations

• CSD.Empirical.QM.QEC.registerUnitary q hq0 hq1 = CSD.Empirical.QM.QEC.controlledUnitary CSD.Empirical.QM.QEC.errorOp q hq0 hq1 0

theorem CSD.Empirical.QM.QEC.registerUnitary_eq (q : Fin 4 → ℝ) (hq0 : ∀ (k : Fin 4), 0 ≤ q k) (hq1 : ∑ k : Fin 4, q k = 1) : registerUnitary q hq0 hq1 = controlledError * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 (errorRotation q hq0 hq1)

theorem CSD.Empirical.QM.QEC.registerUnitary_conjTranspose_mul (q : Fin 4 → ℝ) (hq0 : ∀ (k : Fin 4), 0 ≤ q k) (hq1 : ∑ k : Fin 4, q k = 1) : (registerUnitary q hq0 hq1).conjTranspose * registerUnitary q hq0 hq1 = 1

theorem CSD.Empirical.QM.QEC.krausBlock_registerUnitary_embedEnv (q : Fin 4 → ℝ) (hq0 : ∀ (k : Fin 4), 0 ≤ q k) (hq1 : ∑ k : Fin 4, q k = 1) (k : Fin 4) : QuantumInfo.krausBlock (registerUnitary q hq0 hq1 * LF2.embedEnv (Fin 2 × Fin 2 × Fin 2) (EuclideanSpace.single 0 1)) k = ↑√(q k) • errorOp k

The environment blocks of U_q (· ⊗ e₀) are the Kraus operators √qₖ Eₖ of the single-error channel.

theorem CSD.Empirical.QM.QEC.singleFlipChannel_eq_mixedUnitaryChannel (q : Fin 4 → ℝ) (hq0 : ∀ (k : Fin 4), 0 ≤ q k) (hq1 : ∑ k : Fin 4, q k = 1) : singleFlipChannel q hq0 hq1 = QuantumInfo.Channel.mixedUnitaryChannel errorOp errorOp_conjTranspose_mul_self q hq0 hq1

The single-error channel is the mixed-unitary channel (CanonicalChannels.lean) of the error family.

theorem CSD.Empirical.QM.QEC.stinespringChannel_registerUnitary (q : Fin 4 → ℝ) (hq0 : ∀ (k : Fin 4), 0 ≤ q k) (hq1 : ∑ k : Fin 4, q k = 1) : LF2.stinespringChannel (registerUnitary q hq0 hq1) ⋯ (EuclideanSpace.single 0 1) stinespringChannel_registerUnitary._proof_1 = singleFlipChannel q hq0 hq1

★ The single-error channel is the Stinespring channel of U_q with a ready environment, as channels (equal Kraus families).