§IV.A, p. 4 — one qubit: eigenvalues 0, −2g, −g, −g of L_{σ₋} on |0⟩⟨0|, σ_z, σ_x, σ_y
ProvedDissipativePrep.Unique.one_qubit_spectrumamplitude-dampingdissipative-state-preparationliouvillian-spectrump2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1
Consider a single qubit with Hamiltonian and one jump operator with rate , so that . Then
where , , (basis order ).
These four eigenvectors form a basis of the matrices, so they give the full spectrum , , of the single-qubit Liouvillian; the -qubit spectrum is built from them.
Formalization Note The page says " iff "; read literally the "iff" is false (e.g. is an eigenvector outside ), so the four eigen-equations are stated.
Preamble
import Mathlib import Definitions.Def_DissipativePrep_Unique_Model open scoped Matrix ComplexConjugate open QAlgorithms QAlgorithms.Papers.Independent.Dependency50.P16
Formal statement
namespace DissipativePrep.Unique
theorem one_qubit_spectrum (g : ℝ) (hg : 0 < g) :
let G := gkslGenerator (krausData (0 : Matrix (Fin 2) (Fin 2) ℂ) Matrix.isHermitian_zero
![!![0, 1; 0, 0]] ![g])
G !![1, 0; 0, 0] = 0 ∧
G !![1, 0; 0, -1] = ((-2 * g : ℝ) : ℂ) • !![1, 0; 0, -1] ∧
G !![0, 1; 1, 0] = ((-g : ℝ) : ℂ) • !![0, 1; 1, 0] ∧
G !![0, -Complex.I; Complex.I, 0] = ((-g : ℝ) : ℂ) • !![0, -Complex.I; Complex.I, 0] := by sorry
end DissipativePrep.Unique
Source
Kraus et al., Preparation of entangled states by quantum Markov processes, arXiv:0803.1463v3, p. 4, §IV.A ("We find L_{σ_-^{(k)}}(σ_i^{(k)}) = λ_iσ_i^{(k)} …")
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.