(4) in the proof of Theorem 1.4 — Nᵗ(K) ⊆ cone(K ∩ F̄)

Proved

LovaszSchrijver.IntegerHull.Niter_subset_cone_Fbar

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

convex-coneinteger-hulllift-and-projectp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $K \subseteq Q$ be a closed convex cone in $\mathbb R^{n+1}$ . "Consider the unit cube $Q'$ in the hyperplane $x_0 = 0$ [read: $x_0 = 1$ ] and let $1 \le t \le n$ . Consider any face $F$ of $Q'$ of dimension $n - t$ and let $\bar F$ be the union of faces of $Q'$ parallel to $F$ ." Such a face fixes a set $T$ of $t$ coordinates, so

\bar F = \{x : x_0 = 1,\ 0 \le x_i \le 1 \ (1 \le i \le n),\ x_i \in \{0, 1\} \ (i \in T)\}.

Then, for every nonempty set $T$ of $t = |T|$ coordinates,

N^t(K) \subseteq \operatorname{cone}(K \cap \bar F).

This is the induction claim (4) of the proof of Theorem 1.4: for $t = 1$ it is equivalent to Lemma 1.3, and for $t = n$ it is the nontrivial inclusion $N^n(K) \subseteq K^\circ$ of the theorem.

Formalization Note The page reads "in the hyperplane $x_0 = 0$ ", a misprint for $x_0 = 1$ (the cube's vertices are the 0–1 vectors with $x_0 = 1$ ). $\bar F$ is indexed by the set $T$ of fixed coordinates, which is all it depends on; $\operatorname{cone}$ is the span over nonnegative reals. $K$ is assumed closed, which the paper tacitly assumes (polyhedral in all its applications) and which the proof's use of Lemma 1.3 needs.

Preamble

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

Formal statement

namespace LovaszSchrijver.IntegerHull

theorem Niter_subset_cone_Fbar {ι : Type} [Fintype ι] [DecidableEq ι]
    (K : Set (Option ι → ℝ)) (hK : IsConvexCone K) (hKc : IsClosed K) (hKQ : K ⊆ Q)
    (T : Finset ι) (hT : T.Nonempty) :
    Niter T.card K ⊆ cone (K ∩ Fbar T) := 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. 172, (4) in the proof of Theorem 1.4 (with Q′, F, F̄ from p. 171)

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$ .

Let $T \subseteq \iota$ be a nonempty finite set with $t = |T|$ elements. The statement asserts

N^t(K) \ \subseteq\ \operatorname{cone}\big(K \cap \bar F_T\big),

where the terms mean the following.

The set $\bar F_T$ :

\bar F_T = \{x : x_0 = 1,\ 0 \le x_i \le 1 \ \forall i \in \iota,\ x_i \in \{0,1\}\ \forall i \in T\}.

$\operatorname{cone}(S)$ is the set of all finite nonnegative combinations of elements of $S$ , including $0$ . No closure is taken.
The iterates are

N^0(K) = K, \qquad N^{s+1}(K) = N\big(N^s(K), Q\big).

For arbitrary sets $A, B$ , $N(A,B)$ is the set of $0$ -th columns $Y e_0$ of matrices $Y$ that are symmetric, satisfy $Y_{ii} = Y_{0i}$ for all $i \in \iota$ , and satisfy $u^\top Y v \ge 0$ for all $u \in A^*$ , $v \in B^*$ . Here $A^* = \{u : u^\top x \ge 0\ \forall x \in A\}$ .
The intermediate iterates $N^s(K)$ are plugged in as arbitrary sets; no hypothesis is imposed on them.

Degenerate cases:

$t$ and $\iota$ . Since $T \ne \emptyset$ , $t \ge 1$ and $\iota$ is nonempty, so the case $N^0(K) = K$ is never used.
Empty intersection. If $K \cap \bar F_T = \emptyset$ , the right-hand side is $\{0\}$ .
$T = \iota$ . Then $\bar F_T$ consists of the 0–1 vectors with $x_0 = 1$ .
Hypotheses are satisfiable. $K = \{0\}$ meets them.

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