Lemma 2.7 — (1/(k+2))𝟙 lies in Nᵏ(G)

Proved

LovaszSchrijver.Defect.one_div_add_two_mem_NG

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

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

Let $G = (V,E)$ be a finite graph with no isolated nodes and let $\mathbb 1 \in \mathbb R^V$ be the all-ones vector. Then for every $k \ge 0$ ,

\frac{1}{k+2}\,\mathbb 1 \in N^k(G).

This point shows that $k$ rounds of $N$ cannot cut off the uniform vector $\frac1{k+2}\mathbb 1$ ; it gives the lower bound in Theorem 2.13 and in Corollary 2.8.

Formalization Note $k + 2$ is computed in $\mathbb R$ . For $k = 0$ the statement is $\tfrac12\mathbb 1 \in \mathrm{FRAC}(G)$ .

Preamble

import Mathlib
import Definitions.Def_LovaszSchrijver_Defect_Index

Formal statement

namespace LovaszSchrijver.Defect

theorem one_div_add_two_mem_NG {V : Type} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (hG : ∀ v, ∃ w, G.Adj v w) (k : ℕ) :
    (fun _ : V => 1 / ((k : ℝ) + 2)) ∈ NG k G := 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. 180, Lemma 2.7

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 \in \mathbb{N}$ .

Hypothesis. $G$ has no isolated vertices: every vertex has a neighbour.

Conclusion. The constant vector with every entry $\tfrac{1}{k+2}$ lies in $N^k(G)$ . That is,

\Big(1, \tfrac{1}{k+2}, \dots, \tfrac{1}{k+2}\Big) \in N^k(\mathrm{FR}(G)).

The terms are defined as follows:

$\mathrm{FR}(G) = \{x \in \mathbb{R}^{\{0\}\cup V} : x_j \ge 0\ (j \in V),\ x_j + x_l \le x_0 \text{ for } j \sim l\}$ .
$N^0(K) = K$ and $N^{t+1}(K) = N(N^t(K), Q)$ .
$N(K, Q)$ is the set of $0$ th columns of symmetric matrices $Y$ with $Y_{jj} = Y_{0j}$ for $j \in V$ and $u^\top Y w \ge 0$ for $u \in K^*$ and $w \in Q^*$ .
$Q$ is the cone spanned by 0–1 vectors with $x_0 = 1$ , and $K^*$ is the set of $u$ with $u^\top x \ge 0$ on $K$ .

The denominator $k + 2$ is at least $2$ , so no division by zero occurs.

Degenerate cases.

For $k = 0$ , the claim is that $(\tfrac12, \dots, \tfrac12) \in \mathrm{FRAC}(G)$ .
If $V$ is empty, the hypothesis is vacuous and the claim is that the one-coordinate vector $(1)$ lies in $N^k(\mathrm{FR}(G))$ , where $\mathrm{FR}(G)$ is all of $\mathbb{R}$ .

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