Definitions for Extremal Quantum States in Coupled Systems

Definition

QAlgorithms_Papers_Independent_Intakethird100_P12

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

prove2quantum

The objects the formalized statements of Extremal Quantum States in Coupled Systems (arXiv:quant-ph/0307182) are stated in. Each was checked against the paper by a blind read-back and a moderator.

finiteCouplingSet: PDF p.5: ALL normalized PSD joint operators with the specified partial traces.
flatMatrix: PDF pp.4–5: lexicographic coordinates, second index varying fastest.
rankSplitEquiv: PDF p.3: concatenate the leading k and trailing n-k coordinates. The guard makes subtraction exact, including k=0 and k=n.
permuteMatrix: PDF pp.3,5: sigma M sigma^{-1}, where sigma sends |p(i)> to |i>. Thus inverse conjugation is obtained by replacing p with p.symm.
rankBlockMatrix: PDF p.3, (2.1): block completion, with no positivity assumption on its argument.
rankRow: PDF p.6: R=[I_k|A] in the same flattened rank coordinates.
physicalPerturbation: PDF p.5, (2.10): undo sigma, then restore physical tensor coordinates BEFORE taking either partial trace.
NoZeroMarginalPerturbation: PDF pp.5–7: no nonzero Hermitian perturbation with BOTH marginals zero.
compressedLocalSpace: PDF pp.6,8: image of the REAL Hermitian local-sum space; no complex span. Printed: column [I;A^t]. Changed: R.conjTranspose=[I;A†]. Why: preceding trace identity (2.11), PDF p.6, has A†; PDF p.11 expands this as AXA†. The correction remains subject to independent moderation.
omegaFromBasis: PDF p.9, Theorem 3.1: construct Omega from an actual complex orthonormal basis.

Definition code

import Mathlib
import Definitions.Def_QAlgorithms_Defs_Information
import Definitions.Def_QAlgorithms_Defs_Measurement

/-!
K. R. Parthasarathy, Extremal Quantum States in Coupled Systems, quant-ph/0307182v1.
All page references are PDF pages. Coordinates are relative to arbitrary chosen
subsystem orthonormal bases. Product indexing j+d2*i is lexicographic.
-/

namespace QAlgorithms.Papers.Independent.Intakethird100.P12

open scoped ComplexConjugate ComplexOrder

/-- PDF p.5: ALL normalized PSD joint operators with the specified partial traces. -/
def finiteCouplingSet {d1 d2 : ℕ} (rho1 : Matrix (Fin d1) (Fin d1) ℂ)
    (rho2 : Matrix (Fin d2) (Fin d2) ℂ) :
    Set (Matrix (Fin d1 × Fin d2) (Fin d1 × Fin d2) ℂ) :=
  {rho | IsDensityMatrix rho ∧ traceRight rho = rho1 ∧ traceLeft rho = rho2}

/-- PDF pp.4–5: lexicographic coordinates, second index varying fastest. -/
def flatMatrix {d1 d2 : ℕ} (M : Matrix (Fin d1 × Fin d2) (Fin d1 × Fin d2) ℂ) :
    Matrix (Fin (d1*d2)) (Fin (d1*d2)) ℂ :=
  M.submatrix finProdFinEquiv.symm finProdFinEquiv.symm

/-- PDF p.3: concatenate the leading k and trailing n-k coordinates.
The guard makes subtraction exact, including k=0 and k=n. -/
def rankSplitEquiv {n k : ℕ} (h : k ≤ n) : (Fin k ⊕ Fin (n-k)) ≃ Fin n :=
  finSumFinEquiv.trans (finCongr (by omega))

/-- PDF pp.3,5: sigma M sigma^{-1}, where sigma sends |p(i)> to |i>.
Thus inverse conjugation is obtained by replacing p with p.symm. -/
def permuteMatrix {n : ℕ} (p : Equiv.Perm (Fin n))
    (M : Matrix (Fin n) (Fin n) ℂ) : Matrix (Fin n) (Fin n) ℂ :=
  M.submatrix p p

/-- PDF p.3, (2.1): block completion, with no positivity assumption on its argument. -/
def rankBlockMatrix {n k : ℕ} (h : k ≤ n) (K : Matrix (Fin k) (Fin k) ℂ)
    (A : Matrix (Fin k) (Fin (n-k)) ℂ) : Matrix (Fin n) (Fin n) ℂ :=
  (Matrix.fromBlocks K (K*A) (A.conjTranspose*K)
    (A.conjTranspose*K*A)).submatrix (rankSplitEquiv h).symm (rankSplitEquiv h).symm

/-- PDF p.6: R=[I_k|A] in the same flattened rank coordinates. -/
def rankRow {n k : ℕ} (h : k ≤ n) (A : Matrix (Fin k) (Fin (n-k)) ℂ) :
    Matrix (Fin k) (Fin n) ℂ :=
  fun i j => match (rankSplitEquiv h).symm j with
    | Sum.inl l => if i = l then 1 else 0
    | Sum.inr l => A i l

/-- PDF p.5, (2.10): undo sigma, then restore physical tensor coordinates
BEFORE taking either partial trace. -/
def physicalPerturbation {d1 d2 k : ℕ} (h : k ≤ d1*d2)
    (p : Equiv.Perm (Fin (d1*d2)))
    (A : Matrix (Fin k) (Fin (d1*d2-k)) ℂ) (L : Matrix (Fin k) (Fin k) ℂ) :
    Matrix (Fin d1 × Fin d2) (Fin d1 × Fin d2) ℂ :=
  (permuteMatrix p.symm (rankBlockMatrix h L A)).submatrix finProdFinEquiv finProdFinEquiv

/-- PDF pp.5–7: no nonzero Hermitian perturbation with BOTH marginals zero. -/
def NoZeroMarginalPerturbation {d1 d2 k : ℕ} (h : k ≤ d1*d2)
    (p : Equiv.Perm (Fin (d1*d2)))
    (A : Matrix (Fin k) (Fin (d1*d2-k)) ℂ) : Prop :=
  ∀ L : Matrix (Fin k) (Fin k) ℂ, L.IsHermitian →
    traceRight (physicalPerturbation h p A L) = 0 →
    traceLeft (physicalPerturbation h p A L) = 0 → L = 0

/-- PDF pp.6,8: image of the REAL Hermitian local-sum space; no complex span.
Printed: column [I;A^t]. Changed: R.conjTranspose=[I;A†]. Why: preceding
trace identity (2.11), PDF p.6, has A†; PDF p.11 expands this as AXA†.
The correction remains subject to independent moderation. -/
def compressedLocalSpace {d1 d2 k : ℕ} (h : k ≤ d1*d2)
    (p : Equiv.Perm (Fin (d1*d2)))
    (A : Matrix (Fin k) (Fin (d1*d2-k)) ℂ) : Set (Matrix (Fin k) (Fin k) ℂ) :=
  {M | ∃ (X1 : Matrix (Fin d1) (Fin d1) ℂ) (X2 : Matrix (Fin d2) (Fin d2) ℂ),
    X1.IsHermitian ∧ X2.IsHermitian ∧
    M = rankRow h A * permuteMatrix p
      (flatMatrix (Matrix.kronecker X1 (1 : Matrix (Fin d2) (Fin d2) ℂ) +
        Matrix.kronecker (1 : Matrix (Fin d1) (Fin d1) ℂ) X2)) *
      (rankRow h A).conjTranspose}

/-- PDF p.9, Theorem 3.1: construct Omega from an actual complex orthonormal basis. -/
noncomputable def omegaFromBasis
    (psi : OrthonormalBasis (Fin 2) ℂ (EuclideanSpace ℂ (Fin 2))) :
    EuclideanSpace ℂ (Fin 2 × Fin 2) :=
  ((Real.sqrt 2)⁻¹ : ℂ) •
    (tensorVec (ket (0 : Fin 2)) (psi 0) + tensorVec (ket (1 : Fin 2)) (psi 1))

/-! Sanity checks of coordinate order and block orientation. -/

example {d1 d2 : ℕ} (rho1 : Matrix (Fin d1) (Fin d1) ℂ)
    (rho2 : Matrix (Fin d2) (Fin d2) ℂ)
    (rho : Matrix (Fin d1 × Fin d2) (Fin d1 × Fin d2) ℂ) :
    rho ∈ finiteCouplingSet rho1 rho2 ↔
      IsDensityMatrix rho ∧ traceRight rho = rho1 ∧ traceLeft rho = rho2 := Iff.rfl

example {d1 d2 : ℕ} (M : Matrix (Fin d1 × Fin d2) (Fin d1 × Fin d2) ℂ)
    (i j : Fin d1 × Fin d2) :
    flatMatrix M (finProdFinEquiv i) (finProdFinEquiv j) = M i j := by
  change M (finProdFinEquiv.symm (finProdFinEquiv i))
    (finProdFinEquiv.symm (finProdFinEquiv j)) = M i j
  simp only [Equiv.symm_apply_apply]

example {n k : ℕ} (h : k ≤ n) (i : Fin k) :
    (rankSplitEquiv h).symm (rankSplitEquiv h (Sum.inl i)) = Sum.inl i :=
  (rankSplitEquiv h).symm_apply_apply _

example {n : ℕ} (M : Matrix (Fin n) (Fin n) ℂ) :
    permuteMatrix (Equiv.refl _) M = M := rfl

example {n k : ℕ} (h : k ≤ n) (K : Matrix (Fin k) (Fin k) ℂ)
    (A : Matrix (Fin k) (Fin (n-k)) ℂ) (i j : Fin k) :
    rankBlockMatrix h K A (rankSplitEquiv h (Sum.inl i))
      (rankSplitEquiv h (Sum.inl j)) = K i j := by
  simp [rankBlockMatrix, Matrix.submatrix]

example {n k : ℕ} (h : k ≤ n) (A : Matrix (Fin k) (Fin (n-k)) ℂ)
    (i : Fin k) (j : Fin (n-k)) :
    rankRow h A i (rankSplitEquiv h (Sum.inr j)) = A i j := by
  simp [rankRow]

example {d1 d2 k : ℕ} (h : k ≤ d1*d2) (p : Equiv.Perm (Fin (d1*d2)))
    (A : Matrix (Fin k) (Fin (d1*d2-k)) ℂ) (L : Matrix (Fin k) (Fin k) ℂ)
    (i j : Fin d1 × Fin d2) :
    physicalPerturbation h p A L i j = rankBlockMatrix h L A
      (p.symm (finProdFinEquiv i)) (p.symm (finProdFinEquiv j)) := rfl

example {d1 d2 k : ℕ} (h : k ≤ d1*d2) (p : Equiv.Perm (Fin (d1*d2)))
    (A : Matrix (Fin k) (Fin (d1*d2-k)) ℂ) :
    (0 : Matrix (Fin k) (Fin k) ℂ) ∈ compressedLocalSpace h p A := by
  refine ⟨0, 0, ?_, ?_, ?_⟩
  · simp [Matrix.IsHermitian]
  · simp [Matrix.IsHermitian]
  · have hzero :
        Matrix.kronecker (0 : Matrix (Fin d1) (Fin d1) ℂ)
          (1 : Matrix (Fin d2) (Fin d2) ℂ) +
        Matrix.kronecker (1 : Matrix (Fin d1) (Fin d1) ℂ)
          (0 : Matrix (Fin d2) (Fin d2) ℂ) = 0 := by
      ext i j
      simp [Matrix.kronecker, Matrix.kroneckerMap]
    rw [hzero]
    change (0 : Matrix (Fin k) (Fin k) ℂ) =
      rankRow h A * (0 : Matrix (Fin (d1*d2)) (Fin (d1*d2)) ℂ) *
        (rankRow h A).conjTranspose
    simp only [Matrix.mul_zero, Matrix.zero_mul]

example {d1 d2 : ℕ} (h : 0 ≤ d1*d2) (p : Equiv.Perm (Fin (d1*d2)))
    (A : Matrix (Fin 0) (Fin (d1*d2-0)) ℂ) :
    NoZeroMarginalPerturbation h p A := by
  intro L _ _ _
  exact Subsingleton.elim _ _

example (psi : OrthonormalBasis (Fin 2) ℂ (EuclideanSpace ℂ (Fin 2))) (j : Fin 2) :
    omegaFromBasis psi (0, j) = ((Real.sqrt 2)⁻¹ : ℂ) * psi 0 j := by
  simp [omegaFromBasis, tensorVec, ket]

end QAlgorithms.Papers.Independent.Intakethird100.P12

Source

Extremal Quantum States in Coupled Systems, arXiv:quant-ph/0307182v1, https://arxiv.org/abs/quant-ph/0307182v1

Read-back

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

`QAlgorithms.Papers.Independent.Intakethird100.P12.NoZeroMarginalPerturbation`

For arbitrary natural numbers $d_1,d_2,k$ satisfying $k\le d_1d_2$ , a permutation $p$ of $\{0,\ldots,d_1d_2-1\}$ , and a complex $k\times(d_1d_2-k)$ matrix $A$ , this defines the following proposition: for every Hermitian complex $k\times k$ matrix $L$ , form

B_L= \begin{pmatrix} L & LA\\ A^\dagger L & A^\dagger LA \end{pmatrix}, \qquad (P_L)_{(a,b),(a',b')}=(B_L)_{p^{-1}(d_2a+b),\,p^{-1}(d_2a'+b')}.

If both partial traces vanish—that is, $\sum_b(P_L)_{(a,b),(a',b)}=0$ for all $a,a'$ , and $\sum_a(P_L)_{(a,b),(a,b')}=0$ for all $b,b'$ —then $L=0$ . No positivity assumption is required of $L$ . When $k=0$ , the proposition holds because every matrix of size $0\times0$ is zero; this includes all allowed cases with $d_1d_2=0$ .

`QAlgorithms.Papers.Independent.Intakethird100.P12.compressedLocalSpace`

For arbitrary natural numbers $d_1,d_2,k$ satisfying $k\le d_1d_2$ , a permutation $p$ of $\{0,\ldots,d_1d_2-1\}$ , and a complex $k\times(d_1d_2-k)$ matrix $A$ , this defines the set of complex $k\times k$ matrices $M$ for which there exist Hermitian complex matrices $X_1$ of size $d_1\times d_1$ and $X_2$ of size $d_2\times d_2$ such that

M=R\widetilde H R^\dagger,\qquad R=[\,I_k\;\;A\,].

Here $H$ is the matrix on product indices with entries

H_{(a,b),(a',b')}=(X_1)_{a,a'}\delta_{b,b'}+\delta_{a,a'}(X_2)_{b,b'},

and, writing $f(a,b)=d_2a+b$ , the matrix $\widetilde H$ has entries $\widetilde H_{i,j}=H_{f^{-1}(p(i)),\,f^{-1}(p(j))}$ . No positivity or trace condition is imposed on $X_1,X_2$ . If $k=0$ , the defined set consists of the unique $0\times0$ matrix, including when either product dimension is zero.

`QAlgorithms.Papers.Independent.Intakethird100.P12.finiteCouplingSet`

For arbitrary natural numbers $d_1,d_2$ and arbitrary complex matrices $\rho_1$ of size $d_1\times d_1$ and $\rho_2$ of size $d_2\times d_2$ , this defines the set of complex matrices $\rho$ , indexed by pairs $(a,b)$ with $0\le a<d_1$ and $0\le b<d_2$ , such that $\rho$ is positive semidefinite, $\operatorname{tr}\rho=1$ , and its two partial traces satisfy

\sum_{b=0}^{d_2-1}\rho_{(a,b),(a',b)}=(\rho_1)_{a,a'}, \qquad \sum_{a=0}^{d_1-1}\rho_{(a,b),(a,b')}=(\rho_2)_{b,b'}

for every applicable pair of indices. No density-matrix assumption is imposed on the supplied $\rho_1,\rho_2$ ; the resulting set may be empty. If either dimension is zero, the set is empty because the only matrix on the empty product index set has trace zero.

`QAlgorithms.Papers.Independent.Intakethird100.P12.flatMatrix`

For arbitrary natural numbers $d_1,d_2$ and any complex matrix $M$ whose rows and columns are indexed by $\{0,\ldots,d_1-1\}\times\{0,\ldots,d_2-1\}$ , this defines a complex matrix of size $d_1d_2\times d_1d_2$ by reindexing both coordinates through the product-index bijection $f(a,b)=d_2a+b$ :

\operatorname{flatMatrix}(M)_{r,s}=M_{f^{-1}(r),f^{-1}(s)}.

If either dimension is zero, both the original and resulting matrices have empty index sets.

`QAlgorithms.Papers.Independent.Intakethird100.P12.omegaFromBasis`

Given any complex orthonormal basis $(\psi_0,\psi_1)$ of the Euclidean space $\mathbb C^2$ , indexed by $0,1$ , this defines the vector in $\mathbb C^{\{0,1\}\times\{0,1\}}$

\omega=\frac{1}{\sqrt2}\bigl(e_0\otimes\psi_0+e_1\otimes\psi_1\bigr),

where $e_0,e_1$ are the coordinate vectors, and the tensor product used here has coordinates $(u\otimes v)_{(a,b)}=u_a v_b$ . Equivalently, $\omega_{(0,b)}=(\psi_0)_b/\sqrt2$ and $\omega_{(1,b)}=(\psi_1)_b/\sqrt2$ for $b=0,1$ .

`QAlgorithms.Papers.Independent.Intakethird100.P12.permuteMatrix`

For every natural number $n$ , every permutation $p$ of $\{0,\ldots,n-1\}$ , and every complex $n\times n$ matrix $M$ , this defines the complex $n\times n$ matrix whose entries are

\operatorname{permuteMatrix}(p,M)_{i,j}=M_{p(i),p(j)}.

The same permutation is applied to the row and column indices. The definition also applies when $n=0$ , in which case the matrices have empty index sets.

`QAlgorithms.Papers.Independent.Intakethird100.P12.physicalPerturbation`

For arbitrary natural numbers $d_1,d_2,k$ satisfying $k\le d_1d_2$ , a permutation $p$ of $\{0,\ldots,d_1d_2-1\}$ , a complex $k\times(d_1d_2-k)$ matrix $A$ , and a complex $k\times k$ matrix $L$ , this defines a matrix $P_L$ on the product index set $\{0,\ldots,d_1-1\}\times\{0,\ldots,d_2-1\}$ . Writing $f(a,b)=d_2a+b$ and

B_L= \begin{pmatrix} L & LA\\ A^\dagger L & A^\dagger LA \end{pmatrix}, \qquad (P_L)_{(a,b),(a',b')}=(B_L)_{p^{-1}(f(a,b)),\,p^{-1}(f(a',b'))},

these formulas specify the defined matrix completely. No Hermitian or positivity assumption is imposed on $L$ . If $k=0$ , the result is zero; if $d_1d_2=0$ , the hypothesis forces $k=0$ and the result has an empty index set.

`QAlgorithms.Papers.Independent.Intakethird100.P12.rankBlockMatrix`

For arbitrary natural numbers $n,k$ satisfying $k\le n$ , any complex $k\times k$ matrix $K$ , and any complex $k\times(n-k)$ matrix $A$ , this defines the complex $n\times n$ matrix, with the first $k$ coordinates preceding the remaining $n-k$ coordinates, given by

\begin{pmatrix} K & KA\\ A^\dagger K & A^\dagger KA \end{pmatrix},

where $A^\dagger$ denotes the conjugate transpose of $A$ . No Hermitian, positivity, or rank condition is required of $K$ or $A$ . If $k=0$ , the result is the zero $n\times n$ matrix; if $k=n$ , the result is $K$ . These conventions include $n=k=0$ .

`QAlgorithms.Papers.Independent.Intakethird100.P12.rankRow`

For arbitrary natural numbers $n,k$ satisfying $k\le n$ and any complex $k\times(n-k)$ matrix $A$ , this defines the complex $k\times n$ matrix

R=[\,I_k\;\;A\,].

Explicitly, for $0\le i<k$ and $0\le j<n$ , its entry is $1$ if $j<k$ and $i=j$ , is $0$ if $j<k$ and $i\ne j$ , and is $A_{i,j-k}$ if $j\ge k$ . When $k=0$ , it has no rows; when $k=n$ , it is $I_n$ , including the empty identity when $n=0$ .

`QAlgorithms.Papers.Independent.Intakethird100.P12.rankSplitEquiv`

For arbitrary natural numbers $n,k$ , together with a hypothesis $k\le n$ , this defines a bijection from the disjoint union of $\{0,\ldots,k-1\}$ and $\{0,\ldots,n-k-1\}$ to $\{0,\ldots,n-1\}$ . It sends an index $i$ in the first summand to $i$ , and an index $j$ in the second summand to $k+j$ . Thus the inverse assigns indices below $k$ to the first summand and the remaining indices to the second. The cases $k=0$ , $k=n$ , and $n=k=0$ are included, with the corresponding summands 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