Proposition 2, pp. 21–22 — the multiplicity bound k ≥ aff dim{b(γ) : γ ∈ ℱ} + 1 of Theorems 1 and 2 cannot be lowered to k ≥ aff dim{b(γ) : γ ∈ ℱ}

Proved

QCQPTightness.Sharp.proposition_2

by mikedeng1 · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

convex-hullcounterexamplep2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1qcqpquadratic-eigenvalue-multiplicitysdp-relaxation

For any positive integers $n$ and $k$ there exists a QCQP in $N=nk$ variables with $m=k+1$ constraints such that

Assumptions 1 and 3 are satisfied,
the quadratic eigenvalue multiplicity of the QCQP is $k$ ,
for every semidefinite face $\mathcal F$ of $\Gamma$ ,

k\ \ge\ \operatorname{aff\,dim}\big(\{b(\gamma) : \gamma\in\mathcal F\}\big),

but $\mathrm{Opt}\ne\mathrm{Opt}_{\mathrm{SDP}}$ , and hence $\operatorname{conv}(\mathcal D)\ne\mathcal D_{\mathrm{SDP}}$ .

Theorems 1 and 2 of the paper guarantee $\operatorname{conv}(\mathcal D)=\mathcal D_{\mathrm{SDP}}$ and $\mathrm{Opt}=\mathrm{Opt}_{\mathrm{SDP}}$ under Assumptions 1 and 3 when $k\ge\operatorname{aff\,dim}\{b(\gamma):\gamma\in\mathcal F\}+1$ for every semidefinite face. This proposition shows that the "+1" cannot be removed.

Formalization Note The QCQP is existentially quantified over QCQP (n * k) (k + 1), so $N=nk$ and $m=k+1$ are fixed as on the page. "The multiplicity is $k$ " is IsQuadEigMult k ( $k$ is the largest admissible integer). Faces are nonempty. Both conclusions of the last bullet are stated.

Preamble

import Mathlib
import Definitions.Def_QCQPTightness_Sharp_QCQP
import Definitions.Def_QCQPTightness_Sharp_Faces
import Definitions.Def_QCQPTightness_Sharp_Mult

Formal statement

namespace QCQPTightness.Sharp

/-- Proposition 2 (arXiv:1911.09195v3, pp. 21–22): for all positive integers `n`, `k` there is a
QCQP in `N = nk` variables with `m = k + 1` constraints satisfying Assumptions 1 and 3, with
quadratic eigenvalue multiplicity `k`, with `k ≥ aff dim{b(γ) : γ ∈ ℱ}` for every semidefinite
face `ℱ` of `Γ`, but with `Opt ≠ Opt_SDP` (and hence `conv(𝒟) ≠ 𝒟_SDP`). -/
theorem proposition_2 : ∀ n k : ℕ, 0 < n → 0 < k →
    ∃ P : QCQP (n * k) (k + 1),
      P.Assumption1 ∧ P.Assumption3 ∧ P.IsQuadEigMult k ∧
      (∀ F : Set (Fin (k + 1) → ℝ), P.IsSemidefiniteFace F → affdim (P.bγ '' F) ≤ k) ∧
      P.Opt ≠ P.OptSDP ∧ convexHull ℝ P.D ≠ P.DSDP := by sorry

end QCQPTightness.Sharp

Source

arXiv:1911.09195v3, Proposition 2, pp. 21–22

Human review

Endorsed by Shuze Chen · Oct 10, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 10, 2026
Confirmed by the mission captain (proposal self-audit).

View graph