Linear Optimization

Motivation

Resource-constrained project scheduling with minimum and maximum time lags is the model behind make-to-order production, process-industry batch planning and large engineering projects. When the objective is the project duration or another regular function (nondecreasing in every start time), an optimum can be found among schedules that cannot be shifted to the left. Many objectives in practice are nonregular: net present value, earliness–tardiness costs, resource levelling and resource investment. For these, delaying an activity can pay, and "shift as far left as possible" no longer identifies a finite set of candidate schedules.

Neumann, Nübel and Schwindt (Math. Methods Oper. Res. 52, 2000) answered this with classes of schedules defined by the absence of pairs of opposite shifts: stable, semistable, pseudostable and quasistable schedules, the mirror image of active, semiactive, pseudoactive and quasiactive schedules. Section 3.2 of Neumann, Schwindt and Zimmermann, Project Scheduling with Time Windows and Scarce Resources (Springer 2003), shows that these classes are exactly the extreme points of the feasible region and of its natural convex pieces. The classification of objective functions in §3.3, and every enumeration scheme of the later chapter, rests on that correspondence.

Setting

A project has activities $V=\{0,1,\dots,n+1\}$ with $n\ge1$. Activity $0$ is the project beginning and $n+1$ the project completion. Activity $i$ has an integer duration $p_i$, with $p_0=p_{n+1}=0$ and $p_i>0$ otherwise. The project network $N$ has node set $V$ and arcs $\langle i,j\rangle\in E$ with integer weights $\delta_{ij}$, each encoding a temporal constraint $S_j-S_i\ge\delta_{ij}$. A prescribed deadline $\bar d\in\mathbb N$ is included as the backward arc $\langle n+1,0\rangle$ of weight $-\bar d$. Renewable resources $k$ have capacities $R_k$, and activity $i$ uses $r_{ik}\le R_k$ units while it runs.

A schedule is a vector $S\in\mathbb R^{n+2}$ of start times. The time-feasible region $\mathcal S_T$ collects the schedules with $S_0=0$, $S\ge0$ and $S_j-S_i\ge\delta_{ij}$ on every arc; it is a polyhedron, and a polytope when every activity precedes $n+1$ as in Remarks 1.1.2. A schedule is resource-feasible if at every time $t\ge0$ the running activities $\mathcal A(S,t)=\{i\mid S_i\le t<S_i+p_i\}$ use at most $R_k$ units of every resource. The feasible region is $\mathcal S=\mathcal S_T\cap\mathcal S_R$. It is in general neither convex nor connected.

A schedule induces the strict order $O(S)=\{(i,j)\mid i\ne j,\ S_j\ge S_i+p_i\}$. For a strict order $O$, the order polytope is $\mathcal S_T(O)=\{S\in\mathcal S_T\mid S_j\ge S_i+p_i\ ((i,j)\in O)\}$. The order $O$ is feasible if $\emptyset\ne\mathcal S_T(O)\subseteq\mathcal S$. The schedule polytope of $S$ is $\mathcal S_T(O(S))$.

A shift moves a schedule $S$ to $S'\neq S$. It is global if both are feasible, local if in addition a continuous path inside $\mathcal S$ joins them, order-preserving if $O(S)\subseteq O(S')$, and order-monotone if $O(S)$ and $O(S')$ are comparable. Two shifts from $S$ to $S'$ and $S''$ are opposite if $S''-S=\lambda(S'-S)$ with $\lambda<0$. A feasible schedule is stable, semistable, pseudostable or quasistable if no pair of opposite global, local, order-monotone or order-preserving shifts, respectively, starts at it. It is antiactive if no global right-shift starts at it.

Formalization targets

Goal: Theorem 3.2.10

For every feasible schedule $S$:

$$\begin{aligned} &\text{(a) } S\text{ antiactive}\iff S\text{ maximal in }\mathcal S, \qquad \text{(b) } S\text{ stable}\iff S\in\operatorname{ext}\mathcal S,\\ &\text{(c) } S\text{ semistable}\iff S\in\operatorname{ext}C_S,\ C_S\text{ the component of }\mathcal S\text{ containing }S,\\ &\text{(d) } S\text{ pseudostable}\iff S\in\operatorname{ext}\mathcal S_T(O)\ \text{for all feasible }O\subseteq O(S),\\ &\text{(e) } S\text{ quasistable}\iff S\in\operatorname{ext}\mathcal S_T(O(S)). \end{aligned}$$

Milestones

• Lemma 3.2.4: opposite order-preserving or order-monotone shifts can be taken uniform (all moved activities move by one common amount).
• Lemma 3.2.8: pseudostable schedules are the local extreme points of $\mathcal S$, the points on no segment that lies entirely in $\mathcal S$.
• Lemma 3.2.9: when $S$ is not pseudostable, a segment through $S$ can be found inside one order polytope $\mathcal S_T(O)$ with $O\subseteq O(S)$ feasible.
• Proposition 3.2.13: the quasistable schedules, and every class below them in Fig. 3.2.6, form finite sets.
• Proposition 3.2.16: every vertex of $\mathcal S_T$ is the unique solution of $S_0=0$, $S_j-S_i=\delta_{ij}$ on the arcs of a spanning tree of $N$; for the minimal point, an outtree rooted at $0$.
• Theorem 3.2.18: $S$ is quasistable iff it is the unique solution of such a tree system in the schedule network $N(O(S))$.
• Remark 3.2.7: every activity of a quasistable schedule is tied to another one by a tight duration or time lag, so quasistable schedules are integer-valued.

Significance

The theorem makes four shift-defined classes computable objects: extreme points of explicit polytopes, or of a finite union of them. Together with Proposition 3.2.13, it gives each class of nonregular objective functions in §3.3 a finite candidate set of schedules among which an optimum can be sought (§3.2, p. 207). Theorem 3.2.18 gives the certificate for quasistable schedules: a spanning tree of the schedule network, which the later sections use to enumerate vertices.

The results are proved in the book, except Lemma 3.2.9, whose proof is cited to Neumann, Nübel and Schwindt (2000). As far as a search of the platform shows, none of them has been formalized. A formalization supplies the missing details, among them that connected and path components of $\mathcal S$ coincide and the degenerate vertices behind the tree description. It also produces a reusable library of schedule classes on real-valued start times.

Difficulty

Part (b) is close to the definition, since a pair of opposite global shifts is a segment through $S$ with feasible endpoints. The content is elsewhere. In (c) the definition speaks of continuous trajectories and the right-hand side of connected components, so the proof needs local path-connectedness of a finite union of polytopes. In (d) the feasible region is not convex: an order-monotone shift keeps $S$ and $S'$ in a common order polytope, but $S'$ and $S''$ may lie in different ones. The segment through $S$ has to be moved into a single order polytope $\mathcal S_T(O)$ with $O\subseteq O(S)$, and that is Lemma 3.2.9. Proposition 3.2.16 and Theorem 3.2.18 need the passage from $n+2$ linearly independent tight constraints to a spanning tree. They must allow degenerate vertices, where several trees describe the same point, and must represent the nonnegativity constraints $S_i\ge0$ by arcs of the network.

Formalization scope

Activities are Fin (n + 2); start times are real vectors Fin (n + 2) → ℝ with the pointwise order. Durations, capacities and requirements are natural numbers, and time lags integers. The deadline is the arc $\langle n+1,0\rangle$ of weight $-\bar d$, which is always present, as §3.1 prescribes. Resource constraints are imposed for every $t\ge0$, not only for $0\le t\le\bar d$ as (3.1.2) writes; the proofs use the first reading. Extreme points are Mathlib's Set.extremePoints ℝ, maximal points are Maximal for the pointwise order, and components are connectedComponentIn. A local shift carries an explicit continuous map from unitInterval into $\mathcal S$. Strict orders are asymmetric, transitive relations on $V$. A spanning tree is an arc set of size $n+1$ whose underlying simple graph is connected. Its arcs must be arcs of $N$, resp. of $N(O(S))$, with their network weights, so an arbitrary equation system does not count.

The schedule classes are defined through shifts and nothing else. Defining "stable" as "extreme point", or "pseudostable" as "local extreme point", would make the goal and Lemma 3.2.8 tautologies, and such encodings are ruled out. Proposition 3.2.16 carries the book's standing convention (§1.2, p. 8) that every node is reached from $0$ by a walk of nonnegative length. Without it the statement is false.

The definitions duplicate, under this mission's namespace, the model of the book's Chapter 2 missions (order polytopes, shifts, active classes). They are written to be merged with those once published. Contributions on the geometry of finite unions of polytopes, and on spanning-tree bases of difference constraint systems, are reusable beyond this mission.

Selected references

• K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003, §3.1–3.2. https://doi.org/10.1007/978-3-540-24800-2
• K. Neumann, H. Nübel, C. Schwindt, Active and stable project scheduling, Mathematical Methods of Operations Research 52 (2000), 441–465. https://doi.org/10.1007/s001860000092
• M. Bartusch, R. H. Möhring, F. J. Radermacher, Scheduling project networks with resource constraints and time windows, Annals of Operations Research 16 (1988), 199–240. https://doi.org/10.1007/BF02283745

Motivation

Project scheduling assigns start times to the activities of a project subject to constraints between them. The classical critical path method (CPM) of Kelley and Walker (1959) and the program evaluation and review technique (PERT) allow only minimum time lags: activity $j$ may start no earlier than a given time after activity $i$ starts. Practice also needs maximum time lags: activity $j$ must start no later than a given time after $i$. These express deadlines, release dates, time windows and "no wait" couplings. Once maximum time lags are allowed, the project network has cycles and negative arc weights, and even the existence of a schedule is no longer automatic.

This mission is the first of a series on Neumann, Schwindt and Zimmermann, Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003), a standard reference for resource-constrained project scheduling with general temporal constraints. Chapter 1 contains the temporal part of the theory: feasibility, earliest and latest schedules, floats, and the distance order. Every later chapter adds resource constraints on top of this layer.

Timeline. Roy (1964) introduced the Metra Potential Method, which is scheduling on activity-on-node networks with minimum time lags. Neumann (1975, Sect. 6.4) treated time windows through potentials on networks with arbitrary arc weights. Bartusch, Möhring and Radermacher (1988, Annals of Operations Research 16) developed the general theory of scheduling project networks with resource constraints and time windows, including the feasibility criterion stated below. The book collects these results in Chapter 1.

Setting

A project consists of $n\ge 1$ real activities $1,\dots,n$ and two fictitious activities, $0$ (project beginning) and $n+1$ (project completion), so the node set is $V=\{0,1,\dots,n+1\}$. Each activity $i$ has an integer duration $p_i$, with $p_0=p_{n+1}=0$ and $p_i>0$ for real activities.

A minimum time lag $d^{\min}_{ij}$ between two different activities becomes an arc $\langle i,j\rangle$ of weight $\delta_{ij}=d^{\min}_{ij}$. A maximum time lag $d^{\max}_{ij}$ becomes a backward arc $\langle j,i\rangle$ of weight $\delta_{ji}=-d^{\max}_{ij}$. There is at most one arc per ordered pair, keeping the tightest lag. The result is the activity-on-node (AoN) network $N=(V,E,\delta)$, whose integer weights may be positive, negative or zero and which in general contains cycles. The book establishes that for every node $i$ there is a path from $0$ to $i$ of nonnegative length and a path from $i$ to $n+1$ of length at least $p_i$ (p. 8, from Definition 1.1.1 and Remarks 1.1.2). This is the standing assumption of the chapter.

A schedule is a vector $S=(S_0,\dots,S_{n+1})$ of real start times with $S_0=0$ and $S_i\ge 0$. It is time-feasible if it satisfies the temporal constraints

$$S_j-S_i\ \ge\ \delta_{ij}\qquad(\langle i,j\rangle\in E),$$

and $\mathcal S_T$ is the set of time-feasible schedules. A time-feasible schedule minimizing the project duration $S_{n+1}$ is time-optimal.

The length of a path or cycle is the sum of its arc weights. For an integer $L=LS_{n+1}$, which is either a prescribed maximum project duration $\bar d$ or the shortest project duration, the temporal scheduling network $N^+$ adds the backward arc $\langle n+1,0\rangle$ with weight $-L$. The distance $d_{ij}$ is the length of a longest path from $i$ to $j$ in $N^+$, with $d_{ii}=0$. The earliest and latest start times are $ES_i=d_{0i}$ and $LS_i=-d_{i0}$, the earliest completion time is $EC_i=ES_i+p_i$, and the total float is $TF_i=LS_i-ES_i$. The distance order $\prec_D$ is defined for $i\ne j$ by: $i\prec_D j$ if $d_{ij}>0$, or $d_{ij}=0$ and $d_{ji}<0$.

Formalization targets

Goal: Theorem 1.3.3 (p. 10)

$$\mathcal S_T\ne\emptyset\quad\Longleftrightarrow\quad N\ \text{contains no cycle of positive length}.$$

The statement contains no constants. It is the consistency criterion for the temporal constraints and the entry condition for everything else in the book.

Milestones

1. Distances, §1.3, p. 11, Eq. (1.3.3). If $N^+$ has no cycle of positive length, then $d$ satisfies $d_{ij}\ge\delta_{ij}$ on $E^+$ and the triangle inequality $d_{ij}\ge d_{ih}+d_{hj}$, and it is the smallest family that does.
2. Earliest and latest schedules, §1.3, p. 12. Under the same hypothesis and the standing assumption, $ES=(d_{0i})_i$ is time-feasible and lies below every time-feasible schedule. $LS=(-d_{i0})_i$ is time-feasible, satisfies $LS_{n+1}\le L$, and lies above every time-feasible schedule $S$ with $S_{n+1}\le L$.
3. Remark 1.3.2 (p. 10). If $\mathcal S_T\ne\emptyset$, there is an integer-valued time-optimal schedule.
4. Proposition 1.3.8 (p. 15). For a real activity $i$, $[LS_i,EC_i[\ne\emptyset$ if and only if $i$ is critical ($TF_i=0$) or near-critical ($0<TF_i<p_i$). A further item of the mission, not a milestone, states the claim of §1.4, p. 17 (after Definition 1.4.3): if $N^+$ has no cycle of positive length, $\prec_D$ is a strict order on $V$.

Significance

The result itself. Theorem 1.3.3 tells when the temporal constraints of a project can be met at all. Milestones 1 and 2 identify the earliest and latest schedules with longest path lengths, which makes temporal scheduling a pair of longest-path computations (a forward pass from $0$ and a backward pass to $0$). Remark 1.3.2 justifies working in integer time. The distance order and the base time intervals $[LS_i,EC_i[$ are the inputs of the resource-constrained methods in Chapters 2 and 3: priority rules schedule along $\prec_D$, and base time intervals give lower bounds on resource usage.

Formalizing it. These results are classical and proved, but the book does not prove Theorem 1.3.3; it points to Neumann (1975) and Bartusch et al. (1988). To our knowledge they have no machine-checked form in this generality, with arbitrary integer weights, cycles, fictitious start and end nodes, and the backward arc of $N^+$. The CPM results for acyclic event networks with nonnegative durations already on Prove2Me are a special case. The definitions of this mission (project, AoN network, schedule, $N^+$, distances) are intended as the shared substrate for the later missions of the series, which add renewable and cumulative resources.

Difficulty

The necessity direction of the goal is a telescoping sum around a cycle. The sufficiency direction needs a schedule, and the natural candidate $S_i=d_{0i}$ requires three things: longest path lengths must be well defined, they must be finite, and they must satisfy the temporal constraints. With negative weights and cycles, the maximum over walks is unbounded when a positive cycle exists, and a walk-based definition gives nothing. A path-based definition gives a finite maximum but loses the concatenation property, so the triangle inequality becomes a statement about removing nonpositive cycles from walks. $S_0=0$ and $S_i\ge 0$ further depend on the standing assumption: without it, an arc $\langle i,0\rangle$ with positive weight makes $\mathcal S_T$ empty although no cycle is positive. The same combinatorics of walks, paths and cycles is behind milestones 1 and 2 and the distance-order item.

Formalization scope

Nodes are Fin (n + 2): $0$ is the project beginning and Fin.last (n + 1) the project completion. The field one_le_n records $n\ge 1$. Durations are natural numbers with $p_0=p_{n+1}=0$ and $p_i>0$ for real activities. Arc weights are arbitrary integers on a loop-free Finset of ordered pairs, so parallel arcs cannot occur. Start times are real; integrality appears only as Remark 1.3.2.

Walks are functions Fin (m + 1) → Fin (n + 2). A path is an injective walk, and a cycle is a closed walk with at least one arc and distinct nodes apart from the repeated endpoint. Distances are maxima over the finitely many paths, valued in WithBot ℤ with $\bot=-\infty$ for unreachable pairs. No supremum over an unbounded set is taken. $ES_i$ and $LS_i$ convert these to integers with junk value $0$ for $-\infty$, and every milestone that uses them carries the hypotheses under which the distances are finite. The backward arc of $N^+$ has weight $-L$ for an integer parameter $L$. If $N$ already contains an arc $\langle n+1,0\rangle$, the two arcs merge into one carrying the larger weight, as in the book's convention for parallel lags. The standing assumption of p. 8 is a named predicate and a hypothesis of the goal and of milestones 2 and 4.

A trivializing formalization is ruled out: weights are signed integers and cycles are allowed, so the no-positive-cycle condition is not vacuous, and the standing assumption is satisfiable by projects with maximum time lags.

A complete development needs cycle removal from closed walks, the Bellman-type characterization of longest paths without positive cycles, and total unimodularity or a direct integrality argument for Remark 1.3.2. The walk, path and distance layer is reusable for any difference-constraint system. Proofs of milestones and lemmas on walk decomposition are welcome.

Selected references

• K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003. https://doi.org/10.1007/978-3-540-24800-2
• M. Bartusch, R. H. Möhring, F. J. Radermacher, "Scheduling project networks with resource constraints and time windows", Annals of Operations Research 16 (1988), 201–240. https://doi.org/10.1007/BF02283745
• K. Neumann, Operations Research Verfahren, Band III, Hanser, 1975, Sect. 6.4.
• B. Roy, Les problèmes d'ordonnancement: applications et méthodes, Dunod, 1964.
• J. E. Kelley, M. R. Walker, "Critical-path planning and scheduling", Proceedings of the Eastern Joint Computer Conference, 1959, 160–173. https://doi.org/10.1145/1460299.1460318
• R. K. Ahuja, T. L. Magnanti, J. B. Orlin, Network Flows, Prentice Hall, 1993, Sect. 5.4 and 5.6.

Motivation

Interior-point methods are the standard polynomial-time algorithms for linear programming, and the path-following method that practitioners implement (Chapter 18 of Vanderbei's Linear Programming: Foundations and Extensions) comes without a complete convergence proof. Chapter 22 of the same book presents a closely related algorithm for which a complete analysis can be written down: the homogeneous self-dual predictor–corrector method. It combines two ideas. The first is the self-dual embedding of Ye, Todd and Mizuno (1994), which folds a linear program and its dual into one auxiliary problem that always has feasible solutions, so no feasible starting point is needed. The second is the predictor–corrector scheme of Mizuno, Todd and Ye (1993), which alternates an affine-scaling step with a centering step while keeping the iterates in a neighbourhood of the central path, and reduces the duality measure by a factor $1 - 1/(2\sqrt n)$ every two iterations. The result is an $O(\sqrt n\,L)$ iteration bound, the best known for interior-point methods on linear programs.

Setting

Let $A$ be a real $n \times n$ matrix with $n \ge 2$ that is skew symmetric, $A = -A^T$. The homogeneous self-dual problem (22.4) is

$$\text{maximize } 0 \quad \text{subject to } Ax + z = 0,\quad x, z \ge 0.$$

For $x, z \in \mathbb{R}^n$ write $X, Z$ for the diagonal matrices with the entries of $x, z$ on the diagonal and $e$ for the vector of ones. The infeasibility is $\rho(x, z) = Ax + z$ and the noncomplementarity is $\mu(x, z) = \frac1n x^T z$. For a centering parameter $0 \le \delta \le 1$, step directions $(\Delta x, \Delta z)$ solve the linear system

$$A\Delta x + \Delta z = -(1 - \delta)\rho(x, z), \qquad Z\Delta x + X\Delta z = \delta\mu(x, z)e - XZe. \qquad (22.5)\text{–}(22.6)$$

For $0 \le \beta \le 1$ the neighbourhood is

$$\mathcal N(\beta) = \{(x, z) > 0 : \|XZe - \mu(x, z)e\| \le \beta\mu(x, z)\},$$

with $\|\cdot\|$ the Euclidean norm and $(x, z) > 0$ meaning that every component is strictly positive. The algorithm starts at $x^{(0)} = z^{(0)} = e$ and alternates two steps. A predictor step starts from $(x, z) \in \mathcal N(1/4)$, uses $\delta = 0$, and takes the step length (22.10) $\theta = \max\{t : (x + t\Delta x, z + t\Delta z) \in \mathcal N(1/2)\}$. A corrector step starts from $(x, z) \in \mathcal N(1/2)$, uses $\delta = 1$ and $\theta = 1$.

A general linear program (22.1), $\max c^Tx$ subject to $Ax \le b$, $x \ge 0$ with $A$ now $m \times n$, and its dual (22.2), $\min b^Ty$ subject to $A^Ty \ge c$, $y \ge 0$, are embedded in the homogeneous self-dual problem (22.21):

$$-A^Ty + c\phi + z = 0,\quad Ax - b\phi + w = 0,\quad -c^Tx + b^Ty + \psi = 0,\quad x, y, \phi, z, w, \psi \ge 0.$$

A feasible solution of (22.21) is strictly complementary if $x_j + z_j > 0$, $y_i + w_i > 0$ and $\phi + \psi > 0$ for all $i, j$.

Formalization targets

Goal: Theorem 22.5 (p. 330)

In each predictor step, starting from $(x, z) \in \mathcal N(1/4)$ with any solution $(\Delta x, \Delta z)$ of (22.5)–(22.6) at $\delta = 0$,

$$\theta \ge \frac{1}{2\sqrt n}.$$

The formal statement asserts that every $t \in [0, 1/(2\sqrt n)]$ keeps $(x + t\Delta x, z + t\Delta z)$ in $\mathcal N(1/2)$, and that the supremum of the admissible step lengths is at least $1/(2\sqrt n)$.

Milestones

1. Theorem 22.1: (22.4) is feasible, every feasible point is optimal, and $z^Tx = 0$ on the feasible set.
2. Theorem 22.2: $\Delta z^T\Delta x = 0$, $\bar\rho = (1 - \theta + \theta\delta)\rho$, $\bar\mu = (1 - \theta + \theta\delta)\mu$, and $\bar X\bar Ze - \bar\mu e = (1 - \theta)(XZe - \mu e) + \theta^2\Delta X\Delta Ze$.
3. Lemma 22.4: $\|PQe\| \le \frac12\|r\|^2$ for the scaled directions $p = X^{-1/2}Z^{1/2}\Delta x$, $q = X^{1/2}Z^{-1/2}\Delta z$, $r = p + q$; $\|r\|^2 = n\mu$ when $\delta = 0$; $\|r\|^2 \le \beta^2\mu/(1 - \beta)$ when $\delta = 1$ and $(x, z) \in \mathcal N(\beta)$.
4. Theorem 22.3: a predictor step lands in $\mathcal N(1/2)$ with $\bar\mu = (1 - \theta)\mu$; a corrector step lands in $\mathcal N(1/4)$ with $\bar\mu = \mu$.
5. Theorem 22.7: there are constants $c_j > 0$ with $x_j + z_j \ge c_j$ for every iterate $(x, z) \in \mathcal N(\beta)$.
6. Theorem 22.8: a strictly complementary solution of (22.21) with $\bar\phi > 0$ yields optimal solutions $\bar x/\bar\phi$, $\bar y/\bar\phi$ of (22.1)–(22.2); with $\bar\phi = 0$ it certifies that the primal or the dual is infeasible.

Significance

Theorem 22.5 is the quantitative core of the method. Combined with Theorem 22.3 it gives $\mu^{(2k)} \le (1 - \frac{1}{2\sqrt n})^k$ along the iterates, and therefore at most $4L\sqrt n$ iterations to bring $\mu$ below $2^{-L}$ (§22.2.4). Since the infeasibility tracks the noncomplementarity, $\rho^{(k)} = \mu^{(k)}\rho^{(0)}$, both go to zero at that rate. Theorem 22.8 then converts the output into an answer for the original linear program: optimal primal and dual solutions, or a certificate that one of them is infeasible. Theorem 22.7 is the mechanism behind strict complementarity of the limit (Theorem 22.6, stated in the book without proof).

All results are classical and proved in the book. The mission formalizes those proofs. To the best of the curator's knowledge there is no machine-checked convergence analysis of an interior-point method for linear programming in Mathlib or on this platform; the existing platform material on interior-point methods covers a different, short-step path-following method in equality form.

Difficulty

The algebra of Theorem 22.2 is the first obstacle: the orthogonality $\Delta z^T\Delta x = 0$ is not a consequence of (22.5) alone but of skew symmetry combined with both step equations and the definition of $\mu$, and parts (3)–(4) depend on it. The second is that the book's step length (22.10) is a maximum that need not exist, so a statement about $\theta$ must be phrased about the admissible set of step lengths, and membership in $\mathcal N(1/2)$ requires strict positivity of every component along the whole segment, not only the norm bound at its end. The norm bound alone does not control positivity; an argument that ignores this proves membership in a larger set than $\mathcal N(1/2)$. Theorem 22.7 needs a strictly complementary feasible solution of (22.4), whose existence (Theorem 10.6 in the book, the Goldman–Tucker theorem) is itself a substantial result not available in Mathlib.

Formalization scope

Vectors are functions Fin n → ℝ (and Fin m → ℝ), matrices are Matrix (Fin m) (Fin n) ℝ, and all declarations sit in the namespace VanderbeiLP.SelfDual. The committed conventions are:

• The Euclidean norm is defined explicitly (euclidNorm); Mathlib's default norm on Fin n → ℝ is the sup norm and is not used.
• $\mu(x, z) = \frac1n x^Tz$ with $n \ge 2$, the standing assumption of §22.2, carried as a hypothesis by every theorem about (22.4) together with $A^T = -A$.
• Step directions are any solution of (22.5)–(22.6); existence and uniqueness of the solution are neither assumed nor claimed.
• The predictor step length is the supremum of $\{t \in \mathbb{R} : (x + t\Delta x, z + t\Delta z) \in \mathcal N(1/2)\}$. This set contains $0$ and is bounded above by $1$ along a predictor direction, so the supremum is never a default value. Theorem 22.3(1) is stated under the hypothesis that the maximum exists, as (22.10) presumes.
• Theorem 22.7 is stated for points of $\mathcal N(\beta)$ with $0 \le \beta < 1$ satisfying $\rho(x, z) = \mu(x, z)\rho(e, e)$, the relation all iterates satisfy. The constants $c_j$ are quantified before $(x, z)$ and depend only on $A$ and $\beta$. The existence of a strictly complementary solution of (22.4) is not a hypothesis.
• Theorem 22.8 is for arbitrary $m, n$ and data $(A, b, c)$; "optimal" means feasible and attaining the best objective value among feasible points.
• No explicit constants beyond those printed in the statements ($1/4$, $1/2$, $1/(2\sqrt n)$, $\beta^2/(1-\beta)$) occur; the book leaves no constant implicit in the formalized results.

A trivializing formalization is ruled out: the step length is not a default-valued supremum, $\mathcal N(\beta)$ requires strict positivity and uses the Euclidean norm, and the goal is also stated as the segment property its proof establishes.

Theorem 22.6 (convergence of the iterates to a strictly complementary solution) is stated without proof in the book and is not part of this mission; the $4L\sqrt n$ iteration count of §22.2.4 is an unnumbered corollary. Both are welcome as follow-up work, as is a proof of Theorem 10.6 for skew-symmetric systems, which Theorem 22.7 needs.

Selected references

• R. J. Vanderbei, Linear Programming: Foundations and Extensions, 4th ed., International Series in Operations Research & Management Science 196, Springer, 2014, Chapter 22. https://doi.org/10.1007/978-1-4614-7630-6
• S. Mizuno, M. J. Todd, Y. Ye, On adaptive-step primal–dual interior-point algorithms for linear programming, Mathematics of Operations Research 18(4), 964–981, 1993. https://doi.org/10.1287/moor.18.4.964
• 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), 53–67, 1994. https://doi.org/10.1287/moor.19.1.53
• 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. https://doi.org/10.1515/9781400881987-005

Motivation

Interior-point methods are, together with the simplex method, the standard algorithms for linear programming, and the primal–dual path-following method is the form in which they are implemented in most solvers. Unlike the simplex method, it is a one-phase method: it can start from any point whose primal and dual variables are strictly positive, feasible or not, and drives infeasibility and complementarity to zero simultaneously. The question every user of such a method eventually asks is how fast these three measures of non-optimality decrease.

Chapter 18 of R. J. Vanderbei, Linear Programming: Foundations and Extensions (4th ed., Springer 2014, DOI 10.1007/978-1-4614-7630-6) defines the method from scratch (Fig. 18.1, p. 273) and proves a rate statement, Theorem 18.1 (pp. 277–279): as long as the step lengths stay bounded below and the iterates stay bounded, the primal and dual infeasibilities decay geometrically, and so does the complementarity, at a slower rate. This mission formalizes that theorem and the one-step identities and estimates it is built from. It is the fifth mission of a series on the book; the missions are independent of each other.

Setting

Let $A$ be a real $m \times n$ matrix, $b \in \mathbb{R}^m$, $c \in \mathbb{R}^n$. The primal problem is to maximize $c^Tx$ subject to $Ax + w = b$, $x, w \ge 0$; the dual is to minimize $b^Ty$ subject to $A^Ty - z = c$, $y, z \ge 0$. A primal–dual point is a quadruple $(x, w, y, z)$ with $x, z \in \mathbb{R}^n$, $w, y \in \mathbb{R}^m$; it is strictly positive, $(x, w, y, z) > 0$, if every component is. Write $X, W, Y, Z$ for the diagonal matrices of $x, w, y, z$ and $e$ for the all-ones vector. The norms are $\|v\|_1 = \sum_j |v_j|$ and $\|v\|_\infty = \max_j |v_j|$.

At a point $(x, w, y, z)$ the three measures of progress are the primal infeasibility $\rho = b - Ax - w$, the dual infeasibility $\sigma = c - A^Ty + z$, and the complementarity $\gamma = z^Tx + y^Tw$. Fix parameters $0 < \delta < 1$ and $0 < r < 1$. One iteration of the method, from a strictly positive point, sets $\mu = \delta\gamma/(n+m)$, takes any solution $(\Delta x, \Delta w, \Delta y, \Delta z)$ of the Newton system

$$A\Delta x + \Delta w = \rho, \quad A^T\Delta y - \Delta z = \sigma, \quad Z\Delta x + X\Delta z = \mu e - XZe, \quad W\Delta y + Y\Delta w = \mu e - YWe,$$

computes the step length

$$\theta = r\left(\max_{i,j}\left\{\left|\tfrac{\Delta x_j}{x_j}\right|, \left|\tfrac{\Delta w_i}{w_i}\right|, \left|\tfrac{\Delta y_i}{y_i}\right|, \left|\tfrac{\Delta z_j}{z_j}\right|\right\}\right)^{-1} \wedge 1 \qquad (18.7)$$

(with $\theta = 1$ when all ratios vanish), and moves to $(x + \theta\Delta x, w + \theta\Delta w, y + \theta\Delta y, z + \theta\Delta z)$. This is Fig. 18.1 with the shorter step (18.7) the book adopts for its analysis. Along a sequence of iterates, superscripts $^{(k)}$ denote the quantities at the $k$-th iterate, and $\theta^{(k)}$ is the step length computed there.

Formalization targets

Goal: Theorem 18.1 with the explicit constant

If $t > 0$, $M$ is real, and for all $k \le K$ one has $\theta^{(k)} \ge t$, $\|x^{(k)}\|_\infty \le M$, $\|y^{(k)}\|_\infty \le M$, then for all $k \le K$, with $\tilde t = t(1-\delta)$,

$$\|\rho^{(k)}\|_1 \le (1-t)^k\|\rho^{(0)}\|_1, \qquad \|\sigma^{(k)}\|_1 \le (1-t)^k\|\sigma^{(0)}\|_1, \qquad \gamma^{(k)} \le (1-\tilde t)^k \left(\gamma^{(0)} + \frac{M(\|\rho^{(0)}\|_1 + \|\sigma^{(0)}\|_1)}{\delta t}\right).$$

Milestones

The one-step identities for the infeasibilities, $\tilde\rho = (1-\theta)\rho$ (18.8) and $\tilde\sigma = (1-\theta)\sigma$ (18.9); the one-step complementarity estimate

$$\tilde\gamma \le (1 - (1-\delta)\theta)\gamma + M\|\rho\|_1 + M\|\sigma\|_1 \qquad (18.10)$$

under $\|x\|_\infty, \|y\|_\infty \le M$; and the recursion $\gamma^{(k)} \le (1-\tilde t)\gamma^{(k-1)} + M(1-t)^{k-1}(\|\rho^{(0)}\|_1 + \|\sigma^{(0)}\|_1)$ (18.11). Two unnumbered statements complete the picture: every iteration has $0 < \theta \le 1$ and keeps the point strictly positive, and at any strictly positive point the duality gap satisfies $|b^Ty - c^Tx| \le \gamma + \|\sigma\|_1\|x\|_\infty + \|\rho\|_1\|y\|_\infty$ (§18.5.3).

Significance

Theorem 18.1 separates the convergence question for the path-following method into two parts: a rate statement that holds whenever steps stay long and iterates stay bounded, and the remaining question of when those two conditions hold. It also explains an effect seen in practice: the infeasibilities fall by the factor $1 - t$ per iteration while the complementarity, and hence (by the duality-gap estimate) the gap $b^Ty - c^Tx$, falls only by $1 - \tilde t$. The book stresses that the result is partial, because it does not show that the step lengths remain bounded away from zero; that requires modifications of the method and of the starting point that the book does not carry out.

All statements here are proved in the book. The mission's contribution is a machine-checked version, with the constant of the complementarity bound made explicit. Neither Mathlib nor the platform contains a formal proof of this theorem or a formalization of the infeasible-start primal–dual iteration it concerns; the platform's existing path-following result concerns a different, feasible-start short-step method in equality form.

Difficulty

The infeasibility identities are linear and follow from the first two Newton equations. The complementarity is where the Newton system linearizes a bilinear equation, so the new complementarity contains a second-order term $\theta^2(\Delta y^T\rho - \sigma^T\Delta x)$ that has no sign. Bounding it requires relating the size of the step $\theta\Delta$ to the size of the current iterate through the specific form of the step-length rule (18.7); the rule (18.6) of Fig. 18.1, with signed ratios, does not give such a bound. The multi-step estimate then couples two geometric sequences with different rates, and keeping the constant independent of the horizon $K$ is what makes the statement non-trivial.

Formalization scope

Vectors are Fin n → ℝ and Fin m → ℝ, $A$ is a Matrix (Fin m) (Fin n) ℝ, and points and step directions are a structure PDPoint m n with fields x w y z. The sup-norm is ⨆ j, |v j| (the maximum; 0 for an empty vector). The step length is written with the explicit case $\theta = 1$ when all ratios vanish, since Lean's r / 0 = 0 would otherwise give $\theta = 0$. An iteration is a relation between the current point, a step direction and the next point: the current point is strictly positive, the direction is some solution of the Newton system (uniqueness, which the book asserts under a full-rank assumption, is not assumed), and the next point is current $+\ \theta \cdot$ direction. The hypotheses $0 < \delta < 1$, $0 < r < 1$ (pp. 272–273) are stated in every theorem; $M$ is an arbitrary real number and $K$ a natural number. As in the book, the hypotheses of Theorem 18.1 range over $k \le K$, so the iteration from index $K$ is part of the data.

Explicit constants. The book's Theorem 18.1 asserts only "there exists a constant $\bar M < \infty$". Because $K$ is fixed, that existential is satisfied trivially by $\max_{k \le K}\gamma^{(k)}/(1-\tilde t)^k$, and a statement with $\exists \bar M$ would be empty. The goal therefore uses the constant the book's proof establishes (p. 279, last display): $\bar M = \gamma^{(0)} + M(\|\rho^{(0)}\|_1 + \|\sigma^{(0)}\|_1)/(\delta t)$. Eq. (18.11) is stated with the book's $\tilde M = M(\|\rho^{(0)}\|_1 + \|\sigma^{(0)}\|_1)$ written out.

The formalization needs only finite sums, dot products and matrix–vector products from Mathlib; the definitions of the iteration are reusable for other analyses of the same method (Chapters 19–22 of the book). Contributions are welcome for each milestone separately.

Selected references

• R. J. Vanderbei, Linear Programming: Foundations and Extensions, 4th ed., International Series in Operations Research & Management Science 196, Springer, 2014, Chapter 18, pp. 269–283. https://doi.org/10.1007/978-1-4614-7630-6
• S. J. Wright, Primal-Dual Interior-Point Methods, SIAM, 1997. https://doi.org/10.1137/1.9781611971453

Motivation

Interior-point methods solve linear programs by moving through the interior of the feasible region instead of along its edges, as the simplex method does. The methods used in practice are path-following methods: they track a curve, the central path, that runs through the interior of the feasible region and ends at an optimal solution. Before any such method can be analysed, the curve has to exist. This mission formalizes Chapter 17 of R. J. Vanderbei, Linear Programming: Foundations and Extensions (4th ed., Springer 2014), which defines the central path through the logarithmic barrier problem and proves that it exists exactly when the primal and the dual problem both have strictly positive feasible points.

The chapter's results have a short history. Barrier methods for nonlinear programming go back to Fiacco and McCormick (1968). Interest in interior-point methods for linear programming began with Karmarkar (1984), whose projective algorithm does not mention a central path; the connection between Karmarkar's method and the primal–dual central path was found by Megiddo (1989), with central points traced back to Huard (1967) and an extended study of the path by Bayer and Lagarias (1989). The chapter is the textbook entry point to this line of work and the foundation for the path-following algorithm of Chapter 18.

Setting

Let $A$ be a real $m \times n$ matrix, $b \in \mathbb{R}^m$ and $c \in \mathbb{R}^n$. The primal linear program is to maximize $c^T x$ subject to $Ax \le b$, $x \ge 0$; its dual is to minimize $b^T y$ subject to $A^T y \ge c$, $y \ge 0$. With slack variables $w \in \mathbb{R}^m$ and $z \in \mathbb{R}^n$ they read (17.1)

$$Ax + w = b,\ x, w \ge 0 \qquad\text{and}\qquad A^T y - z = c,\ y, z \ge 0.$$

For a vector $\xi$, $\xi > 0$ means that every component is strictly positive. The primal feasible region has nonempty interior when some $(\bar x, \bar w)$ satisfies $A\bar x + \bar w = b$ with $\bar x > 0$, $\bar w > 0$; the dual feasible region has nonempty interior when some $(\bar y, \bar z)$ satisfies $A^T \bar y - \bar z = c$ with $\bar y > 0$, $\bar z > 0$.

For a parameter $\mu > 0$, the barrier function (17.7) is

$$f(x, w) = c^T x + \mu \sum_{j=1}^n \log x_j + \mu \sum_{i=1}^m \log w_i ,$$

and the barrier problem (17.2) is to maximize $f(x, w)$ subject to $Ax + w = b$, over the domain $x > 0$, $w > 0$ where the logarithms are finite. A solution of the barrier problem is a point of that domain at which $f$ attains its maximum over the domain.

Writing $X, Z, Y, W$ for the diagonal matrices carrying $x, z, y, w$ and $e$ for the all-ones vector, the primal–dual central-path system (17.6) is

$$Ax + w = b, \qquad A^T y - z = c, \qquad XZe = \mu e, \qquad YWe = \mu e,$$

with $x, w, y, z > 0$. The last two equations say $x_j z_j = \mu$ and $y_i w_i = \mu$ for all $j$ and $i$. The set of its solutions $(x_\mu, w_\mu, y_\mu, z_\mu)$, $\mu > 0$, is the primal–dual central path.

The chapter also uses one fact from nonlinear programming: for the problem "maximize $f(x)$ subject to $g_i(x) = 0$, $i = 1, \dots, m$", a critical point is a feasible $x^*$ with $\nabla f(x^*) = \sum_i y_i \nabla g_i(x^*)$ for some Lagrange multipliers $y_i$ (17.3), and $H_f(x^*)$ is the Hessian of $f$ at $x^*$.

Formalization targets

Goal: Theorem 17.2 (p. 265)

For each fixed $\mu > 0$,

$$\exists\, (x, w) \text{ solving the barrier problem} \iff \big(\exists\, \bar x, \bar w > 0 : A\bar x + \bar w = b\big) \wedge \big(\exists\, \bar y, \bar z > 0 : A^T\bar y - \bar z = c\big).$$

Both directions are part of the goal. The statement fixes no constants and no rate; it asserts only when the barrier problem is solvable.

Milestones

1. Theorem 17.1 (p. 261), second-order sufficiency under linear constraints: if the constraints are linear, a critical point $x^*$ with $\xi^T H_f(x^*)\xi < 0$ for every $\xi \ne 0$ satisfying $\xi^T \nabla g_i(x^*) = 0$ for all $i$ is a local maximum on the feasible set.
2. Exercise 10.7 (p. 150): if the primal is feasible and its feasible set $\{x : Ax \le b,\ x \ge 0\}$ is bounded, then there are $y > 0$, $z > 0$ with $A^T y - z = c$.
3. Corollary 17.3 (p. 266): if the primal feasible set (or the dual feasible set) has nonempty interior and is bounded, then for each $\mu > 0$ the system (17.6) has exactly one solution with $x, w, y, z > 0$.

The corollary is stronger than the goal in one direction (it adds uniqueness and the dual variables) and weaker in another (it assumes boundedness).

Significance

The result itself. Theorem 17.2 gives an exact criterion for the barrier problem to be solvable for a fixed $\mu$, and Corollary 17.3 turns it into the statement that the central path is a well-defined curve $\mu \mapsto (x_\mu, w_\mu, y_\mu, z_\mu)$ for all $\mu > 0$. Every path-following method, including the one analysed in Chapter 18 of the same book, targets points on this curve; without existence and uniqueness the "target" of an iteration is undefined. The system (17.6) is also the starting point of the primal–dual Newton step.

Formalizing it. These results are classical and proved in the book; none is formalized in the $Ax \le b$, $x \ge 0$ form used here. The platform has the converse fact in the standard form $Ax = b$, $x \ge 0$ (a solution of the central-path conditions minimizes the barrier, Introduction to Linear Optimization), but not existence. A formal proof of Theorem 17.2 and Corollary 17.3 produces a reusable existence theorem for the central path that downstream missions on path-following and self-dual methods can import.

Difficulty

The "if" direction of Theorem 17.2 is an existence claim on a set that is neither closed nor bounded: the domain $x > 0$, $w > 0$ is open, and the feasible region itself may be unbounded, so the obvious appeal to "a continuous function on a compact set attains its maximum" does not apply directly. The example "maximize $0$ subject to $x \ge 0$" (p. 264), whose barrier $\mu \log x$ has no maximum, shows that the dual hypothesis cannot be dropped. The "only if" direction, which the book calls trivial and does not prove, needs first-order conditions at a maximizer over a relatively open set.

Theorem 17.1 needs a second-order Taylor expansion with a remainder that is $o(\|\xi\|^2)$ uniformly along the constraint subspace, not along individual lines. Exercise 10.7 is a theorem of the alternative and is not a consequence of weak duality alone. Uniqueness in Corollary 17.3 requires the positivity of the solution: the equations $x_j z_j = \mu$, $y_i w_i = \mu$ admit sign-flipped solutions.

Formalization scope

Vectors are Fin n → ℝ and Fin m → ℝ; $A$ is a Matrix (Fin m) (Fin n) ℝ. The book's primal–dual pair in $Ax \le b$, $x \ge 0$ form with slacks is used throughout; there are no explicit constants in this chapter.

Conventions committed to:

• "Nonempty interior" means a feasible point with every component strictly positive, as the proof of Theorem 17.2 says. The topological interior of $\{(x, w) : Ax + w = b,\ x, w \ge 0\}$ in $\mathbb{R}^{n+m}$ is empty whenever $m \ge 1$; reading the theorem that way would make its right-hand side always false for $m \ge 1$, and that reading is ruled out.
• The barrier problem is posed over $x > 0$, $w > 0$ explicitly; Real.log returns $0$ at nonpositive arguments and is never evaluated there.
• Solutions of (17.6) are required to be strictly positive, as in Exercise 17.3 (p. 267).
• "Bounded" is Bornology.IsBounded of the feasible set in $\mathbb{R}^n$ (resp. $\mathbb{R}^m$).
• In Theorem 17.1 the constraints are $Gx = \beta$; $f$ is differentiable near $x^*$ with derivative differentiable at $x^*$, and $\xi^T H_f(x^*) \xi$ is the second Fréchet derivative applied to $(\xi, \xi)$. The local maximum is relative to the feasible set.

Infrastructure a complete development needs: attainment of maxima on compact sets (IsCompact.exists_isMaxOn in Mathlib), first-order conditions on relatively open sets, a theorem of the alternative for Exercise 10.7, and concavity facts about the logarithm. A second-order sufficient condition under affine constraints is not in Mathlib and is reusable beyond linear programming. Proofs of any milestone, including the "only if" half of the goal separately, are welcome contributions.

Selected references

• R. J. Vanderbei, Linear Programming: Foundations and Extensions, 4th ed., International Series in Operations Research & Management Science 196, Springer, 2014, Chapter 17 and Exercise 10.7. https://doi.org/10.1007/978-1-4614-7630-6
• A. V. Fiacco and G. P. McCormick, Nonlinear Programming: Sequential Unconstrained Minimization Techniques, Wiley, 1968. https://doi.org/10.1137/1.9781611971316
• N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica 4 (1984), 373–395. https://doi.org/10.1007/BF02579150
• N. Megiddo, Pathways to the optimal set in linear programming, in Progress in Mathematical Programming, Springer, 1989, 131–158. https://doi.org/10.1007/978-1-4613-9617-8_8
• D. A. Bayer and J. C. Lagarias, The nonlinear geometry of linear programming I, II, Transactions of the AMS 314 (1989), 499–526 and 527–581. https://doi.org/10.1090/S0002-9947-1989-1005525-6

Motivation

Minimum-cost network flow problems are the largest special class of linear programs met in practice: transportation, distribution, assignment, communication and electric networks, facility location and financial planning all reduce to moving material along the arcs of a directed network from supply nodes to demand nodes at least cost. Chapter 14 of R. J. Vanderbei's Linear Programming: Foundations and Extensions (4th ed., Springer 2014, DOI 10.1007/978-1-4614-7630-6) develops the network simplex method, and closes with two structural facts that explain why this class is special: simplex bases are spanning trees of the network, and a network problem with integer supplies has integer basic solutions. Vanderbei then uses integrality to prove a classical theorem of combinatorics, König's theorem on regular bipartite graphs. Chapter 15, §5 treats the maximum-flow problem on the same objects and proves the Max-Flow Min-Cut Theorem.

The combinatorial results are older than linear programming. D. König proved in 1916 that every regular bipartite graph has a perfect matching (Math. Ann. 77). The Max-Flow Min-Cut Theorem is due to Ford and Fulkerson (1956, Canad. J. Math. 8) and, independently, Elias, Feinstein and Shannon (1956). The integrality of network bases is the total unimodularity of incidence matrices, known since the 1950s (Hoffman and Kruskal, 1956).

Setting

A network $(N,A)$ has a finite set $N$ of $m$ nodes and a set of directed arcs $A\subseteq\{(i,j): i,j\in N,\ i\ne j\}$. Node $i$ carries a supply $b_i$ (negative values are demands) with $\sum_i b_i=0$, and arc $(i,j)$ carries a cost $c_{ij}$. The flow $x_{ij}$ on arc $(i,j)$ is the decision variable. The node–arc incidence matrix $A$ has in the column of $(i,j)$ an entry $+1$ in row $j$, $-1$ in row $i$, and $0$ elsewhere. The network flow problem (14.1) is

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

A flow satisfying $Ax=-b$ is balanced; a balanced flow with $x\ge0$ is feasible. Paths ignore arc directions; the network is connected if every two nodes are joined by a path, which is assumed throughout Chapter 14. A spanning tree is a set of arcs that, on all of $N$ and without directions, is connected and has no cycle. Fixing a root node $r$ and deleting its row gives the matrix $\tilde A$. A set $T$ of arcs is a basis if its columns form an invertible square submatrix of $\tilde A$, and a basic feasible solution is a feasible flow vanishing off some basis.

For maximum flow, a source $s$, a sink $t$ and finite upper bounds $u_{ij}$ are given; all $b_i=0$ and an extra arc $(t,s)$ of infinite capacity is added. A feasible flow satisfies $0\le x_{ij}\le u_{ij}$, $x_{ts}\ge0$ and flow balance. A cut is a node set $C$ with $s\in C$, $t\notin C$, and its capacity is $\kappa(C)=\sum_{(i,j)\in A,\ i\in C,\ j\notin C}u_{ij}$.

Formalization targets

Goal: König's Theorem (Theorem 14.3, p. 216)

If $n$ girls and $n$ boys are such that every girl knows exactly $k\ge1$ boys and every boy knows exactly $k$ girls (knowing being symmetric), then there is a bijection $\sigma$ from girls to boys with

$$\text{girl } i \text{ knows boy } \sigma(i)\qquad\text{for all } i .$$

Milestones

1. Theorem 14.1 (p. 205): for a connected network, a set $T$ of arcs indexes a basis of $\tilde A$ if and only if $T$ is a spanning tree.
2. Theorem 14.2, Integrality Theorem (p. 216): with integer supplies, every basic feasible solution is integral,

$$x_{ij}\in\mathbb Z\qquad\text{for all }(i,j)\in A .$$

3. Eq. (15.8) (p. 234): $x_{ts}\le\kappa(C)$ for every feasible flow and every cut.
4. Theorem 15.1, Max-Flow Min-Cut (p. 234):

$$\max\{x_{ts}\}=\min_C \kappa(C),$$

both extrema attained.

The goal is independent of the network definitions in its statement; the milestones are the book's route to it (14.1, 14.2) and the chapter's other duality theorem on the same objects (15.8, 15.1).

Significance

König's theorem is the base case of matching theory: it gives perfect matchings in regular bipartite graphs, hence edge colourings of bipartite graphs with $\Delta$ colours, and via Birkhoff–von Neumann-type arguments the decomposition of doubly stochastic matrices. The Integrality Theorem is the reason assignment, transportation and shortest-path problems can be solved as linear programs without an integrality constraint. Theorem 14.1 is the correspondence the network simplex method is built on. Max-Flow Min-Cut is the prototype of combinatorial min–max theorems.

All four theorems are classical and proved. This mission adds machine-checked versions in the book's own formulation: the incidence matrix with Vanderbei's sign convention $Ax=-b$, bases as square submatrices of $\tilde A$ with a chosen root, and maximum flow as a circulation through an added return arc. The platform already has network integrality, a tree-solution characterisation and max-flow min-cut in the Bertsimas–Tsitsiklis formulation and a Keller–Trotter max-flow statement; none is stated in this form, and Mathlib has Hall's marriage theorem but no regular-bipartite corollary.

Difficulty

The combinatorial content is small; the difficulty is in the passage between matrices and graphs. Theorem 14.1 needs both directions: the book shows that a spanning tree gives a triangularisable, hence invertible, submatrix and leaves the converse (independent columns form a spanning tree) as an exercise, which requires showing that any cycle, including a pair of antiparallel arcs, yields a linearly dependent set of columns and that $m-1$ acyclic arcs span. The book's proof of König's theorem applies the Integrality Theorem to the girl–boy network, which need not be connected, while Chapter 14 assumes connectedness throughout: the statement of 14.2 does not apply to it verbatim. The step "a feasible problem has a basic optimal solution" is also used and is not stated in the chapter.

Formalization scope

• Nodes are a Fintype with decidable equality; arcs are a Finset (N × N), so parallel arcs are excluded as in the book, and IsNetwork excludes loops. Flows are real functions on ordered pairs; only their values on arcs matter.
• "Connected" is preconnectedness of the undirected simple graph of the arcs; a spanning tree is an arc set whose undirected graph is a tree and in which no two arcs join the same pair of nodes.
• A basis is $m-1$ linearly independent columns of the $(m-1)$-row matrix $\tilde A$, the same as an invertible square submatrix. The root $r$ is arbitrary, as in the book ("say, the last one").
• Integer data means integer supplies; costs do not enter Theorem 14.2, since a basic optimal solution is a basic feasible solution.
• In König's theorem both sides are Fin n, knowing is one relation between girls and boys, and $k\ge1$ is a hypothesis: the book's proof divides by $k$, and for $k=0<n$ the claim is false. No connectedness is assumed.
• For maximum flow, the return arc $(t,s)$ is a separate variable; $s\ne t$ and $u_{ij}\ge0$ are hypotheses that the book leaves implicit. Maximum and minimum are stated with attainment.
• No statement involves a constant the book leaves implicit.

A formalization of the goal as a matching of size $n$ in some larger graph, or with the degree conditions on one side only, would be a different theorem; the conclusion is a bijection between exactly the $n$ girls and the $n$ boys using only acquainted pairs.

Useful infrastructure, reusable beyond this mission: the incidence matrix and its total unimodularity, the undirected graph of an arc set. Proofs of König's theorem through Hall's theorem (Mathlib Finset.all_card_le_biUnion_card_iff_exists_injective) are welcome alongside the book's route.

Selected references

• R. J. Vanderbei, Linear Programming: Foundations and Extensions, 4th ed., Springer, 2014. DOI 10.1007/978-1-4614-7630-6
• D. König, Über Graphen und ihre Anwendung auf Determinantentheorie und Mengenlehre, Math. Ann. 77 (1916), 453–465. DOI 10.1007/BF01456961
• L. R. Ford and D. R. Fulkerson, Maximal flow through a network, Canad. J. Math. 8 (1956), 399–404. DOI 10.4153/CJM-1956-045-5
• A. J. Hoffman and J. B. Kruskal, Integral boundary points of convex polyhedra, in Linear Inequalities and Related Systems, Ann. of Math. Studies 38, Princeton University Press, 1956, 223–246.

Motivation

A stochastic linear program is a linear optimization problem whose coefficients depend on a random parameter. Even when the model is feasible and bounded almost surely, its optimal value is itself a random quantity. Knowing only its expectation can hide the probability of unusually favorable or unfavorable outcomes; its full distribution supports threshold probabilities, quantiles, and later risk-sensitive decisions. Chapter II of Peter Kall's Stochastic Linear Programming develops a finite-dimensional method for determining that distribution when the constraint matrix, right-hand side, and objective coefficients depend affinely on the same random vector. Theorem 8, printed p. 29 / PDF35, is the chapter's general distribution formula. This mission asks for that known theorem to be proved in Lean from its reviewed statement.

Setting

Fix a finite parameter vector $t\in\mathbb R^r$. An affine random linear program supplies a matrix $A(t)\in\mathbb R^{m\times n}$, a right-hand side $b(t)\in\mathbb R^m$, and costs $c(t)\in\mathbb R^n$, each affine in $t$. Its optimal value is the extended-real infimum

$$\gamma(t)=\inf\{c(t)^\top x:A(t)x=b(t),\ x\ge 0\}.$$

The parameter has a probability law $\mu$, supported almost surely on a measurable set $T$, with a nonnegative extended-real density $f$ relative to Lebesgue measure. The extended-real value records infeasibility as $+\infty$ and unboundedness as $-\infty$; the target distribution deliberately restricts to the finite-value event $-\infty<\gamma(t)\le\xi$.

A candidate basis is an increasing selection $\sigma:\operatorname{Fin}(m)\to\operatorname{Fin}(n)$. Its basis matrix $B_\sigma(t)$ consists of the selected columns of $A(t)$. Kall enumerates exactly those candidate bases whose determinant is nonzero at some point of $T$. For each one, its raw optimality region consists of the parameters for which $B_\sigma(t)^{-1}b(t)\ge0$ and the reduced costs $c(t)^\top-c_B(t)^\top B_\sigma(t)^{-1}A(t)$ are nonnegative. Matrix inversion is totalized to zero at singular matrices, matching the source convention. The ordered basis regions remove every earlier raw region, so overlapping optimal bases are assigned to the first enumerated basis. On a basis region the associated value is

$$\gamma_\sigma(t)=c_B(t)^\top B_\sigma(t)^{-1}b(t).$$

Assumption A1 is explicit in Lean: the density and support clauses above, both almost-sure feasibility/boundedness implications from Theorem 4, and the existence of one full-row-rank column minor at a point of $T$. The basis enumeration is injective and exhaustive for the almost nonsingular increasing selections.

Formalization targets

Theorem 8: distribution by basis regions

For the ordered regions $B_i$, the theorem states

$$\mu\!\left(\bigcup_i B_i\right)=\sum_i\mu(B_i)=1.$$

For every real threshold $\xi$, it further identifies the finite optimal-value distribution by

$$\mu\{t\in T:-\infty<\gamma(t)\le\xi\} =\sum_i\int_{\{t\in B_i:\gamma_i(t)\le\xi\}} f(t)\,dt.$$

The normalization and distribution identity are the two clauses of the same source theorem and remain one goal. Determinant facts, special stochastic models, and examples elsewhere in the chapter are context rather than additional mission targets.

Significance

The result turns the distribution of a random optimization value into a finite sum of ordinary density integrals over explicitly described parameter regions. It connects parametric linear programming geometry with probabilistic questions about the optimum and provides the chapter's foundation for studying particular stochastic models and derived distributional quantities. Without the coverage and normalization clauses, the integral expression could omit positive-probability parameter regimes; without the finite-value event, extended-real exceptional outcomes would be conflated with a real-valued distribution function.

The theorem is established in the 1976 source, but the staged Lean declaration contains a proof placeholder. Completing it would produce a machine-checked account of the basis-region decomposition under the source's full hypotheses. The reusable content includes the affine model, basis matrix, raw-region inequalities, ordered disjointification, basis value, and the referenced extended-real linear-program value.

Difficulty

The natural pointwise argument chooses an optimal basis and substitutes its basic solution. That alone does not prove a measurable probability decomposition: several bases may be optimal at the same parameter, bases may become singular on exceptional sets, and the optimal value may be infinite. The ordered subtraction of earlier regions resolves overlap only after one proves exhaustive coverage under A1. The final equality must also connect the extended-real infimum to the real basis value on each region and justify the density integrals on the threshold sets. Treating the raw regions as automatically disjoint or silently assuming every parameter has a unique nonsingular optimizer would bypass the central issues.

Formalization scope

All dimensions and basis lists are finite. The law is a probability measure on $\operatorname{Fin}(r)\to\mathbb R$, represented as volume.withDensity f; $T$ is measurable and carries the law almost surely. The density is ENNReal-valued and the displayed integrals are nonnegative lintegrals. No integrability or finite-moment hypothesis is imposed on the optimal value. LPValue is an existing referenced platform definition using EReal.sInf; the book-local declarations remain in the shared Kall1976 namespace. Mathlib's nonsingular inverse supplies the source's zero value at singular matrices.

The formal target must retain both almost-sure implications, the one-point full-rank condition, increasing and exhaustive basis enumeration, region ordering, probability-one normalization, the strict lower bound by $-\infty$, and the weak upper threshold $\le\xi$. Removing any of these clauses would change the reviewed theorem rather than simplify its proof. Contributions may develop measurable-region, finite-basis coverage, LP optimality, and density-integration lemmas, provided they preserve these conventions.

Selected references

• Peter Kall, Stochastic Linear Programming, Springer, 1976, Chapter II §1: Theorem 4 printed p. 25 / PDF31; model (5) printed p. 27 / PDF33; Assumption A1 printed p. 28 / PDF34; Theorem 8 printed p. 29 / PDF35. DOI.