Lemma 1.3 — N(K) ⊆ (K ∩ Hᵢ) + (K ∩ Gᵢ)

Proved

LovaszSchrijver.IntegerHull.N1_subset_H_add_G

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

convex-conelift-and-projectmatrix-conep2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $K \subseteq Q$ be a closed convex cone in $\mathbb R^{n+1}$ , and let $1 \le i \le n$ . With $H_i = \{x : x_i = 0\}$ and $G_i = \{x : x_i = x_0\}$ ,

N(K) \subseteq (K \cap H_i) + (K \cap G_i),

where $+$ is the Minkowski sum $\{y + z : y \in K\cap H_i,\ z \in K \cap G_i\}$ and $N(K) = N(K, Q)$ .

This is the geometric property of $N(K)$ : every point of $N(K)$ splits into a point of $K$ on the facet $x_i = 0$ of $Q$ and a point of $K$ on the opposite facet $x_i = x_0$ . It is the base case ( $t = 1$ ) of the induction proving Theorem 1.4.

Formalization Note The paper's proof goes through (iii″), which needs $K$ closed; the paper tacitly takes $K$ closed (polyhedral in all its applications), and the hypothesis is added. Without it the statement fails (for the cone $\{x : 0 < x_1 < x_0\} \cup \{0\}$ in $\mathbb R^2$ , $N(K) = Q$ while the right-hand side is $\{0\}$ ).

Preamble

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

Formal statement

namespace LovaszSchrijver.IntegerHull

theorem N1_subset_H_add_G {ι : Type} [Fintype ι] [DecidableEq ι]
    (K : Set (Option ι → ℝ)) (hK : IsConvexCone K) (hKc : IsClosed K) (hKQ : K ⊆ Q) (i : ι) :
    N1 K ⊆ (K ∩ H i) + (K ∩ G i) := 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. 171, Lemma 1.3

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 \subseteq V_\iota$ satisfy:

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

Fix a coordinate $i \in \iota$ . The statement asserts

N(K,Q) \ \subseteq\ (K \cap H_i) + (K \cap G_i),

where the terms mean the following.

$H_i = \{x : x_i = 0\}$ and $G_i = \{x : x_i = x_0\}$ .
The sum is the Minkowski sum $\{a + b : a \in K\cap H_i,\ b \in K \cap G_i\}$ .
$N(K,Q) = \{Y e_0 : Y \in M(K,Q)\}$ $N (K, Q) = {Y e_{0} : Y \in M (K, Q)}$ is the set of $0$ $0$ -th columns of matrices $Y$ $Y$ that satisfy:
- $Y$ is symmetric;
- $Y_{jj} = Y_{0j}$ for all $j \in \iota$ ;
- $u^\top Y v \ge 0$ for all $u \in K^*$ , $v \in Q^*$ , where $K^* = \{u : u^\top x \ge 0\ \forall x \in K\}$ and $Q^*$ is defined likewise.

Degenerate cases:

Nonempty $\iota$ . The existence of $i$ forces $\iota$ to be nonempty.
Hypotheses are satisfiable. $K = \{0\}$ meets them. In that case the right-hand side is $\{0\}$ , and the statement asserts $N(\{0\},Q) \subseteq \{0\}$ .

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