Prove2Me

Unnumbered Corollary: extremal rank bound

Open
QAlgorithms.Papers.Independent.Intakethird100.P12.extremal_rank_bound

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

prove2quantum

Let d1,d2d_1,d_2 be the dimensions of finite-dimensional complex Hilbert spaces with chosen orthonormal bases. Let ρ1,ρ2\rho_1,\rho_2 be positive semidefinite operators of trace one. Write C(ρ1,ρ2)C(\rho_1,\rho_2) for all joint density matrices with these two partial traces, and E(ρ1,ρ2)E(\rho_1,\rho_2) for its extreme points over the real scalars. Coordinates in the tensor product use lexicographic order.

For every extreme coupling ρ∈E(ρ1,ρ2)\rho\in E(\rho_1,\rho_2),

rank⁡ρ≤d12+d22−1.\operatorname{rank}\rho\le\sqrt{d_1^2+d_2^2-1}.

This bounds the rank of an extreme point using only the subsystem dimensions. One-dimensional subsystems are included; no full-rank assumption is imposed on the marginals.

Preamble
import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P12
Formal statement
namespace QAlgorithms.Papers.Independent.Intakethird100.P12

open scoped ComplexConjugate ComplexOrder

/-- Unnumbered Corollary after Proposition 2.3, PDF pp.6–7.
No d1,d2>=2 restriction: singleton coupling sets also satisfy the bound. -/
theorem extremal_rank_bound {d1 d2 : ℕ}
    (rho1 : Matrix (Fin d1) (Fin d1) ℂ) (rho2 : Matrix (Fin d2) (Fin d2) ℂ)
    (hm1 : IsDensityMatrix rho1) (hm2 : IsDensityMatrix rho2)
    (rho : Matrix (Fin d1 × Fin d2) (Fin d1 × Fin d2) ℂ)
    (hext : rho ∈ Set.extremePoints ℝ (finiteCouplingSet rho1 rho2)) :
    (rho.rank : ℝ) ≤ Real.sqrt ((d1 : ℝ)^2 + (d2 : ℝ)^2 - 1) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P12
Source
Extremal Quantum States in Coupled Systems, arXiv:quant-ph/0307182v1, PDF p. 6, Unnumbered Corollary after Proposition 2.3: rank bound
Read-back

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

For any natural numbers d1,d2d_1,d_2, let ρ1\rho_1 and ρ2\rho_2 be complex positive semidefinite matrices of sizes d1d_1 and d2d_2, respectively, each with trace 11. Define CC to be the set of complex positive semidefinite matrices σ\sigma, indexed by pairs (i,j)∈{0,…,d1−1}×{0,…,d2−1}(i,j)\in\{0,\ldots,d_1-1\}\times\{0,\ldots,d_2-1\}, with trace 11 and satisfying

∑j=0d2−1σ(i,j),(i′,j)=(ρ1)i,i′,∑i=0d1−1σ(i,j),(i,j′)=(ρ2)j,j′.\sum_{j=0}^{d_2-1}\sigma_{(i,j),(i',j)}=(\rho_1)_{i,i'}, \qquad \sum_{i=0}^{d_1-1}\sigma_{(i,j),(i,j')}=(\rho_2)_{j,j'}.

For every matrix ρ\rho that is an extreme point of CC, with extremality taken over the real numbers, its complex matrix rank satisfies

rank⁡C(ρ)≤d12+d22−1.\operatorname{rank}_{\mathbb C}(\rho)\le \sqrt{d_1^2+d_2^2-1}.

Here an extreme point belongs to CC and cannot be expressed as a strict convex combination of two distinct members of CC. Although zero dimensions are quantified over, the trace-11 hypotheses cannot hold when either dimension is zero.

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