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.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Primal–dual interior point methods follow a path of strictly feasible solutions to a linear program. Their worst case iteration bounds come from controlling a term that is quadratic in each search step. Mizuno, Todd, and Ye asked whether that term is typically much smaller than its worst case bound under a model in which a certain subspace is randomly oriented. Theorem 5 in their technical report gives a probability bound for the negative part of that term. It is a statement about one randomly oriented subspace and a fixed input vector, rather than a stochastic model for an entire algorithm run. The authors explicitly note that assigning the same random subspace model independently at successive iterations would be inconsistent with the algorithm's evolving state. Mizuno, Todd, and Ye, §6
Fix a dimension , an integer with , and a vector . Draw a random -dimensional subspace from the distribution invariant under orthogonal transformations. Let be the Euclidean orthogonal projection of onto , and put , its projection onto . The matrix turns the vector into the coordinatewise product .
For a coordinate vector , let and . Thus records the magnitude of the largest negative coordinate of . An unsubscripted vector norm is always the Euclidean norm. These definitions follow the report's notation on printed pages 2 and 4. Mizuno, Todd, and Ye, §§1–2
The formal model samples an matrix with independent standard normal entries and sets . The report itself gives this construction as an example of the orthogonally invariant law. With probability one, this null space has dimension . The construction covers the endpoint cases and as well: the projection product is then zero. This probabilistic model has no linear programming data in its statement. The optimization setting explains why the quantity matters, while the result depends only on Euclidean projection geometry. Mizuno, Todd, and Ye, §6
For arbitrary choices and at each dimension, the central target is
The logarithm is natural. The theorem asks for the exact coefficient shown in the report, rather than only an asymptotic order. The choice of and may change with ; the result does not require a common probability space for all dimensions. Mizuno, Todd, and Ye, Theorem 5, printed p. 13
The mission includes Lemma 6, which identifies a beta distributed radial coordinate and a uniform spherical direction for a projected vector; the componentwise identities and inequality (18)–(19); the Gaussian norm limit (20); the Gaussian coordinate maximum limit cited in the proof; and Lemma 7, which bounds the sup norm of a rotated uniform spherical direction by with probability tending to one. Their statements, constants, and order follow printed pages 14–15 of the report. Mizuno, Todd, and Ye, §6
The result gives a precise high probability bound for the negative coordinates of the projection product. In the report this product represents the second order term of a primal–dual search direction, and a smaller value permits a larger admissible step in the relevant neighborhood analysis. The theorem therefore supplies a mathematically definite part of the paper's discussion of anticipated improved behavior. It does not by itself prove a typical iteration count: the paper does not provide a consistent random model for the sequence of subspaces visited by the algorithm. Mizuno, Todd, and Ye, §§2, 6–7
The report proves Theorem 5 and the two numbered lemmas on paper. The formalization work is to provide machine checked proofs of the random subspace representation, the beta and spherical laws, the finite dimensional Gaussian limits, and their connection to the projection bound. These results are reusable in other questions about random projections and coordinatewise estimates. The statements in this mission are open formalization targets; compilation of a statement with a proof placeholder does not count as a machine checked proof.
A direct norm bound on and loses the coordinate information needed for the factor . The difficult part is that the desired bound concerns the most negative coordinate of a product of two dependent projections, while the distribution is specified through a random subspace. The paper's deterministic identity (18)–(19) relates this product to an angular coordinate. The remaining probabilistic statements must control the largest coordinate of a uniformly distributed spherical vector, including the numerical constant in Lemma 7. The laws of the radial and angular coordinates also need a sound measurable construction; simply writing a mapped measure without checking the map would not establish the claimed distributions.
Vectors are EuclideanSpace ℝ (Fin n), so is the norm. Coordinate sup norms are separate definitions. A complete development needs finite dimensional inner product geometry, orthogonal projections, Gaussian product measures, beta measures, the uniform spherical law, and limits of real probabilities. The spherical law is encoded as the direction of a standard Gaussian vector. The Gaussian matrix construction fixes the invariant subspace distribution and must be connected to the stated -dimensional law almost surely.
Lemma 6 concerns and , where the beta parameters and the spherical direction are nondegenerate. Its angular direction is assigned zero at the zero coordinate, which has probability zero in this regime; the claimed decomposition and unit norm hold almost surely. Theorem 5 retains , , and . Lemma 7 is stated only for frames in dimensions at least two; finitely many smaller dimensions are assigned probability one in its limit expression. Equation (20) keeps the report's condition . All limits are probabilities tending to one, never probability one at every finite .
Contributions should preserve the source's constants and all three claims of Lemma 6. A proof of the beta law alone, or a bound for a single fixed direction, does not close the corresponding target. The invariant random subspace and projection model, the Gaussian and spherical distribution facts, and the coordinate estimates are each useful independently of this mission.
A production process deteriorates over time, and the state it is in cannot be observed directly. Each period the operator chooses among three actions: produce without looking, produce and inspect the item (which reveals the current state at a cost), or revise the process back to its good state. This is one of the earliest partially observed Markov decision problems with a costly observation action, and it is the prototype of the inspection and machine-replacement models that followed in operations research and maintenance theory. Ross (Management Science 17(9), 1971) set it up for a countable state space, reduced it to a fully observed problem on beliefs, and determined the structure of an optimal policy for two states.
Intuition suggests a three-region policy for two states: produce while the probability of the bad state is small, inspect at intermediate probabilities, revise when it is large. Ross showed that the true structure has up to four regions: produce, inspect, produce again, revise. This mission formalizes that structure theorem and the general results it rests on.
The underlying process has a countable set of states , with transition probabilities from state at the end of a period to state at the beginning of the next. In state , producing without inspection costs , producing with inspection costs , and revising costs ; costs are bounded, and future costs are discounted by . A revision puts the process in state .
The decision maker tracks a belief , a probability vector on the states, ranging over
Producing without inspection moves the belief to , with . Inspecting reveals the state; if it is , the next belief is the row . Revising leads to .
The -discounted optimal cost is the limit of value iteration: and
The three terms with replaced by form the right side of the optimality equation (1). The -optimal produce, inspect and revise regions are the sets of beliefs at which the corresponding term equals , and a stationary rule is -optimal when it always selects an action attaining the minimum.
In the two-state process of §3, state is good and state is bad: , , , , , , with . The belief is a number , the probability of the bad state, , and the optimality equation becomes
There are thresholds with such that the rule
is -optimal, and whenever revising is -optimal at some belief. Degenerate thresholds (empty intervals) are allowed, so the statement fixes only the order of the regions, not their number.
Theorem 3.3 reduces the search for an optimal policy in the two-state problem to the choice of three numbers, and it fixes the order of the regions: there is never a revise region below an inspect region, and inspection never occurs below the deterioration probability . Together with Theorems 3.4 and 3.7 of the same paper (separate missions in this series), it is the basis for computing optimal inspection policies by searching over thresholds. Theorem 2.2 holds for any countable state space and is the general form of the observation that, in partially observed problems with linear-in-belief action costs, the regions of the "information" and "reset" actions are convex while the region of the passive action need not be.
The results are proved in the paper. As far as a search of the Prove2Me library shows (October 2026), none of them is formalized. Related formal work treats other models: belief-state reductions of finite POMDPs, and abstract contraction models for discounted dynamic programming. The mission produces machine-checked versions of the general model's optimality equation, the concavity of its value function, the convexity of two of its regions, and the two-state structure theorem.
The paper's proofs are short and lean on facts quoted from the literature. Theorem 3.3's proof is two sentences long. Filling it in requires several facts that the paper leaves implicit. The revise region of the two-state model is a closed right-hand interval. The inspect region meets in an interval, through the affine embedding of into . The half-open endpoints of the rule select optimal actions. That last point needs continuity of inside , a consequence of concavity, and Lemma 3.2 at the left end. The naive reading of the printed theorem, with all three thresholds in , is false in general (see below), so the threshold bookkeeping cannot be skipped.
On the general side, the optimality equation (1) is quoted from Blackwell. Here it must be proved for value iteration on the belief simplex of a countable state space, where the inspect term is an infinite series of values at the rows . Its convergence and the contraction estimates use the boundedness of the costs.
The general model is a structure over a type ι with [Countable ι], a distinguished state i₀, a transition matrix Pm, costs C I R : ι → ℝ and β. A separate predicate Model.Valid requires nonnegative entries, rows with HasSum (Pm i) 1, bounded costs and 0 < β < 1. The simplex uses HasSum P 1, never tsum, so it consists of genuine probability vectors. is defined as limUnder atTop of value iteration from , which is the paper's own characterization in the proof of Lemma 2.1. It is not an arbitrary function assumed to satisfy (1). The paper's definition as an infimum over measurable policies is not formalized; the policy class would be a separate mission. Regions are subsets of .
The two-state model is the instance ι = Fin 2 with , , , , and its value at the scalar belief is the general at . The general Lemma 2.1 and Theorem 2.2 therefore apply to it without restatement. Standing hypotheses of §3 are , and . is implicit in the paper, where the good state costs and the bad state . "-optimal rule" means a rule selecting a minimizer of the right side of (3) at every , the criterion the paper quotes on p. 588. "Every -optimal policy produces" (Lemma 3.2) means that producing is the unique minimizer.
Threshold repair. The paper prints . This is false when revising is never optimal, for instance when : then always producing is optimal and revising at is strictly worse, so no rule revising on a nonempty is optimal. The goal keeps exactly when the -optimal revise region is nonempty and otherwise allows ; the rest of the printed chain, , is kept. Adding the hypothesis instead would drop a case the paper covers.
The statement admits no trivializing reading. The thresholds are quantified existentially, but the rule must be optimal at every belief in , is pinned down by its definition, and the paper's numbers (, , , , ) satisfy all hypotheses.
Infrastructure needed: tsum manipulations on the belief simplex (linearity of , summability of for bounded ), a sup-norm contraction argument for value iteration, and closure of concavity under minima and pointwise limits. The value-iteration and contraction lemmas are reusable for any discounted model with bounded costs. Contributions of intermediate lemmas, such as continuity of the two-state on or the bridge identities , are welcome.
A prophet inequality compares two observers of a sequence of nonnegative random variables . The prophet knows all values in advance and collects . The gambler sees the values one at a time and must decide, irrevocably, when to stop and collect the current value. For independent variables the gambler's optimal value is at least half of , and the factor is sharp. Prophet inequalities are a basic tool in the analysis of online mechanisms, posted-price auctions and online selection problems, where the gambler's rule is a pricing policy and the prophet is the offline optimum.
Optimal stopping rules are often difficult to compute and to implement. A threshold rule, which stops at the first value at least , is a posted price, and is the form used in applications. Samuel-Cahn (Ann. Probab. 12 (1984) 1213–1216) proved that a threshold rule alone attains the factor : with a median of , Theorem 1 of the paper gives or . Mission I of this series formalizes that theorem.
Timeline (as recounted on p. 1213 of the paper).
Fix and a probability law on . Let be independent with common law , and . For a constant the threshold rules are
The stopped value is or . The truncated expectations are and : they discard the forced stop at time below the threshold. The class is the set of all and with .
The lower half of the theorem uses an explicit family. For , , and , the variables take the values , , with probabilities , , . Two constants enter:
This is unrelated to the of the NOTE in §1 of the paper.
In Lean (SamuelCahnProphet.IID), a sample is x : Fin n → ℝ under iidLaw μ n, the product measure; tIdx x c and sIdx x c are and ; Emax, EstopT, EstopS, EplusT, EplusS are , , and the terms; supE and supEplus are the two suprema over ; threePoint n a b c is the law of ; aStarIID and Q are the constants above.
over i.i.d. nonnegative . It is stated as three facts: for every and law; ; and for every some and law with .
Theorem 1 says a posted price recovers half of the prophet's value. Theorem 2 says this guarantee is tight within the class of threshold rules even under the most favourable independence structure, identical distributions. This matters because for optimal rules the i.i.d. constant is at most (Hill and Kertz 1982); the theorem separates threshold rules from optimal rules in the i.i.d. case and sets the benchmark that later single-threshold and order-selection analyses compare against.
The result is proved in the paper; to our knowledge no machine-checked proof exists. This mission produces one: a formal model of threshold rules on an i.i.d. sample, exact asymptotics of the expected maximum and of two stopped values for a triangular array of three-point laws, the reduction of the class to two rules, and the two-parameter limit. The upper bound (milestone 1) is the i.i.d. case of mission I's goal, and may later be closed by reference to it.
The limits are "easily seen" on the page, but each requires controlling uniformly with the exact law of a stopped index on a product space, including the forced stop at whose contribution vanishes only in the limit. Milestone 3 is a finite claim over an uncountable family of rules: every and with must be shown to coincide almost surely with one of , , or stopping at , and the first and last must be shown dominated by for every finite , not only asymptotically. The final step is a joint limit in , in which while the correction term vanishes like ; an iterated limit is not the statement.
The i.i.d. variables are the coordinates of under the product measure ; all quantities depend only on the joint law, so the supremum over is a supremum over laws with . Indices are 0-based in Fin n with [NeZero n], the paper's index being ⊤. Expectations are lintegrals of ENNReal.ofReal in : no integrability is assumed and is allowed. The sup over ranges over and over both families and . Limits along the triangular array are indexed by and taken in after toReal; the early terms with , where the clipped weights of threePoint do not form a probability measure, do not affect any limit.
The page's ratios are not written literally: in the quotients and take junk values, so a literal supremum of ratios would be decided by degenerate laws. The goal's third fact uses a strict inequality and requires an explicit probability law on , which rules out the Dirac mass at and sub-probability witnesses.
A complete development needs: the law of the first index of a product sample entering a set, expectations of finite-valued functions under Measure.pi, the limit along a triangular array, and elementary bounds on the exponential. The first two are reusable for any threshold or secretary-type stopping problem on i.i.d. samples. Proofs of the milestones in any order are welcome, as is a proof of the upper bound that does not route through the median.
Robertson and Seymour introduced tangles as a way to describe a region of a graph that cannot be isolated by a separation of low order. A separation divides the edges into two sides, and its order counts the vertices shared by those sides. A tangle makes a consistent choice of the side regarded as small at every order below a threshold. This turns an informal idea of a highly connected region into an object with explicit axioms. In Graph Minors. X, the authors connect tangles with branch-width, tree-width and grid minors; the grid construction is the direct example behind that connection. The paper states the existence of a tangle of order in every -grid as (7.3) on p. 173. Robertson and Seymour, 1991.
The result is already proved in the paper. The present target is its Lean statement and proof, together with the two numbered results from §7 on which the construction rests. This mission concerns the grid itself. The paper's further assertion that a grid minor induces a tangle in a larger graph uses the separate minor-transfer result (6.1), whose edge identities require additional definitions. Robertson and Seymour, 1991, pp. 170–173.
Fix an integer . The -grid has vertices for . Two vertices are adjacent exactly when their coordinate differences have absolute values summing to one. For each , is the horizontal row with vertices ; for each , is the vertical column. Write and for their edge sets. The Lean development uses the already published definition of this same simple graph, with coordinates shifted to start at zero. The shift changes no adjacency or row and column relation. Robertson and Seymour, 1991, p. 171.
For an edge set , the edge boundary consists of vertices incident both with an edge in and with an edge outside . The source prints “vertices ” when introducing this set. Since is a set of edges, this is a type slip; the two incidence conditions give the intended reading. An edge set is small if and it contains no complete row edge set . These are two separate requirements. An edge set can have a small boundary while still containing a whole row. Robertson and Seymour, 1991, pp. 171–172.
A subhypergraph specifies subsets and of the grid's vertices and edges, retaining the incidences of the ambient grid. A separation satisfies and ; its order is . Although the grid is a simple graph, these are the paper's hypergraph definitions. A tangle of order contains only separations of order below and satisfies three axioms: it chooses an orientation of every such separation; the union of the first sides of any three chosen separations is not ; and no chosen first side contains every vertex of . The chosen three may coincide. Robertson and Seymour, 1991, pp. 153–154.
The first milestone, (7.1), identifies a symmetry between rows and columns under a low boundary:
The second milestone, (7.2), says that three small edge sets cannot cover all the grid's edges:
The goal, (7.3), defines rather than taking it as an arbitrary set. It selects precisely the separations of order less than for which is small, and asserts
These are the numbered §7 results on pp. 171–173, in the order used by the paper. Robertson and Seymour, 1991, pp. 171–173.
The theorem gives an explicit tangle in a familiar graph for every order . A tangle is more than a numerical connectivity bound: it records coherent choices across all separations below its order. In the paper, the grid tangle feeds the link between large grids and tangles of high order. The extension from a grid minor in another graph to a tangle of that graph invokes (6.1), beyond this mission's goal. The converse direction, that large tree-width forces a large grid minor, is (7.4), proved in Graph Minors V (Robertson and Seymour, 1986); the published definitions and statements of that paper on this platform are about grid minors and tree-width, not tangles. Robertson and Seymour, 1991, pp. 170, 173.
Formalizing (7.3) will make the grid tangle available as a checked object alongside the already published grid graph. It will also produce reusable definitions for an edge boundary, small edge sets and the paper's hypergraph separations. The Lean files here are draft statements with open proofs; the published 1986 grid definition is the existing checked ingredient. No machine-checked proof of (7.1), (7.2) or (7.3) is claimed by this proposal.
The obvious attempt at (7.2) counts boundary vertices column by column. If every column has all its edges in and meets both sets, each column contributes at least two vertices to , so the two boundaries together have at least vertices. This only works when the third set misses the first and last rows; in general the third set can absorb edges of every column, and no single count over the whole grid bounds all three boundaries at once. The statement is a covering property of three sets, not a bound on any one of them, and the paper's argument for it is credited to D. Kleitman and M. Saks. The goal must then meet all three tangle axioms. The page's proof of (7.3) argues the first axiom and says only that the rest follows from (7.2); the third axiom, , is part of the definition and must be established, not dropped. Robertson and Seymour, 1991, pp. 172–173.
The source assumes finite hypergraphs throughout, and §7 fixes . Lean uses a finite simple graph on Fin θ × Fin θ, reusing RobertsonSeymour1986.GM5.grid, and views its edge set as the edge type of a local hypergraph. Subhypergraphs hold vertex and edge subsets with inherited incidence. Set.ncard counts boundary vertices and separation order. Rows and columns use all grid edges whose two endpoints have the specified coordinate. This representation keeps every grid edge's identity, even though it is written as a SimpleGraph edge subtype.
IsSmall retains both and the exclusion of full row edge sets. boundary requires an incident edge on each side of . Both details are necessary for the claimed tangle: an IsSmall without the row clause would call every set with a small boundary small, including sets that contain whole rows, and the resulting set of separations is not a tangle; a boundary defined with "every edge outside " instead of "some edge outside " would be empty and make the size condition vacuous. The formalization keeps the third tangle axiom and does not replace it with an easier condition. The definitions of hypergraph, separation and tangle duplicate the shared encoding used by the other missions for this paper and can later be consolidated. The definitions also include the paper's tangle number and maximum edge size for that shared layer, though the grid goal does not invoke them; on finite inputs their maxima are bounded, and their empty-set value is zero.
The companion missions are Graph Minors. X. Obstructions to Tree-Decomposition I: Tangle Number Equals max(Branch-Width, Largest Edge Size), max(β(G), γ(G)) = θ(G); Graph Minors. X. Obstructions to Tree-Decomposition II: Branch-Width and Tree-Width Satisfy max(β, γ) ≤ ω + 1 ≤ max(⌊3β/2⌋, γ, 1); Graph Minors. X. Obstructions to Tree-Decomposition IV: Mutually Distinguishable Tangles Have a Tree-Decomposition Separating Them by Their Distinctions; and Graph Minors. X. Obstructions to Tree-Decomposition V: A θ-Pervasive Class of Designs Gives a Tree-Decomposition over 𝒮^{3θ−2} ∪ ℛ_{4θ−3}. Those missions address the paper's other main results; this one isolates the grid construction.
A two-stage stochastic program with recourse models a decision taken in two steps: a first-stage decision is fixed before a random outcome is observed, and a second-stage (recourse) decision is chosen after the outcome is known, both subject to constraints and both incurring costs. The model is the standard framework for planning under uncertainty in operations research: capacity planning, production and inventory, energy dispatch, finance.
For linear recourse problems, duality was developed in the 1960s and early 1970s by Wets and others, partly under integrability restrictions on the random data. R. T. Rockafellar and R. J.-B. Wets, Stochastic convex programming: basic duality (Pacific J. Math. 62 (1976), doi:10.2140/pjm.1976.62.173), treat the convex case, where every cost and constraint function is convex, by embedding the problem in a family of perturbed problems and applying the perturbational theory of convex duality (Rockafellar, Conjugate Duality and Optimization, SIAM 1974) together with the theory of convex integral functionals. The paper's dual variables are integrable price systems, interpreted as equilibrium prices for perturbations of the constraints; it is the starting point of a series of papers by the same authors on stochastic convex programming (relatively complete recourse, Kuhn–Tucker conditions, singular multipliers).
Let be a probability space. A vector is chosen subject to and (), at cost . Then is observed and is chosen subject to and (), at cost . The aim is to minimize the expected cost
The standing assumptions are: , convex, closed and nonempty; and convex and finite everywhere; measurable, summable for and bounded for .
Decisions live in and perturbations in . The perturbation functional is the expected cost if satisfies the constraints with right-hand sides and, almost surely, , and otherwise. The problem minimizes .
The space is paired with by , and with in the same way. The Lagrangian is , the dual maximizes over , and the perturbation function is . Conjugates , are taken with respect to the pairing of with .
If and are bounded, then
and in fact is a proper convex function on , lower semicontinuous for the weak topology , the infimum defining is attained for every , and . The goal is the theorem exactly as printed, all conclusions included.
The mission also poses the explicit form (1.8) of the Lagrangian and Corollary 1 (dual solutions are the negatives of subgradients of at ; saddle-point characterization of primal solutions when ).
Theorem 3 gives, for bounded constraint sets, the absence of a duality gap between a convex recourse problem with essentially bounded decisions and its Lagrangian dual over integrable multipliers, together with existence of an optimal decision. Through Corollary 1 it reduces the necessity of the Kuhn–Tucker (saddle-point) optimality conditions to the single question whether is nonempty, and through the paper's later results it describes the directional derivatives of the optimal value with respect to perturbations of the constraints.
The result has been proved since 1976; it has not been machine-checked. A formal development produces the problem model on and spaces, the weak topologies of the pairings, and conjugate duality for extended-real-valued functions on such paired spaces, none of which is currently available as a ready-made Lean statement on this platform.
The obvious argument fails at two points. First, is , and the biconjugate equals only for a lower semicontinuous proper convex function in a topology compatible with the pairing. Lower semicontinuity of in the norm topology of is not enough: the pairing is with , not with the norm dual of , so the relevant topology is the weak topology , and an infimum of lower semicontinuous functions is in general not lower semicontinuous. Second, the lower semicontinuity of itself, in the weak topology, is a statement about convex integral functionals on that rests on measurability of the integrands in jointly with continuity in the decision variables. Boundedness of , is what supplies the compactness that is otherwise missing.
Fin n → ℝ and the products , are dot products. Constraint indices are Fin m.Lp (Fin n → ℝ) ⊤ σ and Lp (Fin n → ℝ) 1 σ, spaces of almost-everywhere classes; all second-stage conditions are stated almost surely. is a probability measure (IsProbabilityMeasure).EReal; infima and suprema are lattice operations in EReal, so there are no junk values for empty or unbounded sets. Every sum has a real first summand, so no convention enters.A complete development needs the identification of with the dual of on a probability space (for weak-* compactness), lower semicontinuity of convex integral functionals, and conjugate duality on paired locally convex spaces. These are reusable well beyond this mission. Proofs of milestones, and of auxiliary lemmas of this kind as separate theorems, are welcome. The mission Stochastic Convex Programming: Basic Duality 2 formalizes the paper's other main result, on the first-stage problem and attainment of the recourse.
Tangles were introduced by Robertson and Seymour in Graph Minors. X (JCTB 1991) to make precise the idea of a "highly connected region" of a graph. A tangle orients every low-order separation of the graph towards one side, consistently. They are the organising notion of the later papers of the Graph Minors series, which culminate in the graph structure theorem and the proof of Wagner's conjecture.
Section 11 of Graph Minors X, Structure relative to a tangle, asks how local and global structure are related. In the paper's words: suppose that has large tangle number, but relative to each high-order tangle the graph has a structure of a certain kind . What can be inferred about the global structure of ? One might guess that has a tree-decomposition into pieces each with structure , but that is false. The theorem of §11 shows that does have a tree-decomposition into pieces which almost have structure . The authors state that they need this for an application in a later paper of the series, cited as [6], Graph minors. XVII. Excluding a non-planar graph (submitted); it appeared as Graph Minors XVI (2003), where the local structure relative to a tangle is a near-embedding in a surface.
A hypergraph has a finite vertex set , a finite edge set and an incidence relation. A subhypergraph has and , with every end of an edge of in . A separation of is a pair of subhypergraphs with and , and its order is .
For , a tangle of order in is a set of separations of order such that (i) for each separation of order one of , is in ; (ii) no three members of have ; (iii) for .
A tree-decomposition of is a tree and subhypergraphs , , whose union is , which are pairwise edge-disjoint, and with whenever lies on the path of between and .
A design is a pair of a hypergraph and a set of subsets of .
For and a class that is -pervasive in ,
If is -pervasive in and , then either some separation of order has
or some location in with design in has for all .
If , there is a tree-decomposition of over with a node such that and the -extension of the design of is in . The goal is the case .
For every , if has no tangle of order , then
Consequently , where is the tangle number. This is the p. 188 remark following (11.3).
(11.1) converts local information, stated tangle by tangle, into a global decomposition. Every piece of the decomposition is either small (at most vertices) or differs from a structure in by at most added vertices. This is the kind of local-to-global step the later Graph Minors papers need: there the local structure near each high-order tangle is a near-embedding in a surface, and a result of this shape glues such local structures along a tree. With it gives a tree-width bound , a weaker form of the tangle/tree-width duality.
The result has been proved since 1991. To our knowledge no proof assistant formalizes it, and none formalizes the hypergraph tangles or tree-decompositions of this paper. This mission produces machine-checked statements of the paper's notions of design, enlargement, location and pervasiveness, the structure theorem, and its inductive strengthening.
The first idea is to take the pieces in themselves as the pieces of the tree-decomposition. That fails, and the paper says so: the pieces can only almost have the structure. Locations for different tangles interact, and the decomposition must absorb up to extra vertices into each piece. The induction also has to control a set of attachment vertices of bounded size: a piece built at one node must still accept the vertices through which it is glued to the rest of the tree. Keeping throughout the recursion is the delicate point, and it is why the strengthened statement (11.3), not (11.1), is the one that admits induction.
Hypergraph V E with an incidence relation. Finiteness is [Finite V] [Finite E] on every theorem. Subhypergraphs, separations, tangles and tree-decompositions are the series' shared encodings (namespace RobertsonSeymour1991.GM10.Structure). The tree of a tree-decomposition is a SimpleGraph on Fin n satisfying IsTree.G.Sub × Set (Set V), and a class of designs is a set of -designs. Classes need not be closed under isomorphism; the paper never uses that.IsPervasive is satisfiable: the class of all designs is -pervasive, through the empty location. The conclusion is satisfiable too: the one-node decomposition lies over . So neither the hypothesis nor the conclusion of (11.1) is vacuous.The other main results of the paper are separate missions of this series:
Contributions are welcome on any item: proofs of (11.2) and (11.3), and of the p. 188 companion. The companion needs two auxiliary facts: a tangle of order in a subhypergraph yields one of order in , and tree-width is bounded by bag size.
The Graph Minors series of Robertson and Seymour proves that finite graphs are well-quasi-ordered under the minor relation. A central tool of the series is the duality between two ways of measuring how "tree-like" a graph is: decompositions along a tree, which certify that a graph is thin, and tangles, which certify that it contains a highly connected region that no small separation can split. Graph Minors X (Robertson and Seymour, 1991) introduces tangles and proves the exact minimax relation between the tangle number and branch-width, an invariant within a constant factor of tree-width. Tangles became a standard object of structural graph theory and were later abstracted to connectivity systems, matroids and data clustering; branch-width is the parameter behind dynamic-programming algorithms on graphs and matroids of bounded width.
A hypergraph consists of a finite vertex set , a finite edge set and an incidence relation; an edge may be incident with any number of vertices, its ends, and the size of an edge is its number of ends. Write for the maximum size of an edge ( if ).
A subhypergraph is given by a set of vertices and a set of edges containing all ends of its edges. A separation of is a pair of subhypergraphs with and no common edge; its order is .
For an integer , a tangle of order is a set of separations of order such that (i) for every separation of order , one of lies in ; (ii) for any three members of ; (iii) for every . The tangle number is the largest order of a tangle in , or if there is none.
A ternary tree is a tree whose vertices have valency or . A branch-decomposition of is a ternary tree with a bijection from its leaves onto . Deleting an edge of splits the leaves, hence , into two parts; the order of is the number of vertices of incident with edges on both sides. The width is the largest order of an edge of , and the branch-width is the minimum width over all branch-decompositions, with when .
The proof goes through an abstract setting. On a finite set , a connectivity function is a symmetric submodular map . A set is efficient if . A bias is a set of efficient sets containing one of for each efficient and no three members covering . Its dual object is a tree-labelling: a ternary tree whose incidences carry efficient sets, complementary across each edge, covering at each internal vertex, and absorbed by a given family at each leaf.
The exception is genuine: a hypergraph with a vertex and only edges without ends has and .
A companion statement, (4.4), computes and, for , .
The minimax theorem makes tangles the exact obstruction to small branch-width: either a branch-decomposition of width at most exists, or a tangle of order witnesses that none does. Every later use of tangles as certificates of high connectivity in the Graph Minors series, including the tree-decomposition of a graph into regions indexed by its maximal tangles and the grid theorem, rests on this duality. The abstract lemma (3.5) applies to any connectivity function, so it also gives the duality for matroid branch-width and for other symmetric submodular functions.
The results are proved in the published paper; none has a machine-checked proof that this mission is aware of. The platform has branch-width objects for set functions on subcubic trees, from the Oum–Seymour approximation of clique-width (ApproxCliqueWidth.Certificate.bw_ge_of_wellLinked, bw_le_of_no_wellLinked), which bound branch-width by well-linked sets, a different obstruction. This mission adds a hypergraph tangle library and the exact minimax.
The inequality and the direction "a tangle of order excludes width " are short. The converse, building a branch-decomposition of width when no tangle of order exists, is the hard direction. A natural first attempt is to merge small separations greedily into a tree, but the submodular uncrossing step can destroy the leaf conditions already established, and an induction on the edge set does not preserve the tangle hypothesis. A second difficulty is bookkeeping: the trees are ternary, so every construction that cuts, joins or contracts trees must restore valencies and , and the passage between leaf labels and edges of needs the labels at the leaves to partition .
The objects live in the namespace RobertsonSeymour1991.GM10.Minimax.
V, E; every theorem assumes [Finite V] [Finite E], as the paper assumes all hypergraphs finite.IsTangle G θ 𝒯 with built in, and the three members in the second axiom need not be distinct. The tangle number is a supremum in of a set bounded by , so it is a maximum.Fin n. A branch-decomposition stores as an injection of the edges onto the leaves.Set E, and is the complement. The incidence with is the adjacent pair , and every condition on labels is required on adjacent pairs only.Junk values would make the goal trivial: a tangle number of from an unbounded set of orders, or a branch-width of from an empty set of decompositions. Neither occurs: every tangle has order at most , and a branch-decomposition exists whenever . The goal also keeps the exact exception , neither dropped nor strengthened.
A complete development needs finite trees with leaf counting, path and component reasoning in SimpleGraph, and submodular uncrossing arguments. The tangle library of §2 and the abstract minimax of §3 can be reused beyond this mission. Contributions of tree lemmas (ternary trees on Fin n, grafting two trees at a leaf, contracting a valency-2 vertex) are welcome.
The other main results of the paper are separate missions of this series: Graph Minors. X. … II: Branch-Width and Tree-Width Satisfy max(β, γ) ≤ ω + 1 ≤ max(⌊3β/2⌋, γ, 1), III: In the θ-Grid, the Separations of Order < θ With Small E(A) Form a Tangle of Order θ, IV: Mutually Distinguishable Tangles Have a Tree-Decomposition Separating Them by Their Distinctions, and V: A θ-Pervasive Class of Designs Gives a Tree-Decomposition over 𝒮^{3θ−2} ∪ ℛ_{4θ−3}.
Many problems in optimization and equilibrium modelling, among them linear and nonlinear complementarity problems, variational inequalities over polyhedra, and the Karush–Kuhn–Tucker conditions of nonlinear programs, can be written as a single generalized equation
where is the normal-cone operator of a closed convex set . S. M. Robinson introduced strong regularity of such an inclusion at a solution in Strongly regular generalized equations (1980) and proved an implicit-function theorem for it: when the linearised inclusion has a locally unique, Lipschitz inverse, solutions of the perturbed problem exist, are locally unique and depend Lipschitz-continuously on the perturbation. Strong regularity has since become the standard stability notion behind sensitivity analysis and the local convergence of Newton-type methods for variational problems; see Dontchev and Rockafellar, Implicit Functions and Solution Mappings (Springer, 2nd ed. 2014, doi:10.1007/978-1-4939-1037-3).
Strong regularity depends only on the linearisation, so deciding it means deciding it for a linear generalized equation. For a general polyhedral set the paper's appendix does this by a reduction: locally around the problem is equivalent to a homogeneous problem on a cone, the reduced form, and strong regularity is equivalent to unique solvability of that reduced form. This mission formalizes that appendix and the criterion it yields.
Work in with the standard inner product, which identifies with its dual. For the normal cone at is
A set is polyhedral convex if it is the intersection of finitely many closed half-spaces. Fix a nonempty polyhedral convex , an real matrix and , and consider
It is strongly regular at a solution with constant if there are neighbourhoods of and of such that for each the perturbed inclusion
has exactly one solution in , and on .
The reduction uses the following objects, all built from the data:
The reduced form of (A.1) at is the inclusion for ; in an orthonormal basis adapted to , and it is with an matrix . It is vacuous when .
If solves (A.1), then (A.1) is strongly regular at if and only if
No Lipschitz constant is fixed: the left side is "strongly regular for some ".
Theorem A.4 turns a local stability property, defined through neighbourhoods and an inverse map, into a finite-dimensional algebraic question about one homogeneous problem on a polyhedral cone. Combined with the Schur-complement criterion of Theorem 3.1, it gives checkable conditions (Corollary 3.2): nonsingularity of a block and positive definiteness, or the P-matrix property, of its Schur complement. Through the KKT reformulation of §4 this is the route by which strong second-order sufficiency and linear independence of binding constraint gradients imply strong regularity in nonlinear programming. The example of p. 53 shows the criterion deciding cases where itself is neither positive definite nor a P-matrix.
The results are classical and proved in the paper; to our knowledge none of them has a machine-checked proof. The formalization adds a coordinate-free statement of the reduced form, which the paper writes only in an adapted basis; a Lean account of exposed faces and tangent cones of polyhedra, with their local conic structure (Propositions A.1–A.2), which the paper lists "without proof" and cites to Rockafellar; and checked versions of the corollary and the example.
The definition of strong regularity is local, while condition (ii) is global on . The obvious argument, "linearise and read off the inverse", does not apply, because is a set-valued map whose graph changes shape from point to point. The step that carries the weight is Proposition A.3: a perturbation of may move the solution off the face , and only polyhedrality, through the finitely many values of on and the local conic structure of A.1–A.2, rules this out uniformly in a neighbourhood. The direction from strong regularity to (ii) needs positive homogeneity of the reduced form to pass from uniqueness near to uniqueness on all of . The direction from (ii) to strong regularity needs the Lipschitz property of a single-valued inverse of a polyhedral multifunction (Robinson 1979, cited as [12, Proposition 2]), which is not elementary.
EuclideanSpace ℝ (Fin n), with inclusions written as memberships: (A.2) is . A matrix acts through Matrix.toEuclideanLin. The normal cone carries the clause , so off ; without it every inclusion would be satisfiable at points outside and the statements would change meaning.Submodule.starProjection.A constrained system can be written as a generalized equation: a smooth or linear expression must balance the normal cone of a feasible set. This form includes variational inequalities and the first-order conditions of many optimization problems. It is useful to know whether a small change in the right-hand side determines one nearby solution and how far that solution moves. In the linear finite-dimensional case, Robinson's Theorem 3.1 gives matrix conditions that guarantee something stronger: a unique solution for every right-hand side, with one Lipschitz bound valid over the entire space. The theorem also identifies an exact matrix criterion when the feasible set is a product with a nonnegative orthant.
The question is relevant whenever some coordinates of a system are free and others are constrained by inequalities. Eliminating the free coordinates produces a smaller matrix, the Schur complement. The resulting condition can be checked on the reduced block, and in the orthant case it becomes the familiar P-matrix criterion from linear complementarity. Robinson states both claims in a single theorem and relates them to the behavior of a generalized equation rather than to an isolated matrix property Robinson, pp. 51–52.
Let be positive integers and give its Euclidean norm. Write , with and . Let be nonempty, closed, and convex, and put . For , the normal cone is
For , is empty. Thus the inclusion itself enforces feasibility. This is Robinson's indicator-subdifferential convention Robinson, pp. 43 and 51.
Partition the real square matrix into blocks , , , and , where is . When is nonsingular, its Schur complement in is
A real matrix is positive definite in the theorem's sense when for every nonzero . Symmetry is not assumed. A P-matrix has strictly positive determinants for every nonempty principal submatrix. Write for the vectors with all components nonnegative. These conventions are stated or used in Theorem 3.1 and its proof.
For , the first target is the sufficient condition
Here “is Lipschitz” includes that exactly one inverse value exists at every . The assertion holds for every nonempty closed convex ; it is not restricted to polyhedral sets.
When , the second target is an equivalence:
The goal theorem is the conjunction of these two statements, matching Theorem 3.1. Its milestones record the paper's local upper Lipschitz assertion for polyhedral multifunctions, the block reduction, the reduced inverse result, the complementarity characterization, and the necessity of nonsingularity.
The first part gives a global sensitivity guarantee for a generalized equation with an arbitrary nonempty closed convex lower-block constraint. For any two right-hand sides, their unique solutions differ by at most a fixed multiple of the distance between those right-hand sides. The second part tells when this guarantee holds for the orthant model: the P-matrix condition is necessary as well as sufficient. These are the precise conclusions of Robinson's theorem; the mission concerns their machine-checked formalization, not an unresolved mathematical conjecture.
A complete development would provide reusable definitions of the normal-cone generalized equation, an explicitly nonsymmetric notion of positive definiteness, P-matrices, and the global inverse property. It would also formalize the linear complementarity characterization quoted in the paper. The current draft has Lean-checked statements with proof placeholders. No proof of Theorem 3.1 or of its milestones is claimed here.
Nonsingularity of the full matrix alone does not decide whether the constrained inverse exists uniquely: the normal cone can change as reaches different faces of . A pointwise uniqueness argument also does not by itself supply one Lipschitz constant on all of . For the orthant case, checking only the full determinant or leading principal minors would miss the criterion Robinson invokes; every nonempty principal minor matters. The difficulty is to connect a global statement about all right-hand sides with the reduced matrix condition while preserving the normal cone's behavior at boundary points Robinson, pp. 51–52.
Lean represents as a Euclidean space indexed by the disjoint union of and . This gives the paper's Euclidean norm rather than the sup norm of a product type. The normal cone is empty off its set, and the inverse property explicitly requires existence for every right-hand side, uniqueness, and one global real Lipschitz bound. The Schur complement appears only with a nonsingular in the substantive claims; matrix inversion on a singular input would otherwise be totalized by Lean. Positive definiteness does not add a symmetry hypothesis. The goal retains as printed; the paper's later remark about zero-dimensional blocks is outside this theorem.
The polyhedral milestones use finite intersections of closed half-spaces. The reduced-operator milestone uses a nonempty closed convex , matching the theorem's setting. The LCP milestone allows any finite dimension; at dimension zero, both its universal uniqueness statement and its empty-minor P-matrix condition hold. A weaker encoding in which the inverse is merely single-valued where it happens to exist would erase the global conclusion and is excluded here.
Solvers can contribute the block-normal-cone equivalence, the global inverse statement for the reduced operator, the polyhedral Lipschitz result, the P-matrix characterization, and the final theorem. The normal-cone and matrix definitions can also serve later generalized-equation missions that use the same conventions.
An isometric model of a graph assigns vectors to vertices so that vector distances reproduce shortest-path distances exactly. The choice of norm matters: a graph that needs many Euclidean coordinates may admit a smaller realization under a different norm. Linial, London, and Rabinovich used this freedom to study the dimension of graph metrics and related geometric questions in their 1995 paper on graph embeddings (Linial–London–Rabinovich, 1995). The complete graph is the first calibration point for the invariant. Every two distinct vertices are equally far apart, so the question becomes how many pairwise equidistant points an arbitrary real normed space of dimension can contain.
The answer is a sharp base-two logarithm. It separates the role of dimension from the particular shape of a norm's unit ball. In particular, a cube equipped with the supremum norm supplies many equidistant vertices, while no norm in the same dimension can accommodate more. Establishing both directions gives a reference case for more complicated graph metrics in the paper's Section 5.
A finite pseudometric space has a finite point set and a distance that is symmetric, vanishes on the diagonal, and satisfies the triangle inequality. Distinct points may have distance zero, as the paper explicitly allows. A norm on is nonnegative, vanishes only at the zero vector, is absolutely homogeneous, and satisfies the triangle inequality. It induces the distance between vectors.
An isometric embedding of into a -dimensional normed space is a map with for every pair. The isometric dimension is the least for which such a norm and map exist. The norm may depend on and ; it is part of the realization rather than a fixed background choice. Lemma 5.1 of the paper states that every -point metric space has an isometric realization in , so this least dimension is taken over a nonempty set (Linial–London–Rabinovich, p. 229).
The complete graph has an edge between every pair of distinct vertices. Its shortest-path distance is zero from a vertex to itself and one between distinct vertices. An isometric realization of is therefore a collection of points whose pairwise distances are exactly one. The paper's Section 5 treats connected graphs, so this mission takes . Its convention is that every logarithm has base two.
The foundational target is the paper's finite embedding statement:
It establishes the domain on which the least-dimension definition has its intended meaning. The remaining milestones isolate the geometric assertions used for complete graphs: a difference-body inclusion, separation of the interiors of certain convex-hull translates, and a cardinality bound for equilateral points in .
The goal is Proposition 5.4 (Linial–London–Rabinovich, p. 231):
The lower bound applies to every real norm on . The upper bound has the more specific target . Both inequalities, including and dimension zero, are part of the mission.
The equation determines the optimal dimension for an equilateral finite metric space when the norm is unrestricted. It also bounds the size of an equilateral set in every -dimensional real normed space by , with equality attainable by vertices of a binary cube under the supremum norm. For graph metrics, it gives a precise baseline against which dimension bounds for trees, cubes, and other connected graphs can be compared. The surrounding section of the paper uses the same geometric vocabulary for those other families (Linial–London–Rabinovich, Section 5).
The mathematical result is proved in the 1995 paper. This mission asks for machine-checked Lean proofs of the specified statements. The local declarations presently encode open proof obligations; compilation checks their types and imports, but does not establish the theorems. A completed development would provide a reusable interface for finite isometric dimension and for equilateral configurations under arbitrary finite-dimensional norms.
The easy direction uses points of a binary cube. The difficult direction must hold uniformly over every possible norm, whose unit ball need not be round or smooth. A direct coordinate count cannot assume that vectors have bounded entries in a prescribed basis. The paper formulates its argument through the convex hull of an equilateral configuration and a comparison of translated sets (Linial–London–Rabinovich, p. 231). Its printed volume line also leaves a degenerate case: if that convex hull has zero volume in the ambient space, cancellation of gives no numerical bound. A complete formal proof must account for such configurations without weakening the theorem to full-dimensional sets.
The Lean representation of is the function space Fin d → ℝ. A norm is an explicit function with all norm axioms, including definiteness and absolute homogeneity. Isometric dimension takes the infimum over dimensions admitting such a norm and an exact distance-preserving map. The complete graph is Mathlib's ⊤ : SimpleGraph (Fin n); its graph distance is converted to a real number. This distance is the discrete zero-or-one metric. The lower bound quantifies over every explicit norm. The cube milestone uses the supremum norm on finite real coordinate vectors. Convex hulls and interiors use the standard topology of this finite-dimensional vector space, which every norm induces.
The formal goal assumes , matching the paper's connected-graph convention; remains included, with dimension zero. The logarithmic expression is Nat.clog 2 n, the ceiling of the base-two logarithm, rather than a floor or a real logarithm. The source uses no unspecified asymptotic constant in Proposition 5.4 or its listed milestones. The empty point space is allowed in the general finite embedding lemma; its pairwise claim is vacuous, while the nonempty cases carry the intended content. The dimension definition is only used for realizable finite distances, so a totalized infimum's value on an unrealizable function has no role in the target.
The exact norm axioms and exact distance equality prevent shortcuts through seminorms, truncated distances, or a weaker distortion bound. The cardinality theorem retains lower-dimensional affine configurations; assuming positive ambient volume would discard part of the result. A complete development needs finite pseudometric geometry, the supremum norm, convex hulls and interiors, and a dimension-sensitive measure argument. Those components are useful beyond this graph. The paper's independent results on degrees, trees, cubes, and other graph families, as well as algorithmic running-time claims elsewhere in the article, are outside this mission.
Tree-width measures how closely a graph resembles a tree. It is the central width parameter of the Graph Minors series of N. Robertson and P. D. Seymour, which proves that finite graphs are well-quasi-ordered by the minor relation, and it governs the complexity of many algorithms: problems that are NP-hard in general become solvable in linear time on graphs of bounded tree-width (Courcelle's theorem). Branch-width, introduced in Graph Minors X (Robertson, Seymour 1991), is a second width parameter, defined from ternary trees whose leaves carry the edges of the graph. It is the natural parameter for the paper's main minimax theorem, which equates branch-width with the maximum order of a tangle, the obstruction to small decompositions.
Section 5 of Graph Minors X shows that the two parameters are equivalent, within a factor 3/2. This is what transfers the tangle duality from branch-width to tree-width, and it is why later work (for instance on matroid branch-width and on rank-width) treats branch-width as an interchangeable substitute for tree-width.
All objects are finite. A hypergraph has a vertex set , an edge set , and an incidence relation; the ends of an edge are the vertices incident with it, and an edge may have any number of ends. is the maximum number of ends of an edge, or if . A subhypergraph consists of subsets of and such that every end of a chosen edge is a chosen vertex; unions, intersections and inclusion of subhypergraphs are taken setwise.
A tree is a connected non-null graph without circuits; its leaves are its vertices of valency at most , and it is ternary if every valency is or .
A branch-decomposition of is a pair with a ternary tree and a bijection from the leaves of onto . The order of an edge of is the number of vertices of such that is an end both of an edge labelling a leaf in one component of and of an edge labelling a leaf in the other. The width of is the maximum order of an edge of , and the branch-width is the minimum width, or if .
A tree-decomposition of is a pair with a tree and a subhypergraph of for every , such that
Its width is , and the tree-width is the minimum width; exactly when . Each part is a subhypergraph and each edge lies in exactly one part, which differs from the familiar vertex-bag tree-decompositions of graphs, but gives the same tree-width on graphs.
The tangle number is the maximum order of a tangle in (p. 154), or if there are none.
The result. (5.1) shows that branch-width and tree-width bound each other up to the factor and the edge-size correction, and the page records that both bounds are attained ( with for the right-hand side, minus a perfect matching for the left-hand side). Together with the minimax theorem (4.3) of the same paper, unless and , it yields (5.2): tangles are, up to the factor , the exact obstruction to tree-decompositions of small width. That duality is the form in which tree-width enters the later papers of the Graph Minors series.
Formalizing it. The result is proved (1991); no machine-checked proof of it is known to exist. The platform holds tree-width statements for simple graphs with vertex bags (Graph Minors V, RobertsonSeymour1986.GM5.treewidth_le_theta9 and excluding_planar_graph), which are a different theorem about a different object. This mission formalizes the hypergraph tree-decomposition and branch-decomposition of Graph Minors X and the comparison between them. The companion missions of this series are Graph Minors. X. Obstructions to Tree-Decomposition I (the minimax theorem (4.3)), III (the grid tangle (7.3)), IV (the tree-decomposition separating distinguishable tangles (10.3)) and V (the structure theorem (11.1)).
The second inequality converts a branch-decomposition into a tree-decomposition; the difficulty is to obtain the bound with the floor and the separate term exactly, not up to an additive error.
The first inequality is where the obvious approach stalls: a tree-decomposition of minimum width is not a branch-decomposition. Its tree may have vertices of any valency, its leaves may carry no edge or several, and an edge may sit at an internal vertex. The three claims of the proof normalize an optimal tree-decomposition step by step without increasing its width. Each step modifies a tree on a finite vertex type while preserving three structural conditions (covering, edge-disjointness, the path condition), and the final step, suppressing vertices of valency , must be shown to produce a ternary tree with the edge orders bounded by part sizes. Most of the formal work is this tree surgery.
V, E with [Finite V] [Finite E] (the paper's "all hypergraphs in this paper are finite", p. 154) and a hypergraph G : Hypergraph V E given by its incidence relation.SimpleGraph (Fin n) with IsTree (connected, hence non-null, and acyclic). A leaf is a vertex of valency at most ; valency is (T.neighborSet t).ncard.sInf of the widths, which is a genuine minimum because a branch-decomposition exists when .sInf in of all bounding every ; the set is nonempty (one-vertex tree with ) and bounded below by , so the sInf is the minimum width and not a junk value.3 * β / 2; the ceiling would be a weaker statement. In (5.2), is stated as , which is equivalent.Infrastructure needed and reusable beyond this mission: tree surgery on SimpleGraph (Fin n) (attaching a leaf, deleting a leaf, splitting a vertex, suppressing valency-2 vertices), the existence of branch-decompositions for , and the computation of sInf-defined widths. Contributions of such lemmas, of proofs of the individual claims, and of small examples (, grids) are welcome.
Many problems of optimization and equilibrium can be written as one inclusion. Some examples are the Karush–Kuhn–Tucker conditions of a nonlinear program, nonlinear complementarity problems, variational inequalities and the equilibrium conditions of economic and traffic models. In each of them a point has to satisfy . In applications the data depend on parameters: estimated coefficients, prices, or the iterate of an algorithm. One then wants to know whether a solution persists under a perturbation of the parameter, whether it stays locally unique, and how fast it moves. For a smooth equation the classical implicit-function theorem answers all three questions. Inequality constraints make the solution set nonsmooth, and the classical theorem no longer applies.
S. M. Robinson's paper Strongly regular generalized equations (Math. Oper. Res. 5 (1980) 43–62) introduced the condition of strong regularity and proved an implicit-function theorem for generalized equations under it. The condition and the theorem became the starting point of the stability theory of variational inequalities and nonlinear programs. Later work characterises strong regularity for nonlinear programs (Robinson's own §4, through the strong second-order sufficient condition), and develops it in the theory of metric regularity and of single-valued Lipschitz localisations (Dontchev–Rockafellar, Implicit Functions and Solution Mappings, Springer 2009/2014). Its sensitivity results underlie the convergence analysis of Newton and sequential quadratic programming methods for these problems.
This mission formalizes §1–§2 of the paper: the definition, the implicit-function theorem (Theorem 2.1) with its proof, and the three results derived from it.
Let be a real normed linear space and its topological dual, the continuous linear functionals on . Let be closed and convex. The normal-cone operator of is
A generalized equation is the inclusion , for a function from an open set to . For it is the equation . For the nonnegative orthant of it is the nonlinear complementarity problem. For a general closed convex it is the variational inequality over .
Let solve the generalized equation, and let be Fréchet differentiable at . Linearising gives the multifunction
The generalized equation is strongly regular at with associated Lipschitz constant if there are neighbourhoods of in and of with the following property: for every the inclusion has exactly one solution in , and on . The condition depends only on , and .
In the parametric problem the function is , with in a topological space and base point . Its partial derivative in is .
Assume that exists on , that and are continuous at , and that solves , strongly regularly with constant . Then for every there are neighbourhoods of and of , and a function , with two properties. First, is the unique solution in of . Second,
Write for the linearisation at , for the residual, and . The milestones are four claims of the proof:
Theorem 2.1 reduces the stability of a nonsmooth problem to a property of one linearised problem at the base point. Once strong regularity is checked at , the solution exists, is locally unique and moves in a Lipschitz manner for every nearby parameter. Corollary 2.2 and Theorem 2.3 make this quantitative. Theorem 2.3 shows that a linear complementarity problem or a quadratic program approximates the nonlinear solution to first order. Theorem 2.4 is the analogue of Banach's perturbation lemma, which keeps an operator invertible under small perturbations. The later sections of the paper give checkable criteria for strong regularity: a Schur-complement test, a reduced-form test over polyhedral sets, and second-order conditions for nonlinear programs. Those criteria are the subject of the companion missions II–IV.
The theorems have been proved since 1980 and have been restated in textbooks. No machine-checked version of strong regularity or of this implicit-function theorem is known. Mathlib has the classical implicit- and inverse-function theorems for maps between Banach spaces, and the contraction mapping principle. It has nothing on normal-cone operators, generalized equations or Lipschitz localisations. The formalization adds this layer. It also shows that Theorem 2.1 needs no completeness of .
The obvious approach is to apply the classical implicit-function theorem. It fails because is set-valued and is not differentiable in any useful sense. The inverse is localised only to a neighbourhood and is single-valued only there. So every step must keep the iterates inside sets on which strong regularity says something. The neighbourhoods have to be chosen in the right order: from , then and , then the ball radius , then the parameter neighbourhood. The estimate (2.4) has to come out with the constant and no larger. The page applies the contraction principle in a space it calls only normed. A faithful proof must also obtain the fixed point without completeness of , for example through the completeness of .
StrongDual ℝ X, the normal cone is a Set (StrongDual ℝ X) that is empty off , and an inclusion is written .HasFDerivAt at every point of , for every . Continuity of at is joint and in operator norm.A complete development needs the following:
The definitions of normal cone and strong regularity are reusable for variational inequalities in general. Contributions are welcome at any level: proofs of the milestones, the goal from the milestones, or the companion results from the goal.
Routing several commodities through one capacitated network at the same time is a basic problem of network optimization, with applications to communication networks, VLSI layout and divide-and-conquer graph algorithms. Its optimum is the value of a linear program, but the natural certificates of an upper bound are combinatorial: every cut of the network limits how much can be routed across it. For a single commodity the max-flow min-cut theorem says that the best cut certificate is exact. With many commodities it is not, and the size of the gap between the best flow and the best cut is the question of this mission.
A multicommodity flow network has a finite vertex set , capacities (zero for non-edges and on the diagonal), and commodities: commodity has a source , a sink and a demand .
A feasible concurrent flow of value sends, for every , units of commodity from to : arc flows satisfy conservation of matter, with net outflow at , at and elsewhere, and the total flow of all commodities through each undirected edge , in both directions, is at most . The maxflow of the network is the largest such .
For , is the capacity of the edges leaving , and is the total demand of the pairs that separates, i.e. with . Every flow of value has to push units across the cut, so
A semi-metric on is a function with , symmetry and the triangle inequality; distinct points may be at distance , as in the paper.
There is an absolute constant such that every network in which some commodity has and has a set with and
The constant is not fixed; only the shape in the number of commodities is asserted.
The theorem bounds the flow–cut gap: the integrality gap of the linear relaxation of the sparsest cut problem is , so solving one linear program and rounding gives an -approximation to the sparsest cut. Sparsest-cut approximations are the engine of approximation algorithms for minimum bisection, graph partitioning, crossing number and VLSI layout. The dependence on rather than on the number of vertices matters when few pairs carry demand. The bound is tight up to the constant: on constant-degree expanders with all-pairs unit demands the gap is (Leighton–Rao).
The result has been proved since 1995 and is textbook material (Williamson–Shmoys, Ch. 15). It has no machine-checked proof. A formalization adds a verified bridge between concurrent flows, LP duality on networks and embeddings of finite metrics; each piece is reusable on its own. Corollary 3.4, Claim 2 in particular is a terminal version of Bourgain's theorem, of which no formal proof exists either.
Two steps carry the weight. The first is the duality between concurrent flows and metrics: Mathlib has no linear programming duality theorem in a form that applies directly, and the dual of the arc-flow program has to be identified with a minimum over semi-metrics, which needs a shortest-path argument on top of LP duality. The second is the embedding: Claim 2 of Corollary 3.4 must achieve distortion on the marked pairs, independent of . A direct application of Bourgain's theorem to the whole space gives , which is not enough when is much smaller than the number of vertices, and the paper's proof is a one-line reference to an earlier argument.
V with [Fintype V] [DecidableEq V]; capacities are a function C : V → V → ℝ with symmetry, nonnegativity and zero diagonal as fields of a Network structure. Commodities are indexed by Fin k; coincident or repeated pairs are allowed.maxflow is the supremum of feasible values; Lean's sSup returns on an unbounded set, which only happens without a commodity of positive demand and distinct endpoints, and the goal assumes one.Schnirelmann showed around 1930, by elementary means, that some absolute constant makes every integer a sum of at most primes. For odd :
The campaign's earlier values ( down to ) came from Schnirelmann's method with every constant written out, using Chebyshev-type lower bounds for and a Selberg sieve whose singular-series weight was crude. The entry hit the limit of that crude weight. This entry replaces it by the sharp weight , using the platform's proved prime-pair sieve (TaoFivePrimes.siebert_prime_pair_bound, Siebert's bound as used by Riesel–Vaughan) and its PrimePairSieve components. No zeta-zero input is used.
A representation of as a sum of at most primes is a finite multiset of primes summing to with at most elements counted with multiplicity. The Schnirelmann density of is (Mathlib: schnirelmannDensity).
This is the campaign template with the value filled in.
Let and . We show , then conclude with Mann's theorem. Write for the scale and for the twin-prime constant.
The argument stays elementary: no prime number theorem and no zeros of or -functions. New reusable components:
PrimePairSieve nodes.The Lean statement is the campaign template verbatim with in place of the value. Already proved on the platform and imported: TaoFivePrimes.siebert_prime_pair_bound, PrimePairSieve_reciprocal_weighted_sifted_bound, PrimePairSieve.divisor_kernel_comparison, PrimePairSieve.reciprocal_base_denominator_dominates_threshold, PrimePairSieve.sieve_constants_certificate, Schnir.basis_of_density.
PrimeNumberTheoremAnd (PrimeNumberTheoremAnd/IEANTN/Chebyshev.lean).All-pairs shortest paths (APSP) computes the shortest distance between every pair of vertices in a weighted graph.
We strengthen the previously formalized bound to for deterministic APSP on directed graphs with polynomially bounded integer weights and no negative cycles, using the same word-RAM model. It formalizes the improvement outlined by Alman and Vassilevska Williams in their conclusion.
Scheduling unrelated parallel machines to minimize the makespan, written , is one of the basic NP-hard problems of scheduling theory. A set of jobs must each be run on one of several machines, and the time a job takes depends arbitrarily on the machine; the goal is to finish all jobs as early as possible. Before the work formalized here, the best polynomial algorithm known guaranteed only a schedule within times the optimum (Davis and Jaffe, 1981), a factor that grows with the number of machines .
Lenstra, Shmoys and Tardos (FOCS 1987; CWI Report OS-R8714, 1987; Math. Programming 46, 1990) gave a polynomial algorithm with guarantee , independent of . Their tool is a rounding theorem: a vertex of a natural linear-programming relaxation can be rounded to an integral schedule that exceeds each machine's budget by at most one job. The rounding theorem and the binary-search framework around it became standard material in approximation algorithms.
There are jobs and machines. If job is scheduled on machine , it takes time units, a positive integer. A schedule assigns every job to one machine . The load of machine is , the makespan of is the largest load, and is the minimum makespan over all schedules.
For deadlines and a threshold , let and . The linear program (LP) has variables for and constraints
The integer program (IP) replaces by and requires . A vertex of (LP) is an extreme point of its feasible polytope. The support graph of a point is the bipartite graph on machines and jobs with an edge whenever .
A -relaxed decision procedure answers, for a deadline , either 'no' or a schedule, such that (1) every schedule it returns has makespan at most , and (2) if it answers 'no', no schedule has makespan at most . The binary search of Lemma 1 starts from the greedy schedule (each job on a machine where it runs fastest), whose makespan is an upper bound , with lower bound , queries the procedure at , moves to on a schedule and to on 'no', and outputs the best schedule found once .
The LP rounding procedure answers, on deadline , by solving (LP) with : 'no' if it is infeasible, and otherwise a 0-1 solution of (IP) obtained by rounding a vertex chosen by the LP solver, supported on .
For every LP solver (every rule choosing a vertex of (LP) when it is feasible), an LP rounding procedure exists, and for every such the output of the binary search satisfies
Theorem 2 gives a constant-factor approximation for that does not depend on . The same rounding theorem drives the paper's second algorithm, a -approximation for a fixed number of machines using polynomial space, and the paper's lower bound shows that no polynomial algorithm achieves a factor below unless . The Rounding Theorem, in its later form for generalized assignment by Shmoys and Tardos (1993), is a standard tool for LP-based scheduling and assignment.
The result is proved; it has, to our knowledge, no machine-checked proof. The platform contains Matoušek and Gärtner's textbook version (MatousekLP.Scheduling.lst_two_approximation, Theorem 8.3.4 of Understanding and Using Linear Programming), which uses a different relaxation: one bound minimized parametrically over , optimal solutions with linearly independent columns, and no per-machine deadlines. This mission formalizes the report's own route: deadlines , arbitrary vertices, binary search over a relaxed decision procedure. A formal proof would also yield reusable statements about extreme points of transportation-type polytopes and matchings in pseudoforests.
The obvious rounding, putting each job on a machine where is largest, can overload a machine by many jobs at once: nothing in feasibility alone prevents many jobs from each placing a small fraction on the same machine. The bound requires that each machine receive at most one job that the vertex treats fractionally, and this fails for general feasible points; it holds only because is a vertex. The step that carries the weight is therefore a statement about the combinatorial structure of the support of an extreme point, which must be derived from the linear independence of the tight constraints, followed by a matching argument on the resulting graph. Neither step is available in Mathlib in the form needed.
On the algorithmic side, the binary search must be shown to return a schedule within although the decision procedure is only approximately correct; the invariants (the lower bound stays below , the stored schedule stays within times the upper bound) have to be tracked through a recursion.
Fin m, jobs Fin n, processing times a matrix P : Matrix (Fin m) (Fin n) ℕ with all entries positive in Lemma 1 and Theorem 2 (the paper's model, p. 2). Loads, makespans and optimal schedules are the published MatousekLP.Scheduling.Schedule definitions applied to the real matrix ; is the makespan of a schedule σopt with IsOptimalSchedule.Set.extremePoints) correspond exactly. Theorem 1 and its steps are stated for real deadlines and real , more general than the paper's integers; the paper's proof does not use integrality, and mission 2 of this series needs non-integral .Discounted Markov decision problems are solved in practice by two classical schemes. Value iteration (successive approximations) is cheap per step but contracts the error only by the discount factor per step, which is slow when is close to . Policy iteration (Howard, 1960) converges in few steps, but each step solves a linear system for the value of the current policy. Puterman and Brumelle (Mathematics of Operations Research, 1979) showed that policy iteration is Newton's method applied to the optimality equation.
Puterman and Shin (Management Science 24, 1978) interpolated between the two schemes: replace the exact policy evaluation by steps of successive approximation. This is modified policy iteration of order . For it is value iteration; as it approaches policy iteration. The paper proves that every order converges and bounds its rate. The scheme remains a standard algorithm in dynamic programming (Puterman, Markov Decision Processes, Wiley 1994, §6.5), and it appears in reinforcement learning as "optimistic" or "generalized" policy iteration.
Timeline. Howard (1960): policy iteration for finite problems. Puterman–Brumelle (1979, circulated earlier): policy iteration as Newton–Kantorovich iteration, and the support inequality for the optimality operator. van Nunen (1976) and van Nunen–Wessels: convergence of related value-oriented methods in a different framework. Puterman–Shin (1978): convergence of modified policy iteration of every order from a starting point with , and the rate bound formalized here.
is a set of states with a -algebra. A family of policies is given. Each is a transition operator: a Markov kernel assigning to each state a probability distribution on . Each policy also has a one-period reward , and the rewards are uniformly bounded: . The discount rate satisfies .
is the Banach space of bounded measurable functions with . A kernel acts on by . For linear on , .
The optimality equation is
The paper assumes throughout that the maximum in (1) is attained for every , by a single policy at every state.
For , the truncated Neumann series is . Modified policy iteration of order runs the recursion
where attains the maximum in (1) at . A solution of exists and is unique. denotes a policy attaining the maximum at . The proofs also use the operators and the set .
If and , then for every
The mission also contains four further theorems that are not milestones: Corollary 2 (asymptotic rate at most when ), Proposition 2 (monotonicity in the order ), the representation (6) , and Proposition 1 (policy iteration as Newton's method).
The result. Bound (8) gives two guarantees. Every order of modified policy iteration converges at least as fast as value iteration, with factor per step. Once the improving policies stabilize near an optimal one, the factor approaches , the factor of value-iteration steps. This justifies spending cheap evaluation sweeps per policy improvement instead of solving a linear system. It also underlies the analysis of the many later variants: action elimination, asynchronous and approximate versions, and optimistic policy iteration in reinforcement learning.
Formalizing it. The theorems are proved on paper. As far as the platform's library shows, none of them is machine-checked: existing items cover value iteration and exact policy iteration for finite state spaces. This mission formalizes the whole chain on general measurable state spaces with Markov kernels, including the support inequality and the comparison operators . Corollary 2 is stated as an upper bound only, because the equality printed on the page fails in degenerate runs (see the item's note).
The obvious route to a rate is the contraction argument for value iteration: is monotone and a -contraction, so its iterates converge geometrically. For that argument does not transfer to the map . The truncated series is taken for the policy chosen at the current point, so the map changes with , and it is not monotone in general. The van der Wal–van Nunen example on p. 1133 of the paper shows that iterates of a higher order need not dominate those of a lower order from the same start. Moreover, without the condition the iterates need not even increase. A rate for (4) is therefore not a corollary of a fixed-point theorem for a single operator.
Formally, a second layer of difficulty is the setting itself. Everything happens in the space of bounded measurable functions on a general measurable space. So every operator applied to an iterate must be shown to preserve boundedness and measurability, and the maxima over policies are suprema over an arbitrary index set.
The Lean development (namespace ModPolicyIter.Conv) represents:
P i : Kernel S S with a measurable reward c i, ;IsBM (measurable and bounded), with supNorm v = ⨆ s, |v s|;The standing assumptions of §2 are carried by the model fields; items using a maximizer assume either global attainment (MaxAttained) or an explicit maximizing policy. A run of (4) is a sequence of functions paired with a sequence of policies, each policy a maximizer at the current iterate. Only is assumed; that later iterates lie in is part of the proofs.
Deviations from the page, all disclosed in the items:
The goal must not be trivialized by assuming , the support inequality, the sandwich of Corollary 1, or anything about . These are milestones to be proved, and none of them is a hypothesis of the goal.
Reusable infrastructure includes Markov kernels as operators on bounded measurable functions (positivity, , measurability of ), completeness of , and the Banach fixed point theorem on . The first of these serves any discounted dynamic-programming mission on general state spaces. Contributions of any milestone, or of helper lemmas about these operators, are welcome.
A firm that sells a product line of different qualities cannot see how much each customer values quality. It can only post a price for every quality and let customers choose. Mussa and Rosen's 1978 paper solves the monopolist's problem in this setting and compares the result with the competitive outcome. Their model is, together with Mirrlees' optimal income tax and Maskin and Riley's later treatment of nonlinear pricing, one of the founding examples of screening: the seller designs a menu so that customers sort themselves. The model's main qualitative prediction, that a monopolist degrades the quality sold to every customer except the one who values quality most, is the origin of the phrase "no distortion at the top". Textbooks on contract theory and mechanism design still teach it in this form.
Timeline. Mussa and Rosen (1978) give the first-order analysis, including "bunching" of customers at a common quality when marginal revenue is not monotone. Maskin and Riley (1984) treat the same problem for nonlinear quantity pricing. Myerson (1981) introduced the "ironing" procedure for non-monotone virtual valuations in auction design, which later became the standard way of describing the bunching conditions of this paper.
Consumer types are numbers with , distributed with a density that is positive and differentiable on the whole interval; . A consumer of type buys at most one unit, and from quality at price gets utility . Producing one unit of quality costs , where , is twice differentiable, and , for .
Under competition, price equals unit cost and type buys the quality with , or nothing when .
The monopolist chooses an assignment , the quality bought by type . It must be nondecreasing, nonnegative and piecewise differentiable on ; such assignments are called admissible. Incentive compatibility and participation fix the consumer surplus at , so the monopolist maximizes
An assignment is optimal if it is admissible and maximizes among admissible assignments. The marginal revenue of quality sold to type is
The paper's analysis runs through the marginal profit of a uniform quality increase for all types ,
For every optimal assignment :
and, if , the limit exists and satisfies (if , then ). In words: for every type below the top that buys under competition, types that do not buy under competition do not buy from the monopolist, and .
The paper's own chain of claims, in order: except at (p. 308); the first-order condition (9), for every admissible deformation; the identity (10) = (12), ; condition (13), ; condition (15), where ; at a jump; the absence of jumps; (17), where ; the bunching conditions (18)–(19); and the absence of a bunch at the top. Companion items state the two-type case of footnote 4, the uniform–quadratic example of §5, and the loss of consumer surplus (§6, "Second").
The result. The goal says how the monopolist differs from competition: it lowers every quality except the top one, and it never serves a type that competition leaves out. The distortion comes from the gap , which closes only at . The same comparison underlies results on second-degree price discrimination, regulation of product lines, and versioning of information goods. The bunching conditions (18)–(19) are an early statement of what is now called ironing.
Formalizing it. The result has been proved since 1978 in the economic literature, under the paper's smoothness assumptions and by a variational argument. As far as is known, it has not been machine-checked: no formal library contains the monopoly quality problem, its first-order conditions or the bunching conditions. The mission produces a checked version with the hypotheses made explicit, including the conventions at the endpoints that the paper leaves implicit. The uniform–quadratic example gives a concrete optimum that certifies the hypotheses are satisfiable.
The obvious argument sets pointwise and compares with . This fails when is not increasing: the pointwise solution is then decreasing somewhere and not admissible. The optimal assignment is constant on some intervals, and on such a bunch pointwise. The comparison with there needs the boundary conditions (18)–(19) and the fact that no bunch reaches . All of these come from one-sided deformations that respect monotonicity, so the first-order conditions are inequalities and need a separate argument for equality. The paper also asserts without a separate step that optimal assignments have no jumps, and later steps use continuity.
Types and assignments are real functions on ; only their values on matter. The type distribution and are the published MechanismDesign.Screening.TypeDistribution and virtualValuation. The standing assumptions are hypotheses of every main statement: is differentiable on (positivity and total mass 1 are part of the distribution), , and are differentiable on , and , on . is an added normalization: quality 0 means not buying. "Piecewise differentiable" means differentiable on outside a finite set. The competitive assignment is never formed; every comparison with is written through . Admissible deformations in (9) are required to keep .
The value does not affect , so a statement about itself would be false; the top-type claim is stated as a left limit. Optimality ranges over admissible assignments only. Any reading under which no optimal assignment exists makes the goal vacuous; the §5 companion rules this out, since its optimal assignment has a kink and uses the same notion of optimality.
Needed infrastructure: interval integrals of monotone functions, first variations under monotonicity constraints, and fundamental-theorem-of-calculus arguments for . The incentive-compatibility reduction (monotonicity and the envelope formula) is not posed here, because it is posed on the platform in Börgers' screening chapter. Related platform item: Börgers' Proposition 2.6 (MechanismDesign.Screening.nonlinear_pricing_optimal) treats a linear-cost, concave-valuation model under regularity, which is a different statement. Contributions to any milestone, and reusable lemmas about monotone deformations, are welcome.
Semiconductor burn-in ovens can process several jobs at once. A group placed in one oven must remain together until the longest job has finished, so increasing batch size saves oven starts but can delay short jobs. When several ovens are available, a scheduler also has to decide which oven receives each batch. Lee, Uzsoy, and Martin-Vega studied this setting and gave guarantees for a simple rule that first groups an arbitrary job list into batches and then sends those batches to the next available oven (Lee, Uzsoy & Martin-Vega 1992, §§2 and 5). Their bounds give a way to assess this easily specified rule against the best possible schedule, even when finding that schedule is difficult.
The paper treats both makespan, the time when all jobs have finished, and maximum lateness, the largest difference between a job's completion time and its due date. These objectives respond differently to batching. The makespan ignores which particular job finishes late; maximum lateness depends on each job's due date. Proposition 4 relates the lateness guarantee to the makespan guarantee of Proposition 1, making the two results a natural formalization unit (Lee, Uzsoy & Martin-Vega 1992, pp. 772–773).
There are jobs, indexed by , with processing times and due dates . All jobs are available at time zero. There are identical batch machines, each able to process at most jobs at once. A batch cannot be interrupted or enlarged after it begins, and its processing time is the largest among its members. A schedule partitions the jobs into nonempty batches, chooses a machine for each batch, and orders the batches on each machine. Batches assigned to a machine run one after another from time zero. Every job in a batch finishes when that batch finishes (Lee, Uzsoy & Martin-Vega 1992, p. 766).
For a set of jobs , write for the least makespan over all valid batchings and machine assignments. Write for the least possible value of , where is job 's completion time. For the full job set, abbreviate these by and . The maximum due date over all jobs is .
Batch list scheduling (BLS) begins with any ordering of the jobs. It divides successive entries into full batches of jobs, apart from a possibly smaller final batch. It then assigns each next batch to a machine that becomes available first. Denote the resulting makespan by and its maximum lateness by . The guarantee applies to every initial list; it does not require an earliest-due-date or longest-processing-time order (Lee, Uzsoy & Martin-Vega 1992, p. 771, Algorithm BLS).
Proposition 1 asserts, for every BLS list,
The milestone list includes the paper's processing-volume lower bound, , and Proposition 1 itself. The latter is stated for arbitrary job subsets as well as the full instance, because the paper applies it to a prefix sub-instance in the proof of Proposition 4 (Lee, Uzsoy & Martin-Vega 1992, p. 772).
The mission's goal is the printed ratio of Proposition 4:
The denominator is positive under the stated conditions, even if the optimal maximum lateness is negative. The remaining milestones record the paper's lower bound for a nonempty sub-instance and its reduction from the full instance to the BLS prefix containing a maximum-lateness job (Lee, Uzsoy & Martin-Vega 1992, p. 773).
The makespan result controls the cost of using an arbitrary initial list and simple next-available-machine assignments instead of optimizing both the batching and machine allocation. At , its factor becomes , the ordinary list-scheduling factor noted by the authors. Proposition 4 gives a corresponding bound for maximum lateness, normalized in a way that remains meaningful when (Lee, Uzsoy & Martin-Vega 1992, pp. 772–773).
These are proved results in the 1992 paper. The formalization work is to give their batch model, sub-instance optima, and the printed inequalities machine-checked statements and eventually proofs. The imported library already has definitions of least-loaded list scheduling and optimal assignment makespan for ordinary items on identical machines. This mission adds the batch layer, its lateness objective, and the comparison between the batch algorithm and unrestricted batch schedules. The Lean declarations here compile as open theorem targets; this proposal does not claim completed machine-checked proofs.
The processing time of a batch is a maximum, while its contribution to the volume of jobs is a sum. Treating each batch as an ordinary job gives a list-scheduling instance, but it does not by itself compare that instance's optimum with the optimum over all ways to form batches. That gap is central to the makespan bound. The lateness goal has a second obstacle: the job that determines the BLS maximum lateness may sit in a batch that is not the last to finish, and due dates prevent a direct substitution of a makespan bound for a lateness bound. Moreover, may be negative, so dividing by it would not give a valid relative error. The stated normalization and its positivity require explicit attention (Lee, Uzsoy & Martin-Vega 1992, proof of Proposition 4).
Jobs are Fin n and machines are Fin m; the paper's first job is Lean index zero. Processing times and due dates are real numbers. The paper's integer-data convention is sufficient for these inequalities but is not needed for their statements. Processing times are positive, all jobs are available at time zero, and the lateness goal requires nonnegative due dates. This last condition makes explicit what the paper's final inequality uses: allowing negative due dates makes Proposition 4 false. The full job set is nonempty. Prefix jobs are the first batches of the given arbitrary list, and the optimal values for a prefix range over every valid batching and assignment of those jobs.
The BLS implementation chunks the list into full batches and a final remainder. A batch is sent to a least-loaded machine, which is the first machine to become free when no idle time is inserted. The published list-scheduling definitions of NumStochOpt.ListScheduling supply this rule and the ordinary assignment optimum. They select the lowest machine index on a tie; identical-machine labels do not affect the resulting completion times. Machine schedules are represented by an ordered batch list and an assignment, with each machine processing its own batches back to back. No bound is obtained by defining the optimum over BLS-shaped consecutive batches, and no theorem fixes a favorable job list.
The mission covers correctness inequalities, not the paper's running-time claims or its later BLPT rule. Useful contributions include proofs of the four milestones, finite-schedule facts showing the optima are attained, and reusable links between batch completion times and least-loaded list scheduling. The parallel batch model can also support other objectives and scheduling rules.
Burn-in is the final testing stage of semiconductor manufacturing: finished integrated circuits are loaded on boards and held in an oven at high temperature for a prescribed minimum time, so that weak devices fail before shipment. An oven holds many boards at once, a load cannot be interrupted, and a board may stay in the oven longer than its specified time but never shorter. Because burn-in times are long compared to the other test operations, the ovens are frequently the bottleneck of the test facility, and the order in which lots enter them determines whether customer due dates are met.
Lee, Uzsoy and Martin-Vega (Operations Research 40(4), 1992) modelled an oven as a batch processing machine and gave polynomial algorithms for several due-date objectives. This mission covers the first of them: one machine, jobs with release times and a common processing time, and the question whether every job can be completed by its due date. Ikura and Gimple (Operations Research Letters 5(2), 1986) had already given an algorithm for this feasibility question when release times and due dates are agreeable; the paper replaces it by a simpler dynamic program, DP1, and uses DP1 with a bisection search to minimize the maximum tardiness.
There are jobs, indexed . Job has a release time (it cannot be processed earlier), a due date , and the common processing time ; all data are natural numbers. One machine processes up to jobs simultaneously.
A batch schedule of a set of jobs is a sequence of batches : nonempty, pairwise disjoint sets of at most jobs whose union is , processed in this order. A batch cannot be interrupted, and no job joins it once it has started. It starts as soon as the previous batch is finished and all its jobs are released, and it takes time :
Job completes at for the batch ; the makespan is . A schedule is feasible (has ) if for every job, and its maximum tardiness is .
Release times and due dates are agreeable if implies . A schedule is in batch-EDD order if no job of an earlier batch has a larger due date than a job of a later batch.
Algorithm DP1. With the jobs indexed in nondecreasing order of due dates, let and, for ,
For an index order nondecreasing in both and , and every ,
The minimum ranges over all batch schedules of the prefix: every batching and every batch order. The case is the paper's statement that DP1 "will find a feasible schedule with minimum makespan if a feasible schedule exists" (p. 768).
DP1 decides feasibility of and, when the instance is feasible, returns the minimum makespan of an on-time schedule. Applied to due dates augmented by a trial value , it decides whether is achievable, which together with the bound of Lemma 2 gives the paper's polynomial procedure for minimizing . The consecutive-partition structure behind it recurs in the paper's later dynamic programs (DP2 for agreeable processing times and due dates, DP3 for the number of tardy jobs), and in much of the later literature on batch scheduling with release dates.
The results are proved in the paper; none of them has a machine-checked proof. The mission formalizes the known proofs. Its formal statements also make explicit two assumptions that the printed text leaves loose: the tie-break of the index order, without which DP1 returns a wrong value, and the hypothesis of Lemma 2, without which the lemma is false.
The obvious argument for the goal is "by Lemma 1 the batches are consecutive, and DP1 enumerates consecutive partitions". Lemma 1 orders the batches by due dates, but it does not make the batches intervals of the index order: jobs with equal due dates may still be split across batches in an order that is not the index order, and when equal due dates are indexed against the release order DP1's value underestimates the start of the batch . The step from batch-EDD order to consecutive batches, and the fact that the exchange never increases the makespan, are the content of the justification milestone. The goal also asserts two directions at once: that the DP value is attained by some feasible schedule, and that no feasible schedule, consecutive or not, finishes earlier.
Jobs are Fin n, 0-based (the paper's job is i - 1); a prefix "jobs " is a prefix length . Data are natural numbers, as the paper assumes ("all data to be integers", p. 769). A batch schedule is a List (Finset (Fin n)); schedules are semi-active, starting every batch as early as possible, which loses nothing for the regular objectives here. DP1 is a def written as printed, with values in ℕ∞ and ; the minimum in the goal is an infimum in ℕ∞ over all valid feasible schedules, so its value on an infeasible prefix is .
Explicit readings of loose phrases:
Not formalized: the running time of DP1, Algorithm 1 (bisection over ) and Corollary 1, whose content is a running time. A formalization that restricts the minimum in the goal to consecutive or batch-EDD schedules would assume the milestones and is excluded; so is a DP value defined as the optimum itself.
The development needs list-based schedule recursions and ℕ∞ arithmetic only; the exchange lemmas for batch schedules (moving a job between batches without delaying later batches) are reusable for the paper's other dynamic programs. Proofs of any milestone, and of auxiliary lemmas on finish, jobCompletion and permutations of batch lists, are welcome.
The classical central limit theorem concerns sums of independent summands. Most sums that arise in statistics and applied probability are not independent: estimating equations of time-series models, stochastic approximation iterates, additive functionals of Markov chains, sequential test statistics. The standard route to asymptotic normality for such sums is to approximate them by sums of martingale differences, for which a central limit theorem holds under conditions close to Lindeberg's. McLeish's 1974 paper gives one of the shortest and most widely used proofs of such a theorem, and its conditions remain the reference form in textbooks (Hall and Heyde 1980, Chapter 3).
Timeline.
Let be a probability space. For each let be a row of real random variables, and let be sub-σ-fields belonging to row . Nothing relates the σ-fields of different rows, and the row lengths are arbitrary. Write .
The array is a martingale difference array (m.d.a.) if each is -measurable and integrable, and almost surely. Put
For real , the complex random variable is the product of Salem and Zygmund. Convergence in probability is written , convergence in is , and convergence in distribution is .
If is a martingale difference array such that (a) , (b) , and (c) , then
The proof of (2.3) goes through an abstract criterion, Theorem (2.1): for an arbitrary array, if for every real
then . The milestones are the claims of the paper's proofs of (2.1) and (2.3), in order:
The mission also states the corollaries of §2: Corollary (2.6) for near-martingales, Corollary (2.7) without moments, Corollary (2.8) under the variance normalisation , Lemma (2.11) (a Scheffé-type lemma), Lemma (2.15), and Corollary (2.13) under the Lindeberg condition and a fourth-moment condition (2.14).
Theorem (2.3) and its corollaries give asymptotic normality of martingale sums under conditions that are checked directly on the summands: the sum of squares rather than the conditional variances, and the maximum rather than a full Lindeberg condition. Through martingale approximation they yield central limit theorems for stationary ergodic sequences, Markov chain averages, stochastic approximation and the asymptotic normality of maximum-likelihood and M-estimators under dependence. Corollary (2.13) shows that under variance normalisation no conditional condition is needed at all.
The theorem is classical and proved. What this mission adds is a machine-checked version in the generality of the paper: an independent filtration per row and arbitrary row lengths. The platform already has formalized statements of martingale central limit theorems for one filtration shared by all rows, rows of length , and bounded or -negligible increments; none of these covers McLeish's array, and the truncation step, the identity for unbounded summands, and the second-moment bound of milestone 7 are not on the platform in this form.
Characteristic functions of cannot be factorised, because the summands are dependent. The natural first idea, conditioning step by step on and expanding , needs conditional second moments that are not assumed. McLeish's product avoids conditioning on characteristic functions, but itself is not bounded: can be large, and its expectation is only when the products are integrable. Any argument must therefore control the size of the products without conditional variances and without finite moments of the individual summands beyond condition (a), and must keep the martingale property intact while doing so. The passage from convergence in probability plus uniform integrability to convergence of complex-valued products, and from convergence of characteristic functions to convergence in distribution, needs measure-theoretic infrastructure that is only partly available in Mathlib.
X : ℕ → ℕ → Ω → ℝ with row lengths k : ℕ → ℕ. The column index is 0-based: the paper's is X n (i-1); only j < k n is ever constrained.Filtration ℕ m0, ℱ n; the paper's is ℱ n i, so is P[X n j | ℱ n j] and X n j is ℱ n (j+1)-measurable.UniformIntegrable … 1 P, which includes measurability and a uniform bound.TendstoInDistribution towards the law of the identity under gaussianReal 0 1.A formalization with one filtration for all rows, rows of length , or an m.d.a. predicate without integrability would state a special case or a vacuous variant of the theorem; the statements here avoid all three.
A complete development needs: products of complex random variables and their integrability, the pull-out property of conditional expectation for bounded factors, uniform integrability and Vitali's theorem for complex-valued families, and Lévy's continuity theorem. These are reusable well beyond this mission. Contributions of proofs of any milestone, of the corollaries, and of general lemmas feeding them are welcome.
In semiconductor manufacturing, finished chips go through burn-in: they are loaded on boards and held in an oven at high temperature to expose early failures. An oven holds a bounded number of boards, a load cannot be interrupted once started, and a chip may stay in the oven longer than its specified burn-in time but not shorter. Lee, Uzsoy and Martin-Vega (Oper. Res. 40(4), 1992) model the oven as a batch processing machine and give polynomial algorithms for several due-date objectives. The model has since become a standard one in scheduling theory; the survey of Potts and Kovalyov (2000) traces the batching literature that grew from it.
This mission formalizes the part of the paper's §3 on minimizing maximum tardiness when all jobs are available at time and processing times and due dates are agreeable. That is the problem the paper writes . The paper's own route is a feasibility test by dynamic programming, Algorithm DP2, which a bisection over due-date shifts turns into a minimizer.
There are jobs . Job has a processing time and a due date , both natural numbers. The machine has capacity . A batch is a nonempty set of at most jobs processed together. It occupies the machine for the processing time of its longest job,
A batch schedule of a job set is a sequence of pairwise disjoint batches covering , processed in this order and back to back from time . Batch and all of its jobs complete at . The makespan is , and the maximum tardiness is
A schedule is feasible when , that is, when every job meets its due date.
A sequence is in batch-EDD order (Definition 1) if no job in an earlier batch has a strictly later due date than a job in a later batch. Processing times and due dates are agreeable if implies . A schedule is consecutive when every batch is a block of indices and the blocks appear in increasing order.
Algorithm DP2 computes values :
Index the jobs so that and . Then for every ,
with . The minimum ranges over all schedules: any batching, any order. This is the paper's reading of as "the minimum completion time of jobs if they can be scheduled feasibly, and infinity otherwise".
DP2 is the paper's feasibility test for with agreeable data. With a bisection over the common shift of the due dates, it yields a polynomial algorithm for minimizing . A correct statement of what DP2 computes is therefore the core of that result. The same consecutive-partition structure underlies the paper's DP1 (release times, equal processing times) and DP3 (number of tardy jobs), which are separate missions of this series.
No machine-checked proof of any of these statements is known. The dynamic program's correctness is argued in the paper only by reference ("the justification of this algorithm is similar to that of algorithm DP1"), and the index order it needs is left implicit. A formal proof pins down exactly which ordering of the jobs makes the recursion correct.
The recursion charges for the last batch and checks only . Both shortcuts rely on the jobs being sorted by due date and by processing time at the same time. Lemma 3's exchange argument sorts a feasible schedule by due date, but it does not by itself produce consecutive blocks of a fixed index order. With ties in due dates the indexing also has to be compatible with processing times. Without that, the recursion is wrong: for , , it gives , while every schedule takes at least . The goal compares the DP with the optimum over all schedules, so the exchange arguments have to bridge arbitrary batchings and the consecutive ones the recursion enumerates. That bridge is the main step left to prove.
Fin n (job of the paper is index ); jobs are jobsUpTo n j. Data are natural numbers; the paper assumes integral data (p. 769).List (Finset (Fin n)); validity requires nonempty batches of size at most inside the job set, pairwise disjoint, covering the set. Batches start as early as possible. Batch time is the maximum processing time in the batch.⊤ : ℕ∞, and the goal's minimum is the infimum in ℕ∞, which is ⊤ exactly when no feasible schedule exists. DP2 is defined by the printed recursion, not as an optimum.Monotone d ∧ Monotone p for DP2 and its justification, and Monotone d for FBEDD;Many approximation results in probability and operations research take the form of a sequence of discrete or jump-driven systems converging to a diffusion or another limit process. When the approximating systems are written as stochastic integral equations, , the key step is to show that the stochastic integrals converge whenever the integrands and the integrators converge. That this is not automatic was known from the work of Wong and Zakai (1965): smooth approximations of Brownian motion produce a Stratonovich, not an Itô, limit. Kurtz and Protter (1991) give a condition on the integrators under which convergence in distribution of the pair (integrand, integrator) in the Skorohod topology implies convergence in distribution of the triple (integrand, integrator, integral). The result is essentially the theorem of Jakubowski, Mémin and Pagès (1989), with a formulation and proof that avoid the general theory of semimartingale characteristics. It underlies diffusion approximations for queueing and storage networks, approximation schemes for stochastic differential equations, and limit theorems for statistics and filters that are written as stochastic integrals.
Time is . A path in a metric space is cadlag if it is right-continuous and has a left limit at every ; is the set of cadlag paths, and . Let be the set of continuous, strictly increasing maps of onto itself. Cadlag paths converge to in the Skorohod (J1) topology if there are with and uniformly on bounded intervals. For a product space the pair converges if one sequence serves both components; this is strictly stronger than convergence of each component.
Let be the real matrices. For a -valued process and an -valued process , the stochastic integral (1.7) is
the limit in probability along partitions of whose mesh tends to zero. Throughout, means . An -adapted cadlag process is a semimartingale if with an -local martingale and of finite variation on bounded intervals, with total variation on . denotes the quadratic variation.
For let and
which collects the part of the jumps larger than ; then has jumps of size at most . Condition C2.2(i) on a sequence asks for decompositions such that for each there are stopping times with and . denotes convergence in distribution.
For each , let be -adapted with paths in , an -semimartingale satisfying C2.2(i) for some . If in the Skorohod topology on , then is a semimartingale with respect to a filtration to which and are adapted, and
The result. Theorem 2.2 reduces convergence of stochastic integrals to two checks: joint convergence of integrand and integrator, and the uniform control C2.2(i) on the integrators. Remarks 2.3 and 2.5 give simple sufficient conditions (stochastic boundedness of plus a second-moment bound; relative compactness for a fixed integrator), and Section 5 of the paper derives from it weak limit theorems for stochastic differential equations driven by semimartingales, including Wong–Zakai-type corrections. Without the theorem, each diffusion approximation that passes through an integral equation needs its own ad hoc argument.
Formalizing it. The theorem is proved and classical; nothing here is open. Lean's Mathlib has no Skorohod space, no stochastic integral against a semimartingale and no semimartingale, so the mission produces the first machine-checked definitions of J1 convergence on , of the left-point stochastic integral (1.7), and of convergence in distribution of cadlag processes, together with the deterministic facts about them that a proof of Theorem 2.2 needs. The definitions are meant to be reused by later missions on weak convergence of processes and on stochastic differential equations (the paper's Theorem 5.4 is planned as a follow-up that references them).
The obvious argument — the integral is a continuous function of the pair (integrand, integrator), so the continuous mapping theorem applies — fails in two ways. First, the map is not continuous in the Skorohod topology, and for a general semimartingale integrator it is not even defined path by path. Example 1.1 makes the failure concrete: with and , each component converges, yet for while , because the jumps of integrand and integrator coalesce in the wrong order; joint convergence of the pair excludes this. Second, Example 1.2 shows that joint convergence is still not enough: integrators whose variation grows without bound (piecewise linear interpolations of Brownian motion) produce an extra drift in the limit. C2.2(i) is the condition that excludes this, and the identification of the limit integral also requires knowing that the limit is a semimartingale, which is not given.
Time is ℝ≥0; a process is a map ℝ≥0 → Ω → E. is Fin m → ℝ and is Fin k → Fin m → ℝ, with the sup metric; products carry the max metric (J1 convergence does not depend on the product metric). The conventions the formal statements commit to:
The theorem has trivializing formalizations, all excluded here: componentwise convergence of in place of joint convergence; an integral not pinned to (1.7) (any process would do); and assuming the limit integral, or the semimartingale property of , as a hypothesis.
Local martingales and cross variations reuse the published Ethier–Kurtz definitions EthierKurtz_IsSourceLocalMartingale and EthierKurtz_HasCrossVariation. A complete development needs the Skorohod space and its tightness theory, the stochastic integral against semimartingales (existence and the Burkholder–Davis–Gundy/Doob estimates), and the quasimartingale criterion of Meyer and Zheng. Contributions to any of these layers are welcome; the deterministic milestones (Lemma 2.1, Lemma 6.2, the continuity of , (1.12)–(1.13), Lemma 6.1) are independent of the probabilistic ones and reusable for any work on the J1 topology.
Alan S. Manne's Linear Programming and Sequential Decisions (Management Science 6(3), 1960, pp. 259–267) is the first formulation of an infinite-horizon, average-cost sequential decision problem as a linear program. The illustration is a single-item inventory problem, but the construction, with unknowns indexed by a state and a decision and constraints expressing statistical equilibrium, became the standard state–action frequency linear program of Markov decision processes. Later LP approaches to average-cost Markov decision processes, including constrained ones, build on it.
Timeline of the LP approach to average-cost problems:
A positive integer bounds inventory accumulation; the stock levels are . At the start of a month the initial stock is observed and a production quantity is chosen; the available stock is . The month's demand is independent of everything else and has law . Backlogs are excluded, so the terminal stock is , which becomes the next initial stock. A finite set of admissible pairs , all with and containing for every , lists the decisions available at each stock level. Costs are three arbitrary real functions: of the initial stock, of the production quantity, and of the shortage level.
A stationary randomized decision rule is a conditional probability of producing at stock , supported on admissible pairs. It makes the initial stock a Markov chain. A statistical equilibrium of is a stationary distribution of that chain: the law of the terminal stock equals the law of the initial stock, (2). The expected monthly cost (1) of in the equilibrium is
the expectation taken under the joint law of (initial stock, production, demand).
The linear program has one unknown per admissible pair, the joint probability of (initial stock , production ). Its constraints are , (4) , and the equilibrium equations
and its objective (9) is with the cost coefficients (10)
The companion equation (8.0) for has right-hand side and is omitted from the constraints. A feasible is decoded into and .
The paper labels no theorem or lemma. The goal is assembled from §1 (third paragraph), §3 (N.B.), §4 (last two paragraphs), §5 and §7 (3), and every milestone is cited by section, display, table or footnote.
Assume for every admissible pair. Then the linear program has an optimal solution, and for every optimal solution , with decoding , is a stationary randomized rule, is a statistical equilibrium of , and
for every stationary randomized rule and every statistical equilibrium of .
The result turns an infinite-horizon control problem into a finite linear program. Equilibrium joint laws of (state, decision) under stationary randomized rules are exactly the feasible points of a polytope, and the average cost is linear on it. Consequences include computability by the simplex method; an economic reading of the dual variables (Manne's footnote 5 interprets them as the relative advantage of starting at a given stock level, related to Bellman's functional equation); and, in later work, the treatment of side constraints, which dynamic programming handles poorly.
The result is classical and proved in the paper (largely by inspection of the definitions). It has not been formalized. The formalization adds three things. First, a precise statement of what is optimized when the chain of a rule is not irreducible: the paper's §7 (3) concedes that a "decomposable" optimum makes the equilibrium depend on initial conditions, and the goal resolves this by optimizing over (rule, equilibrium) pairs. Second, an explicit treatment of the stock levels the equilibrium never visits, where the paper's quotient is undefined. Third, a machine-checked numerical example whose LP is derived from the general definitions, not entered by hand. Derman's later irreducible-case version exists on the platform as a separate open statement; this mission covers Manne's irreducibility-free version on state-dependent action sets.
Each step is elementary; the work is bookkeeping across three descriptions of the same object. The equilibrium is defined through the transition kernel of the controlled chain, the LP through the displayed sums over with conditions and , and the cost through the joint law of three variables. Identifying them needs a reindexing of the admissible pairs by stock level, the interchange of a finite sum with an infinite sum over demands, and . The naive argument "the LP constraints are the equilibrium equations, so the LP optimum is the optimal rule" skips two points. The constraints omit (8.0), so equilibrium at stock level must be recovered from (4) and the bound . And the decoding fails at unvisited stock levels unless a default action is supplied. Existence of an LP optimum requires compactness of the feasible polytope, not just its nonemptiness.
All statements live in the namespace ManneLP.Equilibrium. Conventions:
Finset (ℕ × ℕ) with and every ), a demand law with and HasSum p 1, and costs , . The shortage level is an integer; no convexity, sign or monotonicity of the costs is assumed.tsums; the demand is not assumed bounded. The goal and the cost identity assume the expected shortage cost at each admissible pair is finite (absolutely summable), which the page takes for granted.Trivializing formalizations are ruled out: equilibrium is not defined as (8) (which would make milestone 2 vacuous), (8.0) is not a constraint (which would make milestone 3 vacuous), the cost is not defined as (which would make milestone 5 and the goal's cost clause definitional), and the optimality comparison ranges over all rules and all of their equilibria, not over irreducible chains or pure rules.
Contributions welcome: proofs of the milestones and the goal; computations of the §6 example from the general definitions; reusable lemmas on stationary distributions of finite stochastic matrices and on the existence of LP optima over compact polytopes.
Maximum likelihood estimates, least-squares fits and sample-average approximations of stochastic programs solve , where averages a random integrand over observations. Their classical asymptotic theory rests on the implicit function theorem and needs a smooth, unconstrained problem.
When the estimate is constrained to a set, for example a nonnegativity constraint, a simplex or a polyhedron, the first-order conditions become a generalized equation
where is a multifunction such as the normal cone of the constraint set. The same form describes optimality conditions of stochastic programs and variational inequalities. Aitchison and Silvey (1958) treated equality-constrained maximum likelihood. Huber (1967) allowed nonsmooth estimating functions but required an open parameter domain. Dupačová and Wets (1988) and Shapiro (1989) derived limit laws for solutions of stochastic programs under smoothness of the expected gradient. King and Rockafellar (1993) gave a general theory that needs neither smoothness of the expected map nor single-valuedness of : the limit law of the normalized error is the image of a Gaussian under a contingent derivative, a positively homogeneous and generally nonlinear map, so the limit is generally not normal.
Let be a separable Banach space with norm , and let be the Euclidean norm on and . A multifunction assigns a set to each . Its graph is and its inverse is .
For sets indexed by , the upper limit consists of the points with , for some , and the lower limit of the points reachable along every such sequence. The contingent derivative of at is the multifunction with
is proto-differentiable when this upper limit equals the lower limit, and semi-differentiable when as and . A single-valued is B-differentiable at when in the same sense.
The deterministic problem is with , data and solution map . At a reference pair set . The analytical assumptions M.1–M.4 are as follows. is jointly continuous and B-differentiable in each variable, with the -derivative strong (uniform in near ). is closed and proto-differentiable. is subinvertible: , and a closed-graph, convex-valued selection of near passes through . The contingent derivative is at most single-valued.
The statistical problem has i.i.d. random elements of a measurable space and an integrand on a compact neighborhood of . It satisfies the probabilistic assumptions P.1–P.4: continuity in , measurability in , a finite second moment at one point, and a Lipschitz bound with . The M-estimate is a measurable solution of
and the true equation is with .
Under P.1–P.4 on a compact neighborhood of , B-differentiability of at , and M.2–M.4 for , every sequence of measurable solutions of (2.5) with almost surely satisfies
The goal fixes the limit law completely: the map is the contingent derivative of , and the Gaussian has the covariance of the integrand at .
The three displays (Theorem 2.4's upper-Lipschitz inclusion, and Theorem 2.6's semi-differentiability and Lipschitz bound) are statements the paper cites from King and Rockafellar, Sensitivity analysis for nonsmooth generalized equations ([12]: Proposition 2.1, Theorem 4.1, Remark 4.3). They are cited results, not this paper's own, and are milestones because the proofs of Theorems 2.4 and 2.6 rest on them.
Theorem 2.7 gives the limit law of constrained and nonsmooth M-estimates in a form that can be computed. When is the normal cone of a polyhedron, is piecewise linear, and the limit is the solution of a random linear complementarity or quadratic problem driven by a Gaussian vector. This underlies the asymptotic theory of sample-average approximation in stochastic programming, where the paper applies it to stochastic programs (§3) and to piecewise linear-quadratic tracking problems (§4). Theorem 2.6 separates the deterministic sensitivity analysis from the probability, so any data sequence with a known limit law yields a limit law for the solutions.
The result is proved in the paper modulo the cited theorems of [12] and [11], but none of it is machine-checked. Mathlib has the real-valued i.i.d. central limit theorem, Gaussian measures on Banach spaces and convergence in distribution. It has no multivariate or Banach-space central limit theorem, no contingent derivatives and no set-valued implicit function theorem. Formalizing the mission produces these, along with a checked version of the cited sensitivity results.
The classical argument linearizes at , inverts the Jacobian and applies the delta method. Here is set-valued and its derivative is only positively homogeneous. There is no Jacobian to invert, and the solution map need not be differentiable or even single-valued away from . The replacement for the implicit function theorem is the semi-differentiability of the localized solution map under M.1–M.4. Proving it means controlling both the upper and the lower set limits of difference quotients of solution sets, and subinvertibility is what supplies existence of nearby solutions.
The probabilistic side cannot work coordinate by coordinate either. The estimate solves an equation in the whole function , so convergence of at finitely many points is not enough. The central limit theorem must hold in the sup norm on , which requires tightness of the empirical process, and only then can the deterministic sensitivity result be composed with it.
Points live in EuclideanSpace ℝ (Fin n), and is a real normed space with [CompleteSpace Z] [SeparableSpace Z] where the paper says "separable Banach". Set limits are Kuratowski limits along filters ( is 𝓝[>] 0, and is the product filter). The contingent derivative is defined by (2.2) alone. M.4's printed sum formula equals it under M.1, and this is not assumed. "B-differentiable" is read as the limit (2.4). Products carry Lean's max norm. is s 0, empirical means sum over Finset.range ν, and (2.5) is required for . is empty off . Convergence in distribution is Mathlib's TendstoInDistribution, with the limit on its own probability space. The law of is fixed through linear functionals: . In Appendix A1–A3 the integrand is S → C(↥U, Rn m) with the Borel σ-algebra, and "Gaussian" is IsGaussian.
Explicit choices relative to the printed text:
The conclusion of the goal names its limit: the image of the stated Gaussian under a map whose values lie in the contingent derivative of . A statement asserting only that converges in distribution to some limit, or replacing by a linear map, is a different and weaker theorem. A sorry-free check confirms that the goal's hypotheses can all be met (a degenerate instance with , ).
A complete development needs Kuratowski set convergence and contingent derivatives (reusable across set-valued analysis), a central limit theorem in for Lipschitz-indexed processes (reusable for empirical-process theory), and a continuous-mapping argument for random closed sets. Contributions to any of these layers are welcome, as are proofs of the cited [12] statements.