Lemma 2.12 — some node takes the value ½ at every FRAC-maximizer

Proved

LovaszSchrijver.Defect.exists_half_at_every_maximizer

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 \in \mathbb R_+^V$ . Assume that

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

Then there exists a node $i \in V$ such that every vector $y \in \mathrm{FRAC}(G)$ maximizing $a^{\mathsf T}x$ has $y_i = \tfrac12$ .

In the proof of Theorem 2.13 this node $i$ is the one whose deletion and contraction lower the defect.

Formalization Note As in Lemma 2.11, the two maxima are numbers $s_S < s_F$ with IsGreatest hypotheses.

Preamble

import Mathlib
import Definitions.Def_LovaszSchrijver_Defect_Index

Formal statement

namespace LovaszSchrijver.Defect

theorem exists_half_at_every_maximizer {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) :
    ∃ i : V, ∀ y : V → ℝ, IsFRACMaximizer G a y → y i = 1 / 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. 182, Lemma 2.12

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 vertex has at least one neighbour.
The weights are nonnegative: $a_i \ge 0$ for all $i$ .
$s_S = \max\{a^\top x : x \in \mathrm{STAB}(G)\}$ , and the maximum is attained. Here $\mathrm{STAB}(G)$ is the convex hull of incidence vectors of independent sets of $G$ .
$s_F = \max\{a^\top x : x \in \mathrm{FRAC}(G)\}$ , and the maximum is attained. Here $\mathrm{FRAC}(G) = \{x \ge 0 : x_i + x_j \le 1 \text{ for } i \sim j\}$ .
The inequality is strict: $s_S < s_F$ .

Conclusion. There is a single vertex $i \in V$ such that

y_i = \tfrac12 \quad \text{for every } y \in \mathrm{FRAC}(G) \text{ with } a^\top y \ge a^\top x \ \ \forall x \in \mathrm{FRAC}(G).

The same $i$ works for all maximizers at once; it is not chosen separately for each one.

Degenerate cases.

Hypothesis 1 makes $\mathrm{FRAC}(G)$ bounded. So if $V$ is nonempty, maximizers exist and the conclusion is not vacuous.
If $V$ is empty, or if $a = 0$ , then $s_S = s_F$ . Hypothesis 5 fails and the statement is vacuous.

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