Lemma 2.11 — the graph of edges tight at every FRAC-maximizer is nonbipartite

Proved

LovaszSchrijver.Defect.tightGraph_not_colorable_two

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

bipartite-graphgraph-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 \in \mathbb R_+^V$ be a nonnegative weight vector. Assume that

\max\{a^{\mathsf T}x : x \in \mathrm{STAB}(G)\} < \max\{a^{\mathsf T}x : x \in \mathrm{FRAC}(G)\}.

Let $E'$ be the set of those edges $ij$ of $G$ for which $y_i + y_j = 1$ holds for every vector $y \in \mathrm{FRAC}(G)$ maximizing $a^{\mathsf T}x$ . Then the graph $(V, E')$ is nonbipartite, i.e. it is not 2-colourable.

This is the first step towards locating a node that is half-integral at every fractional optimum (Lemma 2.12), which drives the induction in Theorem 2.13.

Formalization Note The two maxima are given as numbers $s_S, s_F$ together with the hypotheses that they are the greatest elements of $\{a^{\mathsf T}x : x \in \mathrm{STAB}(G)\}$ and $\{a^{\mathsf T}x : x \in \mathrm{FRAC}(G)\}$ ; the assumption is $s_S < s_F$ . "Nonbipartite" is ¬ (V, E').Colorable 2.

Preamble

import Mathlib
import Definitions.Def_LovaszSchrijver_Defect_Index

Formal statement

namespace LovaszSchrijver.Defect

theorem tightGraph_not_colorable_two {V : Type} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (hG : ∀ v, ∃ w, G.Adj v w)
    (a : V → ℝ) (ha : ∀ i, 0 ≤ a i) (sS sF : ℝ)
    (hS : IsGreatest {s : ℝ | ∃ x ∈ STAB G, s = a ⬝ᵥ x} sS)
    (hF : IsGreatest {s : ℝ | ∃ x ∈ FRAC G, s = a ⬝ᵥ x} sF)
    (hlt : sS < sF) :
    ¬ (tightGraph G a).Colorable 2 := 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. 181, Lemma 2.11

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. $a \in \mathbb{R}^V$ and $s_S, s_F \in \mathbb{R}$ .

Hypotheses.

$G$ has no isolated vertices: every $v \in V$ has a neighbour $w$ with $v \sim w$ .
The weights are nonnegative: $a_i \ge 0$ for all $i$ .
$s_S$ is the maximum of $a^\top x$ over $\mathrm{STAB}(G)$ , and it is attained. Here $\mathrm{STAB}(G)$ is the convex hull of the incidence vectors $\chi^A$ of independent sets $A$ (sets with no two elements adjacent).
$s_F$ is the maximum of $a^\top x$ over $\mathrm{FRAC}(G)$ , and it is attained. Here $\mathrm{FRAC}(G) = \{x \in \mathbb{R}^V : x_i \ge 0\ \forall i,\ x_i + x_j \le 1 \text{ for } i \sim j\}$ .
The inequality is strict: $s_S < s_F$ .

Conclusion. The tight graph $G'_a$ has no proper 2-colouring. That is, there is no map $V \to \{1, 2\}$ that gives different colours to every pair of vertices adjacent in $G'_a$ . Here $G'_a$ is the graph on $V$ whose edges are the edges $ij$ of $G$ such that $y_i + y_j = 1$ for every $y \in \mathrm{FRAC}(G)$ that maximizes $a^\top x$ over $\mathrm{FRAC}(G)$ .

Degenerate cases.

Hypothesis 1 forces every coordinate of a point of $\mathrm{FRAC}(G)$ into $[0, 1]$ . So $\mathrm{FRAC}(G)$ is bounded, and hypotheses 3 and 4 are satisfiable.
If $V$ is empty, both sets are the single empty vector, so $s_S = s_F = 0$ . Then hypothesis 5 fails and the statement is vacuous.
If $a = 0$ , then $s_S = s_F = 0$ and the statement is again vacuous.
The only way the conclusion can hold is if $G'_a$ contains an odd cycle.

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