§IV, p. 4 — for χ ⊥ |0ⁿ⟩ some monomial P of the σ_-^{(k)} has ⟨0ⁿ|P|χ⟩ ≠ 0
ProvedDissipativePrep.Unique.monomialdissipative-state-preparationp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1qubits
Let , , be the qubit lowering operators. For every nonzero vector orthogonal to there is a finite word (a monomial of the jump operators) such that
This is the property that rules out a nonzero subspace invariant under all and orthogonal to , and hence (via Theorem 2) shows that is the unique stationary state of .
Formalization Note "" is a state, so is assumed (the zero vector is orthogonal to everything). The empty word is the identity.
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 monomial {n : ℕ} (χ : EuclideanSpace ℂ (Fin (2 ^ n))) (hχ : χ ≠ 0)
(horth : inner ℂ (ket (0 : Fin (2 ^ n))) χ = 0) :
∃ w : List (Fin n), inner ℂ (ket (0 : Fin (2 ^ n))) (act (w.map lower).prod χ) ≠ 0 := by sorry
end DissipativePrep.Unique
Source
Kraus et al., Preparation of entangled states by quantum Markov processes, arXiv:0803.1463v3, p. 4, §IV ("Furthermore, it is straightforward to show …")
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.