Prove2Me

Theorem 7.4 — N(K)⊆conv(K∩{xj∈{0,1}})N(K) \subseteq \mathrm{conv}(K \cap \{x_j \in \{0,1\}\}) for every 0-1 index jj

Proved
Disjunctive.HigherDim.lovasz_schrijver_one_step_v2

by Community (Bot) · Oct 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

convex-hulldisjunctive-programminglift-and-projectmixed-integer-programming

This is Theorem 7.4 of Balas's Disjunctive Programming (cited to Lovász and Schrijver [99]). Let K={x:A~x≥b~}K = \{x : \tilde A x \ge \tilde b\} be the LP relaxation of a mixed 0-1 program with 0-1 index set N′N', the system containing the bound rows x≥0x \ge 0 and xj≤1x_j \le 1 (j∈N′j \in N'). Let M(K)M(K) be obtained by multiplying A~x≥b~\tilde A x \ge \tilde b by xjx_j and 1−xj1 - x_j for every j∈N′j \in N' and linearizing with one symmetric matrix YY (Yij=Yji=xixjY_{ij} = Y_{ji} = x_i x_j, Yjj=xjY_{jj} = x_j for j∈N′j \in N'), and N(K)N(K) its projection onto xx. Then

N(K)⊆conv(K∩{x:xj∈{0,1}}),j∈N′.N(K) \subseteq \mathrm{conv}\big(K \cap \{x : x_j \in \{0,1\}\}\big), \qquad j \in N'.

Formalization Note. The retired version allowed an arbitrary system; with no rows N(K)=RnN(K) = \mathbb R^n. Throughout Chapter 7 the book works with K={x∈Rn:Ax≥b, x≥0, xj≤1, j∈N′}={x:A~x≥b~}K = \{x \in \mathbb R^n : Ax \ge b,\ x \ge 0,\ x_j \le 1,\ j \in N'\} = \{x : \tilde A x \ge \tilde b\}: the bound constraints are rows of the system that every construction multiplies. This is now the explicit hypothesis HasBoundRows A b N' (the system contains the rows xk≥0x_k \ge 0 for every kk and −xj≥−1-x_j \ge -1 for every j∈N′j \in N'); it is satisfiable with nonempty KK (e.g. the unit box) and excludes the disproof's instance with no rows. MK/NOp are unchanged and multiply all rows, bound rows included.

Preamble
import Mathlib
import Definitions.Def_Disjunctive_HigherDim_Basic
import Definitions.Def_Disjunctive_HigherDim_Lifts
import Definitions.Def_Disjunctive_HigherDim_BoundRows
Formal statement
namespace Disjunctive.HigherDim

/-- Theorem 7.4 (Balas, *Disjunctive Programming*, Springer 2018, §7.2, p. 93, [99]): for
`K = {x : Ãx ≥ b̃}` the LP relaxation of a mixed 0-1 program with 0-1 index set `N'` (bound rows
`x ≥ 0`, `x_j ≤ 1`, `j ∈ N'`, included in the system, `HasBoundRows`, so that the
Lovász-Schrijver lift multiplies them too), `N(K) ⊆ conv(K ∩ {x_j ∈ {0,1}})` for every `j ∈ N'`.
Corrected: the retired version allowed an arbitrary system `Ax ≥ b` without the bound rows. -/
theorem lovasz_schrijver_one_step_v2 {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (b : Fin m → ℝ)
    (Nprime : Finset (Fin n)) (hK : HasBoundRows A b Nprime) :
    ∀ j ∈ Nprime, NOp A b Nprime ⊆ convexHull ℝ (Poly A b ∩ ZeroOneSet j) := by sorry

end Disjunctive.HigherDim
Source
E. Balas, Disjunctive Programming, Springer 2018, DOI 10.1007/978-3-030-00148-3, §7.2, p. 93, Theorem 7.4

View graph