Empirical/QM: the controlled-error dilation of a mixed-unitary channel

Category: 3-Local. QM-validity layer (matrix algebra over the K2 Channel / Stinespring layer; no CSD content). BACKLOG #52, the generic half that #53 also needs.

A mixed-unitary channel ρ ↦ ∑ₖ qₖ Eₖ ρ Eₖᴴ (unitary errors Eₖ with weights qₖ ≥ 0, ∑ qₖ = 1) is the environment marginal of one joint unitary on system ⊗ environment, the environment being the finite set of error labels:

• weightVec q = ∑ₖ √qₖ eₖ is the unit environment vector carrying the weights, and weightRotation q e₀ a unitary on the environment with R e₀ = weightVec q (Matrix.UnitaryGroup.exists_unitary_single_eq);
• blockDiagonal E is the controlled error — apply Eₖ when the environment reads eₖ — unitary because each Eₖ is (blockDiagonal_conjTranspose_mul);
• controlledUnitary E q e₀ = blockDiagonal E · (1 ⊗ R), so U (ψ ⊗ e₀) = ∑ₖ √qₖ (Eₖ ψ) ⊗ eₖ (controlledUnitary_conjTranspose_mul);
• ★ stinespringChannel_controlledUnitary — the mixed-unitary channel Channel.mixedUnitaryChannel E q (Kraus operators √qₖ Eₖ, CanonicalChannels.lean) is the Stinespring channel of the controlled unitary with the environment ready in e₀, as channels (krausBlock_controlledUnitary_embedEnv).

RegisterDilation.lean is the instance e = Fin 4, E = errorOp (the three-qubit single-error channel); IndependentNoise.lean is the instance e = Fin 2 × Fin 2 × Fin 2, E = flipOp (independent bit-flips); the Steane instance is Empirical/CSD/QEC/SteaneFlow.lean (BACKLOG #53, 2026-09-27).

Source

Stinespring 1955; Nielsen–Chuang §8.2.3 (environmental models of noise).

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

noncomputable def CSD.Empirical.QM.QEC.weightVec {e : Type u_2} (q : e → ℝ) : EuclideanSpace ℂ e

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

Equations

• CSD.Empirical.QM.QEC.weightVec q = WithLp.toLp 2 fun (k : e) => ↑√(q k)

@[simp]

theorem CSD.Empirical.QM.QEC.weightVec_apply {e : Type u_2} (q : e → ℝ) (k : e) : (weightVec q).ofLp k = ↑√(q k)

theorem CSD.Empirical.QM.QEC.norm_weightVec {e : Type u_2} [Fintype e] (q : e → ℝ) (hq0 : ∀ (k : e), 0 ≤ q k) (hq1 : ∑ k : e, q k = 1) : ‖weightVec q‖ = 1

noncomputable def CSD.Empirical.QM.QEC.weightRotation {e : Type u_2} [Fintype e] [DecidableEq e] (q : e → ℝ) (hq0 : ∀ (k : e), 0 ≤ q k) (hq1 : ∑ k : e, q k = 1) (e₀ : e) : Matrix e e ℂ

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

Equations

• CSD.Empirical.QM.QEC.weightRotation q hq0 hq1 e₀ = ↑(Classical.choose ⋯)

theorem CSD.Empirical.QM.QEC.weightRotation_apply_single {e : Type u_2} [Fintype e] [DecidableEq e] (q : e → ℝ) (hq0 : ∀ (k : e), 0 ≤ q k) (hq1 : ∑ k : e, q k = 1) (e₀ : e) : (Matrix.toEuclideanLin (weightRotation q hq0 hq1 e₀)) (EuclideanSpace.single e₀ 1) = weightVec q

theorem CSD.Empirical.QM.QEC.weightRotation_conjTranspose_mul {e : Type u_2} [Fintype e] [DecidableEq e] (q : e → ℝ) (hq0 : ∀ (k : e), 0 ≤ q k) (hq1 : ∑ k : e, q k = 1) (e₀ : e) : (weightRotation q hq0 hq1 e₀).conjTranspose * weightRotation q hq0 hq1 e₀ = 1

theorem CSD.Empirical.QM.QEC.weightRotation_apply_ready {e : Type u_2} [Fintype e] [DecidableEq e] (q : e → ℝ) (hq0 : ∀ (k : e), 0 ≤ q k) (hq1 : ∑ k : e, q k = 1) (e₀ l : e) : weightRotation q hq0 hq1 e₀ l e₀ = ↑√(q l)

The ready column of the rotation is the weight vector: R l e₀ = √qₗ.

The controlled error and the joint unitary

theorem CSD.Empirical.QM.QEC.blockDiagonal_conjTranspose_mul {n : Type u_1} {e : Type u_2} [Fintype n] [Fintype e] [DecidableEq n] [DecidableEq e] (E : e → Matrix n n ℂ) (hE : ∀ (k : e), (E k).conjTranspose * E k = 1) : (Matrix.blockDiagonal E).conjTranspose * Matrix.blockDiagonal E = 1

The controlled error ⊕ₖ Eₖ is unitary when every Eₖ is.

noncomputable def CSD.Empirical.QM.QEC.controlledUnitary {n : Type u_1} {e : Type u_2} [Fintype n] [Fintype e] [DecidableEq n] [DecidableEq e] (E : e → Matrix n n ℂ) (q : e → ℝ) (hq0 : ∀ (k : e), 0 ≤ q k) (hq1 : ∑ k : e, q k = 1) (e₀ : e) : Matrix (n × e) (n × e) ℂ

The controlled unitary U = (⊕ₖ Eₖ) · (1 ⊗ R_q): rotate the environment into the weight vector, then apply the error the environment names. U (ψ ⊗ e₀) = ∑ₖ √qₖ (Eₖ ψ) ⊗ eₖ. Index (system, environment).

Equations

• CSD.Empirical.QM.QEC.controlledUnitary E q hq0 hq1 e₀ = Matrix.blockDiagonal E * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 (CSD.Empirical.QM.QEC.weightRotation q hq0 hq1 e₀)

theorem CSD.Empirical.QM.QEC.controlledUnitary_conjTranspose_mul {n : Type u_1} {e : Type u_2} [Fintype n] [Fintype e] [DecidableEq n] [DecidableEq e] (E : e → Matrix n n ℂ) (hE : ∀ (k : e), (E k).conjTranspose * E k = 1) (q : e → ℝ) (hq0 : ∀ (k : e), 0 ≤ q k) (hq1 : ∑ k : e, q k = 1) (e₀ : e) : (controlledUnitary E q hq0 hq1 e₀).conjTranspose * controlledUnitary E q hq0 hq1 e₀ = 1

The Stinespring identification

theorem CSD.Empirical.QM.QEC.kronecker_one_mul_embedEnv {n : Type u_1} {e : Type u_2} [Fintype n] [Fintype e] [DecidableEq n] [DecidableEq e] (R : Matrix e e ℂ) (e₀ : EuclideanSpace ℂ e) : Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 R * LF2.embedEnv n e₀ = LF2.embedEnv n ((Matrix.toEuclideanLin R) e₀)

Rotating the environment of a ready embedding: (1 ⊗ R) (ψ ⊗ e₀) = ψ ⊗ (R e₀).

theorem CSD.Empirical.QM.QEC.krausBlock_blockDiagonal_mul_embedEnv {n : Type u_1} {e : Type u_2} [Fintype n] [Fintype e] [DecidableEq n] [DecidableEq e] (E : e → Matrix n n ℂ) (v : EuclideanSpace ℂ e) (k : e) : QuantumInfo.krausBlock (Matrix.blockDiagonal E * LF2.embedEnv n v) k = v.ofLp k • E k

The environment blocks of a controlled error with environment vector v: Eₖ weighted by v k.

theorem CSD.Empirical.QM.QEC.krausBlock_controlledUnitary_embedEnv {n : Type u_1} {e : Type u_2} [Fintype n] [Fintype e] [DecidableEq n] [DecidableEq e] (E : e → Matrix n n ℂ) (q : e → ℝ) (hq0 : ∀ (k : e), 0 ≤ q k) (hq1 : ∑ k : e, q k = 1) (e₀ k : e) : QuantumInfo.krausBlock (controlledUnitary E q hq0 hq1 e₀ * LF2.embedEnv n (EuclideanSpace.single e₀ 1)) k = ↑√(q k) • E k

The environment blocks of U (· ⊗ e₀) are the Kraus operators √qₖ Eₖ.

theorem CSD.Empirical.QM.QEC.stinespringChannel_controlledUnitary {n : Type u_1} {e : Type u_2} [Fintype n] [Fintype e] [DecidableEq n] [DecidableEq e] (E : e → Matrix n n ℂ) (hE : ∀ (k : e), (E k).conjTranspose * E k = 1) (q : e → ℝ) (hq0 : ∀ (k : e), 0 ≤ q k) (hq1 : ∑ k : e, q k = 1) (e₀ : e) : LF2.stinespringChannel (controlledUnitary E q hq0 hq1 e₀) ⋯ (EuclideanSpace.single e₀ 1) ⋯ = QuantumInfo.Channel.mixedUnitaryChannel E hE q hq0 hq1

★ The mixed-unitary channel is the Stinespring channel of the controlled unitary with a ready environment, as channels (equal Kraus families).