Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Douglas–Rachford splitting (DRS) minimizes a sum by alternating between the proximal mappings of the two terms. It is one of the most used first-order methods in signal processing, statistics and control, and, through its dual interpretation, it is the engine behind the alternating direction method of multipliers (ADMM). For convex problems its convergence theory is classical. In nonconvex problems — sparse regression with penalties, rank constraints, phase retrieval, feasibility problems with nonconvex sets — DRS is used routinely, but its theory is recent and depends on how the stepsize and the relaxation are chosen.
Themelis and Patrinos (SIAM J. Optim. 30(1), 2020; preprint arXiv:1709.05747v4) prove that when is -smooth and -hypoconvex and is merely proper and lower semicontinuous, DRS converges subsequentially to stationary points for stepsizes and relaxations in an explicit range. Their §4.2 then shows that these ranges cannot be enlarged: it constructs problems on which DRS fails as soon as the stepsize or the relaxation leaves the range. This mission formalizes that tightness half.
Timeline. Lions and Mercier (1979) proved convergence of DRS for maximal monotone operators. Li and Pong (Math. Program. 2016) gave the first nonconvex analysis, for and a stepsize bound well below . Themelis and Patrinos (2017–2020) introduced the Douglas–Rachford envelope, extended the analysis to all relaxations, reached the bound , and proved with the examples of §4.2 that the bounds are tight.
Write . A function is proper if it is never and finite somewhere. A differentiable is -smooth if is -Lipschitz, and -hypoconvex if is convex; an -smooth function is -hypoconvex for some , and is strong convexity.
The proximal mapping of with parameter is the set
which may be empty or contain several points. Given , one DR-iteration with stepsize and relaxation maps to through
A DRS run is a sequence obtained by iterating this step with any selection from the proximal sets. Its residual is . A point is a fixed point if some admissible step gives .
The paper's standing assumption (Assumption I) is: is -smooth and -hypoconvex, is proper and lower semicontinuous, and . The positive result needs ; Theorem 4.7 asks what happens beyond it.
For every , and there are and satisfying Assumption I such that
The pair may depend on , and only, never on , or the starting point.
For every , and there are , with additionally strongly convex such that, for every , every and every run, either is a fixed point or the residual does not vanish. A further milestone is the expansion identity from its proof.
The result. Theorems 4.7 and 4.8, together with the paper's convergence theorem, give a sharp map of the parameters for which nonconvex DRS is guaranteed to work under Assumption I. For practitioners they say that the stepsize cannot be traded for a larger one without structure on , and that over-relaxation beyond fails even when is strongly convex. The paper's Theorem 4.9 summarizes these facts as tightness of the bound .
Formalizing it. The results are proved on paper but not machine-checked anywhere. The formalization contributes a precise, selection-robust statement — the claim covers every run, including runs through points where a proximal set has two elements — and records two places where the printed statement and the proof do not match (see Formalization scope). Explicit proximal computations for piecewise-quadratic functions and indicators of finite sets, which the milestones need, are reusable for other counterexamples in splitting methods.
The claim is about every run, not one. A proximal set may contain two points, and a counterexample that works for one selection can fail for another. This is exactly what happens at in the paper's example: one admissible selection stays at a minimizer for ever.
The second difficulty is the dimension: the paper's functions live on while the theorems are stated on , and the construction has to be lifted so that the extra coordinates neither create fixed points nor make the residual vanish. Finally, for and large the proximal mapping of is empty or multivalued, so the analysis of a run must not assume a closed-form update.
is EuclideanSpace ℝ (Fin p); is real-valued and is EReal-valued and never . The proximal mapping is a set and a run is any selection; no proximal function is chosen. Every reciprocal bound is multiplied out: is 1 < γ * L, is γ * L < 1, is γ * negPartR σ < 1, so that imposes no constraint. The milestones are stated on , as in the paper.
Departures from the page, each disclosed in the items:
A formalization in which is improper, or in which the argmin is empty, would make the claim degenerate; properness and the argmin clause are part of the existential and rule that out. Weakening p4 to "some run" or "some starting point" is not this theorem.
Contributions welcome: proofs of the milestones (piecewise-quadratic proximal mappings, the prox of ), the lift from to , and the two theorems.
Nesterov's accelerated gradient method for -strongly convex, -smooth functions (NAG-SC) reaches accuracy in gradient steps, against for gradient descent (Nesterov, 1983; Nesterov, 2004). Polyak's heavy-ball method has the same accelerated behaviour on quadratics but not in general, and the two methods share the same classical continuous-time limit, the ODE . That limit therefore cannot explain why one method accelerates and the other does not.
Shi, Du, Jordan and Su (arXiv:1810.08907v3, 2018; Math. Program. 2021) keep the terms of the step size when passing to the limit. The resulting high-resolution ODEs differ between the two methods: the one for NAG-SC contains a gradient correction , a Hessian-driven damping term absent from the heavy-ball ODE. Their Theorem 1 shows that the high-resolution ODE of NAG-SC converges linearly at the accelerated rate , with an explicit constant tied to the step size.
Timeline. Polyak (1964) introduces the heavy-ball method; Nesterov (1983) the accelerated gradient method. Su, Boyd and Candès (2016) derive the low-resolution ODE of Nesterov's method for convex functions. Alvarez, Attouch, Bolte and Redont (2002) study inertial systems with Hessian-driven damping. Shi, Du, Jordan and Su (2018) obtain the high-resolution ODEs and the rates of their Theorems 1–6. Attouch, Chbani, Fadili and Riahi (2020) treat the closely related dynamics .
Let carry the Euclidean inner product and norm . For , is the class of differentiable convex functions , in the sense for all , whose gradient is -Lipschitz. adds that is with a Lipschitz-continuous Hessian . For , is the subclass of of -strongly convex functions:
Write for the minimizer of .
Fix a step size and a starting point . The high-resolution ODE of NAG-SC, (1.11), is
with and . The initial velocity matches the first step of NAG-SC. The Lyapunov function (2.4) is
In Lean these are IsS2 f μ L, IsNAGSCODE f μ s x0 X V (with V the velocity ) and lyap f μ s xs X V t, in the namespace HighResODE.NAGSCODE.
For , and every solution of (1.11), for all ,
Milestones 1–5 hold for every step size . The restriction enters only the goal and, through , milestone 6.
Theorem 1 is the continuous-time half of the paper's explanation of acceleration. With it gives , a linear rate at the accelerated exponent . The Lyapunov function (2.4) is the template from which the paper builds the discrete Lyapunov function (2.6) for NAG-SC itself, and the bracket in Lemma 3.1 is what that discretization uses (Remark 3.3). The heavy-ball ODE (1.10) lacks this term (Lemma 3.2), and that difference is the paper's account of why NAG-SC accelerates and heavy ball does not.
The result is proved in the paper; no machine-checked version is known. A formal proof needs a one-sided differential inequality along a trajectory in , a Grönwall-type integration, and an elementary but delicate rational inequality in . The milestones isolate each of these steps. The Lyapunov computation is also reusable for the sibling missions of this series on the heavy-ball and NAG-C ODEs.
The algebra in (3.4) is routine once the derivative exists. The work is in making that derivative rigorous. Differentiating needs the chain rule for and for . The second uses : the time derivative of is . All derivatives are one-sided at . Passing from to (3.2) needs a comparison argument on , not just a pointwise derivative bound. The constant of the goal rests on the coefficient inequality of milestone 6, and that inequality is tight: its left side tends to as , so no crude estimate closes it.
is EuclideanSpace ℝ (Fin n), is Mathlib's gradient f, and is fderiv ℝ (gradient f) x v. The classes are structures in the first-order form of p. 8. requires ContDiff ℝ 2 f and an existential Lipschitz constant for the Hessian, because the page fixes none. The minimizer is a point with for all .
A solution of (1.11) is a pair of curves with these properties:
Values for are irrelevant. Existence and uniqueness of the solution (the paper's Proposition 2.1) are not assumed: every statement quantifies over every solution. Derivative claims are stated as the existence of a one-sided derivative with the claimed value or bound, never through deriv, which returns where no derivative exists. The ODE predicate fixes as the derivative of , so cannot be chosen freely. The goal assumes only the ODE and the class, never the Lyapunov decay. The initial velocity uses as in (1.11); footnote 4 (p. 5) drops the , a printed slip.
All six milestones are stated. Solvers are welcome to work on any of them. A general one-sided Grönwall lemma on and the chain rule for would serve the other ODE missions of this series as well.
In online matching with multiple prices, a firm sells items with limited inventories to customers who arrive one at a time; each item can be offered at any price from its own finite price set, and the firm must commit to an offer without knowing future customers. Ma and Simchi-Levi (arXiv:1905.04770, Oper. Res. 2020) show that the best possible competitive ratio (worst-case ratio of the online revenue to the offline LP optimum) for a price set is an explicit number , computed from alone.
Two tight ratios were known before. For a single item sold over a price set, Ball and Queyranne (Oper. Res. 2009) found the tight ratio . For many items with one price each, the tight ratio is (Karp, Vazirani and Vazirani 1990; Mehta, Saberi, Vazirani and Vazirani 2007). For a single item whose price ranges over a continuum , Ball and Queyranne give . A reader meeting for the first time asks how it compares with these. Proposition 2 of the paper answers that question with strict inequalities, and this mission formalizes it.
A price set consists of prices
with the convention . Write for .
The booking limits are positive numbers with satisfying
The Ball–Queyranne limits are positive numbers with satisfying
Both systems have exactly one solution (Proposition 1). The paper's ratios are and (Definition 2). Finally, for let be the unique real root of
is the paper's competitive ratio when every item may be priced anywhere in (App. E.1).
In Lean the prices are r : ℕ → ℝ read at , and IsPriceSet m r, IsBookingLimits m r α, IsBQLimits m r σ are the predicates above.
For ,
The result. Inequality (11) shows that the multi-item, multi-price ratio is not obtained by multiplying the single-item ratio by the single-price penalty : the true ratio is strictly larger, so neither the ratio nor the algorithms of the paper can be assembled from the two classical cases. Inequalities (12) and (13) quantify the value of a discrete price menu: restricting the continuum to finitely many prices strictly raises the tight ratio, both for one item (Ball–Queyranne) and for many items (this paper). The ranges of and bound the guarantees in terms of the number of prices alone, and the two-price formula (4) is the explicit instance used throughout the paper's introduction.
Formalizing it. All results here are proved in the paper (App. A); none has a machine-checked proof that we know of. The mission produces a checked theory of the booking-limit systems (7) and (8), which the paper's three main theorems (the competitive ratios of Multi-price Balance and Multi-price Ranking, and the matching upper bound) all rest on, and checked proofs of the comparisons. The booking-limit predicates are the same in the companion missions of this series and are intended to be shared after consolidation.
The statements are elementary, but (7) is a nonlinear system: eliminating leaves a polynomial equation of degree in , with no closed form for . So cannot be computed and compared directly; every inequality has to be derived from properties of the defining equations. The root of (13) is likewise defined only implicitly (via the Lambert function). The naive approach of comparing the two systems equation by equation does not give (11)'s second inequality, because (7) and (8) relate each limit to the first one through different functions and the two families are tied together only by their common normalization . In Lean the main friction is bookkeeping: sums over , natural-number index arithmetic , and the uniqueness arguments, which require strict monotonicity of the functions in (33) and (34).
Conventions: prices are r : ℕ → ℝ, 1-based, with price r 0 = 0 for ; sums over are over Finset.Icc 2 m. The booking limits are not constructed by Classical.choose: every statement takes functions α, σ together with the hypotheses IsBookingLimits m r α / IsBQLimits m r σ (equations (7)/(8), positivity on , sum ). Proposition 1 shows these hypotheses pin down the paper's values on , so no statement is about an arbitrary ; a sanity file exhibits solutions for and for the price set , so the hypotheses are satisfiable. Standing assumptions are those of the paper: throughout and in Proposition 2, (33), (34), as printed. The constant is written .
Clause (13) is stated for every real root of ; milestone 5 proves that exactly one root exists, so the clause is neither vacuous nor weaker than the printed "the unique solution". The monotonicity of is posed on the printed with the value at set explicitly to the limit , since Lean's would otherwise give a junk value there.
Everything needed is in Mathlib (Real.exp, Real.log, Real.sqrt, finite sums). Contributions are welcome on any milestone; the monotonicity lemma and Proposition 1 are reusable by the other missions of this series. The paper's proofs are in its Appendix A (pp. 38–39).
Accelerated first-order methods, the heavy-ball method of Polyak and Nesterov's accelerated gradient (NAG) method, reach an error on a -strongly convex, -smooth problem in gradient steps, , against for plain gradient descent. A long line of work has tried to explain where this square root comes from by reading the methods as discretizations of ordinary differential equations: Su, Boyd and Candès (arXiv:1503.01243), Wibisono, Wilson and Jordan (arXiv:1603.04245), and others.
Luo and Chen (arXiv:1909.03145, Math. Program. 2022) take the view from numerical analysis. Section 2 of their paper treats the quadratic case: the gradient flow is stiff, and an explicit scheme for it needs step size . They embed in a block matrix whose spectrum lies in the left half-plane with condition number , and they show that an explicit Gauss–Seidel splitting scheme for is stable with step size of order . This is the linear-algebra core of the paper's argument. The later sections build the nonlinear schemes (missions 2–8 of this series) on it.
Let be a real symmetric matrix. Its eigenvalues are real, and we assume
with condition number . For any real square matrix , the spectrum is the set of its eigenvalues, which are complex in general, and the spectral radius is .
The two transformations (39) of the paper are the block matrices
For the linear system , write , where is the block lower triangular part of (the two diagonal blocks and the lower-left block) and . The Gauss–Seidel splitting scheme (41) with step size is
The matrix is block lower triangular with diagonal blocks that are multiples of , so the scheme is explicit and never inverts . A one-step scheme is A-stable if .
Appendix A works with the scalar model , where and , and with its Gauss–Seidel matrix , defined in the same way from the lower triangular part of .
For or , if , then the scheme is A-stable and
The goal is the weakest of these statements. Milestones 4 and 5 show that it is attained for heavy ball and strict for NAG.
The result. Theorem 2.1 gives a contraction factor per step for an explicit, matrix-free scheme. Applied to , that is the accelerated linear rate. Eliminating from shows that both transformations discretize the same second-order ODE . The theorem therefore explains acceleration as a stability property of an ODE solver, not as an algebraic trick. The paper's nonlinear schemes (predictor–corrector, gradient correction, Nesterov's method, the proximal variants) are built from this splitting. Their Lyapunov analyses generalize the spectral computation formalized here.
Formalizing it. The result is proved in the paper; to our knowledge no machine-checked proof exists. A formalization has to make the paper's "it is clear that" spectral reduction rigorous: the block diagonalisation through and the identification of the spectrum of a structured non-symmetric matrix with a union of spectra. It also has to treat spectra of real matrices over . Both are reusable well beyond this paper, since every spectral analysis of a momentum method (heavy ball, NAG, their discretizations) runs through the same reduction.
The obvious route bounds a norm of . It fails: is not normal, and the paper stresses that is not controlled by . The bound concerns eigenvalues only, and the eigenvalues are complex.
A second naive route applies a Gershgorin or field-of-values estimate to directly. It loses the square root, because the off-diagonal blocks have norm . The real content is that for each eigenvalue of , the Gauss–Seidel matrix has a negative discriminant exactly when the step-size condition holds. Its eigenvalues are then a conjugate pair on the circle of radius , and does not depend on . Reaching this needs three things: the reduction of the block spectrum to scalar spectra, the explicit inverse of , and a careful equivalence of the discriminant condition with (126).
Matrices are Matrix (Fin d) (Fin d) ℝ, and the block matrices live on Fin d ⊕ Fin d, built with Matrix.fromBlocks.
spectrum ℂ of its complexification. "" is IsGreatest of the set of eigenvalue moduli. "" and "" are stated eigenvalue by eigenvalue, so no junk supremum over an empty set can make a bound vacuous.Two trivializations are ruled out explicitly. A spectral radius defined as sSup over a possibly empty spectrum would make every bound hold vacuously at . A spectrum taken over would miss the complex eigenvalues, which are all of them here.
A complete development needs:
Lemmas of this kind, stated for general symmetric , are welcome as separate theorems.
Many problems in optimization reduce to a linear complementarity problem over a cone: convex quadratic programs, linear and second-order cone programs, and more generally the KKT systems of convex quadratic cone programs (QCPs). First-order solvers for these problems, such as SCS (O'Donoghue–Chu–Parikh–Boyd 2016), must return either a solution or a certificate that none exists, and must do so reliably at scale; in branch-and-bound methods for mixed-integer quadratic programs, for example, fast and robust infeasibility certificates decide which branches are pruned. O'Donoghue (arXiv:2004.02177v4) embeds a monotone linear complementarity problem into a single homogeneous problem that always has a solution, from which either an answer or a certificate of infeasibility can be read off, and solves the embedded problem by Douglas–Rachford (DR) splitting. This is the algorithm behind SCS 3.0.
DR splitting converges for the sum of two maximal monotone operators. The mission formalizes the result that makes the method applicable: the paper's embedding operator is maximal monotone.
Write with points and inner product . An operator on is identified with its graph, a set of pairs (point, value). It is monotone if for all pairs in it, and maximal monotone if it is monotone and not strictly contained in another monotone operator.
Fix and . The matrix is monotone if (3.4); need not be symmetric. For a nonempty closed convex cone with dual cone , the problem asks for with
The paper introduces three operators on :
The embedded problem is . Its solutions with give solutions of the LCP, and its solutions with give certificates of infeasibility.
For every monotone and every ,
In the order the proof of Lemma 4.4 uses them:
The mission also states the following results of the same construction:
Lemma 4.4 is the hinge of the paper. is maximal monotone, so once is too, DR splitting applied to the embedded inclusion converges for every LCP with monotone , feasible or not. This holds whether the problem has a solution or a certificate, without the strict feasibility or strong duality an interior-point homogeneous model relies on. The closed-form resolvent and Lemma 5.1 then turn this into Algorithm 5.1: one cached linear solve with and one scalar quadratic per iteration.
The result is proved in the paper. The DR convergence theorem itself and the extension theorem used for maximality are cited from Bauschke–Combettes. To our knowledge none of the results here has been machine-checked. A formal proof supplies two pieces of value. First, an argument for maximality that does not rest on the Zorn-based extension theorem the paper invokes. Second, a checked statement of the operator underlying a widely used solver, with its exact domains.
Monotonicity of , of and of their union is matrix algebra plus (3.6). The difficulty is maximality: given a pair that is monotonically related to every pair of , one must show it already lies in . There are three regimes, according to the sign of .
The naive route, " is continuous and monotone, so it is maximal", fails because is open and not the whole space. Indeed alone is not maximal. The boundary behaviour is carried entirely by , whose domain condition is exactly what monotonicity forces in the limit.
Points of are pairs in (Fin d → ℝ) × ℝ, and the inner product is written with dotProduct. Operators are Sets of (point, value) pairs. Maximal monotonicity is the containment form over all monotone operators on this space.
The standing assumption "M is monotone" is the explicit hypothesis (M + Mᵀ).PosSemidef in every theorem that involves (all but Lemma 5.1). It is not (which would force symmetry), and the lemmas' sentences do not repeat it. The cone does not enter and is not a hypothesis of the goal. Where a companion uses it, it is a nonempty, closed, convex cone, as on p. 4. The supremum in (4.4) is written pointwise. The dimension is allowed; the goal is true there.
The domain conditions are part of the graphs: in , and together with in . Each of the following trivializing or falsifying formalizations is ruled out:
Lemma 4.2 is stated in the certificate form its proof establishes. The distance-based notion of strong infeasibility is not formalized.
The development needs only finite-dimensional linear algebra from Mathlib: Matrix.mulVec, dotProduct, Matrix.PosSemidef, matrix inverse, and EuclideanSpace for Lemma 5.1. The definitions of monotone and maximal monotone graphs on are reusable. Welcome contributions include:
Many convex problems in signal processing, statistics and control have the composite form "smooth loss plus nonsmooth regulariser, subject to a simple constraint": a least-squares or entropy term , a sparsity or total-variation penalty , and a feasible set such as a box, a simplex or a cone. Accelerated proximal gradient methods (FISTA, Beck and Teboulle 2009; Nesterov's composite gradient methods) reach the optimal rate for such problems when . When a constraint is present, the standard schemes evaluate at extrapolated points that may leave ; for an such as the entropy on , that gradient does not exist.
Luo and Chen (arXiv:1909.03145v4, Math. Program. 2022) derive accelerated first-order methods as discretisations of a single ODE, the NAG flow, and analyse every scheme with one discrete Lyapunov function. Their Section 7.3 turns the predictor–corrector discretisation into a forward–backward splitting, the semi-implicit accelerated forward–backward method (Semi-AFB), whose iterates stay in by construction, and proves for it the same rate as for the unconstrained smooth case.
Timeline. Tseng (2008) gave an accelerated proximal gradient method with rate for this problem with . Nesterov (Math. Program. 2013, "Gradient methods for minimizing composite functions") treated the same problem with -smooth on and -strongly convex, , and obtained the rate with estimate sequences, at the cost of two proximal computations over per iteration. Luo and Chen's Theorem 7.3 (2019, revised 2022) gives the same type of rate with one proximal computation per iteration and a Lyapunov proof.
is a real Hilbert space with inner product and norm . For a set , a function is in if it is continuously differentiable on , with gradient map , and
It is in if moreover is -Lipschitz on , .
The problem (104) is
with closed and convex, , , and proper, closed and convex, with . Let be a minimiser.
Algorithm 4 (Semi-AFB). Given and , for : choose with ; set , and ; let
and set . The Lyapunov function is
For every run of Algorithm 4,
with (89). The contraction (121) is the core; (87) and (88) are its consequences through Lemma B.2.
The result. Theorem 7.3 shows that one explicit gradient step on and one proximal step on restricted to per iteration suffice for acceleration, uniformly in : it gives the rate for convex and the linear rate for strongly convex in one statement, and need not know . All iterates remain in , so the method applies when exists only on .
Formalizing it. The theorem is proved on paper, with a short Lyapunov argument; no machine-checked version is known to exist. A formal proof checks the bookkeeping of the argument, including the role of the domain of , and makes the Lyapunov inequality available as a reusable step for other accelerated splitting schemes. The scalar Lemma B.2 is shared with the paper's other schemes (Theorems 5.1, 5.2 and 7.2).
The first-order condition that the paper uses for , a variational inequality with some , needs the subdifferential sum rule , which requires a constraint qualification that (104) does not impose. It fails, for example, when and meet in a single boundary point. A proof of the goal therefore cannot simply take such a for granted. The second difficulty is bookkeeping: (2) and (4) hold for on only, so each of the points at which they are applied must be shown to lie in , and the convexity of is used at points that must lie in . Finally, (87) and (88) require the scalar recursion of Lemma B.2 for the product , whose square-root estimates are not routine.
is a real Hilbert space (InnerProductSpace ℝ V, CompleteSpace V); is identified with by Riesz. The gradient of is an explicit map gradh with a gradient of within at every point of (HasGradientWithinAt). Nothing is assumed about off , and (4) is not assumed. The extended-valued is encoded by its effective domain D and its real values g : V → ℝ on D. Convexity is ConvexOn ℝ D g, closedness is a closed epigraph, and step 5's argmin over is a minimiser over . The scheme is a hypothesis on sequences (IsAFBRun), with any positive solution of the step relation. Integer powers are used for and . Lemma B.2's is encoded as any real upper bound of .
Standing and added hypotheses: minimises over (the paper assumes argmin ). , and are inputs of Algorithm 4. The hypothesis is added to the page's , because otherwise . The goal makes no subgradient or variational-inequality assumption. Milestone (120) carries the variational inequality as an explicit premise. A trivializing formalization would quantify over sequences assumed to satisfy (121), or replace the argmin of step 5 by an arbitrary point of ; the goal quantifies over genuine runs of Algorithm 4, with a genuine minimisation predicate.
A complete development needs elementary Hilbert-space identities, the minimiser inequality for a strongly convex function over a convex set, the descent inequality (4) on a convex set from (3), and the scalar recursion of Lemma B.2. The last two are reusable across the whole series. Contributions to any milestone are welcome.
The projected gradient method is the basic algorithm for minimising a smooth convex function over a closed convex set. For an objective with an -Lipschitz gradient it converges at the sublinear rate , and the classical way to obtain a linear (geometric) rate is to assume strong convexity. Many objectives that arise in practice are not strongly convex: least squares with a rank-deficient matrix, the dual of a linearly constrained problem, or with strongly convex and singular. Such problems have a whole set of minimisers rather than a single one, yet the projected gradient method is observed to converge linearly on them.
Necoara, Nesterov and Glineur (arXiv:1504.06298, v4 2016; Math. Program. 175 (2019)) introduce a hierarchy of relaxations of strong convexity, measured relative to the optimal set instead of between arbitrary pairs of points, and prove linear convergence of several first order methods under each of them. This mission formalizes the first such result: linear convergence of the projected gradient method on quasi-strongly convex objectives (Theorem 11 of the preprint).
Related conditions have a longer history: the error bounds of Luo and Tseng (1993) for feasible descent methods and the Polyak–Łojasiewicz inequality (Polyak 1963). Karimi, Nutini and Schmidt (2016) compare several of these in the unconstrained case.
Let be a closed convex set, with the Euclidean inner product and norm . Let be a convex function on , differentiable at every point of , whose gradient is Lipschitz on :
Problem (P) is , with optimal set , assumed nonempty.
The projection of onto a closed convex set is . For write for the point of nearest to ; then is the distance from to the optimal set.
is quasi-strongly convex with constant if, for every ,
This is the strong convexity inequality with the second point fixed to . It does not force a unique minimiser. The class of convex functions with -Lipschitz gradient satisfying (10) is denoted , and is the condition number.
The projected gradient method (GM) starts from and iterates
with step sizes .
For and (GM) with , for every ,
Theorem 11 gives a geometric rate for the distance to the optimal set on a class strictly larger than the strongly convex functions. The rate depends only on the ratio , exactly as in the strongly convex case with in place of the strong convexity constant. Through (49) the rate passes to function values, and (50) interpolates between the linear rate and the classical rate as . The paper's later sections show that the class contains, for example, over a polyhedron with strongly convex, which covers dual and least-squares problems with singular data.
The result is proved in the paper; it is not known to be formalized. The mission produces a machine-checked statement of the class (10), the projected gradient iteration with a non-unique optimal set, and the rate (45), together with the intermediate inequalities of the proof. The definitions of the optimal set, the nearest-point projection and the (GM) run are reusable for the companion missions of this series (fast gradient, feasible descent methods) and for other projection-based methods.
The standard proof for strongly convex compares with the unique minimiser and uses strong convexity between and . Here the minimiser is not unique, and the comparison point changes with : the inequality at step is written relative to , and the bound at step must be relative to . The two are linked only through the nearest-point property . In addition, (10) controls only the direction toward , so to absorb the term the proof needs quadratic functional growth at , which is not part of the hypothesis and requires the separate implication (10) ⇒ (22). That implication uses convexity of essentially; (10) alone does not imply it with the same constant by a one-line argument.
In Lean, the work includes the descent lemma on a convex set from a gradient that is Lipschitz only on , the variational inequality of the Euclidean projection, and the implication (10) ⇒ (22) with the same constant.
EuclideanSpace ℝ (Fin n). is a function on the whole space, convex on (ConvexOn ℝ X f) and differentiable at every point of , with = gradient f; the Lipschitz bound (1) is required on with .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":
Harvey–van der Hoeven (2021) use all of these in §2.1, §2.3 and §4–§5 of their 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 . 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).
The machine model, input and output conventions, and the time-bound predicate are those of IntMul_MultitapeModel. That model follows Montanaro's lecture notes:
For subroutines whose input is not of the form , the new definitions file IntMul_MultitapeWords starts the machine on an arbitrary word over . It also provides the encodings
: a single multitape machine multiplies -bit integers for every in worst-case time .
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.
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, with strongly convex and singular. Their optimal sets are not single points, so strong convexity fails, and some weaker property of 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 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).
Work in with the Euclidean inner product and norm . Problem (P) is
with closed and convex and convex, with gradient Lipschitz on with constant :
The optimal set is assumed nonempty. The projection of onto a nonempty closed convex set is the nearest point of to . For write .
The projected gradient step from is , and . The projected gradient method (GM) starts at and iterates for .
has quadratic functional growth with constant , written , when
The condition number is .
Under the standing assumptions of (P):
then satisfies (22) with constant .
Together these say that a uniform one-step contraction of by the gradient step with step size is equivalent to quadratic functional growth.
A companion item states the function-value rate (53), for .
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 per step from growth, and growth constant from contraction factor .
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.
The ⇒ direction is a contraction argument along one step; its difficulty is the projection calculus: the variational inequality characterizing , applied with , and the descent lemma (2), which must be derived from (1) on the convex set only, since need not be smooth off . The nearest point of differs from ; 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 () is not what the paper proves, and the one-step hypothesis cannot be recovered from it without extra work.
Lean represents as EuclideanSpace ℝ (Fin n) and as gradient f. is a function on all of that is differentiable at every point of ; only its values and gradients on enter. The standing assumptions of p. 3 are explicit hypotheses of every theorem: closed and convex, convex on , (1) with , and a named minimiser ; the paper's "simple" (cheap projection) is not a mathematical hypothesis and is dropped, and "closed" for is implied by continuity on . The optimal value is , or , 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 . The page prints "for " 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 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 , and existence of nearest points. Contributions of these lemmas, of the milestones in any order, and of the goal are welcome.
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.
Let carry the Euclidean inner product and the norm . For a set and a point , a nearest point is a point with for every .
Problem (P) is , where
The function has quadratic functional growth with constant (Definition 4, inequality (22)) if, for every and its nearest point ,
The class consists of the convex functions satisfying (1) and (22).
A run of the feasible descent method (FDM) with constants consists of stepsizes , error vectors and iterates () with and, for every ,
The errors are part of the run: any vectors meeting the two conditions are allowed. With , and a run is the projected gradient method (GM) of the paper.
For and every run of (FDM), for all ,
The rate is the one printed in the paper; the statement fixes no numerical values of the constants.
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 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 , , and the error ratio . The paper also notes (p. 30) that linear convergence of to a point of 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.
The obvious argument for projected gradient methods compares with a fixed minimizer and uses strong convexity to contract the distance; here neither is available. There is no strong convexity, 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 is only controlled relative to the step , not absolutely, and the stepsize is only bounded below, so any estimate has to be uniform in and has to measure progress against the moving nearest point of the optimal set rather than a fixed minimizer.
The ambient space is EuclideanSpace ℝ (Fin n); is a function on all of , and only its values and gradients (Mathlib's gradient) at points of enter. The nearest point is the predicate IsNearest S u p, never a choice function, so a run of (FDM) is any pair of sequences , with stepsizes satisfying the predicate IsFDMRun. Statements about hold for every nearest point; since is closed and convex the nearest point is unique. The optimal set is nonempty because a minimizer is a hypothesis, and is , not an infimum. Sequences are indexed from .
Standing assumptions of p. 3 are hypotheses: closed and convex, convex on , differentiable on , (1) with , nonempty. The word "simple" (projection is cheap) is not a mathematical condition and is dropped; closedness of follows from continuity on . The class hypothesis is unbundled into convexity, (1) and (22) with . The constants satisfy , as on the page, and no upper bound on is imposed. The milestone (65) drops every hypothesis it does not need (it uses only convexity of ), 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, is never empty, gradients are only evaluated at points of where is differentiable, and the run conditions are satisfiable by non-stationary sequences (for on , , , ).
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 , 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.
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 of a saddle-point problem. Composite saddle-point problems with a smooth and a bilinear coupling 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:
Let be a real Hilbert space with inner product . A set-valued operator assigns to each a subset . It is monotone if whenever , , and maximally monotone if moreover its graph is not properly contained in the graph of another monotone operator. For , the resolvent sends to the unique point with .
A single-valued is monotone if and -Lipschitz if . A single-valued is -cocoercive () if
The problem (46) is to find with ; its solution set is the zero set . For a step size and initial points , the three-operator forward-reflected-backward scheme (47) is
A sequence converges weakly to if for every .
If is maximally monotone, is monotone and -Lipschitz, is -cocoercive, and
then every sequence generated by (47) converges weakly to a point of .
The two-operator forward-reflected-backward method applied to and would require , since is only known to be -Lipschitz. Theorem 5.2 shows that using through a plain forward step, without reflection, enlarges the range to . In particular, with the scheme is the forward-backward method and the range is , the classical one; with it is the forward-reflected-backward method with its range . The result therefore interpolates between the two methods, with one resolvent, one new evaluation of and one evaluation of 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.
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 but plus a cross term in and a step-length term, so Fejér monotonicity of with respect to the zero set is not available, and the existence of for each zero is not immediate from the energy inequality. The identification of weak cluster points as zeros requires that the graph of the maximally monotone operator 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 as a single Lipschitz operator only reaches the smaller step range and does not prove the theorem.
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:
J : ℝ → H → H with IsResolventFamily A J (for each , ). For maximally monotone it exists and is unique, so this is not an extra assumption.x j is , and both initial points are arbitrary. The step size is one constant .IsCocoercive L₂⁻¹ C with ; the Lipschitz constant satisfies , and is allowed.The goal is not trivialized by these choices: the step range is exactly , not the smaller two-operator range; enters (47) through only; and the conclusion is weak convergence to a point of the zero set of , not of . 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.
Many problems in optimization, variational inequalities and saddle-point problems reduce to a monotone inclusion: find in a real Hilbert space with
where is set-valued and maximally monotone and is single-valued and monotone. Splitting methods solve such inclusions by evaluating directly (a forward step) and only through its resolvent (a backward step). The classical forward-backward method needs to be cocoercive; Tseng's forward-backward-forward method removes that requirement at the price of two evaluations of 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 and one evaluation of per iteration. Their Theorem 2.5 gives weak convergence (a separate mission of this series). This mission targets their Theorem 2.9: when 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:
is a real Hilbert space with inner product . A set-valued operator is monotone if whenever , ; it is maximally monotone if no monotone operator has a strictly larger graph; it is -strongly monotone if and for all such pairs. The resolvent of with step is , characterised by ; for maximally monotone it is single-valued and defined everywhere. A single-valued is monotone if and -Lipschitz if .
The zero set is . Given a step and two starting points , the constant-step forward-reflected-backward method is
For a point the proof uses the two sequences
Let be maximally monotone and -strongly monotone, monotone and -Lipschitz, , and . Then and there are and with
The rate is left existential, as in the paper's phrase "converges R-linearly"; the explicit rate implied by the proof appears in the milestones.
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 instead of reduces to this case by shifting from to , 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 .
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 and of the paper. One step of the printed derivation, the last inequality of (28), does not hold for every step (it needs ). The combined inequality of milestone 4, with the paper's constant , does hold on the whole range, and a formal proof settles this point.
The iteration is not a fixed-point iteration of a contraction in alone: depends on and , and the natural Lyapunov quantity contains the cross term , which has no sign. The obvious argument, bounding by a multiple of , fails because the reflected term 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 from strong monotonicity outweighs what is spent controlling the cross term, uniformly in up to .
[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 , with a separate hypothesis; is only monotone.J : ℝ → H → H with J γ a resolvent of for every . For maximally monotone such a family exists and is unique.x j is the paper's , so x 0 is and x 1 is . The starting points are arbitrary. The energies aSeq, bSeq follow the same shift.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.
An instance has finite sets of blocks, of destinations and of clusters, the latter a partition of , and periods . Block lies in cluster and has weight . A precedence relation on blocks induces one on clusters ( if some block of precedes some block of ), assumed to be a strict partial order. The arc set is its transitive reduction: when is an immediate predecessor of . The closure is , the reverse closure , and for a set of clusters , with .
Variables give the fraction of cluster extracted in period and the fraction of block sent to destination in period . The constraints (2)–(7) of p. 1427 are
together with an integrality condition: full integrality (10) defines the PCPSP-F, and partial integrality (11), " implies for ", defines the PCPSP-P. The general rows include the mining capacity rows (8), .
The cuts are written in the cumulative variables (17), and with . Two clusters , neither preceding the other, are f-incompatible in time if , and p-incompatible if .
For a set of clusters and , the clique inequality
is valid for the PCPSP-F if the are pairwise f-incompatible, and for the PCPSP-P if they are pairwise p-incompatible. If moreover for every , the lifted inequality is valid under the same conditions. The goal is the conjunction of these four validity claims.
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.
The arguments rely on facts the paper uses in one line. Under partial integrality, forces for every predecessor of , not only for the immediate ones of ; 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 , which is not a constraint of the formulation but follows from , and the nonemptiness of clusters. The diamond cut further splits the capacity between periods and uses monotonicity of in time. A natural first attempt, arguing directly from the closure of , does not apply: the formulation constrains only the arcs of .
Blocks, destinations and clusters are finite types; periods are Fin T, index standing for period . An instance carries the block-to-cluster map, the block precedence, values, discount rate, weights, capacities and side rows . Cluster precedence is derived from block precedence; is its covering relation, and constraints (4) and (11) range over only. The closure of a pair, which the page does not define, is . 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 (so each is nonempty), is a strict partial order on clusters, , and . 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 ; 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 is guarded by , 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 , which every milestone shares.
Many problems in optimization, game theory and partial differential equations reduce to a monotone inclusion: find in a real Hilbert space with , where is a maximally monotone set-valued operator with an easily computed resolvent and is a single-valued monotone operator. Saddle-point problems, variational inequalities and composite convex minimization are all of this form. Splitting methods solve such inclusions by evaluating forward and backward (through its resolvent), never inverting .
The classical forward-backward method requires to be cocoercive, which excludes the skew operators arising from saddle-point problems. Tseng's forward-backward-forward method (2000) removed that assumption at the price of a second evaluation of per iteration. Malitsky and Tam (arXiv:1808.04162, SIAM J. Optim. 2020) introduced the forward-reflected-backward method, which needs only monotonicity and Lipschitz continuity of and evaluates once per iteration. Its §4, the subject of this mission, adds inertia (extrapolation along ) and relaxation (averaging with the previous iterate). Inertial and relaxed variants are used in practice to accelerate convergence and to enlarge the range of admissible step sizes; the inertial proximal point algorithm goes back to Alvarez and Attouch (2001).
Let be a real Hilbert space. A set-valued operator is monotone if whenever , , and maximally monotone if its graph is not properly contained in the graph of another monotone operator. Its resolvent with step is , a single-valued map on all of when is maximally monotone. A map is -Lipschitz if and -cocoercive if for all . The zero set is .
Given parameters , and starting points , the relaxed inertial forward-reflected-backward scheme (34) is
With it is equivalently (35), in which the inertial term is absorbed into . The case , is the forward-reflected-backward method; alone gives the inertial method (45).
If is maximally monotone, monotone, , , , , and either (a) is -Lipschitz and
or (b) is -cocoercive, and
then the sequence of (34) converges weakly to a point of .
A companion item states Corollary 4.4, the case , where the conditions become with (Lipschitz) or (cocoercive).
Theorem 4.3 gives an explicit region of for which a single-evaluation, inertial, relaxed splitting method converges for monotone Lipschitz , with no cocoercivity. In the cocoercive case it shows that inertia enlarges the admissible step size beyond that of the plain method (Corollary 4.4(b) allows ); in the Lipschitz case it quantifies the opposite effect. With it recovers the convergence of the inertial proximal point algorithm by an argument different from the classical one.
The theorem is proved in the paper; to our knowledge none of §4 has been machine-checked. The mission produces a formal proof of Theorem 4.3 and of the Lyapunov inequalities behind it. The proof in the paper ends with "the remainder of the proof follows a similar argument to Theorem 2.5"; making that remainder explicit, in particular the convergence of the energy terms , which rests on the factor in (40) rather than on Lemma 4.2 as printed, is part of the work.
The natural energy is not monotone along the iteration: both the reflected term and the inertial term make it increase at some steps, and the standard Fejér argument for forward-backward methods does not apply. The energy that does decrease couples three consecutive iterates through and the residual , and this cross term has no sign. Showing that the energy controls from below, and that the step-size conditions (41) and (42) make all the coefficients positive, is where the specific constants come from. Passing from boundedness to weak convergence then needs an Opial-type argument and the demiclosedness of the graph of the maximally monotone operator , in an infinite-dimensional space where bounded sequences only have weakly convergent subsequences.
The Lean development works in a real inner product space H, complete for the goal and the corollary; the intermediate inequalities need neither completeness nor maximality of and assume only monotonicity. Operator notions come from the published module ThreeOpSplitting.Accel.MonotoneOperators; "-cocoercive" is IsCocoercive L⁻¹ B. The resolvent is supplied as a family J : ℝ → H → H with the hypothesis that J γ is the resolvent of for every ; for maximally monotone such a family exists and is unique, so this loses nothing. Sequences are shifted by one index: Lean's x j is and z j is ; the values z 0, z 1 are never used. Weak convergence is for all , not norm convergence.
Committed conventions: is assumed (the step-size bounds divide by ); is assumed monotone in both cases, as printed; the constants of (41), (42), (43) and Lemma 4.2 are copied exactly. The resolvent hypothesis is not vacuous (the identity is a resolvent family of ), the step-size range is not shrunk, and the conclusion is weak convergence to a zero, not a weaker boundedness or cluster-point statement.
A complete development needs: the Lyapunov inequalities (milestones 2–6), Opial's lemma for sequential weak cluster points, weak sequential compactness of bounded sets in a Hilbert space, and weak–strong closedness of the graph of a maximally monotone operator. The last three are reusable well beyond this mission and contributions of them are welcome.
In many planning problems the decision changes the uncertainty it faces. Opening a facility raises the demand observed near it; a maintenance decision changes the failure distribution of a component; a price shifts the demand law. Decision-dependent uncertainty of this kind breaks the standard assumption of stochastic programming that the probability distribution is fixed in advance. When the distribution is in addition only partly known, the natural model is distributionally robust: the decision maker optimizes against the worst distribution in an ambiguity set whose shape itself depends on the decision.
X. Yu and S. Shen (arXiv:2002.12518v3, 2020; published in Mathematical Programming) study the multistage version of this model with binary state variables, and show that under three families of moment-based ambiguity sets each stage of the dynamic program can be rewritten as a single minimization, which can then be solved by stochastic dual dynamic integer programming (SDDiP). This mission formalizes the first family, Type 1, in which every moment is bounded above and below by decision-dependent functions.
Timeline. Two-stage decision-dependent DRO with moment bounds was reformulated by F. Luo and S. Mehrotra (Distributionally robust optimization with decision dependent ambiguity sets, Optimization Letters, 2020, arXiv:1806.09215), Theorem 3.1. SDDiP for multistage stochastic integer programs is due to J. Zou, S. Ahmed and X. A. Sun (Stochastic dual dynamic integer programming, Math. Program. 175(1–2):461–502, 2019, doi:10.1007/s10107-018-1249-5). Yu and Shen (2020) combine the two in the multistage setting, for Type 1 (moment bounds), Type 2 (mean and covariance) and Type 3 (Delage–Ye type) sets.
Fix one stage of the dynamic program. The state links stage to stage , and the stage variable is used only at stage . The pairs allowed at stage form the stage feasible set , and is the stage cost.
The random vector of stage takes one of values , the same for every decision (Assumption 3). What depends on the decision is the probability vector on these points. is the value of the next stage when the state is and scenario occurs.
Moment functions. For nonnegative integers , the moment functions are , , collected into .
Type 1 ambiguity set. For decision-dependent bounds and ,
Normalization is obtained by choosing one moment function with .
Stage Bellman equation. The stage value is
If is nonempty for every feasible , then (2) equals the joint minimization
In Lean, "equals" is the statement that for every real , is the attained minimum of (2) if and only if it is the attained minimum of (4).
With the moment constraints of (5)–(6) (normalization, first and second moments of each coordinate around affine decision-dependent empirical moments , ) and , , the stage value equals the joint program (7), whose objective (7a) has no -terms.
Theorem 1 removes the inner maximization from every stage of the multistage model. Without it, each stage is a min–max problem whose inner feasible set moves with the binary decision, and SDDiP's cut generation does not apply. After the reformulation, each stage is a single mixed-integer program whose only nonlinearities are products of a binary state with a continuous dual variable, which McCormick envelopes linearize exactly. The paper's facility-location experiments use exactly this route via (7).
The result is proved on paper by a one-line appeal to LP strong duality. No machine-checked version exists. The formal content this mission adds is the precise accounting of what the appeal needs: that the inner LP is bounded (from ), that its dual is attained, that the outer minimum transfers between the two formulations in both directions, and that the sign constraint is present. A Lean development also separates the parts that hold for arbitrary and from the paper's standing linearity and compactness assumptions.
The platform already has a general LP strong duality theorem, LinearOptimization.lp_strong_duality (Bertsimas–Tsitsiklis, Theorem 4.4, on a general-form LP structure; proved). It is a tool for the milestones, not a statement of this paper.
The inner problem is a finite LP, so the difficulty is not depth but bookkeeping that the paper leaves to the reader. Strong duality must be applied to an LP with four families of inequality rows plus sign constraints, with the moment rows written as sums of vectors. The obvious reading of (3) as printed — no — makes Theorem 1 false when has negative entries, because the free variable would force (4b) to be an equality. The equivalence of the two outer minima also needs care: (4) minimizes jointly over and the multipliers, so the attained minimum of (4) must be matched with a pair at which the inner maximum of (2) is attained, in both directions. For (7), the dual of (6) lacks the -terms of (4), so (7) is not a literal instance of Theorem 1: the redundancy of under , has to be used.
All declarations live in the namespace DDMomentDRO.Type1. States are Fin I → ℝ, stage variables Fin I → Fin J → ℝ, scenarios Fin K → Fin J → ℝ, all indices -based. The moment exponents are a matrix e : Fin m → Fin J → ℕ. is an arbitrary real function of : the theorems use nothing about the next stage, so the recursion is not formalized. The binary state is kept as a hypothesis on ; linearity of and compactness and polyhedrality of (p. 5) are dropped, a disclosed generalization. The ambiguity set includes (the proof's (C-17f)), which (3) as printed omits, and no normalization row is added. Minimum and maximum are IsLeast and IsGreatest of explicitly defined value sets, never sSup/sInf, so an empty ambiguity set or an unbounded inner problem cannot produce a junk value; nonemptiness of the ambiguity set at every feasible state is the theorem's hypothesis, as on the page. An empty stage set makes both sides of the equivalence false rather than vacuously true, so it does not trivialize the goal. The objective (7a) is transcribed term by term.
Contributions welcome: proofs of the two duality milestones (from the platform's LP duality or directly from Farkas' lemma in Mathlib), the transfer argument for Theorem 1, and the specialization (7).
Many convex problems met in practice — least squares with a rank-deficient matrix, dual problems of linearly constrained programs, with a strongly convex and a wide matrix — are not strongly convex: their optimal set is a whole affine piece rather than a point. The classical linear-rate theory of first order methods assumes strong convexity, yet these methods are observed to converge linearly on such problems as well.
Necoara, Nesterov and Glineur (arXiv:1504.06298v4, 2016; Math. Program. 175, 2019) introduce a hierarchy of relaxations of strong convexity, all measured relative to the projection onto the optimal set, and prove linear convergence of the projected gradient method, the fast gradient method and feasible descent methods under them. This mission formalizes the result on the fast gradient method (FGM) for the first and strongest relaxation, quasi-strong convexity: an accelerated linear rate, with in place of , under the condition that all extrapolated points share one projection onto the optimal set.
Nesterov's estimate-sequence technique (Nesterov, Introductory Lectures on Convex Optimization, 2004, §2.2) gives the rate for strongly convex functions. The paper shows that the same argument survives when strong convexity is replaced by the quasi-strong inequality at the projection, provided the projections of the points do not move.
Work in with the Euclidean inner product and norm . Problem (P) is
with closed and convex and convex and differentiable with -Lipschitz gradient: . The optimal set is assumed nonempty. For a closed set , denotes a nearest point of in .
is quasi-strongly convex with constant (Definition 1, inequality (10)) if, with ,
The condition number is .
The fast gradient method (FGM) starts from and iterates, for ,
The gradient mapping at is with .
The analysis uses the estimate functions of Lemma 1: for , , , and
If all iterates of (FGM) have the same nearest point in , then
The theorem gives the accelerated linear rate for a class strictly larger than the strongly convex functions. By Remark 1 (p. 27), on an unconstrained problem (FGM) keeps in , so the projection onto never moves; with Theorem 8 of the paper (quasi-strong convexity of for strongly convex smooth ) this covers such problems, and Section 6.1 applies it to consistent linear systems , where is not strongly convex when has a nontrivial kernel.
The result is proved in the paper; nothing here is open mathematically. It has no machine-checked proof: the Nesterov-method items already on the platform concern strongly convex or sublinear settings and do not cover quasi-strong convexity or the same-projection condition. A complete development produces a reusable formal estimate-sequence argument, the gradient-mapping inequality (29) for points outside the feasible set, and the quadratic-growth consequence of (10).
The estimate-sequence argument needs a quadratic lower model of at the point where it is evaluated. Under strong convexity this lower model holds between any two points; under quasi-strong convexity it holds only between a point and its projection onto . Lemma 1 evaluates at a single point for every , so it needs the projections of all to coincide; the obvious attempt to run the strongly convex proof with changing from step to step fails at the induction step (57). This is why the same-projection hypothesis is part of the theorem rather than an artifact.
The second difficulty is bookkeeping: condition (58) concerns the minimum of the recursively defined quadratics , which has no closed form in the statement, and it must be matched against the momentum step of (FGM); this is the only place where the specific value of enters.
EuclideanSpace ℝ (Fin n). The projection is the predicate IsNearest S u p ( minimises ), never a choice function; FGM runs are sequences satisfying this predicate at every step, with and 0-based indices (the page's "for " is a slip).QuasiStrongEverywhere). For , the case of Remark 1, these are exactly the paper's hypotheses.Many planning problems are solved in stages. A decision is taken, uncertainty is revealed, and the next decision reacts to it. Facility location, capacity expansion and network design all fit this pattern. In a growing class of such problems, the distribution of the uncertainty depends on the decision: opening a facility changes the demand it attracts, and a maintenance decision changes the failure rates that follow. Stochastic programs with decision-dependent uncertainty go back to Jonsbråten, Wets and Woodruff (1998) and Goel and Grossmann (2006).
When the distribution is not known exactly, distributionally robust optimization (DRO) optimizes against the worst distribution in an ambiguity set of plausible ones. Moment-based ambiguity sets, which are defined by constraints on the mean and covariance, are one of the standard choices (Delage and Ye, 2010). Luo and Mehrotra (2020) studied single-stage DRO in which such moment sets depend on the decision. Yu and Shen (2020) carry this into the multistage mixed-integer setting. Their goal is to rewrite each stage's min–max Bellman equation as one minimization, so that the stagewise decomposition algorithm SDDiP (Zou, Ahmed and Sun, 2019) applies.
This mission formalizes their reformulation for the Type 2 ambiguity set, which matches a decision-dependent mean and covariance exactly.
Fix a stage . The decision at stage is a pair : a binary state , passed to the next stage, and a stage variable . The pair must lie in a stage feasible set and costs .
The next-stage random vector takes one of finitely many values . This support is fixed (Assumption 3), and only the probabilities are uncertain. The value of being in state when scenario occurs is .
The decision determines a mean and a covariance matrix . The Type 2 ambiguity set is the set of probability vectors that match them exactly:
The Bellman equation (2) of stage is
Throughout, is the Frobenius inner product.
If is nonempty for every feasible , then
The left side is a minimum exactly when the right side is, and the two values agree.
The theorem turns a min–max problem into a single minimization. Under the paper's affine model (12) for and , and with McCormick envelopes for the products of binary states and continuous duals, that minimization becomes a mixed-integer linear program. SDDiP can then solve the multistage model stage by stage, with valid cuts. The Type 2 set is the paper's middle case. It captures correlations between the components of , which the separate moment bounds of the Type 1 set (Theorem 1) cannot, and it still has an LP dual. The Type 3 set of Theorem 3 instead leads to a semidefinite program.
The result is proved in the paper: Appendix C gives a short argument by linear-programming duality. It has not been formalized. A formal proof pins down details the printed proof leaves implicit:
It also yields a reusable, machine-checked instance of LP duality for moment-matching problems on a finite support.
There are two steps. The first is linear-programming strong duality for the inner problem in matrix-valued form. Its constraints are a scalar equation, a vector equation in and a matrix equation in , so the dual variables are a scalar, a vector and a matrix, paired through dot and Frobenius products. Turning this into a standard-form LP to which a library duality theorem applies takes bookkeeping. The second step is the exchange of the outer minimum with the dual minimum. Here attainment matters: the inner maximum must be attained at every feasible , and the stated equality must hold both when the outer minimum exists and when it does not. Weak duality alone gives only one inequality. The naive argument "dualize and combine" also hides the fact that, without , the dual constraints would have to be equalities.
Fin I → ℝ, stage variables are Fin I → Fin J → ℝ, the support is ξ : Fin K → Fin J → ℝ, and the next-stage values are an arbitrary function Qn x k. The theorem uses nothing about the recursion that defines . The covariance map is named Sig.IsLeast, IsGreatest), never sInf/sSup. The goal states that is the least stage value if and only if is the least value of (11). An empty stage set, or an empty ambiguity set, cannot make the statement hold by default values. The ambiguity set is never empty at a feasible state, because that is the theorem's hypothesis, and an empty stage set makes both sides false.First order methods (projected gradient, fast gradient) converge only sublinearly on general smooth convex problems, at rates and in function value. Linear convergence is classically proved under strong convexity, which fails for many problems arising in practice: least squares with a rank-deficient matrix, dual problems of linearly constrained programs, and compositions of a strongly convex with a singular linear map. For such problems the optimal set is not a single point, yet projected gradient methods are still observed to converge linearly.
Necoara, Nesterov and Glineur (arXiv:1504.06298, later Math. Program. 175 (2019)) introduce a hierarchy of relaxations of strong convexity, each obtained by evaluating a strong convexity inequality only at the projection of a point onto the optimal set, and show that first order methods converge linearly on each class. Two of these relaxations are the subject of this mission: quadratic functional growth and the global error bound stated with the gradient mapping. Error bounds of this kind go back to Luo and Tseng (Ann. Oper. Res. 46 (1993)) and Tseng's analysis of feasible descent methods; quadratic growth conditions appear in Anitescu and in Drusvyatskiy–Lewis (Math. Oper. Res. 43 (2018)).
Work in with the Euclidean inner product and norm . Problem (P) is
with closed and convex and convex on , differentiable on , with Lipschitz continuous gradient of constant on : for all . The optimal set is assumed nonempty.
For a set and a point , denotes a point of nearest to ; for nonempty closed convex it exists and is unique. Write . The projected gradient step from is , and the gradient mapping is
When , .
The condition number is . In Lean these are QuadFunGrowth X f κ and ErrorBound X f Lf κ, with written Lf • (x - xp).
Quadratic functional growth with constant implies the global error bound with constant :
In class notation, .
The converse direction, also included as a draft theorem: the error bound with implies quadratic functional growth with constant .
Theorems 6 and 7 together show that, for convex functions with Lipschitz gradient on a closed convex set, quadratic functional growth and the gradient-mapping error bound define the same class of functions up to a change of constant depending only on . A linear convergence proof for projected gradient methods under one condition therefore transfers to the other, and the paper uses this to place the error-bound class inside its hierarchy of relaxations of strong convexity. The explicit constant matters downstream: rates of the form inherit it.
The results are proved in the paper. No machine-checked proof of Theorems 6–7 is known to exist. Related statements formalized elsewhere on the platform concern the unconstrained case (Karimi–Nutini–Schmidt, where replaces ) or the proximal-gradient error bound on sublevel sets (Drusvyatskiy–Lewis), with different constants. A complete development here yields a reusable library of projected-gradient facts on a general closed convex set: the descent inequality, the gradient-mapping inequality and the existence and characterization of projections.
The obvious approach applies (22) at and tries to bound by , as in the unconstrained case where and convexity gives . On a constrained set this fails: is not a subgradient of at , and the available inequality for the gradient mapping, (29), controls only through the value at a different point. Relating the distance to at that point to the distance at , without losing the exact constant , is the central difficulty.
At the Lean level, the descent inequality (2) has to be derived on a convex set from a Lipschitz condition assumed only on , and the variational characterization of the Euclidean projection has to be connected to the nearest-point predicate.
EuclideanSpace ℝ (Fin n). is a real function on all of , convex on (ConvexOn ℝ X f), differentiable at every point of , with = gradient f; its values off never enter.IsNearest), not choice functions; is the predicate IsPGStep. Every statement quantifies over all points satisfying them. Nearest points in nonempty closed convex sets exist, so these quantifiers are not vacuous.A trivializing formalization is ruled out: the error bound uses the gradient mapping and not , the projections are not defined by choice, is nonempty, and no junk gradient value off the differentiability set is used.
Needed infrastructure: the descent lemma on a convex set, the obtuse-angle characterization of the projection onto a closed convex set, existence of nearest points (Mathlib's exists_norm_eq_iInf_of_complete_convex), and closedness and convexity of . These are reusable well beyond this mission; proofs of the milestones and of Theorem 6 are welcome independently.
Linear convergence of gradient-type methods is classically proved under strong convexity. Many problems that arise in practice are not strongly convex: dual formulations of linearly constrained convex problems, least-squares and logistic-type regression with rank-deficient data matrices, convex quadratic programs, and routing problems in data networks all have objectives of the form , where is strongly convex and smooth but the matrix has a nontrivial kernel. Such an is constant along , so it is not strongly convex, and its set of minimizers need not be a single point.
Necoara, Nesterov and Glineur (arXiv:1504.06298v4, published in Math. Program. 175 (2019)) introduce a chain of relaxations of strong convexity: quasi-strong convexity, quadratic gradient growth and quadratic functional growth. They show that projected and fast gradient methods still converge linearly under them. Section 4 of the paper supplies the main examples: compositions , possibly with a linear term and polyhedral constraints. This mission formalizes those examples. The tool behind them is the error bound of Hoffman (1952) for systems of linear inequalities; its use for linear convergence goes back to Luo and Tseng (1993) and Wang and Lin (2014).
Work in with the Euclidean inner product and norm . For a set and a function , the optimal set is and is the optimal value. A nearest point of a set to is a point of minimizing over .
The data are:
The objective is , or in the extensions. The function has Lipschitz gradient with constant on if for . It is quasi-strongly convex with constant if, for every and ,
The class collects the convex functions with -Lipschitz gradient on satisfying this inequality with . The classes (quadratic gradient growth, ) and (quadratic functional growth, ) are defined the same way.
A Hoffman constant for the polyhedron is a number with
where is the componentwise positive part.
If is optimal for and is a Hoffman constant for , then
Theorem 8 makes the linear convergence results of the paper apply to the whole family over polyhedra. That family covers the duals of linearly constrained strongly convex problems and regression with arbitrary design matrices. The rate is explicit in , , and the Hoffman constant. Theorems 9 and 10 extend the picture to a linear term, at the cost of moving to weaker classes. Example 1 shows that the sublevel restriction in Theorem 10 is needed.
All of these results are proved in the paper. None of them has a machine-checked proof that this mission is aware of. A formal development would produce a Lean proof of the class membership, a formal chain-rule computation of the gradient of , and the strict-convexity argument that is constant on the optimal set. These pieces are reusable wherever a composite objective with a rank-deficient linear map appears.
The obvious route, strong convexity of , fails as soon as . Two separate facts have to replace it. The first is that the minimizers of a strongly convex function composed with share the image point , so the optimal set is itself a polyhedron. The second is that the distance to that polyhedron is controlled linearly by the residual on feasible points, which is exactly a Hoffman error bound. Neither follows from local information at a single minimizer. In Theorem 10 the linear term destroys the first fact's simplicity: the value must also be controlled, and that is possible only on bounded sublevel sets.
is EuclideanSpace ℝ (Fin n). and are continuous linear maps, so is the operator norm, which is the spectral norm of the page; it is never the Frobenius norm. Strong convexity is Mathlib's StrongConvexOn Set.univ σg g, which is (5) on all of . The page's "-Lipschitz gradient on " is read on , the domain of . The gradient of the composition is always gradient (fun z => g (A z)), and the identity is a proof step, not part of any statement. is the value at a nearest point of , which is exact because that point is optimal.
Standing assumptions of p. 3: the feasible set is closed and convex (automatic for a polyhedron), the optimal set is nonempty (a named optimal point is a hypothesis), and has Lipschitz gradient (a conclusion here). The "simple" set and "closed" function add no mathematical content and are dropped. The Hoffman constant is a hypothesis, because the page cites its existence (Hoffman 1952) rather than proving it. The hypothesis is the Hoffman inequality for the specific polyhedron , not for every right-hand side.
Trivializing formalizations are ruled out. The projection is a predicate (IsNearest), never a choice function. The optimal set is nonempty by hypothesis. is differentiable everywhere, so no gradient takes a junk value. A sorry-free sanity file shows that the hypotheses of Theorems 8–10 are jointly satisfiable ( on , , ).
A complete development needs the chain rule for gradients through a continuous linear map and its adjoint, first-order characterizations of strong convexity, and optimality conditions for convex differentiable functions on convex sets. Contributions of these as reusable lemmas are welcome, as are proofs of the companion theorems.
Strategic planning of an open pit mine decides, over a horizon of 20 to 50 years, which parts of an ore body are excavated, when, and where the excavated material is sent. A deposit is discretized into blocks, often millions of them, and the decisions are constrained by wall-slope precedences between blocks, by mining and processing capacities, and by blending and other operational rules. The resulting mixed-integer programs are far beyond the reach of general-purpose solvers, so practitioners and researchers rely heavily on preprocessing: rules that provably remove variables before the model is solved.
The oldest such rule is the ultimate pit limit. Lerchs and Grossmann (1965) showed that the most profitable pit, ignoring time and capacities, is a maximum-weight closure of the precedence graph and can be computed by a graph algorithm. Caccetta and Hill (2003) used this limit to eliminate blocks in the capacitated pit problem (C-PIT), where each block has a predefined destination. Rivera Letelier, Espinoza, Goycoolea, Moreno and Muñoz (Operations Research, 2020) extend that result to the general precedence-constrained production scheduling problem with clusters (PCPSP-C) of Bienstock and Zuckerberg (2009): multiple destinations per block, clusters of blocks extracted together, arbitrary nonnegative side constraints, and either full or partial integrality. This mission formalizes that extension, Theorem 1 of the article, together with the surrounding claims of §2 and §4. The source is the published Operations Research article; all page numbers are journal pages.
A PCPSP-C instance consists of a finite set of blocks , destinations , and periods . Sending block to destination is worth (possibly negative); in period it is worth for a discount rate . A relation means that must be extracted no later than . The blocks are partitioned into clusters , with the cluster of ; clusters inherit precedence ( if some block of precedes some block of ), this relation is assumed to be a partial order, and is the set of immediate precedences: when immediately precedes . Blocks have weights , and a matrix inequality collects all side constraints (capacities and others).
The variables are , the fraction of cluster extracted in period , and , the fraction of block sent to in period . The PCPSP-C maximizes subject to
and to an integrality condition: full () or partial (once a cluster has started, each of its immediate predecessors must be completely extracted). An optimal solution is minimal if no other optimal solution lies componentwise below it.
With , the ultimate pit limit problem U-PIT is the linear program
The pit limit of a vector is ; for a PCPSP-C solution it is the pit limit of .
If and , then for either integrality condition, every minimal optimal solution of the PCPSP-C and the minimal optimal solution of U-PIT satisfy
Theorem 1 turns an expensive mixed-integer program into a smaller one using a single maximum-closure computation that ignores time and resources: every cluster outside can be deleted from the instance. In the article's computational study this preprocessing is part of the pipeline that solves industrial instances to near-optimality. The result covers the partial-integrality models used in commercial mine-planning software, not only the full-integrality model of the earlier literature.
The article's proof of Theorem 1 is in an online e-companion; the companion claims of §2 and §4 are stated in the text with brief or cited justifications (claim (b) is attributed to the maximum closure literature, Hochbaum 2008). None of these results has a machine-checked proof. The mission produces a formal model of the PCPSP-C that the sibling missions of this series (clique, variable-right-hand-side and hourglass cuts) share, and a verified justification of a preprocessing step in practical use.
The obvious argument, "a cluster outside the ultimate pit has nonpositive value, so drop it", fails on two counts. First, value is not additive over clusters: U-PIT optimality only says that the clusters outside that can be added to it as a closed set have nonpositive total value, not that each cluster outside it does. Second, the PCPSP-C is a multi-period problem in which a cluster may be extracted in fractions over several periods with different discount factors, and with side constraints that may forbid extracting it at all. The statement therefore depends on the discount factors being decreasing in time, on the side constraints being monotone (), and on minimality of the PCPSP-C solution, without which an optimal solution may also extract clusters of zero value outside the limit.
Everything lives in the namespace OpenPitMIP.UltPit. An instance is a structure over finite types of blocks, destinations and clusters, with periods Fin T (index is period , so the discount factor is ). Block precedence is primitive; cluster precedence and the arc set (the transitive reduction) are derived from it, and the precedence rows (4) and (13) range over only. The standing assumptions of §2.1 are bundled in one hypothesis: the clusters partition the blocks (every cluster is nonempty), cluster precedence is a strict partial order, , and . The integrality condition is a parameter ranging over {full, partial}, and Theorem 1 is stated for both. Optimality and minimality are taken over the whole feasible set, with the componentwise order on the pair . At least one destination is assumed, so that exists. U-PIT is the linear program over , not a binary closure problem.
The theorem is not trivialized: no minimal optimal solution is assumed to exist beyond what the hypotheses give, the discounting is part of the model (with arbitrary period values the theorem is false), and the hypotheses are jointly satisfiable (one block, one cluster, one period, , with the zero solution minimal optimal in both problems).
Contributions welcome: proofs of the milestones, a proof of Theorem 1, and reusable lemmas on closure polytopes (lattice structure, binary minimal optima), which are of interest beyond mining.
A chance-constrained program minimizes a cost over a closed set subject to a constraint that must hold with high probability rather than surely:
where is a random vector, collects the uncertain constraints, and is the tolerated risk. Such models are used in power-system dispatch, portfolio selection, and supply-chain and process design, wherever a constraint may be violated in rare scenarios at a controlled rate.
The probability is rarely computable, so in practice it is replaced by an estimate from an i.i.d. sample . The empirical frequency is a step function of and yields a mixed-integer program. Peña-Ordieres, Luedtke and Wächter (arXiv:1905.07377v2; SIAM J. Optim. 30(3), 2020) replace the indicator by a smooth approximation, which turns the sample problem into a smooth nonlinear program that standard solvers can handle. The question this mission addresses is whether a point accepted by the smoothed sample problem is actually feasible for the true chance constraint, and with what probability.
Timeline. Luedtke and Ahmed (SIAM J. Optim. 19 (2008)) proved finite-sample feasibility guarantees for the empirical (non-smooth) sample approximation, first for finite and then, under a Lipschitz condition on , for bounded (their Theorem 10). Peña-Ordieres, Luedtke and Wächter (2020) extended these guarantees to the smoothed approximation (Theorems 3.8, 3.11 and 3.13 of the preprint).
Let and let be admissible: strictly decreasing, symmetric in the sense , and such that the smoothed indicator
is differentiable on . The paper's concrete choice is a quartic-kernel polynomial (its (2.6)).
For a decision and a level , define
The true feasible set is , and the shifted sample feasible set with shift and sample risk level is
Throughout, has a continuous distribution for each (Assumption 3.1). The margin of a point is ; Assumption 3.7 asks that and .
Suppose is bounded with sup-norm diameter , that for all with probability one (Assumption 3.12), and that Assumption 3.7 holds with and . Then for every ,
The result. Theorem 3.13 gives an explicit, non-asymptotic sample size under which every point accepted by the smoothed sample problem (with a small shift and a slightly tightened risk level ) is feasible for the original chance constraint, uniformly over an infinite decision set. Solving the smooth approximation therefore yields certifiably feasible solutions with a quantified failure probability, the bound depending on the dimension only through the covering number . Corollary 3.9 adds that, under a monotone density near zero, the unshifted smoothed approximation is conservative.
Formalizing it. The results are proved in the paper; none is formalized anywhere to our knowledge. A formal development would produce a machine-checked one-sided Hoeffding bound for averages of bounded functions of an i.i.d. sample, a union bound over a finite candidate set, and a sup-norm covering lemma, assembled into a uniform feasibility guarantee. These ingredients are reused across the sample-average-approximation literature.
The obvious argument is a union bound over , which fails for infinite : the event involves uncountably many points, and is not even obviously measurable. Discretizing by a sup-norm grid is not enough on its own either: a grid point may be infeasible while nearby points are feasible, and the true cdf need not be continuous in . The paper's device is to discretize simultaneously in and in the value of , which requires covering each level slice separately and then transferring sample feasibility from a point to its representative, at the price of the shift and the level change . Keeping the constants exactly as printed, with slices and points per slice, is part of the task.
Fin n → ℝ, whose Mathlib norm is the sup norm used in Assumption 3.12 and Theorem 3.13. is closed (the paper's standing hypothesis).ProbabilityTheory.measure_sum_ge_le_of_iIndepFun with hasSubgaussianMGF_of_mem_Icc_of_integral_eq_zero); and Corollary 3.10, whose printed exponent does not follow from its proof.Contributions welcome: proofs of any milestone, in particular the sup-norm covering lemma and the Hoeffding step, which are reusable beyond this mission.
First-order methods (projected gradient, fast gradient, feasible descent) converge linearly on smooth strongly convex problems, but many problems met in practice are not strongly convex: least squares with a rank-deficient matrix, the dual of a linearly constrained problem, or with strongly convex and singular. Such problems have a whole set of minimisers, and strong convexity, which forces a unique minimiser, fails. Necoara, Nesterov and Glineur (arXiv:1504.06298; Math. Program. 175 (2019)) introduce a family of conditions that relax strong convexity by testing it only against the projection onto the optimal set, and prove that the classical first-order methods still converge linearly under them.
Related unconstrained conditions predate the paper: restricted strong convexity for (Zhang and Cheng, Optim. Lett. 2015, the paper's reference [16]), and the error bounds of Luo and Tseng (1993). Karimi, Nutini and Schmidt (arXiv:1608.04636, 2016) compared similar unconstrained conditions with the Polyak–Łojasiewicz inequality. The constrained hierarchy treated here, with one constant along the whole chain, is the first section of the Necoara–Nesterov–Glineur paper and the basis of its convergence results.
This mission formalizes that hierarchy: Theorem 4 of the paper (arXiv v4, p. 9) and the results it is assembled from.
Let be a closed convex set, with the Euclidean inner product and norm . Let be a convex function on , differentiable at every point of , with gradient Lipschitz on with constant :
The optimal set is assumed nonempty, and is the optimal value. For , denotes the projection of onto : the point of nearest to .
For a constant the paper considers five inequalities, for all :
The classes , , , , are the convex functions satisfying (1) and, respectively, (7), (10), (17), (13), (22). In Lean these are the predicates StrongIneq, QuasiStrong, QuadGradGrowth, QuadUnder and QuadFunGrowth of NecoaraNG.Chain.Setting, over optSet X f and the nearest-point predicate IsNearest.
With the same constant at every step,
that is
The goal is the conjunction of the four implications under the standing assumptions.
A companion item states the remark on p. 7: for convex , (10) alone or (13) alone gives (17) with constant .
The chain gives the hierarchy that the paper's convergence theorems are stated for: the projected gradient method converges linearly on and, in distance to , exactly on ; the fast gradient method keeps its accelerated rate on ; and with strongly convex is in on a polyhedron. Each such result transfers down the chain once the inclusions are known, and the fact that one survives every link is what keeps the rates' constants explicit.
All the statements are proved in the paper. None of them is formalized: the platform has unconstrained analogues (the Karimi–Nutini–Schmidt chain, with an existential constant and no feasible set), but no constrained statement and no statement with a fixed constant. A formal proof would also check the projection-invariance step that the paper uses without comment.
The links and are one-line substitutions. The substance is in Theorems 1 and 3, and specifically in the constant: combining (10) or (13) with the convexity inequality at a single pair of points gives (17) only with constant (the companion item), and the same loss of a factor 2 appears in a direct derivation of (13) from (10). Keeping the full constant is what makes (23) a chain of inclusions with one index, and it is where the geometry of the optimal set enters: the conditions are tested only against the projection , which moves with . Convexity of cannot be dropped: (10) alone does not even imply convexity (p. 5).
EuclideanSpace ℝ (Fin n); is Mathlib's gradient f. The function is defined on all of , with differentiability assumed at every point of ; "continuously differentiable" on follows from (1).ConvexOn ℝ X f), (1) with , a minimiser , . "Simple" (cheap projection) and "closed" for carry no mathematical content here and are dropped.IsNearest (optSet X f) x xbar; each condition is required for every nearest point. is written , which is exact because .StrongConvexOn.The column-subset selection problem (CSSP) asks for columns of a real matrix whose span approximates all of as well as possible in squared Frobenius norm. It is a basic primitive of low-rank approximation, feature selection and numerical linear algebra, studied both for its exact complexity and for approximation algorithms (see Boutsidis, Drineas and Magdon-Ismail, doi:10.1137/12086755X, cited as [2] in the source paper).
Sviridenko, Vondrák and Ward study submodular maximization and supermodular minimization when the objective has bounded total curvature, a parameter introduced by Conforti and Cornuéjols that measures how far a monotone set function is from being linear. Their guarantees improve as decreases. Section 8 of the paper applies this to CSSP: it bounds the curvature of the CSSP objective in terms of the condition number of , so that a well-conditioned matrix has small curvature. This mission formalizes that bound (Lemma 8.2) and the steps of its proof.
Let be a real matrix with columns , so that for , and let be the Euclidean norm. For write for the orthogonal projection of onto , the point of that subspace nearest to (). The CSSP objective is
the squared Frobenius distance from to the nearest matrix whose columns lie in the span of the selected columns.
For a set function on a finite set , the marginal value of at is . The function is monotone decreasing if every . Following (1.1) of the paper, a monotone decreasing has total curvature at most when, for every ,
i.e. the last marginal of is at least a fraction of its first marginal in absolute value.
When the columns of are linearly independent, the condition number is
For with linearly independent columns,
Items 1–7 hold for arbitrary columns; only item 8 and the goal assume independence.
Lemma 8.2 turns a spectral quantity into a combinatorial one. With it, any curvature-dependent guarantee for monotone decreasing set functions can be stated for CSSP in terms of . The paper's Lemma 8.3 shows the bound is asymptotically tight, so is the right order of the curvature.
There is a caveat that the formalization makes explicit. The paper deduces from Lemma 8.1 that is supermodular, and on that basis quotes its supermodular-minimization algorithm for CSSP with factor (p. 12). Both the submodularity half of Lemma 8.1 and the supermodularity of are false as printed. With , and in , the function has . With columns , . A small perturbation gives a counterexample with independent columns. This is the "suppressor variable" phenomenon of regression. The curvature bound itself does not depend on supermodularity and is true, so it is the goal here. The approximation factor for CSSP is not posed, because it rests on the false claim and is stated with .
As far as is known, none of these statements has a machine-checked proof. The results are proved on paper, except the two false claims above. The mission adds a formal proof of the curvature–conditioning bound, and makes explicit which parts of §8 survive.
The individual steps are short linear algebra, but they rest on infrastructure that has to be assembled: orthogonal projections onto spans of finite column families, the Pythagorean identities that relate to projections, and the variational characterization of and of over the unit sphere.
The paper's own route to the large unit vector (milestone 5) does not work as printed. It sets and uses , which is false when , so the signs of the inner products have to be accounted for. In the final step, the ratio is a quotient of two negative numbers. Comparing it with requires the supremum to be finite and the infimum to be strictly positive, which is exactly what independence of the columns provides.
c : Fin n → EuclideanSpace ℝ (Fin m), and is ∑ j, x j • c j. Subsets of are Finset (Fin n). is Finset.univ.erase i and is insert i S.Submodule.starProjection onto Submodule.span ℝ (c '' S), which is finite-dimensional, so the argmin of the page exists and is unique.⨆ and ⨅ of over the unit-sphere subtype of . It is used only under LinearIndependent ℝ c, the page's "non-singular", where both are finite and positive. The page's for dependent columns is not encoded.Useful infrastructure that would be reusable beyond this mission includes Pythagoras for starProjection, monotonicity of projection norms under inclusion of subspaces, and extremal characterizations of and . Contributions of any of the milestones, or of these general lemmas, are welcome.
Strategic open pit mine planning decides which parts of an ore body are excavated, in which period, and to which destination (a processing plant, a stockpile, a waste dump) each block of material is sent. Rivera Letelier, Espinoza, Goycoolea, Moreno and Muñoz (Operations Research 68(5), 2020) model this as a mixed-integer program, the precedence-constrained production scheduling problem with clusters (PCPSP-C), which extends the PCPSP of Bienstock and Zuckerberg (2010) by grouping blocks into clusters that are extracted together. The integer versions of the model have weak linear relaxations on production scheduling instances, so the authors derive cutting planes. Their production cuts (§5.2) exploit the capacity of a single destination together with the precedence structure. This mission concerns the second family of production cuts, the hourglass cuts: they bound how much material must be sent away from a capacitated destination once a cluster is started, using both the predecessors and the successors of that cluster.
Valid inequalities for precedence-constrained knapsack problems have been studied since Boyd (1993) (cited on p. 1433); the paper's contribution is the extension to several destinations, several periods, clusters and partial integrality, the condition used in commercial mine planning software.
All page references are journal pages of the published Operations Research article.
An instance has finite sets of blocks, of destinations and of clusters, the latter a partition of , and periods . Block lies in cluster and has weight . A precedence relation on blocks induces one on clusters ( if some block of precedes some block of ), assumed to be a strict partial order. The arc set is its transitive reduction: when is an immediate predecessor of . The closure is and the reverse closure ; is the set of blocks of a set of clusters, and is the total weight of a set of blocks.
Variables give the fraction of cluster extracted in period and the fraction of block sent to destination in period . The constraints (2)–(7) of p. 1427 are
with an integrality condition: full integrality (10), , defines the PCPSP-F, and partial integrality (11), " implies for ", defines the PCPSP-P. The rows include the destination capacity rows (9), . The cuts are written in the cumulative variables (17).
The simplified setting of §5.2.1 is the mode-knapsack set MK (p. 1433): for a directed acyclic graph , weights and a capacity , the triples with , , , and for every arc . Here is processing and is waste.
Let , , , and let be a set of blocks with . With , the inequality
is valid for the PCPSP-C, that is, for both the PCPSP-F and the PCPSP-P.
In the computational study of §8 (Table 5, p. 1440; discussion on p. 1442) the authors add early start, lifted clique, VRHS and hourglass cuts to the LP relaxation and drop one class at a time; they observe that all classes improve the bound and that the hourglass cuts have the most significant impact. Display (38) makes the separation of the most violated hourglass cut a single pass over the blocks for each cluster, destination and period window. The cuts are valid under partial integrality, the weaker condition that mine planning software imposes, so they strengthen the relaxation of the model actually solved in practice.
Theorem 8 is proved in the paper by a direct calculation; no machine-checked proof exists. A formal proof would certify the inequality in exactly the generality of the model (clusters, several destinations, several periods, both integrality conditions), and the formal model of the PCPSP-C built for it is shared with the other missions of this series.
The inequality is false for the LP relaxation: a fractional start of need not force its predecessors to be complete. Every proof therefore has to use integrality, and the two integrality conditions behave differently. Under partial integrality (11) the implication "started implies predecessors complete" is stated only along the arcs of the transitive reduction , and has to be propagated along chains of immediate predecessors to reach every predecessor of . The capacity step needs that the strict predecessors, itself and its strict successors are pairwise disjoint block sets, which is where the strict partial order is used. The terms are cumulative from period 1 while the terms are summed from ; the two must not be aligned.
Periods are Fin T, so index denotes period . Cluster precedence is derived from the block relation, and is its covering relation. The standing assumptions of §2.1 (clusters partition the blocks, a strict partial order on clusters, discount rate , weights ) are a single hypothesis on the instance. "Valid for the PCPSP-C" is stated as: for each integrality condition, at every feasible whose destination capacity rows (9) hold, which is the page's assumption that (9) is among the rows . The destination , unbound on the page, is a fixed arbitrary destination. In Theorem 8 is a set of blocks and is the weight of together with the blocks of . In MK an arc means precedes , and is reachability in .
Reading "valid" as "valid for the LP relaxation" would make the goal false, while dropping the condition , or the capacity rows, would make it a different statement; neither is the target. In (38) the maximum is taken over all as on the page, without the side condition , which need not satisfy.
A complete development needs only finite sums, finsets and the transitive closure of a relation from Mathlib. Proofs of the milestones, of the MK results and of the goal are all welcome; the lemma that partial integrality propagates along chains of arcs is reusable across all production cuts of the paper.
Unit commitment (UC) is the daily scheduling problem of electricity system operators: decide which generators are switched on in each hour of the next day, and how much each produces, so that supply meets the net load at minimum cost while respecting generation limits, ramping limits and transmission limits. With growing shares of wind and solar power, the net load is uncertain at the time the commitment is fixed. Adaptive robust UC protects the schedule against every net-load trajectory in an uncertainty set.
Lorca, Sun, Litvinov and Zheng (Oper. Res., 2016) argue that the dispatch must be nonanticipative (the output at hour may depend only on loads observed up to ) and propose a multistage robust UC model. To make it computable they restrict the dispatch to affine policies of the observed loads, in the spirit of Ben-Tal, Goryashko, Guslitzer and Nemirovski (Math. Program. 99, 2004). The paper solves the model on the IEEE 118-bus test case and on the 2718-bus Polish system. The two results of this mission are what makes the simplest such policy cheap to solve: under it, the semi-infinite robust constraints on generation, ramping and energy balance collapse to finitely many deterministic constraints.
There are generators , load nodes and periods . A net-load trajectory is , and its total load in period is . The budget uncertainty set (3) is
with nominal loads , deviations and a conservativeness parameter .
The -policy (10) sets the output of generator in period to an affine function of the current total load,
and the -policy (9) is the special case in which does not depend on . Given commitments , output limits and ramp rates , the robust constraints of the affine model (8) require, for all : generation limits (8c); ramping limits ((8d), (8e)); and energy balance (8g).
The extreme total-load scenarios are a trajectory whose total load is maximal over in every period (19), a trajectory whose total load is minimal in every period (20), and the mixed scenarios
of (21), (22).
Under the -policy (or the -policy), for every generator and period :
For a full-dimensional uncertainty set, the robust energy balance (8g) holds if and only if and for all ((15)); for the -policy, and ((14)).
Proposition 6 removes the constraints (8c)–(8e) from the constraint-generation loop of the affine robust UC: they can be imposed before the algorithm starts, through two scenarios per generation constraint and four per ramping constraint, leaving only the worst-case cost constraint and the transmission constraints to be separated. Proposition 4 turns the semi-infinite energy balance into linear equalities. Together they are the reason the -policy scales to the 2718-bus system in the paper's experiments.
Both results are proved in the paper, and the proofs are short. No machine-checked version is known. The formalization fixes the exact handling of the first period (the initial dispatch ), the exact definition of the mixed scenarios, and the dependence of part (ii) on the product structure of , all of which the paper leaves implicit or states loosely.
Part (i) needs only that the constraint is affine in the scalar total load of one period. Part (ii) is where the obvious argument fails: the ramping constraint couples two periods, and a set that is not a product over periods may not contain a trajectory that is simultaneously maximal in period and minimal in period . The separability of is exactly what puts and in . The labels the paper attaches to (25a) and (25d) are swapped relative to (21)–(22); following them literally sends the argument to the wrong scenario.
Fin Ng, Fin Nd, Fin T; trajectories are Fin T → Fin Nd → ℝ. Periods are 0-based: Lean period t is the paper's period , so "periods " in (21)–(22) are the Lean periods s < t.EReal, under the standing assumptions , that make every nonempty and bounded.The development needs only finite sums, products of sets, and order facts about affine functions; it reuses nothing beyond Mathlib. Proofs of the milestones, the goal and Proposition 4 are welcome.