Proposition 1: necessary and sufficient identifiability condition

Open

QAlgorithms.Papers.Independent.Intakethird100.P67.proposition1_identifiability

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $S=\{\rho_k\}_{k=1}^K$ , $K\ge1$ , be density operators in a finite-dimensional complex system. Let $H_{\rm in}$ be the span of their supports and $\Pi$ its orthogonal projector. The complex algebra generated by the samples is understood as the span of nonempty products, whose supported identity is $\Pi$ . Then

\operatorname{Alg}_{\mathbb C}(S)=\mathcal L(H_{\rm in})

if and only if every pair of ambient unitaries $U,V$ with $U\rho_kU^\dagger=V\rho_kV^\dagger$ for all $k$ also has $U\rho U^\dagger=V\rho V^\dagger$ for every density operator $\rho$ supported on $H_{\rm in}$ . Thus the records determine the supported unitary action up to a global phase. The statement uses density outputs rather than arbitrary choices of vector phases.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P67

Formal statement

noncomputable section

open scoped ComplexConjugate Matrix Matrix.Norms.L2Operator

attribute [local instance] Classical.propDecidable

open MeasureTheory Filter

namespace QAlgorithms.Papers.Independent.Intakethird100.P67

variable {I J K L A : Type*} [Fintype I] [DecidableEq I]
  [Fintype J] [DecidableEq J] [Fintype K] [DecidableEq K]
  [Fintype L] [DecidableEq L] [Fintype A] [DecidableEq A]

/-- PDF pp.2–3, Proposition 1: equality of sample density outputs identifies precisely
unitary conjugation on every supported state, iff the supported algebra is full. -/
theorem proposition1_identifiability [Nonempty K] (S : K → Matrix I I ℂ)
    (hS : ∀ k, IsDensityMatrix (S k)) :
    Generates S ↔ ∀ U V : Matrix.unitaryGroup I ℂ,
      (∀ k, densityConjugation (U : Matrix I I ℂ) (S k) = densityConjugation (V : Matrix I I ℂ) (S k)) →
      ∀ rho : Matrix I I ℂ, IsDensityMatrix rho → InSampleSupport S rho →
        densityConjugation (U : Matrix I I ℂ) rho = densityConjugation (V : Matrix I I ℂ) rho := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P67

end

Source

Universal Quantum Emulator, arXiv:1606.02734v2, PDF p. 2, Proposition 1: necessary and sufficient identifiability condition

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

Let $I$ be a finite coordinate type with decidable equality, let $K$ be a finite nonempty sample index type, and let $S_k$ be positive semidefinite complex matrices on $I$ , each with trace $1$ . Define

\Pi=f\!\left(\sum_{k\in K}S_k\right), \qquad f(t)=\begin{cases}0,&t=0,\\1,&t\ne0,\end{cases}

using the real continuous functional calculus, and let $\mathcal A$ be the complex linear span of all products $S_{k_1}\cdots S_{k_r}$ with $r\ge1$ , allowing repeated indices. Then the condition

\forall X,\qquad X\in\mathcal A\ \Longleftrightarrow\ \Pi X\Pi=X

holds if and only if the following statement holds: for every pair of unitary matrices $U,V$ on $I$ , if $US_kU^\dagger=VS_kV^\dagger$ for every $k$ , then $U\rho U^\dagger=V\rho V^\dagger$ for every positive semidefinite trace-one matrix $\rho$ satisfying $\Pi\rho\Pi=\rho$ . The products defining $\mathcal A$ exclude the empty product. The hypotheses on the nonempty family of trace-one matrices cannot be satisfied when $I$ is empty.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph