All missions

Motivation

Every fast integer-multiplication algorithm in the literature is stated for the multitape Turing machine. The algorithms are built from a small set of standard subroutines whose costs are usually quoted as "well known":

• linear-time addition;
• sorting by merging on tapes;
• fast matrix transposition;
• a crude $O(n^{1+\delta})$ multiplier, used for the small multiplications inside fixed-point arithmetic.

Harvey–van der Hoeven (2021) use all of these in §2.1, §2.3 and §4–§5 of their $O(n\log n)$ paper. They cite Brent–Zimmermann for the arithmetic, Knuth vol. 3 for merge sort, and Bostan–Gaudry–Schost for transposition.

This mission formalizes that toolkit in the shared machine model IntMul_MultitapeModel. Its goal is the classical Schönhage–Strassen bound $\mathsf M(n)=O(n\log n\log\log n)$. The toolkit is exactly what is missing before the recursive step of the companion mission, Harvey–van der Hoeven Proposition 5.4, can be decomposed. Proposition 5.4 is the last open link on that mission's main line.

Timeline (multitape Turing model).

• Folklore: schoolbook multiplication in $O(n^2)$; addition in $O(n)$.
• 1962: Karatsuba–Ofman, $O(n^{\log_2 3})$.
• 1963–1966: Toom and Cook, $O(n^{1+\epsilon})$ for every $\epsilon>0$.
• 1971: Schönhage–Strassen, $O(n\log n\log\log n)$.
• 1973 (2nd ed. 1998): Knuth, TAOCP vol. 3 §5.4, merge sorting on tapes.
• 2007: Bostan–Gaudry–Schost, Appendix: transposing an $m\times k$ matrix with $N$ bits in total in $O(N\log\min(m,k))$ on a multitape machine.
• 2019/2021: Harvey–van der Hoeven, $O(n\log n)$, using all of the above.

Setting

The machine model, input and output conventions, and the time-bound predicate $\mathrm{MulTimeBound}$ are those of IntMul_MultitapeModel. That model follows Montanaro's lecture notes:

• $k\ge2$ one-way tapes, with a read-only input tape and a separate output tape;
• $\triangleright$ appears only in cell $0$ of each tape;
• $\mathrm{START}\ne\mathrm{HALT}$, and the halting state freezes the configuration.

For subroutines whose input is not of the form $x\#y$, the new definitions file IntMul_MultitapeWords starts the machine on an arbitrary word over $\{0,1,\#\}$. It also provides the encodings

• $\mathrm{bits}(x)$, a bit string written as a word;
• $u_1\#u_2\#\cdots\#u_m$, a list of words joined by separators.

Formalization targets

Goal: Schönhage–Strassen

$\mathrm{MulTimeBound}(n\mapsto n\ln n\ln\ln n)$: a single multitape machine multiplies $n$-bit integers for every $n\ge1$ in worst-case time $O(n\log n\log\log n)$.

Milestones

1. Schoolbook multiplication: $\mathrm{MulTimeBound}(n^2)$.
2. Karatsuba–Ofman: $\mathrm{MulTimeBound}(n^{\log_2 3})$.
3. Linear-time addition: on input $x\#y$ with $|x|=|y|=n$, output $\operatorname{bin}_{n+1}(\operatorname{val}x+\operatorname{val}y)$ within $c(n+1)$ steps.
4. Merge sort on tapes:
   • Input: $m$ records, each a key of $\ell$ bits and a payload of $q$ bits, written as $k_1\#p_1\#k_2\#p_2\#\cdots$.
   • Output: the records stably sorted by key value, in the same format.
   • Time: $c\,(N+1)(\lceil\log_2 m\rceil+1)$, where $N$ is the input length.
5. Matrix transposition:
   • Input: an $m\times k$ matrix ($m,k\ge1$) with entries of $\ell\ge1$ bits, in row-major order. Entries are separated by $\#$ and rows by $\#\#$.
   • Output: the transpose, in the same format.
   • Time: $c\,(N+1)(\lceil\log_2\min(m,k)\rceil+1)$.

Formalization scope

Constants may depend only on the machine. All time bounds count exact steps of one fixed machine in the shared model. Building machines by composing smaller ones (subroutine calls, scratch tapes, recursion) is the solvers' business; any reusable infrastructure for it is welcome as published lemmas.

Selected references

• A. Schönhage, V. Strassen, Schnelle Multiplikation großer Zahlen, Computing 7 (1971), 281–292.
• A. Karatsuba, Yu. Ofman, Multiplication of multidigit numbers on automata, Soviet Physics Doklady 7 (1963), 595–596.
• D. E. Knuth, The Art of Computer Programming, Vol. 3: Sorting and Searching, 2nd ed., Addison-Wesley, 1998, §5.4.
• A. Bostan, P. Gaudry, É. Schost, Linear recurrences with polynomial coefficients and application to integer factorization and Cartier–Manin operator, SIAM J. Comput. 36 (2007), 1777–1806, Appendix.
• R. P. Brent, P. Zimmermann, Modern Computer Arithmetic, Cambridge University Press, 2011, Ch. 1.
• D. Harvey, J. van der Hoeven, Integer multiplication in time $O(n\log n)$, Ann. of Math. 193 (2021), §2.1.
• A. Montanaro, Computational Complexity, lecture notes, §3–§4.

Motivation

Linear convergence of first order methods is classically tied to strong convexity. Many problems in data fitting, machine learning and control are not strongly convex, yet gradient methods are observed to converge linearly on them: least squares with a rank-deficient matrix, the dual of a linearly constrained quadratic program, $f(x) = g(Ax)$ with $g$ strongly convex and $A$ singular. Their optimal sets are not single points, so strong convexity fails, and some weaker property of $f$ has to explain the observed rates.

I. Necoara, Yu. Nesterov and F. Glineur (arXiv:1504.06298v4, 2016; Math. Program. 175 (2019)) introduce a chain of relaxations of strong convexity — quasi-strong convexity, quadratic under-approximation, quadratic gradient growth, quadratic functional growth — and prove linear rates for several first order methods under each. Among these results, Theorem 13 singles out one condition: for the projected gradient method with constant step size, linear convergence (in the sense made precise below) holds if and only if $f$ has quadratic functional growth. This mission formalizes that equivalence and the two results it rests on, Theorem 5 and Theorem 12.

Related conditions appear in Łojasiewicz's gradient inequality, in Luo and Tseng's error bounds (1993), in the Polyak–Łojasiewicz condition studied by Karimi, Nutini and Schmidt (2016), and in Drusvyatskiy and Lewis's equivalence of quadratic growth and error bounds (2018).

Setting

Work in $\mathbb{R}^n$ with the Euclidean inner product $\langle u, v\rangle = u^\top v$ and norm $\|\cdot\|$. Problem (P) is

$$f^* = \min_{x \in X} f(x),$$

with $X \subseteq \mathbb{R}^n$ closed and convex and $f$ convex, with gradient Lipschitz on $X$ with constant $L_f > 0$:

$$\|\nabla f(x) - \nabla f(y)\| \le L_f \|x - y\| \qquad \forall x, y \in X. \tag{1}$$

The optimal set $X^* = \{x \in X : f(x) \le f(y)\ \forall y \in X\}$ is assumed nonempty. The projection $[u]_S$ of $u$ onto a nonempty closed convex set $S$ is the nearest point of $S$ to $u$. For $x \in X$ write $\bar x = [x]_{X^*}$.

The projected gradient step from $x$ is $x^+ = [x - \tfrac{1}{L_f}\nabla f(x)]_X$, and $\bar x^+ = [x^+]_{X^*}$. The projected gradient method (GM) starts at $x^0 \in X$ and iterates $x^{k+1} = [x^k - \alpha_k \nabla f(x^k)]_X$ for $k \ge 0$.

$f$ has quadratic functional growth with constant $\kappa_f > 0$, written $f \in \mathcal F_{L_f,\kappa_f}$, when

$$f(x) - f^* \ge \frac{\kappa_f}{2}\,\|x - \bar x\|^2 \qquad \forall x \in X. \tag{22}$$

The condition number is $\mu_f = \kappa_f / L_f$.

Formalization targets

Goal: Theorem 13 (p. 23)

Under the standing assumptions of (P):

1. if $f$ satisfies (22) with constant $\kappa_f > 0$, then for every $x \in X$

$$\|x^+ - \bar x^+\|^2 \le \frac{1}{1 + \mu_f}\,\|x - \bar x\|^2 ;$$

2. if for some $0 < \beta < 1$ the step contracts the distance to the optimal set,

$$\|x^+ - \bar x^+\| \le \beta\,\|x - \bar x\| \qquad \forall x \in X,$$

then $f$ satisfies (22) with constant $L_f(1-\beta)^2$.

Together these say that a uniform one-step contraction of $\operatorname{dist}(\cdot, X^*)$ by the gradient step with step size $1/L_f$ is equivalent to quadratic functional growth.

Milestones

• (28): $f(x^+) \le f(x) - \tfrac{L_f}{2}\|x^+ - x\|^2$;
• (26): under the contraction hypothesis, $(1-\beta)\|x - \bar x\| \le \|x - x^+\|$;
• Theorem 5: contraction implies (22) with $\kappa_f = L_f(1-\beta)^2$;
• the one-step inequality $\|x^{k+1} - x\|^2 \le \|x^k - x\|^2 - 2\alpha_k(f(x^{k+1}) - f(x))$ for $0 < \alpha_k \le 1/L_f$ and all $x \in X$;
• (52): under (22), $\|x^{k+1} - \bar x^{k+1}\|^2 \le \tfrac{1}{1+\kappa_f\alpha_k}\|x^k - \bar x^k\|^2$;
• Theorem 12: along (GM) with $\alpha_k = 1/L_f$, $\|x^k - \bar x^k\|^2 \le (1+\mu_f)^{-k}\|x^0 - \bar x^0\|^2$.

A companion item states the function-value rate (53), $f(x^k) - f^* \le \tfrac{L_f\|x^0 - \bar x^0\|^2}{2}(1+\mu_f)^{-(k-1)}$ for $k \ge 1$.

Significance

The result. Theorem 13 identifies quadratic functional growth as the exact condition, in the paper's hierarchy, for linear convergence of projected gradient: every stronger class (strong, quasi-strong convexity, quadratic gradient growth, quadratic under-approximation) gives linear convergence through it, and no condition weaker than (22) can. It also gives explicit constants in both directions: rate $(1+\mu_f)^{-1}$ per step from growth, and growth constant $L_f(1-\beta)^2$ from contraction factor $\beta$.

Formalizing it. The results are proved in the paper; to the knowledge of this mission none of them has a machine-checked proof. The work is to formalize the known proofs: the descent inequality (28) and the variational inequality of the projection onto a closed convex set, the one-step inequality of the projected gradient method, and the two directions of Theorem 13. The projection lemmas and the one-step inequality are reusable for any analysis of projected gradient on convex sets.

Difficulty

The ⇒ direction is a contraction argument along one step; its difficulty is the projection calculus: the variational inequality characterizing $[u]_X$, applied with $u = x^k - \alpha_k\nabla f(x^k)$, and the descent lemma (2), which must be derived from (1) on the convex set $X$ only, since $f$ need not be smooth off $X$. The nearest point $\bar x^{k+1}$ of $x^{k+1}$ differs from $\bar x^k$; the argument must compare distances to two different optimal points.

The ⇐ direction is not a statement about one run of the method: it needs the contraction hypothesis at every feasible point. A version with a multi-step rate along runs ($\operatorname{dist}(x^k, X^*) \le C q^k$) is not what the paper proves, and the one-step hypothesis cannot be recovered from it without extra work.

Formalization scope

Lean represents $\mathbb{R}^n$ as EuclideanSpace ℝ (Fin n) and $\nabla f$ as gradient f. $f$ is a function on all of $\mathbb{R}^n$ that is differentiable at every point of $X$; only its values and gradients on $X$ enter. The standing assumptions of p. 3 are explicit hypotheses of every theorem: $X$ closed and convex, $f$ convex on $X$, (1) with $L_f > 0$, and a named minimiser $x^\star \in X^*$; the paper's "simple" (cheap projection) is not a mathematical hypothesis and is dropped, and "closed" for $f$ is implied by continuity on $X$. The optimal value is $f(x^\star)$, or $f(\bar x)$, never an infimum. Projections are predicates (IsNearest), never chosen points, and every statement quantifies over all nearest points; they exist and are unique on nonempty closed convex sets. Iterates are indexed from $k = 0$. The page prints "for $k \ge 1$" in (GM); this slip is not copied. Theorem 12's "converges linearly to some optimal point" is formalized as the rate (51) only, since convergence of the iterates themselves is not proved on the page. In the goal, part 1 is stated in the squared form of (52).

The formalization does not define the projection by a choice function, does not allow an empty optimal set (which would make every growth inequality vacuous), and does not read the gradient off the set where $f$ is assumed differentiable.

Needed infrastructure: the variational characterization of the Euclidean projection onto a closed convex set, the descent lemma on a convex set, closedness and convexity of $X^*$, and existence of nearest points. Contributions of these lemmas, of the milestones in any order, and of the goal are welcome.

Selected references

• I. Necoara, Yu. Nesterov, F. Glineur, Linear convergence of first order methods for non-strongly convex optimization, arXiv:1504.06298v4, 2016; Math. Program. 175 (2019) 69–107. https://arxiv.org/abs/1504.06298
• Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9
• Z.-Q. Luo, P. Tseng, Error bounds and convergence analysis of feasible descent methods: a general approach, Ann. Oper. Res. 46 (1993) 157–178. https://doi.org/10.1007/BF02096261
• H. Karimi, J. Nutini, M. Schmidt, Linear convergence of gradient and proximal-gradient methods under the Polyak–Łojasiewicz condition, ECML PKDD 2016. https://arxiv.org/abs/1608.04636
• D. Drusvyatskiy, A. S. Lewis, Error bounds, quadratic growth, and linear convergence of proximal methods, Math. Oper. Res. 43 (2018) 919–948. https://arxiv.org/abs/1602.06661

Motivation

Many first order methods used in large-scale convex optimization do not take an exact projected gradient step. Proximal point iterations, random or cyclic coordinate descent, extragradient methods and matrix splitting methods all produce iterates that behave like a projected gradient step corrupted by an error which is small relative to the step itself. Luo and Tseng (Ann. Oper. Res. 1993) grouped these schemes under the name feasible descent methods and proved that they converge linearly when the problem satisfies an error bound, a condition relating the distance to the optimal set to the size of the projected gradient residual. Wang and Lin (JMLR 2014) gave global iteration complexity bounds for the same family under the same kind of error bound.

Necoara, Nesterov and Glineur (arXiv:1504.06298v4, published in Math. Program. 2019) study a chain of conditions weaker than strong convexity under which first order methods still converge linearly. The weakest of them that the paper uses for algorithms is quadratic functional growth: the objective grows at least quadratically in the distance to the optimal set. Their Theorem 15 shows that the whole feasible descent family converges linearly in function values under quadratic functional growth alone. This mission formalizes that theorem and the steps of its proof.

Setting

Let $\mathbb R^n$ carry the Euclidean inner product $\langle u,v\rangle=u^\top v$ and the norm $\|u\|$. For a set $S$ and a point $u$, a nearest point $p=[u]_S$ is a point $p\in S$ with $\|u-p\|\le\|u-z\|$ for every $z\in S$.

Problem (P) is $f^*=\min_{x\in X}f(x)$, where

1. $X\subseteq\mathbb R^n$ is closed and convex;
2. $f$ is convex on $X$ and differentiable at every point of $X$, with gradient $\nabla f$ Lipschitz on $X$ with constant $L_f>0$: $\|\nabla f(x)-\nabla f(y)\|\le L_f\|x-y\|$ for all $x,y\in X$ (inequality (1) of the paper);
3. the optimal set $X^*=\{x\in X: f(x)\le f(y)\ \forall y\in X\}$ is nonempty; $f^*$ is the value of $f$ on $X^*$.

The function $f$ has quadratic functional growth with constant $\kappa_f>0$ (Definition 4, inequality (22)) if, for every $x\in X$ and its nearest point $\bar x=[x]_{X^*}$,

$$f(x)-f^*\ \ge\ \frac{\kappa_f}{2}\,\|x-\bar x\|^2 .$$

The class $\mathcal F_{L_f,\kappa_f}(X)$ consists of the convex functions satisfying (1) and (22).

A run of the feasible descent method (FDM) with constants $\beta,L,\bar L_f>0$ consists of stepsizes $\alpha_k$, error vectors $e^k$ and iterates $x^k$ ($k\ge0$) with $x^0\in X$ and, for every $k$,

$$x^{k+1}=\big[x^k-\alpha_k\nabla f(x^k)+e^k\big]_X,\qquad \|e^k\|\le\beta\|x^{k+1}-x^k\|,\qquad f(x^{k+1})\le f(x^k)-\frac L2\|x^{k+1}-x^k\|^2,\qquad \alpha_k\ge \bar L_f^{-1}.$$

The errors are part of the run: any vectors meeting the two conditions are allowed. With $\alpha_k=1/L_f$, $e^k=0$ and $L=L_f$ a run is the projected gradient method (GM) of the paper.

Formalization targets

Goal: Theorem 15

For $f\in\mathcal F_{L_f,\kappa_f}(X)$ and every run of (FDM), for all $k\ge0$,

$$f(x^k)-f^*\ \le\ \left(\frac{1}{1+\dfrac{L\kappa_f}{4(L_f+\bar L_f+\beta\bar L_f)^2}}\right)^{k}\big(f(x^0)-f^*\big). \tag{64}$$

The rate is the one printed in the paper; the statement fixes no numerical values of the constants.

Milestones, in the order of the proof

1. (65): the optimality condition of the projection step, $\langle x^{k+1}-x^k+\alpha_k\nabla f(x^k)-e^k,\,x-x^{k+1}\rangle\ge0$ for all $x\in X$.
2. The chain after (65): $f(x^{k+1})-f(\bar x^{k+1})\le(L_f+\bar L_f+\beta\bar L_f)\|x^{k+1}-x^k\|\,\|x^{k+1}-\bar x^{k+1}\|$ with $\bar x^{k+1}=[x^{k+1}]_{X^*}$.
3. (66): $f(x^{k+1})-f(\bar x^{k+1})\le\dfrac{2(L_f+\bar L_f+\beta\bar L_f)^2}{\kappa_f}\|x^{k+1}-x^k\|^2$.
4. The one-step contraction: $f(x^{k+1})-f^*\le\Big(1+\dfrac{L\kappa_f}{4(L_f+\bar L_f+\beta\bar L_f)^2}\Big)^{-1}(f(x^k)-f^*)$.

Significance

Theorem 15 replaces the error bound assumption of Luo–Tseng and Wang–Lin by quadratic functional growth, a condition stated purely in terms of function values. Since the paper shows (Theorems 6 and 7) that, for convex $f$ with Lipschitz gradient, the error bound and quadratic functional growth are equivalent up to constants, the theorem gives a direct route to linear convergence for every scheme known to be a feasible descent method, with an explicit rate in the three constants $L$, $L_f$, $\bar L_f$ and the error ratio $\beta$. The paper also notes (p. 30) that linear convergence of $x^k$ to a point of $X^*$ follows from the function-value rate and (22).

The result is proved in the paper. No machine-checked version is known to exist: the prior-art search found no formalization of feasible descent methods, of the Luo–Tseng framework, or of linear convergence under quadratic functional growth on a constrained set. A formal proof would make the general feasible descent template available for instantiation by concrete methods (coordinate descent, proximal point), each of which then needs only to verify the two run conditions.

Difficulty

The obvious argument for projected gradient methods compares $x^{k+1}$ with a fixed minimizer and uses strong convexity to contract the distance; here neither is available. There is no strong convexity, $X^*$ need not be a singleton, and there is no upper bound on the stepsize, so the usual sufficient decrease estimate of the gradient method cannot be derived and is instead an assumption of the run. The error $e^k$ is only controlled relative to the step $x^{k+1}-x^k$, not absolutely, and the stepsize is only bounded below, so any estimate has to be uniform in $\alpha_k$ and has to measure progress against the moving nearest point $\bar x^{k+1}$ of the optimal set rather than a fixed minimizer.

Formalization scope

The ambient space is EuclideanSpace ℝ (Fin n); $f$ is a function on all of $\mathbb R^n$, and only its values and gradients (Mathlib's gradient) at points of $X$ enter. The nearest point $[u]_S$ is the predicate IsNearest S u p, never a choice function, so a run of (FDM) is any pair of sequences $(x^k)$, $(e^k)$ with stepsizes $(\alpha_k)$ satisfying the predicate IsFDMRun. Statements about $\bar x^{k+1}$ hold for every nearest point; since $X^*$ is closed and convex the nearest point is unique. The optimal set is nonempty because a minimizer $x^*$ is a hypothesis, and $f^*$ is $f(x^*)$, not an infimum. Sequences are indexed from $0$.

Standing assumptions of p. 3 are hypotheses: $X$ closed and convex, $f$ convex on $X$, differentiable on $X$, (1) with $L_f>0$, $X^*$ nonempty. The word "simple" (projection is cheap) is not a mathematical condition and is dropped; closedness of $f$ follows from continuity on $X$. The class hypothesis $f\in\mathcal F_{L_f,\kappa_f}$ is unbundled into convexity, (1) and (22) with $\kappa_f>0$. The constants satisfy $\beta,L,\bar L_f>0$, as on the page, and no upper bound on $\alpha_k$ is imposed. The milestone (65) drops every hypothesis it does not need (it uses only convexity of $X$), and the chain after (65) does not assume (22).

Trivializing formalizations are ruled out: the projection is not a choice that could return a junk point, $X^*$ is never empty, gradients are only evaluated at points of $X$ where $f$ is differentiable, and the run conditions are satisfiable by non-stationary sequences (for $f(x)=\frac12\|x\|^2$ on $X=\mathbb R^n$, $\alpha_k=\frac12$, $e^k=0$, $x^k=2^{-k}x^0$).

A complete development needs the variational characterization of Euclidean projections onto convex sets, the first order characterization of convexity for a function differentiable on a convex set, existence of nearest points in closed convex nonempty sets of $\mathbb R^n$, and an induction on the one-step contraction. The first three are reusable well beyond this mission. Proofs of the milestones, and of instances of (FDM) for concrete methods, are welcome.

Selected references

• I. Necoara, Yu. Nesterov, F. Glineur, Linear convergence of first order methods for non-strongly convex optimization, arXiv:1504.06298v4, 2016; Mathematical Programming 175 (2019) 69–107. https://arxiv.org/abs/1504.06298, https://doi.org/10.1007/s10107-018-1232-1
• Z.-Q. Luo, P. Tseng, Error bounds and convergence analysis of feasible descent methods: a general approach, Annals of Operations Research 46 (1993) 157–178. https://doi.org/10.1007/BF02096261
• P.-W. Wang, C.-J. Lin, Iteration complexity of feasible descent methods for convex optimization, Journal of Machine Learning Research 15 (2014) 1523–1548. https://jmlr.org/papers/v15/wang14a.html

Three-operator monotone inclusions

Many problems in convex optimization and variational analysis have the form of a monotone inclusion with three pieces of structure: a nonsmooth part that is only accessible through its resolvent (a subdifferential of a proximable function, or a normal cone of a constraint set), a smooth convex part whose gradient is Lipschitz, and a monotone but non-gradient part such as the skew operator $(z_1,z_2)\mapsto(z_2,-z_1)$ of a saddle-point problem. Composite saddle-point problems $\min_u\max_v\, f(u)+h(u)+\Phi(u,v)-g(v)$ with a smooth $h$ and a bilinear coupling $\Phi$ lead to such inclusions. Splitting methods that use each piece separately, and in the way that is cheapest for it, are the standard tools for these problems.

Timeline of the relevant results:

• 1979: Lions and Mercier study splitting algorithms for the sum of two monotone operators, among them forward-backward splitting, which needs a cocoercive forward operator (Lions–Mercier 1979).
• 2000: Tseng's forward-backward-forward method removes cocoercivity for a Lipschitz monotone operator, at the cost of two forward evaluations per iteration (Tseng 2000).
• 2017: Davis and Yin's three-operator splitting handles $A+B'+C$ with two resolvents and a cocoercive $C$ (Davis–Yin 2017).
• 2020: Malitsky and Tam introduce the forward-reflected-backward method for $A+B$ with $B$ monotone and Lipschitz, and in §5 a three-operator variant for $A+B+C$ with $C$ cocoercive (arXiv:1808.04162v4; SIAM J. Optim. 30(2), 2020).

Setting

Let $H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$. A set-valued operator $A:H\rightrightarrows H$ assigns to each $x$ a subset $A(x)\subseteq H$. It is monotone if $\langle x-y,u-v\rangle\ge0$ whenever $u\in A(x)$, $v\in A(y)$, and maximally monotone if moreover its graph is not properly contained in the graph of another monotone operator. For $\gamma>0$, the resolvent $J_{\gamma A}=(I+\gamma A)^{-1}$ sends $w$ to the unique point $p$ with $\gamma^{-1}(w-p)\in A(p)$.

A single-valued $B:H\to H$ is monotone if $\langle x-y,B(x)-B(y)\rangle\ge0$ and $L_1$-Lipschitz if $\|B(x)-B(y)\|\le L_1\|x-y\|$. A single-valued $C:H\to H$ is $\tfrac1{L_2}$-cocoercive ($L_2>0$) if

$$\tfrac1{L_2}\|C(x)-C(y)\|^2\le\langle C(x)-C(y),x-y\rangle\qquad\forall x,y\in H.$$

The problem (46) is to find $x\in H$ with $0\in(A+B+C)(x)$; its solution set is the zero set $(A+B+C)^{-1}(0)=\{x: -(B+C)(x)\in A(x)\}$. For a step size $\lambda>0$ and initial points $x_0,x_{-1}\in H$, the three-operator forward-reflected-backward scheme (47) is

$$x_{k+1}=J_{\lambda A}\big(x_k-2\lambda B(x_k)+\lambda B(x_{k-1})-\lambda C(x_k)\big)\qquad\forall k\in\mathbb N.$$

A sequence $(x_k)$ converges weakly to $\bar x$ if $\langle x_k,v\rangle\to\langle\bar x,v\rangle$ for every $v\in H$.

Formalization targets

Goal: Theorem 5.2

If $A$ is maximally monotone, $B$ is monotone and $L_1$-Lipschitz, $C$ is $\tfrac1{L_2}$-cocoercive, $(A+B+C)^{-1}(0)\ne\varnothing$ and

$$0<\lambda<\frac{2}{4L_1+L_2},$$

then every sequence generated by (47) converges weakly to a point of $(A+B+C)^{-1}(0)$.

Milestones

1. (48), proof of Lemma 5.1: the monotonicity of $A$ at $x_{k+1}$ and at a zero $x$, expanded into six inner-product terms.
2. Lemma 5.1: for $x\in(A+B+C)^{-1}(0)$ there is $\varepsilon>0$ with

$$\|x_{k+1}-x\|^2+2\lambda\langle B(x_{k+1})-B(x_k),x-x_{k+1}\rangle+(\lambda L_1+\varepsilon)\|x_{k+1}-x_k\|^2\le\|x_k-x\|^2+2\lambda\langle B(x_k)-B(x_{k-1}),x-x_k\rangle+\lambda L_1\|x_k-x_{k-1}\|^2.$$

3. Lower bound (proof of Theorem 5.2): the energy on the left of Lemma 5.1, with $\varepsilon$ removed, is nonnegative.

Significance

The two-operator forward-reflected-backward method applied to $A$ and $B+C$ would require $\lambda<1/(2L_1+2L_2)$, since $B+C$ is only known to be $(L_1+L_2)$-Lipschitz. Theorem 5.2 shows that using $C$ through a plain forward step, without reflection, enlarges the range to $\lambda<1/(2L_1+\tfrac12L_2)$. In particular, with $B=0$ the scheme is the forward-backward method and the range is $\lambda<2/L_2$, the classical one; with $C=0$ it is the forward-reflected-backward method with its range $\lambda<1/(2L_1)$. The result therefore interpolates between the two methods, with one resolvent, one new evaluation of $B$ and one evaluation of $C$ per iteration.

The theorem is proved in the paper, partly by reference: the proof says it is "more or less the same as Theorem 2.5" with Lemma 5.1 in place of Lemma 2.4. No machine-checked proof of Theorem 5.2 or of the two-operator Theorem 2.5 is known to exist. A formalization makes explicit the steps the paper leaves to the reader (the Opial-type argument and the identification of weak cluster points as zeros), and the energy inequality of Lemma 5.1 is reusable for rates and inertial variants.

Difficulty

The energy inequality is a careful but elementary computation with inner products. The difficulty lies in passing from it to weak convergence. The energy is not $\|x_k-x\|^2$ but $\|x_k-x\|^2$ plus a cross term in $B$ and a step-length term, so Fejér monotonicity of $(x_k)$ with respect to the zero set is not available, and the existence of $\lim\|x_k-x\|$ for each zero $x$ is not immediate from the energy inequality. The identification of weak cluster points as zeros requires that the graph of the maximally monotone operator $A+B+C$ be sequentially closed in the weak-strong topology, which in turn needs maximal monotonicity of a sum of a maximally monotone operator and a continuous monotone operator. A naive approach that treats $B+C$ as a single Lipschitz operator only reaches the smaller step range and does not prove the theorem.

Formalization scope

All statements live in a real inner product space H (NormedAddCommGroup, InnerProductSpace ℝ H), with CompleteSpace H for the goal. Set-valued operators are H → Set H. The operator vocabulary (monotone, maximally monotone, Lipschitz with a real constant, cocoercive, resolvent family) is the published module ThreeOpSplitting.Accel.MonotoneOperators. Conventions:

• The resolvent is a hypothesis: a family J : ℝ → H → H with IsResolventFamily A J (for each $\gamma>0$, $\gamma^{-1}(w-J_\gamma w)\in A(J_\gamma w)$). For maximally monotone $A$ it exists and is unique, so this is not an extra assumption.
• Indices are shifted by one: Lean's x j is $x_{j-1}$, and both initial points are arbitrary. The step size is one constant $\lambda$.
• "$\tfrac1{L_2}$-cocoercive" is IsCocoercive L₂⁻¹ C with $L_2>0$; the Lipschitz constant satisfies $L_1\ge0$, and $L_1=0$ is allowed.
• The zero set is $\{x: -(B+C)(x)\in A(x)\}$, and weak convergence is $\langle x_k,v\rangle\to\langle\bar x,v\rangle$ for all $v$.

The goal is not trivialized by these choices: the step range is exactly $(0,2/(4L_1+L_2))$, not the smaller two-operator range; $C$ enters (47) through $-\lambda C(x_k)$ only; and the conclusion is weak convergence to a point of the zero set of $A+B+C$, not of $A+B$. A sorry-free sanity file shows that all hypotheses are jointly satisfiable.

A complete development needs: demiclosedness of maximally monotone graphs, maximal monotonicity of the sum of a maximally monotone and a continuous monotone single-valued operator, and Opial's lemma for weak convergence. These are general and reusable beyond this mission, as is the weak-convergence infrastructure via inner products. Contributions of these lemmas, of proofs of the milestones, and of the goal are welcome.

Selected references

• Y. Malitsky and M. K. Tam, A Forward-Backward Splitting Method for Monotone Inclusions Without Cocoercivity, SIAM J. Optim. 30(2), 2020; arXiv:1808.04162v4. https://arxiv.org/abs/1808.04162v4
• H. H. Bauschke and P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., Springer, 2017. https://doi.org/10.1007/978-3-319-48311-5
• P. Tseng, A modified forward-backward splitting method for maximal monotone mappings, SIAM J. Control Optim. 38(2), 2000. https://doi.org/10.1137/S0363012998338806
• D. Davis and W. Yin, A three-operator splitting scheme and its optimization applications, Set-Valued Var. Anal. 25, 2017. https://doi.org/10.1007/s11228-017-0421-z
• P.-L. Lions and B. Mercier, Splitting algorithms for the sum of two nonlinear operators, SIAM J. Numer. Anal. 16(6), 1979. https://doi.org/10.1137/0716071

Motivation

Many problems in optimization, variational inequalities and saddle-point problems reduce to a monotone inclusion: find $x$ in a real Hilbert space $H$ with

$$0\in (A+B)(x),$$

where $A$ is set-valued and maximally monotone and $B$ is single-valued and monotone. Splitting methods solve such inclusions by evaluating $B$ directly (a forward step) and $A$ only through its resolvent (a backward step). The classical forward-backward method needs $B$ to be cocoercive; Tseng's forward-backward-forward method removes that requirement at the price of two evaluations of $B$ per iteration.

Malitsky and Tam (arXiv:1808.04162, SIAM J. Optim. 30(2), 2020, doi:10.1137/18M1207260) introduced the forward-reflected-backward method, which needs only monotonicity and Lipschitz continuity of $B$ and one evaluation of $B$ per iteration. Their Theorem 2.5 gives weak convergence (a separate mission of this series). This mission targets their Theorem 2.9: when $A$ is strongly monotone, the method converges at a linear rate. Linear rates under strong monotonicity are the standard benchmark against which first-order methods for monotone inclusions are compared, and they decide how the method behaves on regularized saddle-point problems in practice.

Timeline:

• 1979: Lions and Mercier analyse forward-backward splitting for cocoercive $B$.
• 2000: Tseng's forward-backward-forward method handles Lipschitz monotone $B$ with two forward steps per iteration (doi:10.1137/S0363012998338806).
• 2015: Malitsky's projected reflected gradient method treats the variational-inequality special case $A=N_C$ (doi:10.1137/14097238X).
• 2018–2020: Malitsky and Tam prove weak convergence of the forward-reflected-backward method for general maximally monotone $A$, and R-linear convergence for strongly monotone $A$ (Theorem 2.9).

Setting

$H$ is a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$. A set-valued operator $A:H\rightrightarrows H$ is monotone if $\langle x-y,u-v\rangle\ge0$ whenever $u\in A(x)$, $v\in A(y)$; it is maximally monotone if no monotone operator has a strictly larger graph; it is $m$-strongly monotone if $m>0$ and $\langle x-y,u-v\rangle\ge m\|x-y\|^2$ for all such pairs. The resolvent of $A$ with step $\gamma>0$ is $J_{\gamma A}=(I+\gamma A)^{-1}$, characterised by $\gamma^{-1}(w-J_{\gamma A}w)\in A(J_{\gamma A}w)$; for maximally monotone $A$ it is single-valued and defined everywhere. A single-valued $B:H\to H$ is monotone if $\langle x-y,B(x)-B(y)\rangle\ge0$ and $L$-Lipschitz if $\|B(x)-B(y)\|\le L\|x-y\|$.

The zero set is $(A+B)^{-1}(0)=\{x: -B(x)\in A(x)\}$. Given a step $\lambda>0$ and two starting points $x_0,x_{-1}\in H$, the constant-step forward-reflected-backward method is

$$x_{k+1}=J_{\lambda A}\big(x_k-2\lambda B(x_k)+\lambda B(x_{k-1})\big)\qquad(k\in\mathbb N).$$

For a point $x$ the proof uses the two sequences

$$a_k=\tfrac12\|x_k-x\|^2,\qquad b_k=\tfrac12\|x_k-x\|^2+2\lambda\langle B(x_k)-B(x_{k-1}),x-x_k\rangle+\tfrac12\|x_k-x_{k-1}\|^2 .$$

Formalization targets

Goal: Theorem 2.9 (p. 8)

Let $A$ be maximally monotone and $m$-strongly monotone, $B$ monotone and $L$-Lipschitz, $(A+B)^{-1}(0)\ne\varnothing$, and $\lambda\in(0,\tfrac1{2L})$. Then $(A+B)^{-1}(0)=\{\bar x\}$ and there are $q\in(0,1)$ and $M$ with

$$\|x_k-\bar x\|\le M\,q^k\qquad\text{for all }k.$$

The rate $q$ is left existential, as in the paper's phrase "converges R-linearly"; the explicit rate implied by the proof appears in the milestones.

Milestones (proof of Theorem 2.9, pp. 8–9)

1. The energy inequality with strong monotonicity:

$$(1+2m\lambda)\|x_{k+1}-x\|^2+2\lambda\langle B(x_{k+1})-B(x_k),x-x_{k+1}\rangle+(1-\lambda L)\|x_{k+1}-x_k\|^2\le\|x_k-x\|^2+2\lambda\langle B(x_k)-B(x_{k-1}),x-x_k\rangle+\tfrac12\|x_k-x_{k-1}\|^2 .$$

2. (27): with $\varepsilon=\min\{\tfrac12-\lambda L,5m\lambda\}>0$, $\ (1+4m\lambda)a_{k+1}+b_{k+1}+\varepsilon\|x_{k+1}-x_k\|^2\le a_k+b_k$.
3. $b_k\ge0$.
4. With $\alpha=\min\{1+4m\lambda-\tfrac{3\varepsilon}4,1+\tfrac\varepsilon2\}>1$: $\ \alpha(a_{k+1}+b_{k+1})\le a_k+b_k$.
5. $a_{k+1}\le a_{k+1}+b_{k+1}\le\alpha^{-(k+1)}(a_0+b_0)$.
6. $(A+B)^{-1}(0)$ has at most one point.

Significance

The result. Theorem 2.9 shows that the single-forward-evaluation method keeps the linear rate that the forward-backward method enjoys under cocoercivity, and that Tseng's method enjoys at twice the cost per iteration. The paper also notes that strong monotonicity of $B$ instead of $A$ reduces to this case by shifting $mI$ from $B$ to $A$, so the theorem covers strongly monotone saddle-point problems with Lipschitz couplings, for which it gives a geometric bound on the distance to the solution with an explicit contraction factor $\alpha^{-1/2}$.

Formalizing it. The theorem is proved in the paper; nothing about it is open. As far as is known it has no machine-checked proof. The mission produces a checked proof of the rate together with the constants $\varepsilon$ and $\alpha$ of the paper. One step of the printed derivation, the last inequality of (28), does not hold for every step $\lambda\in(0,\tfrac1{2L})$ (it needs $(\lambda L)^2\le\tfrac18$). The combined inequality of milestone 4, with the paper's constant $\alpha$, does hold on the whole range, and a formal proof settles this point.

Difficulty

The iteration is not a fixed-point iteration of a contraction in $x_k$ alone: $x_{k+1}$ depends on $x_k$ and $x_{k-1}$, and the natural Lyapunov quantity $b_k$ contains the cross term $2\lambda\langle B(x_k)-B(x_{k-1}),x-x_k\rangle$, which has no sign. The obvious argument, bounding $\|x_{k+1}-x\|$ by a multiple of $\|x_k-x\|$, fails because the reflected term $\lambda B(x_{k-1})$ couples consecutive steps; the contraction holds only for a combined energy, and only after showing that energy is nonnegative. The constants must be balanced so that the gain $4m\lambda$ from strong monotonicity outweighs what is spent controlling the cross term, uniformly in $\lambda$ up to $\tfrac1{2L}$.

Formalization scope

• $H$ is a type with [NormedAddCommGroup H] [InnerProductSpace ℝ H], plus [CompleteSpace H] in the goal. Operators are A : H → Set H and B : H → H. Monotonicity, strong monotonicity, maximal monotonicity, Lipschitz continuity and resolvents come from the published definition module ThreeOpSplitting.Accel.MonotoneOperators. Strong monotonicity sits on $A$, with $0<m$ a separate hypothesis; $B$ is only monotone.
• The resolvent is a hypothesis, not a construction: the method is driven by a family J : ℝ → H → H with J γ a resolvent of $A$ for every $\gamma>0$. For maximally monotone $A$ such a family exists and is unique.
• Indices are shifted by one: Lean's x j is the paper's $x_{j-1}$, so x 0 is $x_{-1}$ and x 1 is $x_0$. The starting points are arbitrary. The energies aSeq, bSeq follow the same shift.
• $L>0$ is pinned, because the step range $(0,\tfrac1{2L})$ divides by $L$.
• "R-linear convergence" is stated as an explicit geometric bound $\|x_k-\bar x\|\le Mq^k$ with a fixed $q\in(0,1)$, and uniqueness of the zero is part of the conclusion, not a hypothesis. A statement with plain norm convergence, a rate depending on $k$, a hypothesis that the zero is unique, or strong monotonicity on $B$ or on $A+B$ instead of $A$ is not the theorem; neither is a variable-step run.
• The milestones drop maximality of $A$ and completeness of $H$ where the step does not use them, and milestones 3 and 6 are stated with fewer hypotheses than in the proof; each is a stronger statement.
• No infrastructure beyond Mathlib and the published operator module is needed. Proofs of the milestones, alternative proofs of the goal and sharper rates are all useful contributions.

Selected references

• Y. Malitsky, M. K. Tam, A Forward-Backward Splitting Method for Monotone Inclusions Without Cocoercivity, SIAM J. Optim. 30(2), 2020. arXiv:1808.04162v4. https://arxiv.org/abs/1808.04162, https://doi.org/10.1137/18M1207260
• P. Tseng, A modified forward-backward splitting method for maximal monotone mappings, SIAM J. Control Optim. 38(2), 2000. https://doi.org/10.1137/S0363012998338806
• P.-L. Lions, B. Mercier, Splitting algorithms for the sum of two nonlinear operators, SIAM J. Numer. Anal. 16(6), 1979. https://doi.org/10.1137/0716071
• Y. Malitsky, Projected reflected gradient methods for monotone variational inequalities, SIAM J. Optim. 25(1), 2015. https://doi.org/10.1137/14097238X
• H. H. Bauschke, P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., Springer, 2017. https://doi.org/10.1007/978-3-319-48311-5

Motivation

Strategic open pit mine planning decides which parts of an ore body are excavated, when, and where each block of material is sent. Rivera Letelier, Espinoza, Goycoolea, Moreno and Muñoz (Operations Research 68(5), 2020) model the problem as a mixed-integer program, the precedence-constrained production scheduling problem with clusters (PCPSP-C), generalising the formulation of Bienstock and Zuckerberg (2010). Its integer versions have large integrality gaps on production scheduling instances, so the authors derive several families of cutting planes. This mission concerns the first family, the extraction cuts of §5.1: early start cuts, diamond cuts, and clique and lifted clique cuts. They exploit only the mining capacity of each period and the precedence structure, and they are valid both under full integrality and under the partial integrality used in commercial mine planning software.

Clique inequalities for precedence-constrained knapsack problems go back to Boyd (1993); early start cuts to Gaupp (2008, doctoral dissertation, Colorado School of Mines); the diamond cuts resemble cuts of Zhu, Bard and Yu (2006) for multimode project scheduling. The paper's contribution is their extension to the multi-period clustered model and to partial integrality.

All page references are journal pages of the published Operations Research article.

Setting

An instance has finite sets $\mathcal B$ of blocks, $\mathcal D$ of destinations and $\mathcal C$ of clusters, the latter a partition of $\mathcal B$, and periods $\mathcal T=\{1,\dots,T\}$. Block $b$ lies in cluster $c(b)$ and has weight $q_b\ge 0$. A precedence relation $b_1\prec b_2$ on blocks induces one on clusters ($c_1\prec c_2$ if some block of $c_1$ precedes some block of $c_2$), assumed to be a strict partial order. The arc set $\mathcal A$ is its transitive reduction: $(c,c')\in\mathcal A$ when $c'$ is an immediate predecessor of $c$. The closure is $cl(c)=\{c\}\cup\{c':c'\prec c\}$, the reverse closure $rcl(c)=\{c\}\cup\{c':c\prec c'\}$, and for a set $S$ of clusters $q(S)=\sum_{c\in S}\sum_{b\in c}q_b$, with $q_c=q(\{c\})$.

Variables $x_{c,t}$ give the fraction of cluster $c$ extracted in period $t$ and $y_{b,d,t}$ the fraction of block $b$ sent to destination $d$ in period $t$. The constraints (2)–(7) of p. 1427 are

$$x_{c(b),t}=\sum_{d}y_{b,d,t},\qquad \sum_{t}x_{c,t}\le 1,\qquad \sum_{t'\le t}x_{c,t'}\le\sum_{t'\le t}x_{c',t'}\ \ ((c,c')\in\mathcal A),\qquad Gy\le g,\qquad y\ge 0,$$

together with an integrality condition: full integrality (10) $x_{c,t}\in\{0,1\}$ defines the PCPSP-F, and partial integrality (11), "$\sum_{t'\le t}x_{c,t'}>0$ implies $\sum_{t'\le t}x_{c',t'}=1$ for $(c,c')\in\mathcal A$", defines the PCPSP-P. The general rows $Gy\le g$ include the mining capacity rows (8), $\sum_b\sum_d q_b\,y_{b,d,t}\le U_t$.

The cuts are written in the cumulative variables $w_{c,t}=\sum_{t'=1}^{t}x_{c,t'}$ (17), and with $Q_t=\sum_{t'=1}^{t}U_{t'}$. Two clusters $c_1,c_2$, neither preceding the other, are f-incompatible in time $t$ if $q(cl(\{c_1,c_2\}))>Q_t$, and p-incompatible if $q(cl(\{c_1,c_2\})\setminus\{c_1,c_2\})>Q_t$.

Formalization targets

Goal: Theorem 4 (clique and lifted clique cuts), p. 1433

For a set $\{c_1,\dots,c_k\}$ of clusters and $t\in\mathcal T$, the clique inequality

$$\sum_{i=1}^{k}w_{c_i,t}\le 1\tag{23}$$

is valid for the PCPSP-F if the $c_i$ are pairwise f-incompatible, and for the PCPSP-P if they are pairwise p-incompatible. If moreover $c\prec c_i$ for every $i$, the lifted inequality $\sum_{i=1}^{k}w_{c_i,t}\le w_{c,t}$ is valid under the same conditions. The goal is the conjunction of these four validity claims.

Milestones

• (18)–(20), p. 1432: $w_{c,t}\le w_{c,t+1}$, $w_{c,t}\le w_{c',t}$ for $(c,c')\in\mathcal A$, and $\sum_c q_c\,w_{c,t}\le Q_t$ at every feasible point satisfying (8).
• (21), p. 1432: under full integrality, $w_{c,t}\in\{0,1\}$. Its partial counterpart (22), "$w_{c,t}>0$ implies $w_{c',t}=1$ for $(c,c')\in\mathcal A$", is condition (11) verbatim in this formalization, which writes (11) in cumulative form, so it has no item of its own.
• Theorem 2 (early start cuts), p. 1432: if $q(cl(c))>Q_t$, then $w_{c,t}=0$ is valid for the PCPSP-F, and if $q_c>0$, $w_{c,t}\le (Q_t-q(cl(c)\setminus\{c\}))^+/q_c$ is valid for the PCPSP-P.
• Theorem 3 (diamond cuts), p. 1433: for $t_1\le t_2$ and $c_1\prec c_2$, $w_{c_2,t_2}\le w_{c_1,t_1}$ is valid for the PCPSP-F if $q(cl(c_2)\cap rcl(c_1))>Q_{t_1,t_2}=\sum_{t'=t_1}^{t_2}U_{t'}$, and for the PCPSP-P if $q((cl(c_2)\cap rcl(c_1))\setminus\{c_1,c_2\})>Q_{t_1,t_2}$.

Significance

Each of these inequalities cuts off fractional points of the linear relaxation while keeping every integer (or partially integer) schedule, and early start cuts can fix variables to zero before the solve. The paper motivates them by the large integrality gaps it observes on production scheduling instances (§5, p. 1432) and evaluates them, with its production cuts, in the computational study of §8. Because they use only the precedence order and the mining capacity, the extraction cuts apply to any multi-period precedence-constrained knapsack structure, beyond mining.

The results are proved in the paper, by short contradiction arguments. None of them has a machine-checked proof. Formalizing them yields a reusable model of the PCPSP-C with its two integrality regimes, and a checked account of exactly which rows of the formulation each cut relies on: in particular that validity needs the capacity rows (8) and the integrality condition, and fails for the LP relaxation.

Difficulty

The arguments rely on facts the paper uses in one line. Under partial integrality, $w_{c,t}>0$ forces $w_{c',t}=1$ for every predecessor $c'$ of $c$, not only for the immediate ones of $\mathcal A$; this requires chaining condition (11) along covering arcs of a finite strict order, and showing that every precedence is a chain of immediate ones. The counting step needs $x\ge 0$, which is not a constraint of the formulation but follows from $x_{c(b),t}=\sum_d y_{b,d,t}$, $y\ge 0$ and the nonemptiness of clusters. The diamond cut further splits the capacity $Q_{t_1,t_2}$ between periods and uses monotonicity of $w$ in time. A natural first attempt, arguing directly from the closure of $\prec$, does not apply: the formulation constrains only the arcs of $\mathcal A$.

Formalization scope

Blocks, destinations and clusters are finite types; periods are Fin T, index $t$ standing for period $t+1$. An instance carries the block-to-cluster map, the block precedence, values, discount rate, weights, capacities and $m$ side rows $Gy\le g$. Cluster precedence is derived from block precedence; $\mathcal A$ is its covering relation, and constraints (4) and (11) range over $\mathcal A$ only. The closure of a pair, which the page does not define, is $cl(c_1)\cup cl(c_2)$. Incompatibility includes incomparability of the two clusters, as on the page; "pairwise" ranges over distinct members of a finite set, which may be empty or a singleton.

The standing assumptions of §2.1 are hypotheses of every statement: clusters cover $\mathcal B$ (so each is nonempty), $\prec$ is a strict partial order on clusters, $r>0$, and $q_b\ge 0$. A cut "valid for the PCPSP-F (PCPSP-P)" is stated as: at every point feasible for the formulation with full (partial) integrality whose mining capacity rows (8) hold, the inequality holds. The capacity rows enter as an explicit hypothesis because the paper assumes they are among the rows of $Gy\le g$; without them every cut is false. Validity is never asserted for the LP relaxation, where the cuts do not hold, so the integrality condition cannot be dropped. In Theorem 2 the division by $q_c$ is guarded by $q_c>0$, as on the page.

The development needs only finite sums, finite sets and orders from Mathlib. Contributions are welcome on the chaining lemma for covering relations of finite strict orders and on the nonnegativity and monotonicity of $w$, which every milestone shares.

Selected references

• O. Rivera Letelier, D. Espinoza, M. Goycoolea, E. Moreno, G. Muñoz, Production Scheduling for Strategic Open Pit Mine Planning: A Mixed-Integer Programming Approach, Operations Research 68(5):1425–1444, 2020. https://doi.org/10.1287/opre.2019.1965
• D. Bienstock, M. Zuckerberg, Solving LP Relaxations of Large-Scale Precedence Constrained Problems, Proc. 14th Conf. Integer Programming and Combinatorial Optimization (IPCO), 2010, pp. 1–14.
• E. A. Boyd, Polyhedral results for the precedence-constrained knapsack problem, Discrete Applied Mathematics 41(3):185–201, 1993.
• G. Zhu, J. F. Bard, G. Yu, A Branch-and-Cut Procedure for the Multimode Resource-Constrained Project-Scheduling Problem, INFORMS Journal on Computing 18(3):377–390, 2006.