Prove2Me

§IV, p. 4 — c_kφ = 0 for all k iff φ is a multiple of U|0ⁿ⟩

Proved
DissipativePrep.Unique.dark_jumpOps

by mikedeng1 · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

dark-statesdissipative-state-preparationp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1qubits

Let UU be a unitary on nn qubits, σ−(k)=1⊗⋯⊗∣0⟩k⟨1∣⊗⋯⊗1\sigma_-^{(k)} = \mathbb 1\otimes\dots\otimes|0\rangle_k\langle1|\otimes\dots\otimes\mathbb 1, ck=Uσ−(k)U†c_k = U\sigma_-^{(k)}U^\dagger and ∣Ψ⟩=U∣0n⟩|\Psi\rangle = U|0^n\rangle. For every vector φ\varphi,

ckφ=0 for all k=1,…,n  ⟺  φ=a ∣Ψ⟩ for some a∈C.c_k\varphi = 0 \text{ for all } k = 1,\dots,n \iff \varphi = a\,|\Psi\rangle \text{ for some } a\in\mathbb C.

So ∣Ψ⟩|\Psi\rangle is, up to scalars, the only common dark vector of the jump operators ckc_k; for U=1U = \mathbb 1 this is the statement dk∣φ⟩=0 ∀kd_k|\varphi\rangle = 0\ \forall k iff ∣φ⟩∝∣0n⟩|\varphi\rangle \propto |0^n\rangle.

Formalization Note The page writes "∣φ⟩=U∣0n⟩|\varphi\rangle = U|0^n\rangle"; the statement holds up to a scalar factor, which is what is formalized.

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 dark_jumpOps {n : ℕ} (U : Matrix (Fin (2 ^ n)) (Fin (2 ^ n)) ℂ)
    (hU : U ∈ Matrix.unitaryGroup (Fin (2 ^ n)) ℂ) (φ : EuclideanSpace ℂ (Fin (2 ^ n))) :
    (∀ k, act (jumpOps U k) φ = 0) ↔ ∃ a : ℂ, φ = a • target U := by sorry

end DissipativePrep.Unique
Source
Kraus et al., Preparation of entangled states by quantum Markov processes, arXiv:0803.1463v3, p. 4, §IV ("Defining c_k = U d_k U† we have c_k|φ⟩ = 0 iff |φ⟩ = U|0^n⟩ = |Ψ⟩")
Human review

  • Endorsed by Shuze Chen · Oct 21, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 21, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph