Corollary 16: equality of S_oneHalf forbids nontrivial preparation

Open

QAlgorithms.Papers.Independent.Intakethird100.P95.corollary16

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

prove2quantum

Let $\lambda=(\lambda_1,\ldots,\lambda_d)$ be a finite probability vector: every entry is nonnegative and the entries sum to one. Write $\rho_\lambda=\sum_{i,j}\sqrt{\lambda_i\lambda_j}|ii\rangle\langle jj|$ . All logarithms have base two. A PPT operation is a completely positive, trace-preserving map $L$ such that $\Gamma_{\rm out}L\Gamma_{\rm in}$ is completely positive for arbitrary finite ancillary systems; $\Gamma$ transposes Bob in the fixed product basis. Assume in addition that all entries of $\lambda$ are strictly positive, so $d$ is its Schmidt rank. For a positive integer $K$ , $\Phi_K$ denotes the maximally entangled state of Schmidt rank $K$ . For a finite order $t$ , $S_t$ is the Rényi entropy, with $S_0$ the log support size, $S_1=-\sum_i\lambda_i\log_2\lambda_i$ (using $0\log_2 0=0$ ), and $S_t=(1-t)^{-1}\log_2\sum_i\lambda_i^t$ otherwise. The separate infinity order is $S_\infty=-\log_2\max_i\lambda_i$ . Let $K\ge2$ and $d\ge K$ . If $S_{1/2}(\lambda)=\log_2 K$ , then

\Phi_K\to^{\rm PPT}\rho_\lambda\quad\Longrightarrow\quad d=K\;\text{ and }\;\lambda_i=1/K\text{ for every }i.

Thus the entropy equality case permits only the same maximally entangled nonzero spectrum, up to local unitaries.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P95

Formal statement

noncomputable section

open scoped BigOperators Matrix ComplexOrder

open Filter

namespace QAlgorithms.Papers.Independent.Intakethird100.P95

attribute [local instance] Classical.propDecidable Classical.decEq

-- Exact primitives from the pinned accepted library; no local aliases.

open QAlgorithms.Papers.Independent.Claimed50.P28 (maximallyEntangledDensity)

open QAlgorithms.Papers.Independent.Information100.P27 (IsProbability)

open QAlgorithms.Papers.Independent.Information100.P63 (logTwo)

open QAlgorithms.Papers.Independent.Information100.P19 (outer)

open QAlgorithms.Papers.Independent.Dependency50.P18 (bipartiteTensor)

open QAlgorithms.Papers.Independent.Support50.P11 (Loewner)

/-- PDF p.7, Corollary 16: only-if, including the entropy equality boundary.
Full support makes equality of nonzero spectra exactly d=K and uniform entries. -/
theorem corollary16 {d : ℕ} (K : ℕ) (hK : 2 ≤ K) (lam : Fin d → ℝ)
    (hprob : IsProbability lam) (hpos : ∀ i, 0 < lam i) (hd : K ≤ d)
    (hentropy : schmidtRenyi (1 / 2) lam = logTwo (K : ℝ)) :
    Reach (maximallyEntangledDensity K) (schmidtDensity lam) → d = K ∧ ∀ i, lam i = (K : ℝ)⁻¹ := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P95

end

Source

Pure-state transformations and catalysis under operations that completely preserve positivity of partial transpose, arXiv:0801.4322v2, PDF p. 7, Corollary 16: equality of S_oneHalf forbids nontrivial preparation

Read-back

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

For every natural number $d$ , integer $K\ge2$ , and strictly positive probability vector $\lambda\in\mathbb R^d$ , assume $K\le d$ and

2\log_2\!\left(\sum_{i=0}^{d-1}\sqrt{\lambda_i}\right)=\log_2 K, \qquad \log_2 x=\frac{\log x}{\log2}.

Define $\Omega_K=K^{-1}\sum_{i,j=0}^{K-1}|ii\rangle\langle jj|$ and define $\rho_\lambda$ on $\mathbb C^d\otimes\mathbb C^d$ by $(\rho_\lambda)_{(i,j),(k,l)}=\sqrt{\lambda_i\lambda_k}$ if $i=j$ and $k=l$ , and $0$ otherwise. If there exists a complex-linear map $\mathcal L$ sending $\Omega_K$ to $\rho_\lambda$ , preserving the trace of every matrix, and such that both $\mathcal L$ and $\Gamma_{\rm out}\mathcal L\Gamma_{\rm in}$ are completely positive, then $d=K$ and $\lambda_i=1/K$ for every $i$ . Here $\Gamma$ transposes the second tensor factor, $(\Gamma X)_{(i,j),(k,l)}=X_{(i,l),(k,j)}$ , and complete positivity requires positivity preservation under every finite identity amplification, including size zero. Strict positivity and probability mean $\lambda_i>0$ and $\sum_i\lambda_i=1$ .

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