A Sharp Rank-r Partial-Trace Inequality

Let Φ:Md()→ Md() be a completely positive map with a transpose-symmetric Kraus representation. Its Choi operator determines the rank-two constant \[ β_2(Φ) =12_{{ z=1\\ (z)≤2}} z{J(Φ)z}. \] We prove that, for every r≥1, \[ Φ∘τ+(r-1)β_2(Φ) (Δ-1r) \] is r-positive, where τ is transposition and Δ(X)=(X)I. The proof turns the negative spectrum of a partially transposed rank-one operator into the edges of the complete graph Kᵣ. Regrouping by vertices costs its degree $r-1$, rather than its r2 edges. Transpose symmetry protects one direction and is exactly what produces the term -/r. For Φ=ΛU⊗ΛV, with ΛE(X)=(X)I-XT, a sharp double-skew singular-value estimate gives β₂≤1, with equality when both local dimensions are at least two. A map identity then yields, for every operator C of rank at most r on U⊗ V, \[ {_U C}_2^2+{_V C}_2^2 ≤ r C_2^2+1r{ C}^2, \] with dimension-uniform coefficients that are sharp whenever one local dimension is at least r and the other is at least two. A second family, built from the edges of an arbitrary graph, has the same local constant and attains the universal coefficient $r-1$ whenever the graph contains an r-clique. The Choi lifting chain through the partial-trace and graph results, together with its sharpness witnesses, is formalized in Lean~4.