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.
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?
Finding a point that satisfies a finite system of linear inequalities is the feasibility problem underlying linear programming, and it is also the basic step of many methods in signal and image reconstruction, where the system is too large to be solved by elimination. The relaxation method attacks it one inequality at a time: from the current point, move towards the half-space that is violated the most. Each step costs one pass over the rows and no factorization, which is why this family of iterations (with its relatives: Kaczmarz's method for equations, the projection methods for convex feasibility, and the perceptron algorithm) has been studied continuously since the early 1950s.
Timeline:
This mission is the first of three built on the Motzkin–Schoenberg paper: it covers the full-dimensional case, Theorem 1.
Let be -dimensional Euclidean space. A system of linear inequalities
is given by rows and constants . The -th inequality defines the closed half-space , and the set of solutions is the polytope . The system is assumed consistent, so is nonempty. The dimension of is the dimension of its affine hull; means that is not contained in any hyperplane.
Fix a relaxation parameter with . From a point one relaxation step is:
For , is the mirror image of in the boundary hyperplane of . Iterating from a starting point gives a sequence ; the process terminates when some , and otherwise produces an infinite sequence of points outside .
A sequence of points outside is Fejér-monotone with respect to if and for all and all .
Assume and . For every starting point and every choice of farthest half-space at every step:
The goal is the paper's theorem as stated, both cases in one statement. It fixes no constants and no rates.
The result. Case 1 guarantees that the relaxation method never diverges or oscillates: it either solves the system or converges to a boundary solution. Case 2 gives more: for full-dimensional solution sets the reflexion method is a finite algorithm for linear feasibility. Remark 3(b) of the paper shows that this is special to : for each there are planar examples where the iteration never stops. The companion missions of this series treat (Theorem 2, where reflexion may settle on a sphere around the affine hull of ) and reflexion in a general bounded convex set (Theorem 3).
Formalizing it. Both cases are proved in the paper; to our knowledge none is formalized in Lean or Mathlib. The mission produces a reusable model of relaxation for linear inequalities and a Lean proof of a general convergence statement for Fejér-monotone sequences, which also applies to other projection methods. Formalizing the proof in the order of the paper (Lemma 1, then §§5–6) is the intended route; alternative proofs are welcome.
The first idea is that monotone distances to every point of force convergence. They do not in general: Fejér-monotonicity only bounds the sequence and makes each distance converge, and when lies in a hyperplane a Fejér-monotone sequence can keep oscillating between two mirror-image points. Convergence genuinely needs the full dimension of , and the formal argument has to use that hypothesis in an essential way.
For Case 2, the difficulty is that a reflexion step does not shrink the distance to points of on the reflecting hyperplane, so there is no uniform decrease to count. Termination must also use that the system has finitely many inequalities: for the infinite family of supporting half-spaces of a convex body, treated in the third mission of this series, reflexion need not terminate. A proof that works for a single step, or one that uses a fixed tie-breaking rule, does not cover the statement.
EuclideanSpace ℝ (Fin n); the rows are vectors a i, and is inner ℝ (a i) x. Half-spaces are closed. Distances to sets are Metric.infDist.IsRelaxStep a b lam p p', and any maximizing index is allowed at every step. The paper makes the step single-valued by "some pre-assigned rule"; quantifying over all runs of the relation covers every such rule, so each theorem is at least as strong as the paper's.p : ℕ → E in which each point outside is followed by a relaxation step (IsRelaxRun). Termination is ∃ N, p N ∈ A; an infinite sequence is ∀ ν, p ν ∉ A. Every theorem is stated for every run, never for one run.lam, because λ is a Lean keyword.affineSpan ℝ A = ⊤, following the paper's own gloss " is not contained in any hyperplane". "Boundary" is frontier A, and convergence is Tendsto p atTop (𝓝 l).affineSpan ℝ A = ⊤, which includes the paper's polytope.Useful infrastructure: the closed form for and the nearest point in a half-space; the characterization of via a nonempty interior for convex sets. The Fejér-monotone convergence lemma and the half-space projection lemmas are reusable beyond this mission.
Computing the convex hull of a disjunctive set — a union of finitely many polyhedra — is generally hard in direct proportion to how many polyhedra are in the union: Chapter 2's Theorem 2.1 gives a compact lifted description, but working with it still means reasoning about all the disjunctions of the program simultaneously. A natural question, with obvious practical consequences for integer and combinatorial optimization, is whether the convex hull can instead be built up incrementally: impose one disjunction, take the convex hull of what results, then impose the next disjunction on that, and so on. If this "sequential convexification" procedure always reached the true convex hull, computing facets of a hard disjunctive set would reduce to a sequence of much easier single-disjunction computations. Balas shows the answer is negative in general — a two-variable integer program is a standard counterexample — but identifies an important class of disjunctive programs, the facial ones, for which sequential convexification always works. This class includes 0-1 programming (pure or mixed), nonconvex quadratic programming, separable programming, and the linear complementarity problem, though not general integer programming.
Let . A disjunctive program in conjunctive normal form has constraint set
for a finite set and, for each , a finite set of halfspace data — one elementary disjunction per . The program is facial if every inequality appearing in some disjunction defines a face of , i.e. is an extreme subset of for every such . Fixing an ordering of , the sequential-convexification recursion sets (step zero) to be the base polyhedron and, for each subsequent step, imposes the next disjunction and reconvexifies: .
For the necessity direction, write and, reversing every inequality, .
This is the weakest correct statement of the recursion's endpoint: it asserts the sequential procedure reaches exactly (not, say, some fixed superset), and — since is universally quantified — that this holds regardless of the order in which disjunctions are imposed.
for a union of finitely many polyhedra and opposite halfspaces .
The results themselves. Theorem 3.1 is what makes sequential convexification a practical tool rather than a theoretical curiosity: for a 0-1 program with binary variables, it lets the convex hull be built in stages, each requiring only the facets of a two-term disjunction — tractable, in contrast to generating facets of the full integer hull directly. Theorem 3.3 puts the boundary of applicability on rigorous footing: faciality is sufficient but not necessary, and Theorem 3.3 pins down the exact condition, showing precisely why sequential convexification is a genuinely restrictive property (holding for 0-1 programs but not general integer programs) rather than a universal fact about unions of polyhedra.
Formalizing it. No object in this mission — faciality, the sequential-convexification recursion, or the relative-boundary constraint condition — exists on the platform prior to this mission or in Mathlib. This mission restates the disjunctive-set vocabulary of the earlier missions in this series locally (per the series convention that a draft mission cannot import another draft mission's definitions) and is otherwise self-contained.
The natural first guess is that sequential convexification should always work, since at each step the procedure only discards points excluded by a valid disjunction. The book's own two-variable integer-programming example (imposing integrality on , then on ) refutes this directly: the resulting set strictly contains the true integer hull. The reason faciality repairs this is subtle and is exactly what Lemma 3.2 isolates: the recursion's correctness at each step needs the previous partial hull, intersected with the new disjunction's halfspace, to already equal the convex hull of the intersection taken before convexifying — and this commutation of convex hull and halfspace intersection is exactly what fails when the halfspace does not respect a face of the underlying polyhedron. Theorem 3.3 shows this is not merely Lemma 3.2's specific route to a sufficient condition, but the precise dividing line: the "if" direction says checking the boundary condition only for segments between two points already suffices, which is what makes facial sufficiency provable by induction in the first place.
All results are stated over Fin n → ℝ with matrices Matrix (Fin m) (Fin n) ℝ. The disjunction
structure uses a finite index type S with a dependent family of finite index types Qidx : S → Type*, matching the book's S, Q_j. Faciality (Facial) uses Mathlib's IsExtreme directly,
matching the book's own primary definition of "defines a face" rather than its immediate
"clearly equivalent" restatement (F₀ ⊆ {d_i x ≤ d_{i0}}). The relative boundary in Theorem 3.3
("the boundary of in the affine space spanned by ") is Mathlib's
intrinsicFrontier, the standard formalization of a set's boundary relative to its own affine
hull. The book's own "" in the constraint boundary condition's conclusion (rather than
"", which set-membership syntax would require for a set on the left) is read as set
inclusion, the only mathematically sound reading, and is transcribed as ⊆ in the Lean statement
while the milestone's verbatim text preserves the book's own "" unchanged, per the
verbatim-quotation convention.
A trivializing formalization is ruled out explicitly: Theorem 3.1 is stated for an arbitrary
finite S and Qidx, not fixed at a small size (e.g. |S| = 1, which would make the recursion's
endpoint trivially equal to a single step and prove nothing about sequencing), and the recursion's
ordering σ is universally quantified rather than fixed to a canonical choice, matching the
theorem's own order-independence claim.
Theorem 2.1 (the previous mission in this series) shows that the closed convex hull of a union of polyhedra has a compact description after lifting to a higher-dimensional space. That description comes in two dual flavors: a primal one, as the projection of an explicit lifted polyhedron, and a polar one, characterizing the hull's facets directly via a cone built from the disjuncts' own data. Both flavors matter in practice: a cutting-plane algorithm needs to know exactly which inequalities are facet-defining (so as not to waste effort generating redundant cuts), and the two routes — projection and polarity — offer complementary tools for deciding this. This mission formalizes both routes and the machinery connecting them, closing out Chapter 2 of Balas, Disjunctive Programming (Springer, 2018).
The projection route (§2.2–2.3) develops general facts about projecting an arbitrary polyhedron that predate and underlie the disjunctive-programming application: the classical projection formula via extreme rays of a projection cone, how dimension and facet structure behave under projection, and a refinement (via a coordinate transformation) that eliminates the redundant inequalities the plain projection formula can produce. The polarity route (§2.4) develops the reverse polar, an object introduced by Balas specifically for this purpose, whose iterated application recovers the closed convex hull of a disjunctive set directly, culminating in an exact characterization of when an inequality is facet-defining purely in terms of extreme rays of an explicit cone .
For a matrix system with rows, let , and let be its projection onto the -space. The projection cone is . A vector is an extreme ray of a cone if , , and the ray it generates is an extreme subset of . The dimension of a polyhedron is the dimension of its affine hull, and a set is a facet of if it is a proper face of of dimension . Partitioning 's rows into those tight throughout (the equality subsystem) and the rest, and denote the rank of the tight rows' combined and -only submatrices, respectively.
For , the polar is and the reverse polar is ; more generally the scaled polar at level is . For a disjunctive set with and , the cone .
For a full-dimensional disjunctive set () and :
Proposition 2.13 ( bounded), Theorem 2.14 ( when ), Corollary 2.15 (), Theorem 2.16 (the scaled polar stabilizes: ), and Corollary 2.17 () — each the weakest statement needed for the next.
Theorem 2.5 (), Proposition 2.6 (projection preserves integrality), Theorem 2.7 (), Corollaries 2.8–2.10 (facet/face behavior under projection), and Proposition 2.11 / Corollary 2.12 (sharper facet characterizations via a coordinate-transformed projection cone).
The results themselves. Theorem 2.18 is the practical payoff of the entire polarity apparatus: it turns "is this inequality facet-defining for the convex hull of a union of polyhedra" from a geometric question into an algebraic one about extreme rays of an explicit, finitely-generated cone built directly from the disjuncts' own constraint data — exactly the kind of question a cutting-plane algorithm needs answered to avoid generating redundant cuts. The projection track is foundational general polyhedral theory in its own right (Theorem 2.5's formula underlies Benders decomposition and classical Fourier-Motzkin elimination as special cases, per the book's own remarks), independently useful beyond the disjunctive setting.
Formalizing it. No object in this mission — polars, reverse polars, projection cones, extreme
rays of a cone, or the dimension/facet apparatus of a polyhedron — exists on the platform prior to
this mission or in Mathlib (a q=polar search returns only an unrelated cyclic-polytope
construction from the Hirsch-conjecture series, with different conventions and object). This
mission restates the disjunctive-set vocabulary of the companion ConvexHull mission locally
(per the series convention that a draft mission cannot import another draft mission's
definitions) and builds the polarity apparatus from scratch on top of it.
The natural first attempt at Theorem 2.18 tries to characterize facets of directly from the lifted-polyhedron representation of Theorem 2.1, projecting facet by facet. This misses the point of the polarity route entirely: Theorem 2.18's proof instead goes through , showing a vertex of corresponds to a nonhomogeneous subset of rank of 's own defining system being tight — algebra entirely in the dual space of multipliers, never touching the lifted polyhedron's facets directly. The two obstacles Theorem 2.14 and Proposition 2.13 exist to clear are, respectively: reverse polars do not satisfy the ordinary polar's clean involution property (an extra summand appears, capturing recession directions the reverse-polar construction alone cannot see), and reverse polars are either empty or automatically unbounded (never merely "small"), which is why the apparatus needs the normalization throughout.
All results are stated over finite index sets and matrices Matrix (Fin (m h)) (Fin n) ℝ
(disjunctive-set data, m : Q → ℕ dependent) or Matrix (Fin m) (Fin p) ℝ /
Matrix (Fin m) (Fin q) ℝ (projection-track data). PolyDim and IsFacet are stated generically
over any real vector space (via Module.finrank of vectorSpan and Mathlib's IsExtreme), so the
same definitions serve both Poly2-shaped pairs and cl conv F ⊆ Fin n → ℝ directly in Theorem
2.18. IsExtremeRay is likewise stated generically, reused for cones in plain vector space,
(v,v0)-space, and the triple (v,w,v0)-space Proposition 2.11 needs.
Two results (Proposition 2.11, Corollary 2.12) build on a coordinate-transformed polyhedron
Q̃/cone W̃ that the book itself only cites from [14] rather than constructing; consistent with
the book's own treatment, this mission takes W̃ (or its (v,v0)-projection) as given data
together with its defining relationship to Proj_x(Q), rather than re-deriving the transformation
— a choice recorded in MODERATION_NOTES.md, not a weakening of either statement's content.
Proposition 2.11's complexity remark ("O(max{m,q}³)") is a proof aside about the transformation's
cost, not part of either result's mathematical claim, and is out of scope per the book-wide
disposition (triage.json).
A trivializing formalization is ruled out explicitly: the projection-track results are stated for
generic m, p, q, never fixed at small values, and Theorem 2.18 is stated for a generic finite
disjunctive index set Q, not specialized to |Q| = 1 (which would collapse W_0 to ordinary
LP polarity and prove nothing about unions).
Boolean networks model gene regulatory networks by giving each gene an on/off value and updating all values synchronously by logical rules (Kauffman, 1969). Adding external Boolean inputs gives Boolean control networks (BCNs), in which a designer (a drug, an intervention) chooses the inputs over time. The basic control-theoretic question is controllability: can the inputs drive the network from any configuration to any other? Cheng and Qi (Automatica 2009) answered it for BCNs using the semi-tensor product of matrices, which rewrites a BCN as a linear recursion on canonical basis vectors.
Biological regulation is not instantaneous: transcription and translation introduce delays, so the next value of a gene can depend on several past values. Lu, Zhong, Ho, Tang and Cao (SIAM J. Control Optim. 2016) study delayed BCNs, in which the update reads the last states, and give criteria for two kinds of controllability, including the case where some configurations are dangerous and must be avoided (in biology, states corresponding to disease). The mission formalizes their criteria.
Write . A state is and an input value is . Fix . The delayed BCN (2.2) is
with arbitrary Boolean functions , collected into one map with . A trajectory is the window of the last states; its last entry is the current state. One step maps under the input to . A control sequence of length is , with inputs chosen freely; denotes the trajectory after steps from an initial trajectory .
The transition-count matrix has rows and columns indexed by trajectories: is the number of input values taking trajectory to trajectory in one step. For a set of forbidden trajectories, is with the rows and columns of replaced by zeros, and is with those rows and columns deleted.
The notions of controllability are:
A real square matrix of size is reducible (Definition 3.7) if a simultaneous permutation of rows and columns brings it to block upper-triangular form with square diagonal blocks; it is irreducible otherwise, so every matrix is irreducible.
counts the control sequences of length steering to while avoiding ; counts those steering the initial trajectory to ; is the set of trajectories with current state .
for every , , , every update map and every forbidden set . It is the most general criterion of the paper.
A supporting item, Lemma 3.9 (corrected form), relates Definition 3.7 to positivity of entries of powers for nonnegative matrices of size at least 2.
The criteria replace a question about control sequences of unbounded length by a finite test on one nonnegative integer matrix of size . The counting identities give more than a yes/no answer: they enumerate the control sequences achieving a transfer, which is what a designer choosing among interventions needs, and they handle forbidden states by passing to forbidden trajectories.
The results are proved in the paper; none of them has a machine-checked proof. Formalizing them yields a reusable Lean model of delayed (and, for , ordinary) Boolean control networks defined directly through their dynamics, together with a checked bridge from dynamic reachability to the combinatorics of nonnegative matrices. A formal version also pins down points the printed text leaves loose: Lemma 3.9 as printed is false (it characterizes primitive, not irreducible, matrices), and the two different matrices (zeroed) and (deleted) must not be confused.
The central step is the passage between three objects: reachability under the dynamics, positivity of entries of powers of , and the block-triangular definition of irreducibility. The counting identity for powers of is a statement about sequences of inputs, not about paths in a graph, so the bijection between control sequences and weighted walks has to be established with the avoidance constraint carried at every intermediate time, including the endpoints. The equivalence between Definition 3.7 and strong connectivity is the classical graph-theoretic characterization, but it has edge cases the obvious argument misses: a zero matrix is irreducible by Definition 3.7 yet has no positive power, which is exactly why Definition 3.11 allows while Definition 3.1 does not. A proof that routes through "some power of is entrywise positive", following the printed Lemma 3.9, proves a false intermediate statement.
Conventions committed to in Lean:
Fin n → Bool (true is the paper's 1); a trajectory is Fin μ → State n with index 0 the oldest state and index the current state; is a standing assumption (NeZero μ); are arbitrary and no assumption is placed on the update functions.Matrix.IsIrreducible, which differs on matrices.Controllability is defined through the dynamics and control sequences, never as positivity of entries of powers of ; a formalization that defines reachability by would reduce Theorems 3.10 and 3.12 to library facts and is ruled out.
Needed infrastructure: the correspondence between control sequences and products of entries of (the core of Proposition 3.5), and the equivalence of Definition 3.7 with strong connectivity of the support graph for nonnegative matrices (Mathlib's Matrix.IsIrreducible, Matrix.isIrreducible_iff_exists_pow_pos and Matrix.pow_apply_pos_iff_nonempty_path cover much of the second part for sizes at least 2). Both are reusable beyond this mission, for ordinary BCNs, probabilistic BCNs and finite automata. Contributions of either piece, or of the semi-tensor-product bridge identifying with , are welcome.
A 0–1 integer program asks for the best 0–1 vector satisfying a system of linear inequalities. Its linear relaxation is easy to optimize over, but the relaxation is usually much larger than the convex hull of the 0–1 solutions. Lift-and-project methods close this gap systematically: they lift the relaxation to a higher-dimensional space, add constraints that every 0–1 point satisfies there, and project back, obtaining a tighter relaxation that still contains every 0–1 solution.
L. Lovász and A. Schrijver introduced one of the two standard lift-and-project hierarchies in Cones of matrices and set-functions and 0–1 optimization (SIAM J. Optim., 1991). Their operators and represent a 0–1 point by the matrix , impose linear (and for semidefinite) constraints on such matrices, and project back to . The same paper applies the operators to the stable set polytope, where one round already produces the odd hole, odd wheel, clique and odd antihole constraints. The Lovász–Schrijver hierarchy, the Sherali–Adams hierarchy (1990) and Lasserre's semidefinite hierarchy (2001) are the three reference lift-and-project methods; their rank lower bounds are a standard tool for proving that a relaxation cannot solve a combinatorial problem in few rounds.
This mission formalizes the first structural fact about the operator : iterating it times on any relaxation in variables yields exactly the 0–1 hull (Theorem 1.4 of the paper).
Vectors live in with coordinates ; the space of the original problem is the hyperplane , and polytopes are replaced by the convex cones they generate.
For convex cones , the matrix cone consists of the real matrices such that
adds the condition that is positive semidefinite. The projections are and , where is the 0th unit vector. The cut operator is , and its iterates are , .
Two families of hyperplanes appear in the proofs: and , the hyperplanes through the two opposite facets of in direction .
For every closed convex cone ,
The statement is uniform in and in : no polyhedrality, no bound on the number of constraints, and no assumption that contains a 0–1 point.
Theorem 1.4 is what makes a hierarchy rather than a single cut: the relaxations reach the 0–1 hull after at most rounds, so the -rank of a valid inequality (the least with the inequality valid for ) is a well-defined number between and . The rest of the paper measures combinatorial constraints by this rank: odd hole constraints have rank one on the stable set polytope, and the rank of a stable set inequality is bounded by its defect. Rank lower bounds for lift-and-project hierarchies, in the literature that followed, all presuppose this finite convergence.
The theorem is proved in the paper; to the best of available knowledge none of the Lovász–Schrijver operators has been formalized in a proof assistant. A formalization provides machine-checked definitions of the matrix cones and the cut operators that later missions in this series (odd holes, the defect bound, the constraints) state their results against, and a checked proof of the column characterization (iii″) that all of those proofs use.
The inclusion follows from Lemma 1.1 once each is known to be a convex cone. The reverse inclusion is the content. A first attempt shows that one round of forces one coordinate to be integral, and then iterates; but is not contained in the union of and , only in their Minkowski sum (Lemma 1.3), so a point of is not itself integral in any coordinate. The induction must carry a statement about cones spanned by intersections with unions of cube faces, and it needs each iterate to again be a closed convex cone inside so that Lemma 1.3 can be reapplied. Closedness of the projection is not automatic: a linear image of a closed cone need not be closed.
Option ι for a finite type ι; none is and some i is , and is the cardinality of ι, which may be .PointedCone.hull ℝ S; and are defined as spans of 0–1 vectors, as on the page, not by the inequality description .Contributions welcome: proofs that is a closed convex cone contained in whenever is, a proof of , and lemmas on cones spanned by the intersection of a generating set with a supporting hyperplane; these are reusable by the other missions of the series.
Manufacturing cells, communication protocols, traffic systems and database transaction managers are naturally described not by differential equations but by sequences of discrete events: a machine starts, a part arrives, a message is lost. Ramadge and Wonham's 1987 paper (SIAM J. Control Optim. 25(1)) set up a control theory for such systems in which the plant is an automaton, the controller is another automaton that may disable some events, and specifications are formal languages. The framework, now called supervisory control theory or the Ramadge–Wonham framework, is the standard model for the logical control of discrete event systems and underlies the textbook treatment in Cassandras and Lafortune (Introduction to Discrete Event Systems, 2008) and Wonham and Cai (Supervisory Control of Discrete-Event Systems, 2019).
The question the paper answers is the basic synthesis question of the theory: given a plant, a set of legal behaviours and a set of minimally acceptable behaviours, when does a controller exist that keeps the plant legal, achieves at least the acceptable behaviour, and never deadlocks, and what is the least restrictive such controller?
A generator is with a state set , a finite alphabet of events, a partial transition function , an initial state and marker states . Extending to strings, the generated language is the set of strings for which is defined, and the marked language is the subset of those that end in . The closure of a language is its set of prefixes; is closed if . Throughout, is assumed trim in the sense : every generated string can be completed to a marked one.
The alphabet is split into controllable events and uncontrollable events . A supervisor consists of a deterministic, accessible automaton , whose state set may be infinite, and a map assigning to each state the set of controllable events it enables; uncontrollable events are always enabled. The closed loop runs and in lockstep: an event occurs when the plant can execute it, the supervisor enables it, and the supervisor's automaton can follow it. This defines the languages , and the controlled language .
is complete if its automaton never refuses an event that the plant can execute and enables; it is proper if it is complete and
that is, every closed-loop string can be completed to a marked task. A language is controllable if and . For , is the class of controllable sublanguages of and the class of sublanguages of with .
Given , the Supervisory Marking Problem (SMP) asks for a proper with , and the Supervisory Control Problem (SCP) for a proper with .
and in each case the solving supervisor can be taken minimally restrictive: its marked (respectively controlled) language equals the supremal element and contains that of every proper supervisor whose language lies in .
Theorem 7.1 reduces the existence of a correct, non-blocking controller to a single language inclusion, and identifies the supremal controllable sublanguage as the behaviour of the least restrictive solution. That object is the backbone of the later theory: modular and decentralized control, control under partial observation, and the computational results that is regular and computable when is finite and regular all start from it.
The result is proved in the paper and has been taught for decades; it is not open. Mathlib has no model of generators with partial transitions, supervisors or controllability (its DFA has a total transition function and a single accepted language), and no formalization of this theory exists on the platform. This mission provides one: a reusable Lean model of generators with partial transitions, supervisors with possibly infinite state, closed loops and controllability, together with the paper's existence theorems stated against it. A second mission on the same paper (quotients of supervisors, Theorem 10.1) builds on the same objects.
The combinatorial core of Proposition 7.1 is a short prefix-closure computation. The work lies in the constructions: to show existence, a supervisor must be built for an arbitrary controllable language, which in general is not regular, so the supervisor needs an infinite state set (for example strings of the target language) together with a proof that the closed loop generates exactly the intended language, is complete, and is proper. The converse directions require relating the closed-loop run to separate runs of the plant and of the supervisor's automaton. The naive shortcut of reading the "sup" as an arbitrary member of containing skips the content of the supremal-element milestone; the goal is stated with the actual union.
α with [Fintype α]; strings are List α, the empty string is [], and is s ++ [σ]. Languages are Set (List α); the closure is pre K = {s | ∃ t, s ++ t ∈ K}.Q : Type, a partial transition δ : α → Q → Option Q, an initial state and a marker set. No finiteness is assumed on states, of the plant or of the supervisor. Supervisors and generators live in Type 1.Ec → Bool; an event outside is enabled by definition, so uncontrollable events cannot be disabled.sSup in the complete lattice Set (List α).Welcome contributions: the basic run lemmas (closed-loop runs project to plant and supervisor runs), the string-state supervisor construction, and proofs of the milestones in the given order.
Clique-width is a graph parameter introduced by Courcelle and Olariu (Discrete Appl. Math. 101 (2000)) that measures how far a graph is from being built by a few labelled operations. Every problem expressible in monadic second-order logic with quantification over vertices and vertex sets (MSO) can be solved in linear time on graphs given together with a decomposition of bounded clique-width (Courcelle, Makowsky and Rotics, Theory Comput. Syst. 33 (2000)). Bounded clique-width is more general than bounded tree-width: complete graphs have unbounded tree-width but clique-width .
For fixed there was, before this paper, no polynomial-time algorithm that either decides that a graph has clique-width at least or outputs a decomposition of clique-width bounded by a function of ; the best known algorithm, by Johansson (2001), gave width . Oum and Seymour (J. Combin. Theory Ser. B 96 (2006)) closed this gap with approximation , through rank-width and a factor-3 approximation for the branch-width of symmetric submodular functions.
Timeline:
All graphs are finite and simple. For a finite set , a function is submodular if and symmetric if .
A branch-decomposition of is a pair where is a tree with at least two vertices and all degrees at most , and is a bijection from onto the leaves of . Removing an edge of splits the leaves in two; the width of is of the set of elements of on one side. The width of is the largest edge width, and the branch-width is the least width of a branch-decomposition, with when .
A set is well-linked with respect to if for every partition of and every with , .
Let be the adjacency matrix of over . For disjoint , is the rank of the submatrix of with rows and columns , and the cut-rank function is . The rank-width is .
A -expression is a term built from constants (a vertex with label ), the operators (; add all edges between labels and ), (relabel into ) and disjoint union . Its value is the labelled graph it produces; has clique-width if some -expression has value isomorphic to .
An interpolation of is a function on disjoint pairs that agrees with on , is monotone, submodular in the sense , and has .
For a graph with at least one vertex and an integer :
The same explicit condition decides which side of the approximation holds; this is what the paper's algorithm certifies.
The dichotomy turns clique-width, for which no exact polynomial algorithm is known even for fixed , into a parameter that can be approximated with an explicit witness in each direction. Downstream, every algorithm for graphs of bounded clique-width that needs a -expression as input becomes applicable to graphs given without one, at the cost of an exponential blow-up of the width.
The result is proved in the literature; this mission formalizes it. To our knowledge none of the objects involved — branch-width of set functions, rank-width, cut-rank, -expressions, clique-width — has been formalized in Mathlib, and the submodularity of submatrix rank (Proposition 6.1) is absent from Mathlib's Matrix.rank API. The formal development would give reusable definitions of branch-decompositions of arbitrary integer set functions, of cut-rank, and of clique-width, and a machine-checked link between the combinatorial and the linear-algebraic width parameters.
The upper bound in Theorem 5.2 is the core. The natural approach, growing a branch-decomposition one leaf split at a time while keeping the width at most , gets stuck at a leaf carrying a set with : a split of into two parts of -value below has to be found, and it must be found from the failure of well-linkedness of a set that is not obviously related to . The paper's device is the interpolation , which attaches a matroid to whose base has exactly elements. Formalizing this requires handling partial branch-decompositions, their extensions, and a maximality argument over trees, none of which exists in Mathlib.
Proposition 6.3's upper bound is a second, independent difficulty: a rank-decomposition must be converted into a -expression by an induction over a rooted binary tree, with a relabelling argument bounding the number of labels by the number of distinct nonzero rows of a matrix of rank . Its lower bound needs the tree structure of a -expression to be read as a branch-decomposition.
The ground set is a Fintype V with DecidableEq V; subsets are Finset V; set functions are Finset V → ℤ, as in the paper. A branch-decomposition is a tree T : SimpleGraph (Fin n) with , all neighbour sets of size at most , and an injective map from onto the vertices of degree ; the side of an edge is found by reachability from after deleting . Branch-width, rank-width and clique-width are never computed as minima: "" is the predicate " and , or a branch-decomposition of width at most exists", lower bounds say that every branch-decomposition has a wide edge, and "" is " has a -expression". Labels are Fin k. The value of a -expression has as vertex type the occurrences of constants (a nested sum type), and requires . Cut-rank uses Matrix.rank over ZMod 2 of submatrices of SimpleGraph.adjMatrix. An interpolation is a function on all pairs of subsets whose axioms are imposed on disjoint pairs only.
Running time is not formalized. The paper's Theorem 1.1 asserts an algorithm; there is no cost model on the page, and the goal states the certificate the algorithm returns instead. Without the running time, " or " holds for every graph, so that reading is ruled out as a formalization of the goal; so are well-linkedness with respect to anything other than , widths defined by an unguarded infimum (which is on an empty family), -expressions whose value is not the graph up to isomorphism or whose may join equal labels, and Theorem 5.1 stated for .
Correction of Theorem 5.1. As printed, Theorem 5.1 fails for : a singleton is always well-linked, but the edgeless graph on two vertices has cut-rank identically and branch-width . The milestone carries the hypothesis ; the goal uses the theorem only at size .
The graph with no vertex is excluded from the goal and from the upper bound of Proposition 6.3, since it has no -expression for any . Contributions welcome: proofs of the milestones, lemmas on branch-decompositions (suppressing degree-2 vertices, extending partial decompositions), and submatrix-rank submodularity, which is reusable beyond this mission.
David S. Johnson's 1974 paper Approximation Algorithms for Combinatorial Problems (J. Comput. System Sci. 9 (1974) 256–278) was one of the first systematic worst-case analyses of polynomial-time heuristics for NP-complete optimization problems. Its Section 5 proves the harmonic bound for the greedy algorithm on minimum-cardinality set cover, a result that still underlies the standard approximation guarantee.
Section 6, the subject of this mission, asks what happens when the cost of a cover is its total size rather than its number of sets. This problem, SET COVERING II (EC), is the optimization version of the EXACT COVER recognition problem of Karp's list (Karp 1972): a family has a disjoint subcover exactly when the optimum equals the number of covered points. Johnson shows that the change of measure breaks the cardinality greedy but that a greedy rule based on an overlap ratio recovers essentially the same guarantee. The same accounting (paying for each newly covered point) later became the standard analysis of greedy weighted set cover (Chvátal 1979).
An input is a finite family of finite sets. Its covered set is . A subcover is a subfamily with , and its measure is
The optimum is the least measure of a subcover; since every subcover has measure at least , an optimal subcover is one with the least possible overlapping. The subproblem EC admits only families in which every set has at most points.
Algorithm C2 keeps a subfamily SUB (initially empty), the unused sets LEFT (initially ) and the uncovered points UNCOV (initially ). While UNCOV is nonempty it chooses LEFT minimizing
the number of already-covered points of per newly covered point, and moves from LEFT to SUB, removing its points from UNCOV. When several sets tie, any of them may be chosen; a subcover is choosable by C2 if some sequence of admissible choices returns it.
The overlap of a chosen set is at the moment it is chosen, and the cumulative overlap of a run returning is the sum of these overlaps.
For all and ,
and for all sufficiently large , . In the size-free form used here, for every :
The result. The measure penalizes overlap, and the paper notes (without proof, p. 270) that an algorithm returning an optimal cover for the cardinality measure can be a factor from optimal for this one. Theorem 6 shows that the ratio rule C2 is within of the least-overlap cover, and the lower bound shows that no analysis of C2 can beat . The two bounds differ by less than for every . The theorem was an early instance of a logarithmic guarantee for a weighted covering problem, where each set's cost is its size.
Formalizing it. The theorem has been proved since 1974; no machine-checked proof is known to exist. The mission produces a formal model of the EC problem and of C2 as a nondeterministic process, the overlap identity, and the discrete form of the paper's area-under-a-curve estimate. The last is the part the paper argues informally, through a step function and an integral.
The cardinality argument for C1 counts the sets chosen; here the sets have different sizes, so it does not apply. The overlap C2 pays per newly covered point is not bounded by a constant: early choices can be free and late ones cost up to per point, and the bound on the cumulative overlap must hold against the whole run, for every sequence of tie-breaks.
In a formal proof the integral must be replaced by a sum. Covered points arrive in blocks (one block per chosen set), the charge is constant on a block but the bound depends on the covered fraction at the start of the block, and the sum has to be compared with a logarithm. The terms and that the paper drops using must be controlled as well, and the relation must itself be proved from optimality. The lower bound needs an explicit run of C2 through ties on an input with points, checking at every stage that the intended set is a ratio minimizer.
p : ℕ with S : Fin p → Finset α (0-based, repetitions allowed; a repeated set counts twice in the measure if both copies are chosen, which C2 never does). Subcovers and SUB, LEFT are index sets. is a minimum over the finite, nonempty set of subcovers (Finset.inf'), never a junk value.RunOV.Real.log; is Mathlib's harmonic k.The overlap identity and the discrete integral comparison are reusable for any greedy covering analysis that charges cost per newly covered point. Contributions welcome include proofs of the milestones, the invariants of the C2 run relation (SUB and LEFT partition the indices; UNCOV SUB), and the explicit lower-bound run.
Many problems in signal processing, statistics and function interpolation ask for a solution of a linear system that uses as few columns of as possible: a sparse approximate solution. Natarajan's 1995 paper Sparse Approximate Solutions to Linear Systems (SIAM J. Comput. 24(2):227–234) was motivated by radial basis interpolation, where each column corresponds to a basis function and fewer columns mean a cheaper interpolant. The paper does two things. It proves that finding the sparsest approximate solution is computationally hard (§2, Theorem 1), and it analyses a greedy column-selection algorithm whose number of chosen columns is within a factor, depending on the conditioning of , of the optimum (§3, Theorem 2; a separate mission of this series).
The hardness theorem is the reason the second half of the paper exists: once exact minimization is ruled out, one settles for approximation guarantees. It is cited throughout the compressed-sensing literature as the canonical statement that -minimization under an error constraint is NP-hard, and is the starting point for the later theory of when convex relaxations recover sparse solutions.
The argument follows the classical reduction from Exact Cover by 3-sets (X3C) to minimum-weight solutions of linear systems in Garey and Johnson (1979), pp. 221 and 246, adapted to an approximate right-hand side.
Sparse approximate solution (SAS). Given a matrix , a vector and a tolerance , find a vector with whose number of nonzero entries, written , is as small as possible. Here is the Euclidean norm.
Exact Cover by 3-sets (X3C). An instance is a ground set and a list of subsets of , each with exactly three elements. An exact cover is a sub-collection , , such that every element of occurs in exactly one set of .
The transformation. From an X3C instance build the SAS instance with
In Lean, is Fin m, the collection is C : Fin n → Finset (Fin m) with hC : ∀ j, (C j).card = 3, an exact cover is an index set J with IsExactCover C J, the matrix is incidence C, the vector is onesVec m, is Matrix.toEuclideanLin (incidence C) x, and is nnz x.
For every X3C instance as above,
This is the sentence the proof of Theorem 1 (p. 228) establishes: "the constructed instance of SAS has a solution with or fewer entries if and only if the given instance of X3C has a solution."
The result. The equivalence shows that deciding whether a sparse approximate solution with a prescribed number of nonzeros exists is at least as hard as X3C, which is NP-complete. Consequently no polynomial-time algorithm computes the optimum of SAS unless P = NP, and approximation algorithms such as the greedy method of §3 are the natural object of study. The same instance shows hardness persists for 0/1 matrices, a right-hand side of all ones and a constant tolerance, so the difficulty does not come from ill-conditioned data or from vanishing precision.
Formalizing it. The reduction is proved in the paper; this mission produces a machine-checked proof of its correctness, the combinatorial core of every NP-hardness claim for -constrained least squares. No prior machine-checked version is known to exist, on the platform or elsewhere. The complexity-theoretic wrapper is out of scope (see below).
The forward direction is a direct computation. The converse contains the only real step, which the paper passes over with "it is clear". From one gets only that every entry of is in ; the entries of themselves are arbitrary reals, possibly negative or not equal to , so need not be an indicator vector and need not hold. The exact-cover property must therefore be extracted from support sizes alone: every element is covered by some column in the support, the support has at most columns of three elements each, and a counting argument forces the chosen sets to be pairwise disjoint. Reading off a cover from the values of (for instance, taking the with ) does not work.
EuclideanSpace ℝ (Fin m) and EuclideanSpace ℝ (Fin n), so ‖·‖ is the paper's . Using the sup norm of Fin m → ℝ would give a different statement.C : Fin n → Finset (Fin m): repeated sets are allowed and are distinct indices; an exact cover is a set of indices, and on the SAS side one nonzero entry is counted per index, so both sides treat duplicates consistently.hC.PiLp.norm_apply_le), Finset.card_biUnion_le, and Finset.card_biUnion for disjoint unions. Contributions of a reusable exact-cover API, or of a polynomial-time reduction framework that could later wrap this equivalence into an NP-hardness theorem, are welcome.Multistage stochastic programs are solved on a finite scenario tree: a discrete probability distribution whose support points are paths of a random process. Realistic trees have far too many scenarios for the resulting optimization problem, so practitioners reduce the tree, keeping of its scenarios and redistributing the probability of the deleted ones. The reduction should keep the reduced distribution as close as possible to the original one in a probability metric that controls the optimal value of the stochastic program (Dupačová, Gröwe-Kuska, Römisch, Math. Program. 95 (2003)).
Choosing the best scenarios is a set-covering problem and NP-hard, and the algorithms used in practice (backward reduction, fast forward selection) are heuristics without error guarantees. Heitsch and Römisch (2003) therefore derived test instances with an exactly known optimum: regular binary and ternary scenario trees, for which the minimal reduction distance has a closed form once is not too small. This mission formalizes the ternary case, Proposition 3.2 of that paper. The binary case (Proposition 3.1) is a separate mission of the same series.
Fix a depth and branch widths , with . A regular ternary scenario tree has scenarios, one for each index tuple , where is the successor chosen at level . Choosing successor adds the increment , and scenario is the vector with
All scenarios have probability . The distance between scenarios is the maximum norm .
Deleting the scenarios of an index set and moving each deleted scenario's probability to a nearest kept scenario costs the reduction distance
which by Theorem 2.1 of the paper is the optimal transport-type distance between the original distribution and the best distribution supported on the kept scenarios. The minimal reduction distance to scenarios is .
Let and let with and . Then any two distinct scenarios are at distance at least ; there is a set of scenarios each paired with a scenario outside it at distance exactly ; and for each with ,
with the minimum attained.
The result gives an exact optimal value for an NP-hard reduction problem on an infinite family of instances. Heitsch and Römisch use it in their numerical section to measure how far the heuristics' reduced trees are from optimal (Examples 4.1 and 4.2 are the binary and ternary test trees of that study). A closed form of this kind is also the only way to certify that a heuristic is exactly optimal on some instances rather than only competitive with other heuristics.
The proposition is proved in the paper, but the published proof of its central step is one sentence: "Similarly as in Proposition 3.1 it can be shown that there exists an index for each …". A formal proof supplies that case analysis, which is absent from the literature. The formalization also settles two points the printed statement leaves loose (see Formalization scope): the count of pairs at distance , and the definition of when some widths vanish. No machine-checked version of this result or of the reduction distance is known to exist.
The lower bound is routine: two distinct scenarios first differ at some level , where their coordinates differ by or . The substance is attainment: one must exhibit, for every , a kept set of size whose every deleted scenario lies at distance exactly from some kept one. The obvious candidate, keeping the scenarios that take the middle branch at level , has every other scenario at distance exactly from a kept one, but it keeps scenarios and so covers only . Going down to kept scenarios forces a deleted scenario and its partner to differ at more than one level, and since coordinates are running sums the differences at levels and accumulate on top of the one at level . The paper's proof of this step is not written out, and it depends on the widths of the two levels below : the hypothesis is essential, and the result is false without it (for and one has , not ).
Finset.inf' over the complement of ; the complement must be nonempty, so no default value arises. is stated as IsLeast of the set of all values with : the goal asserts both the lower bound for every and attainment by some . A formalization that exhibits a single with , or states an infimum without attainment, or drops any hypothesis on , is a different (and in the last case false) statement.Multistage stochastic programs are solved on a finite scenario tree, a discrete probability measure whose atoms are paths of a stochastic process. The size of the deterministic equivalent grows with the number of scenarios, so practitioners replace the original measure by a measure supported on of its scenarios. Stability theory for stochastic programs (Dupačová, Gröwe-Kuska and Römisch, Math. Program. 95 (2003), doi:10.1007/s10107-002-0331-0) bounds the change of the optimal value by a probability metric between the two measures, which leads to the optimal scenario reduction problem: choose which scenarios to delete so that this distance is smallest.
That problem is a set-covering problem and is NP-hard, and the algorithms that Heitsch and Römisch study in the same paper (backward reduction, fast forward selection) are heuristics without error guarantees. To test them one needs original measures whose optimal reduction distance is known exactly. Section 3 of Heitsch and Römisch, Scenario Reduction Algorithms in Stochastic Programming, Comput. Optim. Appl. 24 (2003) (doi:10.1023/A:1021805924152) supplies such instances: regular binary and ternary scenario trees, for which the minimal distance to any reduced tree with at least a fixed fraction of the scenarios is an explicit formula. This mission formalizes the binary case, Proposition 3.1.
Fix a horizon and level parameters , with . A regular binary scenario tree has scenarios. A scenario is determined by a branch at every level , and is the vector with
All scenarios start at the root and carry probability . Scenarios are compared in the maximum norm .
Deleting the scenarios with indices in and moving each deleted scenario's probability to a nearest kept scenario costs the reduction cost
which by Theorem 2.1 of the paper is the minimal Kantorovich-type distance between and a measure supported on the kept scenarios. The minimal reduction distance for kept scenarios is .
In the Lean development, scenarios are indexed by σ : Fin K → Fin 2 (Fin-index is tree level , value is the branch , value is ), lev σ k is the branch at level , scenario δ σ : Fin (K+1) → ℝ is , and redCost δ J hJ is .
Let , , and . Then any two distinct scenarios are at distance at least ; there is a set of scenarios each of which has a partner outside at distance exactly ; and for every with
The result. Proposition 3.1 gives the exact optimum of an NP-hard combinatorial problem on an explicit, parametrized family of instances of every size . Section 4 of the paper uses it (Example 4.1, ) as ground truth for the relative accuracy of backward reduction and fast forward selection. Without it, the quality of a heuristic reduction on a large tree could only be compared with other heuristics or with lower bounds.
The formalization. The proposition is proved in the paper; to our knowledge no machine-checked version exists. A formal proof certifies the benchmark values, and the statement also corrects the printed text in two places. First, "there are distinct pairs … at distance exactly " is false as an exact count (for , there are twenty such pairs, not six), so the goal states "at least", in the form the proof exhibits. Second, the paper's sign-based definition of degenerates when some , although the proposition still holds; the mission defines by branch indices.
The lower bound is a direct computation. The content is the matching upper bound: a set of the prescribed size for which every deleted scenario has a kept scenario at the minimal possible distance. A natural first attempt pairs scenarios that differ only at level . That handles only half of the scenarios with a single partner each, and it cannot reach deleted scenarios. Once scenarios differ at more than one level, their maximum-norm distance is a maximum of several partial sums, and keeping all of them at most is exactly where the hypothesis enters. Without it, eq. (20) fails: for , and the true minimum is , not . The passage from to general also needs care: the deleted set must shrink while each remaining deleted scenario keeps its partner among the kept ones.
Fin K → Fin 2, which has exactly elements. The paper's -tuple has a level-0 entry with no choice, so it is dropped, and the vector keeps its coordinates with .δ : ℕ → ℝ, with and the arg min stated for only. is not assumed, because the paper allows and the proposition holds with zeros.Fin (K+1) → ℝ, which is the maximum norm, and is written out.Finset.inf'.IsLeast over the set of attained values , , so both the lower bound and attainment are part of the goal. A proof of for a single exhibited , or a real infimum without attainment, does not prove the goal.Useful infrastructure: sup-norm lemmas for Fin n → ℝ (pi_norm_le_iff_of_nonneg, norm_le_pi_norm), Finset.inf' lemmas, and counting functions Fin K → Fin 2 with prescribed values (Fintype.card_fun, Fintype.card_pi). The tree and reduction-cost definitions are shared in spirit with the ternary-tree mission of this series (Proposition 3.2), and a proof whose structure transfers to is welcome. Contributions of proofs of the milestones individually, in any order, are welcome.
Multistage and two-stage stochastic programs are solved numerically on a discrete probability distribution: a finite set of scenarios with probabilities . The size of the resulting optimization problem grows with , and scenario sets produced by sampling or by historical data are often far too large to be solved directly. Scenario reduction replaces the original distribution by one supported on a small subset of the scenarios, chosen so that the optimal value and solutions of the stochastic program change as little as possible.
Stability theory for stochastic programs (Rachev and Römisch, 2002) shows that this change is controlled by a probability distance of Fortet–Mourier type, which for discrete measures is bounded by the value of a transportation problem. Dupačová, Gröwe-Kuska and Römisch (2003) turned this into a combinatorial problem and proposed greedy backward and forward heuristics. Heitsch and Römisch (2003) gave faster versions of both heuristics; the forward version, fast forward selection, is the subject of this mission. Implementations of these reduction heuristics are distributed with the GAMS modelling system (SCENRED) and are used in energy and finance applications of stochastic programming.
Let be a finite-dimensional real vector space with a norm , let , and let be continuous and nondecreasing with . The cost between two points of is
It is nonnegative, symmetric, and zero on the diagonal.
The original distribution is with and . Deleting the scenarios in a set and assigning new weights , , to the kept ones gives . The distance between and is the optimal value of the transportation problem
The reduction cost of deleting is
and the optimal reduction problem (8) minimizes over all with , where is the number of scenarios to keep.
Forward selection builds the kept set greedily. With and , it chooses
Fast forward selection (Algorithm 2.4) computes the same choices through an updated cost matrix: , , , and .
For and every run of Algorithm 2.4, with any tie-breaking in the arg min,
Theorem 2.5 certifies that the cheap update of Algorithm 2.4 (one pairwise minimum per matrix entry and step) produces exactly the greedy forward selection defined through the reduction costs, and that the running objective is the reduction cost of the scenarios deleted so far. Combined with Theorem 2.1, is the optimal transportation distance between and the best measure on the kept scenarios, which is the quantity practitioners monitor to decide how many scenarios to keep. The lower bound (12) and the optimality condition give a posteriori quality certificates for any reduced set.
All results of this mission are proved in the paper or in the works it cites (Dupačová et al., 2003); none is open. To the best of a platform search, none has been machine-checked. The mission provides a verified specification of a widely deployed algorithm, a formal link between a combinatorial set-covering objective and a finite transportation problem, and definitions (reduction cost, transportation plans with a partially free target marginal, greedy runs with arbitrary tie-breaking) reusable by the regular-tree missions of this series and by later scenario-tree construction papers.
The mathematics is elementary; the difficulty is bookkeeping. The recursion for refers to the previous step's column , which itself was updated, so unrolling it to a minimum over is an induction on in which the index sets , the 1-based step counter and the complement structure all move together. The natural first attempt, identifying with the minimum over the complement of , is off by one step: the correct set is the complement of , which contains itself. For Theorem 2.1 the lower bound requires using that for kept scenarios and that every plan ships all of somewhere outside ; the attainment part requires constructing the plan explicitly from the choice , including scenarios for which several kept scenarios are equally near.
ω : Fin N → E with E a finite-dimensional real normed space; the paper's closed set plays no role beyond containing the scenarios and is omitted. Scenarios need not be distinct.ℝ → ℝ with the paper's assumptions imposed on (IsGrowthFunction); every theorem carries them, together with and .Finset.inf', never a real infimum with a default value.u : ℕ → Fin N with 1-based steps. is the printed recursion, extended to all indices; runs are any sequences satisfying the arg-min conditions, so every tie-breaking rule is covered.A monotone variational inequality asks for a point at which a monotone operator and a convex function are in equilibrium. It unifies convex minimization (where is a gradient), convex–concave saddle-point problems (where is the skew gradient of a Lagrangian), Nash equilibria of monotone games, and complementarity problems in economics and traffic assignment. In operations research, first-order methods for such problems are the workhorse behind large-scale saddle-point formulations of linear and conic programs, where only one operator evaluation and one projection or proximal step per iteration are affordable.
The classical method for Lipschitz monotone operators is Korpelevich's extragradient method (1976) and its proximal variant, Tseng's forward–backward–forward method (2000); both need two evaluations of per iteration. The reflected projected gradient method of Malitsky (SIAM J. Optim., 2015) uses one evaluation of but evaluates it at , a point that may lie outside the domain of . Malitsky's Golden Ratio Algorithm (GRAAL), introduced in Golden Ratio Algorithms for Variational Inequalities (preprint 2018; published in Mathematical Programming, doi:10.1007/s10107-019-01416-w), uses one evaluation of , always at a feasible point, and one proximal step per iteration. Its fixed-step version, Theorem 1 of that paper, is the subject of this mission; the explicit, adaptive-step version (Theorem 2) is a separate mission of this series.
Let be a finite-dimensional real inner product space with inner product and norm . Let and write . Let . The variational inequality is
The standing assumptions are:
The proximal operator of is . Let be the golden ratio, so that . For a step and arbitrary starting points , the Golden Ratio Algorithm generates, for ,
The first line is a convex combination of the newest iterate and the previous average; the second is a forward–backward step taken from the average rather than from .
If is -Lipschitz on (), (C1)–(C3) hold, and , then there is with
Both sequences converge, to one and the same solution. The goal is stated with the paper's exact step range; no rate is claimed, as the paper claims none.
The result. Theorem 1 shows that monotone variational inequalities with a Lipschitz operator can be solved with one operator evaluation and one proximal step per iteration, with evaluated only at points of , where it is defined. This matters when is expensive (a large matrix–vector product, a simulation) or undefined outside the feasible set (for instance an operator involving on the positive orthant). The analysis also explains the constant: the averaging weight is the largest with , and the step bound follows from it. The fixed-step analysis is the template for the explicit, adaptive-step EGRAAL of the same paper (Theorem 2), which needs only local Lipschitz continuity of .
The formalization. The theorem has a published proof, and no machine-checked version of it or of GRAAL is known. Mathlib contains the golden ratio, Lipschitz conditions, lower semicontinuity and cluster points, but no proximal operator of an extended-valued function, no prox-inequality and no Fejér-monotonicity convergence lemma. This mission produces those pieces and a complete convergence proof for a first-order VI method, which are reusable for projected gradient, forward–backward, extragradient and reflected-gradient analyses.
The naive approach, to show that decreases, fails: GRAAL is not Fejér monotone in , because the forward step is taken from the average and uses rather than at the new point. The quantity that decreases is an energy mixing with the successive difference , and both the averaging identity and the Lipschitz estimate must produce matching coefficients for the cross terms to cancel. The energy inequality alone gives only boundedness and vanishing successive differences; convergence of the whole sequence, and the fact that the limit solves (1) when is merely lower semicontinuous and extended-valued, is a separate step. On the formal side, takes the value , so the prox-inequality and the variational inequality must be handled in extended arithmetic without letting decide anything.
E with [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E].E → EReal. (C2) is IsProperConvexLSC g: never , somewhere finite, convex epigraph , and LowerSemicontinuous g on all of E. is effDom g = {x | g x ≠ ⊤}.E → E; monotonicity and the Lipschitz bound are required on effDom g only. The step range is 0 < λ, λ ≤ φ / (2 * L) with 0 < L and φ = Real.goldenRatio.solutionSet g F: points of effDom g satisfying (1) for every , evaluated in EReal.IsProxPoint (fun x => λ * g x) w z⁺, not a choice function, so no junk value is involved. A run of (6) is IsGRAALRun g F λ z zbar on sequences ℕ → E indexed as in the paper: and are free and the entry is unused.∃ zs ∈ solutionSet g F, Tendsto z atTop (𝓝 zs) ∧ Tendsto zbar atTop (𝓝 zs).The hypotheses of the goal are jointly satisfiable, so the theorem is not vacuous: for and every point is a solution and constant sequences form a run of (6); a formalization under which IsGRAALRun has no instances, or in which may be empty, is ruled out. Two hypotheses are added to printed statements and flagged in their notes: in Lemma 1, which is false without it, and in Eq. (14), needed at because the paper's is only defined on .
Welcome contributions: existence and uniqueness of the proximal point of a proper convex lsc function in finite dimensions; the prox-inequality; Fejér-monotonicity lemmas; the energy inequality; and the final convergence argument. The prox and Fejér infrastructure is independent of the golden ratio and is shared with the second mission of this series.
The nearest common ancestor (nca) problem asks, for a fixed rooted tree and a sequence of vertex pairs , for the deepest vertex that is an ancestor of both. It is a basic step in suffix-tree string algorithms and is equivalent to range-minimum queries (Bender, Farach-Colton, 2000). Harel and Tarjan, Fast Algorithms for Finding Nearest Common Ancestors, SIAM J. Comput. 13 (1984) 338–355, gave the first algorithm answering each query on a static tree in constant time on a random-access machine after linear preprocessing.
Their construction reduces the general problem to the case of a complete binary tree, where §3 of the paper shows that nca queries can be answered "by direct calculation" on vertex numbers: multiplication, division, powers of two, the base-two logarithm and bitwise exclusive or. The later simplification of Schieber and Vishkin (1988) is built on the same in-order numbering of a complete binary tree. This mission formalizes that arithmetic core.
Timeline, as reviewed in the paper's §1 (pp. 338–340):
Fix and let be the complete binary tree of depth . A vertex is identified with the path from the root to it, a word of at most left or right turns; the root is the empty word and has vertices. Following the paper's Appendix (pp. 354–355):
The vertices of are numbered from to in symmetric order (in-order): at every vertex, first the left subtree, then the vertex, then the right subtree. is the number of and the vertex numbered . For (Fig. 1 of the paper) the root is , its children and , and the leaves . denotes bitwise exclusive or and the base-two logarithm.
Two procedures of §3 use only numbers, heights and :
The algorithm to compute (p. 342) runs the nca depth algorithm to obtain and then the depth algorithm on . The goal states that it returns the nearest common ancestor: for all vertices of , with the output of the nca depth algorithm and ,
In the order the paper uses them:
Two supporting statements pin the definitions to the paper: is a bijection onto , and the longest common prefix is the deepest common ancestor.
The constant-time nca computation on complete binary trees is the base case of the whole paper: §§4–5 embed an arbitrary tree into a moderately sized complete binary tree through a compressed tree and a balanced binary tree, and every query ends with the arithmetic of §3. The same idea, that in-order numbers encode ancestry in their low-order bits, underlies the Schieber–Vishkin algorithm. Lemma 1 identifies the height with the 2-adic valuation of the number, and Lemma 4 identifies the nca height with the position of the highest differing bit.
The results are proved in the paper, with the proofs left as "easy to verify". No machine-checked version of this numbering or of these four lemmas is known to exist in Mathlib or on this platform. A formal development supplies proofs of the four lemmas and the two algorithms, and a reusable library connecting in-order ranks of a complete binary tree to binary arithmetic (Nat.log, bitwise xor, 2-adic valuation).
The numbering is defined by a traversal order, while the lemmas speak about divisibility, floor division and exclusive or. The work lies in connecting the rank of a vertex in symmetric order to its closed form , where is its left-to-right position. That counting argument sums the sizes of the subtrees that precede and is where most of the effort goes. Lemma 4 then needs the observation that two unrelated numbers agree in all bits above the height of their nca and differ in the bit at that height. This is a statement about Nat.testBit of the exclusive or, and it fails for related vertices. The algorithm statements add a case analysis whose first two cases overlap when .
List Bool of length at most (false = left). Ancestry is the prefix relation, the longest common prefix, depth the length, and height . None of these structural notions uses the numbering.Nat.log 2 x, which agrees for . is ^^^ on , and floor division is / on .Proofs of any milestone are welcome.
The nearest common ancestor problem asks, for a rooted tree and two of its vertices and , for the deepest vertex that is an ancestor of both, written . It appears as a subroutine in string algorithms (suffix trees), in graph algorithms (path queries, dominators) and in the analysis of set-union structures. Aho, Hopcroft and Ullman (On finding lowest common ancestors in trees, SIAM J. Comput. 5, 1976) posed it in several versions, differing in how much the tree changes while the queries are answered.
Harel and Tarjan (Fast Algorithms for Finding Nearest Common Ancestors, SIAM J. Comput. 13, 1984) study how the answer depends on the machine model. On a random-access machine, where addresses can be computed arithmetically, they preprocess a static tree in linear time and then answer each query in constant time. On a pointer machine, where memory can only be traversed by following pointers, their §2 shows that no representation of the tree allows constant-time queries: steps are needed in the worst case. This mission formalizes that lower bound.
Timeline.
A pointer machine stores its data as a collection of nodes. Each node has a fixed number of fields, and a pointer field holds either a node or nil. The machine can follow a pointer from a node it holds, but it cannot compute an address. Following Harel and Tarjan (p. 340), a static tree is represented by a list structure: each tree vertex is represented by a single node , distinct vertices by distinct nodes, and the structure may contain further nodes that represent no vertex. Each node has two pointer fields; the paper reduces any fixed number of pointers to two "without loss of generality". To answer a query on and , the machine is given pointers to and and must return a pointer to .
The node is accessible from in steps or less if it can be reached from by following at most pointers. Write for the set of such nodes. A run of steps from input nodes and is a sequence in which each is the content of a pointer field of a node among . A query with answer is answered in steps if some run of at most steps holds .
The tree is the complete binary tree of height , with leaves. Its vertices are the words (the root-to-vertex path, = left), the ancestors of are its prefixes, the depth of is and its height is . Then is the longest common prefix of and . Logarithms are binary: .
For every , every node type, every list structure with two pointers per node and every injective representation of the complete binary tree with leaves: if every nca query on two leaves is answered in steps, then
This is the last display of the proof (p. 341), which is what the paper's means. The representation is arbitrary and is quantified before the query bound, so the bound holds for every representation.
where is the set of leaves.
The result. Theorem 1 shows that van Leeuwen's pointer-machine algorithm for static trees is optimal up to a constant factor, and that the constant-time queries of the paper's §§3–5 depend on address arithmetic. It is an early nontrivial lower bound for pointer machines on a natural problem; the paper compares it with Tarjan's lower bound for disjoint-set union on a pointer machine (J. Comput. System Sci. 18, 1979).
Formalizing it. The theorem is proved in the paper; as far as could be determined no machine-checked version exists, and Mathlib has no pointer-machine model. The mission produces an explicit, reusable definition of pointer-machine runs and accessibility together with a complete proof of the explicit bound. A formal model of this kind is the precondition for stating any other pointer-machine lower bound.
The statement must hold for every representation, including structures with many auxiliary nodes and arbitrary pointers between tree nodes. Arguing about one natural representation, such as parent pointers, where a leaf is far from its ancestors, says nothing about other representations: a structure with shortcut pointers or auxiliary nodes may bring some ancestors close to some leaves, and the bound must survive every such choice. In the formal setting the counting also has to handle overlaps: nodes reachable from several leaves, nodes that represent no vertex, and pointer cycles.
N, not necessarily finite. ptr : N → Fin 2 → Option N gives the two pointer fields (none = nil), and rep : Vertex h → N is required to be injective. acc ptr j a is defined recursively. Run ptr a b t held is an inductive predicate for runs of steps, AnsweredIn asks for some run of at most steps holding the answer, and AnswersLeafQueriesIn ptr rep k requires this for every pair of leaves.Vertex h is {s : List Bool // s.length ≤ h}, nca is the longest common prefix, and a separate theorem identifies it with the Appendix's deepest common ancestor. counts leaves, not vertices.Real.logb 2. For Lean's gives the true statement ; for , .Set.encard in , so finiteness is part of each claim. Divisions are cleared: .AnswersLeafQueriesIn is satisfiable: the parent-pointer representation answers every leaf query in steps. If rep were not injective, a constant rep would answer every query in zero steps, so injectivity is kept in the goal. The milestones do not need it and do not assume it.Many estimation problems in statistics, signal processing and bioinformatics minimize a composite function : a smooth convex loss plus a convex but nonsmooth penalty or constraint , such as the lasso's norm or the indicator of a convex set. Proximal Newton-type methods handle such problems by minimizing, at each iterate , a model in which is replaced by its second-order Taylor expansion. Widely used solvers of this kind (glmnet, newGLMNET, QUIC) never solve these model subproblems exactly; they stop an inner iterative solver early by some heuristic. Lee, Sun and Saunders (arXiv:1206.1623v13, 2014) proposed an adaptive stopping rule for the inner solver and proved that it preserves fast local convergence. This mission formalizes that local convergence theory (§3.4 of the paper).
Timeline:
Work in with the Euclidean inner product. The smooth part is twice continuously differentiable and strongly convex with constant : for all . Its gradient is Lipschitz with constant , its Hessian is Lipschitz with constant , and for a constant . The nonsmooth part is proper, closed and convex, and may take the value ; it is given by its domain and its values on . The problem is , and denotes its (unique) optimal solution.
The proximal mapping of is . The composite gradient step with step length is
with ; it vanishes exactly at minimizers of and plays the role of the gradient. The step is the unit step on . The model at is with .
The inexact proximal Newton method with unit step lengths produces , where the direction is any point satisfying the adaptive stopping condition
for a forcing term . The Eisenstat–Walker choice is
Both parts are asserted together. The statement fixes no constant beyond the existence of , and .
Theorem 3.10 justifies stopping the inner solver of a proximal Newton method at a relative accuracy that is set by the current optimality measure : a constant small forcing term keeps linear convergence, and forcing terms that decay to zero recover superlinear convergence, with no sufficient-descent condition on the subproblem and for a generic nonsmooth . Theorem 3.11 shows that the self-adjusting choice (2.25) achieves the superlinear regime automatically. Together they are the composite analogue of the inexact Newton theory used in most large-scale smooth solvers.
The results are proved in the paper. No machine-checked proof of any of them is known, and the platform contains no proximal mapping, composite gradient step or inexact Newton condition. A formalization adds a checked proximal-operator toolkit (existence and nonexpansiveness of , the optimality characterization of , strong monotonicity of ) and a precise form of the theorem: the paper's proofs mix two scalings of the composite step and cite a lemma where another is meant, so the formal proof settles which constants are valid.
The obvious argument compares the inexact step with the exact proximal Newton step and treats the gap as a perturbation. For composite functions this fails: the exact step is defined by a nonsmooth inclusion, and the stopping condition bounds a residual of the model's composite gradient step, not the distance to the model's minimizer. The link between the two is strong monotonicity of the composite gradient step (Lemma 3.9), which requires controlling the proximal mapping of a general closed convex jointly with the curvature of ; for it is immediate, and for general it is the central step. A second difficulty is that the threshold on is not scale invariant: a threshold below chosen arbitrarily does not give convergence, so the admissible has to come out of the analysis.
The space is EuclideanSpace ℝ (Fin n). The nonsmooth part is a pair : nonempty and convex, convex on , and the extended function ( on , off ) lower semicontinuous; indicator functions of closed convex sets are included. The proximal mapping is a total function chosen among the minimizers over , which exist uniquely under these hypotheses. , and are functions of the split and a scalar, never of alone. The Hessian is the derivative of the gradient map, measured in operator norm. Sequences are indexed from ; a run requires and . Rates are stated without quotients.
" sufficiently close to " is an existential radius chosen before the run; assuming , letting the radius depend on the run, or reading part 1 as "for every " (which is false: , , diverges) are ruled out. The forcing sequence of Theorem 3.10 is fixed in advance; that of Theorem 3.11 depends on the iterates through (2.25), with a free first term .
A complete development needs existence, uniqueness and firm nonexpansiveness of the proximal mapping of an extended-valued closed convex function, the subgradient characterization of , and a second-order Taylor bound for functions with Lipschitz Hessian. These are reusable well beyond this mission. Contributions of any of them, of the milestones, or of alternative proofs of Lemma 3.9 are welcome.
The maximum-flow problem asks how much of a commodity can be sent from a source to a sink through a network whose edges carry capacities. It is a basic model of operations research. Transportation, scheduling, bipartite matching and image segmentation reduce to it, and it is the inner step of many combinatorial algorithms.
Goldberg and Tarjan introduced the push–relabel (preflow) method in A New Approach to the Maximum-Flow Problem (J. ACM 35(4), 1988). Ford–Fulkerson-type algorithms augment along whole source–sink paths. The push–relabel method instead moves excess flow across single edges, guided by integer distance labels on the vertices. Whatever order its local operations are applied in, it is correct and performs of them (§3 of the paper). Section 4 shows that one particular order, processing the active vertices first-in, first-out, cuts the dominant term, the number of nonsaturating pushes, to . The method and its FIFO and highest-label variants are the standard practical maximum-flow codes.
Timeline:
A flow network has a finite vertex set with , a capacity on every ordered pair, a source and a sink . The edges are the pairs with , and there are no loops. A preflow is a function on vertex pairs with and . Its excess must be nonnegative at every . The residual capacity is . A labeling assigns each vertex a value in . A vertex is active if and .
The two basic operations (Fig. 1 of the paper) are:
The algorithm starts by saturating every edge leaving , with and for .
In the first-in, first-out algorithm (§4), each vertex scans a fixed list of its neighbours through a current edge. The push/relabel operation pushes through the current edge if possible. Otherwise it advances the current edge, or, at the end of the list, returns to the first edge and relabels . Active vertices wait in a queue , initially . The discharge operation removes the front vertex and repeats push/relabel until or increases. Every vertex that becomes active meanwhile is appended to , and is appended too if it is still active. Passes over the queue are defined inductively. Pass 1 consists of the discharges of the initially queued vertices. Pass consists of the discharges of vertices added during pass .
For every network, every edge-list order, every initial queue order, and every run of the FIFO algorithm,
The constant is the printed one.
Corollary 4.4 is the combinatorial core of Theorem 4.5, which states that the FIFO algorithm runs in time. Theorem 4.2 shows that the remaining work of the implementation is plus constant time per nonsaturating push. The bound of Corollary 4.4 is therefore what separates the FIFO method from the bound of the generic method, which matters on dense networks. The same pass-counting argument is reused for the parallel algorithm of §6 and underlies later analyses of highest-label and wave variants.
The results are proved in the paper. Formalizing them adds an analysis of a push–relabel algorithm, which the platform does not yet have. Its existing network-flow material states max-flow min-cut and Ford–Fulkerson termination in an arc-based model with nonnegative flows (the Introduction to Linear Optimization missions). The mission builds a precise operational model of the FIFO implementation, with edge lists, current edges and a queue carrying pass numbers, and states an explicit operation count for it. A companion mission in this series treats the generic algorithm's correctness and its operation bound.
The obvious argument is the potential-function count of §3, over the sum of the labels of active vertices. It yields only and does not use the queue discipline at all. The bound has to charge nonsaturating pushes to passes over the queue, and then bound the number of passes by the total growth of the labels. Neither step is visible in the generic algorithm, because both depend on the order in which vertices are processed.
Making this rigorous requires invariants of the implementation that the paper uses silently:
Lemma 4.1 in particular depends on the current-edge scan: an edge passed over earlier stays inadmissible until is relabeled.
The Lean development works in namespace GoldbergTarjan.FIFO. Vertices form a type V with [Fintype V] [DecidableEq V], and is Fintype.card V. Capacities are c : V → V → ℝ with c ≥ 0 and c v v = 0. Flows are antisymmetric real functions on all ordered pairs, not nonnegative arc flows. Excess is computed from the flow. Labels are in ℕ∞, and the empty minimum in relabel is ⊤.
The state of the algorithm consists of the flow, the labels, the current-edge index cur v into the edge list L v, and the queue Q : List (V × ℕ), each entry tagged with its pass number. Push/relabel (Fig. 3) is a total function, and a discharge (Fig. 4) is a relation carrying the number of push/relabel operations it performs. A run consists of the states S 0, …, S K with S 0 the initial state and consecutive states related by one discharge. The printed variant of Fig. 4, which stops as soon as is relabeled, is the one formalized. Counts are natural numbers over all push/relabel operations of all discharges. The number of passes is the largest pass tag of a discharged entry.
All constants are explicit, exactly as printed:
No asymptotic notation is used, and no assumption is made.
A model without current edges, where relabeling happens whenever no push applies, would make Lemma 4.1 vacuous and change the algorithm. Pass numbers that are not propagated by the "added during pass " rule would make the pass count arbitrary. Both are ruled out by the definitions. A sorry-free check, outside the proposal, exhibits a three-vertex network with two legal discharges, two passes and no nonsaturating push, so the run hypotheses are satisfiable.
Reusable beyond this mission are the network, preflow, push and relabel definitions and Lemma 3.5, which is about an arbitrary preflow. Contributions welcome: invariants of FIFO runs (preflow, valid labeling, queue = active set, cur within bounds), proofs of the milestones, and the reduction of Corollary 4.4 to Lemma 4.3.
Many estimation problems in statistics, machine learning and signal processing minimize a composite function, the sum of a smooth loss and a convex but nonsmooth regularizer or constraint: the lasso and -regularized logistic regression, the graphical lasso for sparse inverse covariance estimation, and constrained least squares, where the nonsmooth part is the indicator function of a convex set. First-order proximal gradient methods (ISTA, FISTA, SpaRSA) are the standard tools, and their convergence is at best linear. Practical solvers such as glmnet, newGLMNET and QUIC instead minimize a local quadratic model of the smooth part plus the nonsmooth part at every iteration, and in practice they need far fewer iterations.
Lee, Sun and Saunders (arXiv:1206.1623, SIAM J. Optim. 2014) put these methods into one framework, proximal Newton-type methods, and proved that they inherit the local convergence rates of Newton and quasi-Newton methods for smooth problems. This mission formalizes the exact-subproblem half of their analysis, ending with q-superlinear convergence of proximal quasi-Newton methods whose Hessian approximations satisfy the Dennis–Moré criterion.
Timeline. Dennis and Moré (1974) characterized superlinear convergence of quasi-Newton methods for smooth equations and minimization by what is now called the Dennis–Moré condition. Tseng and Yun (2009) analyzed coordinate gradient descent for composite problems with a scaled quadratic model. Byrd, Nocedal and Oztoprak (2013) studied inexact proximal Newton methods for -regularized problems. Lee, Sun and Saunders (2012–2014) proved quadratic and superlinear local convergence for a generic closed convex .
The problem is
The smooth part is twice continuously differentiable and strongly convex with constant , meaning for all (Definition 3.2). Its gradient and Hessian are Lipschitz continuous with constants and . The nonsmooth part is a proper closed convex function that may take the value . Its effective domain is nonempty and convex, and denotes the optimal solution of (1.1), which is unique by strong convexity.
At an iterate the method chooses a symmetric positive definite matrix and computes the search direction , the minimizer of the model subproblem
The predicted decrease is . A step length satisfies the sufficient descent condition (2.19) if for a fixed . A backtracking line search with factor takes for the least that passes, so the unit step is tried first. The update is (Algorithm 1). With this is the proximal Newton method. With any other choice of it is a proximal quasi-Newton method. The sequence satisfies the Dennis–Moré criterion if
If for all , with , and satisfies (3.2), then every run of Algorithm 1 from any satisfies
The goal fixes no rate constant. It asserts only the shape of the convergence.
In the order the proof uses them:
The result. Theorem 3.7 is the composite counterpart of the Dennis–Moré theorem. It says that the rate of a proximal quasi-Newton method is governed by how well approximates the Hessian of the smooth part along the steps actually taken, whatever the nonsmooth part is. It covers proximal BFGS-type methods for -regularized and constrained problems, and it explains why solvers built on these methods reach high accuracy in few iterations. Theorem 3.4 gives the corresponding quadratic rate when the exact Hessian is used.
Formalizing it. The results are proved in the paper. None of them has a machine-checked proof: the platform currently has Newton's method only for smooth objectives (Boyd–Vandenberghe's quadratic phase in the mission Convex Optimization V: Newton's Method), and nothing on proximal or composite Newton-type methods. The formalization also settles two defects of the printed text. Theorem 3.1 is false as printed, since it lacks an upper bound on : with , and the iterates stall at about . It is therefore stated here under the assumptions of §3.3. Proposition 3.6 uses an undefined constant (read as ), and the first-order inequalities in its printed proof contain a typo. The explicit constant in Theorem 3.4 is the one the paper's proof derives.
The difficulty is the nonsmooth part. For smooth the Newton step solves a linear system, and the classical analysis works with that closed form. Here is defined only as the minimizer of a nonsmooth subproblem, and every estimate on it has to come from the optimality of that minimizer, i.e. from the firm nonexpansiveness of scaled proximal maps in a norm that changes with . A natural first idea is to apply the smooth Dennis–Moré argument to . It fails because is not differentiable and may be outside . The superlinear rate also depends on the line search eventually accepting the unit step. That acceptance comes only from a third-order Taylor bound combined with (2.15) and the Dennis–Moré residual, and a line search that may return any admissible step does not give it.
EuclideanSpace ℝ (Fin n), and matrices are continuous linear operators. is Mathlib's gradient, and is fderiv ℝ (gradient g). "Positive definite" includes symmetry, and is stated through quadratic forms of a symmetric .EReal, never arithmetic. Replacing by a real-valued function on all of would exclude indicator functions and is not the paper's setting.The maximum-flow problem asks how much of a commodity can be sent from a source to a sink through a network whose edges have capacities. It is a basic model in operations research (transportation, scheduling, bipartite matching) and a standard subroutine in combinatorial optimization.
Classical algorithms, from Ford and Fulkerson (1956) through Edmonds–Karp and Dinic (1970–1972) and Karzanov (1974), increase a feasible flow along augmenting paths or blocking flows. Goldberg and Tarjan, A New Approach to the Maximum-Flow Problem (J. ACM 35(4), 1988, doi:10.1145/48014.61051), replaced this global view by a local one: the push-relabel method maintains a preflow, which may violate conservation at intermediate vertices, and moves excess along edges toward vertices with smaller distance labels. The generic method, with the basic operations applied in any order, is the starting point of the FIFO, highest-label and dynamic-tree implementations analysed later in the same paper, and push-relabel codes remain among the fastest practical maximum-flow solvers.
This mission formalizes §2–§3 of the paper: the generic algorithm is correct, and it stops after a number of basic operations bounded by an explicit polynomial in the numbers of vertices and edges, whatever order of operations is chosen.
A flow network has a finite vertex set with , a source and a sink , and a capacity for every ordered pair of vertices, positive exactly on the edges ; , and there are no loops, .
Flows are real functions on all vertex pairs. A function satisfies the capacity constraint if and antisymmetry if for all pairs. The excess of is . A flow also has for ; a preflow only for . The value of a flow is , and a maximum flow is a flow of maximum value.
The residual capacity is ; pairs with are the edges of the residual graph . A valid labeling is with , and on every residual edge. A vertex is active if , and .
The two basic operations (Fig. 1 of the paper) are:
The generic algorithm (Fig. 2) starts from the preflow that saturates every edge leaving and is zero elsewhere, with the simple labeling , otherwise, and applies applicable basic operations in any order while one exists. An execution with basic operations is a sequence of states from the initial state, each obtained from the previous one by one applicable operation.
Assume the paper's standing assumption . For every execution with basic operations,
and if no basic operation applies in the final state, then is a maximum flow. The paper states the bound as and proves it as "immediate from Lemmas 3.8, 3.9, and 3.10"; the goal states the sum of those three printed bounds. Since every execution is this short, no order of operations runs forever.
In the order the proof uses them: Lemma 2.1 (at an active vertex a push or a relabel applies); Lemma 3.1 (the labeling stays valid); Theorem 3.2 (Ford–Fulkerson: a flow is maximum iff is unreachable from in ); Lemma 3.3 (under a valid labeling is unreachable from ); Lemma 3.5 (from any vertex with positive excess, is reachable); Lemma 3.6 (labels never decrease; a relabeling increases the label); Lemma 3.7 ( throughout); Theorem 3.4 (termination with finite labels gives a maximum flow); Lemma 3.8 ( relabelings per vertex, in total); Lemma 3.9 ( saturating pushes); Lemma 3.10 ( nonsaturating pushes, under ). A further, non-milestone item states the unnumbered invariant that every is a preflow.
The generic bound shows that push-relabel terminates in a polynomial number of steps without any rule for choosing the next operation; the specific orderings of §4–§5 of the paper (first-in first-out, ; dynamic trees, ) refine only the count of nonsaturating pushes, and reuse Lemmas 3.1–3.9 unchanged. The correctness argument, a valid labeling excludes augmenting paths, is the template for the push-relabel minimum-cost flow and assignment algorithms that followed.
These results are proved in the paper and are textbook material. Their machine-checked counterparts are, as far as is known here, not on the Prove2Me platform: the platform's network-flow statements (from Introduction to Linear Optimization, e.g. LinearOptimization.max_flow_min_cut) use a different model, with arc-indexed nonnegative flows and extended-real capacities, and contain nothing about preflows, labels or operation counts. This mission produces a formal account of the antisymmetric-flow model, of Ford–Fulkerson in that model, and of the amortized counting arguments, with the constants the paper prints.
The correctness half is short once the invariants are in place; the difficulty is in the counting. The label bound (Lemma 3.7) is a statement about the whole execution, and it depends on a structural fact about preflows (Lemma 3.5) whose truth rests on antisymmetry and on the nonnegativity of excesses. The obvious first idea for the push counts, bounding pushes per edge or per vertex locally, fails for nonsaturating pushes: flow pushed across a pair can be pushed back later, and nothing local limits how often this happens, so Lemma 3.10 holds only as an amortized statement over the entire execution and depends on both earlier counts. Saturating pushes on a pair can also recur, in both directions, and Lemma 3.9 has to control the interaction between the two directions.
Formally, all of this is reasoning about arbitrary interleavings of operations, with labels in and real-valued flows.
ℕ∞, with ; the relabel value is an infimum, which is on the empty set.σ : ℕ → State V with a length , starting at the Fig. 2 state with the simple labeling (the paper's own assumption for its proofs), each step an applicable push or relabel. "Terminates" means that no basic operation applies, the loop guard of Fig. 2. The three counts are cardinalities of the sets of step indices of each kind.Welcome contributions: proofs of the invariants (preflow, valid labeling, label monotonicity), of Ford–Fulkerson for antisymmetric flows (reusable beyond this mission), and of the counting lemmas. The FIFO bound of §4 is the subject of a companion mission.
Large retailers pay their suppliers weeks or months after delivery, and small suppliers fill the gap with short-term finance. In factoring the supplier sells the receivable to a factor for immediate cash; in reverse factoring the retailer arranges the program with a bank, which pays the supplier early at a rate priced on the retailer's credit rating. Retailers commonly attach a condition: the supplier must accept a longer payment term. Wuttke et al. (Journal of Operations Management, 2019) report that buyers extended payment terms by 54 days on average on adopting reverse factoring and that many suppliers delayed adoption; Corsten (2010) reports suppliers resisting a program because of the demanded payment delay (both as cited by Kouvelis and Xu, pp. 6082–6083). How long an extension a retailer can demand, and what it gains by demanding it, is therefore a practical design question.
Kouvelis and Xu (Management Science 67(10), 2021) answer it inside a Stackelberg supply chain model with credit and liquidity risk. This mission formalizes their answer, Proposition 6 of §5.3: the retailer's optimal payment extension when she keeps the existing wholesale price.
Demand has density , distribution function and ; on with the upper end of the support, is continuous there, the mean is finite, and the failure rate is strictly increasing. Write for expected sales and .
A retailer (the leader) sets a wholesale price , and a capital-constrained supplier (the follower) chooses a production quantity ; the retail price exceeds the unit cost . Each firm has a credit rating , a default probability with strictly decreasing, and an interest premium with decreasing. The lead time is , the payment term , and are the liquidity risks.
Under a post-shipment scheme with coefficient the supplier earns
with (recourse factoring), (non-recourse factoring) and (reverse factoring with payment extension ). The retailer earns under factoring and
under reverse factoring, where is the supplier's best response. Its first-order condition is (Eq. (12)).
Before reverse factoring, the supplier uses the better of the two factoring schemes. By Proposition 4 this is non-recourse, with equilibrium , when , and recourse, with , when . The retailer keeps the existing wholesale price and solves problem (13): maximize over , subject to the supplier's acceptance (his reverse factoring profit is at least his existing one). is the rating at which , and .
(i) If , reverse factoring is dominated by recourse factoring. (ii) If , reverse factoring should be offered with
where with in the non-recourse case, and with in the recourse case.
A follow-on item states Corollary 3(ii): the retailer's profit strictly increases, and the supplier's profit is unchanged when .
Proposition 6 is the paper's prescription for program design. It says which suppliers should be offered reverse factoring: every supplier below the indifference rating and above the non-recourse feasibility threshold. It also gives the extension in closed form, the unconstrained optimum clipped to the supplier's acceptance limit. Two consequences are drawn in the paper: non-recourse factoring is dominated once the extension is optimized, and reverse factoring may leave the supplier exactly as well off as before, so it is not necessarily a win-win (Corollary 3).
The proofs are in the paper's Online Appendix B and have not been machine-checked. A formal proof here produces a checked derivation of the projection formula from the model's primitives. It covers the strict-IFR analysis of the follower's response, the reduction of the acceptance constraint to an interval, and the unimodality of the retailer's objective. The same analysis of the pull game with an effective unit cost recurs across the supply chain finance literature.
The retailer's objective depends on through two opposing channels: the liquidity factor increases, while expected sales decrease because the supplier's effective cost rises. Neither factor is concave in , and the objective need not be concave. The natural move, to set the derivative to zero and call the root a maximum, proves nothing without a sign analysis. That analysis needs the monotonicity of along the implicitly defined response , which is where strict IFR enters. The acceptance constraint compares the supplier's profits in two different games (reverse factoring at against the existing equilibrium). Reducing it to requires the supplier's best-response profit as an explicit increasing function of his quantity. Identifying the existing equilibrium requires Proposition 4, whose "adopted" compares equilibrium profits of two Stackelberg games.
The model is a single Lean structure SupplyChainFactoring.Extension.Model. Demand is a probability measure on with a density , and is an extended real. "Continuous p.d.f. with in " is read as continuity on , with outside the support. Credit functions are real functions constrained on . The finance derivations behind the profit functions (Eqs. (1), (5), (6), Lemma 1) are not formalized: the profit functions are the model.
Readings of informal words, each also recorded in the item's Formalization Note:
Three misprints of the paper are corrected: "if " is read as "if "; "the retailer's maximization problem in (16)" refers to (13); the middle line of the display on p. 6082 carries a stray factor , and the last line is used.
The hypotheses on cannot be met when , and the goal then says nothing about the case, as in the paper. The existing equilibrium, and are never free parameters: is the paper's explicit formula, and the reduction of acceptance to is a milestone to be proved, not an assumption. Every logarithm is applied to a quantity the hypotheses force positive. A formalization that assumed acceptance equivalent to or assumed unimodality would be trivial and is excluded.
The pull game with an effective cost has the same structure as Cachon's pull contract without salvage value (platform items CachonPushPull.*), but those items assume IGFR demand with a salvage value, so they are not reused. Reusable infrastructure welcome: the strict-IFR lemmas (, and increasing) and the explicit best response of a newsvendor-type follower.
Arrival processes to call centers and hospital emergency departments are routinely modeled as nonhomogeneous Poisson processes (NHPPs): Poisson processes whose arrival rate varies over the day. Staffing and queueing models built on this assumption are only as good as the assumption itself, so practitioners test it on data. The standard test, going back to Brown et al. (2005, doi:10.1198/016214504000001808), divides the day into short subintervals, treats the rate as constant on each, rescales the arrival times within each subinterval to , combines all the rescaled data, and applies a Kolmogorov–Smirnov (KS) test of uniformity.
Kim and Whitt (2014, doi:10.1287/msom.2014.0490) ask when this piecewise-constant approximation is justified. If the true rate is not constant on a subinterval, the rescaled arrival times are not uniform, and with enough data the KS test rejects the Poisson hypothesis even when the process really is an NHPP. Section 3 of the paper quantifies this effect through a single number, the degree of nonhomogeneity, and shows how it behaves when the interval is cut into equal pieces. This mission formalizes that section's exact computations for a linear arrival rate.
An arrival rate function on an interval , , is nonnegative, integrable, and strictly positive except at finitely many points. Its cumulative arrival rate is
Conditionally on arrivals in , the arrival times of an NHPP with rate , divided by , are distributed as the order statistics of independent random variables on with the conditional cdf
The degree of nonhomogeneity is the Kolmogorov distance of from the uniform cdf,
It is zero exactly when is constant, and it is the limit of the KS test statistic as the amount of data grows.
For , divide into subintervals of length . For the -th subinterval has cumulative rate , conditional cdf , and share of arrivals . The data of all subintervals, each rescaled to and combined, have the conditional cdf (LEMMA 1).
The linear arrival rate is with and , not identically zero. When its relative slope is ; on the -th subinterval the relative slope is .
In the Lean development these are cumRate, condCdf, degree, subCum, subCdf, weight, mixCdf, linRate and subSlope, in the namespace NHPPArrivals.LinearRate.
For the linear rate, there is a constant such that for every
with, if ,
and, if ,
and in both cases . The constant may depend on , and , but not on ; its value is left open, as in the paper.
The result gives a quantitative criterion for the piecewise-constant approximation: for a linear rate, cutting the interval into equal pieces reduces the degree of nonhomogeneity of the combined data by a factor of order . Since the KS critical value at sample size is of order , this tells a practitioner how fine the subintervals must be, relative to the amount of data, before a KS test of the Poisson hypothesis stops rejecting merely because the rate varies within subintervals. The paper's later THEOREM 6 and its practical guidelines (§3.4, §3.6) rest on these formulas.
The results are proved in the paper by direct calculation; none of them has a machine-checked proof. The mission produces a verified library of the conditional-cdf calculus for NHPPs on an interval (the conditional cdf, its degree of nonhomogeneity, the subinterval decomposition) and the exact linear-rate formulas that the testing literature cites.
The computations are elementary, but two steps are not immediate. First, the supremum of over is a supremum of a nonsmooth function; showing that it is attained at requires knowing the sign of on the whole interval, and for the combined cdf it requires that all the pieces attain their maximal deviation at the same point, which is special to linear rates. For a general rate the naive identity fails: the sup of a sum is at most the sum of the sups, with equality only when the maximizers coincide. Second, LEMMA 1 is a statement about the law of a rescaled random variable (the fractional part of ), which requires splitting a measure along the subintervals and handling their boundary points.
Rates are real functions ; only their values on enter. is an interval integral, subintervals are indexed by with natural numbers cast to reals, and is computed in . All quotients are real divisions; the hypotheses of every statement (, , , and or for the linear rate; integrability, nonnegativity and a finite zero set for a general rate) make every denominator and positive. is the paper's standing assumption of §3.3; excluding is §3.2's requirement that the rate be positive except at finitely many points. The degree of nonhomogeneity is sSup of the image of , and every statement that uses it also asserts that the supremum is attained, so no default value of sSup can make a statement true. The constant of THEOREM 5 is quantified before ; choosing it after would make the bound empty. The statements are about the general definitions of (17) applied to , not about the closed forms (18)–(19), which are separate milestones. The formula for in (19) is stated for only: is undefined when .
The Poisson process itself is not formalized. LEMMA 1's "i.i.d. random variables" is the paper's THEOREM 1 (the conditioning property) applied to each arrival; LEMMA 1 is stated for the law of one arrival time, the probability measure with density on . THEOREM 1, THEOREMS 2–3 and COROLLARY 1 (limits of the empirical cdf and of the KS statistic) are out of scope: they need a point-process layer, the Glivenko–Cantelli theorem and KS critical values, none of which exists in Mathlib. THEOREM 6 is out of scope because the paper gives only a sketch comparing with the KS critical value.
Contributions welcome: proofs of the milestones, general lemmas on sups of for convex cdfs, and the measure-splitting argument of LEMMA 1, which is reusable for any subinterval-based test of the Poisson hypothesis.
Dynamic programming, as introduced by Bellman in the early 1950s, solves sequential decision problems through a functional equation: the value of a problem started in a given state equals the best one-stage return plus the value of the problem started in the state that decision leads to. In practice the argument usually runs backwards. One writes down the functional equation, finds or characterizes a solution, and reads off the structure of optimal decisions from that solution. This is legitimate only if two things hold: an optimal policy exists at all, and the solution of the functional equation that was found is the optimal value, not some other solution of the same equation.
Samuel Karlin's 1955 paper The Structure of Dynamic Programing Models (Naval Research Logistics Quarterly 2(4):285–294) gives an abstract deterministic model in which both questions can be posed precisely. It proves existence of optimal strategies by a compactness argument (Theorem 1), derives the functional equation, which it calls the Principle of Optimality, and identifies the condition under which a solution of that equation is the optimal return: a tail term must vanish. Later treatments of dynamic programming on general state spaces, such as Blackwell's discounted and positive programming (1965–1967) and the monographs of Bertsekas and Shreve, state their verification theorems in the same form, with a solution of the optimality equation plus a condition at infinity.
The model has a state space , a Hausdorff topological space, and a decision space , a nonempty compact Hausdorff space. A strategy is a sequence of decisions, one per stage. The strategy space carries the product topology and is compact by Tychonoff's theorem.
The data are:
From an initial state , a strategy generates the trajectory , , and the weights with . The total yield is
and the optimal return is . The standing assumption of the paper, display (1), is that the partial sums converge uniformly in for each .
Let solve the functional equation
with the maximum attained, and suppose that for every
Then for every , and the maximum is attained (pp. 290–291, §Uniqueness).
Milestone 3 says that the optimal return solves the functional equation. The goal gives the converse on a class of candidate solutions: any solution with a vanishing tail is the optimal return. Together they justify solving a dynamic program by solving its functional equation. The paper's two examples, a two-operation allocation problem with discounting and a resource allocation model driving the state to the origin, obtain uniqueness among bounded solutions and among continuous solutions vanishing at the origin respectively, by checking the tail condition. Without the tail condition the conclusion fails; the paper notes that the limit term "need not be true in general for any solution to the functional equation".
All four milestones and the goal are classical results with published proofs. None of them has a machine-checked proof on this platform: its existing Bellman-equation theorems concern finite-state stochastic models with a constant discount factor, and this model has neither restriction. The mission produces a formal version of the general deterministic model on topological state spaces, with optimality characterized by a verification theorem, which later missions on the paper's examples can reuse.
Existence rests on continuity of on the product space. Each term depends on the first decisions through the composite map , and continuity of that composite in all decisions at once does not follow from separate continuity of in and in . The limit of the series is continuous only because the convergence is uniform.
For uniqueness, the paper's display "" is not an identity: a maximum of a sum is not the sum of the maxima. A proof has to bound from above by the yield of every strategy and from below by the yield of one particular strategy, and the lower bound fails if the tail term is controlled only from above. Attainment of the maximum in the conclusion needs a strategy to be exhibited, not only a supremum computed.
A strategy is a function s : ℕ → D, with the product topology. Lean's 0-based index is the paper's stage : s 0 is , trajectory T ω s 0 is , and weight P s k is , so weight P s 0 = 1. The total yield is a tsum and the optimal return a supremum over all strategies. "Maximum" is encoded as IsGreatest of a range, so every stated maximum is attained. Uniform convergence of (1) is TendstoUniformly of the partial sums to along atTop.
The formalization commits to the following, relative to the page:
Lean's tsum of a non-summable series is , and a supremum of an unbounded family is . Neither default can make a statement trivially true. The uniform-convergence hypothesis forces the series to converge, and under Theorem 1's hypotheses is continuous on a compact space, so the supremum is a maximum. The goal's conclusion is stated without a supremum. A sorry-free check confirms that all hypotheses of the goal hold on a concrete instance with non-zero return: two decisions, constant return , , and .
Needed infrastructure: Tychonoff's theorem, continuity of uniform limits, and attainment of maxima on compact spaces, all in Mathlib. The mission's own definitions are the trajectory, weights, partial and total yield, and the optimal return. Contributions of intermediate lemmas are welcome, for example continuity of , summability from uniform convergence, and the upper and lower tail estimates for . So are formalizations of the paper's Remarks 1 and 3 (Dini's theorem and convergence of the -stage optimal returns).
Integer programming asks whether a system of linear inequalities has a solution . In fixed dimension it is solvable in polynomial time: Lenstra (1983) proved this by showing that a convex body without integer points is "flat" in some integral direction, so that the search splits into few lower-dimensional subproblems. Kannan's 1987 paper in Mathematics of Operations Research sharpened this approach. It computes a Korkine–Zolotarev ("reduced") basis of a lattice, solves the shortest and closest vector problems exactly in operations, and runs integer programming in arithmetic operations. Underneath the algorithm sits a purely geometric statement, Theorem (5.5): a lattice-free convex body meets only boundedly many integer translates of some integral subspace.
Timeline.
is Euclidean space with dot product and length , and is the set of integer vectors. For linearly independent , the lattice is the set of integer combinations , , and is a basis. Gram–Schmidt orthogonalisation gives and unit vectors , and , so and . The determinant is . is the length of a shortest nonzero vector of . The projected lattice is the image of under orthogonal projection onto the complement of . A basis is reduced (Definition 2.6) if for every and for .
A convex body is a convex set of positive volume, which for a convex set means nonempty interior. A subspace has a basis of integer vectors if it is the real span of integer vectors. Its integer translates are the sets with .
In Lean, is EuclideanSpace ℝ (Fin k), a basis is b : Fin m → EuclideanSpace ℝ (Fin k), the lattice is lattice b = Submodule.span ℤ (Set.range b), is gsLen b j, is gsCoeff b i j, is latticeDet b, is lambdaOne, is projLattice b j, and a reduced basis is IsReduced b.
For and every bounded convex set with nonempty interior and there is a subspace spanned by integer vectors with and
The printed theorem allows "an dimensional space " with and bound . Taken literally that is trivial (, one translate). The proof on the same page takes , of dimension , and remarks that this "ensures that the subspace is always of dimension at least 1". The goal states that reading.
Theorem (5.5) is a structural form of the flatness theorem. For it says that a lattice-free convex body meets fewer than consecutive integer hyperplanes of some integral direction. For smaller it gives a finer decomposition of into translates, each a lower-dimensional integer program. This is the recursion behind fixed-dimension integer programming, and statements of this form are used in lattice-point enumeration, in the geometry of numbers (covering minima), and in cutting-plane theory (lattice-free bodies define split and intersection cuts). Propositions 4.2 and 4.3 are the correctness core of exact closest-vector enumeration.
The results are proved in the literature, though Theorem (5.5) is proved "albeit sketchily" in the paper itself. As far as is known, none of them is formalized: Mathlib has Minkowski's convex body theorem and the ZLattice API, but not Gram–Schmidt lattice invariants, Korkine–Zolotarev bases, Hermite-type bounds, nearest-plane rounding, or any flatness theorem. This mission produces the first machine-checked versions. It also corrects three statements that are wrong as printed (below), so the formal statements are the ones that can be relied on.
The naive route to (5.5) is to take a flat direction directly: bound the lattice width of and count hyperplanes. That needs a flatness theorem with an explicit bound below , which is itself the hard part. The paper's argument instead needs John's theorem (every convex body lies between an ellipsoid and its -fold dilation), a reduced basis of the transformed lattice, and a counting argument across projected lattices that combines Minkowski's bound on each with the covering estimate of Proposition 4.2. None of John's theorem, reduced bases or the projected-lattice counting is in Mathlib.
Proposition 4.3 is also delicate as printed: the per-coordinate count on p. 24 undercounts the integers in a closed interval, so the printed arithmetic cannot be transcribed as it stands. Proposition 2.16 in the paper is the correctness of the algorithm SHORTEST. Here only the existence of a reduced basis is needed, which requires attainment of on every projected lattice and a lifting argument (Proposition 1.9).
Conventions: indices are 0-based (Fin m), so the paper's is projLattice b (j-1) and its bound is m ^ (m - i). Gram–Schmidt is Mathlib's unnormalised gramSchmidt. Lattices are Submodule ℤs of a real Euclidean space generated by a linearly independent family, and is allowed, because (1.12) and 4.2 are applied to projected lattices. The goal counts translates as sets with Set.encard, so the bound includes finiteness. is assumed convex, bounded and with nonempty interior, but not closed.
Three printed statements are corrected, and the corrections are recorded in each item's Formalization Note.
Trivializing formalizations are ruled out: the goal forbids , which gives one translate, and , where no translate meets . It requires nonempty interior (the empty set would satisfy everything) and counts with encard (an infinite count cannot become ).
Out of scope: the paper's algorithms (SHORTEST, SELECT-BASIS, ENUMERATE, CLP, CLP′, ILP) and their operation and bit counts (Theorems 2.17, 3.9, 4.5, 5.4), because Mathlib has no cost model. Also out of scope is §6 (NP-completeness of the closest vector problem and Cook reductions), because Mathlib has no complexity classes. The definitions of this mission (lattice, gsLen, gsCoeff, latticeDet, lambdaOne, projLattice, IsReduced) are reusable for any later work on lattice reduction. Contributions are welcome at every level: John's theorem, Hermite-type bounds, Korkine–Zolotarev existence, and the counting lemmas.
A semidefinite program (SDP) minimizes a linear objective subject to a linear matrix inequality (LMI) . In applications the coefficient matrices are measured, estimated or rounded. A solution that is feasible for the nominal data can become infeasible for data that differ from it by an arbitrarily small amount.
El Ghaoui, Oustry and Lebret (SIAM J. Optim. 9(1), 1998) introduced robust semidefinite programs (RSDPs): the constraint must hold for every admissible perturbation of the data, and the robust solution is the best point that survives all of them. Their §5 works out the examples in which the robust counterpart has a closed form. The simplest and most widely quoted is the case where every coefficient matrix is perturbed independently and without structure (§5.1): the robust LMI becomes the single convex constraint . The same computation gives closed-form robust versions of linear programs (§5.3), of largest-eigenvalue minimization (§5.4) and of matrix-norm minimization (§5.6), each of which is the nominal problem plus a Tikhonov-type term . Robust linear programming under ellipsoidal uncertainty was developed at the same time by Ben-Tal and Nemirovski (Math. Oper. Res., 1998); robust least squares, the prototype of §5.6, by El Ghaoui and Lebret (SIAM J. Matrix Anal. Appl., 1997).
Fix , a level , and symmetric matrices . For write and (the Euclidean norm). For a matrix , is its spectral norm, the largest singular value, and means that is symmetric positive semidefinite.
An unstructured perturbation is a block row of blocks, viewed as one matrix. It perturbs each coefficient independently:
The robust feasible set is
and the RSDP is: minimize over . With , the matrix whose -th block is for , the perturbation reads (the paper's (19)).
Three further models use the same pattern. In a robust LP, the data of each constraint are shifted by an independent with . In robust eigenvalue minimization one minimizes the worst case over of . In robust maximum-norm minimization, with , , and one minimizes .
For every ,
The RSDP and problem (21), "minimize subject to ", therefore have the same feasible set, optimal value and solutions. The goal fixes no numerical data: , , and are arbitrary.
The goal shows that robustness against unstructured perturbations costs no more than the nominal problem: the robust counterpart is an LMI of the same size , with a right-hand side that is a convex function of and grows like . The sets have no flat faces, which the paper's §5.2 uses to define the robust center of an LMI and which underlies the uniqueness and continuity of the robust solution (the second sentences of Theorems 5.1–5.4, from §4 under hypotheses H1–H3). Theorems 5.3 and 5.4 exhibit robustification as a Tikhonov regularization with parameter or , and Theorem 5.2 turns a robust LP into a second-order cone program.
All four closed forms are proved in the paper, partly by appeal to the general SDP reformulation of its §3. No machine-checked version of any of them exists, to our knowledge. The mission produces the robust counterparts as identities of feasible sets, stated for every , together with the three intermediate steps of §5.1, so that later missions on the uniqueness and stability halves can import them.
The goal is an exchange of a universal quantifier over an infinite family of matrices with a single matrix inequality. The inequality bounds each perturbation, but the converse needs, for each failing direction, one admissible perturbation that attains the bound; the constant comes from the two copies and , and the constant is the spectral norm of , which holds only because is normed as one block row. Normed block by block, the worst case and the constant change. In the milestone route, the positivity of needs a separate argument before any Schur complement can be taken, since the Schur complement with respect to is undefined at , and the elimination of needs the attainment of . For Theorem 5.4 the difficulty is the attainment: an upper bound on the maximum is immediate, while the lower bound requires exhibiting an admissible perturbation that attains it.
Matrices are Matrix (Fin r) (Fin c) ℝ. Coefficients are indexed by Fin (m + 1) with index 0 the constant term. A block row is one matrix with columns indexed by pairs (i, b) : Fin (m + 1) × Fin n (or Fin q), and is Mathlib's operator norm (open scoped Matrix.Norms.L2Operator), the largest singular value, never the default entrywise norm. The vector norm is written as , never as Mathlib's sup norm on Fin m → ℝ. is (A - B).PosSemidef. Standing assumptions made explicit: symmetric; (§3, p. 36); in milestone 2 (at every is feasible); in Theorem 5.4 (empty matrices have norm ).
Readings and corrections of the printed text:
A formalization in which is an entrywise or blockwise norm, is the sup norm, or the robust set quantifies over a single block, changes the constant and is not this theorem; the statements here rule these out by construction.
Useful, reusable infrastructure: the spectral norm of , Schur complements for positive semidefinite block matrices, and spectral norms of rank-one matrices. Proofs of the three §5.1 milestones and direct proofs of the goal are both welcome.
A semidefinite program (SDP) minimizes a linear objective subject to a linear matrix inequality (LMI) . SDPs model problems in control, combinatorial optimization, statistics and engineering design, and they are solved efficiently by interior-point methods. In applications the data are rarely known exactly: they come from measurements, from linearized models, or from rounding. A solution that is optimal for the nominal data may violate the constraint for data that differ only slightly.
El Ghaoui, Oustry and Lebret (SIAM J. Optim. 9(1), 1998) asked for robust solutions: points that satisfy the constraint for every admissible value of an unknown but bounded perturbation, and among them one that minimizes . Their paper, together with the contemporaneous work of Ben-Tal and Nemirovski on robust convex optimization (Math. Oper. Res. 23(4), 1998), founded robust semidefinite programming. The perturbation model they use, the linear-fractional representation (LFR), is the standard uncertainty model of robust control, where the same exact reformulation appears as the multiplier characterization of quadratic stability under norm-bounded uncertainty.
This mission formalizes the first main result of the paper: when the perturbation is full (an arbitrary matrix of bounded spectral norm), the robust problem is exactly an SDP with one extra scalar variable.
Fix natural numbers and a decision vector . The data are:
For a matrix , denotes its largest singular value (the spectral norm), and means that is symmetric positive semidefinite. A perturbation is a matrix . The perturbed constraint matrix is the LFR (5)
which is well defined exactly when . For a linear subspace of , the robust feasible set (2) is
and the robust SDP (4) is: minimize subject to , for a given . In this mission , the full perturbation case, and the paper's standing assumption of §3.1 is .
Under , , and , for every ,
The paper states that the robust SDP and a corresponding solution can be computed by solving the SDP "minimize subject to (10)" in the variables . Both problems have the objective , so the identity above, between and the -projection of the feasible set of (10), is the content of that sentence. A companion item states the solution correspondence explicitly: is optimal for the robust SDP if and only if is optimal for (10) for some .
The paper cites the S-procedure as the classical result behind Lemma 3.1; it is already proved on the platform (ConvexOptimization.s_procedure) and is included as a reference item.
The robust feasible set is defined by infinitely many matrix inequalities, one per perturbation, each rational in ; in general such a set is convex but has no tractable description, and the paper notes that the structured version of the problem is NP-hard. Theorem 3.1 shows that for full perturbations nothing is lost by replacing that semi-infinite constraint with a single LMI of size in one extra variable. Consequences: the robust problem is solved by a standard SDP solver; the largest admissible perturbation level is a generalized eigenvalue problem; and the exact result is the benchmark against which the paper's sufficient conditions for structured perturbations (Theorem 3.2) and its closed-form counterparts for unstructured perturbations (Theorem 5.1) are measured.
The result is proved in the paper (from the S-procedure, with the details deferred to a cited report). To the best of available knowledge it has no machine-checked proof. The mission produces a formal statement of the LFR model and of the robust feasible set that later missions on robust SDPs can reuse, a formal proof of the well-posedness condition, and a formal proof of the exact reformulation built on the platform's S-procedure. Formalizing it also records two points the printed statement leaves implicit: the result needs and a nonempty perturbation output dimension .
The direction from the LMI to robust feasibility is elementary. The converse is the substance: robust feasibility is a statement about a continuum of perturbations, each entering rationally, and testing the LMI against finitely many extreme perturbations does not produce a multiplier . The exactness of the reformulation rests on a lossless certificate for an implication between quadratic inequalities, which holds only under a strict feasibility condition; that condition is where enters, and without it the lemma is false. The well-posedness milestone requires showing that is also necessary, which is not a norm estimate but needs a perturbation that makes singular.
Matrices are Mathlib Matrix (Fin a) (Fin b) ℝ. The affine maps are given by coefficient lists indexed by Fin (m + 1), the constant term first. The norm on matrices is the operator norm, opened with open scoped Matrix.Norms.L2Operator; it is the largest singular value, and no other matrix norm is used. is Matrix.PosSemidef, which includes symmetry. Block matrices are Matrix.fromBlocks over the index type Fin n ⊕ Fin q, with top-right and bottom-left. Mathlib's matrix inverse returns at a singular matrix, so the condition appears in the robust feasible set in the same universally quantified clause as positive semidefiniteness, as the paper's "well defined" requires; dropping it, or using an entrywise matrix norm, would change the set and is excluded.
Readings and corrections of the printed statements:
Welcome contributions: proofs of the well-posedness milestone (a spectral-norm and singular-vector argument, reusable wherever must be invertible); of Lemma 3.1 from the S-procedure (the reachability lemma for norm-bounded perturbations is reusable in robust control); of the goal from Lemma 3.1 by rescaling; and general lemmas on the spectral norm of rank-one matrices and on Schur complements of block matrices.