Linear Optimization

Motivation

An integer linear program $\max\{wx : Ax \le b,\ x \text{ integral}\}$ is usually attacked through its linear programming relaxation $\max\{wx : Ax \le b\}$, which drops the integrality constraint. Two questions follow at once. How far can an optimal solution of the relaxation be from an optimal integer solution? And how many rounds of rounding-based cutting planes are needed before the relaxation describes the integer points exactly? Branch-and-bound, cutting-plane methods and the parametric analysis of integer programs all depend on the answers.

W. Cook, A.M.H. Gerards, A. Schrijver and É. Tardos, Sensitivity theorems in integer linear programming (Math. Programming 34 (1986) 251–264), answer both in terms of the number of variables $n$ and the largest subdeterminant $\Delta(A)$ of the constraint matrix, independently of the right-hand side.

Timeline.

• 1958–1963: Gomory introduces integer rounding cuts. In 1973 Chvátal (Discrete Math. 4) shows that finitely many rounds reach the integer hull of a bounded polyhedron.
• 1977–1979: Blair and Jeroslow prove that for a fixed matrix $A$ the distance between LP and IP optima, and the gap between their values, are bounded by constants depending on $A$.
• 1980: Schrijver (Ann. Discrete Math. 9) proves that the Chvátal closure of a rational polyhedron is a polyhedron, and that every rational polyhedron, bounded or not, reaches its integer hull after finitely many rounds.
• 1986: Cook, Gerards, Schrijver and Tardos prove the explicit bounds of this mission, $n\Delta(A)$ for proximity, and show that every integral matrix has finite Chvátal rank.
• Later work, for example Eisenbrand and Weismantel (2018), replaces the $\ell_\infty$ proximity bound by $\ell_1$ bounds for programs in standard form.

Setting

All matrices, vectors and polyhedra are rational. Let $A$ be an integral $m\times n$ matrix. A square submatrix of order $k$, where $1\le k\le\min(m,n)$, keeps $k$ rows and $k$ columns of $A$. The quantity $\Delta(A)$ is the largest $|\det B|$ over all such submatrices $B$. So $\Delta(0)=0$, and $\Delta(A)\ge 1$ whenever $A\ne 0$. Norms are $\|x\|_\infty=\max_i|x_i|$ and $\|x\|_1=\sum_i|x_i|$.

For $b\in\mathbb{Q}^m$ write $P=\{x\in\mathbb{Q}^n : Ax\le b\}$. An optimal solution of $\max\{wx : Ax\le b\}$ is a point of $P$ maximizing $wx$. For $\max\{wx : Ax\le b,\ x\text{ integral}\}$ it is an integral point of $P$ maximizing $wx$ among the integral points of $P$. A rational polyhedron is a set $\{x : Dx\le d\}$ with $D$, $d$ rational. The integer hull $P_I$ is the convex hull of the integral points of $P$.

If $ay\le\beta$ for all $y\in P$, with $a$ integral and $\beta$ rational, then every integral point of $P$ satisfies the Chvátal cut $ax\le\lfloor\beta\rfloor$. The Chvátal closure $P'$ is the set of points satisfying all Chvátal cuts. Set $P^{(0)}=P$ and $P^{(i)}=(P^{(i-1)})'$. Then $P_I\subseteq P^{(i)}$ for all $i$. The Chvátal rank of $P$ is the least $t$ with $P^{(t)}=P_I$. The Chvátal rank of the matrix $A$ is the supremum of the Chvátal ranks of $\{x : Ax\le b\}$ over all integral vectors $b$.

Formalization targets

Goal: Theorem 10 (p. 260)

$$\sup_{b\in\mathbb{Z}^m}\ \operatorname{rank}\{x : Ax\le b\}\ \le\ 2^{n^3+1}\,n^{5n}\,\Delta(A)^{n+1}.$$

In particular, every integral matrix has finite Chvátal rank, and the bound does not depend on $m$ or on $b$.

Milestones, in attack order

1. Theorem 1 (p. 252). Suppose $Ax\le b$ has an integral solution and the LP maximum exists. Then every LP optimum has an IP optimum within $\ell_\infty$-distance $n\Delta(A)$, and every IP optimum has an LP optimum within the same distance.
2. Corollary 2 (p. 253). Under the same hypotheses, $\max\{wx: Ax\le b\}-\max\{wx : Ax\le b,\ x\text{ integral}\}\le n\Delta(A)\|w\|_1$.
3. Theorem 5 (p. 255). Changing $b$ to $b'$ moves LP optima by at most $n\Delta(A)\|b-b'\|_\infty$ and IP optima by at most $n\Delta(A)(\|b-b'\|_\infty+2)$. This result is off the goal's path.
4. Theorem 6 (p. 256). A non-optimal integral solution can be improved by an integral solution within $\ell_\infty$-distance $n\Delta(A)$.
5. Theorem 7 (p. 257). A single integral matrix $M$, with entries at most $n^{2n}\Delta(A)^n$ in absolute value, gives $\{x: Ax\le b\}_I=\{x : Mx\le d_b\}$ for every $b$ for which $Ax\le b$ has an integral solution.
6. Theorem 8, printed "Theorem 9" (p. 259). If a rational polyhedron $P\subseteq\mathbb{Q}^n$ has no integral point, then $P^{(n^{2n}2^{n^3})}=\emptyset$.
7. Corollary 9 (p. 260). Let $q=\max\{wx : x\in P_I\}$ with $w$ integral. Then $P^{(r)}\subseteq\{x : wx\le q\}$ for $r=(n^{2n}2^{n^3}+1)(\lfloor\max\{wx : x\in P\}\rfloor-q)+1$.

Significance

The result. Theorem 10 shows that the number of Gomory–Chvátal rounding rounds needed for $\{x : Ax\le b\}$ is controlled by $A$ alone. It is the first general finite bound on the Chvátal rank of a matrix. Earlier, the matrices of Chvátal rank 0 had been characterized by Hoffman and Kruskal: they are the matrices whose transpose is unimodular. Some classes of rank 1 had also been characterized (Edmonds–Johnson, Gerards–Schrijver). The proximity results of §2 are used on their own. They bound the work needed to solve an integer program from an LP optimum, and they show that the optimal value of an integer program changes at most affinely with $b$. They are also the standard starting point for the later proximity literature.

Formalizing it. All results are proved in the paper. As far as is known, none of them has a machine-checked proof: the Prove2Me corpus holds no Chvátal rank bound, and its existing proximity theorems concern a different bound, the $\ell_1$ bound with $\Delta$ the largest entry. This mission asks for Lean proofs of the paper's statements with the constants exactly as printed. It also builds a reusable layer over $\mathbb{Q}$: polyhedra, LP and IP optimality, integer hulls, the Chvátal closure and the Chvátal rank.

Difficulty

The proximity theorems need a conic decomposition $\bar x-\bar z=\sum\lambda_i g^i$ into integral generators with entries bounded by $\Delta(A)$. That requires Cramer's rule bounds on cone generators and Carathéodory's theorem, and neither is in Mathlib in this form for rational polyhedral cones.

Theorem 7 needs finite generation of integral cones with explicit coefficient bounds, together with LP duality.

The Chvátal-rank part is harder. The obvious induction on the value of a valid inequality fails, because the value gap $\lfloor\max_P wx\rfloor-q$ is not bounded independently of $b$ until Theorem 7 and Corollary 2 bound it by $n^{2n+2}\Delta(A)^{n+1}$. Theorem 8 itself rests on a flatness theorem for lattice-free polyhedra (Lenstra; Grötschel–Lovász–Schrijver), which the paper cites without proof. It also needs Schrijver's lemma that $P^{(k)}\cap F\subseteq F^{(k)}$ for faces $F$, and invariance under unimodular affine maps. None of these is in Mathlib.

Formalization scope

• Rationality. Everything is over $\mathbb{Q}$, following the paper's standing assumption on p. 252. Points are Fin n → ℚ, $A$ is Matrix (Fin m) (Fin n) ℤ cast to $\mathbb{Q}$, and a polyhedron is a finite system of rational inequalities.
• $\Delta(A)$. Only nonempty submatrices count, so $\Delta(0)=0$.
• Optimality. "The maximum exists" means an optimal solution exists. Existence claims that the paper proves are part of the conclusions: the IP optimum in Theorem 1 and Corollary 2, and $\max\{wx : x\in P\}$ in Corollary 9.
• Chvátal closure. It is defined for every subset of $\mathbb{Q}^n$, using all integral $a$ and rational $\beta$. The rank is valued in $\mathbb{N}\cup\{\infty\}$, with $\infty$ if no iterate equals $P_I$. A version with junk value $0$ would make the goal trivial and is not used. The matrix rank is a supremum over integral $b$, as printed.
• Added hypotheses. Theorems 1 and 6 carry the hypothesis $A\ne0$. For $A=0$ the bound $n\Delta(A)=0$ makes both statements false, and the proof on p. 257 assumes $A\ne0$ as well. In Corollary 9 the value $q$ is taken to be an integer. This loses nothing, because a maximum of an integral $w$ over $P_I$ is attained at an integral point.
• Constants. All constants are exactly as printed, written in $\mathbb{N}$ with $0^0=1$.

A complete development needs the following:

• cone generation with Cramer bounds and Carathéodory's theorem;
• LP duality and Farkas' lemma over $\mathbb{Q}$;
• the polyhedrality of $P'$ for rational polyhedra (Schrijver 1980);
• Schrijver's face lemma and unimodular invariance;
• a flatness theorem.

The LP, cone and Chvátal-closure layers are reusable beyond this mission. Proofs of any milestone are welcome, and so is groundwork such as polyhedrality of the Chvátal closure or the flatness theorem, submitted as separate theorems.

Selected references

• W. Cook, A.M.H. Gerards, A. Schrijver, É. Tardos, Sensitivity theorems in integer linear programming, Mathematical Programming 34 (1986) 251–264. https://doi.org/10.1007/BF01582230
• V. Chvátal, Edmonds polytopes and a hierarchy of combinatorial problems, Discrete Mathematics 4 (1973) 305–337. https://doi.org/10.1016/0012-365X(73)90167-2
• A. Schrijver, On cutting planes, Annals of Discrete Mathematics 9 (1980) 291–296. https://doi.org/10.1016/S0167-5060(08)70085-2
• W. Cook, C.R. Coullard, Gy. Turán, On the complexity of cutting-plane proofs, Discrete Applied Mathematics 18 (1987) 25–38. https://doi.org/10.1016/0166-218X(87)90039-4
• F. Eisenbrand, R. Weismantel, Proximity results and faster algorithms for integer programming using the Steinitz lemma, ACM Transactions on Algorithms 16 (2020), Art. 5. https://doi.org/10.1145/3340322

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

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

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.