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 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Quadratic programming, the minimisation of a quadratic function subject to linear inequality constraints, is a basic subproblem of nonlinear optimisation (sequential quadratic programming, trust-region methods) and a model in its own right in portfolio selection, least-squares estimation and control. The classical solution methods are active-set methods: they keep a set of constraints treated as equalities, minimise over the resulting affine set, and then decide which constraint to drop or add (Gill, Murray and Wright, Practical Optimization, 1981; Fletcher, Practical Methods of Optimization, Vol. 2, 1981). Their finite-termination proofs need either a nondegeneracy assumption (linearly independent active constraints) or an anti-cycling rule, because under degeneracy the choice of the constraint to drop, made from Lagrange multiplier estimates, can cycle.
Calamai and Moré (Mathematical Programming 39, 1987) showed that the gradient projection method can take over the step that leaves a working set. Their Algorithm 6.1 alternates two kinds of step: an arbitrary non-increasing step that adds constraints to the working set until the equality-constrained subproblem is solved, and a single projected-gradient step once it is solved. Theorem 6.2 states that this algorithm terminates at a stationary point for every quadratic that is bounded below on the feasible polyhedron, with no nondegeneracy assumption and no anti-cycling rule. The same paper's Sections 2–4 (the subject of the first two missions of this series) supply the properties of the gradient projection step that the argument uses.
Timeline of the ingredients:
Let be a finite-dimensional real inner product space (the paper's with a general inner product). The feasible set is a polyhedron
with active set . The objective is a quadratic function with self-adjoint but not necessarily positive semidefinite, so may be nonconvex. Its gradient is taken with respect to the inner product of .
The projection into is , and a point is stationary if for every .
A gradient projection step from is with satisfying the sufficient decrease condition (2.1) with a constant , the condition (2.2) that or for some at which the decrease test (2.3) with constant fails, and the upper bound (3.2).
A working set is a set ; problem (6.2) is , over an affine set that ignores the inequality constraints outside .
Algorithm 6.1 produces iterates and working sets from :
For every quadratic bounded below on , all constants , , , and every run of Algorithm 6.1,
The theorem makes no assumption on the boundedness of the iterates and none on the linear independence of the constraints.
Theorem 6.2 separates the two roles an active-set method plays: solving equality-constrained subproblems, for which any method that does not increase may be used, and choosing the next working set, which the gradient projection step does. The consequence is a finitely terminating quadratic programming algorithm for nonconvex quadratics that needs neither nondegeneracy nor an anti-cycling rule, and a template for large-scale bound-constrained and linearly constrained solvers that combine projection steps with subspace minimisation.
The result is proved in the paper and is classical; no machine-checked version is known. A formalization produces a checked finite-termination theorem for an active-set method on degenerate problems, together with reusable pieces: the projection onto a polyhedron as a total function with its variational inequality, the descent estimate of a projected step, and a predicate describing active-set runs with working sets, which other active-set algorithms can reuse.
The obvious argument — each step decreases and there are finitely many working sets — fails on two counts. First, step (b) only guarantees , so values alone do not rule out infinitely many iterations; the nesting of working sets and the final clause of step (b) are what bound consecutive (b)-steps. Second, a gradient projection step taken at a solution of (6.2) can in principle leave unchanged, and nothing in the algorithm's rules says directly that it makes progress; that it does so at every non-stationary iterate is a property of the projection and of the step conditions (2.1)–(2.2), not of the algorithm. A further point is that the minimum of (6.2) is taken over an affine set, not over , and the link between the value at a step-(a) iterate and later iterates runs through the requirement .
The space is a finite-dimensional real inner product space E; is Mathlib's gradient. Constraints are indexed by Fin m, working and active sets are Finset (Fin m), and a run is a predicate IsAlgorithm61Run on three sequences , , indexed from . The run does not stop by itself; "the algorithm terminates at a stationary iterate" is rendered as the existence of an index with stationary. The projection is argmin made total by a junk value that is unreachable when is nonempty, closed and convex. The paper's "" between working sets is inclusion. A quadratic function is with symmetric and no definiteness assumption.
A trivializing formalization — a run predicate that forces to be stationary, or that no sequence satisfies — would make the goal empty; the step rules here are the paper's verbatim, and a run on with starting at the non-stationary point satisfies the predicate. Replacing step (a) by "any step that strictly decreases " would assume the central fact and is not acceptable.
A complete development needs: the variational inequality of the projection (Lemma 2.1(a)), the descent estimate (2.5), the characterisation of stationary points as fixed points of the projected step, and a finiteness argument over the finitely many subsets of Fin m. Proofs of the milestones, of these auxiliary facts, and of the goal are all welcome.
Many combinatorial optimization problems on graphs are linear programs over a polytope whose inequality description is unknown. The stable set polytope is the standard example: maximizing a linear function over it is the maximum weight stable set problem, which is NP-hard, and no complete inequality description is known for general graphs. A productive line of work, begun in V. Chvátal's 1975 paper On certain polytopes associated with graphs (J. Combin. Theory Ser. B 18 (1975) 138–154), asks instead how such descriptions behave under graph operations: if descriptions are known for small graphs, can one write one down for a graph built from them?
Section 5 of that paper answers this for substitution, the operation that replaces a vertex of one graph by a whole second graph. Substitution contains three familiar constructions as special cases: duplicating a vertex, forming the join of two graphs, and forming the lexicographic product (composition). Duplication is one of the two ingredients of Lovász's proof of the perfect graph theorem (Lovász 1972); substitution in general is the operation under which perfection is preserved, and graphs built from simple pieces by substitution are a recurring source of classes with tractable stable set polytopes.
All graphs are finite, undirected and loopless. A stable set of a graph is a set of vertices no two of which are adjacent. Write for the set of incidence vectors of stable sets (the zero–one vectors with stable), and
for the stable set polytope. A finite system of linear inequalities in the variables is a defining linear system of when its set of solutions is exactly .
Let and be graphs with , and let . The graph obtained from by substituting for has vertex set . Its edges are the edges of , the edges of , and every edge joining a vertex of to a neighbour of in . In Lean the vertex type is the disjoint sum {u : V₁ // u ≠ v} ⊕ V₂ and the graph is substitute G₁ v G₂.
For let
be a defining linear system of , with finite index sets and real coefficients, and put for . Then
is a defining linear system of . The statement fixes no particular system for or : any defining systems of the two pieces produce one for , with rows besides nonnegativity.
where and are the maxima of over with and respectively, and is the maximum of over .
Theorem 5.1 gives an explicit construction: from a polyhedral description of and it writes one of , row by row, with no loss. Specialized to it gives Corollary 5.2 of the paper, a defining linear system for the join ; applied repeatedly it gives defining systems for lexicographic products, and applied with it describes the effect of duplicating a vertex. Applied to clique systems, whose coefficients are 0 and 1, the rows of (5.1) are again clique inequalities of , so the class of graphs whose stable set polytope is described by nonnegativity and clique inequalities is closed under substitution.
The result has been proved in print since 1975. As far as a search of the Prove2Me catalogue shows, none of it, including Proposition 2.1 and the substitution operation itself, has a machine-checked statement or proof. The mission asks for a formal proof of the theorem and of the two combinatorial and polyhedral steps it rests on. The definitions of , and graph substitution, and the LP characterization of Proposition 2.1, are reusable by every other mission on stable set polytopes and on polyhedral descriptions of 0–1 sets.
That every point of satisfies (5.1) is a short case check on stable sets of . The difficulty is the reverse inclusion: that no point outside satisfies (5.1). The first idea, taking a point that satisfies (5.1) and splitting it directly into a point of and a point of , fails: (5.1) couples the two input systems through products of their coefficients and right-hand sides, and a fractional solution of (5.1) carries no evident decomposition into the two pieces. Nothing is assumed about the signs of the input coefficients, so the rows of (5.1) can mix positive and negative terms, and the positive part in place of is what keeps the system valid when .
The polyhedral step behind Proposition 2.1, relating a convex hull of finitely many points to an inequality system through linear programming duality, is not available in Mathlib in this form and has to be built.
SimpleGraph on a Fintype with decidable equality; the substituted graph lives on {u : V₁ // u ≠ v} ⊕ V₂, which builds in .IsIndepSet); is convexHull ℝ (S G), never the solution set of an inequality system.a : J → V → ℝ, b : J → ℝ. The nonnegativity rows are kept as a separate conjunct ∀ u, 0 ≤ x u everywhere; Proposition 2.1 is false without them. "Defining linear system" is set equality of the solution set with .[Nonempty V₂]) in Theorem 5.1. The paper's graphs have nonempty vertex sets and its proof picks a vertex of ; with , and , (5.1) is just and the theorem fails. The validity milestone does not need it.sSup over a finite set that always contains the zero vector or the incidence vector of , so no junk value of sSup can occur.Contributions welcome: a proof of Proposition 2.1 (the reusable core), the combinatorial decomposition, the validity case check, and the assembly of the goal.
Minimizing a smooth function subject to linear inequality constraints is the core subproblem of much of nonlinear optimization: bound-constrained problems, quadratic programs, and the subproblems of sequential quadratic programming and augmented Lagrangian methods all have this form. Methods for these problems are usually built from two parts, one that decides which constraints hold with equality at the solution and one that solves the resulting equality-constrained problem quickly. The first part only pays off if the decision stabilizes after finitely many iterations; otherwise the fast local method never gets to run.
Calamai and Moré (Math. Programming 39, 1987) proved that this stabilization is a property of the limit point, not of the algorithm. Any feasible sequence that converges and whose projected gradients tend to zero identifies the active constraints of a nondegenerate limit in finitely many steps. This is the result that later active-set and gradient-projection methods for bound-constrained and linearly constrained problems invoke to justify switching to a fast local phase.
Timeline.
Let be a finite-dimensional real inner product space (the paper's with a general inner product) and let be continuously differentiable on the feasible set, with gradient taken with respect to the inner product of .
The feasible set is a polyhedral set
for constraint normals and scalars . The active set at is .
A direction is feasible at if for all sufficiently small . The tangent cone is the closure of the set of feasible directions. The projected gradient is the point of closest to :
A point is stationary if for all . It is a Kuhn–Tucker point if with . It is nondegenerate if the active normals are linearly independent and the multipliers satisfy for every .
A Lagrange multiplier estimate is a map . It defines the binding set . The estimate is consistent if whenever , the point is a nondegenerate Kuhn–Tucker point, and for every .
Let be an arbitrary sequence in converging to . If and is nondegenerate, then
The sequence need not come from any particular algorithm. The goal asserts eventual equality of the index sets, not inclusion.
The result. Theorem 4.1 separates identification from convergence. Any method that keeps its iterates feasible and drives the projected gradient to zero inherits finite identification, whatever its step-size rule or search direction. After identification the constrained problem is locally an unconstrained problem on the affine subspace , so Newton-type or conjugate-gradient methods can take over. Theorem 4.2 carries the same conclusion to methods that drop constraints according to the signs of multiplier estimates. The companion missions of this series use the result: the gradient projection method drives the projected gradients to zero (mission I), and a gradient projection algorithm for quadratic programs terminates finitely (mission III).
Formalizing it. The theorems are proved in the paper. No machine-checked version of the projected gradient, of tangent cones of polyhedra with their active-set description, or of finite active-set identification is known to exist. Formalization adds a reusable account of tangent cones and polar cones of polyhedral sets and of the equivalence between stationarity and the Kuhn–Tucker conditions for linear constraints, together with a method-independent identification theorem stated at the level of generality of the paper.
Two different limits are involved. Convergence is enough to show that no inactive constraint of is active at for large . The hard direction is the converse: a constraint active at might be inactive at infinitely many , approached from the interior. Convergence of the points alone cannot rule this out. The projected gradient is also not continuous, because the tangent cone changes when a new constraint becomes active. So the hypothesis cannot be passed to the limit naively. Both nondegeneracy conditions matter: without linear independence, or with a zero multiplier, the statement fails.
The space is a real inner product space E with [FiniteDimensional ℝ E], and is Mathlib's gradient. "Continuously differentiable on " means DifferentiableAt ℝ f x for every together with ContinuousOn (gradient f) Ω. The constraints are indexed by Fin m. is polyhedron c δ, and is activeSet c δ x : Finset (Fin m).
The tangent cone is defined as the closure of the feasible directions, not by the polyhedral formula, which is a milestone. The projected gradient is the nearest point of to , chosen by a choice function that returns only when no nearest point exists. That never happens at a point of a polyhedral set.
Nondegeneracy is bundled as IsNondegenerate c δ f x*: , the family is linearly independent, and positive multipliers represent . "For all sufficiently large " is ∀ᶠ k in Filter.atTop.
In Theorem 4.2 the paper leaves one condition implicit: the estimate at must be the Kuhn–Tucker multiplier vector, . Without it the statement is false, so it is an explicit hypothesis. Consistency is required only along feasible sequences and only in the coordinates .
A formalization that assumes , assumes the active sets are eventually constant, weakens nondegeneracy to nonnegative multipliers, or concludes only inclusion is not the paper's theorem and does not satisfy this mission.
Needed infrastructure: tangent cones of convex sets, the Moreau decomposition into a closed convex cone and its polar, Farkas' lemma in a general inner product space, and orthogonal projections onto subspaces spanned by linearly independent vectors. The polyhedral tangent-cone and Kuhn–Tucker results are reusable beyond this mission. Proofs of any milestone are welcome, as are auxiliary lemmas on polyhedral cones.
Minimizing a smooth function over a closed convex set on which projection is cheap (a box, a ball, a simplex) is a routine subproblem in large-scale optimization. Box-constrained minimization is the inner solver of augmented Lagrangian methods, and bound-constrained least squares, image restoration and density estimation all have this form. The classical gradient projection method of Goldstein and of Levitin and Polyak needs only gradients and projections, but with constant or monotone Armijo step lengths it is slow.
Spectral projected gradient (SPG) methods, introduced by Birgin, Martínez and Raydan (paper), combine three ingredients. The first is the projection. The second is the Barzilai–Borwein (spectral) step length , an inverse Rayleigh quotient of the average Hessian along the last step. The third is the nonmonotone line search of Grippo, Lampariello and Lucidi, which compares a trial value with the worst of the last objective values instead of the current one. The paper defines two variants. This mission concerns SPG1, which backtracks along the projection arc , as in Bertsekas's analysis of the Armijo rule for gradient projection. The companion mission concerns SPG2, which backtracks along a fixed feasible direction.
Timeline:
Let be nonempty, closed and convex, with the Euclidean inner product and norm . Let have continuous partial derivatives on an open set , and write . The orthogonal projection is the unique point of nearest to . The scaled projected gradient is for and . A point is a constrained stationary point if for all .
The parameters are an integer , reals , a sufficient-decrease constant and safeguards . Algorithm SPG1 (Algorithm 2.1) starts from and . At iteration it does the following.
replace by any . When (1) holds, set and . 3. Spectral step. With , and , set if , and otherwise .
The first trial of each backtracking is the spectral step , not . The sufficient-decrease term in (1) is , with no factor .
In Lean these objects are written as follows:
P with the predicate IsProjOnto Ω P;scaledProjGrad P f t;IsConstrainedStationary Ω f;nonmonotoneRef f x M k;SPG1Test;IsSPG1Run Ω f P M αmin αmax γ σ₁ σ₂ x α.For every infinite run of SPG1 and every accumulation point of ,
The statement fixes no parameter values, and it assumes neither convexity of nor a bounded level set.
Theorem 2.2 is the global convergence guarantee for SPG1. It holds without monotone decrease of and with no restriction on the spectral step beyond the safeguards. Lemma 2.2 carries Bertsekas's curvilinear Armijo analysis, stated for monotone gradient projection, over to the nonmonotone spectral setting. The projection-arc search is the natural one when is a box or a polyhedron: there the arc is piecewise linear and each trial point is feasible by construction.
Status: the theorem is proved in the literature. This paper's proof reads "Use Lemma 2.2 with the proof technique of [7]", and Lemma 2.2 is quoted from Bertsekas's Nonlinear Programming (Lemma 2.3.1 and Theorem 2.3.3 (a)). No Lean formalization of this theorem, of the Armijo analysis along the projection arc, or of the monotonicity of is known. The mission produces a formal proof and a reusable Lean interface for projection-based first-order methods on convex sets.
For monotone descent methods, the usual argument shows that decreases, so the total decrease is finite and the per-iteration decrease tends to zero. That argument fails here, because need not decrease. Only the window maximum is nonincreasing, and a small decrease of this maximum does not by itself give a small decrease at the iterates that approach a given accumulation point .
Along the projection arc there is a second obstacle. The decrease predicted by (1) is , and depends nonlinearly on : for the trial point is not a rescaling of the first one. So small accepted steps do not translate into small multiples of a fixed direction, as they do for SPG2. The step lengths may also tend to zero, is only on a neighbourhood of , and no Lipschitz constant for is available.
Space and data. The space is EuclideanSpace ℝ (Fin n) with inner ℝ and the 2-norm. is a total function EuclideanSpace ℝ (Fin n) → ℝ with ContDiffOn ℝ 1 f U on an open U ⊇ Ω, and is Mathlib's gradient f. Every trial point is a projection, so the algorithm evaluates and only at points of .
Iteration and trials. Iterations are indexed from . The backtracking choice (2) is universally quantified. At each iteration, a run carries a finite trial list with and ; test (1) fails at every trial but the last and holds at the last.
Step size. is given by Step 3 exactly.
Accumulation point. An accumulation point is MapClusterPt x̄ atTop x.
Lemma 2.2 (i). The paper names the domain but defines only for , so the milestone is stated on .
Excluded simplifications. None of the following is SPG1:
Nor is a goal that states instead of the variational inequality, or one that adds convexity of , a Lipschitz gradient or a bounded level set.
Non-vacuity. The hypotheses of the goal are satisfiable. Take , , , , , , , and . Then the iterates with form an infinite run with accumulation point .
Infrastructure. A complete development needs:
iInf form, norm_eq_iInf_iff_real_inner_le_zero) and the nonexpansiveness of the projection;The projection lemmas, including Lemma 2.2 (i), are reusable for any gradient projection method and are welcome as separate contributions.
A conic quadratic program minimizes a linear objective subject to constraints of the form . Interior-point methods solve such programs in polynomial time, but around 2000 the available solvers handled far smaller instances than linear programming codes did. Ben-Tal and Nemirovski (Math. Oper. Res. 26(2), 2001) asked whether a conic quadratic program can be replaced by a linear program of comparable size, and answered it by approximating each second-order cone by a projection of a polyhedral cone. Their Theorem 1.1 builds such an approximation with accuracy using variables and inequalities. The present mission is their Proposition 3.1: this size is optimal in order, because every polyhedral -approximation needs inequalities.
The question of how many linear inequalities are needed to represent or approximate a convex set as a projection (its extension complexity) has since become a subject of its own, and the lower bound of Proposition 3.1 is one of its early explicit instances for a non-polyhedral cone.
For write . The Lorentz cone is
Let . A polyhedral -approximation of is a linear map such that
Here is componentwise, is the number of auxiliary variables and the number of homogeneous linear inequalities. Equivalently, the polyhedral cone projects onto a cone of the -space with . The slice of at height one is , and denotes the closed unit ball.
The constant is absolute, as in the paper, and no value is fixed; the goal asserts only the order of growth.
The result. Proposition 3.1 shows that the construction of Theorem 1.1 is optimal up to an absolute factor in the number of inequalities: approximating a conic quadratic constraint in dimension to relative accuracy by linear inequalities costs inequalities, no more and no less. It separates what lifting (auxiliary variables) buys, a logarithmic dependence on , from what it cannot buy, a sub-linear dependence on or on . Without auxiliary variables a polytope approximating the ball needs facets; the proposition says the logarithm of that count is the true cost even when lifting is allowed.
Formalizing it. The result is proved in the paper, in about fifteen lines that appeal to "elementary geometry" and to an unstated covering estimate. No machine-checked proof is known to exist. The mission produces a checked proof of the lower bound together with reusable facts: the finiteness bound on extreme rays of a pointed polyhedral cone and a lower bound on the number of balls needed to cover a Euclidean sphere, which Mathlib does not contain in this form. A companion mission of this series formalizes the matching upper bound (Theorem 1.1).
The obvious argument counts vertices of : at most of them, and a polytope between and needs many vertices. The difficulty is in making "many" quantitative with the right exponent. A direct volume comparison of with gives nothing, since may have the volume of . The argument needs the transfer from "the convex hull of the points contains " to "the points are -dense on the outer sphere", and then a lower bound on the size of a covering of a sphere by balls whose centres need not lie on the sphere, uniform down to and up to , where is only and the radius is comparable to the sphere's radius. A second, easily overlooked step is the passage to a line-free cone: itself may contain lines in the -directions, in which case it has no extreme rays at all.
Vectors of are Fin k → ℝ, and the Euclidean norm is written out as eucNorm y = √(∑ i, y i ^ 2); the norm Mathlib puts on Fin k → ℝ is the sup norm, under which is polyhedral and the goal is false. A polyhedral approximation is an -linear map (Fin k → ℝ) × ℝ × (Fin p → ℝ) →ₗ[ℝ] (Fin q → ℝ), and , are the dimensions of its types; with arbitrary (nonlinear) maps, would give , so linearity is what makes the statement non-trivial. "Extreme ray" means a ray , , that is an extreme subset (Mathlib IsExtreme) of the cone, counted once per ray.
Corrections of the printed statement. Proposition 3.1 is printed for every positive integer . It is false for : is polyhedral, and is a polyhedral -approximation with for every , so fails for small . The goal and the counting milestone are therefore stated for , which is the case the proof covers. The phrase "polyhedral approximation" in the proof is read as . The paper's constants are existential and quantified before every variable they are uniform over; no numerical value is asserted.
A complete development needs the Minkowski–Weyl representation of pointed polyhedral cones by extreme rays, basic convex-hull and separation arguments in Euclidean space, and a lower bound for covering numbers of spheres (for instance by a cap-measure or volume argument). The extreme-ray and covering lemmas are independent of the Lorentz cone and are welcome as stand-alone contributions.
Many decision problems in operations research are solved in two stages: a model predicts the unknown cost vector of a linear optimization problem from features, and the predicted costs are then passed to a solver. The smart predict-then-optimize (SPO) loss of Elmachtoub and Grigas measures the quality of a prediction by the excess true cost of the decision it induces, rather than by the prediction error itself. El Balghiti, Elmachtoub, Grigas and Tewari study how well the empirical SPO loss generalizes. Their margin-based bounds (Theorems 4 and 5 of the paper) require a geometric condition on the feasible region, the strength property, and a way to compute the distance to degeneracy that enters the margin loss.
Section 5 of the paper verifies this condition in the two cases that matter in practice. For strongly convex regions it is Theorem 7 (mission III of this series). This mission covers the other case, §5.2: feasible regions that are polytopes given by a list of points, which includes the unit simplex of multiclass classification and the feasible regions of shortest-path, assignment and other combinatorial problems written as convex hulls.
Let be a finite-dimensional real vector space (the paper's ) with a norm . A cost vector is a linear functional on ; its value at is written , and its dual norm is .
The feasible region is a polytope with a known convex hull representation: pairwise distinct points and
Redundant points (points that are convex combinations of the others) are allowed. For a cost vector , is the problem , and an optimization oracle is any map with for every .
If is not a singleton, then for every oracle , has the strength property with parameter
The result. Formula (10) turns the distance to degeneracy, defined as an infimum over an infinite non-convex set, into a minimum of explicit ratios that needs one oracle call. This makes the margin SPO loss of the paper computable for polytopes. The strength claim, combined with the paper's Theorems 4 and 5, yields margin-based generalization bounds for the SPO loss over any polytope with a known vertex list, with a dependence on the hypothesis class through its multivariate Rademacher complexity rather than through a Natarajan dimension. For the unit simplex it recovers known margin bounds for multiclass classification (Example 8).
Formalizing it. The results are proved in the paper; to our knowledge none of them is machine-checked. A formalization produces, beyond the four statements, a Lean account of the normal fan of a polytope presented by a point list, its interplay with uniqueness of linear-optimization solutions, and distances to its boundary measured in a dual norm. These are standard facts of polyhedral theory that Mathlib does not yet state in this form.
The obstacle is that is a distance to the degenerate set, and that set is neither convex nor given by inequalities: it is a union of lower-dimensional pieces of the normal fan, so no projection formula applies, and its description depends on which points of the representation are redundant. Relating a dual-norm ball around to the finitely many inequalities of eq. (9) is where the argument needs care. A Euclidean shortcut is not available: the norm is arbitrary, and the numerator of (10) and the distance are measured in different norms. A second trap is the oracle: at a degenerate it may return a point that is not among the , and (10) must still hold.
StrongDual ℝ E, whose operator norm is the dual norm. Interiors and distances in the cost space use that norm.v : Fin K → E, injective, with = convexHull ℝ (Set.range v). Nonemptiness, compactness and convexity of (the paper's §2 standing assumptions) follow from this representation; Proposition 2 and the diameter identity add , which is that nonemptiness.S.Nontrivial. Without it , and the strength property holds for free; with it, and is a genuine distance. The goal's parameter is stated to be positive, so the Lean conventions on unbounded or one-point sets and cannot trivialize it.Metric.infDist to ; is Metric.diam, correct here because is bounded. Minima and maxima over finite index sets are stated with IsLeast/IsGreatest, so no junk value of min' or sInf enters.Many computations in numerical linear algebra, statistics and computational physics need the trace of a matrix that is never formed explicitly: may be an inverse, a matrix function , or a product of large operators, and the only affordable access is a routine that returns or for a given vector . Monte Carlo trace estimators handle this setting: draw random vectors and average the quadratic forms , each of which costs one matrix–vector product.
Avron and Toledo (J. ACM 2011) compare such estimators by the number of samples that guarantee relative error with probability , and by the number of random bits each sample consumes. Hutchinson's estimator (Hutchinson 1990) and the Gaussian estimator need random bits per sample. Section 8 of the paper studies two estimators that sample only from the standard basis vectors and so need about bits per sample, which allows the samples to be generated in advance. The plain version has a sample bound that depends on how uneven the diagonal of is; the mixed version first multiplies on both sides by a random orthogonal mixing matrix of the kind introduced by Ailon and Chazelle (2006) for the fast Johnson–Lindenstrauss transform and used by Avron, Maymounkov and Toledo (2010) in least-squares solvers. This mission formalizes the resulting sample bound, Theorem 8.4.
Let , let be symmetric positive semi-definite, and let be the standard basis of .
A random variable is an -approximator of if
(Definition 4.1).
The unit vector estimator with samples is
where are independent uniform random samples from (Definition 3.4). Each term is a diagonal entry of chosen uniformly at random. Its behaviour is governed by
which lies between and .
A random mixing matrix is , where the seed is a fixed orthogonal matrix and is diagonal with i.i.d. Rademacher entries, (Definition 3.5). The seed enters through
which satisfies ; normalized DFT and Hadamard matrices attain , DCT and DHT matrices have (p. 8:5).
The mixed unit vector estimator is
with as above, independent of (Definition 3.6). It is the unit vector estimator applied to , whose trace equals .
For every orthogonal seed , every symmetric positive semi-definite , every , and every ,
Theorem 8.2 alone shows that the unit vector estimator can need order samples: when the trace is concentrated on one diagonal entry, . Theorem 8.4 removes the dependence on entirely. For a Fourier-type seed with the bound becomes samples for every positive semi-definite , while each sample still costs about random bits, and the bits of are drawn once. Among the estimators of the paper this is the only one with both an -independent sample bound and logarithmic randomness per sample (Table I, p. 8:5). Lemma 8.3 is a standalone statement about randomized orthogonal transforms that is used well beyond trace estimation, in the analysis of subsampled randomized Hadamard transforms, sketching-based least squares, and fast Johnson–Lindenstrauss embeddings.
All results of the mission are proved in the literature: Lemma 8.3 in the cited works, the rest in the paper. As far as the platform's catalogue shows, none has a machine-checked proof. The mission produces checked statements of the paper's Section 8 with their exact constants, a probability model for random sign matrices and uniform basis-vector sampling that other randomized linear-algebra missions can reuse, and, once proved, a checked instance of Hoeffding's inequality applied to a concrete estimator.
The obvious argument for Theorem 8.4 applies Theorem 8.2 to . That matrix is random, so Theorem 8.2, which is a statement about a fixed matrix, cannot be applied directly: the proof must condition on , use that the samples are independent of , and combine a failure event over with a conditional failure event over the , each with probability at most . The second difficulty is Lemma 8.3: each entry is a Rademacher sum whose coefficient vector has squared norm at most , and the bound needs a sub-Gaussian tail for such sums together with a union bound over all entries. Bounding the diagonal of through the diagonal of alone does not work: each mixed diagonal entry depends on all entries of , including the off-diagonal ones.
Everything is over . The paper allows complex unitary seeds; since the estimator uses the transpose , the mission takes real orthogonal (). Matrices are Matrix (Fin n) (Fin n) ℝ, "symmetric positive semi-definite" is Matrix.PosSemidef, and is assumed throughout. The sample spaces are explicit product measures: indices uniform on Fin n with , the diagonal of with the -fold Rademacher product law, and, for , the product of the two, which makes and the independent as the paper assumes implicitly. Probabilities are Measure.real. and are maxima over finite nonempty index sets; uses real division, whose value at is irrelevant because a positive semi-definite matrix with zero trace is . The sample-count thresholds are exactly the paper's constants.
Deviations from the page, all recorded in the items' Formalization Notes: Definition 3.4 and Theorem 8.2 are stated for positive semi-definite rather than positive definite (the proof uses only ); Table I's entry for the mixed estimator, which disagrees with Theorem 8.4, is not used; the proof of Theorem 8.4 prints the conditional failure probability as "" where is meant, and no statement copies it; Remark 8.5 ("for some small ") has no pinned constant and is not stated.
A formalization in which is an arbitrary orthogonal diagonal matrix, the are correlated with , or the law of the estimator is assumed rather than constructed would make the goal either false or a restatement of its hypotheses; the product-measure model rules this out.
Needed infrastructure: Hoeffding's inequality for bounded i.i.d. sums (in Mathlib as sub-Gaussian moment generating function bounds), a sub-Gaussian tail for Rademacher linear combinations, conditioning on one factor of a product measure, and the spectral theorem for real symmetric matrices. The Rademacher sign model and the random-mixing-matrix entry bound are reusable beyond this mission. Proofs of any milestone, and alternative arguments for Lemma 8.3, are welcome.
The k-median problem asks to open facilities among a set of candidate sites so that the total distance from clients to their nearest open facility is as small as possible. It is a basic model of facility location and of clustering, and it is NP-hard, so the question studied in approximation algorithms is how close a polynomial-time method can get to the optimum.
Local search is the method most used in practice: start from any facilities and repeatedly replace a few of them by others whenever this lowers the cost. Arya, Garg, Khandekar, Meyerson, Munagala and Pandit (SIAM J. Comput. 33(3), 2004) gave the first analysis of a local search for k-median with a bounded performance guarantee using only medians. For single swaps they proved a locality gap of (Theorem 3.2, the subject of the first mission of this series); allowing up to facilities to be exchanged at once improves the gap to , which the paper notes improves on the -approximation of Charikar and Guha. That -swap bound is the result this mission formalizes.
Timeline (as recounted in §1 of the paper):
A metric instance consists of a finite set of clients, a finite set of facilities and a distance on that is nonnegative, symmetric and satisfies the triangle inequality; is the cost of serving client by facility .
For a nonempty set of open facilities, each client is served by its nearest open facility, and
Fix an integer . A -swap deletes a set of at most facilities and adds a set of the same size. The -swap neighbourhood of is
and is locally optimum when for every . The locality gap is the supremum, over instances, of the ratio between the cost of a locally optimum solution and the cost of a global optimum.
In Lean the instance is MetricInstance Cl Fa with the distance on Cl ⊕ Fa, the cost is kmCost I S hS (defined only for nonempty S), and local optimality is IsPSwapLocalOpt I p S hS, all in the namespace LocalSearchFL.MultiSwap.
For every metric instance, every integer , every , every locally optimum with , and every nonempty with ,
This is the bound concluded at the end of §3.4 (p. 553, announced p. 551). The comparison solution is arbitrary, not only an optimum, which is the strongest form printed.
The bound shows that the simplest optimization heuristic, stopped at any local optimum, is within a constant factor of optimal for metric k-median, and that the factor tends to as the neighbourhood grows; the paper's tight example (§3.5, given for and stated to generalize to every ) shows that the analysis cannot be improved for this neighbourhood. Combined with the standard -improvement rule (p. 548), it yields a polynomial-time -approximation. The analysis template (charging each client's reassignment through a bijection of , and averaging the local-optimality inequalities of carefully chosen swaps) was reused for facility location, capacitated variants and k-means.
The result has been proved since 2001. What this mission adds is a machine-checked proof: no formalization of the k-median problem or of any locality-gap bound is known to exist in Mathlib or on this platform. The combinatorial milestones (capture, the partition of Claim 3.1, the weighted swaps, the bijection of Property 3.2) are independent of the metric and are reusable in any local-search analysis of clustering objectives.
For single swaps each facility of is paired with one facility of and a direct counting argument suffices. With -swaps, a facility of may capture several facilities of at once, and a group of facilities of may jointly capture a facility of that none of them captures alone. Pairing facilities one by one then fails: the clients of a captured facility cannot be reassigned cheaply unless the capturing set is swapped out together with everything it captures. Swapping whole groups is only allowed when a group has at most members; larger groups must be split into single swaps, and the weights must be chosen so that every facility of is counted exactly once while no facility of is counted more than times. Getting the constant (rather than a weaker one) depends on this exact accounting.
Cl, Fa with Fintype and DecidableEq; solutions are Finset Fa. The distance is real-valued on Cl ⊕ Fa; d x x = 0 is not assumed (the paper neither states nor uses it).kmCost I S hS ≤ (3 + 2 / (p : ℝ)) * kmCost I O hO, with the constant computed in .Needed infrastructure: finite sums over clients, Finset.inf', permutations (Equiv.Perm), and a weighted double-counting argument over the swaps. Proofs of the combinatorial milestones and alternative routes to the goal are welcome.
Line searches are the step-size rules inside most methods for smooth unconstrained minimization : steepest descent, conjugate gradient, quasi-Newton and limited-memory methods all choose a direction and then a step along it. Classical Armijo and Wolfe rules are monotone: they require . Grippo, Lampariello and Lucidi (SIAM J. Numer. Anal., 1986) observed that insisting on monotone decrease can slow a method down, and proposed comparing with the maximum of the last function values instead. That max-based rule discards good function values and depends strongly on , and Dai showed that R-linearly convergent iterates can violate it for every fixed memory .
Zhang and Hager (SIAM J. Optim., 2004) replaced the maximum by a weighted average of all previous function values. Their averaged nonmonotone line search is used in practical codes, for example with L-BFGS and in later nonmonotone spectral and conjugate-gradient methods. This mission formalizes the paper's first main result: global convergence to stationary points for nonconvex .
Let be continuously differentiable, with gradient at the -th iterate. The Nonmonotone Line Search Algorithm (NLSA) has parameters
It maintains weights and reference values :
with chosen at each step. The iterates are , where the step satisfies one of two rules, fixed for the whole run:
The choice gives , the monotone line search; gives .
The direction assumption asks for constants with (2.4) and (2.5) for all sufficiently large . The level set is , and is the set of points whose distance to is at most , where .
Suppose is bounded from below, for every , the direction assumption holds, and is Lipschitz continuous on (Wolfe rule) or on (Armijo rule). Then
and if ,
so every limit of a convergent subsequence of iterates is a stationary point. No convexity is assumed.
Theorem 2.2 is the convergence guarantee that makes the averaged reference value usable in practice: any direction method whose directions are uniformly gradient-related (for example L-BFGS with bounded Hessian approximations) inherits stationarity of its limit points when combined with this line search, for every choice of the weights . The monotone Wolfe and Armijo results are the special case . The same estimates, (2.8) and (2.15), are the input to the paper's second main result, R-linear convergence for strongly convex (Theorem 3.1, a separate mission in this series).
The result is proved in the paper. It has no machine-checked proof that this mission is aware of: the platform has monotone backtracking statements for convex problems, but no nonmonotone line search, no Wolfe conditions and no Zoutendijk-type global convergence theorem for nonconvex . A complete development also provides reusable Lean statements of the Wolfe and Armijo conditions and of step-size lower bounds under local Lipschitz continuity of the gradient.
Each step is elementary, but the argument has several places where a naive formalization fails. The Lipschitz hypothesis is only local: on for the Wolfe rule, on the -neighbourhood for the Armijo rule. So the proof must first show that every iterate stays in even though is not monotone. This needs and the monotonicity of , and then that the Armijo rule's rejected trial point lies in . The Armijo lower bound uses the maximality of the integer exponent and a first-order Taylor bound along a segment. The passage from (2.14) to (2.6) and (2.7) uses the two growth bounds on . The first gives only , since does not force .
The space is EuclideanSpace ℝ (Fin n) with the Euclidean norm, is ContDiff ℝ 1, and the paper's row vector acting on is the inner product of Mathlib's gradient f x with . , and are defined by recursion from the run. A run is an infinite sequence satisfying the update, , and the chosen rule at every . The stopping test is not modelled. The Armijo exponent ranges over (it may be negative since ), and "largest" is IsGreatest. and the distance to are computed in , so unbounded directions give .
The following repairs and readings of the printed statements are made:
The following formalizations would make the goal trivial or empty and are ruled out:
liminf, which is for a divergent sequence;Welcome contributions: proofs of the milestones in the listed order, and general lemmas on Wolfe and Armijo steps under local gradient Lipschitz continuity, which are reusable for other line-search methods.
The finite-horizon theory of chunk 02a-model-bellman-equation (Bäuerle and Rieder's Theorem
2.3.8, the Structure Theorem) reduces the existence of an optimal policy and the validity of the
Bellman equation to a single abstract hypothesis: the Structure Assumption (SAN), the existence
of function classes and decision-rule classes closed under the
one-step optimality operator . That theorem does not say when (SAN) actually holds for a
given Markov Decision Model — checking it directly from the definition would require exhibiting,
for every value function that could arise, both its regularity and a measurable action attaining
its supremum, an infinite regress. This mission formalizes the classical resolution: sufficient
conditions on the primitive data of the model (the admissible-action correspondence, the
transition kernel, the one-stage reward) under which (SAN) is guaranteed, so that Theorem 2.3.8
becomes usable in practice rather than merely an existence statement.
Fix a Markov Decision Model (chunk 02a's
Definition 2.1.1), now with , Borel spaces. A measurable is an
upper bounding function (Definition 2.4.1) if , , and for constants ; write for the value functions of weighted growth at most
for some . A set-valued map is upper semicontinuous if
and force to have an accumulation point in (Definition A.2.1); it
is continuous if also every point of is approximated by a sequence from the .
Suppose the model has an upper bounding function , and for every : (i) is compact for every ; (ii) is upper semicontinuous on for every and every ; (iii) is upper semicontinuous on for every . Then , satisfy (SAN). Unlike the two milestone theorems that precede it in the chapter (Theorem 2.4.6 and Theorem 2.4.10, both of which also assume the correspondence varies semicontinuously or continuously with ), Theorem 2.4.13 assumes nothing about as a set-valued map beyond pointwise compactness of each fiber ; correspondingly it needs semicontinuity of the objective only in the action variable, at each state separately, and it recovers all of as the regularity class rather than a semicontinuous or continuous sub-class of it.
Proposition 2.4.3 and Proposition 2.4.8 show, respectively, that preserves upper semicontinuity (resp. continuity) of and that a maximizer exists, when is compact and is upper semicontinuous (resp. continuous); Theorem 2.4.6 and Theorem 2.4.10 package these into concrete instances of (SAN). Lemma 2.4.7 gives a checkable criterion — weak continuity of the kernel — for Theorem 2.4.6's integral-semicontinuity hypothesis. Proposition 2.4.11 drops all topological structure on itself, keeping only pointwise compactness of plus semicontinuity of the objective in the action alone, and is what the goal theorem invokes directly, via a projection theorem of Kunugui and Novikov in place of the sequential compactness argument used for Proposition 2.4.3.
Compactness of the action set together with semicontinuity of the reward is the textbook
Weierstrass mechanism for the existence of a maximizer in ordinary optimization; the content of
this chapter is doing the same thing correctly when the maximization varies measurably over an
uncountable state space , so that the resulting maximizer is not just pointwise-optimal but a
genuine decision rule (a measurable function of the state). No formalized version of this theory
exists on the platform: BertsekasDP's existence theorems are for finite state-and-action-space
models, where is automatically compact (in the discrete topology) and every real-valued
function on it is automatically semicontinuous, so none of this chapter's actual content —
choosing a measurable maximizing selection as the state varies continuously — has any analogue
there. This chunk earns the generalization rather than restating that finite-state prior art.
The three "compactness implies (SAN)" theorems of this chapter (2.4.6, 2.4.10, 2.4.13) trade regularity of the action correspondence against regularity of the resulting value-function class: assuming more about how varies (continuity, in Theorem 2.4.10) buys a stronger conclusion (continuous, not merely upper semicontinuous, value functions); assuming nothing about beyond pointwise compactness (Theorem 2.4.13, the goal) forces the weakest conclusion, that the whole class is preserved, via a genuinely different, measure-theoretic argument (a projection theorem) rather than the sequential compactness argument common to Propositions 2.4.3 and 2.4.8. Formalizing all three side by side, rather than only the goal in isolation, is what exposes this trade-off as three logically independent theorems rather than one theorem instantiated three times, and is why every one of the section's numbered results is kept as an item of this mission (per the CAPTAIN's budget instruction to include, not cut, results of genuine independent content) rather than only the smallest set literally required by the goal's own proof tree.
State and action spaces carry MeasurableSpace, TopologicalSpace, BorelSpace instances
throughout (the section's own standing assumption that , are Borel spaces), but no
metrizability or separability instance is required beyond what each statement's own topology
needs — sequences suffice for every semicontinuity notion used here, matching the book's own
Appendix A, which is stated for metric spaces. The Markov Decision Model, its operators
(, , ), the notion of a maximizer, and the Structure Assumption are restated
from chunk 02a-model-bellman-equation in this mission's own MDPFinance.Semicontinuous
namespace (drafts in this series cannot import one another). Set-valued upper/lower
semicontinuity (Appendix A.2.1) is formalized with the book's own sequential definition, not
Mathlib's neighborhood-filter-based UpperHemicontinuous/LowerHemicontinuous for
correspondences — the book explicitly remarks that its own definition is "slightly more
restrictive than other definitions appearing in the literature" (p. 351), so identifying the two
without proof would silently substitute a different notion. The classes ,
are formalized via the book's own equivalent bound-by-a-constant
characterization rather than through the weighted supremum norm itself, avoiding
EReal division and its 0/0 := 0 convention for no loss of content. Each of Theorem 2.4.6's
and Theorem 2.4.10's closing "in particular" sentences — restating chunk 02a's Theorem 2.3.8
applied to the (SAN) instance just constructed — is not repeated in this mission's Lean, since it
is a corollary of a different chunk's goal, not new content of this section; only the "(SAN) is
satisfied" conclusion that is this section's own contribution is stated. A trivializing
formalization of the goal would specialize to a finite type or fix to a single
compact set independent of , making hypotheses (i)-(iii) vacuous; this mission states the
theorem for arbitrary Borel and a genuinely state-dependent .
Many computations in numerical linear algebra, statistics and computational physics need the trace of a matrix that is never formed explicitly: may be an inverse, a matrix function , or a product of large operators, and the only affordable access is a routine that returns for a given vector . Examples include log-determinants and the generalized cross-validation criterion in statistics, counting eigenvalues in an interval, and charge densities in electronic-structure computations. Monte Carlo trace estimators handle this setting: draw random vectors , and average the quadratic forms , each of which costs one matrix–vector product.
Hutchinson (1990) introduced the estimator with Rademacher vectors and computed its variance. Avron and Toledo (J. ACM 2011) replaced variance statements with sample bounds: how many samples guarantee relative error with probability . Section 6 of their paper proves one such bound for an entire class of estimators at once, the normalized Rayleigh-quotient trace estimators, which contains Hutchinson's estimator and the unit vector estimator. This mission formalizes that bound (Theorem 6.1).
Let be symmetric positive semi-definite, with eigenvalues and rank . Write for the largest eigenvalue and
defined for ; it is the condition number of on its range.
A normalized Rayleigh-quotient trace estimator of with samples is
where are independent random vectors in with and for each (Definition 3.2). The vectors need not be identically distributed. Hutchinson's vectors ( entries, i.i.d. uniform) and the vectors with uniform are instances.
A random variable is an -approximator of if
(Definition 4.1).
For every nonzero symmetric positive semi-definite , every , , and every normalized Rayleigh-quotient estimator of ,
The result is distribution-free within the class: it needs only normalization and unbiasedness, so it covers Hutchinson's estimator, the unit vector estimator and any future normalized scheme with one argument. For well-conditioned matrices of full or nearly full rank the required number of samples is , independent of . For ill-conditioned matrices the bound degrades with , which is the reason the paper proves sharper estimator-specific bounds in Sections 7 and 8; Theorem 6.1 is the baseline those results are compared against (Table I, p. 8:5).
The theorem is proved in the paper. No machine-checked version of it, or of any sample bound for trace estimators, is known to exist. The formalization adds a precise statement of the class of estimators on a general probability space, a corrected threshold (see below), and a Lean development that connects Mathlib's spectral theorem for symmetric matrices with its Hoeffding inequality for independent bounded variables.
Each step is short on paper; the work is in the interfaces. The eigenvalue inequality of milestone 1 requires relating the number of nonzero eigenvalues (with multiplicity) to and handling the maximum and minimum over the nonzero spectrum. Milestone 2 is the Rayleigh-quotient bound , which is a consequence of the spectral decomposition rather than a one-line identity. Milestone 3 applies Hoeffding's inequality to summands that are bounded only almost surely, are not identically distributed, and whose mean is fixed by hypothesis rather than computed; the two-sided bound must be assembled from two one-sided tails, and the event must be rescaled to a statement about the sum . A naive attempt that fixes a particular distribution for the (Rademacher, say) proves a different, narrower theorem and does not settle the goal.
Matrix (Fin n) (Fin n) ℝ with A.PosSemidef and A ≠ 0; eigenvalues are Mathlib's IsHermitian.eigenvalues. is lambdaMax (the maximum eigenvalue) and is kappaF (maximum over minimum of the finite set of nonzero eigenvalues); both are Finset.max'/min'/sup' of nonempty finite sets. is a placeholder, and every statement assumes .z : Fin M → Ω → Fin n → ℝ satisfying IsNormalizedRayleighSample P A z: each measurable, the family mutually independent (iIndepFun), almost surely, and . The estimator is universally quantified over this class. Unbiasedness is required for the given only, as on the page. Probabilities are P.real of events; is a natural number and is (M : ℝ)⁻¹.IsNormalizedRayleighSample.Cost and benefit allocation problems arise whenever several parties share a joint undertaking: towns building a common water supply, divisions of a firm sharing overhead, users of a multi-purpose reservoir. They are modelled as cooperative games, and a rule that divides the joint value among the players is an allocation procedure. The standard such rule, the Shapley value, was characterized by Shapley (1953) through efficiency, symmetry, a dummy axiom and additivity. Additivity (the allocation of a sum of two games is the sum of the allocations) is a mathematical convenience with little direct appeal in applications, and it has been the most criticized of the four axioms.
H. P. Young's paper Monotonic Solutions of Cooperative Games (Int. J. Game Theory 14, 1985) studies allocation procedures through monotonicity: how a player's allocation should respond when the game changes. Its Theorem 1 shows that the core is incompatible with coalitional monotonicity for five or more players (the subject of the sister mission of this series). Its Theorem 2, the subject of this mission, shows that efficiency, symmetry and a single monotonicity axiom — strong monotonicity — determine the Shapley value, with no additivity axiom at all. The result is widely cited as Young's axiomatization of the Shapley value, usually in the form with the marginality condition (7) that the paper states in its remarks.
Timeline:
Fix and the player set . A game is a function on the coalitions with ; superadditivity is not assumed. An allocation procedure is a map assigning to each game a vector with (efficiency).
The marginal contribution of player to coalition (Eq. (3)) is
defined for every . The Shapley value is
The axioms:
A primitive game () takes the value on coalitions containing and elsewhere.
For every map from games on to ,
Both directions are part of the goal: the Shapley value has the three properties, and it is the only map that has them.
Efficiency and symmetry of the Shapley value are supporting theorems of the existence half; the paper uses them without separate statement.
The result. Theorem 2 shows that additivity is not needed to single out the Shapley value: a player's payoff is pinned down by symmetry, efficiency, and the requirement that it respond monotonically to that player's own marginal contributions. This gives the Shapley value a justification that can be checked directly in applications — a division that improves its marginal contributions to every coalition is never penalized — and the marginality form (7) is the standard starting point for characterizations on restricted classes of games and for extensions to games with a variable player set.
The formalization. The theorem is proved and classical; no machine-checked proof of it is known to exist. The mission produces a checked proof of Young's characterization together with reusable infrastructure: marginal contributions, the unanimity-game basis of the space of games (a Möbius-inversion statement on the subset lattice), the Shapley value on unanimity games, and the Shapley value's efficiency, symmetry and monotonicity for the published ShapleyValue definition. These are the ingredients of most other axiomatizations of the Shapley value (Shapley 1953, Hart–Mas-Colell's potential) and are useful beyond this mission.
The existence half is a direct computation. The uniqueness half cannot proceed by linearity, since is not assumed additive: knowing on each primitive game says nothing directly about on their sum. The obvious idea — decompose into primitive games and add up — therefore fails. What must be controlled instead is how much of a game each player "sees" through the marginal-contribution vector alone, and how symmetry and efficiency distribute what remains. The formal proof also has to manage the dependence of the argument on a minimal-length expression (9) while keeping all comparisons inside the class of games with .
Fin n: the paper's player is the Lean index . The player set is fixed, and is a single map Game n → Fin n → ℝ, as in the paper; no lower bound on is needed (at both sides of the goal hold).Game n := {v : Finset (Fin n) → ℝ // v ∅ = 0}. The normalisation is essential: on arbitrary set functions a constant game would receive per player from every efficient symmetric procedure, but from the Shapley formula, and Theorem 2 would be false.Supermodularity.Cooperative.ShapleyValue, written as a sum over with weight ; it agrees term by term with the formula above.Contributions welcome: proofs of the milestones in any order, general lemmas on unanimity-game expansions over Finset powersets, and alternative proofs of the uniqueness half.
Every packet-switched network — an internet router, a data-center fabric, a wireless base station — must decide, timeslot by timeslot, which of many competing transfers to schedule under shared physical constraints (link capacities, interference between simultaneous transmissions). Walton (2015) introduced the random proportional scheduler (RPS): rather than solving a combinatorial scheduling problem exactly, RPS picks a randomized link configuration whose mean matches the proportionally-fair allocation of Kelly (1997) applied at the link level, then disaggregates the resulting transfer budget across competing packet classes by independent random selection. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) devotes Sections 12.6-12.7 to this policy, and closes the book with Theorem 12.28: under an explicit load condition, RPS is stable. This mission formalizes that closing result and the machinery beneath it. It is the fourteenth and final mission of a series covering the book chapter by chapter; the series as a whole runs from the equivalence of stochastic-processing-network stability and fluid-model stability (mission I, Theorem 3.5/6.2) through discrete-time, slotted packet networks (missions XII-XIV), and this mission's own goal theorem is the last numbered result the book proves.
A packet network with fixed routing (Section 12.6) has I packet classes; each class i
routes, after one hop of processing, deterministically to a single successor class or exits the
network — encoded here as a function . The K
links are indexed by , and a matrix assigns each class to the single link its next
transfer uses; denotes the classes belonging to link . At the start of a
timeslot, is the vector of class-level packet counts and the
corresponding link-level counts. The RPS algorithm (four steps, page 245 of the printed book):
(a) solve the concave program (Eq. 12.57), where is the finite set of feasible link configurations
and its convex hull; (b) randomize a link configuration with mean ;
(c) transfer packets over link ; (d) select which packets to transfer uniformly
at random from each link's queue. This makes a discrete-time
Markov chain. The function is exactly the proportionally fair (PF) allocation function
of Section 10.1, applied here with the link-level demand vector in place of the PF model's
job-class demand vector.
Here is the vector of external arrival rates, the resulting vector of total (external plus internally routed) arrival rates into each class, and the input-output matrix determined by . The load condition (12.50) is the natural feasibility requirement — average link traffic strictly below some feasible mean capacity — and the theorem asserts it is also sufficient for stability.
Lemma 12.23 is an almost-sure convergence result for a residual process tracking the gap between RPS's actual per-class transfers and their conditional means — a bounded martingale-difference sum, hence governed by the strong law of large numbers. Theorem 12.24 is the RPS fluid equation: along any fluid limit on the event where both Lemma 12.12's arrival-process SLLN and Lemma 12.23's residual-process SLLN hold, every occupied class's departure rate is pinned to . Proposition 12.26 identifies the resulting RPS fluid model as literally a special case of the PF fluid model of Section 10.4 (one demand group per link, playing the role of the PF model's reduced allocation set), and Theorem 12.27 is this chapter's own version of the fluid-to-stochastic transfer theorem (Theorem 6.2's slotted-time analogue, restricted to RPS): fluid stability of the RPS model implies positive recurrence of .
The result itself. Theorem 12.28 closes the loop the book opens with proportional fairness in Chapter 10: PF was introduced there as a static resource-allocation rule with no queueing content; Theorem 12.28 shows that layering PF onto a genuinely dynamic, multi-hop, discrete-time packet network — RPS — inherits stability under exactly the load condition one would hope for, with no loss from the randomized disaggregation step (d) of the algorithm. Combined with Theorem 12.8 (packet-network stability implies subcriticality, mission XII) and Eq. (12.50)'s equivalence to that subcritical region under fixed routing, this makes RPS maximally stable: it is stable whenever any Markovian policy could be.
Formalizing it. A live prior-art check (GET /theorems?q=proportional+scheduling) finds no
relevant hits on the platform. This mission's genuine content is Proposition 12.26's reduction:
rather than re-deriving an entropy-Lyapunov stability argument specific to RPS, it identifies the
RPS fluid model precisely with mission IX's PF fluid model under an explicit correspondence, so
that Theorem 12.28(a) is a direct instance of mission IX's own Theorem 10.5 and Theorem 12.28(b)
a direct instance of this mission's own Theorem 12.27. This is the payoff the whole
proportional-fairness apparatus (missions IX-X) was built for.
The central subtlety is that Theorem 12.24's departure-rate equation is stated in terms of a
class-indexed process , while the chapter's own general fluid-equation machinery
(Theorem 12.13, mission XII) is built around an activity-indexed process — a distinction that
matters when a packet network has more service types than classes. Under Sections 12.6-12.7's own
fixed-routing model, however, the book's remark that " ... is an I-vector of actual
packet transfers by class" (page 245) collapses this distinction: each class has a single
associated activity, so the activity-indexed and class-indexed views coincide, and the RPS fluid
model can be built directly on the same class-indexed apparatus the PF fluid model (Section 10.4)
already uses. Missing this identification is the natural way to get stuck restating Proposition
12.26 as a mere analogy rather than the literal equivalence the book states. A second difficulty
is Lemma 12.23 itself: its proof cites Feller's strong law for bounded martingale-difference
sequences as an external fact rather than deriving it, so a faithful statement must commit to an
explicit representation of "martingale difference sequence" (a filtration and Mathlib's
Martingale predicate) even though no full measure-theoretic construction of the underlying
probability space is attempted.
Classes and links are Fin-indexed; route : Fin I → Option (Fin I) records each class's
deterministic routing successor (none meaning exit), and the resulting input-output matrix
and routing matrix are derived from it rather than taken as independent data (this chunk
verifies , the identity Proposition 12.26's reduction to the PF model relies on).
The RPS optimization apparatus (psi, groupAggregate, the PF fluid-model predicate) is restated
verbatim from mission IX, and the general packet-network fluid equations restated from mission
XII, since concurrently-drafted chunks in this series never import one another's Lean files even
within a shared sub-namespace. The formalization does not admit a trivializing reading: the load
condition in Theorem 12.28 is a genuine strict inequality against the convex hull of feasible
configurations (not weakened to or to a single configuration), RPSFluidStable quantifies
over every solution of the RPS fluid model (not a hand-picked one), and Proposition 12.26 is
stated as a two-sided equivalence, not a one-directional inclusion that would understate "special
case." Contributions completing the five by sorry proofs are welcome, particularly Lemma 12.23's
martingale strong law (Feller 1971, Theorem 3, Section VII.8) and Theorem 12.24's fluid-limit
argument (mirroring mission XII's own Theorem 12.13 proof).
Retailers of fashion and seasonal goods sell a fixed stock over a short season and routinely cut the price part-way through it. The markdown trades off two effects: a late discount keeps early, high-valuation customers paying the full price, while an early discount reaches customers whose interest in the product fades as the season goes on. Aviv and Pazgal (MSOM 2008) build a two-price model of this trade-off with Poisson arrivals and valuations that decline exponentially over the season, and compare sellers facing myopic customers, who buy as soon as the current price is acceptable, with sellers facing strategic customers, who may wait for the discount.
This mission formalizes the benchmark of that comparison in which the problem can be solved in closed form: myopic customers who all share the same base valuation, so that the only source of price discrimination is the decline of valuations over time. Proposition 4 of the paper identifies the optimal premium price, discount price and discount time, and the paper's Proposition 5 and Example 1 then measure how much strategic behaviour costs the seller against it.
The season is . Customers arrive as a Poisson process with rate , so is the expected number of arrivals in the season. Every customer has base valuation , and a customer's valuation at time is for a fixed decline parameter (equivalently with ; is the fraction of the valuation left at the end of the season). In the paper's notation this is the case , , of a family of Gamma-distributed base valuations with mean and coefficient of variation ; the tail of the base valuation is for and otherwise.
The seller posts a premium price on and a discount price from the discount time on, and has unlimited inventory. A myopic customer arriving at buys at once iff ; otherwise the customer waits and buys at iff . A customer arriving after buys iff the current valuation is at least . The expected numbers of buyers in the three groups are the segment rates , and , and the expected revenue is
For a price let , the time at which the valuation has fallen to , and write , . The reduced objective is
every maximizer of together with every with attains , and, if , the maximizer is unique,
and every with is optimal.
For :
Proposition 4 gives an explicit optimal markdown policy in a model where segmentation happens purely by arrival time: it shows that the discount time is not pinned down but can be placed anywhere in the interval in which the valuation lies between the two prices, and that for strongly declining valuations the optimal prices do not depend on at all. The paper uses it as the benchmark against which the strategic-customer equilibrium of Proposition 5 and the losses of Example 1 are measured.
The result is proved in the paper by a short argument; nothing in it has been machine-checked. A formal development makes the three observations of the proof precise (in particular, that prices outside are dominated, which the paper leaves implicit) and supplies the omitted calculus for the special case.
The revenue is defined through integrals of a step function of time, and the reduction to needs these integrals evaluated in every configuration of , and , including prices above (nobody buys) and below (everyone buys, at a needlessly low price). The paper's proof covers only and asserts the domination of the remaining prices without argument. The special case is a constrained two-variable maximization of a function that is not jointly concave; the unconstrained critical point must be shown to be feasible exactly when , and boundary points of the region must be excluded.
Everything is over . Logarithms are Real.log, powers are real powers, the segment rates are interval integrals ∫ t in a..b of the tail , and with . The model definitions (, , and the revenue) are stated for a general tail , decline factor, season length and discount time and then specialized.
The following readings of the paper's words are fixed:
IsGreatest of the set of attainable revenues.The decimals and are not stated. A formalization that restricted prices to in the revenue maximization, or that fixed in advance, would assume half of what the proposition proves and is ruled out. Welcome contributions include general lemmas evaluating interval integrals of indicator functions of intervals, and the domination argument for prices outside .
Robust optimization (RO) protects a decision against every parameter value in an uncertainty set. For a decision and a parameter with objective to be maximized, the robust problem around a nominal parameter with a deviation set is
When deviations are not adversarial, this formulation is known to be conservative (Delage and Mannor, 2010; Xu and Mannor, NIPS 2006). A common remedy in practice is uncertainty set shrinkage: fix and solve the same problem over the shrunken set . The heuristic is easy to implement, but the meaning of the set is unclear, and it has lacked a justification.
Section 4.2 of Xu, Caramanis and Mannor (2012) supplies one, using the paper's distributional interpretation of RO: the shrunken problem approximately solves a distributionally robust stochastic program (DRSP) with two scenarios. This mission formalizes that result, Theorem 4.1, and its two corollaries.
Let carry the Euclidean norm and its Borel -algebra, and let be the set of Borel probability measures on . Let be any set of decisions and . Fix , a deviation set , and . Write .
The two-scenario set is
A distribution in describes a system that is, with probability at least , in a normal state where the parameter equals , and otherwise in an abnormal state where the parameter deviates by an element of . The DRSP value of a decision is .
Two further quantities enter. The radius of the deviation set is . The curvature bound is a constant with
where is the Hessian of at and is the positive-semidefinite order. In the Lean development these are scenarioSet x₀ Δ (1 - α), drspValue, devRadius Δ and HasBoundedHessian (f v) h, all in the namespace DistInterpRO.Shrinkage.
If is twice differentiable with for all , then for all
Corollary 4.2 (p. 104): if every is linear, the shrunken value equals the DRSP value exactly. Corollary 4.3 (p. 105): if is star shaped, every is convex with and has Hessian bounded by , then the shrunken value lies between the DRSP values over and , where requires only .
The result gives a physical meaning to the parameter of the shrinkage heuristic: is a lower bound on the probability that the system is in its nominal state. The error vanishes when the objective is linear in the parameter (Corollary 4.2), which covers linear programs with uncertain costs and Markov decision processes with uncertain rewards; in that case shrinkage is exactly a two-scenario DRSP. The paper also shows by example (p. 104) that without a curvature condition the two problems can differ, so the Hessian bound is the operative hypothesis.
The result is proved in the paper; to our knowledge it has no machine-checked proof. Formalizing it adds a checked link between the discrete two-point structure of the DRSP value and the smooth analysis of the shrunken minimum, with every standing hypothesis written out (see below). The mean-value and gradient-Lipschitz steps are general facts about functions on Euclidean space with bounded Hessian and are reusable elsewhere.
Two points need care. First, the step from the Hessian bound , a bound on a quadratic form, to the Lipschitz bound on the gradient requires the operator norm of the Hessian, which equals the largest absolute value of its quadratic form only because the Hessian is symmetric; symmetry of second derivatives must be invoked for a function that is merely twice (Fréchet) differentiable, not twice continuously differentiable. Second, the DRSP value is an infimum over an infinite-dimensional set of measures; identifying it with the two-point value requires both a construction of a near-optimal measure and a lower bound valid for every admissible measure, including measures that spread their abnormal mass over all of .
is EuclideanSpace ℝ (Fin m) with its Borel -algebra. Measures are Measures, and membership in includes IsProbabilityMeasure. Infima are real infima over subtypes; integrals are Bochner integrals.
The formalization makes the following readings explicit:
The Lean functions drspValue and devRadius return on an empty or unbounded input; the hypotheses above exclude those inputs, so no statement holds through a junk value. A formalization that dropped would make the inequalities hold or fail for the wrong reason and is ruled out.
Contributions welcome: the Lipschitz-gradient lemma for bounded Hessians in Euclidean space, the evaluation of the two-scenario DRSP value, and the combination into Theorem 4.1 and its corollaries.
Robust optimization (RO) protects a decision against every realisation of an uncertain parameter in a prescribed uncertainty set; distributionally robust stochastic programming (DRSP) protects it against every probability distribution in a prescribed distribution set. The two paradigms are usually treated separately. When the n uncertain parameters live in different spaces, it is folklore that RO over a product of sets is DRSP over the distributions supported on that product (Delage and Ye, Operations Research 2010).
In data-driven problems the situation is different: the parameters are samples, and all of them lie in the same space . Robustifying each sample by its own uncertainty set gives the objective , and the sets typically overlap. Xu, Caramanis and Mannor (Math. Oper. Res. 2012) show that this objective is again a worst-case expectation, now over distributions on itself rather than on . This equivalence is what the same paper uses to prove that box-robust sample average optimisation is statistically consistent, and to explain the shrinkage heuristic of RO.
Let and write . Let be the set of Borel probability measures on . The data are:
For write and . The distribution set is
Each must give every union of uncertainty sets at least the total weight of its indices. For the expectation is the extended integral .
as an identity in , with no boundedness assumption on and no disjointness assumption on the .
The result. Theorem 2.1 turns a robust problem with overlapping uncertainty sets into a distributionally robust one on the original space . This is what allows distributions in to be compared with the true data-generating distribution as grows: in §3 of the paper a kernel density estimator is shown to lie in for box uncertainty sets, which yields consistency of box-robust sample average optimisation (Theorem 3.1); in §4.2 the nested-distribution form (Corollary 5.2) explains why shrinking an uncertainty set approximates a two-scenario DRSP (Theorem 4.1). The disjoint case recovers the classical product-space equivalence.
Formalizing it. The result is proved in the paper, through the strong duality of a semi-infinite linear program (Isii 1962). It has no machine-checked proof. The mission produces the equivalence as an identity of extended reals, together with a reusable definition of the union-mass distribution set. A proof need not follow the paper's duality route; any correct argument is welcome.
The inequality from the left side is the easy half: point masses with belong to . The substance is the reverse bound, that no can do better than . For disjoint sets this is immediate, since . For overlapping sets a measure may place mass in intersections, and a single point of can serve several indices at once; the constraint family over all subsets is what prevents this, and the bound has to exploit the whole family, not the singleton constraints. The paper does this by appeal to semi-infinite LP duality, a theorem that Mathlib does not contain. Measure-theoretic side conditions (unbounded , infinite integrals, infima equal to ) must also be handled rather than assumed away.
Fin m → ℝ with its Borel -algebra; no norm is used. Indices are Fin n, subsets are Finset (Fin n), and is Finset.Iic i.Set (Measure (Fin m → ℝ)) whose membership includes IsProbabilityMeasure; the constraint is imposed for every subset, and included.expect μ f, defined in EReal as the difference of two lower Lebesgue integrals, . The Bochner integral is not used, because its value on non-integrable functions would falsify Eq. (4). Both sides of Eq. (4) are EReal infima; the left infimum ranges over the nonempty set .Model): the set , the extended expectation, dual feasibility, and the nested dual vector. The extended expectation and the union-mass distribution set are reusable beyond this mission. Welcome contributions: a proof through semi-infinite LP duality, a direct measure-theoretic proof (for instance a layer-cake argument for the lower bound), and proofs of the corollaries from the goal.Stochastic approximation is the family of recursive algorithms that locate a zero of a function observed only through noisy evaluations. It goes back to Robbins and Monro (1951) and today underlies stochastic gradient descent, temporal-difference learning, Q-learning and actor–critic methods in reinforcement learning, and models of learning by boundedly rational agents.
The standard analysis is the O.D.E. method (Ljung 1977; see Kushner and Yin 1997): the interpolated iterates are compared with the solutions of an ordinary differential equation, and convergence of the algorithm follows from the stability of that ODE. The method has one well-known gap. It assumes, rather than proves, that the iterates remain bounded with probability one. In applications this stability hypothesis is often the hardest part: for asynchronous Q-learning and adaptive critic algorithms, almost sure boundedness had been proved only for discounted cost or after adding a projection step (Borkar and Meyn, p. 460).
Borkar and Meyn (SIAM J. Control Optim. 38 (2000)) close this gap with a scaling argument borrowed from the fluid-model approach to the stability of queueing networks (Dai 1995; Dai and Meyn 1995). They show that boundedness itself follows from the asymptotic stability of the origin for a second, "fluid-limit" ODE obtained by rescaling the drift. This mission formalizes that stability theorem for tapering step sizes, and the convergence theorem that follows from it.
Fix and work in with the Euclidean norm. Let and let be a deterministic sequence of positive step sizes. On a probability space , random vectors and satisfy the stochastic approximation recursion
Its mean ODE is (1.2). For the scaled field is , with the scaled ODE (1.4).
A point is globally asymptotically stable for if it is a Lyapunov-stable equilibrium and every solution converges to it.
Under (A1), (A2) and (TS), if has a unique globally asymptotically stable equilibrium , then for every initial condition ,
The goal contains no constants and no rates, only the qualitative conclusion.
Under (A1), (A2) and (TS), for every initial condition,
The result. Theorem 2.1 (i) turns the stability hypothesis of the O.D.E. method into a checkable condition on a deterministic ODE. Theorem 2.2 then gives convergence to with no a priori boundedness assumption. The paper applies this to reinforcement learning, obtaining the first convergence proof for asynchronous Q-learning and adaptive critic algorithms for average-cost Markov decision processes (the asynchronous extension, Theorem 2.5, is sketched in the paper and is not part of this mission). The same fluid-limit criterion is now a textbook tool; see Borkar, Stochastic Approximation: A Dynamical Systems Viewpoint (2008), Chapter 3.
Formalizing it. The theorems are proved in the paper, and the proofs are short but rely on several standard facts stated informally: uniform convergence of to on compact sets, continuous dependence of ODE solutions on initial data and on the vector field, and the martingale convergence theorem. No machine-checked version of the O.D.E. method or of this stability criterion is known to exist. A formal development would give a verified link between discrete-time stochastic recursions, martingale convergence in Mathlib, and the stability theory of Lipschitz ODEs.
The obvious approach is to compare the iterates with solutions of over windows of fixed ODE time and to control the accumulated noise by martingale convergence. This fails without boundedness: the noise bound in (A2) grows with , so the deviation from the ODE can only be controlled relative to the current size of the iterate, and nothing prevents the iterates from escaping to infinity.
A second difficulty is that the hypothesis (A1) concerns only the fluid limit , which describes the drift at infinite scale. It says nothing directly about at any finite state, and nothing about the noise. Any argument therefore has to transfer information from the limit to the recursion at random, path-dependent scales, uniformly over those scales, while the noise is controlled only relative to the current size of the iterate. In Lean this involves ODE comparison and Gronwall estimates on a random partition of the time axis, conditional second-moment estimates for a rescaled recursion, and a vector-valued martingale convergence argument, none of which is available off the shelf for this setting.
The state space is EuclideanSpace ℝ (Fin d). An ODE solution is a forward solution on : the derivative is taken within at each , which makes solutions continuous there. Stability notions are the standard ones (Lyapunov stability; asymptotic, global asymptotic and global exponential stability, the last in the form ). All vector fields in the mission are Lipschitz, so forward solutions exist and are unique, and quantifying over "every solution" is meaningful.
The filtration in (A2) is the natural filtration of the iterates. Because , it carries the same information as the paper's . (A2) includes integrability of and , so that the conditional expectations are meaningful. The theorems quantify over every probability space and every noise process satisfying (A2); the goal and Theorem 2.1 (i) take a deterministic initial condition, as the paper does. Stating the goal for a particular noise model (no noise, or i.i.d. noise) would be a different and much weaker theorem, and is ruled out. "" is boundedness above of the set of norms, not a real supremum, which Lean sets to on unbounded sets. Second-moment suprema in Lemma 4.5 are taken in .
The proof objects of Section 4.1 (time grid , blocks and , scales , the interpolation , the rescaled iterates and noise sum) are separate definitions built from the step sizes and the sample path, as on the page. The piecewise ODE solutions and are characterized by a predicate, and the lemmas hold for every function satisfying it.
Useful infrastructure, reusable beyond this mission: Lipschitz ODE comparison and continuous-dependence estimates in Mathlib's ODE library, uniform convergence of on compact sets, the discrete Gronwall lemmas, and -bounded vector-valued martingale convergence. Contributions are welcome on any milestone. The two Gronwall lemmas and Lemma 4.1 are self-contained entry points.
Statistical learning theory asks when the empirical frequencies of a whole class of events converge to their probabilities uniformly over the class. Vapnik and Chervonenkis answered this question in 1971 (Theory Probab. Appl. 16 (1971) 264–280) by attaching to every class of sets a single combinatorial quantity, the growth function, and bounding the probability of a large uniform deviation in terms of it. For that bound to be useful, the growth function must grow more slowly than an exponential. The first result of the paper, Theorem 1, shows that the growth function of any class is either exactly or bounded by a polynomial. This dichotomy is the reason finite VC dimension (the size of the largest fully shattered sample) became the central complexity measure of learning theory.
Timeline of the combinatorial core:
Let be a set and a collection of subsets of . A sample of size is a finite sequence of elements of ; repetitions are allowed. Each induces in the sample the subsample of the terms that lie in , which is determined by the set of positions .
The index is the number of different subsamples induced by the sets of , i.e. the number of distinct sets of positions with . It is at most . The growth function is
the maximum over all samples of size . For the rays on the line ; for the open subsets of , .
The function on pairs of natural numbers is defined by the recurrence (1) of the paper,
In the Lean development these are index S x for x : Fin r → X, growthFunction S r, and Phi n r in the namespace VapnikChervonenkis.GrowthFunction.
For a nonempty class , either for every , or, with the first value of at which fails,
The exponent is pinned down by minimality: and for every .
Theorem 1 converts the distribution-free bound of Theorem 2 of the same paper into a convergence statement: whenever the growth function is not identically , the right-hand side is a polynomial times a decaying exponential, so relative frequencies converge to probabilities uniformly over . The same dichotomy underlies sample-complexity bounds for PAC learning, covering-number bounds for VC classes, and the notion of VC dimension itself; the exponent is the VC dimension plus one.
The results are classical and proved. Mathlib contains the Sauer–Shelah lemma for finite set families (Finset.card_shatterer_le_sum_vcDim in Mathlib/Combinatorics/SetFamily/Shatter.lean). The platform has several open formal statements of Sauer's lemma for growth functions over finite point sets (ComputationalLearning.sauer_lemma, FoundationsML.RademacherVC.sauer_lemma, HighDimProb.Chaining.sauer_shelah) and a closed form for Kearns–Vazirani's (ComputationalLearning.phi_closed_form, the same recurrence). No statement of Theorem 1, and none over the paper's sequence model of samples, is formalized. This mission formalizes the paper's own route: Lemma 1 in the paper's form, the polynomial bound on , and the dichotomy with the minimal exponent. It also provides the growth function over sequences that the companion missions (Theorem 2, and the entropy criterion Theorem 4) are stated with.
The obvious argument has two steps: bound by whenever no subsample of size is fully split, then bound by . The first step is the Sauer–Shelah lemma, and it does not follow from counting alone. A class can induce many subsamples on points without inducing all on any fixed of them, and no counting of subsamples one position at a time rules this out. The second step is elementary but must hold uniformly for all , including , where and the bound uses .
Samples are sequences, not sets. With repeated points, two positions carrying the same point can never be separated, so Lemma 1 must be applied to position sets rather than point sets. Transferring Mathlib's set-family lemma to this setting is a bookkeeping step that does not reduce to a citation.
x : Fin r → X with positions ; repetitions are allowed. A subsample of size is x ∘ e with e : Fin n → Fin i strictly increasing.index S x counts distinct Finset (Fin r) of positions {i | x i ∈ A} with A ∈ S. Counting point sets A ∩ {x_1, …, x_r} instead would be a different object when points repeat; the growth function over finite sets of points (as in ComputationalLearning_VC) differs from when has fewer than elements.growthFunction S r is the supremum in ℕ of index S x over all samples; the family is bounded by , so it is a maximum. When is empty and its value is ; exactly when is nonempty.Phi is defined by the recurrence (1). The paper introduces as the maximal number of components into which hyperplanes cut -space; that geometric identity (Example 3) is not part of this mission.No measure, σ-algebra or probability appears: the class is an arbitrary collection of subsets of a bare type. Needed infrastructure: basic API for index (monotonicity in the sample, behaviour under restriction to a subsample) and a bridge between samples and Mathlib's set families (Finset.Shatters, Finset.vcDim). Both are reusable by the two companion missions of this paper, and contributions of either are welcome.
Scheduling jobs on unrelated machines so as to minimize the makespan (the time at which the last machine finishes) is one of the central problems of approximation algorithms. For the general problem, Lenstra, Shmoys and Tardos (1990) gave a 2-approximation and showed that no polynomial-time algorithm achieves a factor below unless P = NP; closing the gap between and has been open since.
The restricted assignment problem is the special case in which every job has a single size and may only run on a given set of machines. The hardness already holds here, and the best known algorithms were still -approximations. Every linear program previously used for the problem has integrality gap , so a better LP lower bound was the natural target.
Svensson (2011) showed that the configuration LP of Bansal and Sviridenko (2006), whose variables assign whole sets of jobs to machines, has integrality gap at most . Its optimum therefore gives a polynomial-time estimate of the optimal makespan within a factor strictly better than .
An instance consists of finite sets (jobs) and (machines), sizes , and for each job a set . A schedule is a map with . The load of machine is , and the makespan is the largest load. is the least makespan of a schedule.
For a target makespan , a configuration for machine is a set of jobs that may all run on ( for ) with . Write for the set of configurations. The configuration LP asks for with
Its dual has variables and constraints for all and . is the least at which [C-LP] is feasible, and .
In the Lean development these are configs Γ p T i, CLPFeasible Γ p T, CLPDualFeasible Γ p T y z and schedLoad p σ i, in the namespace RestrictedAssignment.Svensson.
For every instance with and every ,
Equivalently . The statement is scale-free and does not define .
The milestones follow the paper's proof, which normalizes and sets :
Three facts from Section 2 complete the list: normalization by scaling, , and monotonicity of feasibility in .
The theorem shows that the configuration LP is a strictly stronger relaxation than those behind the factor- algorithms. With the known polynomial-time approximate solvability of the LP, it gives a polynomial-time algorithm that estimates the optimal makespan of restricted assignment within . The local search in the proof finds a schedule of the same quality, but it is not known to run in polynomial time. Later work lowered the constant to (Jansen and Rohwedder, 2017) along the same lines.
The result is proved on paper. As far as known, no part of it has a machine-checked proof. Formalizing it gives:
The milestones are stated with the corresponding hypotheses.
The obvious approach, rounding a fractional configuration solution, loses a factor . If each machine takes one configuration and the collisions of jobs chosen twice or not at all are repaired, the repair can double a load. This is where every earlier LP-based bound stalls.
The milestones along the paper's route are hard for two reasons. First, the dual pair rounds job sizes down by class (big to , medium to ). Proving requires a case analysis over how each blocked machine came to be blocked. The two claims are therefore false for arbitrary states of the search and hold only for states the algorithm actually reaches, so the invariants of reachable states have to be formalized too. Second, the search both adds and removes blockers, so no simple quantity decreases at every step. Termination needs a potential defined on the whole history of the search.
Jobs and machines are finite types with decidable equality, sizes are real numbers with , and admissible machines are a Finset per job. Schedules are total maps with stated explicitly. Partial schedules are maps Option M. Constants are exact rationals in . Values of moves live in Lex (ℝ × ℝ).
Algorithm 2 is a step relation Step, not a function. The move of minimum lexicographic value is a hypothesis on the chosen pair, so every tie-breaking rule is covered. The blocker tree is stored as its list of blockers in insertion order. Claims 4.7, 4.8 and Lemma 4.6 quantify over states reachable from the initial state, as their proofs require. Lemma 4.9 asserts that no infinite run exists.
Three statements would trivialize the goal, and the formalization rules them out:
Theorem 1.1 (polynomial time), the separation oracle, and Section 3's two-size case are not part of the mission.
Useful contributions include:
The configuration LP definitions are reusable for the Santa Claus problem and for bin packing.
Cutting planes for mixed-integer linear programs are often derived from a few rows of an optimal simplex tableau. Keeping rows for basic integer variables , dropping the nonnegativity of (Gomory's corner polyhedron, Gomory 1969) and then the integrality of the nonbasic variables leaves the set of with . Balas observed in 1971 that convex sets with no integral point in their interior give valid inequalities for such sets (Balas 1971). Andersen, Louveaux, Weismantel and Wolsey (2007) for two rows, and Borozan and Cornuéjols (2009) for any number of rows, showed that for rational data the irredundant valid inequalities correspond to maximal lattice-free convex sets. Basu, Conforti, Cornuéjols and Zambelli (arXiv:1701.06543; Math. Oper. Res. 35(3), 2010) removed the rationality assumption. This mission formalizes that result, Theorem 3 of their paper.
Fix , a point and a linear subspace , and assume that the affine space contains an integral point. Products such as are standard inner products.
A function is sublinear if for and .
with on and a maximal lattice-free convex set in with in its interior.
The goal is stated as one conjunction. It fixes no constants and makes no rationality assumption on or .
In the order in which the proof on pp. 15–21 uses them:
Theorem 3 says that the minimal valid inequalities of are exactly those produced by maximal lattice-free convex sets, up to the equivalence forced by the affine hull . It also says that for irrational , where valid inequalities can have negative coefficients, some equivalent form always has nonnegative coefficients. The paper derives two further results from it: a description of the closure of in a suitable norm (Theorem 4), and a reduction of extreme inequalities of the infinite model to finite ones (Theorem 5). Both results remain unproved without it.
The result has a complete proof in the paper, which relies on the cited Theorem 28 from Basu, Cornuéjols, Zambelli. To our knowledge none of it is machine-checked. A formalization would provide a definitional layer for corner relaxations, lattice-free sets and valid inequalities, which is currently absent from Mathlib. It would also expose where the page is imprecise; see the scope section.
For rational data every valid inequality can be written with right-hand side and nonnegative coefficients, and is then the gauge of . For irrational this fails. Since , adding to changes nothing on , so coefficients can be negative, and may have a full-dimensional recession cone. A maximal lattice-free set containing then yields a that need not lie below (the example on pp. 21–22 shows this). One must first pass to an equivalent inequality whose set has no full-dimensional recession cone within . This step combines the structure theorem for maximal lattice-free sets in irrational subspaces (Theorem 9 of the paper) with a duality argument. A second obstacle is that is an arbitrary function: validity alone gives no convexity or continuity, and Lemma 23 is needed to recover them.
EuclideanSpace ℝ (Fin q), is a Submodule, and is W →₀ ℝ. The printed phrase "the set has finite cardinality" is read as ordinary finite support.The paper is imprecise in three places, and the formalization departs from the page in each:
Two kinds of contributions are especially welcome: reusable infrastructure for polars of convex sets relative to a subspace and for sublinear functions on submodules, and a proof of Theorem 28.
Cutting planes for mixed-integer linear programs are often derived from convex sets that contain no integer point in their interior. Balas observed in 1971 that every such lattice-free convex set containing the current fractional LP solution in its interior yields a valid inequality, the intersection cut (Balas, Intersection cuts, Oper. Res. 19, 1971). The strongest cuts come from sets that are inclusionwise maximal, so the shape of maximal lattice-free convex sets matters to multi-row cut generation.
The case where the set lives in a subspace arises in practice. Taking rows of an optimal simplex tableau restricts the integer points to an affine subspace of spanned by the tableau columns. When is irrational, its integer points span only a proper subspace . The classical theory does not cover this case, and it is the case that the second mission of this series (minimal valid inequalities of the relaxation ) needs.
Timeline.
Work in with the Euclidean inner product and the open balls . For , denotes its linear span.
A lattice of a linear space is an additive group generated by linearly independent vectors with (Definition 6, IsLatticeOf Λ V). A linear subspace is a -subspace if it has a basis contained in (Definition 7, IsLambdaSubspace Λ V L). For , the line is a -subspace and the line is not.
For sets the interior relative to is (intW W S). The relative interior is .
Let be a linear space. A set is a -free convex set of if , is convex and . It is maximal if no other -free convex set of properly contains it (Definition 8, IsLambdaFree, IsMaxLambdaFree).
The statements also use a polyhedron in ( intersected with finitely many closed half-spaces), a polytope (convex hull of a finite set), the dimension of the affine hull with (affDim), and a facet: a nonempty face of a valid inequality with . The recession cone is and the lineality space is .
For a lattice of and a linear space with , a set is a maximal -free convex set of if and only if
For , is a maximal -free convex set of if and only if either is a polyhedron with a polytope, a -subspace and , with no lattice point in and a lattice point in the relative interior of every facet; or is an affine hyperplane of whose direction is not a -subspace.
Lemma 13 (bounded full-dimensional case), Lemma 15 (lattice points near half-lines), Lemma 16 ( stays -free), Lemma 17 (projection along a -subspace is a lattice), Lemma 18 (lattice points near non-lattice subspaces), Lemma 19 (maximal hyperplanes), Claims 1 and 2 in the proof of Theorem 10, and identity (6), .
Theorem 10 says that maximal lattice-free sets are cylinders over polytopes with a lattice point on every facet, apart from the irrational hyperplanes. This is the structural fact behind the finiteness of facet counts (at most ) and behind every classification of maximal lattice-free sets in low dimension, such as the triangles and quadrilaterals of the two-row relaxation. Theorem 9 extends it to irrational subspaces. There the new cases are the half-spaces of (iii), which have on their boundary, and the hyperplanes of (ii), whose trace on is a hyperplane of that is not a -subspace. Theorem 9 is the geometric input to the paper's Theorem 3: every minimal valid inequality of is the gauge of a maximal lattice-free convex set of .
These results are proved on paper. No machine-checked version of Lovász's theorem, of Theorem 9, or of the lattice-approximation Lemmas 15 and 18 is known to exist. The mission produces the definitions of lattices of subspaces, relative interiors and lattice-free sets on which the second mission of the series builds.
The obvious argument separates each lattice point from by a half-space and intersects the half-spaces. It gives a polyhedron only when finitely many lattice points matter, that is, when is bounded. For unbounded , the recession directions must be shown to be lineality directions and to be spanned by lattice vectors. Both steps rest on simultaneous Diophantine approximation (Dirichlet's theorem) applied in irrational directions, and on a density argument for the projected lattice when the lineality space is not a -subspace. In the subspace setting of Theorem 9, one must also track the interiors relative to and to separately. Identity (6) holds only when meets , and the half-space case (iii) is exactly the case where it does not.
is EuclideanSpace ℝ (Fin n), linear spaces are Submodule ℝ, and is an AddSubgroup. All declarations live in the namespace MaxLatticeFree.Geometry. Every interior is relative (intW, relint). With the ambient topological interior, every subset of a proper subspace would be trivially lattice-free, and the classification would collapse. A lattice must have a linearly independent generating family; a dense finitely generated subgroup such as is excluded. Dimensions are integers with , and facets are nonempty, so no dimension equation holds through truncated subtraction.
Two readings of the page are fixed.
The paper's Theorem 1 (the same result for and affine ) is not included, and neither are the cited results of Barvinok and Dirichlet (Theorems 11, 14, Corollary 12). They are welcome as supporting lemmas. Infrastructure that is useful beyond this mission includes Dirichlet's simultaneous approximation theorem in , discreteness of lattices of subspaces, and the relation between intW/relint and Mathlib's intrinsicInterior.
Mission VI showed that two structural families of queueing networks — feedforward routing, and any network under HLSPS control — are stable throughout their entire subcritical region: no extra condition beyond the standard load condition is ever needed. Until the early 1990s it was widely conjectured that this held for every queueing network. Rybko and Stolyar's 1992 example disproved it: a specific, entirely reasonable two-station network, still subcritical, whose buffer contents grow without bound under a particular non-idling policy. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) devotes the third part of Chapter 8 to mapping the boundary this discovery opened up: which network structures still enjoy subcriticality-implies-stability (unidirectional rings), and, for a network that does not, exactly what extra condition restores it (the two-station, five-class re-entrant line, the book's own worked instance of the Rybko–Stolyar phenomenon).
A queueing network is globally stable (Definition 8.22) if it is Markov-chain stable under every simply structured, non-idling control policy — the strongest policy-independent notion of stability a network can have. At the fluid-model level (Definition 8.23, restricting to single-server stations, ), this becomes: every solution of the fluid equations (8.20)-(8.23) plus the non-idling condition (8.42) is driven to the origin, uniformly in its starting size. A unidirectional ring network routes each customer type through a fixed cyclic sequence of stations; a two-station, five-class re-entrant line (Figure 8.3) routes its single input stream through five classes in a fixed order, alternating between two stations.
The two-station, five-class re-entrant network's fluid model is globally stable if and only if
The first two conditions together are the standard load condition; the third is a genuinely new "virtual station condition," the direct analogue of the Rybko–Stolyar network's own extra requirement. This is the weakest possible target for the phenomenon it captures: a two-sided iff, so it cannot be strengthened by dropping either the necessity or the sufficiency direction, and it isolates the exact extra condition rather than a merely sufficient one.
Lemma 8.20 (restated from mission VI, since this chunk's page range overlaps mission VI's at page 164) is a general departure-rate extinction criterion. Theorem 8.21 proves stability of an "assembly with complementary side business" network via a first two-dimensional piecewise-linear Lyapunov function. Theorem 8.24 shows unidirectional ring networks are globally stable throughout their entire subcritical region — no extra condition needed, in sharp contrast to the goal theorem's network. Lemma 8.26 gives four algebraic sufficient conditions for the workload derivative inequalities the goal theorem's Lyapunov argument needs; Lemma 8.27 shows these conditions are simultaneously satisfiable exactly when (8.47)-(8.49) hold — the geometric core of the sufficiency direction.
The result itself. Theorem 8.25 is the book's own fully worked instance of the field's most cited stability-boundary phenomenon: it pins down, for a specific and analyzable network, exactly how much more than subcriticality is required, and shows the extra requirement (8.49) is not an artifact of the proof technique but a genuine necessary condition, via an explicit unstable sample path under the "extreme" priority policy that violates it. Theorem 8.24, by contrast, demonstrates that the ring topology is not automatically pathological in this way, delineating the boundary from the other side.
Formalizing it. Searches for "re-entrant line," "Rybko-Stolyar," and "virtual station"
(q=re-entrant%20line, q=Rybko-Stolyar, q=virtual%20station) return no results specific to
this material; this mission is a from-scratch formalization of global stability at both the
Markov-chain and fluid-model tiers, unidirectional ring networks, the two-station five-class
re-entrant line, and the assembly-with-side-business network.
Theorem 8.25's necessity direction needs an entirely different proof technique from its sufficiency direction: rather than a Lyapunov argument, it requires exhibiting an explicit unstable fluid model solution under a specific "extreme" static-buffer-priority policy — a sample-path construction, echoing the divergent-cycle construction mission III's own chapter (Section 6.2) gives for the original Rybko–Stolyar network, that the book itself says is "omitted" as analogous. A formalization that stated only the sufficiency direction (dropping the "only if") would misrepresent the theorem entirely, since sufficiency alone is not what makes this result the field's canonical boundary-of-stability statement. A second difficulty is genuinely geometric: Lemma 8.27's proof intersects a parallelogram of admissible pairs with a wedge region, then separately solves an analogous system for — reducing a five-dimensional existence claim to two two-dimensional geometric arguments, each depending on (8.47)-(8.49) in a way that is not visible from the inequalities' surface form alone.
Missions IV/VI's queueing-network model data, fluid-equation specialization, and workload
operator are restated locally (drafts in this series do not import one another), as is mission
VI's non-idling fluid model (renamed to track Definition 8.23's own name, FluidModelGloballyStable,
even though defeq in shape). Definition 8.22 (network-level global stability) is stated abstractly
over an uninterpreted policy type and two predicates, since the concrete "simply structured
non-idling policy" and "positive recurrence under a policy" notions belong to mission I's
apparatus, not a dependency of this chunk. The unidirectional ring network is characterized as a
structural property of an ordinary flat-indexed queueing network (a partial successor function
encoding the deterministic route) rather than by re-introducing the book's own two-index
type/stage bookkeeping — a faithful re-encoding, since every ring network in the book's sense is
representable this way. The re-entrant line's routing (station 1 serves classes 1,3,5; station 2
serves classes 2,4) was recovered from the explicit computations in Lemma 8.26's own proof, not
read off Figure 8.3 directly, though the two are cross-checked as consistent. The
assembly-with-side-business network, which needs a genuinely multi-input activity outside Chapter
2's "unitary network" vocabulary, is packaged directly via its already-derived fluid equations
(8.36)-(8.39) rather than a general SPN activity structure. Theorem 8.25 is stated as a bare
↔, exposing neither the sufficiency direction's Lyapunov witnesses nor the necessity direction's
instability construction — a formalization that dropped either direction of the iff, or that
conflated the unidirectional ring's cyclic structure with an unrestricted deterministic routing
graph, would each be an unfaithful weakening. IsGloballyStable, FluidModelGloballyStable,
IsUnidirectionalRing, and the re-entrant line's Lyapunov ingredients (reentrantG1/reentrantG2/
reentrantH1/reentrantH2) are the primary reusable contributions; contributions completing the
six by sorry proofs — Theorem 8.25's necessity direction in particular, which needs machinery
this mission does not otherwise build — are welcome.
Mission V supplied the general Lyapunov machinery — the extinction criteria of Lemmas 8.5, 8.6 and 8.11 — but a Lyapunov function does not construct itself. For a specific network structure and control policy, one must exhibit a concrete function and verify the drift condition. J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) devotes the second half of Chapter 8 to two such constructions, chosen to illustrate the two basic templates every later stability chapter follows: a piecewise-linear Lyapunov function tailored to a structural network property (feedforward routing), and a linear one that works for an unrestricted network but is tailored to a specific control policy (head-of-line proportional service, HLSPS). Together they cover, as a corollary, the generalized Jackson network — the classical multiclass queueing network with one server per class — under ordinary non-idling FCFS.
A queueing network (Section 2.6, restated from mission IV) is feedforward (Definition 8.13) if its stations admit a numbering under which no station routes work to a lower-numbered one (feedback to the same station is still allowed). The workload operator (Eq. 8.24) gives, for any buffer-contents vector , the total service effort each pool would need to drain to emptiness with no further arrivals; the load vector of the standard load condition is (Eq. 8.25), and the total arrival rate vector (including internally routed traffic) is the unique solution of the traffic equations . A queueing network under HLSPS control (Definition 8.17) splits each pool's capacity among its classes in fixed proportions (Eq. 8.30) — a policy general enough to reduce, for a generalized Jackson network (one class per pool), to ordinary non-idling FCFS.
For any queueing network under HLSPS control with proportion vector , if
the corresponding fluid model is stable, and hence (Theorem 6.2) the network itself is stable under HLSPS control. This is the weaker of the two possible capstones only in the sense that it fixes one specific policy; it is chosen over Theorem 8.14 as the goal because it needs the full generality of the workload-based linear Lyapunov argument (Lemma 8.20) with no structural restriction on the network's routing, whereas Theorem 8.14 trades policy generality for a feedforward restriction.
Lemma 8.15 isolates the workload derivative identity at a busy
station under any non-idling policy — the calculational engine both Theorem 8.14 and (via Lemma
8.20's analogous linear-potential argument) Theorem 8.18 rely on. Theorem 8.14 shows a
feedforward network is stable under any non-idling policy, via a piecewise-linear Lyapunov
function built from the routing matrix's block-triangular structure. Lemma 8.20 (numbered in the
book but omitted from this mission's planning brief — added here, see STATUS.md) is the direct
structural engine behind the goal theorem: a uniform excess departure rate over the total arrival
rate at every non-empty class forces extinction. Corollary 8.19 specializes Theorem 8.18 to
generalized Jackson networks, where HLSPS provably reduces to non-idling FCFS.
The result itself. Theorem 8.18 is the book's demonstration that dropping a structural network restriction (feedforward) is possible at the cost of committing to one specific, practically implementable control policy — and Corollary 8.19 shows this specific policy's stability theorem recovers, as a special case, the folklore stability result for the classical multiclass Jackson network under FCFS, arguably the single most studied queueing model in the field. Theorem 8.14, in turn, is the sharpest possible policy-agnostic statement: for feedforward networks, subcriticality alone (with no assumption at all beyond non-idling) suffices.
Formalizing it. Searches for "Jackson network" and "workload" (q=Jackson%20network,
q=workload) return no relevant results (per triage.json); this mission is a from-scratch
formalization of feedforward networks, the workload operator, HLSPS control, and their stability
theorems, building directly on mission III's Theorem 6.2 and mission V's Lyapunov criteria.
Theorem 8.14's proof needs a genuinely delicate construction: a sequence of positive weights , chosen via the routing matrix's block-triangular structure (guaranteed by feedforwardness) so that the piecewise-linear function is positive-definite and has the right drift everywhere — an inductive argument over stations that does not generalize to non-feedforward networks, which is exactly why Theorem 8.18 needs an entirely different (linear, policy-specific) argument rather than a direct strengthening of 8.14's. A second, more subtle difficulty is that Theorem 8.14 and Theorem 8.18 are not related as special case and generalization in the book's own proof structure, despite their overlapping conclusions on feedforward networks under FCFS-like policies: 8.14 is agnostic to policy but needs feedforward structure, while 8.18 is agnostic to structure but needs the specific HLSPS policy — formalizing one as a corollary of the other would misrepresent the book's actual logical dependencies.
Mission IV's queueing-network model data and fluid-equation specialization are restated locally
(drafts in this series do not import one another). The workload operator's matrix inverse
is supplied as external data with its defining two-sided-inverse property, rather
than derived from substochasticity/transience hypotheses on (Chapter 2 material, out of
series scope) — the same convention mission III used for its process-family apparatus. The
non-idling and HLSPS fluid models are each packaged as their own predicate plus a
Definition-6.3-style stability specialization, and Corollary 8.19 deliberately reuses the
non-idling stability object (not a separately restated "FCFS fluid model") since the book's own
remark identifies the two exactly for generalized Jackson networks. A formalization that stated
Theorem 8.14 as a corollary of Theorem 8.18, or vice versa, would misrepresent the chapter's
actual proof architecture (see Difficulty); this mission keeps them as independent milestones/
goal, per BRIEF.md's own instruction. Lemma 8.20, numbered and within this chunk's page range
but absent from the planning brief's disposition table, is added as a milestone rather than
silently dropped, since it is the structural step the goal theorem's own proof cites by name.
QueueingNetworkData, workloadOperator, IsFeedforward, and the non-idling/HLSPS fluid-model
predicates are the primary reusable contributions; contributions completing the five by sorry
proofs are welcome.
Mission III's Theorem 6.2 — "fluid limit stability implies SPN stability" — converts a probabilistic stability question into a real-analysis question, but it only supplies the generic fluid equations (6.1)-(6.6), which hold under any control policy and therefore say nothing policy-specific: (6.1)-(6.6) alone never force a fluid path to reach zero. To actually prove a concrete queueing network stable, one must first identify the extra fluid equation a specific policy forces on every fluid limit path, and prove that this extra equation genuinely holds — a task the book calls "justifying" the equation "through the same fluid limit procedure used in the proof of Theorem 6.5." J. G. Dai and J. Michael Harrison's Processing Networks: Fluid Models and Stability (Cambridge University Press, forthcoming; cited here from the authors' pre-publication draft, 2020-4-2, http://spnbook.org) carries out this derivation for four control-policy families in Chapter 7, laying the groundwork every later stability chapter of the book (feedforward networks, the Rybko–Stolyar boundary, back-pressure, proportional fairness, task allocation) builds on.
The first-come-first-served (FCFS) analysis traces to Rybko and Stolyar's 1992 fluid-scaling argument and was first stated in closed form as Eq. (2.6) of M. Bramson's 1996 paper on FCFS queueing networks; Bramson also showed by example (1994) that FCFS networks can be unstable even under the standard load condition, motivating the need for a precise fluid-equation characterization rather than an informal one.
A queueing network (Section 2.6) is an SPN with one activity per buffer: buffer/class is served by a unique pool , and on completion a class- job becomes class with probability (the routing matrix). denotes the set of classes served by pool . The fluid equations (6.1)-(6.6) specialize accordingly: consumption is the identity () and the output matrix is .
Three control-policy families are studied. A policy is non-idling if no server sits idle while a job waits in one of its buffers. A static buffer priority (SBP) policy is non-idling and additionally orders same-pool classes by a fixed priority permutation , always serving the highest-priority non-empty class first; it is non-preemptive if a job's service, once begun, is never interrupted by a later higher-priority arrival. Under FCFS, jobs at a pool are served strictly in arrival order — the workload-based analysis of Section 7.3. Section 7.4 studies a fourth, more general family: a unitary network (one service type per class) under a relaxed control policy , where is the updated job-count vector and is any capacity-respecting, degree-zero-homogeneous function (Assumption 7.6) — a family general enough to include non-idling and SBP policies as special cases, and to anticipate the proportionally fair allocation studied in Chapters 9-10.
For a queueing network under FCFS control, every fluid limit path satisfies (6.1)-(6.6) and
where is the fluid arrival rate into class and is pool 's fluid-scaled immediate workload. This is the weakest natural target: an identity that pins down exactly the time-shift FCFS imposes, without asserting anything about how quickly or whether the fluid model reaches zero (that is left to the Lyapunov arguments of later chapters, once this equation is in hand).
Theorem 7.2 (non-idling): forces pool 's aggregate service rate to run at full capacity . Theorem 7.3 (non-preemptive SBP): the same conclusion with sharpened to the priority set (Eq. 7.5), for every buffer . Theorem 7.8 (general relaxed control): under Assumption 7.6, forces 's derivative to equal exactly — the common generalization from which the non-idling and SBP fluid equations both follow as special cases of a suitable .
The result itself. Theorem 7.5 is the precise bridge that lets FCFS-specific stability questions be attacked by the Lyapunov-function method Theorem 6.2 licenses: without a closed-form fluid equation, "does an FCFS network satisfy the standard load condition stably?" has no tractable deterministic reformulation. Bramson's 1994 example (an FCFS network unstable despite satisfying the standard load condition) shows the equation's content is not vacuous — FCFS fluid limits genuinely can misbehave, and this equation is precisely what any subsequent stability or instability argument for FCFS networks must reason about.
Formalizing it. No result about FCFS, non-idling, static-buffer-priority, or general relaxed
control policies exists on Prove2Me (q=first-come-first-served, q=FCFS, q=priority policy
all return zero hits, consistent with triage.json's record that none of this book's Chapters
6-14 machinery is on the platform). This mission is a from-scratch formalization of queueing
networks, their three named control-policy families, and the four policy-specific fluid
equations Chapter 7 derives for them.
The obvious shortcut for Theorem 7.3 — reuse Theorem 7.2's hypothesis and conclusion verbatim with replaced by — conflates the preemptive and non-preemptive SBP policies: Remark 7.4 explicitly notes the underlying pathwise identity (7.4) (used directly by Theorem 7.2) holds unconditionally under preemption but only asymptotically, via a vanishing-remainder argument bounding the leftover processing time of interrupted-but-continuing jobs, under non-preemption — the theorem actually being formalized is about the harder, non-preemptive case. For Theorem 7.5, the central difficulty is that FCFS's defining property is a genuinely time-shifted identity (departures at match arrivals at ), not a same-instant conditional statement like the non-idling and SBP equations — an approach that tried to state FCFS as a same-instant condition on or alone, without introducing the auxiliary workload process , could not express the theorem's actual content. A further subtlety Theorem 7.8's proof flags directly (Remark 7.9) is that the tempting converse — " implies zero service rate" — is false in general (a corrected version appears only later, as Lemma 8.9); this mission's goal and milestone statements are careful to assert only the one-directional implication the book actually proves.
Mission III's fluid-limit-path apparatus (Definition 6.6, u.o.c. convergence) is restated locally
in this chapter's own namespace rather than imported, since drafts in this series do not import
one another; the restatement is trimmed to the four raw processes this
chapter's proofs need, omitting mission III's "delayed random walk" machinery. The non-idling and
non-preemptive-SBP hypotheses are both formalized via one shared predicate, FullyUtilized,
applied to different index sets ( vs. ) — the pathwise full-utilization identity
(7.4) that each policy's proof establishes for its own priority classes, taken as a hypothesis
rather than re-derived from a lower-level model of server scheduling (Chapter 2's construction of
the service-starting mechanism is out of scope for this chapter, exactly as it was for mission
III's SPNProcessFamily). Likewise, the FCFS goal theorem hypothesizes the raw identity (7.12)
(rewritten via the material-balance equation to avoid needing the raw arrival process) and the
fluid-scaled limit of the raw workload process (7.17), rather than re-deriving either from the
"delayed random walk" of Eq. (6.47). A formalization that dropped the workload shift
from Theorem 7.5's conclusion, or that stated Theorem 7.8's converse implication
(which Remark 7.9 explicitly disclaims), would each be an unfaithful trivialization or
overstatement ruled out here. QueueingNetworkData, ProcessFamily, FullyUtilized, and
SatisfiesAssumption76 are the primary reusable contributions of this mission; contributions
completing the four by sorry proofs — each of which needs the u.o.c.-convergence and
dominated-convergence arguments mission III's own proofs still lack — are welcome.
Walras (1874) described an economy as a system of simultaneous equations, one per market, and argued that a set of prices clearing all markets exists because the number of equations equals the number of unknowns. Counting equations proves nothing, and the question of whether competitive equilibrium exists at all remained open for eighty years. Wald (1935–36) proved existence in special production models under restrictive assumptions on demand. In 1954 Kenneth Arrow and Gérard Debreu gave the first existence proof for a general model with production, many consumers, convex technologies and preferences given by utility indicators (Econometrica 22 (1954) 265–290); McKenzie published an independent proof for a trade model in the same year (Econometrica 22 (1954) 147–161). The resulting Arrow–Debreu model is the reference model of general equilibrium theory and the starting point of market-equilibrium problems in operations research and algorithmic game theory.
The paper proves two existence theorems. This mission is the first, Theorem I, whose key assumption is that every consumer initially holds a positive amount of every commodity. A second mission treats Theorem II, which replaces that assumption by a weaker condition on labour supply.
There are commodities; a commodity vector is an element of , compared componentwise ( means for all ; means for all ). The inner product is .
Assumptions I–IV are: (I.a) each is closed, convex and contains ; (I.b) with ; (I.c) ; (II) each is closed, convex and bounded from below; (III.a) is continuous on ; (III.b) no is a satiation point; (III.c) if and then ; (IV.a) some satisfies ; (IV.b) and .
A competitive equilibrium is a tuple such that
An abstract economy (§2) is a game in which each player's feasible set depends on the other players' actions ; an equilibrium point is a profile at which every player maximizes its pay-off over its feasible set. The proof builds an abstract economy with the consumers, the producers and a fictitious market participant who chooses and receives , and a truncated version in which all choices are restricted to a large cube .
The statement fixes no constants; its only added hypothesis is .
In the order of the paper's argument:
Theorem I shows that the competitive model is consistent: under convexity, continuity, non-satiation and survival assumptions, prices exist at which profit maximization, utility maximization and market clearing hold simultaneously. The welfare theorems, comparative statics, and algorithms that compute equilibria (Scarf's method, market-equilibrium algorithms) presuppose it. Lemma 2.5, Debreu's social-equilibrium theorem (PNAS 38 (1952) 886–893), is also used on its own for generalized Nash equilibrium problems with coupled constraints.
The theorem is proved and textbook material (Debreu, Theory of Value, 1959). To the best of the catalog search, no proof assistant library contains Theorem I, Lemma 2.5, or a Kakutani-type fixed-point theorem for correspondences; on this platform the only related results are Brouwer's fixed-point theorem (AGT.brouwer_fixed_point, proved) and Nash's theorem for finite games (AGT.nash_existence), a special case of Lemma 2.5 with constant constraint sets. The mission produces a machine-checked proof of the paper's argument and, along the way, reusable statements about abstract economies and their equilibria.
The central difficulty is Lemma 2.5. The paper does not prove it but cites Debreu (1952), whose proof uses the Eilenberg–Montgomery fixed-point theorem for correspondences with contractible values. Brouwer's theorem alone does not suffice: the best-response correspondence of an abstract economy is set-valued, and its closed graph must be established from the continuity of the feasible-set correspondences, which is a maximum-theorem argument that Mathlib does not contain. A Kakutani-type fixed-point theorem, or an approximation argument reducing to Brouwer, is needed.
A second difficulty is non-compactness. The economy has unbounded action sets, so the Lemma does not apply to it directly. The boundedness of the attainable sets (§3.3.1) is an asymptotic argument using the irreversibility and no-free-production assumptions I.b and I.c, and the passage from back to (§3.4.1) needs the attainable choices to lie in the interior of the cube, so that local optimality implies global optimality through III.c. A fixed-point argument on an excess-demand function does not apply directly: demand need not be single-valued or even defined at every price.
Commodity space is Fin l → ℝ with its componentwise order; the paper's strict vector inequality is written coordinatewise (∀ h, x h < ζ i h), not with the order-theoretic strict inequality on functions. Consumers are Fin m, producers Fin n, and the players of are Fin m ⊕ Fin n ⊕ Unit. Utilities are total functions, and every assumption on them quantifies over only. "Maximizes" is always written as membership plus an inequality against every feasible alternative, never through a supremum. Continuity of a constraint correspondence is the paper's sequential definition (§2.4), a lower-hemicontinuity condition, required at every point of the other players' action space; convergence is asked only in the other players' coordinates.
Two hypotheses are made explicit because the formal statements would otherwise be false: Theorem I and §3.4.0 assume (for the price simplex is empty), and Lemma 2.5 assumes every action set nonempty (otherwise, with two or more players and all action sets empty, every hypothesis holds vacuously). The Remark of §3.3.5 carries, as a hypothesis, the nonemptiness of established in §3.3.4. A formalization that makes Theorem I trivial, for instance by taking to contain , by reading IV.a with the order-theoretic strict inequality, or by allowing an empty commodity space, is ruled out by these definitions.
A complete development needs: Kakutani's fixed-point theorem (or a Brouwer-based substitute) for compact convex subsets of ; Berge's maximum theorem for the best-response correspondence; the asymptotic-cone argument for §3.3.1; and elementary convex analysis for the budget sets. The abstract-economy definitions and Lemma 2.5 are reusable beyond this mission, including by the Theorem II mission. Contributions of any of these components are welcome, as are alternative proofs of Lemma 2.5.