Proof of Theorem 2.13 — deletion and contraction of the half-integral node have smaller defect

Proved

LovaszSchrijver.Defect.defect_deletion_contraction_lt

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

graph-theoryp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1stable-set-polytope

Let $G = (V,E)$ be a finite graph with no isolated nodes, and let $a^{\mathsf T}x \le b$ be an inequality with $a \in \mathbb Z_+^V$ , $b \in \mathbb Z_+$ , valid for $\mathrm{STAB}(G)$ , whose defect

r = 2\max\{a^{\mathsf T}x - b : x \in \mathrm{FRAC}(G)\}

is positive. Let $i \in V$ be a node with $y_i = \tfrac12$ at every vector $y \in \mathrm{FRAC}(G)$ maximizing $a^{\mathsf T}x$ (such a node exists by Lemma 2.12). Then both the deletion and the contraction of $i$ result in constraints with smaller defect:

the deletion $a_{V-i}^{\mathsf T}x \le b$ has a defect, and it is $< r$ ;
the contraction $a_{V-\Gamma(i)-i}^{\mathsf T}x \le b - a_i$ has a defect, and it is $< r$ .

This is the claim on which the induction on $r$ in the upper bound of Theorem 2.13 rests.

Formalization Note Deletion and contraction are the zero-extended coefficient vectors on the same graph $G$ (see the definition item), and their defects are taken over $\mathrm{FRAC}(G)$ , as in the paper's proof. The contraction's right-hand side $b - a_i$ is computed in $\mathbb R$ . The existence of each defect (the maximum being attained) is part of the conclusion.

Preamble

import Mathlib
import Definitions.Def_LovaszSchrijver_Defect_Index

Formal statement

namespace LovaszSchrijver.Defect

theorem defect_deletion_contraction_lt {V : Type} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (hG : ∀ v, ∃ w, G.Adj v w)
    (a : V → ℕ) (b : ℕ) (hvalid : Valid (STAB G) (fun j => (a j : ℝ)) b)
    (r : ℝ) (hr : IsDefect G (fun j => (a j : ℝ)) b r) (hr0 : 0 < r)
    (i : V) (hi : ∀ y : V → ℝ, IsFRACMaximizer G (fun j => (a j : ℝ)) y → y i = 1 / 2) :
    (∃ r₁ : ℝ, IsDefect G (deletion (fun j => (a j : ℝ)) i) b r₁ ∧ r₁ < r) ∧
    (∃ r₂ : ℝ, IsDefect G (contraction G (fun j => (a j : ℝ)) i) ((b : ℝ) - (a i : ℝ)) r₂ ∧
      r₂ < r) := 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. 182, proof of Theorem 2.13 (upper bound), second paragraph

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. The weights $a \in \mathbb{N}^V$ and the right-hand side $b \in \mathbb{N}$ are natural numbers, treated as real numbers wherever they appear below. $r \in \mathbb{R}$ and $i \in V$ .

Hypotheses.

$G$ has no isolated vertices.
The inequality $a^\top x \le b$ is valid for $\mathrm{STAB}(G)$ , the convex hull of incidence vectors of independent sets.
$r$ is the defect of $a^\top x \le b$ : $r = \max\{2(a^\top x - b) : x \in \mathrm{FRAC}(G)\}$ , and the maximum is attained. Here $\mathrm{FRAC}(G) = \{x \ge 0 : x_j + x_k \le 1 \text{ for } j \sim k\}$ .
The defect is positive: $r > 0$ .
Every $y \in \mathrm{FRAC}(G)$ that maximizes $a^\top x$ over $\mathrm{FRAC}(G)$ has $y_i = \tfrac12$ .

Conclusion. Both of the following hold.

Deletion. Let $a'$ be $a$ with $a_i$ replaced by $0$ . There is an $r_1 < r$ that is the defect of $a'^\top x \le b$ :

r_1 = \max_{x \in \mathrm{FRAC}(G)} 2\,(a'^\top x - b), \quad \text{attained}.

Contraction. Let $a''$ be $a$ with $a_i$ and every $a_w$ for $w$ adjacent to $i$ replaced by $0$ . There is an $r_2 < r$ that is the defect of $a''^\top x \le b - a_i$ :

r_2 = \max_{x \in \mathrm{FRAC}(G)} 2\,\big(a''^\top x - (b - a_i)\big), \quad \text{attained}.

The subtraction $b - a_i$ is ordinary real subtraction, so it can be negative. The graph is still $G$ in both parts: nothing is removed from it.

Degenerate cases.

If $V$ is empty, $\mathrm{FRAC}(G)$ is a single point and the defect is $-2b \le 0$ . Hypothesis 4 then fails. In any case, no vertex $i$ exists, so the statement is vacuous.
Hypothesis 1 makes $\mathrm{FRAC}(G)$ bounded, so maximizers exist and hypothesis 5 is a real constraint.

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