The OR Formalization Drive

Motivation

The conjugate gradient method (cg-method) of Hestenes and Stiefel is the standard iterative solver for linear systems $Ax=k$ with a symmetric positive definite matrix $A$. It is used for the large sparse systems of finite-element and finite-difference discretizations, as the inner solver of Newton-type and interior-point methods in optimization, and as the prototype of the Krylov subspace methods. Its original 1952 paper (Hestenes and Stiefel, J. Res. NBS 49(6), 1952) already presented it as two things at once: a direct method that reaches the exact solution in at most $n$ steps, and a method of successive approximations whose intermediate estimates are useful in their own right.

The second view needs a guarantee that the intermediate estimates actually approach the solution. The method is built to decrease the $A$-weighted error $f(x)=(h-x,A(h-x))$, and the residual $|k-Ax_i|$ need not decrease (Section 18 of the paper, p. 432, notes that it can increase at every step). Theorem 6:3 of the paper supplies the guarantee in the plain Euclidean length: the distance $|h-x_i|$ from the estimate to the solution decreases strictly at every step, by an exactly computable amount. This mission formalizes that theorem together with the relations from Sections 5 and 6 of the paper on which its proof rests.

Timeline:

• 1952: Hestenes and Stiefel introduce the method and prove, in one paper, finite termination (Theorems 4:2 and 5:2), the monotone decrease of the error function $f$ (Theorem 6:1), and the monotone decrease of the Euclidean error (Theorem 6:3). The later literature on cg as an iterative method for large sparse systems takes these properties as its starting point.

Setting

Let $A$ be a real $n\times n$ matrix that is symmetric and positive definite, let $k\in\mathbb{R}^n$, and let $h$ be the solution of $Ah=k$. Write $(x,y)=x_1y_1+\cdots+x_ny_n$ and $|x|^2=(x,x)$. From an arbitrary starting point $x_0$, the cg-method (5:1) computes estimates $x_i$, residuals $r_i$ and direction vectors $p_i$ by

$$p_0=r_0=k-Ax_0,\quad a_i=\frac{|r_i|^2}{(p_i,Ap_i)},\quad x_{i+1}=x_i+a_ip_i,\quad r_{i+1}=r_i-a_iAp_i,\quad b_i=\frac{|r_{i+1}|^2}{|r_i|^2},\quad p_{i+1}=r_{i+1}+b_ip_i .$$

The error vector of $x_i$ is $y_i=h-x_i$. The error function (4:5) is $f(x)=(h-x,A(h-x))$, which is nonnegative and vanishes only at $x=h$. The Rayleigh quotient (4:12) of a vector $z\neq 0$ is $\mu(z)=(z,Az)/|z|^2$. The Lean development names these cgIter A k x₀ i (with fields .x, .r, .p), cgAlpha for $a_i$, errorFun A h x and rayleigh A z.

Formalization targets

Goal: Theorem 6:3

For every step that the method performs, that is, every $i$ with $r_i\neq 0$,

$$|y_i|^2-|y_{i+1}|^2=\frac{f(x_{i+1})+f(x_i)}{\mu(p_i)}\qquad\text{and}\qquad |y_{i+1}|<|y_i| .$$

The paper writes the step from $x_{i-1}$ to $x_i$; the Lean statement shifts the index by one. The goal holds for every dimension $n$, every symmetric positive definite $A$, every $k$ and every $x_0$.

Milestones

1. Theorems 4:2 and 5:2: some $m\le n$ has $x_m=h$.
2. Theorem 5:3, (5:6a): $(p_i,p_j)=|r_j|^2|p_i|^2/|r_i|^2$ for $i\le j$.
3. Theorem 6:1, (6:1): $f(x_i)-f(x_{i+1})=a_i|r_i|^2=\mu(p_i)|x_i-x_{i+1}|^2$.
4. Theorem 6:1, (6:2): $f(x_i)-f(x_j)=\sum_{l=i}^{j-1}a_l|r_l|^2$ for $i<j$.
5. Section 6, (6:6): $(y_{i+1},x_{i+1}-x_i)=f(x_{i+1})/\mu(p_i)$.

Significance

The theorem is what makes an early stop of the cg-method safe in the norm a user usually cares about. Every intermediate estimate is closer to the solution, in Euclidean distance, than the previous one, and the identity (6:5) states by how much. It also separates the cg-method from methods that minimize the residual: the $A$-norm error, the Euclidean error and the residual behave differently, and only the first two are monotone along cg.

The results are proved in the 1952 paper. They have not been formalized: the Prove2Me library has no statement of the conjugate gradient recursion (5:1), and Mathlib has none either. What this mission adds is a machine-checked version of the paper's Section 6 argument for the recursion exactly as printed, including the case analysis at termination that the paper leaves implicit, and a reusable Lean definition of the cg iteration with its basic identities.

Difficulty

The obvious argument does not reach the conclusion. The method decreases $f(x)=(y,Ay)$ at every step, but a decrease in this $A$-weighted norm does not imply a decrease in the Euclidean norm: for a single step along an arbitrary direction, even the best step for $f$ can lengthen the Euclidean error. So the theorem cannot be proved one step at a time from the local minimization property. It depends on how the current direction relates to all the later directions of the same run, and those relations in turn rest on the mutual orthogonality of the residuals and the conjugacy of the directions, which are established by an induction over the whole run.

A second difficulty is bookkeeping at the end of the run. The recursion divides by $|r_i|^2$ and by $(p_i,Ap_i)$, which vanish after termination. Every milestone has to hold, or be guarded, past that point, and the goal needs the hypothesis $r_i\neq 0$ exactly because the strict inequality fails once $x_i=h$.

Formalization scope

Vectors are Fin n → ℝ, the scalar product is dotProduct (⬝ᵥ), $Ax$ is Matrix.mulVec (*ᵥ), and the standing assumption is A.PosDef, which in Mathlib includes symmetry. The solution $h$ is a variable with the hypothesis A *ᵥ h = k. Indices are 0-based. The cg recursion is the definition cgIter, which computes (5:1b)–(5:1f) literally and in order; it has no stopping rule, and Lean's convention $t/0=0$ makes it stay at $h$ with $r_i=p_i=0$ once $r_m=0$. Lengths appear squared, as $(y,y)$. The milestones are stated for every index without a termination guard, because both sides of each identity vanish after termination; only the goal carries $r_i\neq 0$.

Two formalizations would trivialize the goal and are ruled out. The goal does not assume termination ($x_m=h$) or any bound on $i$: it quantifies over every cg run and every step that takes place. And it is about the Euclidean length $|h-x_i|$, not the error function $f$ (that is Theorem 6:1, a different and weaker statement) and not the residual.

A complete development needs Theorem 5:1 (orthogonality of residuals, conjugacy of directions) for the literal recursion, the identities (5:2) and (5:3c), and the positivity of $(p,Ap)$ for $p\neq 0$. These are reusable for any further work on the cg-method, including the sister mission on finite termination. Proofs of any milestone, and alternative proofs of Theorem 6:3 through the Krylov-subspace characterization, are welcome.

Selected references

• M. R. Hestenes and E. Stiefel, Methods of Conjugate Gradients for Solving Linear Systems, J. Res. Natl. Bur. Stand. 49(6), 409–436, 1952. https://doi.org/10.6028/jres.049.044 (publisher's scan: https://nvlpubs.nist.gov/nistpubs/jres/049/jresv49n6p409_A1b.pdf)

Motivation

Many operational systems move between a finite number of states at random times: a machine alternates between working and repair, a queue between occupancy levels, an inventory between stock positions. When the time spent in a state is not exponential and not a fixed period, neither discrete-time Markov decision processes nor continuous-time Markov chains describe the system faithfully. William S. Jewell's 1963 paper Markov-Renewal Programming. I extends Howard's Markov decision processes to Markov-renewal processes (also called semi-Markov processes), in which the time between transitions is a random variable whose law depends on the current state, the next state, and the decision taken. The resulting model, now called a semi-Markov decision process, is standard in maintenance, queueing control and reliability.

Timeline:

• 1954: Lévy, Smith and Takács independently introduce Markov-renewal and semi-Markov processes; Pyke later surveys them.
• 1960: Howard, Dynamic Programming and Markov Processes, introduces policy iteration for finite discrete-time Markov decision processes.
• 1962: Blackwell, Discrete Dynamic Programming, shows that for the discounted discrete-time problem a stationary policy is optimal among all policies.
• 1963: Jewell formulates Markov-renewal programming, with a continuous discount factor α, and carries Howard's algorithm and Blackwell's stationarity result over to it. Part II of the paper treats the undiscounted (infinite-return) models.

Setting

A Markov-renewal program has a finite set of states $S$ (the paper's $i = 1, \dots, N$) and a finite, nonempty set of alternatives (the paper's $z = 1, \dots, Z$), each available in every state. For each alternative $z$ and states $i, j$ it specifies:

• a transition probability $p^z_{ij} \ge 0$, with $\sum_j p^z_{ij} = 1$;
• a sojourn-time distribution $F^z_{ij}$, the law of the time $\tau$ between entering $i$ and moving to $j$, with $\tau \ge 0$ and $F^z_{ij}(0) = 0$;
• for each continuous discount factor $\alpha > 0$, a real number $\rho^z_{ij}(\alpha)$, the expected discounted return earned during that transition.

The Laplace–Stieltjes transform $\tilde f^z_{ij}(s) = \int_0^\infty e^{-st}\,dF^z_{ij}(t)$ is the expected discount $\mathbb E[e^{-s\tau}]$ over one interval. The average one-step return is $\rho^z_i(\alpha) = \sum_j p^z_{ij}\rho^z_{ij}(\alpha)$, and for a vector of returns $v$ the test quantity is

$$\rho^z_i(\alpha) + \sum_j p^z_{ij}\,\tilde f^z_{ij}(\alpha)\,v_j .$$

A stationary policy is a map $d : S \to A$; a nonstationary policy is a sequence $\pi = (\pi_0, \pi_1, \dots)$ of such maps, $\pi_k$ being used at the $k$-th transition. The $n$-step return $V^\pi_i(n)$ of a policy, with boundary rewards $V_i(0,\alpha)$, is the test quantity of $\pi_0(i)$ applied to the $(n-1)$-step return of the shifted policy; the optimal $n$-step return $V_i(n,\alpha)$ of equation (6) replaces $\pi_0(i)$ by a maximum over $z$. The value-determination equations (15) of a stationary policy $d$ are $v_i = \rho^{d(i)}_i(\alpha) + \sum_j p^{d(i)}_{ij}\tilde f^{d(i)}_{ij}(\alpha) v_j$.

The algorithm of Fig. 1 alternates two steps: solve (15) for the current policy, then in every state pick an alternative maximizing the test quantity, keeping the old alternative if it still attains the maximum. It stops when two successive policies are identical.

Formalization targets

Goal (p. 947)

For every $\alpha > 0$: (15) has a unique solution for every stationary policy, and every run $(d_k, v_k)$ of Fig. 1 reaches $d_{K+1} = d_K$ with $K < Z^N$, where

$$\lim_{n\to\infty} V^{d_K}_i(n) = (v_K)_i,\qquad \lim_{n\to\infty} V^\pi_i(n) \le (v_K)_i \ \ \forall \pi,\qquad \lim_{n\to\infty} V_i(n,\alpha) = (v_K)_i ,$$

for every state $i$ and all boundary rewards, every limit existing. This is the paper's "the algorithm of Fig. 1 produces an optimal, stationary policy that is as good as any optimal, nonstationary policy".

Milestones

1. p. 945: $0 \le p^z_{ij}\tilde f^z_{ij}(s) < 1$ for $s > 0$.
2. Claim (a): (15) has exactly one solution for each stationary policy.
3. Eq. (15): the $n$-step return of a stationary policy converges to a solution of (15).
4. p. 946: $I - \tilde q(\alpha)$ is invertible and $([I-\tilde q(\alpha)]^{-1})_{ii} \ge 1$.
5. Claim (b): a change of policy raises the return of some state and lowers none.
6. Claim (c): a policy reproduced by the improvement step is optimal among stationary policies.
7. Claim (d): a run of Fig. 1 terminates within $Z^N$ cycles.
8. Eq. (14): $V_i(n,\alpha)$ converges, independently of the boundary rewards, to a solution of $v_i = \max_z\{\rho^z_i(\alpha) + \sum_j p^z_{ij}\tilde f^z_{ij}(\alpha) v_j\}$.
9. p. 946: some stationary policy's return dominates the limiting return of every nonstationary policy.

Significance

The result says that the infinite-step discounted Markov-renewal program is solved exactly, in finitely many cycles, by a finite-dimensional algorithm, and that the answer is a stationary policy. As the paper notes, this matters operationally because a nonstationary policy is hard to follow. The sojourn distributions enter only through the numbers $\tilde f^z_{ij}(\alpha)$, so the same algorithm serves any sojourn-time law. For fixed $\alpha$ the model is a discounted Markov decision process whose discount factor depends on the transition, which contains Howard's and Blackwell's constant-discount problem as the case of intervals of fixed length (p. 943).

The results are classical and proved in the literature. The paper itself refers the proofs to Howard and Blackwell. Machine-checked versions exist on this platform for finite stochastic shortest path and constant-discount problems (Bertsekas, Dynamic Programming and Optimal Control, Prop. 7.2.2 and 7.3.1, mission Dynamic Programming and Optimal Control VII). No formal treatment of Markov-renewal programs, of transition-dependent discounting, or of the retention rule of Fig. 1 is known to exist. The mission produces a verified policy-iteration theorem for semi-Markov decision processes, with an explicit termination bound and the comparison against nonstationary policies.

Difficulty

The discount over one transition, $\tilde f^z_{ij}(\alpha)$, varies with $i$, $j$ and $z$, so the problem is not a constant-$\gamma$ contraction of textbook form; the relevant bound is that every row of $\tilde q(\alpha)$ sums to less than one, which rests on $F^z_{ij}(0) = 0$. Entries in $[0, 1)$ alone, the paper's stated justification of Claim (a), do not make $I - \tilde q(\alpha)$ invertible: the $2 \times 2$ matrix with every entry $1/2$ has entries in $[0,1)$, yet $I$ minus it is singular.

Finite termination is not automatic either. If the improvement step may switch between tied maximizers, the iterates can cycle forever between two policies with equal returns; the retention rule of Fig. 1 excludes this, and Claim (b) must deliver a strict increase in some state, with no decrease anywhere, to rule out revisiting a policy. Comparing with nonstationary policies requires controlling returns of arbitrary policy sequences, whose limits must be shown to exist, not assumed.

Formalization scope

• States and alternatives are finite types; alternatives are nonempty. Every alternative is available in every state.
• $F^z_{ij}$ is a probability measure on $\mathbb R$ with no mass on $(-\infty, 0]$. The transform is integrated over $(0, \infty)$, which carries all the mass.
• The one-transition returns $\rho^z_{ij}(\alpha)$ are arbitrary real numbers, a generalization of the paper's Stieltjes integral (4), which is not formalized. The reward functions $R^z_{ij}(t\mid\tau)$ do not appear.
• Returns of policies are defined by the one-step recursion (the policy form of (6)); the Markov-renewal process is not built as a stochastic process.
• Policies are the paper's: deterministic and Markov, nonstationary ones indexed by the number of transitions made. Randomized and history-dependent policies are not in the comparison class.
• The following informal words are read as follows. "Solve the set of simultaneous equations": (15) has exactly one solution. "Strictly increases the expected return of at least one state": no state's return decreases and one strictly increases, under the hypothesis that the policy changed. "No other policy can lead to higher expected returns" in Claim (c): no stationary policy. "Terminates in a finite number of cycles": two successive policies coincide at some cycle $K < Z^N$. "If there is no improvement in the test quantity, retain the same alternative": the old alternative is kept whenever it attains the maximum. "Optimal" and "as good as any nonstationary policy": the limiting return of the returned policy dominates that of every policy from every state, for all boundary rewards. "$\lim_{n\to\infty} V_i(n,\alpha)$": the limit is proved to exist. "$\max_z$": a maximum over the finite nonempty set of alternatives.
• Eq. (14) is printed with $v_i(\alpha)$ inside the sum over $j$; the formalization uses $v_j(\alpha)$, as (6), (15) and Fig. 1 do.
• Every statement fixes one $\alpha > 0$. The undiscounted models (16)–(19), the finite-time and mixed-horizon models (9)–(13), and the infinite-time case of the stationarity result are out of scope.
• The return of a policy is never defined through a matrix inverse, whose Mathlib value for a singular matrix is $0$; (15) is a predicate, and the goal asserts unique solvability, so a vacuous reading through junk inverses or assumed limits is excluded.

Reusable infrastructure: bounds for substochastic matrices with row sums below one (invertibility, Neumann series, nonnegative inverse), convergence of iterated Bellman operators with transition-dependent discount, and the policy-iteration termination argument with a tie-breaking rule. Proofs of any milestone and alternative arguments are welcome.

Selected references

• W. S. Jewell, Markov-Renewal Programming. I: Formulation, Finite Return Models, Operations Research 11(6), 938–948, 1963. https://doi.org/10.1287/opre.11.6.938
• W. S. Jewell, Markov-Renewal Programming. II: Infinite Return Models, Example, Operations Research 11(6), 949–971, 1963. https://doi.org/10.1287/opre.11.6.949
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
• D. Blackwell, Discrete Dynamic Programming, Annals of Mathematical Statistics 33(2), 719–726, 1962. https://doi.org/10.1214/aoms/1177704593
• R. Pyke, Markov Renewal Processes: Definitions and Preliminary Properties, Annals of Mathematical Statistics 32(4), 1231–1242, 1961. https://doi.org/10.1214/aoms/1177704863
• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005, Section 7.2–7.3.

Motivation

Bin packing asks for the fewest unit-capacity bins that hold a given list of item sizes. It models cutting stock, memory allocation, file placement and the loading of trucks, and it is NP-hard, so in practice lists are packed by simple rules that look at one item at a time. The two most widely used rules are First-Fit and Best-Fit, and the question that Johnson, Demers, Ullman, Garey and Graham answered in 1974 is how far from optimal they can be in the worst case.

Their headline answer is that both rules use at most about $\tfrac{17}{10}$ times the optimal number of bins, and that $\tfrac{17}{10}$ is asymptotically attained. The lists that force this ratio use items larger than $\tfrac12$. When all items are known to be small, which is typical of memory and storage applications, the guarantee is much better, and this mission is about that refinement: the paper's Theorem 2.3 and its corollary, which determine the asymptotic worst-case ratio of First-Fit and Best-Fit exactly as a function of the largest allowed item size $\alpha\le\tfrac12$.

Timeline. Ullman (1971) introduced the worst-case analysis of First-Fit with a $\tfrac{17}{10}L^*+3$ bound. Garey, Graham and Ullman (1972) and Johnson's thesis (MIT, 1973) extended it to Best-Fit and to the decreasing variants. The 1974 SIAM paper collects these results; Theorem 2.3 there is the parametric bound for items of size at most $\alpha$. The additive constants in the unrestricted $\tfrac{17}{10}$ bound were sharpened over the following four decades, culminating in Dósa and Sgall's proof (2013) that $FF(L)\le\lfloor\tfrac{17}{10}L^*\rfloor$.

Setting

A list is a finite sequence $L=(a_1,\dots,a_n)$ of real numbers in $(0,1]$. Its optimum $L^*$ is the least number of bins into which the elements of $L$ can be placed so that no bin contains numbers whose sum exceeds $1$. The level of a bin is the sum of the numbers in it. For a real $\alpha>0$, write $L\subseteq(0,\alpha]$ when every element of $L$ is at most $\alpha$.

First-Fit ($FF$) considers bins $B_1,B_2,\dots$, all initially empty, and places $a_1,a_2,\dots,a_n$ in that order: $a_i$ goes into the bin $B_j$ of least index whose level $\beta$ satisfies $\beta\le 1-a_i$. Best-Fit ($BF$) is the same except that, among the bins with $\beta\le 1-a_i$, it chooses one of largest level $\beta$ (least index among ties). $FF(L)$ and $BF(L)$ denote the numbers of nonempty bins at the end.

The restricted worst-case ratios are

$$R^\alpha_{FF}(k)=\max\Big\{\frac{FF(L)}{L^*}: L\subseteq(0,\alpha],\ L^*=k\Big\},\qquad R^\alpha_{BF}(k)=\max\Big\{\frac{BF(L)}{L^*}: L\subseteq(0,\alpha],\ L^*=k\Big\}.$$

Throughout, $0<\alpha\le\tfrac12$ and $m=\lfloor\alpha^{-1}\rfloor$, an integer with $m\ge 2$ and $\tfrac1{m+1}<\alpha\le\tfrac1m$.

Formalization targets

Goal: the asymptotic ratio (Corollary of Theorem 2.3, p. 308)

$$\lim_{k\to\infty}R^\alpha_{FF}(k)=\lim_{k\to\infty}R^\alpha_{BF}(k)=1+\frac{1}{\lfloor\alpha^{-1}\rfloor}.$$

The goal is stated as a limit, which is the stable form of the result: it is unaffected by any improvement of the additive constants below.

Theorem 2.3(i): the lower bound (p. 307)

For each $k\ge1$ there is a list $L\subseteq(0,\alpha]$ with $L^*=k$ and $FF(L)\ge\frac{m+1}{m}L^*-\frac1m$; likewise for $BF$.

Two steps of the First-Fit upper bound (p. 308)

If no element of $L$ exceeds $\frac1m$, then in the First-Fit packing every bin except possibly the last contains at least $m$ elements, and all but at most two bins have level at least $\frac{m}{m+1}$.

Theorem 2.3(ii): the upper bounds (p. 307)

For every list $L\subseteq(0,\alpha]$,

$$FF(L)\le\frac{m+1}{m}L^*+2,\qquad BF(L)\le\frac{m+1}{m}L^*+2.$$

Significance

The theorem gives an exact, parametric description of how the worst case of the two greedy rules improves as items shrink: the asymptotic ratio is $\tfrac32$ when items are at most $\tfrac12$, $\tfrac43$ when at most $\tfrac13$, and tends to $1$ as the maximum item size tends to $0$. Combined with the $\tfrac{17}{10}$ bound for unrestricted lists, it shows that the bad behaviour of First-Fit is caused entirely by items larger than $\tfrac12$. Such parametric bounds are the standard way bin-packing heuristics are compared in the literature on online and semi-online packing, and the construction in part (i) is a reusable template for lower-bound lists.

The paper proves the First-Fit upper bound and the lower bound (the verification of the lower-bound construction is left to the reader). The Best-Fit upper bound is stated but not proved: the paper says only that "a similar, but slightly more complicated, argument can be used". A formal proof of the goal therefore requires supplying that argument. None of these results is known to have a machine-checked proof; Mathlib contains no bin-packing development.

Difficulty

For First-Fit the upper bound is a counting argument, but it rests on a property of the run, not of the final packing: an item that went into a later bin did not fit into an earlier bin at the moment it was placed. Turning that into a statement about the final levels requires an invariant maintained through the whole sequence of placements.

The Best-Fit upper bound is harder because that property fails: Best-Fit may put a small item into a fuller, later bin while an earlier, lighter bin still has room, so a light early bin and a light later bin can coexist longer than under First-Fit. The paper gives no argument for this case.

The lower bound requires computing the exact behaviour of both algorithms on a specific interleaved list with item sizes perturbed by powers of $m$, and computing $L^*$ exactly for that list, which needs a matching lower bound on the optimum.

Formalization scope

A list is L : List ℝ with the hypothesis IsList L (every element in $(0,1]$); $L\subseteq(0,\alpha]$ is the additional hypothesis ∀ a ∈ L, a ≤ α. $L^*$ is optBins L, a sInf in ℕ over numbers of bins admitting a feasible assignment; the hypothesis IsList makes the set nonempty. The runs ffPack L and bfPack L are folds over the list that keep the nonempty bins in the order they were opened, each with its contents; an item that fits nowhere opens a new bin at the end, which is the paper's "least $j$" over infinitely many empty bins. Comparisons are exact (classical decidability on ℝ), and $FF(L)$, $BF(L)$ are the lengths of the final bin lists. $m$ is Nat.floor α⁻¹, cast before any division.

The ratios $R^\alpha_{FF}(k)$, $R^\alpha_{BF}(k)$ are suprema taken in ℝ≥0∞: an unbounded family would give $+\infty$, never a default value, and at $k=0$ the only admissible list is empty and the value is $0$. The goal is a Tendsto … atTop (𝓝 (1 + (⌊α⁻¹⌋₊)⁻¹)) statement in ℝ≥0∞. A real-valued sSup would have returned $0$ on an unbounded family and made a false bound look provable; that encoding is ruled out. The upper bounds keep the additive constant $2$ and the lower bound the subtractive $\frac1m$ exactly as printed.

The two proof steps are stated under the proof's own hypothesis "no element exceeding $1/m$", which is weaker than $L\subseteq(0,\alpha]$.

A complete development needs invariants of the First-Fit and Best-Fit folds, a lower bound $L^*\ge\sum_i a_i$, and exact evaluation of both runs on the construction of part (i). Lemmas about the fold encoding of First-Fit and Best-Fit and about $L^*$ are reusable in the companion missions on the $\tfrac{17}{10}$, $\tfrac{11}{9}$ and $\tfrac{71}{60}$ bounds of the same paper. Contributions on the Best-Fit upper bound are especially welcome, since the source gives no proof.

Selected references

• D. S. Johnson, A. Demers, J. D. Ullman, M. R. Garey, R. L. Graham, Worst-Case Performance Bounds for Simple One-Dimensional Packing Algorithms, SIAM Journal on Computing 3(4):299–325, 1974. https://doi.org/10.1137/0203025
• J. D. Ullman, The Performance of a Memory Allocation Algorithm, Technical Report 100, Princeton University, 1971.
• M. R. Garey, R. L. Graham, J. D. Ullman, Worst-Case Analysis of Memory Allocation Algorithms, Proc. 4th ACM Symposium on Theory of Computing, 143–150, 1972. https://doi.org/10.1145/800152.804907
• D. S. Johnson, Near-Optimal Bin Packing Algorithms, PhD thesis, Massachusetts Institute of Technology, 1973. http://hdl.handle.net/1721.1/57819
• G. Dósa, J. Sgall, First Fit Bin Packing: A Tight Analysis, Proc. 30th STACS, LIPIcs 20:538–549, 2013. https://doi.org/10.4230/LIPIcs.STACS.2013.538

Motivation

The Critical-Path Method (CPM) was introduced by J. E. Kelley, Jr. (Remington Rand) and M. R. Walker (du Pont) in Critical-Path Planning and Scheduling (Proc. Eastern Joint Computer Conference, 1959, pp. 160–173, doi:10.1145/1460299.1460318). Together with PERT, developed at the same time for the Polaris programme, it became the standard way to plan and schedule large projects in construction, maintenance and engineering, and it is taught in every introductory operations research course.

The paper reduces project scheduling to arithmetic on a directed acyclic graph: the earliest and latest times of the project's events are computed by two recursions, and the jobs whose timing has no slack, the critical jobs, are singled out by an equation. Its central structural claim is that critical jobs, when they exist, form a path from the start of the project to its end. The paper states this without proof ("a detailed development being reserved for a separate paper", p. 161). This mission formalizes that claim and the facts about the two recursions on which it rests.

Setting

A project network has $n+1$ events labelled $0,1,\dots,n$ with $n \ge 1$: event $0$ is the origin and event $n$ the terminus. A job is an arrow from an event $i$ to an event $j$, written job $(i,j)$; the jobs form a finite set $P$ of ordered pairs of events. Two standing assumptions of the paper (pp. 161–162) are part of the model:

1. every job has $i < j$ (events are labelled so that the head of an arrow has the larger label);
2. origin precedes and terminus follows every event: for every event $k$ there are chains of jobs from $0$ to $k$ and from $k$ to $n$.

Each job has a real duration $y_{ij}$. The earliest event times $t^{(0)}$ are given by display (1) of the paper,

$$t_0^{(0)} = 0,\qquad t_j^{(0)} = \max\,[\,y_{ij} + t_i^{(0)} \mid i<j,\ (i,j)\in P\,],\quad 1\le j\le n,$$

and, for a project completion time $\lambda \ge t_n^{(0)}$, the latest event times $t^{(1)}$ by display (2),

$$t_n^{(1)} = \lambda,\qquad t_i^{(1)} = \min\,[\,t_j^{(1)} - y_{ij} \mid i<j,\ (i,j)\in P\,],\quad 0\le i\le n-1.$$

The maximum time available for job $(i,j)$ is $t_j^{(1)} - t_i^{(0)}$. The job is critical if this equals its duration, $t_j^{(1)} - t_i^{(0)} = y_{ij}$, and a floater if it exceeds it. A critical path is a contiguous path of critical jobs from origin to terminus: events $0 = v_0, v_1, \dots, v_k = n$ with every $(v_{r-1}, v_r)$ a critical job of $P$.

In the Lean development these are ProjectNetwork n (with field P), earliest N y, latest N y λ, maxTimeAvailable, IsCritical, IsFloater and IsCriticalPath, in the namespace CriticalPath.Events.

Formalization targets

Goal: critical jobs force $\lambda = t_n^{(0)}$ and a critical path (p. 163)

For every project network, durations $y$ and completion time $\lambda \ge t_n^{(0)}$,

$$\bigl(\exists (i,j)\in P,\ t_j^{(1)} - t_i^{(0)} = y_{ij}\bigr) \;\Longrightarrow\; \lambda = t_n^{(0)} \ \wedge\ \exists\ \text{a critical path}.$$

This is the paper's "A project will contain critical jobs only when $\lambda = t_n^{(0)}$. If a project does contain critical jobs, then it also contains at least one contiguous path of critical jobs through the project diagram from origin to terminus." Only the "only when" direction is asserted, as on the page.

Milestones

1. Display (1), pp. 162–163. $t^{(0)}$ is the least vector $t$ with $t_0 = 0$ and $y_{ij} \le t_j - t_i$ for every job.
2. Display (2), p. 163. For $\lambda \ge t_n^{(0)}$, $t_n^{(1)} = \lambda$ and $t^{(1)}$ is the greatest vector $t$ with $t_n \le \lambda$ and $y_{ij} \le t_j - t_i$ for every job.
3. Critical or floater, p. 163. For $\lambda \ge t_n^{(0)}$, $t_i^{(0)} \le t_i^{(1)}$ for every event, and every job is critical or a floater: $t_j^{(1)} - t_i^{(0)} \ge y_{ij}$.
4. Delay of a critical job, p. 163. Lengthening a critical job by $\delta \ge 0$ raises $t_n^{(0)}$ by exactly $\delta$.

Significance

The result. The theorem is what makes the method's name meaningful: it says that the jobs without slack are not scattered but line up along an origin–terminus path, and that such jobs exist only when the project is scheduled at its earliest possible completion time. Project managers use this to decide which jobs to watch, which to expedite, and which may slip; the delay statement (milestone 4) is the quantitative form of that advice. The characterisations of (1) and (2) as least and greatest feasible schedules are the bridge between CPM and linear programming: they identify $t^{(0)}$ and $t^{(1)}$ with extreme solutions of the system of difference constraints $y_{ij} \le t_j - t_i$, which the paper's own §3 uses to build the project cost curve.

Formalizing it. The results are classical and folklore, but the paper proves none of them, and textbook treatments usually define the critical path as a longest path, which makes the goal a tautology. This mission states the claims with the paper's own definitions: criticality by the float equation, event times by the recursions. To the best of current knowledge no machine-checked version of these statements for activity-on-arrow networks exists; the platform has a related activity-on-node development (Brucker and Knust, Complex Scheduling) in which the critical path is defined as a longest path.

Difficulty

The recursions (1) and (2) are local: each event looks only at its immediate predecessors or successors. The goal is global: from one critical job it asserts a statement about the whole completion time and a whole origin–terminus path. The float equation $t_j^{(1)} - t_i^{(0)} = y_{ij}$ mixes a quantity computed forward from the origin with one computed backward from the terminus, and neither recursion alone says anything about the other. The naive reading "a critical job lies on a longest path" is not available as a definition: it is, in substance, what has to be established from the recursions. The formal overhead is the well-founded recursion on the labels, in both directions, and the bookkeeping of lists of events forming a path.

Formalization scope

Events are Fin (n + 1), origin 0, terminus Fin.last n, with 1 ≤ n. Jobs are a Finset of ordered pairs, so there is at most one job per ordered pair. The standing assumptions (labels increase along jobs; origin precedes and terminus follows every event, via Relation.ReflTransGen) are fields of the structure ProjectNetwork and are never dropped. Durations and times are real numbers; durations are a function Fin (n+1) → Fin (n+1) → ℝ read only on jobs of P, with no sign condition, as in the paper's deterministic case.

The event times are defined by the recursions (1) and (2) themselves, by well-founded recursion on the label with Finset.sup'/Finset.inf' over the predecessor/successor set; these sets are nonempty by the standing assumptions, so no fallback value exists. The latest times are defined for every real $\lambda$; the paper's assumption $\lambda \ge t_n^{(0)}$ is a hypothesis of every theorem that uses them.

Disclosed readings: "earliest time occurance" (milestone 1) and "latest time … relative to a fixed project completion time" (milestone 2) are read as least and greatest vectors satisfying the job constraints $y_{ij} \le t_j - t_i$ (the paper's constraint (8), p. 165); milestone 3 is the fact implicit in the dichotomy "critical or floater"; "comparable delay" (milestone 4) is read as an exact delay of $\delta$ in $t_n^{(0)}$ for $\delta \ge 0$.

A trivializing formalization is ruled out: defining a critical job or path through longest paths, or taking $t^{(0)}$ and $t^{(1)}$ as arbitrary functions satisfying (1) and (2), would make the goal a restatement of its definitions; here criticality is the float equation and the times are computed by the recursions. Dropping the reachability assumptions would make (2) ill-defined at events without successors.

Contributions welcome: proofs of the milestones, general lemmas on longest paths in finite labelled DAGs and on difference constraints $y_{ij} \le t_j - t_i$, which are reusable for the companion mission on the project cost curve.

Selected references

• J. E. Kelley, Jr. and M. R. Walker, Critical-Path Planning and Scheduling, Papers presented at the December 1–3, 1959, Eastern Joint IRE-AIEE-ACM Computer Conference, pp. 160–173, 1959. doi:10.1145/1460299.1460318
• J. E. Kelley, Jr., Critical-Path Planning and Scheduling: Mathematical Basis, Operations Research 9(3), pp. 296–320, 1961. doi:10.1287/opre.9.3.296
• P. Brucker and S. Knust, Complex Scheduling, 2nd ed., Springer, 2012. doi:10.1007/978-3-642-23929-8

Motivation

A large engineering or construction project is a set of jobs with precedence constraints, and most jobs can be finished faster at a higher cost (overtime, more crews, faster equipment). Planners want to know, for every possible project duration, the cheapest way to meet it. The resulting trade-off between duration and direct cost is what management compares with overhead, penalties and market losses when it picks a schedule.

J. E. Kelley, Jr. and M. R. Walker introduced the critical-path method (CPM) in 1959, from work at du Pont and Remington Rand (Kelley and Walker 1959). Alongside the critical-path computation, they modelled each job's cost as a linear function of its duration and posed the choice of durations as a parametric linear program. They stated that its optimal value, as a function of the project duration $\lambda$, is a non-increasing, piecewise linear, convex function, which they called the project cost curve. The 1959 paper gives no proof and defers the detailed development to a separate paper (Kelley 1961). Fulkerson (1961) gave a network-flow algorithm that computes the curve. Time–cost trade-off analysis ("crashing") has been a standard part of project management since then.

Setting

A project network has events labelled $0, 1, \dots, n$ with $n \ge 1$. Event $0$ is the origin and event $n$ the terminus. A finite set $P$ of jobs is given, each an ordered pair $(i,j)$: an arrow from event $i$ to event $j$. As in the paper, labels increase along arrows ($i < j$ for every $(i,j) \in P$), the origin precedes every event, and the terminus follows every event.

For job durations $y = (y_{ij})$, the earliest event times are given by recursion (1):

$$t_0^{(0)} = 0,\qquad t_j^{(0)} = \max\,[\,y_{ij} + t_i^{(0)} \mid i<j,\ (i,j)\in P\,],\quad 1\le j\le n,$$

and $t_n^{(0)}(y)$ is the earliest project completion time.

Each job has a crash duration $d_{ij}$ and a normal duration $D_{ij}$ with $0 \le d_{ij} \le D_{ij}$, and a linear job cost $a_{ij}y_{ij} + b_{ij}$ with $a_{ij} \le 0$, $b_{ij} \ge 0$. The project (direct) cost is

$$\text{(7)}\qquad \sum_{(i,j)\in P} (a_{ij} y_{ij} + b_{ij}).$$

A schedule for $\lambda$ is a pair $(y,t)$ with

$$\text{(5)}\ d_{ij}\le y_{ij}\le D_{ij},\qquad \text{(8)}\ y_{ij}\le t_j-t_i\quad ((i,j)\in P),\qquad \text{(9)}\ t_0=0,\ t_n=\lambda.$$

Let $\Lambda$ be the set of $\lambda$ for which a schedule exists. For $\lambda \in \Lambda$ the project cost curve $C(\lambda)$ is the minimum of (7) over schedules for $\lambda$. Write $\lambda_c = t_n^{(0)}(d)$ (all jobs crashed) and $\lambda_N = t_n^{(0)}(D)$ (all jobs normal).

Formalization targets

Goal: the shape of the project cost curve (p. 165)

$$C \text{ is non-increasing on } \Lambda,\qquad C \text{ is piecewise linear on } \Lambda,\qquad C \text{ is convex on } \Lambda .$$

Piecewise linear means finitely many breakpoints $\beta_0<\dots<\beta_m$ with $\Lambda\subseteq[\beta_0,\infty)$, and affine pieces on $\Lambda\cap[\beta_k,\beta_{k+1}]$ and on $\Lambda\cap[\beta_m,\infty)$. The goal fixes no breakpoints or slopes. It asserts only the shape the paper claims, on the whole of $\Lambda$.

Milestones

1. Feasible range (p. 165, "until no further reduction in project completion time is possible"): $\Lambda = [\lambda_c, \infty)$.
2. Existence of optimal schedules (p. 165, the linear program (8), (9)): for every $\lambda\in\Lambda$ the minimum of (7) is attained.
3. All-normal solution (p. 165): $(D, t^{(0)}(D))$ is a minimum cost schedule for $\lambda = \lambda_N$.
4. $\lambda$ is the earliest completion time (p. 165, "within the limits of most interest"): for $\lambda_c\le\lambda\le\lambda_N$ some minimum cost schedule $(y,t)$ for $\lambda$ has $t_n^{(0)}(y)=\lambda$.

Significance

The cost curve is the output of CPM's cost analysis. Its convexity is what makes the paper's parametric procedure valid: jobs are expedited in order of increasing marginal cost, and the curve is traced from $\lambda_N$ down to $\lambda_c$ one linear piece at a time. Monotonicity justifies reading the curve as a trade-off. Piecewise linearity with finitely many pieces means the whole curve is determined by finitely many characteristic schedules, the vertices plotted in the paper's Fig. 3. The milestones identify the domain of the curve, show that it is well defined, and fix its right end at the all-normal solution.

These facts are classical: they follow from parametric linear programming, and Kelley (1961) and Fulkerson (1961) develop them in detail. No machine-checked proof of them is known. Prove2Me has a related result, LinearOptimization.lp_optimal_cost_convex_in_rhs (Bertsimas–Tsitsiklis, Theorem 5.1): convexity of the optimal cost of a standard-form LP in its right-hand side. It covers convexity only, for a different LP form, and says nothing about monotonicity or finitely many pieces. This mission adds a formal model of CPM's time–cost program and the full three-part shape theorem.

Difficulty

Convexity alone follows from the usual argument: a convex combination of optimal schedules for two durations is a schedule for the combined duration. Monotonicity needs the structure of the network: when $\lambda$ increases, only the constraints (8) on jobs ending at the terminus loosen, because no job leaves the terminus. The hard part is piecewise linearity with finitely many pieces. Convexity does not imply it, and a general result on value functions of linear programs has to be tied to this specific program, whose right-hand side depends on $\lambda$ only through $t_n = \lambda$. The domain is also unbounded, so the argument must show that the curve is eventually a single affine (in fact constant) piece. It cannot just produce finitely many pieces on a compact interval.

Formalization scope

Events are Fin (n + 1) with origin 0 and terminus Fin.last n, and 1 ≤ n. Jobs are a Finset of ordered pairs, with at most one job per ordered pair. The standing assumptions of pp. 161–162 are fields of ProjectNetwork: labels increase along jobs, and reachability via Relation.ReflTransGen from the origin and to the terminus. Times and durations are real. Job data are functions Fin (n+1) → Fin (n+1) → ℝ, constrained and read only on $P$. The hypotheses $0\le d_{ij}\le D_{ij}$, $a_{ij}\le 0$ and $b_{ij}\ge 0$ are fields of JobData. Recursion (1) is earliest, defined by well-founded recursion on the label. It uses a fallback value $0$ for an event without predecessors, which occurs only at the origin. The paper's $\lambda$ is written lam. Constraint (9) fixes $t_n = \lambda$ exactly, and the event times are otherwise unconstrained.

The goal takes $C : \mathbb{R}\to\mathbb{R}$ with the hypothesis that $C(\lambda)$ is the least element of the set of costs of schedules for $\lambda$, for every $\lambda \in \Lambda$. All three conclusions are stated on $\Lambda$ only. This rules out the trivializing formalizations:

• a junk-valued infimum off $\Lambda$ plays no role;
• $C$ is tied to the program, and the hypothesis on $C$ is satisfiable by milestone 2;
• piecewise linearity requires finitely many pieces that cover all of $\Lambda$;
• all three properties are claimed, not convexity alone.

The goal keeps $a_{ij}\le 0$, as the page does throughout §3, although monotonicity and convexity would hold without it.

Disclosed readings:

• Milestone 1 renders "until no further reduction in project completion time is possible" as $\Lambda=[\lambda_c,\infty)$.
• Milestone 4 reads "within the limits of most interest" as $\lambda_c\le\lambda\le\lambda_N$. It asserts that some optimal schedule has $t_n^{(0)}(y)=\lambda$. "Every" is false: when all $a_{ij}=0$, the all-crash durations are optimal for every $\lambda$.

A complete development needs:

• the existence of LP optima under a bounded objective, or a direct compactness argument on the feasible polyhedron;
• a parametric-LP or polyhedral argument for finitely many linear pieces;
• basic facts on the recursion (1).

The one-variable notion IsPiecewiseLinearOn and the facts on earliest event times can be reused in scheduling missions. Proofs of the milestones, of any of the three goal conjuncts separately, and general lemmas on parametric LP value functions are all welcome.

Not formalized: general piecewise linear convex job costs (deferred by the paper to its references [7], [8]), and the primal–dual procedure itself (a method, not a claim).

Selected references

• J. E. Kelley, Jr. and M. R. Walker, Critical-Path Planning and Scheduling, Proc. Eastern Joint IRE-AIEE-ACM Computer Conference, 1959, pp. 160–173. https://doi.org/10.1145/1460299.1460318
• J. E. Kelley, Jr., Critical-Path Planning and Scheduling: Mathematical Basis, Operations Research 9(3), 1961, pp. 296–320. https://doi.org/10.1287/opre.9.3.296
• D. R. Fulkerson, A Network Flow Computation for Project Cost Curves, Management Science 7(2), 1961, pp. 167–178. https://doi.org/10.1287/mnsc.7.2.167
• D. Bertsimas and J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, §5.2 (the optimal cost as a function of the right-hand side).

Motivation

Interior point methods solve a linear program by following a central path: a curve of minimizers of a penalized objective that trades off cost against distance from the boundary of the feasible region. The classical analysis of path following with the logarithmic barrier needs $O(\sqrt{m}\,L)$ iterations for a program with $m$ constraints, where $L$ is the bit complexity of the input (Renegar 1988). For programs with many more constraints than variables, $m$ can be far larger than the dimension $n$ or the rank of the constraint matrix, and the $\sqrt m$ factor is then the bottleneck.

Lee and Sidford (FOCS 2014) reduce the iteration count to $\tilde O(\sqrt{\mathrm{rank}(A)}\,L)$ by following a weighted central path in which each constraint carries its own positive weight, and the weights are re-computed as the algorithm moves. Their improved maximum-flow algorithm is an application of the same method.

Timeline. Karmarkar (1984) gave the first polynomial-time interior point method for linear programming. Renegar (1988) showed that path following with the logarithmic barrier needs $O(\sqrt m L)$ iterations. Nesterov and Nemirovskii (1994) showed that a universal self-concordant barrier yields $O(\sqrt n L)$ iterations, but that barrier is not known to be efficiently computable. Lee and Sidford (2014) achieved $\tilde O(\sqrt{\mathrm{rank}(A)}L)$ iterations, each reducible to $\tilde O(1)$ linear-system solves.

This mission covers the first half of that framework (§IV of the paper): the weighted central path, the weighted Newton step, and the centering theorem that shows a single step followed by re-weighting makes constant-factor progress.

Setting

Let $A\in\mathbb R^{m\times n}$, $b\in\mathbb R^m$, $c\in\mathbb R^n$, and consider the linear program

$$\min_{x\in\mathbb R^n:\ Ax\ge b} c^Tx .$$

The slack of a point $x$ is $s(x)=Ax-b$, and the interior is $S^0=\{x : Ax>b\}$, the points with all slacks strictly positive. For a path parameter $t$ and a vector of positive weights $w\in\mathbb R^m_{>0}$, the weighted penalized objective is

$$f_t(x,w)=t\,c^Tx-\sum_{i=1}^m w_i\log s(x)_i .$$

A pair $(x,w)$ is feasible if $x\in S^0$ and $w>0$.

Write $S_x=\mathrm{diag}(s(x))$, $W=\mathrm{diag}(w)$ and $\|v\|_M=\sqrt{v^TMv}$. The Newton step and the centrality are

$$\vec h_t(x,w)=\big(A^TS_x^{-1}WS_x^{-1}A\big)^{-1}\big(tc-A^TS_x^{-1}w\big),\qquad \delta_t(x,w)=\big\|\vec h_t(x,w)\big\|_{A^TS_x^{-1}WS_x^{-1}A}.$$

The matrix $A^TS_x^{-1}WS_x^{-1}A$ is the Hessian of $f_t$ in $x$, and $tc-A^TS_x^{-1}w$ is its gradient; $\delta_t(x,w)=0$ exactly when $x$ minimizes $f_t(\cdot,w)$.

For slacks $s$ and weights $w$ the projection matrix is $P_{S^{-1}A}(w)=W^{1/2}S^{-1}A(A^TS^{-1}WS^{-1}A)^{-1}A^TS^{-1}W^{1/2}$ and the slack sensitivity is

$$\gamma(s,w)=\max_{i\in[m]}\big\|W^{-1/2}\vec 1_i\big\|_{P_{S^{-1}A}(w)} .$$

A weight function (Definition 4) is a differentiable map $\vec g:\mathbb R^m_{>0}\to\mathbb R^m_{>0}$ from slacks to weights with constants $c_1$ (size, a bound on $\|\vec g(s)\|_1$), $c_\gamma\ge1$ (slack sensitivity, $\gamma(s,\vec g(s))\le c_\gamma$), $c_r\ge1$ (step consistency, two inequalities on the Jacobian $G'(s)$ of $\vec g$ that hold for every $r\ge c_r$), and uniformity $\|\vec g(s)\|_\infty\le2$.

Formalization targets

Goal: Theorem 5 (Centering with Weights), §IV.C

Let $\vec g$ be a weight function for $A$ with constants $c_1,c_\gamma,c_r$, let $x^{(old)}\in S^0$, $s^{(old)}=s(x^{(old)})$, and

$$x^{(new)}=x^{(old)}-\frac{1}{1+c_r}\,\vec h_t\big(x^{(old)},\vec g(s^{(old)})\big).$$

If $\delta_t(x^{(old)},\vec g(s^{(old)}))\le\frac{1}{100c_\gamma c_r^2}$, then $x^{(new)}\in S^0$ and

$$\delta_t\big(x^{(new)},\vec g(s^{(new)})\big)\le\Big(1-\frac{1}{4c_r}\Big)\delta_t\big(x^{(old)},\vec g(s^{(old)})\big).$$

The theorem is stated for every weight function, not for the specific one constructed in §V of the paper; that construction is the subject of a separate mission.

Milestone: Lemma 3 (Split Newton Step), §IV.B

For feasible $(x^{(old)},w^{(old)})$ and $r\ge0$, the split step $x^{(new)}=x^{(old)}-\frac1{1+r}\vec h_t$, $w^{(new)}=w^{(old)}+\frac r{1+r}W_{(old)}S_{(old)}^{-1}A\vec h_t$ satisfies, whenever $\delta_t\le\frac1{8\gamma}$,

$$\delta_t\big(x^{(new)},w^{(new)}\big)\le\frac{2}{1+r}\,\gamma\,\delta_t^2,$$

with $\gamma=\gamma(s(x^{(old)}),w^{(old)})$, and the new pair is feasible.

Milestone: Lemma 1, §IV.B

For feasible $(x,w)$ and $\alpha,t\ge0$:

$$\delta_{(1+\alpha)t}(x,w)\le(1+\alpha)\delta_t(x,w)+\alpha\sqrt{\|w\|_1}.$$

Significance

Theorem 5 is the centering half of the weighted path-following method. Combined with Lemma 1, it shows that the path parameter can be doubled, while staying close to the weighted central path, in a number of steps of the form (5) controlled by $c_\gamma$, $c_r$ and $\sqrt{c_1}$. The paper then constructs (§V, Theorem 1) a weight function with $c_1=2\,\mathrm{rank}(A)$, $c_\gamma=2$ and $c_r$ logarithmic in $m/\mathrm{rank}(A)$, which yields the $\tilde O(\sqrt{\mathrm{rank}(A)})$ iteration bound. The theorem isolates exactly which properties of a weighting scheme are needed, so it applies to any weight function satisfying Definition 4.

The FOCS extended abstract states these results without proofs; the proofs are in the arXiv full version (arXiv:1312.6677). The results are proved on paper. No machine-checked formalization of weighted path following, or of the Lee–Sidford framework, is known. A formal proof would check the constants $\frac1{100}$, $\frac1{4}$, $\frac18$ and $\frac2{1+r}$ as stated in the extended abstract, and would produce reusable Lean infrastructure for Newton steps of barrier functions with explicit matrix formulas.

Difficulty

The standard analysis of Newton's method on a self-concordant barrier gives quadratic convergence of centrality for a fixed barrier. Here the barrier changes during the step: the weights are reset to $\vec g(s(x^{(new)}))$, so the new centrality is measured with respect to a different Hessian and a different gradient. The obvious argument, analysing the step at fixed weights and then treating the re-weighting as a small perturbation, does not give a contraction factor independent of $m$: without control of how $\vec g$ reacts to changes in the slacks, the re-weighting can undo the progress of the step. The step-consistency conditions of Definition 4 are the only hypotheses that control this reaction, and they are pointwise bounds on the Jacobian of $\vec g$, while the step moves the slacks by a finite amount.

Formalization scope

Vectors are Fin n → ℝ and Fin m → ℝ, matrices Matrix (Fin m) (Fin n) ℝ, and products are Matrix.mulVec and dotProduct. $S^{-1}$ is the diagonal matrix of reciprocals, $W^{\pm1/2}$ the diagonal matrices of $\sqrt{w_i}^{\pm1}$, and $\|v\|_M=\sqrt{v^TMv}$. The Newton step and centrality are defined by the explicit formulas (3) and (4), not by derivatives of $f_t$; the centrality uses the Hessian-norm form of (4). The Jacobian $G'(s)$ is the Fréchet derivative fderiv ℝ g s, and $\|\cdot\|_\infty$ is Mathlib's sup norm.

Conventions fixed where the paper is silent:

1. Full column rank. Every theorem assumes A.rank = n. The paper uses $(A^TS_x^{-1}WS_x^{-1}A)^{-1}$ without comment; the inverse exists for positive slacks and weights exactly when $A$ has full column rank. Lean's matrix inverse is $0$ on singular matrices, which would make $\vec h_t$, $\delta_t$ and $\gamma$ vanish and every statement trivially true; the rank hypothesis rules this trivializing reading out.
2. Size as an upper bound. Definition 4's "$c_1(\vec g)=\|\vec g(s)\|_1$" is read as $\|\vec g(s)\|_1\le c_1$ for all $s>0$ (the paper's own weight function reports a $c_1$ above its $\ell_1$ norm). $c_1$ does not enter Theorem 5.
3. Operator norm. Step consistency's first bullet is written as $\|(I+r^{-1}G^{-1}G'S)y\|_{G(s)}\le\|y\|_{G(s)}$ for all $y$.
4. Lemma 3's $r$ ranges over $r\ge0$, and $\gamma(x,w)$ means $\gamma(s(x),w)$.
5. Feasibility of the new point is part of the conclusion of Lemma 3 and Theorem 5, since the page's conclusion evaluates quantities defined only on the interior.
6. Maximum over $[m]$ is a supremum over Fin m (attained for $m\ge1$, equal to $0$ for $m=0$).
7. The path parameter $t$ is unrestricted in Theorem 5 and Lemma 3, as on the page; Lemma 1 assumes $t\ge0$ as the page does.

A complete development needs basic facts about weighted norms and the projection matrix $P_{S^{-1}A}(w)$, spectral comparison of the matrices $A^TS^{-1}WS^{-1}A$ for nearby slacks and weights, and calculus for vector-valued maps on the positive orthant. The weighted-norm and projection-matrix material is reusable for any interior point analysis. Proofs of the milestones, alternative arguments, and sharper constants are welcome.

Selected references

• Y. T. Lee, A. Sidford, Path Finding Methods for Linear Programming: Solving Linear Programs in Õ(√rank) Iterations and Faster Algorithms for Maximum Flow, FOCS 2014, pp. 424–433. https://doi.org/10.1109/FOCS.2014.52
• Y. T. Lee, A. Sidford, Path Finding I: Solving Linear Programs with Õ(√rank) Linear System Solves, arXiv:1312.6677, 2013. https://arxiv.org/abs/1312.6677
• J. Renegar, A polynomial-time algorithm, based on Newton's method, for linear programming, Mathematical Programming 40, 1988, pp. 59–93. https://doi.org/10.1007/BF01580724
• N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica 4, 1984, pp. 373–395. https://doi.org/10.1007/BF02579150
• Y. Nesterov, A. Nemirovskii, Interior-Point Polynomial Algorithms in Convex Programming, SIAM, 1994. https://doi.org/10.1137/1.9781611970791

Motivation

Newton's method is the standard second-order algorithm for unconstrained minimization, but without safeguards it has no global guarantee: far from a minimizer the Newton step can increase the objective, and at a point where the Hessian is indefinite the step can head for a saddle point or a maximum. The usual repairs (line search, trust regions, Levenberg–Marquardt damping) come with convergence proofs, but for nonconvex objectives those proofs typically give no rate at all, or only the rate of the gradient method.

Nesterov and Polyak (Math. Program. 108 (2006) 177–205) proposed to regularize the second-order Taylor model of the objective with a cubic term and to take as the next iterate a global minimizer of the regularized model. They showed that the resulting method has a global worst-case rate of convergence to points satisfying the second-order necessary conditions, for every objective with a Lipschitz continuous Hessian and without any convexity. That rate, $O(k^{-2/3})$ for the gradient norm, is better than the $O(k^{-1/2})$ of the gradient method. It became the reference point for the complexity theory of nonconvex second-order optimization: adaptive variants (Cartis, Gould and Toint, Math. Program. 127 (2011) 245–295) and lower bounds showing that $O(\epsilon^{-3/2})$ iterations are optimal among second-order methods (Carmon, Duchi, Hinder and Sidford, Math. Program. 184 (2020) 71–120) are stated against it.

This mission formalizes the general convergence result of that paper, Theorem 1 of Section 3, together with the properties of the cubic step from Section 2 on which it rests.

Setting

Let $F \subseteq \mathbb{R}^n$ be a closed convex set with nonempty interior, and let $f$ be twice differentiable on $F$ with gradient $f'(x)$ and Hessian $f''(x)$. A starting point $x_0 \in \operatorname{int} F$ is fixed, and $F$ is assumed to contain the level set $\mathcal{L}(f(x_0)) = \{x \in \mathbb{R}^n : f(x) \le f(x_0)\}$ in its interior. Assumption 1: the Hessian is Lipschitz continuous on $F$ in the spectral norm, $\|f''(x) - f''(y)\| \le L\|x - y\|$ for all $x, y \in F$, with $L > 0$.

For a parameter $M > 0$ the cubic model of $f$ at $x$ is

$$m_{M,x}(y) = \langle f'(x), y - x\rangle + \tfrac12 \langle f''(x)(y - x), y - x\rangle + \tfrac{M}{6}\|y - x\|^3 .$$

The cubic-regularized Newton step $T_M(x)$ is any global minimizer of $m_{M,x}$ over $\mathbb{R}^n$; it exists because the model is continuous and coercive. Write $r_M(x) = \|x - T_M(x)\|$ and $\bar f_M(x) = f(x) + \min_y m_{M,x}(y)$.

The cubic regularization of Newton method (3.3) fixes $L_0 \in (0, L]$, starts at $x_0$ and, for $k \ge 0$, chooses $M_k \in [L_0, 2L]$ such that $f(T_{M_k}(x_k)) \le \bar f_{M_k}(x_k)$, then sets $x_{k+1} = T_{M_k}(x_k)$. The choice $M_k = L$ always passes the test.

Write $\lambda_n(A)$ for the smallest eigenvalue of a symmetric matrix $A$. The measure of local optimality is

$$\mu_M(x) = \max\Big\{ \sqrt{\tfrac{2}{L + M}\,\|f'(x)\|},\ -\tfrac{2}{2L + M}\,\lambda_n(f''(x)) \Big\}.$$

It is nonnegative and vanishes exactly when $f'(x) = 0$ and $f''(x) \succeq 0$.

Formalization targets

Goal: Theorem 1, inequality (3.4)

If $f(x) \ge f^*$ for all $x \in F$, then every run of method (3.3) satisfies, for every $k \ge 1$,

$$\min_{1 \le i \le k} \mu_L(x_i) \le \frac{8}{3}\cdot\left(\frac{3\,(f(x_0) - f^*)}{2k\cdot L_0}\right)^{1/3}.$$

The constant $8/3$ and the exponent $1/3$ are the paper's; the statement holds for every admissible choice of the parameters $M_k$ and of the global minimizers $x_{k+1}$.

Milestones, in attack order

1. Lemma 1 (2.2): $\|f'(y) - f'(x) - f''(x)(y - x)\| \le \tfrac12 L\|y - x\|^2$ on $F$.
2. Eq. (2.5): $f'(x) + f''(x)(T - x) + \tfrac12 M\|T - x\|(T - x) = 0$ for $T = T_M(x)$.
3. Proposition 1 (2.7): $f''(x) + \tfrac12 M r_M(x) I \succeq 0$.
4. Lemma 2 (2.8): $\langle f'(x), x - T_M(x)\rangle \ge 0$ when $f(x) \le f(x_0)$.
5. Lemma 4 (2.11): $f(x) - \bar f_M(x) \ge \tfrac{M}{12} r_M(x)^3$.
6. Lemma 4 (2.12): for $M \ge L$, $T_M(x) \in F$ and $f(T_M(x)) \le \bar f_M(x)$.
7. Lemma 3 (2.9): $\|f'(T_M(x))\| \le \tfrac12(L + M) r_M(x)^2$ when $T_M(x) \in F$.
8. Lemma 5: $\mu_M(T_M(x)) \le r_M(x)$.
9. Theorem 1, first claim: $\sum_{i \ge 0} r_{M_i}(x_i)^3 \le \tfrac{12}{L_0}(f(x_0) - f^*)$.
10. Theorem 1, second claim: $\lim_{i\to\infty} \mu_L(x_i) = 0$.

Significance

Inequality (3.4) is a global, dimension-free complexity bound for reaching approximate second-order stationarity. It controls both the gradient norm, $\min_{1\le i\le k}\|f'(x_i)\| = O(k^{-2/3})$, and the most negative curvature, $\max\{0, -\lambda_n(f''(x_i))\} = O(k^{-1/3})$, along the best iterate, from a single scalar potential $f(x_0) - f^*$. The second claim of Theorem 1 gives the asymptotic counterpart: every limit point satisfies the second-order necessary conditions. Section 4 of the paper derives its faster rates for star-convex and gradient-dominated functions from the same Section 2 lemmas.

The result is proved on paper and widely cited; to our knowledge no machine-checked proof of it or of the Section 2 lemmas exists. A formalization adds a checked statement of the method with its exact constants, and reusable facts about global minimizers of cubic models (Proposition 1 in particular) that the companion missions on star-convex, gradient-dominated and locally quadratic convergence also rely on.

Difficulty

Most steps are short inequalities, but two are not. Proposition 1 is a statement about a global minimizer of a nonconvex function: the first- and second-order conditions of a local minimizer give only $f''(x) + \tfrac12 M r I + \tfrac{M}{2r}(T - x)(T - x)^\top \succeq 0$, which is weaker. The natural first attempt, "take the second-order optimality condition of the model at $T$", therefore fails. The paper proves it in Section 5.1 through a one-dimensional dual characterization of the minimizer.

The second is Lemma 2's second claim, used for (2.12): showing that $T_M(x)$ stays in $F$ requires a boundary argument along the segment from $x$ to $T_M(x)$, since the Taylor bounds are only available inside $F$. The remaining work is calculus in $\mathbb{R}^n$: the integral form of Taylor's theorem for the gradient under a Lipschitz Hessian, and eigenvalue perturbation for the second entry of $\mu$.

Formalization scope

The space is EuclideanSpace ℝ (Fin n) for arbitrary n : ℕ. The gradient and Hessian are maps g and H with HasGradientAt f (g x) x and HasFDerivAt g (H x) x at every x ∈ F. At boundary points of $F$ this asks for two-sided derivatives, a mild strengthening of "twice differentiable on $F$". The Lipschitz condition uses the operator norm, which is the spectral norm. $T_M(x)$ is represented by the predicate IsCubicStep (global minimizer of cubicModel), and every lemma is stated for every such minimizer. The run predicate IsCubicNewtonRun is 0-based. It writes $\bar f_{M_k}(x_k)$ as $f(x_k)$ plus the model value at $x_{k+1}$, which is the minimum because $x_{k+1}$ attains it. $\lambda_n$ is lamMin, the Rayleigh-quotient infimum over the unit sphere, which equals the smallest eigenvalue for the (symmetric) Hessian. The lower bound $f^*$ is required on $F$ only. The minimum over $1 \le i \le k$ is written as the existence of an index attaining the bound.

A stationary point of the cubic model is not an admissible step, and the run must keep the test $M_k \in [L_0, 2L]$ and the acceptance test. Replacing the step by any point with $f(x_{k+1}) \le f(x_k)$ makes the goal false, and dropping the square root in $\mu_M$ makes Lemma 5 false. The statements rule out all three. Lemma 5 carries the hypothesis $T_M(x) \in F$, which its printed proof uses and which holds at every iterate.

A complete development needs the Taylor bounds (2.2)–(2.3) for vector-valued derivatives on convex sets, and first- and second-order optimality for the cubic model. It also needs a proof of Proposition 1 (Section 5.1 or any other correct argument) and eigenvalue perturbation via Rayleigh quotients. The cubic-model lemmas and Proposition 1 are reusable across the whole series. Proofs of any milestone, alternative proofs of Proposition 1, and general Mathlib-level lemmas about Rayleigh quotients are welcome.

Selected references

• Yu. Nesterov and B. T. Polyak, Cubic regularization of Newton method and its global performance, Mathematical Programming, Ser. A 108 (2006) 177–205. https://doi.org/10.1007/s10107-006-0706-8
• C. Cartis, N. I. M. Gould and Ph. L. Toint, Adaptive cubic regularisation methods for unconstrained optimization. Part I: motivation, convergence and numerical results, Mathematical Programming 127 (2011) 245–295. https://doi.org/10.1007/s10107-009-0286-5
• Y. Carmon, J. C. Duchi, O. Hinder and A. Sidford, Lower bounds for finding stationary points I, Mathematical Programming 184 (2020) 71–120. https://doi.org/10.1007/s10107-019-01406-y
• Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9