The OR Formalization Drive

Motivation

Many combinatorial optimization problems are integer programs: linear objectives and linear constraints, with the extra requirement that the variables be integers. Dropping that requirement gives the LP relaxation, which is solvable efficiently but in general only bounds the integer optimum. For a small but important class of problems the relaxation loses nothing: its optimum is attained at an integral point, so linear programming solves the combinatorial problem exactly. Bipartite matching is the standard example, and the job-assignment problem that opens Chapter 3 of Matoušek and Gärtner's Understanding and Using Linear Programming (Springer 2007) is a maximum-weight perfect matching problem in a bipartite graph.

The same phenomenon, combined with linear programming duality, produces combinatorial min–max theorems. The oldest of them is König's theorem (1931) on matchings and vertex covers in bipartite graphs; Hall's marriage theorem (1935) follows from it. This mission formalizes the book's treatment of both strands: the integrality of the bipartite matching LP (Section 3.2), total unimodularity and König's theorem (Section 8.2), and, on the same objects for general graphs, the LP-rounding 2-approximation for vertex cover (Section 3.3).

Setting

Let $G = (V, E)$ be a finite simple graph. A bipartition of $G$ is a pair of disjoint sets $X, Y$ with $X \cup Y = V$ such that every edge joins a vertex of $X$ to a vertex of $Y$; $G$ is bipartite if it has one. A matching is a set $M \subseteq E$ in which each vertex is incident to at most one edge; a vertex cover is a set $C \subseteq V$ containing at least one end-vertex of every edge. A matching is maximum if no matching has more edges; a vertex cover is minimum if no vertex cover has fewer vertices.

The incidence matrix of $G$ has a row for each vertex and a column for each edge, with entry $1$ when the vertex lies on the edge and $0$ otherwise. A real matrix is totally unimodular if every square submatrix, obtained by deleting some rows and some columns, has determinant $0$, $1$ or $-1$.

Given real edge weights $w_e$, the integer program (3.1) maximizes $\sum_{e} w_e x_e$ subject to $\sum_{e \ni v} x_e = 1$ for every vertex $v$ and $x_e \in \{0,1\}$; its 0/1 solutions are the perfect matchings. Its LP relaxation replaces $x_e \in \{0,1\}$ by $0 \le x_e \le 1$. The vertex-cover relaxation (3.3) minimizes $\sum_v x_v$ subject to $x_u + x_v \ge 1$ for every edge $\{u,v\}$ and $0 \le x_v \le 1$.

Formalization targets

Goal: König's theorem (Theorem 8.2.2)

For every finite bipartite graph $G$,

$$\max\{|M| : M \text{ a matching of } G\} \;=\; \min\{|C| : C \text{ a vertex cover of } G\}.$$

Total unimodularity (Lemmas 8.2.3–8.2.5)

$$A \text{ TU} \;\Rightarrow\; (A \mid e_i) \text{ TU}; \qquad A \text{ TU},\ b \in \mathbb{Z}^m,\ \max\{c^Tx : Ax \le b,\ x \ge 0\} \text{ attained} \;\Rightarrow\; \text{attained at some } x^* \in \mathbb{Z}^n;$$

and the incidence matrix of a bipartite graph is totally unimodular.

Integrality of the perfect-matching relaxation (Theorem 3.2.1)

If the LP relaxation of (3.1) for a bipartite graph with real weights is feasible, it has an optimal solution with all $x_e \in \{0,1\}$, which is also optimal for (3.1).

Consequences on the same objects

Hall's theorem (Theorem 8.2.1): if $|N(T)| \ge |T|$ for every $T \subseteq X$, where $N(T) \subseteq Y$ is the set of neighbours of $T$, then some matching covers every vertex of $X$. And for an arbitrary graph, with $x^*$ optimal for (3.3), $S_{LP} = \{v : x^*_v \ge \tfrac12\}$ and $S_{OPT}$ a minimum vertex cover (§3.3, p. 38):

$$S_{LP} \text{ is a vertex cover and } |S_{LP}| \le 2\,|S_{OPT}| .$$

Significance

König's theorem says that for bipartite graphs the two natural certificates, a matching (a lower bound on any vertex cover) and a vertex cover (an upper bound on any matching), always meet. It makes maximum matchings and minimum vertex covers computable by linear programming, whereas minimum vertex cover in general graphs is NP-hard; Section 3.3's rounding bound quantifies what the LP still gives in that general case. Lemma 8.2.4 is the general tool behind this and behind the max-flow min-cut theorem that the book mentions on p. 148: any integer program with a totally unimodular constraint matrix and integral right-hand side can be solved as a linear program.

All results here are classical and proved. The formalization work is to connect them: Mathlib already has the definition of total unimodularity (Matrix.IsTotallyUnimodular), closure under appending unit-like rows, and Hall's theorem in the form of Finset.all_card_le_biUnion_card_iff_exists_injective. To the best of the drafting survey, neither König's theorem nor the total unimodularity of bipartite incidence matrices nor the integrality lemma 8.2.4 is in Mathlib, and no König statement was found among the platform's missions. The mission produces these in a form that later chapters on network flows and combinatorial duality can import.

Difficulty

The inequality "maximum matching $\le$ minimum vertex cover" is immediate, since each edge of a matching needs its own cover vertex. The difficulty is the reverse inequality, and it is exactly where bipartiteness is needed: the triangle has maximum matching $1$ and minimum vertex cover $2$. Along the book's route, the obstacle is that LP duality equates the optima of the two relaxations, which are real numbers; one must show that both relaxations already have integral optimal solutions, which is the content of total unimodularity and Lemma 8.2.4. Theorem 3.2.1 is a separate integrality statement with equality constraints and weights of arbitrary sign; it is not a consequence of the Birkhoff–von Neumann theorem unless the graph is complete bipartite with equal sides.

Formalization scope

Graphs are SimpleGraph V on a Fintype vertex type with decidable equality; edges are elements of Sym2 V, and a matching is a Finset (Sym2 V) of edges. Bipartiteness is the existence of finite sets $X, Y$ forming a bipartition; the empty graph and the empty vertex type are allowed and the statements remain the book's there. Vertex covers are Mathlib's SimpleGraph.IsVertexCover. Matrices are real; LP vectors are Fin n → ℝ (0-based indices) or indexed by the edge set or the vertices. An "optimal solution" is always a feasible point that is at least as good as every feasible point: no supremum or infimum over a possibly empty or unbounded set is used, and König's theorem asserts that both a maximum matching and a minimum vertex cover exist and have equal size. Lemma 8.2.4 takes $b \in \mathbb{Z}^m$ and allows real $c$; its conclusion is an integral optimal solution, not merely an integral feasible one. Theorem 3.2.1 is the perfect-matching version with equality constraints, not the "$\le 1$" matching version discussed in the book's remarks.

A formalization in which König's theorem compares a supremum and an infimum of possibly empty sets, or in which "optimal" is not tied to feasibility, would be trivializing and is ruled out by these conventions.

Useful infrastructure, reusable beyond this mission: Laplace expansion arguments for totally unimodular matrices, the equivalence of the inequality form with the equational form, existence of optimal basic feasible solutions, and LP duality in inequality form (the platform's LinearOptimization.lp_strong_duality states duality for a general-form LP). Combinatorial proofs of König and Hall are equally welcome; only the statements are fixed.

Selected references

• J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §3.2–3.3 and §8.2. https://doi.org/10.1007/978-3-540-30717-4
• D. Kőnig, "Gráfok és mátrixok", Matematikai és Fizikai Lapok 38 (1931), 116–119.
• P. Hall, "On representatives of subsets", Journal of the London Mathematical Society 10 (1935), 26–30. https://doi.org/10.1112/jlms/s1-10.37.26
• A. J. Hoffman, J. B. Kruskal, "Integral boundary points of convex polyhedra", in Linear Inequalities and Related Systems, Annals of Mathematics Studies 38, Princeton, 1956, 223–246. https://doi.org/10.1515/9781400881987-014
• A. Schrijver, Theory of Linear and Integer Programming, Wiley, 1986, Chapter 19.

Motivation

Every finite algorithm for linear programming rests on one structural fact: if a linear program has an optimum at all, it has one at a point singled out by finitely many linear conditions. The simplex method walks between such points, and exact complexity analyses, sensitivity analysis and integrality arguments all start from them. Chapter 4 of J. Matoušek and B. Gärtner, Understanding and Using Linear Programming (Springer, 2007, DOI 10.1007/978-3-540-30717-4), establishes this fact for linear programs in equational form, in the definitions that the rest of the book (the simplex method of Chapter 5, duality in Chapter 6, the applications in Chapter 8) uses.

This mission is the second of a series formalizing that book. It fixes the book's notion of a basic feasible solution and of a vertex, and targets the theorem that optimal solutions exist whenever the program is feasible and bounded, and can then be chosen basic.

Setting

A linear program in equational form is

$$\text{maximize } c^{T}x \quad\text{subject to}\quad Ax=b,\ x\ge 0,$$

where $A$ is a real $m\times n$ matrix, $b\in\mathbb{R}^m$, $c\in\mathbb{R}^n$, and $x\ge 0$ means every coordinate of $x$ is nonnegative. A feasible solution is an $x\in\mathbb{R}^n$ satisfying both constraints; the set of them is $P$. An optimal solution is a feasible $x$ with $c^{T}y\le c^{T}x$ for every feasible $y$. The objective is bounded from above if some real $M$ satisfies $c^{T}x\le M$ for all feasible $x$.

Throughout Section 4.2 the book assumes that $A$ has $n\ge m$ columns and rank $m$ (its rows are linearly independent). For $S\subseteq\{1,\dots,n\}$, $A_S$ denotes the matrix formed by the columns of $A$ with indices in $S$. A basis is an $m$-element set $B$ for which $A_B$ is nonsingular, i.e. its columns are linearly independent. A basic feasible solution is a feasible $x$ for which some basis $B$ has $x_j=0$ for every $j\notin B$.

A point $v$ is a vertex of $P$ if $v\in P$ and some nonzero $c\in\mathbb{R}^n$ satisfies $c^{T}v>c^{T}y$ for every $y\in P\setminus\{v\}$: $v$ is the unique maximizer over $P$ of a nonzero linear function.

Formalization targets

Goal: Theorem 4.2.3 (p. 46)

For $A$ of rank $m$ with $n\ge m$,

$$\Bigl(P\neq\emptyset\ \wedge\ \exists M\ \forall x\in P,\ c^{T}x\le M\Bigr)\ \Longrightarrow\ \exists\,x^{*}\ \text{optimal},$$ $$\exists\,x^{*}\ \text{optimal}\ \Longrightarrow\ \exists\,\tilde x\ \text{optimal and basic feasible}.$$

Both parts are one theorem, as in the book. Part (i) says optimal solutions fail to exist only for the two obvious reasons, infeasibility and unboundedness; part (ii) says an optimum can always be found among basic feasible solutions.

Milestones

1. Lemma 4.2.1 (p. 45): a feasible $x$ is basic if and only if the columns of $A_K$ are linearly independent, where $K=\{j : x_j>0\}$.
2. Proposition 4.2.2 (p. 45): for a basis $B$ there is at most one feasible solution vanishing outside $B$.
3. The statement proved inside the proof of Theorem 4.2.3 (p. 47): if the objective is bounded above, every feasible $x_0$ is dominated by a basic feasible $\tilde x$, $c^{T}\tilde x\ge c^{T}x_0$.
4. Theorem 4.4.1 (p. 54): a point of $P$ is a vertex of $P$ if and only if it is a basic feasible solution.

Significance

Theorem 4.2.3 gives a finite, if impractical, algorithm for linear programming: enumerate the at most $\binom{n}{m}$ sets $B$, solve $A_Bx_B=b$, and keep the best nonnegative solution. It is the correctness backbone of the simplex method, which visits basic feasible solutions in a smarter order, and it is the source of the book's claim that a feasible and bounded linear program has an optimal solution. Theorem 4.4.1 identifies this algebraic notion with the geometric corners of the feasible polyhedron, which is what makes statements such as "the LP relaxation has an integral vertex" in later chapters meaningful.

All of these results are classical and fully proved in the book. The value of formalizing them here is the definition layer: later missions of this series (Bland's rule, the central path, the scheduling application) state their results about bases and basic feasible solutions in exactly these definitions, and a proved Theorem 4.2.3 in this form lets them import the existence of an optimal basic solution instead of re-deriving it. Related facts are already machine-checked on Prove2Me in the formulation of Bertsimas and Tsitsiklis (Introduction to Linear Optimization I and II: minimization over polyhedra $\{x : a_i^{T}x\ge b_i\}$, extreme points, basic solutions as $n$ active linearly independent constraints). Those statements concern a different presentation of the program and a different notion of basic solution; connecting them to the equational-form statements here is itself a welcome contribution.

Difficulty

The obvious argument for part (i), "a continuous function on a closed set bounded above attains its supremum", fails: the feasible set is usually unbounded, and a linear function bounded above on an unbounded closed convex set need not obviously attain its supremum without using the polyhedral structure. The existence of an optimum is exactly the nontrivial content of part (i); compactness is not available.

For milestone 1, the delicate direction is the converse: a set of linearly independent columns indexed by $K$ must be completed to an $m$-element basis, which requires the rank-$m$ assumption. For Theorem 4.4.1, the direction from vertex to basic feasible solution is not local: a vertex is defined by an optimization property, while basicness is a statement about the support of the point.

Formalization scope

All items live in the namespace MatousekLP.BFS and share one definition module, MatousekLP.BFS.EquationalForm. Conventions:

• vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ; the book's indices $1,\dots,n$ are 0, …, n-1;
• $Ax=b$ is A *ᵥ x = b, $x\ge 0$ is 0 ≤ x (pointwise), $c^{T}x$ is c ⬝ᵥ x;
• a subset $B$ of indices is a Finset (Fin n); "$A_B$ nonsingular" is linear independence over $\mathbb{R}$ of the family of columns of $A$ indexed by the elements of $B$, together with B.card = m;
• the standing assumption of §4.2 is the pair of hypotheses m ≤ n and A.rank = m on every theorem;
• "optimal" and "bounded from above" are stated against every feasible point. No real supremum over the feasible set appears anywhere, so an empty or unbounded feasible set cannot make a statement hold through a default value;
• "vertex" is the book's unique-maximizer definition of p. 53, not Mathlib's Set.extremePoints; the book's remark on p. 55 that the two coincide is not used as a definition;
• Theorem 4.4.1 carries the extra hypothesis $n\ge 1$: for $n=0$ there is no nonzero vector in $\mathbb{R}^0$, the single feasible point $0$ is basic but not a vertex, and the book's equivalence fails.

A formalization in which "optimal" were defined through sSup of the objective over the feasible set would make part (ii) trivially true or false on unbounded programs; the definitions here rule that out. Dropping the rank hypothesis would make part (ii) false (no basis exists when the rows are dependent), so it is not optional.

Reusable infrastructure: the column-restriction and basis vocabulary, the support set $K$, and the extension of a linearly independent set of columns to a basis of the column space are needed again in the simplex chapter. Proofs of any milestone, and bridges to Mathlib's Set.extremePoints or to the Bertsimas–Tsitsiklis statements on the platform, are welcome.

Selected references

• J. Matoušek and B. Gärtner, Understanding and Using Linear Programming, Universitext, Springer, 2007, Chapter 4, pp. 41–56. https://doi.org/10.1007/978-3-540-30717-4
• D. Bertsimas and J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Chapter 2.
• G. M. Ziegler, Lectures on Polytopes, Graduate Texts in Mathematics 152, Springer, 1995. https://doi.org/10.1007/978-1-4613-8431-1

Motivation

Every linear program comes with a second linear program, its dual, whose feasible solutions certify bounds on the optimum of the first. The duality theorem of linear programming says that these certificates are perfect: when both programs are feasible, the best bound equals the optimum. The theorem underlies the analysis of the simplex method, sensitivity analysis and shadow prices in operations research, the minimax theorem for zero-sum games, max-flow/min-cut and König-type min-max theorems in combinatorial optimization, and the primal–dual design of approximation and online algorithms.

The Farkas lemma, a theorem of the alternative for linear systems, contains the essence of duality: a system of linear equations or inequalities either has a (nonnegative) solution, or a single linear combination of its rows proves that it has none. It goes back to Farkas (1902) and Minkowski's work on finitely generated cones; the duality theorem itself is due to von Neumann (1947) and Gale, Kuhn and Tucker (1951).

This mission formalizes Chapter 6 of Matoušek and Gärtner's textbook Understanding and Using Linear Programming (Springer, 2007): the duality theorem in the book's form, weak duality, the Farkas lemma in its algebraic, geometric and three-variant forms, and the lemmas of two self-contained proofs of the Farkas lemma, one analytic (nearest points in finitely generated cones) and one via minimally infeasible systems.

Setting

Let $A$ be a real matrix with $m$ rows and $n$ columns, $b\in\mathbb{R}^m$, $c\in\mathbb{R}^n$. Vector inequalities are componentwise. The primal and dual linear programs are

$$\text{(P)}\quad\max\ c^{T}x \ \text{ s.t. } Ax\le b,\ x\ge 0, \qquad\qquad \text{(D)}\quad\min\ b^{T}y \ \text{ s.t. } A^{T}y\ge c,\ y\ge 0.$$

A feasible solution of (P) is an $x\in\mathbb{R}^n$ satisfying its constraints; an optimal solution is a feasible $x^*$ with $c^{T}x\le c^{T}x^*$ for every feasible $x$. (P) is unbounded if its objective takes arbitrarily large values on feasible solutions. For the minimization (D) the notions are mirrored: an optimal $y^*$ has $b^{T}y^*\le b^{T}y$ for all feasible $y$, and (D) is unbounded if $b^{T}y$ takes arbitrarily small values.

For $a_1,\dots,a_n\in\mathbb{R}^m$, the convex cone generated by them is $C=\{t_1a_1+\dots+t_na_n : t_i\ge 0\}$; a primitive cone is one generated by $k\le m$ linearly independent vectors. A system $Ax\le b$ of $m$ inequalities is minimally infeasible if it has no solution but dropping any one inequality makes it solvable.

Formalization targets

Goal: the duality theorem (§6.1, p. 83)

For (P) and (D) as above, exactly one of the following occurs:

1. neither (P) nor (D) is feasible;
2. (P) is unbounded and (D) is infeasible;
3. (P) is infeasible and (D) is unbounded;
4. both are feasible; then both have optimal solutions, and every optimal $x^*$ of (P) and optimal $y^*$ of (D) satisfy

$$c^{T}x^*=b^{T}y^*.$$

Milestones

• Proposition 6.1.1 (weak duality). $c^{T}x\le b^{T}y$ for all feasible $x$ of (P) and $y$ of (D); hence (P) unbounded forces (D) infeasible, and (D) unbounded forces (P) infeasible.
• Proposition 6.4.1 (Farkas lemma). Exactly one of: $Ax=b$ has a solution $x\ge 0$; some $y$ has $y^{T}A\ge 0^{T}$ and $y^{T}b<0$. Already on the platform as LinearOptimization.farkas_lemma (Proved) and linked as a reference.
• Proposition 6.4.3 (three variants). Solvability of $Ax=b$, $x\ge0$; of $Ax\le b$, $x\ge 0$; and of $Ax\le b$ with $x$ free, each characterized by a certificate condition on $y$.
• Proposition 6.4.2 (geometric Farkas lemma). $b$ lies in the cone generated by $a_1,\dots,a_n$, or a hyperplane through $0$ separates the cone from $b$ strictly — exactly one.
• Lemmas 6.5.4, 6.5.5, 6.5.3, 6.5.1. Primitive cones are closed; a finitely generated cone is a finite union of primitive cones; hence it is closed (6.5.3, on the platform as Polyhedral.isClosed_conicSpan, Proved); hence it has a point nearest to any $b\notin C$.
• Lemmas 6.6.2 and 6.6.1. $Ax=b$ is solvable iff every $y$ with $y^{T}A=0^{T}$ has $y^{T}b=0$; in a minimally infeasible system, for every $i$ some $\tilde x^{(i)}$ satisfies all inequalities except the $i$th with equality.

Significance

The result. The duality theorem converts optimality into feasibility: a pair $(x,y)$ of primal and dual feasible solutions with $c^{T}x=b^{T}y$ is a short, checkable certificate that both are optimal, and the theorem guarantees such a certificate exists whenever an optimum does. It classifies every primal–dual pair into four behaviours and excludes the other five combinations of feasible-bounded, unbounded and infeasible. Later chapters of the same book rest on it: the minimax theorem for zero-sum games, the integrality of bipartite matching polytopes, the LP rounding for unrelated-machine scheduling, and the Delsarte bound for codes.

Formalizing it. All results here are classical and fully proved in the book; the work is formalization. Mathlib contains a Farkas lemma for proper cones in Hilbert spaces and closedness facts for finitely generated cones, and the platform already has Bertsimas–Tsitsiklis-style duality for a general-form minimization (LinearOptimization.lp_strong_duality) and matrix Farkas lemmas. What is missing is the textbook statement in Matoušek's inequality form (P)/(D), with its four-case exclusive classification, together with the chain of named lemmas that make two different elementary proofs of the Farkas lemma machine-checkable. The analytic chain (6.5.x) and the minimally-infeasible chain (6.6.x) are reusable independently of LP.

Difficulty

Weak duality is a two-line computation. The difficulty is entirely in the reverse direction, that a feasible bounded (P) forces the dual to be feasible with the same value. Any proof must use something beyond linear algebra over $\mathbb{R}$: either the termination of the simplex method with an anticycling rule, a topological fact (a finitely generated cone is closed), or an extremal argument (an optimal solution of an auxiliary LP). The naive geometric argument — take the nearest point of the cone to $b$ — fails without closedness, and closedness of the cone generated by a set is false for infinitely generated cones (the cone over a disc touching the origin is an open half-plane plus a point), so finiteness has to be used, which is the role of the primitive-cone decomposition. In the four-case theorem itself, the remaining obstacle is attainment: "bounded and feasible" must be upgraded to "an optimum exists" for both programs, which is not a consequence of Farkas-type statements alone.

Formalization scope

• Vectors are Fin n → ℝ and matrices Matrix (Fin m) (Fin n) ℝ; the book's indices $1,\dots,n$ become $0,\dots,n-1$. The row vector $y^{T}A$ is Aᵀ *ᵥ y, so $y^{T}A\ge 0^{T}$ is 0 ≤ Aᵀ *ᵥ y; scalar products are ⬝ᵥ.
• Optimal solutions and unboundedness are stated against every feasible point; no sSup/sInf is used, so no junk value of an empty or unbounded supremum enters. "Exactly one of the four cases" is ∃! k : Fin 4, DualityCase A b c k, with the book's case $k$ at index $k-1$; a plain disjunction would be weaker than the book.
• Cone items live in EuclideanSpace ℝ (Fin m), so the nearest point of Lemma 6.5.1 is Euclidean and $y^{T}x$ is the inner product. The convex cone generated by $a_1,\dots,a_n$ is the set of nonnegative combinations (it contains $0$, also for $n=0$).
• A trivializing formalization — case 4 read as "if both have optimal solutions then their values agree", which is weak duality plus nothing — is ruled out: case 4 asserts the existence of both optima from feasibility alone.
• Lemma 6.3.1 (the dual solution read off the final simplex tableau) and Lemma 6.5.2 (nearest point in a nonempty closed set, available in Mathlib as IsClosed.exists_infDist_eq_dist) are not separate targets. The Fourier–Motzkin elimination of §6.7 has no numbered result.
• Contributions welcome: proofs of any milestone, the two Farkas-lemma chains, and bridges to the general-form duality already on the platform.

Selected references

• J. Matoušek and B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, Chapter 6. https://doi.org/10.1007/978-3-540-30717-4
• J. Farkas, Theorie der einfachen Ungleichungen, J. Reine Angew. Math. 124 (1902), 1–27. https://doi.org/10.1515/crll.1902.124.1
• D. Gale, H. W. Kuhn and A. W. Tucker, Linear programming and the theory of games, in Activity Analysis of Production and Allocation, Wiley, 1951, 317–329.
• M. Conforti, M. Di Summa and G. Zambelli, Minimally infeasible set-partitioning problems with balanced constraints, Mathematics of Operations Research (cited in the book as to appear; the source of the proof in §6.6).
• D. Bertsimas and J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Chapter 4.

Motivation

Interior point methods solve linear programs in a number of iterations polynomial in the input size, and in practice they compete with the simplex method on large instances. Their modern form goes back to Karmarkar's projective algorithm (Karmarkar 1984); the primal–dual path-following variant analysed in textbooks follows a curve, the central path, defined by a perturbed system of optimality conditions. Two facts make the method well defined. First, the central path exists and is unique whenever the primal and dual programs have strictly feasible points. Second, an arbitrary linear program, possibly infeasible or unbounded, can be embedded in an auxiliary program that has an explicit starting point on its own central path and whose suitable optimal solutions either solve the original program or certify that it has no optimum.

Chapter 7, §7.2 of Matoušek and Gärtner, Understanding and Using Linear Programming (Springer 2007), presents both facts in elementary form, following Terlaky (2001). This mission formalizes its three numbered lemmas.

Timeline. The homogeneous system bearing their names is due to Goldman and Tucker (1956), in the study of the structure of optimal solution sets; the self-dual embedding for interior point methods was introduced by Ye, Todd and Mizuno (1994), and the book's presentation follows the skew-symmetric form in Roos, Terlaky and Vial (2005).

Setting

Let $A$ be a real $m\times n$ matrix, $b\in\mathbb{R}^m$, $c\in\mathbb{R}^n$. The linear program in equational form (7.2) is

$$\text{maximize } c^{T}x \text{ subject to } Ax=b,\ x\ge 0,$$

where $A$ has rank $m$; its dual (7.5) is: minimize $b^{T}y$ subject to $A^{T}y\ge c$, $y\in\mathbb{R}^m$. The notation $x>0$ means that all coordinates of $x$ are strictly positive. For $\mu>0$ the barrier function is $f_\mu(x)=c^{T}x+\mu\sum_{j=1}^n\ln x_j$, defined for $x>0$. The central-path system (7.4), in unknowns $x,s\in\mathbb{R}^n$ and $y\in\mathbb{R}^m$, is

$$Ax=b,\qquad A^{T}y-s=c,\qquad (s_1x_1,\dots,s_nx_n)=\mu\mathbf 1,\qquad x,s\ge 0 .$$

For the embedding, the book switches to the inequality form (7.7): maximize $c^{T}x$ subject to $Ax\le b$, $x\ge 0$, with dual: minimize $b^{T}y$ subject to $A^{T}y\ge c$, $y\ge 0$. The Goldman–Tucker system (GTS) is

$$Ax-\tau b\le 0,\qquad -A^{T}y+\tau c\le 0,\qquad b^{T}y-c^{T}x\le 0,\qquad x,y\ge 0,\ \tau\ge 0,$$

and $\rho=\rho(x,y)=c^{T}x-b^{T}y$ is the slack of its last inequality. With $u=(y,x,\tau)\in\mathbb{R}^k$, $k=n+m+1$, (GTS) reads $M_0u\le 0$, $u\ge 0$ for the skew-symmetric matrix

$$M_0=\begin{pmatrix}0&A&-b\\-A^{T}&0&c\\b^{T}&-c^{T}&0\end{pmatrix}.$$

Put $r=\mathbf 1+M_0\mathbf 1$, $M=\begin{pmatrix}M_0&-r\\r^{T}&0\end{pmatrix}$ and $q=(0,\dots,0,k+1)\in\mathbb{R}^{k+1}$. The self-dual program (SD) in $v=(u,\vartheta)$ is: maximize $-q^{T}v$ subject to $Mv\le q$, $v\ge 0$. Its slacks are $z=q-Mv$, and a feasible $v$ is strictly complementary if $v_j>0$ or $z_j>0$ for every $j=1,\dots,k+1$.

Formalization targets

Goal: Lemma 7.2.1 (p. 121)

If (7.2) has a feasible $\tilde x>0$ and (7.5) has a feasible $\tilde y$ with $\tilde s=A^{T}\tilde y-c>0$, then for every $\mu>0$

$$\exists!\,(x^*,y^*,s^*)\ \text{solving (7.4)},\qquad x^*=\arg\max\{f_\mu(x): Ax=b,\ x>0\}\ \text{(uniquely)}.$$

Milestones

1. Claim in the proof of Lemma 7.2.1 (p. 121): under the lemma's assumptions and for fixed $\mu>0$, the set $Q=\{x: Ax=b,\ x>0,\ f_\mu(x)\ge f_\mu(\tilde x)\}$ is bounded.
2. Lemma 7.2.2 (p. 126): no solution of (GTS) has $\tau\ne 0$ and $\rho\ne 0$; exactly one of "a solution with $\tau>0$" and "a solution with $\rho>0$" exists; in the first case $\frac1\tau x$ and $\frac1\tau y$ are optimal for (7.7) and its dual; in the second, (7.7) is infeasible or unbounded.
3. Lemma 7.2.3 (p. 128): (SD) is feasible and bounded, every optimal solution has $\vartheta=0$ and its $u$-part solves (GTS), and every strictly complementary optimal solution gives a solution of (GTS) with $\tau>0$ or $\rho>0$.

Significance

Lemma 7.2.1 is what makes "the central path" a well-defined object: without existence, a path-following method has nothing to follow, and without uniqueness the point $x^*(\mu)$ that the algorithm approximates is not determined. It also identifies the barrier maximizer with the solution of the Lagrange system (7.4), which is the system the Newton steps of the algorithm linearize. Lemmas 7.2.2 and 7.2.3 remove the need for an interior starting point and for knowing in advance that the program has an optimum: every linear program reduces to computing a strictly complementary optimal solution of a program with a known interior point on its central path.

The three lemmas are classical and proved in the book (7.2.2 as a sketch). Formalizing them adds a machine-checked account of the central path in equational form, and of the Goldman–Tucker and self-dual constructions with explicit block matrices, reusable by any later formalization of interior point complexity bounds. As far as a search of the platform shows, no formal statement of the Goldman–Tucker system or of the self-dual embedding exists there; the nearest item, Lemma 9.5 of Introduction to Linear Optimization XII (Bertsimas–Tsitsiklis), characterizes the central path by KKT conditions and is not linked to a formal statement.

Difficulty

For Lemma 7.2.1, uniqueness of a maximizer follows from strict concavity, but existence does not: the feasible region $\{Ax=b,\ x>0\}$ is open relative to its affine hull and typically unbounded, and $f_\mu$ need not attain its supremum on such a set. The interior dual point is what rules out escape to infinity; the primal interior point is what rules out escape to the boundary. Identifying the maximizer with the unique solution of (7.4) further needs the Lagrange multiplier rule on an open set and the full row rank of $A$ to determine $y$ from $s$.

For Lemma 7.2.2 the exclusivity and the optimality statements are weak-duality arguments, but existence of a solution with $\rho>0$ when (7.7) is infeasible or unbounded requires a Farkas-type alternative for both the primal and the dual, and the case split in the book's sketch ("the dual case is analogous") must be carried out. Lemma 7.2.3 requires bookkeeping with the block structure of $M$ and the skew-symmetry of $M_0$.

Formalization scope

Vectors are functions Fin n → ℝ and Fin m → ℝ; the book's indices $1,\dots,n$ become $0,\dots,n-1$. Matrices are Matrix (Fin m) (Fin n) ℝ, inequalities between vectors are componentwise, $x>0$ is ∀ j, 0 < x j. The rank condition of (7.2) is the hypothesis A.rank = m. Optimal solutions and unboundedness are expressed against every feasible point, never through a real supremum. The vector $u=(y,x,\tau)$ is indexed by Fin m ⊕ Fin n ⊕ Unit and $v=(u,\vartheta)$ by (Fin m ⊕ Fin n ⊕ Unit) ⊕ Unit; $M_0$, $r$, $M$ and $q$ are defined entrywise on these index types, with the last entry of $q$ equal to $k+1=n+m+2$. "Exactly one" in Lemma 7.2.2 is Xor.

Lean's Real.log returns $0$ for nonpositive arguments, so a statement comparing $f_\mu$ over $\{Ax=b\}$ or $\{Ax=b,\ x\ge 0\}$ would be a different, and generally false or trivial, claim; every comparison of barrier values is restricted to points with all coordinates strictly positive. The unique solution of (7.4) is stated as existence plus equality of every solution with it, not as existence of some solution.

Useful infrastructure: strict concavity of sums of logarithms, the Lagrange multiplier rule for affine constraints (Mathlib's IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt or a direct orthogonality argument), compactness of closed bounded sets in Fin n → ℝ, and Farkas' lemma in the forms of Proposition 6.4.1 of the book. Proofs of the milestones, alternative arguments, and general lemmas about skew-symmetric linear programs are all welcome.

Selected references

• J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §7.2. https://doi.org/10.1007/978-3-540-30717-4
• T. Terlaky, An easy way to teach interior-point methods, European Journal of Operational Research 130(1), 2001, 1–19.
• C. Roos, T. Terlaky, J.-P. Vial, Interior Point Methods for Linear Optimization, 2nd ed., Springer, 2005. https://doi.org/10.1007/b100325
• A. J. Goldman, A. W. Tucker, Theory of linear programming, in Linear Inequalities and Related Systems, Annals of Mathematics Studies 38, Princeton University Press, 1956, 53–97.
• Y. Ye, M. J. Todd, S. Mizuno, An $O(\sqrt{n}L)$-iteration homogeneous and self-dual linear programming algorithm, Mathematics of Operations Research 19(1), 1994, 53–67. https://doi.org/10.1287/moor.19.1.53
• N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica 4, 1984, 373–395. https://doi.org/10.1007/BF02579150
• F. A. Potra, S. J. Wright, Interior-point methods, Journal of Computational and Applied Mathematics 124, 2000, 281–302.

Why zero-sum games belong in a linear programming course

A two-player zero-sum game models any situation in which one party's gain is exactly the other party's loss: a military allocation in the spirit of Colonel Blotto, a sealed-bid contest, rock–paper–scissors. The central question is what each player should do when the opponent is also reasoning about them. John von Neumann answered it in 1928 with the minimax theorem (von Neumann 1928): each player has a strategy guaranteeing the same number, the value of the game, whatever the opponent does. The theorem underlies modern game theory, robust decision making, and the analysis of online learning algorithms, where regret bounds are routinely derived from it.

Section 8.1 of Matoušek and Gärtner's Understanding and Using Linear Programming (Springer 2007) presents the theorem as an application of linear programming duality. This mission is the sixth of a series formalizing the capstone results of the book.

Setting

Alice has $m \ge 1$ pure strategies and Bob has $n \ge 1$. A real $m \times n$ payoff matrix $M = (m_{ij})$ records Alice's gain, and Bob's loss, when Alice plays her $i$th and Bob his $j$th pure strategy. A mixed strategy of Alice is a probability vector $\mathbf x \in \mathbb R^m$, $\sum_i x_i = 1$, $\mathbf x \ge \mathbf 0$; a mixed strategy of Bob is a probability vector $\mathbf y \in \mathbb R^n$. When the players randomize independently, Alice's expected payoff is

$$\mathbf x^T M \mathbf y = \sum_{i,j} m_{ij} x_i y_j .$$

The worst-case payoffs are

$$\beta(\mathbf x) = \min_{\mathbf y} \mathbf x^T M \mathbf y, \qquad \alpha(\mathbf y) = \max_{\mathbf x} \mathbf x^T M \mathbf y,$$

over mixed strategies. A mixed strategy of Bob is a best response against $\mathbf x$ if it minimizes $\mathbf x^T M\mathbf y$; a mixed strategy of Alice is a best response against $\mathbf y$ if it maximizes it. A pair $(\tilde{\mathbf x}, \tilde{\mathbf y})$ is a mixed Nash equilibrium (Definition 8.1.1) if each is a best response against the other. Alice's $\tilde{\mathbf x}$ is worst-case optimal if $\beta(\tilde{\mathbf x}) = \max_{\mathbf x} \beta(\mathbf x)$; Bob's $\tilde{\mathbf y}$ is worst-case optimal if $\alpha(\tilde{\mathbf y}) = \min_{\mathbf y}\alpha(\mathbf y)$.

The proof in the book passes through three linear programs: the dual of (8.1), which for a fixed $\mathbf x$ maximizes $x_0$ subject to $M^T \mathbf x - \mathbf 1 x_0 \ge \mathbf 0$; program (8.2), the same with $\mathbf x$ as variables subject to $\sum_i x_i = 1$, $\mathbf x \ge \mathbf 0$; and program (8.4), which minimizes $y_0$ subject to $M \mathbf y - \mathbf 1 y_0 \le \mathbf 0$, $\sum_j y_j = 1$, $\mathbf y \ge \mathbf 0$.

Formalization targets

Goal: Theorem 8.1.3 (minimax theorem for zero-sum games)

For every $m \times n$ payoff matrix with $m, n \ge 1$: worst-case optimal mixed strategies exist for both players; for any worst-case optimal $\tilde{\mathbf x}$ of Alice and $\tilde{\mathbf y}$ of Bob, the pair $(\tilde{\mathbf x}, \tilde{\mathbf y})$ is a mixed Nash equilibrium; and there is a single number $v$, the value of the game, with

$$\beta(\tilde{\mathbf x}) = \tilde{\mathbf x}^T M \tilde{\mathbf y} = \alpha(\tilde{\mathbf y}) = v$$

for every such pair. The third clause is what distinguishes the theorem from the existence of some saddle point.

Milestones

1. $\beta$ and $\alpha$ are attained minima and maxima (p. 135).
2. Lemma 8.1.2(i): $\beta(\mathbf x) \le \mathbf x^T M \mathbf y \le \alpha(\mathbf y)$ for all mixed $\mathbf x, \mathbf y$, hence $\max_{\mathbf x}\beta \le \min_{\mathbf y}\alpha$.
3. Lemma 8.1.2(ii): both strategies of a mixed Nash equilibrium are worst-case optimal.
4. Lemma 8.1.2(iii): $\beta(\tilde{\mathbf x}) = \alpha(\tilde{\mathbf y})$ implies that $(\tilde{\mathbf x}, \tilde{\mathbf y})$ is a mixed Nash equilibrium.
5. The dual of (8.1) has optimal value $\beta(\mathbf x)$ (p. 137).
6. Eq. (8.3): an optimal solution $(\tilde x_0, \tilde{\mathbf x})$ of (8.2) satisfies $\tilde x_0 = \beta(\tilde{\mathbf x}) = \max_{\mathbf x}\beta(\mathbf x)$.
7. Eq. (8.5): an optimal solution $(\tilde y_0, \tilde{\mathbf y})$ of (8.4) satisfies $\tilde y_0 = \alpha(\tilde{\mathbf y}) = \min_{\mathbf y}\alpha(\mathbf y)$.
8. Programs (8.2) and (8.4) both have optimal solutions, and their optimum values coincide (p. 138).
9. The minimax equality (p. 137):

$$\max_{\mathbf x}\min_{\mathbf y}\mathbf x^T M \mathbf y = \min_{\mathbf y}\max_{\mathbf x}\mathbf x^T M \mathbf y .$$

Significance

The theorem gives a complete prescription for zero-sum play: a worst-case optimal strategy secures at least the value against any opponent, and a worst-case optimal opponent holds the player to at most the value, so both players can announce their strategies in advance without loss. With Lemma 8.1.2(ii) it yields a characterization: a pair of mixed strategies is a Nash equilibrium if and only if both are worst-case optimal. The minimax equality is used downstream in online learning (regret-to-value arguments), in robust optimization, and in Yao's principle for randomized algorithms.

The mathematics is classical and proved; what this mission adds is a machine-checked version in the book's own formulation. The platform already has AGT.zero_sum_minimax (Algorithmic Game Theory I), which proves the existence of a saddle point, and the general FamousTheorems.sion_minimax_theorem. Neither states that every pair of worst-case optimal strategies is an equilibrium with a common value, and neither exhibits the LP route: the dual of (8.1), the programs (8.2) and (8.4), and their duality. The mission records that route statement by statement, so that it can be reused as a worked instance of LP duality.

Difficulty

Lemma 8.1.2 is routine; the entire content is the reverse inequality $\max_{\mathbf x}\beta(\mathbf x) \ge \min_{\mathbf y}\alpha(\mathbf y)$. The obvious attack, maximizing $\beta$ directly, fails because $\beta$ is a minimum of linear functions and hence not linear, so its maximization is not a linear program as written. The obstacle is removed only by an appeal to LP duality in the proof, together with the facts that the simplices are nonempty and compact, and that the relevant programs are feasible and bounded so that optima exist. None of this is supplied by the pure-strategy structure of the game: pure Nash equilibria need not exist (rock–paper–scissors has none).

Formalization scope

Pure strategies are indexed by Fin m and Fin n, with the book's standing assumption $m, n \ge 1$ carried as hypotheses 1 ≤ m, 1 ≤ n by every theorem; the book's indices $1,\dots,m$ become $0,\dots,m-1$. Mixed strategies are Mathlib's stdSimplex ℝ (Fin m), the payoff is x ⬝ᵥ (M *ᵥ y). $\beta(\mathbf x)$ is the real sInf and $\alpha(\mathbf y)$ the real sSup of the payoffs over the opponent's simplex; milestone 1 states that these are attained. A mixed Nash equilibrium is defined in the verbal form of Definition 8.1.1 (mutual best responses). Worst-case optimality is defined against all mixed strategies, never as a saddle-point condition, so the goal is not circular with Lemma 8.1.2(iii). LP optimality is stated as "feasible and at least as good as every feasible point", so no supremum over a possibly empty or unbounded feasible set is used.

The book's clause that worst-case optimal strategies "can be efficiently computed by linear programming" is algorithmic and is not part of the formal statement; there is no complexity model. A goal asserting only the existence of worst-case optimal strategies, or only the existence of some equilibrium, would drop the theorem's third clause and is ruled out: the common value $v$ is quantified before all pairs of worst-case optimal strategies.

A complete development needs compactness of the standard simplex, continuity of the bilinear payoff, and a strong duality theorem for linear programs in the form of the programs (8.2)/(8.4); the latter is reusable across the whole series. Proofs by other routes (Sion's theorem, a separating hyperplane argument, fixed points) are welcome for the goal; the LP milestones stand on their own as statements about the programs.

Selected references

• J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §8.1, pp. 131–142. https://doi.org/10.1007/978-3-540-30717-4
• J. von Neumann, "Zur Theorie der Gesellschaftsspiele", Mathematische Annalen 100 (1928), 295–320. https://doi.org/10.1007/BF01448847
• M. Sion, "On general minimax theorems", Pacific Journal of Mathematics 8 (1958), 171–176. https://doi.org/10.2140/pjm.1958.8.171

Motivation

Scheduling indivisible jobs on parallel machines to finish all of them as early as possible is a basic problem in operations research and in the theory of algorithms. In the unrelated machines model each job may take a different time on each machine, with no relation between the rows of the time table, as when machines of different types (black-and-white, duplex, colour copiers in the book's example) handle jobs of different kinds. Minimizing the makespan in this model is NP-hard, so the question is how close to the optimum a polynomial-time algorithm can get.

• 1990. Lenstra, Shmoys and Tardos (Math. Programming 46, 259–271) give a polynomial-time algorithm that rounds a basic optimal solution of a linear programming relaxation and returns a schedule of makespan at most $2\,t_{\mathrm{opt}}$. The same paper shows that approximating the optimum makespan within a factor less than $3/2$ is NP-hard.
• 2007. Matoušek and Gärtner present the algorithm in §8.3 of Understanding and Using Linear Programming in a simplified, somewhat less efficient form: minimize $t^*(T) + T$ over the thresholds $T$ rather than binary-searching for the smallest $T$ with $t^*(T) \le T$. This mission follows the book's presentation.

The gap between $3/2$ and $2$ for the general unrelated-machines problem has remained open since 1990; it is the standard example of LP rounding driven by the sparsity of basic solutions.

Setting

There are $m$ machines $M$ and $n$ jobs $J$; $d_{ij} > 0$ is the running time of job $j$ on machine $i$. A schedule is a map $\sigma : J \to M$ assigning each job to one machine. The load of machine $i$ is $\sum_{j:\sigma(j)=i} d_{ij}$, the makespan of $\sigma$ is the largest load, and $t_{\mathrm{opt}}$ is the makespan of an optimal schedule, one whose makespan is at most that of every schedule.

For a real threshold $T$, the linear program $\mathrm{LPR}(T)$ in the variables $t$ and $x_{ij}$ is

$$\begin{aligned} \text{minimize } \ & t \\ \text{subject to } \ & \textstyle\sum_{i \in M} x_{ij} = 1 \ \ (j \in J), \qquad \textstyle\sum_{j \in J} d_{ij} x_{ij} \le t \ \ (i \in M),\\ & x_{ij} \ge 0, \qquad x_{ij} = 0 \ \text{ whenever } d_{ij} > T . \end{aligned}$$

Its optimal value is $t^*(T)$, with $t^*(T) = \infty$ when $\mathrm{LPR}(T)$ is infeasible. The constraint matrix $A$ has one row per machine, one per job and one per pair with $d_{ij} > T$; the column of $x_{ij}$ carries $d_{ij}$ in the row of machine $i$, $1$ in the row of job $j$, and $1$ in the row of the constraint $x_{ij} = 0$ if present. Assumption 8.3.1 on a solution $x^*$ is that the columns of $A$ belonging to its nonzero variables are linearly independent; basic feasible solutions satisfy it. The support graph of $x^*$ is the bipartite graph $G = (M \cup J, E)$ with $E = \{\{i,j\} : x^*_{ij} > 0\}$.

Formalization targets

Goal: Theorem 8.3.4

Let $T^*$ minimize $t^*(T) + T$ over all real $T$ and let $(t^*, x^*)$ be an optimal solution of $\mathrm{LPR}(T^*)$ satisfying Assumption 8.3.1. Then there is a schedule $\sigma$ with $x^*_{\sigma(j) j} > 0$ for every job $j$ and

$$\max_{i \in M} \sum_{j : \sigma(j) = i} d_{ij} \;\le\; 2\, t_{\mathrm{opt}} .$$

Milestones

1. Lemma 8.3.2. Every subgraph of the support graph $G$ has at most as many edges as vertices: $|E'| \le |M'| + |J'|$.
2. Lemma 8.3.3. For $T \ge 0$ and an optimal solution $(t^*, x^*)$ of $\mathrm{LPR}(T)$ satisfying Assumption 8.3.1, some schedule along the edges of $G$ has makespan at most $t^* + T$.
3. Proof of Theorem 8.3.4, first step. $\mathrm{LPR}(t_{\mathrm{opt}})$ is feasible and $t^*(t_{\mathrm{opt}}) \le t_{\mathrm{opt}}$.
4. Proof of Theorem 8.3.4, second step. $t^*(T^*) + T^* \le 2\,t_{\mathrm{opt}}$.

Significance

The theorem gives a polynomial-time 2-approximation for an NP-hard problem, and its proof isolates a reusable principle: a basic solution of an assignment-type LP has a support graph in which every subgraph has at most as many edges as vertices (a pseudoforest), so all but a matching's worth of the fractional assignment is already integral. The same sparsity argument underlies rounding results for the generalized assignment problem and for many later scheduling and allocation relaxations.

The result has been proved since 1990 and is textbook material. It is not formalized on Prove2Me or, to the maintainers' knowledge, in Mathlib. This mission produces a machine-checked version of the rounding theorem together with the counting lemma on basic solutions, the relaxation inequality $t^*(t_{\mathrm{opt}}) \le t_{\mathrm{opt}}$, and the bound on the chosen threshold, each stated on shared definitions of the scheduling LP.

Difficulty

The obvious approach, rounding every job to the machine carrying the largest fraction of it, can overload a machine by many jobs at once and gives no constant factor. The bound $t^* + T$ needs two facts that are not visible from the LP value alone: that the support of a basic solution is sparse in the precise sense of Lemma 8.3.2, which has to be read off the linear independence of columns of the constraint matrix after deleting rows; and that the jobs left fractional can be matched injectively to machines, which requires a Hall-type condition derived from that sparsity. Relating linear independence of real column vectors to an edge count in a bipartite graph, and then producing a matching, is where the formal work lies.

A second subtlety is the threshold $T$: the bound $t^* + T \le 2 t_{\mathrm{opt}}$ holds only because $T^*$ is chosen by minimizing over thresholds, and the relaxation at $T = t_{\mathrm{opt}}$ must be compared with the one at $T^*$ through optimal solutions of different linear programs.

Formalization scope

Machines are Fin m, jobs are Fin n (0-based; the book's machines $1,\dots,m$ and jobs $m+1,\dots,m+n$ are disjoint index sets), running times form d : Matrix (Fin m) (Fin n) ℝ, and the standing hypothesis $d_{ij} > 0$ of §8.3 appears in every theorem. A schedule is a function Fin n → Fin m; the makespan is the supremum of the loads over the finite type Fin m, which is the maximum for $m \ge 1$. The optimum $t_{\mathrm{opt}}$ is the makespan of a schedule assumed optimal, never an infimum.

Optimal values of $\mathrm{LPR}(T)$ are never written as sInf: statements quantify over optimal solutions, i.e. feasible $(t, x)$ with $t \le t'$ for every feasible $(t', x')$. The book's convention $t^*(T) = \infty$ for infeasible $\mathrm{LPR}(T)$ is encoded by letting thresholds without an optimal solution impose no condition in the minimality hypothesis on $T^*$, which reads $t^* + T^* \le t + T$ for every real $T$ and every optimal solution $(t, x)$ of $\mathrm{LPR}(T)$. The constraint matrix used in Assumption 8.3.1 has rows indexed by Fin m ⊕ Fin n ⊕ {(i, j) // T < d i j} and excludes the column of $t$, as on p. 151.

"Efficiently construct" in Lemma 8.3.3 and "computes" in Theorem 8.3.4 are formalized by the property of the constructed schedule, not by its running time: every job goes to a machine $i$ with $x^*_{ij} > 0$. This constraint is what rules out the trivializing formalization — "some schedule has makespan at most $2 t_{\mathrm{opt}}$" is true of the optimal schedule itself and says nothing about the rounding.

A complete development needs: finite linear algebra (a linearly independent family of vectors supported on $k$ coordinates has at most $k$ members), Hall's marriage theorem (available in Mathlib as Finset.all_card_le_biUnion_card_iff_exists_injective), and the existence of an optimal solution of a feasible, bounded linear program (used to apply the minimality of $T^*$ at $T = t_{\mathrm{opt}}$). The counting lemma for basic solutions and the definitions of $\mathrm{LPR}(T)$ are reusable for other assignment relaxations. Proofs of any milestone, and alternative proofs of Lemma 8.3.3 by the direct pseudoforest argument of p. 153–154, are welcome.

Selected references

• J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §8.3, pp. 148–156. https://doi.org/10.1007/978-3-540-30717-4
• J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, Mathematical Programming 46 (1990), 259–271. https://doi.org/10.1007/BF01585745

Motivation

A binary error-correcting code is a set of $n$-bit words chosen so that the words stay distinguishable after a few bits have been corrupted in transmission. A code can correct any $r$ errors exactly when every two of its words differ in at least $2r+1$ positions. The more words the code has, the more information each transmitted block carries. So the central quantitative question of coding theory is how large a code of given length and minimum distance can be. Codes are used in every technology that transmits or stores data, from disks and phones to deep-space probes.

In 1973 Philippe Delsarte showed that an upper bound on this maximum size is the optimum value of an explicit linear program (Delsarte, An algebraic approach to the association schemes of coding theory, Philips Res. Repts. Suppl. 10, 1973). The bound was far stronger than the classical volume argument and remains a standard tool. This mission formalizes the self-contained proof of the bound in §8.4 of Matoušek and Gärtner's textbook (Springer 2007). That proof follows Best, Brouwer, MacWilliams, Odlyzko and Sloane (IEEE Trans. Inform. Theory 24, 1978). The mission also covers the step of Delsarte's original argument that the book isolates as a lemma.

Timeline.

• 1950: Hamming introduces single-error-correcting codes and the sphere-packing bound.
• 1973: Delsarte proves the linear programming bound using association schemes.
• 1978: Best et al. give the elementary parity proof and small improvements, among them $A(17,3) \le 6552$.
• 2005: Schrijver replaces the linear program by a semidefinite program and improves many entries of the code tables (IEEE Trans. Inform. Theory 51).

Setting

A word is $\mathbf w = (w_1,\dots,w_n) \in \{0,1\}^n$, and a code is any set $C \subseteq \{0,1\}^n$. The Hamming distance $d_H(\mathbf w,\mathbf w')$ is the number of positions $j$ with $w_j \ne w'_j$. The weight $|\mathbf w|$ is the number of ones in $\mathbf w$. The word $\mathbf w \oplus \mathbf w'$ is the entrywise sum modulo 2. For $I \subseteq \{1,\dots,n\}$, the restricted distance $d^I_H(\mathbf w,\mathbf w')$ counts only the differing positions that lie in $I$.

A code has distance $d$ if $d_H(\mathbf w,\mathbf w') \ge d$ for all distinct $\mathbf w,\mathbf w' \in C$ (Definition 8.4.1). The quantity $A(n,d)$ is the maximum of $|C|$ over all codes $C \subseteq \{0,1\}^n$ with distance $d$.

For $0 \le i,t \le n$ the Krawtchouk numbers are

$$K_t(n,i) = \sum_{j=0}^{\min(i,t)} (-1)^j \binom ij \binom{n-i}{t-j}.$$

The distance distribution of a code $C$ is

$$\tilde x_i(C) = \frac{1}{|C|}\,\bigl|\{(\mathbf w,\mathbf w')\in C^2 : d_H(\mathbf w,\mathbf w') = i\}\bigr|, \qquad i=0,\dots,n.$$

The Delsarte linear program has variables $x_0,\dots,x_n$. It maximizes $x_0+\dots+x_n$ subject to:

• $x_0 = 1$;
• $x_i = 0$ for $1 \le i \le d-1$;
• $\sum_{i=0}^n K_t(n,i)\,x_i \ge 0$ for $1 \le t \le n$;
• $x \ge 0$.

For Delsarte's original argument, $M_i$ is the $2^n\times 2^n$ matrix whose $(\mathbf v,\mathbf w)$ entry is $1$ when $d_H(\mathbf v,\mathbf w) = i$ and $0$ otherwise. The weights are $\tilde y_i = |\{(\mathbf w,\mathbf w')\in C^2 : d_H = i\}| / (2^n\binom ni)$.

Formalization targets

Goal: Theorem 8.4.3 (the Delsarte bound)

$$A(n,d) \;\le\; \max\Bigl\{\textstyle\sum_{i=0}^n x_i \;:\; x \text{ feasible for the Delsarte program}\Bigr\}\quad\text{for all } n, d.$$

The goal is stated against every upper bound $v$ of the objective on the feasible set. No particular optimum value is fixed, so the statement covers every $n$ and $d$ at once.

Milestones, in attack order

1. Lemma 8.4.5. For every $I$ and $C$, the pairs in $C^2$ with even $d^I_H$ are at least as many as the pairs with odd $d^I_H$.
2. Corollary 8.4.6. $\sum_{(\mathbf w,\mathbf w')\in C^2}(-1)^{(\mathbf w\oplus\mathbf w')^T\mathbf v}\ge 0$ for every $\mathbf v$.
3. Proposition 8.4.4. $\sum_{i=0}^n K_t(n,i)\,\tilde x_i(C) \ge 0$ for every $C$ and every $t = 1,\dots,n$.
4. §8.4, p. 160. The values $\tilde x_i(C)$ sum to $|C|$. For a nonempty code with distance $d$, the vector $\tilde x(C)$ is feasible for the program.
5. Lemma 8.4.2 (sphere-packing bound). $A(n,2r+1) \le \lfloor 2^n / \sum_{i=0}^r\binom ni\rfloor$.
6. Lemma 8.4.7. $\tilde M = \sum_{i=0}^n \tilde y_i M_i$ is positive semidefinite.

Significance

The Delsarte bound turns an extremal problem over the $2^{2^n}$ subsets of the cube into a linear program with $n+1$ variables. For $A(17,3)$ it gives $6553$, while the sphere-packing bound gives $7281$. Many entries of the standard code tables rest on this bound or its refinements. The positive semidefiniteness in Lemma 8.4.7 is the starting point of the semidefinite programming bounds of Schrijver and of later work. The same framework also underlies the linear programming bounds for spherical codes and sphere packings.

The theorem is classical and fully proved in the literature. Neither Mathlib nor this platform has a formal statement or proof of it. Mathlib has Hamming distance and binomial coefficients, but it has no $A(n,d)$, no Krawtchouk numbers and no LP bound for codes. This mission would produce the first formal statement and proof. It would also produce reusable identities on Krawtchouk sums and character sums over $\{0,1\}^n$.

Difficulty

Two of the program's constraints are immediate once $\tilde x_i$ is defined: $\tilde x_0 = 1$, and $\tilde x_i = 0$ for $i < d$. The difficulty lies in the Krawtchouk constraints. They do not follow from counting pairs at a single distance. They require a sign-weighted count over all words of weight $t$, and the sum must then be regrouped by the distance of each pair. That regrouping identifies a count of words, split by how many ones they share with a fixed word, with the Krawtchouk number. Formally this is an exchange of finite sums together with a binomial counting identity, and the index bookkeeping, including the range $j \le \min(i,t)$, has to be exact.

The obvious attempt proves the inequality one distance class at a time. It fails because the individual terms $K_t(n,i)\,\tilde x_i$ have no sign. Only the whole sum is nonnegative.

Formalization scope

• Words and codes. Words are Fin n → Bool, with bit $1$ as true. The book's positions $1,\dots,n$ become 0, …, n-1. Codes are Finsets of words, and $d_H$ is Mathlib's hammingDist.
• The maximum $A(n,d)$. $A(n,d)$ is a Finset.sup over the finite family of codes with distance $d$. This family contains the empty code, so the maximum is attained.
• Krawtchouk numbers. $K_t(n,i)$ is an integer, and its natural-number subtractions are honest for $i \le n$ and $j \le t$.
• LP variables and the $x_i = 0$ constraints. The LP variables are indexed by Fin (n+1) with no index shift. The constraints $x_i = 0$ are imposed for $1 \le i < d$, so they are vacuous for $d \le 1$.
• The empty code. Lean's convention $1/0 = 0$ gives $\tilde x(\emptyset) = 0$. Proposition 8.4.4 then holds trivially, and the feasibility milestone carries the hypothesis $C \ne \emptyset$ that the book's division presupposes.
• The sphere-packing floor. The floor in the sphere-packing bound is natural-number division by a denominator that is at least $1$.
• Positive semidefiniteness. This is Mathlib's Matrix.PosSemidef over $\mathbb R$.

No trivialization. The goal is not stated as "$A(n,d) \le \sup$" with a real supremum, which Lean would evaluate to $0$ on an empty or unbounded set. Its hypothesis ranges over upper bounds of a feasible program: $(1,0,\dots,0)$ is always feasible, so the hypothesis is never vacuous.

Contributions welcome. Useful lemmas include:

• Krawtchouk identities, for example $\sum_{t}K_t(n,i) = 2^n[i=0]$ and $K_i(n,t)\binom ni = K_t(n,i)\binom nt$;
• counting words of weight $t$ that meet a fixed support in exactly $j$ positions;
• general facts on character sums $\sum_{\mathbf w\in C}(-1)^{\mathbf w^T\mathbf v}$.

These are reusable for other LP and SDP bounds in coding theory.

Selected references

• J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §8.4. https://doi.org/10.1007/978-3-540-30717-4
• P. Delsarte, An algebraic approach to the association schemes of coding theory, Philips Research Reports Supplements 10, 1973.
• M. R. Best, A. E. Brouwer, F. J. MacWilliams, A. M. Odlyzko, N. J. A. Sloane, Bounds for binary codes of length less than 25, IEEE Trans. Inform. Theory 24 (1978), 81–93. https://doi.org/10.1109/TIT.1978.1055827
• A. Schrijver, New code upper bounds from the Terwilliger algebra and semidefinite programming, IEEE Trans. Inform. Theory 51 (2005), 2859–2866. https://doi.org/10.1109/TIT.2005.851748

Motivation

A deep-space probe sends a vector $w\in\mathbb{R}^k$ encoded as $z=Qw\in\mathbb{R}^n$, and up to about 8% of the transmitted numbers may be corrupted arbitrarily. Section 8.5 of Matoušek and Gärtner's Understanding and Using Linear Programming (Springer 2007, DOI 10.1007/978-3-540-30717-4) shows that decoding reduces to finding a sparse solution of an underdetermined linear system $Ax=b$, and that under suitable conditions this sparse solution is found exactly by a single linear program. The same problem arises in signal processing (sparse representations in redundant wavelet dictionaries) and in computer tomography, and it is the core of what became known as compressed sensing.

Timeline, as recorded in the book's references:

• 1999: Chen, Donoho and Saunders introduce basis pursuit, minimizing the $\ell_1$-norm subject to $Ax=b$ (SIAM J. Sci. Comput. 20).
• 2005: Candès, Rudelson, Tao and Vershynin prove that for every $\alpha\in(0,1)$ there is $\beta(\alpha)>0$ such that a random $\lfloor\alpha n\rfloor\times n$ matrix is exact for $\lfloor\beta n\rfloor$-sparse vectors with probability exponentially close to 1 (FOCS 2005).
• 2006: Donoho, via neighborliness of centrally symmetric polytopes, obtains the constants $\alpha=0.75$, $\beta=0.08$ used in the book, and shows that no $\lfloor 0.75n\rfloor\times n$ matrix is exact for $r>0.25n$ when $n$ is large (Discrete Comput. Geom. 35).
• 2006: Linial and Novik prove further upper bounds showing that these existence results are asymptotically optimal (Discrete Comput. Geom. 36).

Setting

Let $A$ be a real $m\times n$ matrix with $m<n$ and $b\in\mathbb{R}^m$. The support of $x\in\mathbb{R}^n$ is $\operatorname{supp}(x)=\{i: x_i\ne 0\}$. For an integer $r\ge 0$, a sparse solution of $Ax=b$ is an $x$ with $Ax=b$ and $|\operatorname{supp}(x)|\le r$. The $\ell_1$-norm is $\|x\|_1=|x_1|+\dots+|x_n|$.

Basis pursuit is the optimization problem

$$\text{(BP)}\qquad\text{minimize } \|x\|_1\ \text{ subject to } x\in\mathbb{R}^n,\ Ax=b,$$

which is equivalent to the linear program

$$\text{(BP}'\text{)}\qquad\text{minimize } u_1+\dots+u_n\ \text{ subject to } Ax=b,\ -u\le x\le u,\ u\ge 0 .$$

The matrix $A$ is BP-exact for $r$ if for every $b\in\mathbb{R}^m$: whenever $Ax=b$ has a solution $\tilde x$ with at most $r$ nonzero components, $\tilde x$ is the unique optimal solution of (BP). The crosspolytope is $B^n_1=\{x:\|x\|_1\le 1\}$, the kernel of $A$ is $L=\{x: Ax=0\}$, and $L+z=\{\ell+z:\ell\in L\}$. For $z$ with $\|z\|_1=1$, the cone at $z$ is $C_z=\{t(x-z): t\ge 0,\ x\in B^n_1\}$, and $L$ is good for $z$ if $(L+z)\cap B^n_1=\{z\}$.

Formalization targets

Goal: Lemma 8.5.4 (reformulation of BP-exactness)

For $m<n$ and $r\le m$:

$$A \text{ is BP-exact for } r\iff \forall z\in\mathbb{R}^n\ \text{with}\ \|z\|_1=1,\ |\operatorname{supp}(z)|\le r:\quad (L+z)\cap B^n_1=\{z\}.$$

This is the book's geometric characterization of exact recovery, and the statement on which the known probabilistic proofs are built.

Milestones

1. Observation 8.5.1: $Ax=b$ has at most one sparse solution for every $b$ if and only if every $2r$ or fewer columns of $A$ are linearly independent.
2. The remark after it (p. 169): under $m<n$, that column condition forces $m\ge 2r$.
3. Equivalence of (BP) and (BP′) (p. 170): in every optimal solution of (BP′), $u_i=|x_i|$; and $x$ is optimal for (BP) iff $(x,|x|)$ is optimal for (BP′).
4. From the proof of Lemma 8.5.4 (p. 173): if $Az=b$, the solution set of $Ax=b$ is exactly $L+z$.
5. From "Intuition for BP-exactness" (p. 174): for $\|z\|_1=1$ and $|\operatorname{supp}(z)|\le r$, $L$ is good for $z$ iff $L\cap C_z=\{0\}$.

Further draft item: Theorem 8.5.2

With $m=\lfloor 0.75n\rfloor$, $r=\lfloor 0.08n\rfloor$ and $A$ an $m\times n$ matrix of independent $N(0,1)$ entries, there is a constant $c>0$ such that for every $n$

$$\Pr[A \text{ is BP-exact for } r]\ \ge\ 1-e^{-cm}.$$

The book states this without proof. It is included as a separate theorem, not a milestone of the goal.

Significance

Lemma 8.5.4 converts an algorithmic property, that an $\ell_1$ linear program returns a prescribed sparse vector for every right-hand side, into a purely geometric property of the kernel of $A$ relative to the low-dimensional faces of the crosspolytope. With milestone 5 it becomes the statement that $L$ avoids a finite family of cones, which is where union bounds over faces and estimates for random subspaces enter. Observation 8.5.1 separates what is information-theoretically possible (uniqueness of sparse solutions) from what is computationally achievable by linear programming; finding a sparse solution directly is NP-hard in general. Theorem 8.5.2 is the quantitative payoff: a fixed fraction of arbitrary gross errors can be corrected by solving one linear program.

All of these results are proved in the literature; Lemma 8.5.4, Observation 8.5.1 and the milestones are elementary, and Theorem 8.5.2 rests on Donoho's polytope-neighborliness analysis. The platform has a related formalization of Wainwright's restricted nullspace property (Theorem 7.8 of High-Dimensional Statistics, namespace HighDimStat.SparseLinear), which fixes a support set $S$ rather than characterizing exactness for all $r$-sparse vectors through the crosspolytope. A machine-checked proof of Theorem 8.5.2 with the constants $0.75$ and $0.08$ is, to our knowledge, not available anywhere; it would require substantial Gaussian and high-dimensional geometry infrastructure.

Difficulty

For the goal and milestones the difficulty is bookkeeping, not ideas: the scaling between a sparse solution $\tilde x$ and the boundary point $\tilde x/\|\tilde x\|_1$, the case $\tilde x=0$, and the fact that BP-exactness quantifies over all right-hand sides $b$ while the geometric side quantifies over boundary points of the crosspolytope.

Theorem 8.5.2 is of a different order. A union bound over the $\binom{n}{r}2^r$ faces of dimension $r-1$ reduces it to bounding the probability that a random $(n-m)$-dimensional subspace meets one cone $C_F$ nontrivially, and getting that probability small enough to beat the combinatorial factor with the stated numerical constants is the hard part. Rough asymptotic estimates do not give $0.08$ at $\alpha=0.75$.

Formalization scope

Vectors are functions Fin n → ℝ (the book's indices $1,\dots,n$ become $0,\dots,n-1$) and matrices are Matrix (Fin m) (Fin n) ℝ. The $\ell_1$-norm is written out as $\sum_i|x_i|$, since Mathlib's norm on Fin n → ℝ is the sup norm. The support is a Finset of indices. Optimality in (BP) and (BP′) is stated against every feasible point; no infimum is taken, so an empty or unbounded feasible set cannot create a spurious optimum. "Every $2r$ or fewer columns" ranges over finsets of distinct column indices, column $j$ being Aᵀ j. The hypotheses $m<n$ and $r\le m$ of Lemma 8.5.4 are kept as on the page, although the equivalence does not use them; $m<n$ is also the standing assumption of §8.5 needed for $m\ge 2r$.

In Theorem 8.5.2 the random matrix has the product law of independent gaussianReal 0 1 entries, the constant $c>0$ is quantified before $n$, and measurability of the BP-exact event is part of the conclusion, so the bound concerns a genuine probability rather than an outer measure.

A trivializing formalization is ruled out: BP-exactness requires uniqueness among all minimizers for every right-hand side, not just optimality of $\tilde x$, and the crosspolytope condition is an equality of sets, not an inclusion that $z$ alone would satisfy.

All definitions live in one module (MatousekLP.SparseRecovery.BasisPursuit); the $\ell_1$ and support vocabulary is reusable for later sparse-recovery missions. Contributions are welcome on every milestone, on the goal, and on the infrastructure towards Theorem 8.5.2 (Gaussian measures on matrix spaces, measurability of the BP-exact event, the face structure of the crosspolytope).

Selected references

• J. Matoušek and B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §8.5. https://doi.org/10.1007/978-3-540-30717-4
• S. S. Chen, D. L. Donoho and M. A. Saunders, Atomic decomposition by basis pursuit, SIAM J. Sci. Comput. 20(1), 1999, 33–61. https://doi.org/10.1137/S1064827596304010
• E. J. Candès, M. Rudelson, T. Tao and R. Vershynin, Error correction via linear programming, Proc. 46th IEEE FOCS, 2005, 295–308. https://doi.org/10.1109/SFCS.2005.5464411
• D. L. Donoho, High-dimensional centrally symmetric polytopes with neighborliness proportional to dimension, Discrete Comput. Geom. 35, 2006, 617–652. https://doi.org/10.1007/s00454-005-1220-0
• N. Linial and I. Novik, How neighborly can a centrally symmetric polytope be?, Discrete Comput. Geom. 36, 2006, 273–281. https://doi.org/10.1007/s00454-006-1235-1