Lemma 2.2 — valid deletion and contraction of one node give validity for N(K)

Proved

LovaszSchrijver.Defect.valid_N_of_deletion_contraction

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

graph-theorylift-and-projectp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1stable-set-polytope

Let $G = (V,E)$ be a finite graph with no isolated nodes. The paper states this lemma for "any convex body $K$ containing $\mathrm{STAB}(G)$ and contained in $\mathrm{FRAC}(G)$ " (p. 177); it is stated here for the homogenized body. Let $K \subseteq \mathbb R^{V\cup\{0\}}$ be a closed convex cone with $K \subseteq \mathrm{FR}(G)$ , and say that an inequality $a^{\mathsf T}x \le b$ on $\mathbb R^V$ is valid for $K$ if it holds for every $x \in \mathbb R^V$ with $\binom1x \in K$ , and valid for $N(K)$ if it holds for every $x$ with $\binom1x \in N(K)$ .

If $a^{\mathsf T}x \le b$ is an inequality such that for some $v \in V$ both the deletion and the contraction of $v$ give an inequality valid for $K$ , then $a^{\mathsf T}x \le b$ is valid for $N(K)$ :

a_{V-v}^{\mathsf T}x \le b \ \text{ and } \ a_{V-\Gamma(v)-v}^{\mathsf T}x \le b - a_v \text{ valid for } K \ \Longrightarrow\ a^{\mathsf T}x \le b \text{ valid for } N(K).

Applied to $K = N^{t}(\mathrm{FR}(G))$ , it passes validity from $N^t(G)$ to $N^{t+1}(G)$ ; this is how the induction in Theorem 2.13 climbs one level at a time.

Formalization Note The body $K$ is taken in homogenized (cone) form so that it applies to $N^{t}(\mathrm{FR}(G))$ . The hypothesis "containing $\mathrm{STAB}(G)$ " is dropped (the lemma is stronger without it). $K$ is assumed closed: the paper tacitly takes $K$ closed (polyhedral in all its applications), and Lemma 1.3, from which this lemma follows, needs it. Deletion and contraction are the zero-extended coefficient vectors on the same graph. $a$ is an arbitrary real vector.

Preamble

import Mathlib
import Definitions.Def_LovaszSchrijver_Defect_Index

Formal statement

namespace LovaszSchrijver.Defect

theorem valid_N_of_deletion_contraction {V : Type} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (hG : ∀ v, ∃ w, G.Adj v w)
    (K : Set (Option V → ℝ)) (hK : IsConvexCone K) (hKc : IsClosed K) (hKFR : K ⊆ FR G)
    (a : V → ℝ) (b : ℝ) (v : V)
    (hdel : Valid {x | hom x ∈ K} (deletion a v) b)
    (hcon : Valid {x | hom x ∈ K} (contraction G a v) (b - a v)) :
    Valid {x | hom x ∈ N1 K} a b := by sorry

end LovaszSchrijver.Defect

Source

Lovász and Schrijver, Cones of matrices and set-functions and 0–1 optimization, SIAM J. Optim. 1(2) (1991), p. 178, Lemma 2.2 (with the preamble on p. 177, Section 2.b)

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Setting. $V$ is a finite type with decidable equality and $G$ is a simple graph on $V$ with decidable adjacency. $K \subseteq \mathbb{R}^{\{0\}\cup V}$ , $a \in \mathbb{R}^V$ , $b \in \mathbb{R}$ and $v \in V$ . For a set $L \subseteq \mathbb{R}^{\{0\}\cup V}$ , write its slice as

L|_{x_0=1} = \{\, x \in \mathbb{R}^V : (1, x) \in L \,\}.

Hypotheses.

$G$ has no isolated vertices.
$K$ is a convex cone: nonempty, closed under addition, and closed under nonnegative scaling.
$K$ is topologically closed.
$K \subseteq \mathrm{FR}(G) = \{x : x_j \ge 0\ (j \in V),\ x_j + x_k \le x_0 \text{ for } j \sim k\}$ .
Deletion. For every $x \in K|_{x_0=1}$ :

\sum_{w \ne v} a_w x_w \le b.

Contraction. For every $x \in K|_{x_0=1}$ :

\sum_{w \ne v,\ w \not\sim v} a_w x_w \le b - a_v.

No sign conditions are imposed on $a$ or $b$ .

Conclusion. $a^\top x \le b$ holds for every $x \in N(K)|_{x_0=1}$ . Here $N(K) = N(K, Q)$ is defined as follows:

$N(K, Q)$ is the set of $0$ th columns $Y e_0$ of matrices $Y$ indexed by $\{0\}\cup V$ that are symmetric, have $Y_{jj} = Y_{0j}$ for $j \in V$ , and satisfy $u^\top Y w \ge 0$ for all $u \in K^*$ and $w \in Q^*$ ;
$K^* = \{u : u^\top x \ge 0\ \forall x \in K\}$ ;
$Q$ is the cone spanned by the 0–1 vectors with $x_0 = 1$ .

Degenerate cases.

A vertex $v$ must exist, so $V$ is nonempty. With hypothesis 1, $G$ then has an edge.
If $K$ has no point with $x_0 = 1$ (for example $K = \{0\}$ ), hypotheses 5 and 6 are vacuous. The statement then asserts $a^\top x \le b$ on $N(K)|_{x_0=1}$ with no further assumption on $a$ or $b$ .

Human review

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

View graph