Semidefinite extension complexity of the separable set, with applications to approximate disentanglers

We prove quantitative lower bounds on the semidefinite extension complexity of the set of separable quantum states on $\mathbb{C}^d\otimes\mathbb{C}^d$. We consider semidefinite programs (SDPs) that approximate the maximum acceptance probability of a measurement over separable states, the optimization problem underlying QMA(2). In the extended-formulation model of Harrow, Natarajan, and Wu (HNW), all measurements share a common feasible region and an objective-independent embedding of product states that exactly reproduces their acceptance probabilities. For every $0<θ<2/7$, there are constants $c_θ,a_θ>0$ such that, for sufficiently large $d$, any such SDP with uniform additive error $0<a\le a_θ$ has size at least $d^{c_θ\min\{a^{-1/3},d^θ\}}$. The bound applies at sufficiently small constant error, is superpolynomial in $d$ whenever $a=o(1)$, and becomes $d^{Ω(d^θ)}$ when $a\le d^{-3θ}$, improving HNW's quasipolynomial bound at inverse- square error. The same bound holds for any SDP-representable convex set of states that contains all separable states and lies within trace distance $a$ of them, giving a quantitative counterpart to Fawzi's theorem that the separable set has no exact semidefinite representation. Our proof combines the quantitative pseudo-density theorem of Lee, Raghavendra, and Steurer with explicit block-positive operators and Chebyshev amplification. Our main results are supported by Lean proofs.