Proposition 2.1: common rank-block representation and midpoint summands

Open

QAlgorithms.Papers.Independent.Intakethird100.P12.common_rank_block

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

prove2quantum

Let $\rho$ be a complex positive semidefinite matrix of order $n$ , with actual rank $k<n$ . Define $B_A(L)=\begin{pmatrix}L&LA\\A^\dagger L&A^\dagger LA\end{pmatrix}$ , where $A$ has size $k\times(n-k)$ and $L$ has order $k$ . There exist a permutation unitary $\sigma$ , such a matrix $A$ , and a strictly positive definite matrix $K$ of order $k$ for which

\sigma\rho\sigma^{-1}=B_A(K).

The same $\sigma,A$ work for every decomposition $\rho=\tfrac12(\rho'+\rho'')$ into positive semidefinite matrices: there exist positive semidefinite matrices $K',K''$ of order $k$ such that

\sigma\rho'\sigma^{-1}=B_A(K'),\qquad\sigma\rho''\sigma^{-1}=B_A(K'').

This common representation controls midpoint decompositions even when their summands are singular. No trace normalization is imposed; $k=0$ is allowed. The source's unqualified “positive definite” means positive semidefinite, as its Gram-matrix proof confirms.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P12

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P12

open scoped ComplexConjugate ComplexOrder

/-- Proposition 2.1, PDF pp.3–4: the source's 'positive definite' means PSD;
only K is strict. The SAME sigma,A precede all midpoint summands. -/
theorem common_rank_block {n k : ℕ} (rho : Matrix (Fin n) (Fin n) ℂ)
    (hpsd : rho.PosSemidef) (hrank : rho.rank = k) (hkn : k < n) :
    ∃ (p : Equiv.Perm (Fin n)) (A : Matrix (Fin k) (Fin (n-k)) ℂ)
      (K : Matrix (Fin k) (Fin k) ℂ),
      K.PosDef ∧ permuteMatrix p rho = rankBlockMatrix hkn.le K A ∧
      ∀ (rhoFirst rhoSecond : Matrix (Fin n) (Fin n) ℂ),
        rhoFirst.PosSemidef → rhoSecond.PosSemidef →
        rho = (1 / 2 : ℂ) • (rhoFirst + rhoSecond) →
        ∃ (KFirst KSecond : Matrix (Fin k) (Fin k) ℂ),
          KFirst.PosSemidef ∧ KSecond.PosSemidef ∧
          permuteMatrix p rhoFirst = rankBlockMatrix hkn.le KFirst A ∧
          permuteMatrix p rhoSecond = rankBlockMatrix hkn.le KSecond A := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P12

Source

Extremal Quantum States in Coupled Systems, arXiv:quant-ph/0307182v1, PDF p. 3, Proposition 2.1: common rank-block representation and midpoint summands

Read-back

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

For all natural numbers $n,k$ and every complex $n\times n$ matrix $\rho$ , assume that $\rho$ is positive semidefinite, has rank exactly $k$ , and satisfies $k<n$ . Then there exist a permutation $p$ of $\{0,\ldots,n-1\}$ , a complex $k\times(n-k)$ matrix $A$ , and a positive definite complex $k\times k$ matrix $K$ such that, defining

B_A(H)= \begin{pmatrix} H & HA\\ A^\dagger H & A^\dagger HA \end{pmatrix},

one has $\rho_{p(i),p(j)}=B_A(K)_{i,j}$ for all $i,j$ . Moreover, for every pair of positive semidefinite complex $n\times n$ matrices $\rho_{\mathrm{First}},\rho_{\mathrm{Second}}$ satisfying $\rho=\tfrac12(\rho_{\mathrm{First}}+\rho_{\mathrm{Second}})$ , there exist positive semidefinite complex $k\times k$ matrices $K_{\mathrm{First}},K_{\mathrm{Second}}$ such that

(\rho_{\mathrm{First}})_{p(i),p(j)}=B_A(K_{\mathrm{First}})_{i,j}, \qquad (\rho_{\mathrm{Second}})_{p(i),p(j)}=B_A(K_{\mathrm{Second}})_{i,j}

for all $i,j$ , using the same $p,A$ chosen above. No trace normalization is assumed. The hypotheses exclude $n=0$ but allow $k=0$ ; in that case the displayed block matrices are zero, and positive definiteness of the empty $K$ is vacuous.

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