III B: attained SDP optimum detects extendability, (11)–(12)

Open

QAlgorithms.Papers.Independent.Intakethird100.P30.sdpCharacterization

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

prove2quantum

Let $A,B$ be finite nonempty systems and let $P\succeq0$ be any operator on $A\otimes B$ , without a trace-one assumption. Identify $B'$ with a copy of $B$ . Consider

t_{\min}(P)=\min\{t\in\mathbb R:\ \exists R=R^\dagger, \ R+tI\succeq0,\ \operatorname{Tr}_{B'}R=P, \ \operatorname{Tr}_{B}R=P\}.

Both marginal constraints use their actual coefficient partial traces and the stated register identification. The feasible objective set is nonempty and bounded below, and its finite infimum is attained. Moreover,

\mathrm{Ext}_B(P)\Longleftrightarrow t_{\min}(P)\le0, \qquad \neg\mathrm{Ext}_B(P)\Longleftrightarrow t_{\min}(P)>0.

Whenever the optimum is nonpositive, every minimizing $R$ is a positive symmetric extension. The optimization variable $R$ is initially only Hermitian; requiring it positive in the feasible set would change the SDP. The zero operator is included.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P30

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P30

open scoped BigOperators Matrix ComplexConjugate ComplexOrder

attribute [local instance] Classical.propDecidable Classical.decEq

variable {I J K L A B : Type}

variable [Fintype I] [Fintype J] [Fintype K] [Fintype L]

variable [Fintype A] [Fintype B]

/-- PDF p.5, (11)–(12): finite attained SDP optimum detects extendability.
All finite nonempty systems and all PSD P, including zero, are covered. -/
theorem sdpCharacterization [Nonempty A] [Nonempty B]
    (P : Matrix (A × B) (A × B) ℂ) (hP : P.PosSemidef) :
    (slackValues P).Nonempty ∧ BddBelow (slackValues P) ∧
    (∃ R, SDPFeasible P (sdpMinimum P) R) ∧
    (BobExtendible P ↔ sdpMinimum P ≤ 0) ∧
    (¬ BobExtendible P ↔ 0 < sdpMinimum P) ∧
    (∀ R, SDPFeasible P (sdpMinimum P) R → sdpMinimum P ≤ 0 → IsBobCopyExtension P R) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P30

end

Source

Numerical evidence for bound secrecy from two-way post-processing in quantum key distribution, arXiv:1612.07734v2, PDF p. 5, III B: attained SDP optimum detects extendability, (11)–(12)

Read-back

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

For nonempty finite types $A$ and $B$ with decidable equality and a positive semidefinite complex matrix $P$ indexed by $A\times B$ , let $S$ consist of those real $t$ for which some Hermitian matrix $R$ indexed by $(A\times B)\times B$ satisfies $R+tI\succeq0$ and

\sum_{c\in B}R_{((a,b),c),((a',b'),c)} = \sum_{c\in B}R_{((a,c),b),((a',c),b')} =P_{(a,b),(a',b')}

for all $a,a',b,b'$ , and put $s=\inf S$ . The theorem asserts that $S$ is nonempty and bounded below; that some such $R$ is feasible at $t=s$ ; that there exists a positive semidefinite $R$ with these two marginals exactly when $s\le0$ ; that no such positive semidefinite extension exists exactly when $0<s$ ; and that every matrix feasible at $t=s$ is itself a positive semidefinite extension whenever $s\le0$ . Neither $P$ nor its extensions are required to have trace $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