(iii″) — for K₂ = Q, condition (iii) says the columns of Y and the first-column differences lie in K

Proved

LovaszSchrijver.IntegerHull.mem_M_Q_iff_columns

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 $Y$ be an $(n+1)\times(n+1)$ real matrix that is symmetric and satisfies $y_{ii} = y_{0i}$ for $1 \le i \le n$ (conditions (i) and (ii)). Write $Y e_j$ for the $j$ th column of $Y$ ( $0 \le j \le n$ ). Then $Y \in M(K, Q)$ if and only if

Y e_j \in K \ \ (0 \le j \le n) \qquad\text{and}\qquad Y e_0 - Y e_i \in K \ \ (1 \le i \le n).

In the paper's words: "In this case, $K_2^* = Q^*$ is generated by the vectors $e_i$ and $f_i$ [where $f_i = e_0 - e_i$ ], and hence (iii′) has the following convenient form: (iii″) Every column of $Y$ is in $K$ ; the difference of the first column and any other column is in $K$ ."

This column description of $M(K)$ is the working form of condition (iii) used in the proofs of Lemmas 1.3 and 1.5.

Formalization Note Coordinates are indexed by Option ι, with none the 0th coordinate; the "first column" is column none. The paper derives (iii″) from the rewriting (iii′) $YK_2^* \subseteq K_1$ , which uses $K^{**} = K$ ; the paper tacitly takes $K$ closed (polyhedral in all its applications), and the hypothesis IsClosed K is added for this reason.

Preamble

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

Formal statement

namespace LovaszSchrijver.IntegerHull

theorem mem_M_Q_iff_columns {ι : Type} [Fintype ι] [DecidableEq ι]
    (K : Set (Option ι → ℝ)) (hK : IsConvexCone K) (hKc : IsClosed K) (hKQ : K ⊆ Q)
    (Y : Matrix (Option ι) (Option ι) ℝ) (hY_symm : Y.IsSymm)
    (hY_diag : ∀ i : ι, Y (some i) (some i) = Y none (some i)) :
    Y ∈ M K Q ↔
      (∀ j : Option ι, Y *ᵥ Pi.single j 1 ∈ K) ∧
        ∀ i : ι, Y *ᵥ Pi.single none 1 - Y *ᵥ Pi.single (some i) 1 ∈ 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, Section 1.a, (iii″)

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}$ with coordinates $x_0$ and $(x_i)_{i\in\iota}$ . Let $Q \subseteq V_\iota$ be the set of all finite nonnegative combinations of vectors whose coordinates are all in $\{0,1\}$ and whose $0$ -th coordinate is $1$ .

Let $K \subseteq V_\iota$ satisfy:

$K$ is nonempty and closed under addition and under multiplication by every real $c \ge 0$ ;
$K$ is topologically closed;
$K \subseteq Q$ .

Let $Y$ be a real matrix indexed by $\{0\}\sqcup\iota$ such that:

$Y$ is symmetric;
$Y_{ii} = Y_{0i}$ for every $i \in \iota$ .

For $j \in \{0\}\sqcup\iota$ , let $Y e_j$ denote the $j$ -th column of $Y$ .

The statement asserts:

Y \in M(K,Q) \iff \Big(Y e_j \in K \text{ for every } j \in \{0\}\sqcup\iota\Big) \ \text{and}\ \Big(Y e_0 - Y e_i \in K \text{ for every } i \in \iota\Big).

Here $M(K,Q)$ is the set of symmetric matrices $Y$ with $Y_{ii} = Y_{0i}$ for all $i \in \iota$ and with

u^\top Y v \ge 0 \quad \text{for all } u \in K^*,\ v \in Q^*.

In this expression, $K^* = \{u : u^\top x \ge 0\ \forall x \in K\}$ , and $Q^*$ is defined likewise. Because symmetry and the diagonal condition are assumed as hypotheses, the left-hand side holds exactly when the inequality condition holds.

Degenerate cases:

The hypotheses are satisfiable. For example, $K = \{0\}$ and $Y = 0$ meet all of them.
$K = \{0\}$ . Then $K^* = V_\iota$ , and the right-hand side requires every column of $Y$ to be $0$ .
Empty $\iota$ . Then $V_\iota = \mathbb{R}$ , $Q = [0,\infty)$ , and $K$ is $\{0\}$ or $[0,\infty)$ . $Y$ is a $1\times1$ matrix $(y)$ on which the hypotheses impose nothing. The right-hand side reduces to $y \in K$ , since the second conjunct 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