Lemma 1.1 — (K₁ ∩ K₂)° ⊆ N₊(K₁, K₂) ⊆ N(K₁, K₂) ⊆ K₁ ∩ K₂

Proved

LovaszSchrijver.IntegerHull.hull01_subset_Nplus_subset_N_subset_inter

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

lift-and-projectmatrix-conep2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1semidefinite

Let $K_1, K_2 \subseteq Q$ be closed convex cones in $\mathbb R^{n+1}$ . Then

(K_1 \cap K_2)^\circ \subseteq N_+(K_1, K_2) \subseteq N(K_1, K_2) \subseteq K_1 \cap K_2 .

Here $(K_1 \cap K_2)^\circ$ is the cone spanned by the 0–1 vectors in $K_1 \cap K_2$ .

The lemma says that the operators $N$ and $N_+$ are relaxation-tightening cuts: they never lose a 0–1 point and never add a point outside the cones they start from.

Formalization Note The three inclusions are stated as one conjunction. The last inclusion uses the rewriting (iii′), which needs $K_i^{**} = K_i$ ; the paper tacitly takes the cones closed (polyhedral in all its applications), so both cones are assumed closed. For a non-closed cone the last inclusion can fail.

Preamble

import Mathlib
import Definitions.Def_LovaszSchrijver_IntegerHull_Basic
import Definitions.Def_LovaszSchrijver_IntegerHull_MatrixCone
open Matrix Pointwise

Formal statement

namespace LovaszSchrijver.IntegerHull

theorem hull01_subset_Nplus_subset_N_subset_inter {ι : Type} [Fintype ι] [DecidableEq ι]
    (K₁ K₂ : Set (Option ι → ℝ)) (hK₁ : IsConvexCone K₁) (hK₂ : IsConvexCone K₂)
    (hK₁c : IsClosed K₁) (hK₂c : IsClosed K₂) (hK₁Q : K₁ ⊆ Q) (hK₂Q : K₂ ⊆ Q) :
    hull01 (K₁ ∩ K₂) ⊆ Nplus K₁ K₂ ∧ Nplus K₁ K₂ ⊆ N K₁ K₂ ∧ N K₁ K₂ ⊆ K₁ ∩ K₂ := by sorry

end LovaszSchrijver.IntegerHull

Source

Lovász and Schrijver, Cones of matrices and set-functions and 0–1 optimization, SIAM J. Optim. 1(2) (1991), p. 170, Lemma 1.1

Read-back

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

Let $\iota$ be a finite type with decidable equality, and let $V_\iota = \mathbb{R}^{\{0\}\sqcup\iota}$ . Let $Q$ be the set of finite nonnegative combinations of vectors with all coordinates in $\{0,1\}$ and $0$ -th coordinate $1$ .

Let $K_1, K_2 \subseteq V_\iota$ each satisfy:

nonempty and closed under addition and nonnegative scaling;
topologically closed;
contained in $Q$ .

The statement asserts the chain

(K_1\cap K_2)^\circ \ \subseteq\ N_+(K_1,K_2) \ \subseteq\ N(K_1,K_2) \ \subseteq\ K_1 \cap K_2,

where the terms mean the following.

$(K_1\cap K_2)^\circ$ is the set of all finite nonnegative combinations of vectors of $K_1\cap K_2$ whose coordinates (including $x_0$ ) all lie in $\{0,1\}$ . It always contains $0$ .
$N(K_1,K_2) = \{Y e_0 : Y \in M(K_1,K_2)\}$ $N (K_{1}, K_{2}) = {Y e_{0} : Y \in M (K_{1}, K_{2})}$ is the set of $0$ $0$ -th columns of matrices $Y$ $Y$ that satisfy:
- $Y$ is symmetric;
- $Y_{ii} = Y_{0i}$ for all $i \in \iota$ ;
- $u^\top Y v \ge 0$ for all $u \in K_1^*$ , $v \in K_2^*$ , where $K^* = \{u : u^\top x \ge 0\ \forall x \in K\}$ .
$N_+(K_1,K_2)$ is the same set, but with $Y$ additionally required to be positive semidefinite.

Degenerate cases:

Hypotheses are satisfiable. $K_1 = K_2 = \{0\}$ meets all of them.
No 0–1 vectors in the intersection. If $K_1\cap K_2$ contains no nonzero 0–1 vector, the first set is $\{0\}$ .
Empty $\iota$ . $V_\iota = \mathbb{R}$ , $Q = [0,\infty)$ , and each $K_j$ is $\{0\}$ or $[0,\infty)$ .

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