Theorem 5.2 — $\mathrm{STAB}(G)$ of a graph on $n \ge 1$ vertices has no $\mathcal S^n_+$ -lift

Proved

ConeLifts.StableSet.stab_no_psd_lift

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

cone-liftsp2o-batch-p200ap2o-gran-per-chapterp2o-plan-paperp2o-v1semidefinite-programmingstable-set-polytope

Let $G$ be any graph with $n \ge 1$ vertices. Then the stable set polytope $\mathrm{STAB}(G) \subseteq \mathbb R^n$ does not admit an $\mathcal S^n_+$ -lift: there is no affine subspace $L$ of the real $n\times n$ matrices and no linear map $\pi$ into $\mathbb R^n$ with

\mathrm{STAB}(G) = \pi(\mathcal S^n_+ \cap L).

For a perfect graph $G$ , Lovász's construction gives an $\mathcal S^{n+1}_+$ -lift of $\mathrm{STAB}(G)$ (Theorem 5.1); this theorem shows that the matrix size $n+1$ cannot be lowered to $n$ , for any graph.

Formalization Note All lifts are excluded, proper or not. The ambient space of the lift is all real $n\times n$ matrices; this does not change which sets have lifts (see HasPSDLift). The hypothesis $n \ge 1$ makes explicit that the graph has vertices: for $n = 0$ , $\mathrm{STAB}(G) = \{0\} = \pi(\mathcal S^0_+)$ and the printed statement would be false.

Preamble

import Mathlib
import Definitions.Def_ConeLifts_StableSet_stab
import Definitions.Def_ConeLifts_StableSet_HasPSDLift

Formal statement

namespace ConeLifts.StableSet

/-- **Theorem 5.2** (Gouveia, Parrilo & Thomas, arXiv:1111.3164v2, p. 19): let `G` be any graph
with `n` vertices. Then `STAB(G)` does not admit a `Sⁿ₊`-lift.

All lifts are excluded, proper or not: there is no affine subspace `L` of the real `n × n`
matrices and no linear map `π` to `ℝⁿ` with `STAB(G) = π(Sⁿ₊ ∩ L)`. The hypothesis `n ≥ 1` is
the paper's reading of "a graph with n vertices": for `n = 0`, `STAB(G) = {0} = π(S⁰₊)` and the
printed statement fails. -/
theorem stab_no_psd_lift (n : ℕ) (hn : 1 ≤ n) (G : SimpleGraph (Fin n)) :
    ¬ HasPSDLift n (stab G) := by sorry

end ConeLifts.StableSet

Source

Gouveia, Parrilo & Thomas, Lifts of Convex Sets and Cone Factorizations, arXiv:1111.3164v2, p. 19, Theorem 5.2

Human review

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

View graph

Theorem 5.2 — STAB(G)\mathrm{STAB}(G)STAB(G) of a graph on n≥1n \ge 1n≥1 vertices has no S+n\mathcal S^n_+S+n​-lift

Theorem 5.2 — $\mathrm{STAB}(G)$ of a graph on $n \ge 1$ vertices has no $\mathcal S^n_+$ -lift