Kraus operator automata and projection-valued measures: examples from Grudka et al.

References:

• Quantum Synchronizing Words: Resetting and Preparing Qutrit States, Grudka et al., 2025

def grudka_Z : Fin 2 → Fin 2 → Matrix (Fin 3) (Fin 3) ℤ

The example Kraus operators from QCNC 2026.

Equations

• grudka_Z = ![![!![0, 0, 0; 1, 0, 0; 0, 0, 0], !![0, 0, 0; 0, 0, -1; 0, 1, 0]], ![!![0, -1, 0; 1, 0, 0; 0, 0, 1], 0]]

def grudka_R₀ {R : Type u_1} [RCLike R] : Fin 2 → Fin 2 → Matrix (Fin 3) (Fin 3) R

Equations

• grudka_R₀ = ![![!![0, 0, 0; 1, 0, 0; 0, 0, 0], !![0, 0, 0; 0, 0, -1; 0, 1, 0]], ![!![0, -1, 0; 1, 0, 0; 0, 0, 1], 0]]

noncomputable def grudka_R (θ : ℝ) : Fin 2 → Fin 2 → Matrix (Fin 3) (Fin 3) ℝ

Equations

• grudka_R θ = ![![!![0, 0, 0; 1, 0, 0; 0, 0, 0], !![0, 0, 0; 0, 0, -1; 0, 1, 0]], ![!![Real.cos θ, -Real.sin θ, 0; Real.sin θ, Real.cos θ, 0; 0, 0, 1], 0]]

noncomputable def grudka_C (θ : ℂ) : Fin 2 → Fin 2 → Matrix (Fin 3) (Fin 3) ℂ

Equations

• grudka_C θ = ![![!![0, 0, 0; 1, 0, 0; 0, 0, 0], !![0, 0, 0; 0, 0, -1; 0, 1, 0]], ![!![Complex.cos θ, -Complex.sin θ, 0; Complex.sin θ, Complex.cos θ, 0; 0, 0, 1], 0]]

theorem grudka_B_QuantumChannel (θ : ℝ) : QuantumChannel (grudka_R θ 1)

1/24/26

theorem grudka_A_QuantumChannel (θ : ℝ) : QuantumChannel (grudka_R θ 0)

theorem grudka_QuantumChannel (θ : ℝ) (i : Fin 2) : QuantumChannel (grudka_R θ i)

noncomputable def grudka_map (θ : ℝ) {n : ℕ} (word : Fin n → Fin 2) : densityMatrix (Fin 3) → densityMatrix (Fin 3)

Grudka et al. map does indeed map density matrices to density matrices.

Equations

• grudka_map θ word = krausApplyWord_map word (grudka_R θ) ⋯

@[implicit_reducible]

noncomputable instance instNormedRingMatrixFinOfNatNatComplex_kraus_2 : NormedRing (Matrix (Fin 2) (Fin 2) ℂ)

Equations

• instNormedRingMatrixFinOfNatNatComplex_kraus_2 = Matrix.frobeniusNormedRing

@[implicit_reducible]

noncomputable instance instNormedAlgebraRealMatrixFinOfNatNatComplex_kraus_2 : NormedAlgebra ℝ (Matrix (Fin 2) (Fin 2) ℂ)

Equations

• instNormedAlgebraRealMatrixFinOfNatNatComplex_kraus_2 = Matrix.frobeniusNormedAlgebra

theorem grudka_helper : Matrix.mulᵣ ![1, 0, 0] (Matrix.transpose ![1, 0, 0]) = !![1, 0, 0; 0, 0, 0; 0, 0, 0]

theorem MO_grudka0_language_nonempty : MOlanguageAcceptedBy 0 ⋯ ≠ ∅

For the Grudka channel with start state 0, the probability of accepting the empty word is 1 > 1/2 hence ![] is in the corresponding measure-once language. This can be generalized to any quantum channel.

theorem grudka_language_nonempty : languageAcceptedBy 0 (grudka_R 0) ≠ ∅

theorem grudka₀_basic_operation : krausApply (grudka_R₀ 0) (pureState e₁) = pureState e₂

theorem grudka_basic_operation : krausApply (grudka_R 0 0) (pureState e₁) = pureState e₂

theorem grudka_basic_operation₂ : krausApply (grudka_R₀ 0) (pureState e₂) = pureState e₃

theorem MO_grudka1_language_nonempty : MOlanguageAcceptedBy 1 ⋯ ≠ ∅