Linear Optimization

Motivation

Finding a point that satisfies a finite system of linear inequalities is the feasibility problem underlying linear programming, and it is also the basic step of many methods in signal and image reconstruction, where the system is too large to be solved by elimination. The relaxation method attacks it one inequality at a time: from the current point, move towards the half-space that is violated the most. Each step costs one pass over the rows and no factorization, which is why this family of iterations (with its relatives: Kaczmarz's method for equations, the projection methods for convex feasibility, and the perceptron algorithm) has been studied continuously since the early 1950s.

Timeline:

• 1922. Fejér observes that the set of points of $E_n$ that no other point dominates in distance to a closed set $A$ is the convex hull of $A$ (Motzkin and Schoenberg 1954, p. 393). This idea of moving to a point that is closer to every point of $A$ drives the method.
• 1954. Agmon (Canad. J. Math. 6, 382–392) proves that for a relaxation parameter $0 < \lambda < 2$ the iterates either reach the solution set or converge to a point on its boundary.
• 1954. Motzkin and Schoenberg (Canad. J. Math. 6, 393–404) reprove Agmon's theorem from a single lemma about Fejér-monotone sequences and treat the extreme case $\lambda = 2$, the reflexion method. When the solution set has full dimension, reflexion always stops after finitely many steps; no parameter $0 < \lambda < 2$ has this property.

This mission is the first of three built on the Motzkin–Schoenberg paper: it covers the full-dimensional case, Theorem 1.

Setting

Let $E_n$ be $n$-dimensional Euclidean space. A system of $m$ linear inequalities

$$\sum_{j=1}^n a_{ij}x_j + b_i \ge 0 \qquad (i = 1, \dots, m)$$

is given by rows $a_i \in E_n$ and constants $b_i \in \mathbb R$. The $i$-th inequality defines the closed half-space $H_i = \{x : \langle a_i, x\rangle + b_i \ge 0\}$, and the set of solutions is the polytope $A = \bigcap_{i=1}^m H_i$. The system is assumed consistent, so $A$ is nonempty. The dimension $r$ of $A$ is the dimension of its affine hull; $r = n$ means that $A$ is not contained in any hyperplane.

Fix a relaxation parameter $\lambda$ with $0 < \lambda \le 2$. From a point $p \notin A$ one relaxation step is:

1. choose $j$ with $\operatorname{dist}(p, H_j) = \max_i \operatorname{dist}(p, H_i)$, a farthest half-space;
2. let $q \in H_j$ be the point with $|p - q| = \operatorname{dist}(p, H_j)$;
3. set $p_1 = p + \lambda (q - p)$.

For $\lambda = 2$, $p_1$ is the mirror image of $p$ in the boundary hyperplane of $H_j$. Iterating from a starting point $p_0$ gives a sequence $p_0, p_1, p_2, \dots$; the process terminates when some $p_N \in A$, and otherwise produces an infinite sequence of points outside $A$.

A sequence $q_0, q_1, \dots$ of points outside $A$ is Fejér-monotone with respect to $A$ if $q_i \ne q_{i+1}$ and $|q_{i+1} - a| \le |q_i - a|$ for all $a \in A$ and all $i$.

Formalization targets

Goal: Theorem 1 (p. 395)

Assume $A \ne \emptyset$ and $r = n$. For every starting point and every choice of farthest half-space at every step:

$$\text{Case 1: } 0 < \lambda < 2 \implies \big(\exists N,\ p_N \in A\big) \ \lor\ \big(p_\nu \to l \text{ for some } l \in \partial A\big),$$ $$\text{Case 2: } \lambda = 2 \implies \exists N,\ p_N \in A .$$

The goal is the paper's theorem as stated, both cases in one statement. It fixes no constants and no rates.

Milestones

1. §1, pp. 393–394. For $p \notin H_j$, $q$ the point of $H_j$ nearest to $p$ and $p_1 = p + \lambda(q - p)$ with $0 < \lambda \le 2$: $p_1 \ne p$ and $|p_1 - a| \le |p - a|$ for all $a \in A$, strictly when $\lambda < 2$; for $\lambda = 2$ equality holds exactly at the points of $A$ on the boundary $\pi_j$ of $H_j$. Stated for any violated half-space, as on the page, so it covers every relaxation step.
2. §5, p. 398. An infinite relaxation sequence is Fejér-monotone with respect to $A$.
3. Lemma 1, Case 1, p. 397. If $A$ has dimension $n$, every Fejér-monotone sequence converges to a point.
4. §5, p. 399. The limit of a convergent infinite relaxation sequence lies on the boundary of $A$.

Significance

The result. Case 1 guarantees that the relaxation method never diverges or oscillates: it either solves the system or converges to a boundary solution. Case 2 gives more: for full-dimensional solution sets the reflexion method is a finite algorithm for linear feasibility. Remark 3(b) of the paper shows that this is special to $\lambda = 2$: for each $0 < \lambda < 2$ there are planar examples where the iteration never stops. The companion missions of this series treat $r < n$ (Theorem 2, where reflexion may settle on a sphere around the affine hull of $A$) and reflexion in a general bounded convex set (Theorem 3).

Formalizing it. Both cases are proved in the paper; to our knowledge none is formalized in Lean or Mathlib. The mission produces a reusable model of relaxation for linear inequalities and a Lean proof of a general convergence statement for Fejér-monotone sequences, which also applies to other projection methods. Formalizing the proof in the order of the paper (Lemma 1, then §§5–6) is the intended route; alternative proofs are welcome.

Difficulty

The first idea is that monotone distances to every point of $A$ force convergence. They do not in general: Fejér-monotonicity only bounds the sequence and makes each distance $|q_\nu - a|$ converge, and when $A$ lies in a hyperplane a Fejér-monotone sequence can keep oscillating between two mirror-image points. Convergence genuinely needs the full dimension of $A$, and the formal argument has to use that hypothesis in an essential way.

For Case 2, the difficulty is that a reflexion step does not shrink the distance to points of $A$ on the reflecting hyperplane, so there is no uniform decrease to count. Termination must also use that the system has finitely many inequalities: for the infinite family of supporting half-spaces of a convex body, treated in the third mission of this series, reflexion need not terminate. A proof that works for a single step, or one that uses a fixed tie-breaking rule, does not cover the statement.

Formalization scope

• The space is EuclideanSpace ℝ (Fin n); the rows are vectors a i, and $\sum_j a_{ij} x_j$ is inner ℝ (a i) x. Half-spaces are closed. Distances to sets are Metric.infDist.
• The relaxation step is a relation IsRelaxStep a b lam p p', and any maximizing index $j$ is allowed at every step. The paper makes the step single-valued by "some pre-assigned rule"; quantifying over all runs of the relation covers every such rule, so each theorem is at least as strong as the paper's.
• A run is a sequence p : ℕ → E in which each point outside $A$ is followed by a relaxation step (IsRelaxRun). Termination is ∃ N, p N ∈ A; an infinite sequence is ∀ ν, p ν ∉ A. Every theorem is stated for every run, never for one run.
• The parameter $\lambda$ is named lam, because λ is a Lean keyword.
• Nonemptiness of $A$ ("assumed from the outset not to be void") is an explicit hypothesis. $r = n$ is affineSpan ℝ A = ⊤, following the paper's own gloss "$A$ is not contained in any hyperplane". "Boundary" is frontier A, and convergence is Tendsto p atTop (𝓝 l).
• Lemma 1, Case 1 is stated for an arbitrary set $A$ with affineSpan ℝ A = ⊤, which includes the paper's polytope.
• The milestones of §5 (Fejér-monotonicity of the sequence, the limit on the boundary) are stated for $0 < \lambda \le 2$ and without the dimension hypothesis. The paper proves them in §5 for $0 < \lambda < 2$ and reuses the same argument in §6 for $\lambda = 2$.
• Rows with $a_i = 0$ are allowed (they give $H_i = E_n$ once $A \ne \emptyset$); no nondegeneracy hypothesis is imposed.
• Ruled out: a formalization of Case 2 that asserts termination for some starting point or some choice of indices, or one whose run hypothesis cannot be satisfied, would be vacuous. A relaxation step exists from every point outside a nonempty $A$, so the statement constrains every sequence the method can produce.

Useful infrastructure: the closed form $\operatorname{dist}(p, H) = \max(0, -(\langle u, p\rangle + c))/|u|$ for $u \ne 0$ and the nearest point in a half-space; the characterization of $\operatorname{affineSpan} = \top$ via a nonempty interior for convex sets. The Fejér-monotone convergence lemma and the half-space projection lemmas are reusable beyond this mission.

Selected references

• T. S. Motzkin and I. J. Schoenberg, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6 (1954), 393–404. https://doi.org/10.4153/CJM-1954-038-x
• S. Agmon, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6 (1954), 382–392. https://doi.org/10.4153/CJM-1954-037-2
• H. H. Bauschke and J. M. Borwein, On projection algorithms for solving convex feasibility problems, SIAM Review 38 (1996), 367–426. https://doi.org/10.1137/S0036144593251710

Motivation

Convexity is what makes optimization tractable: a linear program's feasible region is convex, and this single fact underwrites the simplex method, LP duality, and everything built on top of them. Integer and disjunctive programs have no such luck — their feasible regions are unions of polyhedra, and a union of convex sets is generally not convex. If the convex hull of such a union could always be described compactly, integer programming would reduce to linear programming: optimize the same linear objective over the hull instead of the union, and any optimal vertex of the hull is automatically integral. The obstacle has always been that the convex hull of a union of polyhedra in $\mathbb{R}^n$, described directly by its facets in $\mathbb{R}^n$, typically needs exponentially many inequalities.

Balas's Theorem 2.1, proved in the 1970s and presented here as Chapter 2 of Disjunctive Programming (Balas, Springer 2018), breaks this exponential barrier by changing where the description lives. Rather than writing down the hull's facets in $\mathbb{R}^n$, Theorem 2.1 lifts the problem to a higher-dimensional space — one auxiliary copy of $\mathbb{R}^n$ per polyhedron in the union — where the hull becomes the projection of a single, explicitly given polyhedron whose size grows only linearly with the number of polyhedra. This "extended formulation" technique, born here, became one of the central tools of modern integer programming and combinatorial optimization: representing a hard polytope as the projection of an easy one in higher dimension underlies, for instance, the polynomial-size extended formulations known for many combinatorial polytopes.

Setting

Fix a finite index set $Q$. For $h \in Q$, let $A_h$ be a real matrix and $b_h$ a vector of matching row dimension, and set $P_h := \{x \in \mathbb{R}^n : A_h x \ge b_h\}$. The union $F := \bigcup_{h \in Q} P_h$ is the disjunctive set. Write $Q^* := \{h \in Q : P_h \ne \emptyset\}$ for the feasible disjuncts.

The recession cone of a nonempty polyhedron $P_h$ is $C_h := \{y : A_h y \ge 0\}$: the set of directions along which one can travel indefinitely from any point of $P_h$ while remaining in $P_h$. For a subset $M \subseteq Q$ and sets $S_h$ ($h \in M$), the (finite) Minkowski sum $\sum_{h \in M} S_h$ is $\{x : x = \sum_{h \in M} y^h \text{ for some } y^h \in S_h\}$. The maximal indices $Q^{**} \subseteq Q^*$ are the feasible disjuncts whose polyhedron is not contained in any other feasible disjunct's polyhedron.

Given a set $S \subseteq \mathbb{R}^n \times \beta$, its projection onto $x$ is $\mathrm{Proj}_x(S) := \{x : \exists\, y \in \beta,\ (x,y) \in S\}$.

Formalization targets

Theorem 2.1 (goal) — the convex hull of a disjunctive set

$$\mathrm{cl}\,\mathrm{conv}(F) = \mathrm{Proj}_x(P), \qquad P := \Big\{(x, \{y^h\}_{h \in Q^*}, \{y^h_0\}_{h \in Q^*}) : x = \!\!\sum_{h \in Q^*}\!\! y^h,\ A_h y^h - b_h y^h_0 \ge 0,\ y^h_0 \ge 0,\ \!\!\sum_{h \in Q^*}\!\! y^h_0 = 1 \Big\}.$$

This is the weakest correct statement: it claims only that the closed convex hull equals the projection of this specific lifted polyhedron $P$, not any stronger uniqueness or minimality claim about lifted representations in general (that refinement is Theorem 2.1's own follow-up discussion, not part of the theorem itself).

Corollary 2.2 — the extreme-point correspondence

Extreme points of $\mathrm{cl}\,\mathrm{conv}(F)$ correspond bijectively to the extreme points of $P$ that place all of their mass on a single disjunct's coordinates.

Theorem 2.3 — tightness of the lifted representation

$$P_Q = P \iff C_k \subseteq \sum_{h \in Q^*} C_h \quad \forall\, k \in Q \setminus Q^*,$$

where $P_Q$ is the variant of $P$ indexed by all of $Q$ rather than only $Q^*$.

Theorem 2.4 — from the convex hull to the union itself

Under two recession-cone conditions on $Q^{**}$, restricting $P_Q$'s $y^h_0$ variables to $\{0,1\}$ makes its $x$-projection recover $F$ itself, not merely $\mathrm{cl}\,\mathrm{conv}(F)$.

Significance

The result itself. Theorem 2.1 is the founding extended-formulation result of integer programming: it shows that every union of finitely many polyhedra — hence every mixed-integer program's feasible region, once expressed in disjunctive normal form — has a lifted description of size linear in the number of disjuncts, in stark contrast to the union's own facet description, which is generally exponential. Corollary 2.2 shows this lifting is not merely an upper bound with extraneous points: its extreme points correspond exactly, one-to-one, with the extreme points of the object it represents. Theorems 2.3 and 2.4 sharpen the picture: 2.3 tells you exactly when you can avoid knowing in advance which disjuncts are nonempty, and 2.4 tells you exactly when the same family of lifted systems, restricted to integral $y^h_0$, describes the union $F$ exactly rather than only its convex hull — this is Jeroslow and Lowe's characterization of when a disjunctive set is representable as the feasible region of an integer program at all.

Formalizing it. No object in this mission — the disjunctive set $F$, its lifted polyhedron $P$, recession cones of a union's components, or the extreme-point correspondence between a polytope and its lift — exists on the platform prior to this mission or anywhere in Mathlib (substrate.md records zero LP/polyhedron modules in Mathlib as of this writing). This mission is a from-scratch formalization of the book's central construction, restating (rather than importing) the disjunctive-set vocabulary introduced by the companion IntroDuality mission, per the series' convention that a draft mission cannot import another draft mission's definitions.

Difficulty

The natural first attempt at Theorem 2.1 tries to prove the two inclusions $\mathrm{cl}\,\mathrm{conv}(F) \subseteq \mathrm{Proj}_x(P)$ and $\mathrm{Proj}_x(P) \subseteq \mathrm{cl}\,\mathrm{conv}(F)$ by a direct facet-by-facet or vertex-by-vertex argument in $\mathbb{R}^n$ — exactly the exponential-size approach the theorem exists to avoid. The book's own first proof instead works entirely with convex combinations: an arbitrary point of $\mathrm{cl}\,\mathrm{conv}(F)$ is a combination of at most $|Q^*|$ points, one from each polyhedron in the union (Carathéodory-style), which converts directly into a point of $P$ by splitting the combination's weight across the lifted coordinates — and conversely, a point of $P$ decomposes, disjunct by disjunct, into a convex combination of that disjunct's own vertices and extreme rays. Neither direction ever needs to enumerate facets of $\mathrm{cl}\,\mathrm{conv}(F)$ in $\mathbb{R}^n$. The second proof (via projection and the polar cone $W$ of the lifted system) shows the projected inequalities coincide with exactly the valid-inequality characterization of Theorem 1.2 (disjunctive Farkas), which is a different, complementary way of seeing why no facet of $\mathrm{cl}\,\mathrm{conv}(F)$ is missed.

Formalization scope

All theorems are stated over a finite index set Q : Type* with [Fintype Q], matrices Matrix (Fin (m h)) (Fin n) ℝ with m : Q → ℕ allowed to depend on h, and vectors in Fin n → ℝ. DisjunctiveSet, FeasibleIndices, MaximalIndices, RecessionCone, and MinkowskiSumOver fix the chapter's vocabulary; ProjX, LiftedPolyhedron, and IntegerRestricted fix the lifted system and its variants. cl conv F is Mathlib's closure (convexHull ℝ ·); extreme points use Mathlib's Set.extremePoints.

LiftedPolyhedron ranges its auxiliary vectors $\{y^h\}$, $\{y^h_0\}$ over all of $Q$ rather than only the index subset Qidx the book restricts to, forcing the components outside Qidx to zero. This is an equivalent, Finset/decidability-free encoding — appending zero terms changes neither the defining sums nor the constraints — documented as a convention, not a weakening, in MODERATION_NOTES.md; the same definition instantiates both the $(2.1)$ system (Qidx = Q^*) and the $(2.1)_Q$ variant (Qidx = Q) that Theorem 2.3 compares.

A trivializing formalization is ruled out explicitly: taking $|Q^*| = 1$ collapses the lifted system to $x = y^1$, $y^1_0 = 1$, a vacuous restatement of $x \in P_1$ that proves nothing about unions. Every theorem here is stated for a generic finite Q, never specialized to a fixed small size. Contributions beyond this mission's statements would need genuine polyhedral machinery (vertex/extreme-ray decomposition of a polyhedron, Carathéodory's theorem for cones) that is itself absent from Mathlib and would be welcome as a separate, reusable definitions layer.

Selected references

• E. Balas, Disjunctive Programming, Springer, 2018. DOI: 10.1007/978-3-030-00148-3, Chapter 2, §2.1.
• E. Balas, Disjunctive programming: Properties of the convex hull of feasible points, Discrete Applied Mathematics 89 (1998), 3–44 (reprint of a 1974 MSRR, cited in the text as [6], the origin of Theorem 2.1).
• M. Conforti, M. Di Summa, Y. Faenza, On the size of extended formulations for polytopes associated with unions of polyhedra, SIAM Journal on Discrete Mathematics, cited in the text as [59] — establishes the tightness (minimum additional-variable count) of Theorem 2.1's lifted representation.
• R. G. Jeroslow, J. K. Lowe, Modelling with integer variables, Mathematical Programming Study 22 (1984), 167–184 (cited in the text as [86]; the characterization behind Theorem 2.4's significance).

Motivation

Linear programming duality is one of the load-bearing facts of optimization: every feasible linear program has a dual whose value matches the primal's, and this correspondence drives the simplex method's stopping criterion, sensitivity analysis, and most complexity results for polyhedral problems. Integer and mixed-integer programs have no such duality theorem in general — the feasible region of a mixed-integer program is not convex, and the entire apparatus of linear programming duality is built on convexity.

Disjunctive programming, introduced by Egon Balas in the early 1970s, closes part of this gap. A disjunctive set is a union of finitely many polyhedra rather than a single polyhedron — the natural convex-analytic shadow of the "either/or" logical structure that integer variables encode (an integer variable's feasible region is a finite union of half-open pieces, hence a disjunction of the linear constraints that pin it to each value). Balas's insight was that disjunctive programs — linear programs whose feasible region is such a union — admit a strong duality theorem of their own, generalizing the linear-programming case rather than replacing it. This mission formalizes that theorem (Theorem 1.5 of Balas, Disjunctive Programming, Springer 2018) together with the two results the same chapter builds around it: the founding construction of the field, the intersection cut (Theorem 1.1, circa 1970), and the disjunctive generalization of Farkas' Lemma (Theorem 1.2), which characterizes every valid inequality — hence every cutting plane — for a disjunctive set.

Setting

Fix a finite index set $Q$. For each $h \in Q$, let $A_h$ be a real $m_h \times n$ matrix and $b_h \in \mathbb{R}^{m_h}$, and set $P_h := \{x \in \mathbb{R}^n : A_h x \ge b_h\}$. The union $F := \bigcup_{h \in Q} P_h$ is a disjunctive set: any (linear) system of inequalities combined with the logical connectives "and", "or", "not" reduces, via its disjunctive normal form, to a set of exactly this shape. Because a union of convex sets need not be convex, $F$ is generally nonconvex even though each $P_h$ is a polyhedron.

A disjunctive program minimizes a linear objective over such a union:

$$(DP)\qquad z_0 = \min\Big\{ c x : x \in \textstyle\bigcup_{h \in Q} X_h \Big\}, \qquad X_h := \{x : A_h x \ge b_h,\ x \ge 0\}.$$

Its dual $(DD)$ pairs a scalar $w$ with one dual multiplier vector $u_h$ per disjunct, requiring $w \le u_h b_h$ and $u_h A_h \le c$, $u_h \ge 0$, simultaneously for every $h \in Q$, and maximizes $w$. Write $Q^* := \{h \in Q : X_h \ne \emptyset\}$ for the disjuncts whose primal system is feasible, and $Q^{**} := \{h \in Q : U_h \ne \emptyset\}$ (with $U_h := \{u_h \ge 0 : u_h A_h \le c\}$) for those whose dual system is feasible.

The theorems below also use two objects from the origin of the subject (§1.2): given a basic solution $\bar x$ of a linear program's optimal simplex tableau, with basic index set $I$ and nonbasic index set $J$, the tableau's coefficients $\bar a_{ij}$ ($i \in I$, $j \in J$) determine, for each nonbasic $j$, an extreme ray direction $r^j$ of the associated LP cone. A convex set $S$ is $P_I$-free at $\bar x$ if $\bar x$ lies in the interior of $S$ and that interior contains no point of the mixed-integer feasible set $P_I$.

Formalization targets

Theorem 1.1 — the intersection cut

$$\lambda^*_j := \max\{\lambda_j \ge 0 : \bar x + \lambda_j r^j \in S\}, \qquad \sum_{j \in J} \frac{1}{\lambda^*_j}\, x_j \ge 1.$$

The displayed inequality cuts off $\bar x$ but excludes no point of $P_I$, for any $P_I$-free convex set $S$ containing $\bar x$ in its interior.

Theorem 1.2 — Farkas' Lemma for Disjunctive Sets

$$\big(\forall x \in F,\ \alpha x \ge \alpha_0\big) \iff \big(\forall h \in Q^*,\ \exists\, u_h \ge 0,\ u_h A_h = \alpha,\ \alpha_0 \le u_h b_h\big).$$

Theorem 1.5 (goal) — duality for disjunctive programs

Under the Regularity Condition — $(Q^* \ne \emptyset$ and $Q \setminus Q^{**} \ne \emptyset) \Rightarrow Q^* \setminus Q^{**} \ne \emptyset$ — exactly one of:

1. both $(DP)$ and $(DD)$ are feasible, each attains an optimum, and $z_0 = w_0$; or
2. one of the two is infeasible, and the other is infeasible or has no finite optimum.

This is the weakest faithful statement of the theorem: it asserts only the shape of the dichotomy established by Balas, not any strengthened or specialized form of it.

Corollary 1.6 — necessity of the Regularity Condition

If the Regularity Condition fails, $(DP)$ is feasible, and $(DD)$ is infeasible, then $(DP)$ still has a finite minimum — exhibiting the duality gap that opens up once the condition is dropped.

Significance

The results themselves. Theorem 1.5 is the mission-critical fact that makes disjunctive programming a genuine extension of linear programming rather than an unrelated combinatorial device: every LP-duality-based algorithmic tool (bounding, sensitivity, complementary-slackness optimality certificates) has a disjunctive-programming counterpart because of this theorem. Theorem 1.1's intersection cut is the historical seed of an entire branch of integer-programming algorithms — lift-and-project cuts, mixed-integer Gomory cuts, and the split closure (later missions of this series) all specialize or generalize it. Theorem 1.2 is the structural fact that makes cutting-plane generation for disjunctive sets tractable at all: every valid inequality decomposes into per-disjunct Farkas certificates.

Formalizing it. None of these results, nor the union-of-polyhedra machinery they are stated over, exist on the platform prior to this mission: the platform's existing Farkas' Lemma and linear-programming strong duality theorems (SmaleNinth.farkas_lemma, SmaleNinth.lp_strong_duality) are the ordinary single-polyhedron statements, which is exactly the special case $|Q|=1$ of the theorems formalized here — genuinely different statements, not restatements. This mission is a from-scratch formalization of the disjunctive generalization, including the vocabulary (disjunctive sets, the paired primal/dual index sets $Q^*, Q^{**}$, the Regularity Condition) that the rest of the fifteen-mission Balas series builds on.

Difficulty

The obvious first attempt collapses the disjunctive dual $(DD)$ to $|Q|$ separate ordinary LP duals, one per disjunct, and tries to combine their individual strong-duality statements. This fails: $(DD)$ couples all disjuncts through the single shared scalar $w$, which must simultaneously satisfy $w \le u_h b_h$ for every $h \in Q$ at once, not disjunct-by-disjunct. The Regularity Condition exists precisely because this coupling can break down — Balas's own example (a two-term disjunctive program with an infeasible dual but a feasible, bounded primal) shows that without the condition, situation (2) of the dichotomy can fail: the primal can have a finite optimum with no matching dual optimum. Any formalization that omits the Regularity Condition, or weakens it to an informal restriction like "nondegenerate", either proves a false statement or proves nothing (a vacuous hypothesis), which Corollary 1.6 exists specifically to rule out.

Formalization scope

All three theorems are stated over a finite index set Q : Type* with [Fintype Q], real matrices Matrix (Fin (m h)) (Fin n) ℝ with row-dimension m : Q → ℕ allowed to depend on h (the book never assumes a common row count across disjuncts), and vectors in Fin n → ℝ. Poly, PolyNonneg, and DualPoly are the plain, nonnegative-orthant, and dual polyhedral systems respectively; FeasibleIndices and RegularityCondition pin $Q^*$/$Q^{**}$ and the Regularity Condition exactly as stated on p. 13. "No finite optimum" is formalized via UnboundedBelowOn / UnboundedAboveOn: nonempty (feasible) together with no finite bound on the objective, matching Balas's case (2), which explicitly distinguishes infeasibility from unboundedness.

A trivializing formalization is ruled out explicitly: fixing $|Q| = 1$ collapses Theorem 1.5 to ordinary LP duality (already on the platform) and Theorem 1.2 to ordinary Farkas' Lemma, so both theorems are stated for a generic finite Q, never specialized. Theorem 1.5's "exactly one of" dichotomy is formalized as a logical Xor of the two situations, not a weaker Or, since the book asserts mutual exclusivity, not merely that one holds.

The intersection-cut theorem (1.1) is formalized over a generic finite index type ι standing for the full set of structural and surplus variables, with I J : Finset ι the basic/nonbasic partition; a complete development would additionally need the simplex-tableau apparatus connecting ι, I, J, and abar to an actual linear program, which lies outside this mission and belongs instead to the tableau-focused later missions of the series (SimplexTableau, RayCGLP). The extremeRay and PIFree definitions introduced here are local to this mission and are restated, not imported, by later missions that need related vocabulary — per the series' convention that a draft mission cannot import another draft mission's definitions.

Selected references

• E. Balas, Disjunctive Programming, Springer, 2018. DOI: 10.1007/978-3-030-00148-3, Chapter 1.
• E. Balas, Intersection cuts — a new type of cutting planes for integer programming, Operations Research 19 (1971), 19–39. (Theorem 1.1's origin, cited in the text as [4].)
• E. Balas, Disjunctive programming, Annals of Discrete Mathematics 5 (1979), 3–51. (Cited in the text as [9], the origin of Theorem 1.5.)

Motivation

A 0–1 integer program asks for the best 0–1 vector satisfying a system of linear inequalities. Its linear relaxation is easy to optimize over, but the relaxation is usually much larger than the convex hull of the 0–1 solutions. Lift-and-project methods close this gap systematically: they lift the relaxation to a higher-dimensional space, add constraints that every 0–1 point satisfies there, and project back, obtaining a tighter relaxation that still contains every 0–1 solution.

L. Lovász and A. Schrijver introduced one of the two standard lift-and-project hierarchies in Cones of matrices and set-functions and 0–1 optimization (SIAM J. Optim., 1991). Their operators $N$ and $N_+$ represent a 0–1 point $x$ by the matrix $xx^{\mathsf T}$, impose linear (and for $N_+$ semidefinite) constraints on such matrices, and project back to $\mathbb R^{n+1}$. The same paper applies the operators to the stable set polytope, where one round already produces the odd hole, odd wheel, clique and odd antihole constraints. The Lovász–Schrijver hierarchy, the Sherali–Adams hierarchy (1990) and Lasserre's semidefinite hierarchy (2001) are the three reference lift-and-project methods; their rank lower bounds are a standard tool for proving that a relaxation cannot solve a combinatorial problem in few rounds.

This mission formalizes the first structural fact about the operator $N$: iterating it $n$ times on any relaxation in $n$ variables yields exactly the 0–1 hull (Theorem 1.4 of the paper).

Setting

Vectors live in $\mathbb R^{n+1}$ with coordinates $x_0, x_1, \dots, x_n$; the space $\mathbb R^n$ of the original problem is the hyperplane $x_0 = 1$, and polytopes are replaced by the convex cones they generate.

• A convex cone is a nonempty set closed under addition and nonnegative scaling. For a set $S$, $\operatorname{cone}(S)$ is the set of nonnegative combinations of finitely many vectors of $S$.
• The polar cone of $K$ is $K^* = \{u : u^{\mathsf T}x \ge 0 \text{ for all } x \in K\}$.
• A 0–1 vector has every coordinate, $x_0$ included, equal to $0$ or $1$. The cube cone $Q$ is the cone spanned by the 0–1 vectors with $x_0 = 1$; it is the cone over the unit cube.
• For a convex cone $K$, $K^\circ$ is the cone spanned by the 0–1 vectors in $K$. For $K \subseteq Q$ this is the cone over the convex hull of the 0–1 points of the relaxation.

For convex cones $K_1, K_2 \subseteq Q$, the matrix cone $M(K_1, K_2)$ consists of the $(n+1)\times(n+1)$ real matrices $Y = (y_{ij})$ such that

1. $Y$ is symmetric;
2. $y_{ii} = y_{0i}$ for $1 \le i \le n$ (the diagonal equals the 0th column);
3. $u^{\mathsf T} Y v \ge 0$ for every $u \in K_1^*$ and $v \in K_2^*$.

$M_+(K_1, K_2)$ adds the condition that $Y$ is positive semidefinite. The projections are $N(K_1, K_2) = \{Ye_0 : Y \in M(K_1, K_2)\}$ and $N_+(K_1, K_2) = \{Ye_0 : Y \in M_+(K_1, K_2)\}$, where $e_0$ is the 0th unit vector. The cut operator is $N(K) = N(K, Q)$, and its iterates are $N^0(K) = K$, $N^t(K) = N(N^{t-1}(K))$.

Two families of hyperplanes appear in the proofs: $H_i = \{x : x_i = 0\}$ and $G_i = \{x : x_i = x_0\}$, the hyperplanes through the two opposite facets of $Q$ in direction $i$.

Formalization targets

Goal: Theorem 1.4

For every closed convex cone $K \subseteq Q$,

$$N^n(K) = K^\circ .$$

The statement is uniform in $n$ and in $K$: no polyhedrality, no bound on the number of constraints, and no assumption that $K$ contains a 0–1 point.

Milestones

1. Condition (iii″). For a closed convex cone $K \subseteq Q$ and a symmetric $Y$ with $y_{ii} = y_{0i}$: $Y \in M(K, Q)$ if and only if every column of $Y$ is in $K$ and the difference of the first column and any other column is in $K$.
2. Lemma 1.1. For closed convex cones $K_1, K_2 \subseteq Q$,

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

3. Lemma 1.3. For a closed convex cone $K \subseteq Q$ and every $1 \le i \le n$,

$$N(K) \subseteq (K \cap H_i) + (K \cap G_i).$$

4. Claim (4) in the proof of Theorem 1.4. For every set $T$ of $t \ge 1$ coordinates, with $\bar F$ the union of the faces of the unit cube that fix the coordinates in $T$ to $0$ or $1$,

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

5. The remark after Lemma 1.1. $N(K_1 \cap K_2, K_1 \cap K_2) \subseteq N(K_1, K_2) \subseteq N(K_1 \cap K_2, Q)$.

Significance

Theorem 1.4 is what makes $N$ a hierarchy rather than a single cut: the relaxations $K \supseteq N(K) \supseteq N^2(K) \supseteq \dots$ reach the 0–1 hull after at most $n$ rounds, so the $N$-rank of a valid inequality (the least $t$ with the inequality valid for $N^t(K)$) is a well-defined number between $0$ and $n$. The rest of the paper measures combinatorial constraints by this rank: odd hole constraints have rank one on the stable set polytope, and the rank of a stable set inequality is bounded by its defect. Rank lower bounds for lift-and-project hierarchies, in the literature that followed, all presuppose this finite convergence.

The theorem is proved in the paper; to the best of available knowledge none of the Lovász–Schrijver operators has been formalized in a proof assistant. A formalization provides machine-checked definitions of the matrix cones and the cut operators that later missions in this series (odd holes, the defect bound, the $N_+$ constraints) state their results against, and a checked proof of the column characterization (iii″) that all of those proofs use.

Difficulty

The inclusion $K^\circ \subseteq N^n(K)$ follows from Lemma 1.1 once each $N^t(K)$ is known to be a convex cone. The reverse inclusion is the content. A first attempt shows that one round of $N$ forces one coordinate to be integral, and then iterates; but $N(K)$ is not contained in the union of $K \cap H_i$ and $K \cap G_i$, only in their Minkowski sum (Lemma 1.3), so a point of $N(K)$ is not itself integral in any coordinate. The induction must carry a statement about cones spanned by intersections with unions of cube faces, and it needs each iterate $N^t(K)$ to again be a closed convex cone inside $Q$ so that Lemma 1.3 can be reapplied. Closedness of the projection $N(K)$ is not automatic: a linear image of a closed cone need not be closed.

Formalization scope

• Coordinates of $\mathbb R^{n+1}$ are indexed by Option ι for a finite type ι; none is $x_0$ and some i is $x_i$, and $n$ is the cardinality of ι, which may be $0$.
• $\operatorname{cone}(S)$ is Mathlib's PointedCone.hull ℝ S; $Q$ and $K^\circ$ are defined as spans of 0–1 vectors, as on the page, not by the inequality description $0 \le x_i \le x_0$.
• $M(K_1, K_2)$ is defined by condition (iii) through the polar cones; the column form (iii″) is a milestone, not the definition.
• The operators $N$, $N_+$ and the iterates are defined on arbitrary sets; the hypotheses (convex cone, contained in $Q$, closed) are carried by the theorems.
• Closedness. The paper tacitly takes its cones closed (they are polyhedral in all its applications), and the rewriting (iii′) on p. 169 needs it. Every statement here assumes the cones closed. Without this the goal is false: for $K = \{x : 0 < x_1 < x_0\} \cup \{0\}$ in $\mathbb R^2$, $K^\circ = \{0\}$ while $N(K) = Q$.
• In the proof of Theorem 1.4 the page places the cube $Q'$ in the hyperplane "$x_0 = 0$"; this is a misprint for $x_0 = 1$, and claim (4) is formalized with $x_0 = 1$.
• Not formalized in this mission: Lemma 1.2 (the dual description of $N(K)^*$), Lemma 1.5 (the $N_+$ analogue of Lemma 1.3, part of a later mission), and the algorithmic results of Section 1.c.

Contributions welcome: proofs that $N(K)$ is a closed convex cone contained in $Q$ whenever $K$ is, a proof of $Q^* = \operatorname{cone}\{e_i, e_0 - e_i\}$, and lemmas on cones spanned by the intersection of a generating set with a supporting hyperplane; these are reusable by the other missions of the series.

Selected references

• L. Lovász and A. Schrijver, Cones of matrices and set-functions and 0–1 optimization, SIAM Journal on Optimization 1(2) (1991) 166–190. https://doi.org/10.1137/0801013
• H. D. Sherali and W. P. Adams, A hierarchy of relaxations between the continuous and convex hull representations for zero-one programming problems, SIAM Journal on Discrete Mathematics 3(3) (1990) 411–430. https://doi.org/10.1137/0403036
• J. B. Lasserre, Global optimization with polynomials and the problem of moments, SIAM Journal on Optimization 11(3) (2001) 796–817. https://doi.org/10.1137/S1052623400366802
• M. Laurent, A comparison of the Sherali–Adams, Lovász–Schrijver, and Lasserre relaxations for 0–1 programming, Mathematics of Operations Research 28(3) (2003) 470–496. https://doi.org/10.1287/moor.28.3.470.16391

Why the assignment dual matters

The subgradient method maximizes a concave, piecewise-linear function $w(\pi)=\min_k\{c_k+\pi\cdot v_k\}$ by moving along a subgradient $v_k$ of an active piece with a prescribed step. Held, Wolfe and Crowder's 1974 paper Validation of subgradient optimization tested the method on three families of Lagrangean duals from combinatorial optimization — the assignment problem, a relaxation of the travelling salesman problem in the style of Held and Karp, and multicommodity flows — and gave the first systematic account of when the method works in practice.

On randomly generated assignment problems of order $n\le 30$ the authors observed that the method usually did not merely converge: it stopped, after finitely many steps, at an iterate whose subgradient was exactly zero. Their explanation is a structural fact about the assignment dual, Theorem 3.1 of the paper: when the optimal assignment is unique — the typical case for random integer costs — the set of optimal dual prices has full dimension $n$, so a sequence of steps of decreasing length can land inside it. This mission formalizes that theorem and the steps of its proof.

Setting

There are $n$ men and $n$ jobs, and a real $n\times n$ cost matrix $A=(a_{ir})$: $a_{ir}$ is the cost for which man $i$ does job $r$. A one-to-one assignment is a permutation $\sigma$ of $\{1,\dots,n\}$, where $\sigma(r)$ is the man doing job $r$; its cost is $\sum_r a_{\sigma(r)\,r}$. The assignment problem (3.1) asks for a permutation of minimal cost; the assignment is unique if exactly one permutation attains that minimum.

The linear relaxation of (3.1), over doubly stochastic matrices $x=(x_{ir})$, has the dual linear program (3.2), $\max\{\sum_i\pi_i+\sum_r\rho_r : \pi_i+\rho_r\le a_{ir}\}$. For fixed prices $\pi\in\mathbb R^n$ on the men the best $\rho$ is $\rho_r=\min_s[a_{sr}-\pi_s]$, which leaves the dual function (3.3)

$$w(\pi)=\sum_{i=1}^n\pi_i+\sum_{r=1}^n\min_s\,[a_{sr}-\pi_s],$$

the inner minimum being over the men $s$ for each job $r$. The optimal set is $\Omega=\{\pi : w(\pi')\le w(\pi)\ \text{for all }\pi'\}$.

To put $w$ in the form $\min_k\{c_k+\pi\cdot v_k\}$ the paper uses assignments in a weaker sense: arbitrary functions $A:\{1,\dots,n\}\to\{1,\dots,n\}$, $n^n$ of them, with cost $c_A=\sum_r a_{A(r)\,r}$ and vector $(v_A)_i=1-\#\{r:A(r)=i\}$ (3.4). The subgradient step raises the price of a man assigned no job and lowers the price of a man assigned several; $v_A=0$ exactly when $A$ is a permutation.

In the Lean development these are assignCost, assignVec, IsOptimalAssignment, w and optSet in the namespace HeldWolfeCrowder.Assignment.

Formalization targets

Goal: Theorem 3.1 (p. 70)

If the assignment problem has a unique optimal permutation, then

$$\dim\operatorname{aff}\,\Omega=n .$$

The hypothesis is uniqueness among permutations; the conclusion is the dimension of the affine hull of the optimal set.

Milestones, in the order the proof uses them

1. Eq. (3.4): $w(\pi)=\min_A\{c_A+\sum_i\pi_i(v_A)_i\}$ over all $n^n$ assignments $A$.
2. §3, Eqs. (3.1)–(3.3): $w$ attains its maximum, and $\max w$ equals the cost of an optimal permutation.
3. Eq. (3.5): if $\sigma$ is the unique optimal permutation, some maximizer $\bar\pi$ of $w$ has, for every job $r$, the minimum $\min_s[a_{sr}-\bar\pi_s]$ attained only at $s=\sigma(r)$.
4. Eq. (3.6): for an optimal permutation $\sigma$, the set $\Pi=\{\pi : a_{ir}-\pi_i>a_{\sigma(r)\,r}-\pi_{\sigma(r)}\ \text{for all } r,\ i\ne\sigma(r)\}$ is convex and open, $v=0$ on it, and $\Pi\subseteq\Omega$.

Significance

The theorem turns an empirical observation into a statement about the problem: finite termination of the subgradient method on assignment problems is a property of the dual, not luck. Since $w$ is unchanged by adding the same constant to every price, $\Omega$ always contains a line; Theorem 3.1 says that, under uniqueness, it is as large as it can be. The paper (p. 70) cites the argument of its Section 2 that, with a full-dimensional optimal set, termination of the method is "nearly certain".

The result is proved in the paper; none of it is known to be machine-checked. What the formalization adds is a checked link between three classical ingredients: the integrality of the assignment polytope (Birkhoff–von Neumann, which Mathlib has as doublyStochastic_eq_convexHull_permMatrix), linear-programming duality, and strict complementary slackness, which neither Mathlib nor the platform has in the form needed. The piecewise-linear representation (3.4) is reusable wherever the assignment dual appears as a Lagrangean subproblem.

Difficulty

The inclusion $\Pi\subseteq\Omega$ is elementary; the substance is that $\Pi$ is nonempty. The obvious candidate — any optimal dual solution — fails: an optimal $\pi$ may leave ties $a_{sr}-\pi_s=a_{\sigma(r)\,r}-\pi_{\sigma(r)}$ for some $s\ne\sigma(r)$, so it sits on the boundary of $\Omega$ and shows nothing about dimension. What is needed is an optimal price vector with all these inequalities strict at once, and uniqueness of the optimal permutation is a statement about the primal side only; transferring it to the dual side goes through the linear relaxation (3.1), whose uniqueness is not the hypothesis, and through a strict complementarity property that is not available in Mathlib or on the platform.

Formalization scope

Men and jobs are both Fin n; the costs are a : Matrix (Fin n) (Fin n) ℝ with a i r the cost of man i on job r; prices are π : Fin n → ℝ (no inner product or norm is needed, so no EuclideanSpace). The inner minimum of (3.3) is Finset.univ.inf' over the men, well defined for every n. One-to-one assignments are Equiv.Perm (Fin n) with σ r the man doing job r, so the orientation of the matrix matches (3.3); arbitrary assignments are functions Fin n → Fin n. "Of dimension $n$" is Module.finrank ℝ (vectorSpan ℝ (optSet a)) = n. The page prints the index condition of (3.6) as "$i\ne r$"; the formalization uses $i\ne\sigma(r)$, which is what the argument requires. The case $n=0$ is allowed and trivial.

A statement asserting only that $\Omega$ is nonempty, or that it has dimension at least one, is not this theorem: both hold for every cost matrix, the second because $\Omega$ is invariant under adding a constant to all prices. The goal requires the full value $n$, and its hypothesis is uniqueness of the optimal permutation, not of the optimal linear-programming solution.

A complete development needs: the assignment linear program and its integrality (Mathlib's Birkhoff–von Neumann theorem), weak and strong duality between (3.1) and (3.2) or directly $\max w=\min_\sigma c_\sigma$, and a strict complementarity statement for this primal–dual pair; the last two are reusable beyond this mission. Contributions of any of these, and of alternative arguments for (3.5) that avoid strict complementary slackness, are welcome.

Selected references

• M. Held, P. Wolfe, H. P. Crowder, Validation of subgradient optimization, Mathematical Programming 6 (1974) 62–88. https://doi.org/10.1007/BF01580223
• M. Held, R. M. Karp, The traveling-salesman problem and minimum spanning trees: Part II, Mathematical Programming 1 (1971) 6–25. https://doi.org/10.1007/BF01584070
• H. W. Kuhn, The Hungarian method for the assignment problem, Naval Research Logistics Quarterly 2 (1955) 83–97. https://doi.org/10.1002/nav.3800020109
• A. J. Goldman, A. W. Tucker, Theory of linear programming, in H. W. Kuhn, A. W. Tucker (eds.), Linear Inequalities and Related Systems, Annals of Mathematics Studies 38, Princeton University Press, 1956, 53–97.
• Mathlib, Mathlib/Analysis/Convex/Birkhoff.lean (Birkhoff–von Neumann theorem, doublyStochastic_eq_convexHull_permMatrix). https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Analysis/Convex/Birkhoff.lean

Motivation

Integer programs are routinely solved by first solving their linear programming (LP) relaxation and then searching for an integer optimum near the fractional one. How near an integer optimum must be is the subject of proximity theorems. They bound the search region of branch-and-bound and of dynamic programming, and they turn a fractional optimum into a starting point for exact algorithms.

The classical bound is due to Cook, Gerards, Schrijver and Tardos (Math. Programming 34, 1986): for an integer program in inequality form $\max\{c^Tx : Ax\le b,\ x\in\mathbb Z^n\}$ that is feasible and bounded, every optimal LP solution $x^*$ has an optimal integer solution $z^*$ with $\|x^*-z^*\|_\infty\le n\cdot\delta$, where $\delta$ is the largest absolute value of a subdeterminant of $A$. For programs in standard form $Ax=b$ with $m$ rows this gives, via the Hadamard bound, $\|z^*-x^*\|_1\le n^2\cdot m^{m/2}\Delta^m$, which grows with the number of variables $n$.

Eisenbrand and Weismantel (ACM Trans. Algorithms 16(1), Article 5, 2019; conference version SODA 2018) removed the dependence on $n$ altogether, using the Steinitz lemma on rearranging vectors so that all partial sums stay short. Their bound depends only on $m$ and on the largest absolute value $\Delta$ of an entry of $A$, and it is the basis of their faster algorithms for integer programs with few constraints.

Setting

Fix natural numbers $m$ (rows) and $n$ (variables). The data are a matrix $A\in\mathbb Z^{m\times n}$, a right-hand side $b\in\mathbb Z^m$, an objective $c\in\mathbb Z^n$ and upper bounds $u\in\mathbb N^n$. A natural number $\Delta$ bounds the entries: $|a_{ij}|\le\Delta$ for all $i,j$. The integer program (10) is

$$\max\{c^Tx : Ax=b,\ 0\le x\le u,\ x\in\mathbb Z^n\},$$

and its LP relaxation is the same problem over $x\in\mathbb R^n$. Its feasible region $P=\{x\in\mathbb R^n: Ax=b,\ 0\le x\le u\}$ is a polytope, lpPolytope A b u. An optimal vertex solution is an optimal solution of the LP relaxation (IsLPOptimal) that is an extreme point of $P$. An optimal integer solution is IsIPOptimal. Both are maxima.

Distances are measured in the $\ell_1$-norm $\|z-x\|_1=\sum_i|z_i-x_i|$.

A vector $y\in\mathbb Z^n$ is a cycle of $z^*-x^*$ (Eq. (14)) if $Ay=0$ and, for every $i$, $|y_i|\le|(z^*-x^*)_i|$ and $y_i(z^*-x^*)_i\ge0$: an integer kernel vector that is sign-compatible with $z^*-x^*$ and dominated by it (IsCycle).

The Steinitz lemma (Theorem 1.1) concerns vectors $x_1,\dots,x_n$ in an $m$-dimensional normed space with $\sum_i x_i=0$ and $\|x_i\|\le1$. It asserts a permutation $\pi$ with $\|\sum_{j\le k}x_{\pi(j)}\|\le c(m)$ for all $k$, and the paper uses Sevast'anov's constant $c(m)=m$.

Formalization targets

Goal: Theorem 3.3 (p. 5:8)

If (10) has an integer feasible point and $x^*$ is an optimal vertex solution of its LP relaxation, then there is an optimal solution $z^*$ of (10) with

$$\|z^*-x^*\|_1\ \le\ m\cdot(2m\Delta+1)^m .$$

The constant is the paper's. The goal holds for all $m$, $n$, $b$, $c$ and $u$; only $m$ and $\Delta$ enter the bound.

Milestones, in the order the proof uses them

1. Lemma 3.1 (p. 5:8): for an LP optimum $x^*$, an integer optimum $z^*$ and a cycle $y$ of $z^*-x^*$, the vector $z^*-y$ is integer feasible, $x^*+y$ is LP feasible, and $c^Ty\le0$.
2. Lemma 3.2 (p. 5:8): if $z^*$ minimizes $\|z^*-x^*\|_1$ among the optimal integer solutions, then $z^*-x^*$ has no nonzero cycle.
3. Theorem 1.1 with $c(m)=m$ (p. 5:4): the Steinitz lemma in any $m$-dimensional real normed space.
4. Proof of Theorem 3.3 (pp. 5:8–5:9): round a vertex $x^*$ towards an integer vector and write $\{x^*\}$ for the remainder. Then $\|-A\{x^*\}\|_\infty\le\Delta m$ and $-A\{x^*\}=w_1+\dots+w_m$ with integer $w_j$, $\|w_j\|_\infty\le\Delta$.
5. Proof of Theorem 3.3, Eq. (20) (p. 5:9): a sequence of integer vectors of $\ell_\infty$-norm at most $m\Delta$ in which no value repeats $m+1$ times has length at most $m(2m\Delta+1)^m$.
6. Eq. (21) (p. 5:9), a consequence: $c^T(x^*-z^*)\le\|c\|_\infty\cdot m(2m\Delta+1)^m$ for every optimal integer solution $z^*$.

Significance

The bound is independent of the number of variables. Combined with the paper's dynamic program, it gives the paper's running-time results for integer programs with upper bounds: an optimal LP vertex is computed, and the integer optimum is searched for within an $\ell_1$-ball of radius $m(2m\Delta+1)^m$ around it. Eq. (21) bounds the absolute integrality gap by the same quantity, scaled by $\|c\|_\infty$. The Steinitz lemma with constant $m$ is a general tool in discrepancy theory and in scheduling algorithms.

All of these results have published proofs. No machine-checked proof of Theorem 3.3 or of the Steinitz lemma is known to this mission, and Mathlib has no Steinitz lemma. The mission asks for complete Lean proofs of the milestones and of the goal. A proof of the Steinitz lemma with constant $m$ for arbitrary norms is reusable well beyond integer programming.

Difficulty

Lemmas 3.1 and 3.2 and the counting step are elementary. The substance lies in two places. The first is the Steinitz lemma with the linear constant $m$ for an arbitrary norm: the bound must hold uniformly in the number $n$ of vectors, and the constant must be exactly $m$, because the goal's constant $(2m\Delta+1)^m$ counts integer points of $\ell_\infty$-norm at most $m\Delta$. The second is the passage from a vertex to at most $m$ fractional coordinates. The paper argues this in one sentence ("$x^*$ has at most $m$ positive entries"), which is not literally true for (10) with upper bounds: coordinates at their upper bound $u_i>0$ are positive. The correct fact concerns coordinates strictly between $0$ and $u_i$, and it has to be derived from the extreme-point property of $P$.

Formalization scope

• All declarations live in the namespace IPProximity.Eisenbrand. The data are integral: A : Matrix (Fin m) (Fin n) ℤ, b : Fin m → ℤ, c : Fin n → ℤ, u : Fin n → ℕ (entries $u_i=0$ allowed), Δ : ℕ. They are cast to ℝ once, inside the LP definitions. $m=0$ and $n=0$ are allowed.
• "Vertex" is Mathlib's Set.extremePoints ℝ (lpPolytope A b u). It is not defined through bases or by counting fractional coordinates.
• The $\ell_1$-distance is the explicit sum ∑ i, |(z i : ℝ) - x i|. Mathlib's norm on Fin n → ℝ is the sup norm, and it is used only where the paper has $\|\cdot\|_\infty$ (the $\|c\|_\infty$ of Eq. (21)).
• The goal adds one hypothesis the paper leaves implicit: (10) has an integer feasible point. The paper's proof begins with "Let $z^*$ be an optimal integer solution"; without this hypothesis the conclusion is false.
• Eq. (14) is formalized literally, so $y=0$ is a cycle, and Lemma 3.2 is stated for nonzero cycles, which is what its proof establishes. Dropping the vertex hypothesis would make the goal false, so the goal keeps it. The constant is exactly $m(2m\Delta+1)^m$, with no hidden existential constant.
• The Steinitz milestone is stated for any finite-dimensional real normed space of dimension $m$ with the explicit constant $m$. The goal needs only the $\ell_\infty$ case on $\mathbb R^m$.
• Out of scope: the dynamic program and the running-time theorems of Sections 2 and 4, and the refinement $\|z^*-x^*\|_1\le2\Delta$ for $m=1$.

Contributions welcome: proofs of any milestone, in particular the Steinitz lemma, and a proof of the goal from the milestones.

Selected references

• F. Eisenbrand, R. Weismantel, Proximity Results and Faster Algorithms for Integer Programming Using the Steinitz Lemma, ACM Transactions on Algorithms 16(1), Article 5, 2019. https://doi.org/10.1145/3340322
• W. Cook, A. M. H. Gerards, A. Schrijver, É. Tardos, Sensitivity theorems in integer linear programming, Mathematical Programming 34, 251–264, 1986. https://doi.org/10.1007/BF01582230
• E. Steinitz, Bedingt konvergente Reihen und konvexe Systeme, Journal für die reine und angewandte Mathematik 143, 128–176, 1913. https://doi.org/10.1515/crll.1913.143.128
• S. Sevast'janov, Approximate solution of some problems of scheduling theory (in Russian), Metody Diskretnogo Analiza 32, 66–75, 1978 (reference [31] of the paper).
• V. S. Grinberg, S. V. Sevast'yanov, Value of the Steinitz constant, Functional Analysis and Its Applications 14(2), 125–126, 1980 (reference [16] of the paper).

Motivation

A branching in a directed graph is a set of edges that contains no cycle (even ignoring directions) and in which no two edges point to the same node; a connected branching is an arborescence, a tree rooted at one node with all edges directed away from the root. The optimum branching problem asks, for real weights on the edges, for a branching of maximum total weight. It contains the minimum-cost spanning arborescence problem (the directed analogue of the minimum spanning tree), which appears in network design, in the analysis of broadcast and routing structures, in phylogenetics, and in dependency parsing in computational linguistics, where maximum spanning arborescences are the standard decoding step of graph-based parsers.

J. Edmonds solved the problem in Optimum branchings (J. Res. Nat. Bur. Standards 71B (1967) 233–240). The paper gives an algorithm (the shrinking algorithm usually attributed to Chu–Liu and Edmonds) and, proved together with it, a polyhedral theorem: the linear system that every branching obviously satisfies has no other vertices. This was one of the first integral polyhedron theorems beyond bipartite matching and network flows, and together with Edmonds' matching polytope (1965) it set the pattern of polyhedral combinatorics: describe the convex hull of the combinatorial objects by linear inequalities, and prove optimality by a linear programming dual.

Timeline:

• 1965: Y. J. Chu and T. H. Liu describe the shrinking algorithm for the maximum arborescence.
• 1965: Edmonds, Paths, trees, and flowers and Maximum matching and a polyhedron with 0,1-vertices: the matching polytope.
• 1967: Edmonds, Optimum branchings: the algorithm, Theorem 2 (vertices of the branching polyhedron), and the dual certificate built along the algorithm.
• 1970–1971: Edmonds' matroid intersection theorem, which contains the branching polyhedron theorem as the intersection of a graphic matroid and a partition matroid.
• 1977–1986: faster implementations (Tarjan; Gabow, Galil, Spencer and Tarjan).

Setting

A graph $G$ consists of a finite set $V$ of nodes and a finite set $E$ of edges. Each edge $e$ is directed toward a node $\mathrm{front}(e)$, its front end, and away from a different node $\mathrm{rear}(e)$, its rear end. Parallel edges are allowed; loops are not.

For $F\subseteq E$, a node $v$ meets $k$ edges of $F$ if $\#\{e\in F:\mathrm{front}(e)=v\}+\#\{e\in F:\mathrm{rear}(e)=v\}=k$. A set $B\subseteq E$ is a forest if it contains no polygon, i.e. no nonempty $F\subseteq B$ in which every node meets zero or two edges of $F$; it is a branching if in addition distinct edges of $B$ have distinct front ends. The incidence vector $x^B\in\mathbb R^E$ of $B$ has $x^B_e=1$ for $e\in B$ and $0$ otherwise.

The branching polyhedron $P_G\subseteq\mathbb R^E$ is the set of $x$ with

• $(L_1)$ $x_e\ge0$ for every edge $e$;
• $(L_2)$ $\sum_{e:\,\mathrm{front}(e)=v}x_e\le1$ for every node $v$;
• $(L_3)$ $\sum_{e:\,\mathrm{front}(e),\mathrm{rear}(e)\in S}x_e\le|S|-1$ for every set $S$ of two or more nodes.

A vertex of a set $P\subseteq\mathbb R^E$ is a point of $P$ that is the unique maximizer over $P$ of some linear function $x\mapsto\sum_e c_ex_e$.

For weights $c\in\mathbb R^E$, the dual variables are $y_h$ for each node $v_h$ and $y_S$ for each $S$ with $|S|\ge2$; write $w_e=\sum_{S\ni\mathrm{front}(e),\mathrm{rear}(e)}y_S$ and $(b,y)=\sum_hy_h+\sum_S(|S|-1)y_S$. Edmonds' conditions are (15) $y_h\ge0$, (16) $y_S\ge0$, (17) $y_{\mathrm{front}(e)}+w_e\ge c_e$ for every edge, and, for a branching $B$, (18) $y_h\ne0\Rightarrow$ some edge of $B$ enters $v_h$, (19) $y_S\ne0\Rightarrow$ exactly $|S|-1$ edges of $B$ lie inside $S$, (20) $y_{\mathrm{front}(e)}+w_e=c_e$ for $e\in B$.

Formalization targets

Goal: Theorem 2 (p. 235)

$$\{x:\ x\text{ is a vertex of }P_G\}\;=\;\{x^B:\ B\text{ is a branching of }G\}.$$

Both inclusions, for every finite loopless directed multigraph.

Milestones

1. §5, p. 236: for every branching $B$, $x^B\in P_G$.
2. §5, p. 236: for every branching $B$, $x^B$ is a vertex of $P_G$.
3. §6, (12)–(14): if $B$ is a branching and $y$ satisfies (15)–(20), then $(c,x^B)=(b,y)$, $x^B$ maximizes $(c,x)$ over $P_G$, and $y$ minimizes $(b,y)$ subject to (15)–(17).
4. §7, p. 237: for every $c\in\mathbb R^E$ there are a branching $B$ and a $y$ satisfying (15)–(20).
5. Lemma 1, p. 236: for every $c\in\mathbb R^E$ some branching vector lies in $P_G$ and maximizes $\sum_ec_ex_e$ over $P_G$.

Significance

Theorem 2 says that the linear program $\max\{(c,x):x\in P_G\}$ always has an optimal solution that is a branching, and that every vertex of $P_G$ is one. Consequently optimum branchings, and after the reductions of the paper's §2 optimum spanning and rooted arborescences, can be computed by linear programming, and their optimality is certified by a dual vector satisfying (15)–(20). The same statement underlies the separation-based treatment of arborescence constraints in integer programming formulations of network design and of the asymmetric travelling salesman problem. The integrality of the dual for integer weights (the paper's §8) yields min–max theorems of König type for branchings.

The result is proved and classical; no machine-checked proof of it in a proof assistant is known. The mission asks for the paper's own proof chain: branching vectors are points and vertices of $P_G$, linear programming optimality from complementary slackness, existence of a dual certificate for every weight vector, and the deduction of Theorem 2. Proofs through matroid intersection or total dual integrality would also establish the goal and are welcome as alternative routes.

Difficulty

The inclusion "branching vectors are vertices" and the certificate criterion are short. The substance is Milestone 4: for arbitrary real weights, a branching and a dual vector satisfying the complementary slackness conditions must exist simultaneously. Finiteness gives an optimum branching at once, but that says nothing about optimality over the fractional points of $P_G$; the difficulty is the dual. The natural attempt, taking $y_S=0$ for all sets and $y_h$ the largest positive weight entering $v_h$, violates (20) as soon as the greedy choice closes a circuit: the $(L_3)$ duals of nested node sets, arising from repeatedly shrinking circuits, are needed, and they must be kept nonnegative through weight changes of the form $c_3+c_0-c_4$ on edges entering a shrunk circuit.

Formalization scope

A graph is a structure Graph V E with front rear : E → V and a proof that front e ≠ rear e; V and E carry Fintype and DecidableEq. Edge sets are Finset E; vectors are E → ℝ; the linear function with weights c is ∑ e, c e * x e. A branching is defined combinatorially (no nonempty edge subset in which every node meets zero or two edges, and distinct front ends), never by counting edges inside node sets, and $P_G$ is the solution set of $(L_1)$–$(L_3)$, never a convex hull; either shortcut would make half of Theorem 2 true by definition. A vertex is a unique maximizer of a linear function, as on p. 236 (Mathlib's Set.exposedPoints has the same content); the set variables of the dual are a function Finset V → ℝ whose values on sets of fewer than two nodes are ignored. The right side of $(L_3)$ is the real number $|S|-1$.

Implicit conventions made explicit: the no-loop condition is part of the graph (with a loop $e$, the vector of $\{e\}$ is a vertex of $P_G$ but not a branching); parallel edges are allowed; weights have arbitrary sign and the empty branching is allowed. The mission does not model the algorithm of §4 or Theorem 1's notion of a "good" algorithm; Milestone 4 states only the existence of a certificate, which is what Lemma 1 uses.

Useful reusable infrastructure: finite directed multigraphs with an edge type, forests via polygons, and a finite LP duality lemma for $\max\{c^\top x: x\ge0,\ Ax\le b\}$; contributions of either are welcome.

Selected references

• J. Edmonds, Optimum branchings, J. Res. Nat. Bur. Standards Sect. B 71B (1967), 233–240. https://doi.org/10.6028/jres.071b.032
• Y. J. Chu and T. H. Liu, On the shortest arborescence of a directed graph, Scientia Sinica 14 (1965), 1396–1400.
• J. Edmonds, Maximum matching and a polyhedron with 0,1-vertices, J. Res. Nat. Bur. Standards 69B (1965), 125–130. https://doi.org/10.6028/jres.069B.013
• R. E. Tarjan, Finding optimum branchings, Networks 7 (1977), 25–35. https://doi.org/10.1002/net.3230070103
• H. N. Gabow, Z. Galil, T. Spencer and R. E. Tarjan, Efficient algorithms for finding minimum spanning trees in undirected and directed graphs, Combinatorica 6 (1986), 109–122. https://doi.org/10.1007/BF02579168
• A. Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer (2003), Chapter 52.