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.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. A high-probability approximation guarantee is a separate claim requiring an explicit probability bound. The optimum includes entangled states. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Every pure integer program, once its linear programming relaxation has been solved, can be relaxed further to a problem over a finite Abelian group: the nonbasic variables must satisfy a single congruence in the group of the optimal basis. R. E. Gomory introduced this relaxation in 1965 and studied the convex hull of its solutions in Some polyhedra related to combinatorial problems (Linear Algebra Appl. 2 (1969), 451–558, doi:10.1016/0024-3795(69)90017-2). The facets of these group polyhedra are valid inequalities for every integer program whose basis produces the same group, and they became the source of cutting planes for integer programming: Gomory's mixed-integer cut and the later theory of corner polyhedra and subadditive valid inequalities descend from them.
The number of facets grows fast with the order of the group, so a list of facets for each group is not a usable description. Section 3D of the paper, "Lifting up Faces", gives a structural tool instead: facets of the polyhedron of a small group produce facets of the polyhedron of every larger group that maps onto it. This mission formalizes that construction (THEOREM 19) and its converse (THEOREM 20).
Let be a finite Abelian group, written additively, with zero and order , and let . For a right-hand side , the group equation asks for nonnegative integers , , with
Its solution set is ; when , the zero solution is excluded, as stipulated on p. 474. Each solution is a point of , a space of dimension , and the master polyhedron is the convex hull of . Gomory reads a solution as a path from to that uses the element exactly times; with arc lengths its length is .
An inequality , written , is a face of when , every satisfies it, and the solutions on the hyperplane generate that hyperplane: every point of it is a weighted sum, with total weight 1, of such solutions. A face is therefore a facet; Gomory says "face" throughout, and so does this mission. The solutions with are the minimal paths.
Let be a homomorphism of onto a second finite Abelian group , with kernel . A coefficient vector on is lifted to by
so that every element of the kernel gets coefficient .
If and is a face of with , then
For instance, the face of lifts through reduction mod 2 to the face of (p. 488).
Conversely, a face of with and for some is the lift of a face of for some of onto a group with .
THEOREMS 19 and 20 together say that the faces of with and a zero coefficient are exactly the faces lifted from proper quotients of . A catalogue of these positive-right-hand-side faces therefore only needs the faces with all coefficients positive; the rest come from smaller groups. Gomory uses this to explain the tables of Appendix 5: for and every such face is a lift of the single nontrivial face of , and for a direct sum every face of the polyhedron of a summand not containing extends to a face for (p. 489). The same idea, sending facets of one group problem to facets of another by a homomorphism, recurs in the later theory of group relaxations and infinite group problems.
Both theorems are proved in the paper. To the knowledge of this mission, neither the group polyhedra, their faces nor the lifting theorem has a machine-checked formalization; the platform's other "lifting" results (lifted cover facets of the knapsack polytope, cone lifts of convex sets) are different notions. The mission produces a reusable definition layer for master group polyhedra and their faces, stated once for an arbitrary finite Abelian group, and a formal version of the passage between faces of a group and of its quotients.
Validity of the lifted inequality is a one-line computation (milestone 2). The content is that the lift is a facet: one must exhibit affinely independent solutions on the hyperplane, while the quotient face only supplies of them. A solution of the quotient problem does not determine a solution for ; coset representatives must be chosen and the path closed by a kernel element, and the kernel coordinates, which all have coefficient zero, must still be filled to full rank.
The obvious reduction, "a facet pulls back to a facet under a surjective map", fails here because the map from -paths to -paths is a linear projection from dimension to and does not lift independence by itself. It also fails at : with , , , the face of lifts to , which is valid but not a face of .
The formalization uses one definition file for an arbitrary finite Abelian group ([AddCommGroup G] [Fintype G] [DecidableEq G]), instantiated at both and . It commits to the following readings:
Function.Surjective ψ, and is .A formalization that proves only validity of the lift, or that defines faces without the generation condition (so that every valid inequality is a "face"), would be trivial and is ruled out by the definition of IsFace.
The development needs finite sums over fibres of , a choice of coset representatives, and a rank argument for a block matrix with full-rank diagonal blocks. The definitions of , and face are reusable for any further result on master group polyhedra. Proofs of the milestones in any order, alternative proofs of the face criterion, and a proof of THEOREM 20 are welcome.
Finite group equations arise when an integer program is expressed relative to an integer basis: the residue of a candidate solution in a finite Abelian group records whether it satisfies the original integrality requirement. Gomory's group polyhedron collects the nonnegative integer solutions with one prescribed residue. Its faces give valid linear inequalities for the group relaxation, so a description of those faces is useful to anyone studying integer programming cuts or the geometry of integer hulls. Gomory's 1969 paper develops the group equation and its polyhedra in this setting and then gives a finite system for the faces of the largest, or master, polyhedron. Gomory 1969, pp. 457–458, 474, 480–483.
The main question is how to recognize a facet inequality without ranging over every nonnegative integer solution of the group equation. The paper's Theorem 7 characterizes facets through a system with one row for each integer solution, an infinite collection in general. Theorem 18 replaces that family by rows determined by pairs of group elements and a rank condition at the candidate coefficient vector. Gomory 1969, pp. 469–470, 481–483.
Let be a finite Abelian group with zero , and let . For a subset and a right-hand side , a group-equation solution is a nonnegative integer vector satisfying
The set of solutions is , and the group polyhedron is their convex hull in the real coordinate space . The master polyhedron uses . This mission concerns ; Gomory specifies a separate convention at , excluding the zero solution from that master polyhedron. Gomory 1969, pp. 457–458, 474–475.
Gomory calls a face when , all points of satisfy the inequality, and its tight points generate the entire hyperplane by affine combinations. Thus "face" means a facet of full hyperplane dimension here. The equivalent integer-point criterion uses the tight members of , which is the representation adopted in Lean. A basic feasible solution of a linear system satisfies every equation and inequality and has tight rows whose coefficient vectors span the full variable space. Gomory 1969, pp. 468–469.
The path to the goal starts with the sign of the face coefficients, the infinite-system characterization, and the shortest-path interpretation. An integer vector represents a path whose total group displacement is and whose length is . The shortest-path statements lead to subadditivity and complementary equalities for face coefficients. For , Theorem 17 collects the row conditions needed for the final system. Gomory 1969, pp. 469–473, 480–481.
The target is Theorem 18. Fix and . With , system (13) is
The goal asserts the full equivalence
The equation rows, ordered pair rows, and nonnegativity rows all count toward basicness; is held fixed. Gomory 1969, pp. 481–483, Theorem 18.
Theorem 18 turns a geometric property defined against infinitely many integer vectors into a finite test in coefficient variables. A solver can check its displayed equations and inequalities and then check whether the tight row vectors have full rank. That gives a concrete route to enumerating the facet coefficient vectors of for a fixed finite group, the use Gomory reports immediately after the proof. Gomory 1969, p. 483.
The result was proved in the paper; the work here is to formalize that known theorem and the numbered results it uses. The group-solution model, the integer-point facet criterion, and the generic tight-row definition of basic feasibility can also support other group-polyhedron arguments. The local prior-art search found related formalizations of facets and polyhedra, but none with the same integer-point-generated hyperplane and finite-group conventions, so these definitions are stated for this paper's objects.
Validity of the rows of (13) for a face does not by itself establish Theorem 18. Basicness requires the tight rows to span all coefficient directions, and the converse must turn that rank information into enough tight integer solutions to generate a hyperplane. A supporting inequality that is tight at only a smaller face would pass a mere feasibility check while failing Gomory's face definition. The shortest-path results connect the group equations to the coefficient restrictions, but do not erase the rank requirement. Gomory 1969, pp. 468–470, 472–473, 481–483.
Lean uses a finite Abelian group and a Finset of nonzero elements. Its real vectors have coordinates indexed by itself, with no unconstrained zero coordinate. The group equation is a finite sum of natural-number multiples in ; is the real convex hull of the cast integer solutions. A face requires a nonzero normal, validity on every integer solution, and equality between the affine span of tight integer points and the entire hyperplane. This excludes the trivial reading that merely asks for one tight point. It also makes an empty solution set incapable of supplying a face. Theorem 7 assumes nonempty (), as the paper does implicitly: with no coordinates every vector would be trivially basic.
Paths are represented by their nonnegative integer arc-multiplicity vectors. The same vector can describe several arc orders, but the length and group displacement used here depend only on multiplicity. Shortestness is stated by comparison with every competing vector of the same displacement; no infimum with an empty-set default is used. The complement and subadditivity rows of (13) use , and the subadditivity rows include ordered pairs with equal entries. Basic feasible solutions use the span of tight coefficient rows, including equation rows, in the full real space of variables.
The mission includes the paper's Theorems 6, 7, 10, 17, Lemmas 1–2, and both numbered corollaries on p. 473 as milestones. Contributions that establish the affine-span and rank equivalences, or reusable finite-group shortest-path and polyhedral lemmas, directly advance the target. Theorems for and for other sections of the paper are outside this mission's stated domain.
A decision maker may choose an action whenever a system changes state, even though the time until the next change is random. Maintenance and replacement decisions are examples: a repair choice changes both the next operating state and the length of time before another choice is available. A discrete-time Markov decision model gives every decision epoch the same duration. A semi-Markov decision process allows the holding time to depend on the current state, action, and next state. Kallenberg's Chapter 7 develops discounted and average-reward versions of this finite-state model, including a characterization of optimal discounted value through inequalities and a linear program (Kallenberg 1983, Chapter 7).
The mission focuses on the discounted part of that chapter. The result is known: Kallenberg proves it as Theorem 7.2.1. The formalization task is to state and eventually prove the result for the same policy class and the same general holding-time distributions. Those details matter because a stationary-policy-only version would omit the comparison that the theorem makes with all admissible policies.
Let be a nonempty finite state set. Each has a finite nonempty set of available actions. If action is chosen, the next state is with probability , with . Conditional on , the nonnegative time until that transition has distribution . The action earns a lump reward immediately and a reward rate during the ensuing sojourn. Neither the holding-time laws nor the reward rates are required to be identical across transitions (Kallenberg 1983, pp. 210–212).
Fix a positive continuous discount rate . The factor applied after elapsed time is . Assumption 7.2.1 requires the Laplace–Stieltjes transform of each conditional holding-time law to satisfy
The assumption is strict for every triple; it does not require a particular parametric family. Define the one-epoch expected discounted reward and discounted transition entry by
A policy is a sequence of randomized decisions. At each epoch its choice may depend on every previously observed state and chosen action and the current state. It does not observe previous sojourn times when choosing. Let be the expected sum of discounted lump and rate rewards from initial state , as in equation (7.2.1). The DRD value vector is , with the supremum over this full policy class. A real vector is DRD-superharmonic when
These are Kallenberg's Definitions 7.2.1 and 7.2.2 (p. 214).
Theorem 7.2.1 states that the value vector itself satisfies the superharmonic inequalities and lies below every other vector satisfying them:
This is the mission goal. Its content includes both clauses: merely showing that every superharmonic vector bounds policy rewards would leave out the assertion that the value is superharmonic.
Lemma 7.2.1 expresses as a sum of expected discounted state-action occupancies. Theorem 7.2.2 says that a feasible action choice attaining equality in the value equation at every state yields an optimal pure stationary policy. Theorem 7.2.3 says that positive support in an optimal solution of the dual linear program (7.2.11) yields such a policy. Their statements and exact conditions are the mission's milestones (Kallenberg 1983, pp. 212, 216–217).
The goal turns a supremum over possibly history-dependent randomized policies into a finite system of inequalities indexed by available state-action pairs. The next two results explain how equality in those inequalities and an optimal linear-programming solution identify a pure stationary policy with the same value. Thus the finite programs are statements about the original semi-Markov process rather than a separate discounted matrix model (Kallenberg 1983, pp. 214–217).
Kallenberg supplies paper proofs. This mission supplies Lean statements and a shared model interface; the proposed theorem items still require machine-checked proofs. The model's arbitrary conditional holding-time measures, its distinction between the current reward and future discounted value, and its history-dependent policy class are reusable for other finite semi-Markov arguments. The average-reward section of Chapter 7 is outside this mission.
The straightforward finite-state discounted equation concerns expected one-step rewards. The source value, however, is defined from rewards earned at random physical times, and a policy can react to its entire discrete history. Identifying these two descriptions requires accounting for the joint state, action, and elapsed-time law without giving the policy access to past holding times. Holding times may equal zero with positive probability; the strict transform assumption excludes a degenerate law concentrated entirely at zero, but it does not make each holding time strictly positive. A second issue is real-valuedness: all-policy suprema and integrals must represent the finite quantities in the source rather than Lean's default values on ill-posed inputs.
Lean uses finite types for states and actions, with a nonempty available-action finset for each state. Conditional sojourn laws are probability measures on with no mass on negative times. This includes arbitrary distributions on and permits an atom at zero. The model stores stochastic transition rows, lump rewards, and rate rewards. The discounted layer stores and the source's strict per-triple transform inequality. The expected one-epoch reward uses a Lebesgue integral against each sojourn law.
Policy decision rules read a list of past state-action pairs and the current state. Finite-horizon value recursively integrates the original epoch reward and its holding-time discount; policy value is its limit. The coordinatewise supremum ranges over all such policies. The occupation sum of Lemma 7.2.1 is a separate theorem, not the definition of policy value. A proof must establish convergence and boundedness from Assumption 7.2.1 so that Lean's total limit, integral, and real-supremum operations have their intended meanings.
The dual program sums only over actions available in each state and uses strictly positive weights , equality flow constraints, and nonnegative variables as printed. Its pure stationary selector must choose an available action with positive dual mass in every state. Contributions establishing the occupation identity, value bounds, Bellman inequalities, or dual decoding all fit the mission.
An integer program in standard form, subject to , , integer, is easy to state and hard to solve. Its linear programming relaxation is solved by the simplex method, which ends at an optimal basis . The difference between the two problems is the integrality of , and R. E. Gomory's 1969 paper Some polyhedra related to combinatorial problems (Linear Algebra Appl. 2, 451–558, doi:10.1016/0024-3795(69)90017-2) measures that difference with a finite Abelian group. Dropping only the nonnegativity of the basic variables leaves a problem whose feasible set has a simple structure: its convex hull is the corner polyhedron, and its integer points are the solutions of an equation in the group .
The first section of the paper uses this to explain when the integer program reduces to the group problem. Its asymptotic theorem says that if lies far enough inside the cone where is LP-optimal, then an optimal solution of the group problem gives an optimal integer solution. Gomory first proved this in 1965 (On the relation between integer and noninteger solutions to linear programs, PNAS 53, 260–265, doi:10.1073/pnas.53.2.260) by a counting argument on group solutions. The 1969 paper proves it again through the geometry of the corner polyhedron. The vertices of that polyhedron are irreducible, and an irreducible point is small. This is the version formalized here.
Let be an integer matrix, with a nonsingular matrix (the first columns) and the matrix of the remaining columns . As on p. 452 of the paper, contains an unit matrix. Let and . The integer program (2) is
The relative prices are , with components . is an optimal LP basis when and every .
The group is , where and is the lattice of integer combinations of the columns of . Let be the quotient map. is finite of order . Let be the set of nonzero elements among , and put . The group equation is
and is the convex hull of its solutions in . A nonnegative integer is irreducible if any two integer vectors with and are equal.
The group costs are . Problem (8) minimizes over the solutions of the group equation. A corresponding vertex of a point (Remark 1) is a nonnegative integer with three properties: ; at most one positive per group element; and when . It uses only least cost columns when only if .
The cone is where is LP-optimal. is the set of its points at Euclidean distance at least from its frontier, and is the largest Euclidean length of a column .
If , is a vertex of minimizing (8), and is a corresponding vertex using only least cost columns, then
THEOREM 4 explains why integer programs with large right-hand sides are often easy. For outside a band of width along the boundary of the cone , the integer optimum is the LP solution plus a correction that depends only on the class of modulo the lattice of . That correction is periodic in and can be tabulated once for the group elements. The vertex form adds a structural statement: the correction can be read off a vertex of the corner polyhedron, so the faces and vertices of corner polyhedra (the subject of the rest of the paper) bear directly on integer programming. Display (10) shows such optimal solutions are small: their nonbasic parts satisfy .
All results here are proved in the paper. None of them is formalized yet. The 1965 version of the asymptotic theorem, posed as THEOREM 1 of the mission on Gomory (1965), is in the same family of statements. Its hypothesis is that the group solution is optimal; here the hypothesis is that it is a vertex of . Its counting lemma (a short optimal group solution) and its bound have counterparts in milestones 4 and 6.
An optimal solution of the group problem need not be short. Group solutions can be made longer without changing their cost (add a zero-cost cycle), and a long nonbasic part can push out of the cone , making negative. The goal must therefore use the vertex hypothesis. Vertices are irreducible (THEOREM 2), and irreducibility bounds their size through a pigeonhole count in the finite group (THEOREM 1). The formal work is spread across three settings: the convex geometry of the hull of an infinite integer set, the arithmetic of the quotient and its order, and the linear algebra connecting , the cone and its frontier.
Vectors on are functions on the subtype of a Finset of the group. Integer solutions are -valued, and is convexHull ℝ of their real images. THEOREMS 1 and 2 are stated for an arbitrary finite Abelian group and any finite not containing , as in the paper. The integer program uses the basis as the first columns, Fin m ⊕ Fin n. is the real matrix inverse, and every statement assumes . Optimality of means feasibility plus for every feasible integer ; no supremum is taken. The loose phrases of the paper are read as follows.
The printed slip on p. 462 ( for THEOREM 1's product) is corrected in the Lean. Dropping the vertex hypothesis from the goal is not a valid formalization (the statement becomes false in general), and neither is defining irreducibility with real (THEOREM 1 then fails). The existence of a minimizing vertex, which the paper takes for granted, is not posed.
A complete development needs the finiteness and order of (Mathlib's AddSubgroup.index_eq_natAbs_det), extreme points of convex hulls (extremePoints_convexHull_subset), and an argument that a closed cone with deep inside it contains the ball around . The group-polyhedron definitions and THEOREMS 1–2 apply to any finite Abelian group and are reusable beyond this mission. Proofs of any milestone are welcome independently.
A two-person zero-sum stochastic game (also called a Markov game) is a Markov decision problem with two decision makers who pull in opposite directions: at every time point both players choose an action simultaneously, one player pays the other, and the system moves to a random next state whose law depends on the current state and both actions. Stochastic games were introduced by Shapley (Shapley 1953) and are the standard model for adversarial sequential decisions in operations research, economics and computer science (pursuit–evasion, inspection, robust control against an adversarial environment).
Shapley proved that a discounted stochastic game has a value and that both players have stationary optimal policies. The value, however, is in general not computable by linear programming: it need not lie in the field generated by the data. Kallenberg's Example 6.2.1 (after Parthasarathy and Raghavan) has rational data and an irrational value in one state. When only one player controls the transition probabilities, the situation changes: the value and stationary optimal policies are the optimal solutions of one pair of dual linear programs (Parthasarathy & Raghavan, as cited in Kallenberg 1983, pp. 192 and 196; Kallenberg 1983, Chapter 6).
Timeline.
The state space is with . In state player I chooses an action from a finite nonempty set and player II an action from a finite nonempty set . Player I then receives from player II, and the next state is with probability , where .
A history at time is . A policy of player I chooses, at each time and history, a probability distribution on ; policies of player II are defined likewise. A policy is stationary, written or , if the distribution depends only on the current state. With the expected reward in period from initial state , the total reward is .
A pair is optimal if, componentwise,
and then is the value of the game.
Assumption 6.2.1 (contraction). There are and with for all , , . The discounted game is the case .
Assumption 6.2.2 (single controller). does not depend on ; it is written .
For a stationary write and . A vector is TMG-superharmonic if some stationary of player II satisfies for all , . For weights the two linear programs are
Under Assumptions 6.2.1 and 6.2.2, let and be optimal solutions of (6.2.1) and (6.2.2), and . Then
The goal fixes no constants; it states that the LP pair produces the value and optimal stationary policies.
Theorems 6.2.1 and 6.2.2 hold for the general contracting game. Assumption 6.2.2 enters only from (6.2.1) on.
The result. Theorem 6.2.3 turns a single-controller game into a finite computation, Algorithm XXVII: solve one LP pair and read off the value and optimal stationary policies of both players. A consequence (Remark 6.2.1) is that the value and the optimal decision rules lie in the field generated by the rewards and transition probabilities. Example 6.2.1 shows this fails without Assumption 6.2.2. Theorem 6.2.4 matches the feasible points of the dual program with the stationary policies of the controlling player. This is the game version of the correspondence between state-action frequencies and policies in Markov decision problems.
Formalizing it. All results are proved in the book, and Theorem 6.2.1 is classical. None of them is formalized: the platform has turn-based stochastic games with positional strategies (TBSGStrategyIteration), which do not cover simultaneous moves or history-dependent randomized policies. The mission adds a reusable model of simultaneous-move stochastic games with history-dependent policies, together with machine-checked optimality of the LP solution against every such policy.
There are two difficulties. First, optimality in (6.1.1) is against every history-dependent randomized policy of the opponent, while the LP produces only stationary policies. Fixing one player's stationary policy reduces the game to a Markov decision problem for the other player (Remark 6.1.1), and the facts needed from that problem (stationary policies suffice, and the value is the smallest superharmonic vector) are theorems about contracting MDPs, not consequences of the LP. Second, Theorem 6.2.2 rests on Shapley's existence theorem, which is not a linear-programming fact: its usual proof is a fixed-point argument for the Shapley operator built from one-stage matrix games. Remark 6.2.2 indicates a route that avoids it, through the bounded polytope of state-action frequencies of a contracting MDP. Either way, LP duality alone does not give optimality against non-stationary opponents.
Fin N with . Actions live in finite types α, β, and , are nonempty Finsets. Rows are substochastic.tsum of the period rewards, which converges absolutely under Assumption 6.2.1, and every theorem assumes it.Restricting either player's policy class to stationary policies would make the optimality claims of Theorems 6.2.1 and 6.2.3 a statement about a finite family and is ruled out: the comparison class is all history-dependent randomized policies.
Lemma 6.1.1 is Mathlib's isSaddlePointOn_value (Mathlib/Order/SaddlePoint.lean) and is not restated. The LP duality theorems of Chapter 1 are proved on the platform (LinearOptimization.lp_strong_duality, lp_complementary_slackness) and may be used. Useful contributions include: the reduction of Remark 6.1.1 (a fixed stationary opponent gives an MDP), the contracting-MDP facts it needs, and a proof of Theorem 6.2.1. The model definitions are reusable for any finite stochastic game.
A Markov decision model describes a system that repeatedly occupies a state, receives a reward when an action is chosen, and then moves according to action-dependent probabilities. Termination may occur after any action. In a model with signed rewards, a policy that continues indefinitely can have a different total-reward behavior from one that eventually leaves the active states. Section 3.3 of Kallenberg's 1983 monograph therefore asks for the best policy within the transient class. The restriction occurs naturally in stopping problems: a decision maker may continue for a while, but the expected number of visits to each active state must remain finite.
The chapter relates that policy problem to a finite linear program. The central question is stronger than finding a policy with a large average over initial states. It asks for one policy that is optimal from every initial state among all transient policies, including policies that randomize and use the entire observed history. Kallenberg's Theorem 3.3.5 says that an extreme optimal point of the program identifies such a policy, and that the policy can be pure and stationary. Theorem 3.3.5, p. 57.
Let be a nonempty finite state set. Each state has a finite nonempty set of available actions. If action is selected, the system earns the real reward and then moves to with probability . The row sum is at most one; any missing mass represents termination. Action sets can differ across states. These are the conventions of Section 2.2, pp. 19–20.
A policy selects an action distribution at each decision epoch. It may depend on the entire state-action history. A Markov policy depends only on time and the current state; a stationary policy uses the same state-dependent distribution at every time; a pure stationary policy selects one action in each state. These four classes are denoted , , , and . The first decision occurs at time in the book.
Write for the chance of being in state and choosing action at time , given initial state . A policy is transient if the expected number of visits to each state is finite from every initial state:
For such a policy, its expected total reward is finite. Section 3.3 assumes that at least one transient policy exists. Its transient value is , which can still be infinite as the policy varies. Section 2.2, pp. 21–23; §3.3, pp. 49–50.
Fix positive weights . The linear program (3.3.7) maximizes over nonnegative state-action arrays satisfying the flow equations
Its feasible set is . A transient stationary rule has an occupation vector , where is the -weighted expected number of visits to state-action pair . Theorem 3.3.3 identifies transient stationary rules bijectively with and identifies extreme points with pure rules. Theorem 3.3.4 compares the occupation sets of all four policy classes: , where the bar means closed convex hull. Theorems 3.3.3–3.3.4, pp. 54–55.
The goal is Theorem 3.3.5, p. 57. If is an extreme optimal solution of that program and is the action with , then the pure stationary policy is transient and
A stronger companion statement is Theorem 3.3.6, p. 58: under the correspondence of Theorem 3.3.3, a stationary policy is optimal transient exactly when its occupation vector is optimal for (3.3.7), in the two directions printed on the page. The milestone list follows the chapter's numbered results on the finite-value Bellman equation, the smallest superharmonic vector, the stationary-policy/LP correspondence, the four occupation sets, and the preservation of optimality. The goal itself does not assume that is finite; the existence of an extreme LP optimum is its stated premise.
An LP optimum is a vector of occupation amounts, not an implementable policy by itself. Theorem 3.3.5 converts an extreme optimum into an action choice at each state. It also upgrades a scalar objective weighted by to simultaneous optimality of the resulting policy from every initial state. This is the bridge between the finite optimization problem and the original control problem. The scope is specifically transient optimality: Example 3.3.4, p. 58 gives a policy outside that comparison class with larger total reward.
The result is proved in the book. The work here is to give its model, occupation map, linear program, and numbered supporting statements precise Lean interfaces that can later receive machine-checked proofs. The reusable parts include finite substochastic MDP data, history-dependent policy semantics, transient visit sums, and state-action occupation vectors. The theorem proofs are open in this proposal.
Optimizing a weighted sum of rewards is not, by itself, the same as optimizing every state's reward. The linear program also describes flows of expected visits, while the theorem talks about actual policies and all initial states. A solver must account for both links without assuming that all policies are stationary. The geometry of an extreme feasible point matters because the theorem selects an action from each state using a positive coordinate. Existence of a transient policy does not by itself bound the supremum of transient rewards; Example 3.3.1, p. 50 makes that distinction explicit.
Lean uses Fin N with for states and a finite action type with a state-dependent finite nonempty available-action set. Only available state-action pairs index occupation vectors and LP variables. Transition rows are substochastic, not necessarily stochastic. Rewards are real and may have either sign. A general policy is a normalized action kernel on full finite histories; its Markov, stationary, and pure stationary subclasses remain distinct. The history list is stored newest first, and Lean's time index zero corresponds to the book's time one. All state-action probabilities are finite sums over histories; transience is summability of state-visit probabilities, and occupation counts are infinite sums used under that condition.
The LP flow constraints are equalities and is strictly positive. The goal does not normalize to a probability distribution, matching (3.3.7); Theorem 3.3.4 uses the initial-distribution convention of p. 55 and hence normalizes it. Theorem 3.3.3 uses the matrix inverse only for transient stationary rules. For Theorems 3.3.1–3.3.2, nonemptiness of the transient class and boundedness above of each transient reward set make the real supremum meaningful. Theorem 3.3.5 uses neither boundedness as an extra hypothesis nor a restriction of the comparison class to stationary policies. A formalization that compares only with stationary (or Markov) policies, or that identifies the classes , , , , would make Theorems 3.3.4 and 3.3.5 much weaker or trivial, and is ruled out: the comparison class is every history-dependent randomized transient policy. Mathlib's finite sums, matrices, summability, convex hull, and extreme-point definitions provide the general library interface. Contributions establishing the policy/occupation identities and the chapter's numbered milestones are within scope.
Integer linear programming asks for the best point whose coordinates are integers, even though linear programming methods naturally search over real points. In his 1958 note, Gomory describes a systematic way to add a constraint that excludes a fractional simplex solution while retaining every nonnegative integer solution. This mission isolates that single cut and its effect on the objective value. The note announces an iterative finite algorithm, but explicitly defers a proof of finiteness to another treatment. The target here is the cut's correctness for one tableau.
The cut belongs to the history of cutting plane methods for integer programs. Related formalized objects include a Chvátal closure and intersection cuts based on lattice free sets, but their data and cut constructions differ from the row and fractional part formula in Gomory's note. The note itself contrasts its systematic row operation with earlier problem specific constraints used by Dantzig, Fulkerson, and Johnson and by Markowitz and Manne. Those comparisons explain why a reusable row formula is useful; they do not assert an identity between the different cuts.
A tableau is a finite array of real numbers . Row represents the objective variable ; rows represent . Column holds constants; columns multiply the negatives of the variables . A solution of (2) is a pair satisfying
The original integer program requires , every , and every to be nonnegative integers. The simplex solution of this tableau has and . It is a real tableau solution, whether or not any of its coordinates are integers.
Choose a row whose constant is not an integer. For each coefficient let be the greatest integer at most that coefficient, and let be its fractional part. Equation (3) defines a new variable
The augmented system (2)* adds this equation to the tableau. Feasibility now also requires ; an integer solution additionally requires . For example, the one row relation admits the integer solution , and its cut value is . At the simplex point , the same cut value is .
The main target combines exclusion of the simplex solution, exact correspondence of nonnegative integer solutions, and equality of their attained objective values. Writing and for the two sets of nonnegative integer solutions, the correspondence is
Every member of has the displayed cut value for , and the projection that drops leaves unchanged. Consequently a real is the greatest attained value for (2) exactly when it is the greatest attained value for (2*). The statement does not assume either set has a maximum.
The milestones follow the paragraphs on page 277: projection of feasible solutions, the impossibility of integer solutions when the selected row has a fractional constant but only integral other coefficients, exclusion of the simplex point, the identity proving integral, and its nonnegativity on integer solutions. These are the claims the note uses to pass from the cut formula to the correspondence and the objective statement.
The result certifies that equation (3) removes the current fractional simplex point while retaining every integer candidate and its objective value. It is the local correctness condition needed before one can safely reoptimize an integer program after adding this constraint. The note's argument is a mathematical result about one tableau, independent of whether the subsequent sequence of pivots terminates.
This mission supplies a machine checkable interface for the tableau, the fractional cut, and the projection between their integer feasible sets. The theorem statements are drafted and compile with open proofs; this mission does not claim that the paper's result already has a machine checked proof here. A completed proof would make the one cut result available for later developments about iterations, optimization, or stronger cut families.
The cut value is visibly at least when the nonbasic variables are nonnegative, but that inequality alone does not give : the right side is negative for the chosen row. The key additional statement is that the real expression for is an integer on an integer tableau solution. Formalization must preserve both facts while using the same sign convention for the tableau and the cut. Merely defining the augmented solution as a pair together with its computed cut value would make the correspondence automatic and would omit the new variable's integrality and nonnegativity requirements.
Lean uses real valued tableau coefficients and real valued variables with a separate predicate for being an integer. This lets the fractional simplex point and integer feasible points inhabit the same space. The row and column sets are finite, including the cases and ; row is , column is the constant column, and Lean's Fin n index denotes the paper's . The selected row can be row in Lean. Gomory chooses a constraint row, but the local cut argument needs only the selected row's variable to be integral, and is integral in the stated problem. Every variable, including and the added , is required to be nonnegative and integral in an integer solution.
The fractional part uses the greatest integer at most a real number, including negative coefficients. The objective comparison uses greatest elements of the sets of attained values, so empty and unbounded sets receive no artificial supremum. Nonnegative constants and objective row coefficients are features of the simplex setting, but the five local claims and goal remain valid without those extra hypotheses. The paper's loose phrases “cuts off,” “one-one correspondence,” and “can be replaced” are represented by infeasibility of the augmented simplex point, a unique extension and projection preserving , and equivalence of greatest attained values, respectively.
The mission does not formalize the derivation of (2) from (1) by simplex pivots, dual simplex reoptimization, finiteness of repeated cutting, the equation bound and deletion of re-entering variables, the suggested choice of largest fractional part, or the reported E101 runs. These concern an iterative process the note does not define fully, or empirical observations. Reusable contributions include a verified fractional part identity, the integer extension theorem, and solution set correspondence for a real tableau.
Finite Markov decision models are often described by policies that choose an action from the current state. The admissible class in a total reward problem is wider: a randomized decision may use the complete history of observed states and chosen actions. For an undiscounted infinite horizon, the expected number of visits to a state may be infinite, and the total reward may be an extended real number. It matters whether a test carried out on finitely many pure stationary policies really controls this wider class. Kallenberg's Section 3.2 answers that question for finite models whose transition rows may lose probability mass when the process terminates.
The chapter is part of a 1983 account of linear programming methods for finite Markovian control. Its Theorem 3.2.4 collects earlier characterizations of transience and relates them to a finite linear program. The historical attribution in Kallenberg's Remark 3.2.2 is precise: Veinott (1969) established the equivalence of the first three conditions for nonrandomized policies, Hordijk (1976, course notes) extended the first four to general policies, and Denardo and Rothblum (1979) established the link between pure stationary transience and the LP condition. The mission targets Kallenberg's combined five-way statement, rather than treating those partial precedents as separate conclusions. Kallenberg, pp. 42–43.
Let be a finite nonempty state space of size . For every state , let be a nonempty finite set of actions. Choosing gives the transition number to state , with . The missing mass is the probability that the system terminates before another decision epoch. This is a substochastic model; replacing the inequality by equality would change the question. Kallenberg, §2.2.
A policy specifies, at each epoch , a probability distribution on after the full history . It may be randomized and may depend on all preceding states and actions. A memoryless policy depends only on the epoch and current state. A pure stationary policy chooses a single admissible action in state at every epoch. Write for the probability of state at epoch from initial state . The policy is transient when for every pair . Kallenberg, pp. 20–23.
The finite-horizon survival recursion starts from and sets for . A model is contracting if there is a strictly positive vector and a scalar for which for every admissible . These objects are determined by the transition system; rewards do not enter the five-way characterization. Kallenberg, p. 23 and pp. 41–43.
For any fixed , Theorem 3.2.4 states the equivalence of: transience of every pure stationary policy; transience of every policy; ; contraction; and existence of a finite solution of
“Finite solution” means an attained finite optimum. The are arbitrary positive right-hand sides, not a choice that the theorem is allowed to make after seeing the model. The state count is the exponent in , and the inequality is strict. Kallenberg, Theorem 3.2.4, pp. 42–43.
The milestones follow the results the chapter uses on the way to Theorem 3.2.4, in attack order:
Assumption 3.2.1 says that every policy's expected total reward exists in ; it is a hypothesis of items 2–4 only. Kallenberg, pp. 32–33, 37–42.
The theorem gives four finite or structured ways to recognize a property quantified over all policies. The survival condition uses only recursion steps, and the contraction condition supplies a weighted geometric bound on continuation. The LP links the same property to a finite-dimensional optimization problem. Each characterization can serve a different later argument without assuming the policy class has been reduced to stationary rules. Kallenberg, Theorem 3.2.4.
The five-way theorem and its supporting results are proved in the book; this mission asks for machine-checked proofs of their stated finite-model versions. The Derman–Strauch policy result is quoted by Kallenberg without proof, so its formal proof is a separate substantial contribution. None of these results has a machine-checked proof yet. The general history and occupancy definitions can be reused by later total-reward and constrained-control missions.
Checking only the finitely many pure stationary transition matrices does not directly bound the occupation counts of a history-dependent policy. Such a policy can change its action distribution after each observed path, and it need not be a mixture of stationary policies chosen once at the start. Likewise, is a finite-horizon bound, whereas transience is a statement about an infinite series of visit probabilities. The main difficulty is connecting these different quantifiers without changing the policy class. The LP condition adds a second boundary: its constraints use , and finite value includes attainment. Kallenberg, pp. 41–45.
States are Fin N with , and actions form one finite ambient type with a nonempty admissible subset at each state. Transitions are real nonnegative numbers with row sums at most one. Epoch is Lean index zero. A history records states and earlier actions; policy decision rules are normalized and supported on the current state's admissible actions. Occupancies are finite sums of transition products, so the definition of transience is summability of a nonnegative real sequence, not a bound on an individual term.
The reward layer is separate from the transition system. It uses extended real limits under Assumption 3.2.1, while the five-way goal needs no reward hypothesis. Sums of extended reals are only asserted for p-summable , where no and meet with positive coefficients; the convention is the book's. The LP objective and constraints range only over admissible state-action pairs. Its finite-solution predicate includes a feasible optimizer. Contraction allows an arbitrary componentwise positive weight and requires ; it does not normalize to the all-ones vector. The -step test uses the cardinality of the original state space.
All-policy transience means every history-dependent randomized policy. Restricting that quantifier to Markov or stationary policies would remove the central content of the theorem. Useful contributions include finite-history probability identities, the Derman–Strauch occupancy theorem, the maximal-survival recursion, the stationary total-optimality result, and the finite LP characterization. The occupancy and policy definitions are reusable beyond this mission.
Finite Markov decision models describe repeated choices whose consequences depend on the present state. They are used when a planner needs one rule that works from every starting state, yet the rule may in principle respond to the entire observed history. Linear programming offers a different description: it records how often each state and action are used, without representing the order of decisions. Kallenberg's account connects these two descriptions for a contracting total-reward model, in which the system may terminate after a transition and all policies have finite expected occupation counts (Kallenberg 1983, §§2.2 and 3.4).
The question is whether the frequency vectors attainable by general randomized policies are already attainable through the simpler stationary classes. This matters for constrained planning: restrictions on expected total resource use are linear in frequencies, while a direct search over every history-dependent policy has no comparable finite parameterization. Kallenberg's Theorem 3.4.8 makes the exact comparison, including initial distributions that assign zero probability to some states (Kallenberg 1983, pp. 72–74).
Let be a nonempty finite set of states. Each has a nonempty finite action set . Taking earns a real reward and moves to with probability . A row may sum to less than one; the missing probability is termination. A policy specifies a probability distribution over after every finite history ending in . A Markov policy uses only time and current state, a stationary policy uses only current state, and a pure stationary policy chooses a single action in each state. These are the classes , , , and of §2.2 (Kallenberg 1983, pp. 19–21).
The standing contraction assumption supplies weights and with
It is weaker in form than fixing a common discount factor: the weights may differ across states. The assumption makes every policy transient, so expected total rewards and state-action frequencies are finite (Kallenberg 1983, Assumption 3.4.1 and Theorem 3.2.4).
For an initial probability distribution , with and , write for the expected total number of visits to state at which action is chosen, averaged over the initial state. Let , , , and collect these frequency vectors for the four policy classes. The frequency polytope consists of nonnegative vectors satisfying conservation of expected flow at each state:
These equalities are those of the dual linear program (3.3.7), and the set names follow Notation 3.3.1 (Kallenberg 1983, pp. 53–55).
The first milestones identify the total-reward value vector as the smallest TMD-superharmonic vector, establish a bijection between stationary policies and feasible frequencies when every , and show that an optimal linear-programming solution yields a pure stationary policy optimal from every state (Kallenberg 1983, Theorems 3.4.1–3.4.3).
The mission goal allows zero entries in the initial distribution and compares all four policy classes:
The overbar is Kallenberg's notation for the closed convex hull, rather than topological closure alone. Since there are finitely many pure stationary policies, is finite and its convex hull is already closed (Kallenberg 1983, Definition 1.2.1(i) and Theorem 3.4.8).
The goal says that the finite LP flow constraints characterize exactly the frequencies of arbitrary history-dependent randomized policies. It also says that every such vector is a convex combination of frequencies from pure stationary policies. A resource-constrained objective that depends linearly on expected state-action use can therefore be expressed over without losing feasible frequency vectors. Kallenberg states this constrained consequence in Theorem 3.4.9; that theorem is beyond this mission's selected milestones (Kallenberg 1983, pp. 73–74).
The results are proved in the book. The remaining work here is a machine-checked development of their definitions and proofs, including the passage from arbitrary histories to finite flow equations. The history and frequency interfaces can also be reused for other finite, terminating control models. A proof of the goal would make explicit which uses of contraction and finite action sets justify the infinite sums and the closed convex hull.
For a stationary policy, the frequency equation can be written with a finite transition matrix. A general policy has a separate decision distribution after each possible history, so there is no single stationary transition matrix to substitute into that formula. A direct identification of with therefore skips the main issue. Moreover, the stationary-policy correspondence is one-to-one only when every initial weight is positive. When , different rules at never-visited states may have identical frequencies; the set equality must survive this loss of injectivity (Kallenberg 1983, Theorem 3.4.2 and Remark 3.4.3).
States and their action sets are finite and nonempty. Actions are indexed by their state, so an illegal state-action pair cannot occur. Transition rows are substochastic; rewards, values, and frequencies are real. Histories contain the past state-action pairs and current state, and time index represents the book's period . The four frequency sets range over genuinely different policy classes. In particular, the general set permits every legal history-dependent randomized policy; defining it through stationary policies would erase the goal's content.
The initial distribution in the goal may have zero coordinates. The strictly positive weights in the bijection and LP-optimality milestones are the different convention of §3.3. Frequencies and rewards use infinite sums; contraction supplies their convergence. The value vector is a coordinatewise supremum over legal policies, bounded under contraction. The LP uses equalities, not relaxed inequalities, and the pure-policy set is convexified only in the goal's first equality. Needed infrastructure includes finite history probabilities, stationary transition matrices, inverse stationary flows, superharmonic vectors, and finite-dimensional convex geometry. Contributions that establish these interfaces and the three stated milestones are in scope.
Multi-level programs model a hierarchy of decision makers: a leader commits to a decision, a follower optimises given it, a follower of the follower optimises given both, and so on. Bilevel programs are the standard model of Stackelberg competition, toll setting, network interdiction and many other leader–follower problems in operations research (Candler and Townsley 1982; Bard and Falk 1982). When every level has a linear criterion and the constraints are linear, each player's problem looks like a linear program, and it is natural to hope that the whole hierarchy is solvable in polynomial time.
R. G. Jeroslow's 1985 paper (Math. Programming 32, 146–164) shows that this hope fails at every level of the polynomial hierarchy: a -level linear program with fixed criteria can encode the truth of a quantified Boolean sentence. The result places multi-level linear programming in the polynomial hierarchy and is widely cited for the -hardness of such programs; NP-hardness of bilevel linear programs (Corollary 4.6) is its special case .
A multi-level program has real variables , a feasible set (a polyhedron in the linear case), and players who move in that order; player controls and minimises a fixed linear criterion . The solution sets are defined from the last mover upwards: is the set of at which player 1's criterion is minimal given the choices of all earlier movers, and in general keeps the points of minimising among the points of that agree with on . The value is on , when . The sets can be empty even when is a nonempty polytope: the paper's four-level Example has because is not closed.
A propositional formula over blocks of atoms (block has atoms) is encoded by the linear system : one variable per non-atomic subformula, with the inequalities (3.1a)–(3.1c) for , , . The quantifier of block is when is even, so
is a sentence.
The game adds a bookkeeper, player , who moves last. Player controls the atoms of , and player also controls auxiliary variables ; the bookkeeper controls the , a variable fixed to , and auxiliary variables . Two gadgets, (4.1) and (4.6), let the bookkeeper and player 1 turn the linear criteria into the piecewise-linear functions (or for universal ) and , where is the length of , , and at , otherwise.
Let be the set of optimal solutions of . Then ; at every optimum all atom variables and all are binary; and
Moreover, when (3.3) holds, is player 's block in some optimum iff is binary and the sentence (4.17) holds at the truth valuation of .
In attack order: Lemma 3.1 (correctness of on binary inputs); Lemma 4.1 (robustness of near binary inputs); Lemmas 4.2 and 4.3 (the bottom two levels of a bounded linear multi-level program are solvable, via LP duality); the bookkeeper identities and in ; (4.2) and (4.3) (player 1's and player 's responses on the gadgets); Lemma 4.4 (the induction on with the higher blocks fixed). Companion theorems: Corollary 4.6 (the bilevel case: value iff ), the §2 Example, and Proposition 3.2 (the pure binary game ).
The theorem shows that deciding the value of a -level linear program with fixed criteria is at least as hard as deciding sentences, so known exact algorithms for multi-level linear programs cannot be expected to run in polynomial time once , and even recognising an optimal move is -hard. The bilevel case is an early NP-hardness proof for bilevel linear programming, and the construction (a bookkeeper player and absolute-value gadgets that force binary choices) is a template for hardness reductions to leader–follower problems.
The result is proved in the paper but, to our knowledge, has no machine-checked formalization. A formal development makes precise the solution concept (conditional rather than lexicographic minimisation), which the literature states in several inequivalent ways, and checks a proof whose printed version leaves cases to the reader (the , cases of Lemma 4.1, the universal cases of Lemma 4.4) and applies Lemma 4.3 to a feasible set that is unbounded (the (4.1) variable has no upper bound).
The obvious argument, "each existential player picks a satisfying assignment and each universal player a counterexample", works for the pure binary game (Proposition 3.2) but not for continuous variables: a player may choose fractional values, and the solution sets of a multi-level program need not exist (the §2 Example). The work is in showing that every player is forced to binary choices. Player 1's fractional choices are ruled out only through the robustness estimate of Lemma 4.1 with the weight , and the existence of optimal solutions at every level has to be established along the induction, since it fails for general three-level programs.
k : Fin p is the paper's , owned by player in .solSet encodes the conditional minimisation of (3.7), p. 152. HasValue N w requires ; the value is not modelled.A complete development needs a linear-programming duality argument for Lemma 4.2 (Mathlib has IsExtreme and Set.extremePoints; LP duality is on the platform as a single-level theorem) and an induction over the levels of the game. The definitions MultilevelProgram, solSet and the formula encoding LSys are reusable for other complexity results on hierarchical optimisation. Proofs of any milestone, including the generic Lemmas 4.2–4.3 and the formula Lemmas 3.1 and 4.1, are welcome independently.
Reliability theory classifies life distributions by how they age. A device whose failure rate tends to increase over time is "wearing out", and the class of distributions with increasing hazard rate average (IHRA) is the one that is closed under forming coherent systems of independent components (Birnbaum, Esary and Marshall, 1966). This makes IHRA the natural ageing class for systems. It also raises a question: which physical failure mechanisms produce IHRA lives?
Esary, Marshall and Proschan's paper Shock Models and Wear Processes (Ann. Probability 1, 1973) answers this for two kinds of mechanism. In the first, damage arrives in discrete amounts at the epochs of a Poisson process of shocks. In the second, damage accumulates continuously. In both, the device fails when the accumulated damage first exceeds a fixed capacity. This mission covers the second kind: a wear process and its first passage time above a level. The paper shows that the first passage time is IHRA under three qualitative conditions: wear starts at zero and only grows, the process is Markov, and accumulated wear and age make further wear more likely. Nothing else is assumed about the law of the wear.
A short timeline. Birnbaum, Esary and Marshall (1966) introduced the IHRA class and proved it is closed under coherent systems. Morey (1965) studied first passage times of wear processes under an extra monotonicity assumption. Esary, Marshall and Proschan (1973), §4, proved the IHRA property first for Poisson shocks with i.i.d. damages (Corollary 4.2, (4.7)), then for dependent damages (Lemma 4.1b, (4.7b)), and finally for continuous wear (Theorem 4.10).
Let be a probability space. "Decreasing" means non-increasing throughout.
A survival function is IHRA if is decreasing on (p. 631). For an exponential life, is constant. IHRA says the average failure rate over never decreases.
Dependent damages. Let be nonnegative random variables, the damages caused by successive shocks, and let and . The paper's conditions (p. 636) are:
Wear process. is the wear accumulated in . The conditions (pp. 640–641) are:
The first passage time above a level is . Its survival function is , and is the distribution function of the wear at time .
If satisfies (4.8), (4.9) and (4.10), then for every level
that is, has an IHRA distribution.
An optional extra item states Corollary 4.2 (4.7b): Poisson shocks of rate with damages satisfying (4.3)–(4.5) give an IHRA life .
The result. Theorem 4.10 derives an ageing property of a failure time from qualitative properties of the damage process alone: no distributional form, no stationarity and no independence of increments is assumed. Together with the closure of IHRA under coherent systems, this lets a reliability engineer conclude that a system built from components failing by wear has an IHRA life. Examples include processes with nonnegative stationary independent increments started at the origin, such as compound Poisson processes and infinitesimal renewal processes (p. 641). Lemma 4.1b is the discrete analogue: a sequence of probabilities with decreasing is what Theorem 3.1 (3.4) needs to give an IHRA life under Poisson shocks.
Formalizing it. The results are proved in the paper. As far as we know none of them has been machine-checked. The formalization needs, and would make reusable, a statement of the Markov property for a continuous-time real process in terms of Mathlib's conditional expectation, versions of conditional distributions with monotonicity constraints, and the passage from a discrete-time grid to continuous time for first passage times. Each of these is a step a probabilist writes in one line and a proof assistant does not.
The paper's proof is short, but every sentence hides a measure-theoretic step. The first claim, that the grid increments satisfy (4.3)–(4.5), requires turning the Markov property and the monotonicity of the increment law into conditional laws of given . Those conditional laws are defined only almost everywhere, and the monotonicity must be preserved along the way. Lemma 4.1b itself is an induction that integrates the monotonicity conditions against the law of . The extension from rational to arbitrary ratios uses the monotonicity of paths. The identification of as a right limit of needs the pathwise reading of (4.8). The natural first idea, approximating by a compound Poisson process, would add hypotheses the theorem does not have.
All objects sit in the namespace ShockWear.WearProcess, in one definition file. The committed conventions:
pr with IsProbabilityMeasure. Time is ; with every measurable.condDistrib. The monotonicity conditions (4.4), (4.5), (4.10) are imposed on these versions, on the paper's regions , . "Is decreasing in " is read as "has a version decreasing in ".X i is the paper's , and the kernel κ k describes given .Trivializing formalizations are ruled out: (4.9) and (4.10) are not replaced by independence or stationarity of increments, nor by a compound Poisson model. Those are examples (p. 641), not hypotheses. Monotonicity is never imposed on Mathlib's condDistrib itself, whose values off the support of are unconstrained. A sorry-free local check confirms the hypotheses are satisfiable: the deterministic process satisfies (4.8)–(4.10), and constant damages satisfy (4.3)–(4.5).
Contributions are welcome on any milestone. The reduction (milestone 2) and the induction of Lemma 4.1b are the substantial parts. Lemmas about versions of conditional distributions under Markov processes would be reusable well beyond this mission.
A Markov decision chain is a controlled Markov chain: in each state the controller picks an action, collects a reward and moves to a random next state with probabilities that depend on the state and the action. Under the average reward criterion, the long-run reward per step, an optimal policy can be computed by linear programming. For chains in which every stationary policy has a single recurrent class (the unichain case) this goes back to Manne (1960), de Ghellinck (1960) and d'Epenoux (1960): the variables of the dual linear program are long-run state–action frequencies, and the vertices of its feasible set are exactly the pure stationary policies.
In the general multichain case a policy may split the state space into several recurrent classes with transient states between them, and the frequency picture breaks down. Denardo and Fox (1968) and Denardo (1970) gave linear programs that require solving several programs in sequence. Hordijk and Kallenberg (Management Science 25(4), 1979) showed that one pair of dual linear programs suffices: from an optimal dual solution one reads off an average optimal policy (their Theorems 7 and 8). To make the correspondence between policies and dual solutions explicit, they attach to every stationary policy a representative, a particular feasible solution of the dual program, and prove (Theorem 10) that the representative of a pure stationary policy is a vertex of the feasible set. This mission formalizes Theorem 10.
Timeline:
The state space is finite. Each state has a finite nonempty set of actions; action in state earns and moves to with probability , . Fix weights with .
The dual linear program has one pair of variables for each state and each admissible action . Its feasible set consists of the with
A pure stationary policy uses the action whenever the chain is in state . Its transition matrix is . For a stochastic matrix , the limit matrix exists, and the deviation matrix is . A state is recurrent if every state reachable from it can reach it back, and transient otherwise; the set collects the transient states, and the states reachable from a recurrent state form an ergodic set. Write for the ergodic sets of .
The representative of is
with for and, for , . The paper defines the same formulas for randomized stationary policies , with in place of .
for every finite Markov decision chain, every positive probability vector and every pure stationary policy . The statement contains feasibility of the representative.
Theorem 10 is the vertex half of the policy–solution correspondence of Hordijk and Kallenberg: every pure stationary policy appears as a basic feasible solution of one linear program, in the multichain case and without any communication assumption. It connects the simplex method on that program with the set of pure policies, and it is a building block for the later literature on linear programming for multichain Markov decision problems. The paper also records that the converse fails: an extreme point may induce a randomized policy.
The result is proved in the paper. As far as is known it has not been machine-checked. A formal proof also checks the exact form of : the paper prints the denominator of as , a sum over all states, and with that reading the representative is not feasible as soon as transient states feed an ergodic set (two states, : ). The denominator is the one the paper's own feasibility computation on p. 360 uses, and it is the one stated here.
Feasibility is a calculation with the identities and . Extremality is the substance. Restricted to the pairs , the constraints become the square system (7) in the state variables, and system (7) determines and the transient part of , but on each ergodic set it determines only up to adding a multiple of the stationary distribution of that class: the matrix is singular, with one degree of freedom per ergodic set. The naive argument, that the equality constraints alone pin the point down, therefore fails as soon as there is an ergodic set; the extra information has to come from the nonnegativity constraints, and that is why the exact value of matters. In the general multichain setting this requires the class structure of a finite Markov chain (closed classes, transient states, the support of , uniqueness of invariant vectors on a closed communicating class), little of which is in Mathlib in usable form.
MarkovDecisionProcesses.StationaryMDP: finite states, finite actions, admissible sets (nonempty), transition probabilities nonnegative with unit row sums. and are the published limitMatrix and deviationMatrix of Blackwell's Lemma 1, whose identities are the open platform theorems BlackwellDiscreteDP.NearOne.lemma_1a and lemma_1d.Set.extremePoints ℝ. Membership in it includes feasibility.vecMul. Recurrence and accessibility are the published IsRecurrent and Accessible; the ergodic set of a recurrent is the set of states accessible from . The maximum in is a Finset.sup' over that finite nonempty set.Little's law says that the long-run average number of customers in a system equals the arrival rate times the average time a customer spends there. It is one of the most used identities in queueing theory, and it holds on individual sample paths under weak conditions (Little 1961; Stidham 1974). Many quantities of interest are not head counts, however: the work in the system, the cost accumulated by customers in progress, the number of tokens a customer holds in some state. For these a more general relation is needed, between a time average and a customer average , of the form .
Heyman and Stidham (Oper. Res. 28 (1980)) prove such a relation on each sample path, for an arbitrary real-valued function attached to each customer, under a support condition that is much weaker than the continuous-sojourn assumption of the theorem. They then show by a counterexample that the support condition cannot simply be dropped, even when every customer function is an indicator.
Timeline.
Fix one sample path. Customers arrive at epochs ; ties are allowed. The arrival count is the number of with , and the arrival rate is when the limit exists.
Customer carries a real-valued function on . Its total is , and the rate is . The customer average and time average are
When is the indicator of , is the sojourn time and is the number in system, so is .
The ASSUMPTION of the paper is that for each there is with
For signed write , , and let , , , be the corresponding totals, rates and averages.
Assume (i), (ii) and (v) for every . If , and exist with and , then exists, equals , exists, and
The result. converts between a time average, which is what a system designer measures, and a customer average, which is what a customer experiences. Applied to different it yields , the relation between average work in system and average customer work, and relations between time-stationary and embedded-chain probabilities; §2 of the paper derives the GI/M/c/K relation this way. Because the support condition (i)–(ii) allows a customer's contribution to be interrupted (leaving and re-entering the system), it covers preemptive priority queues and nodes of networks, which the continuous-sojourn theorem does not. The counterexample marks the boundary: with interrupted sojourns, indicator functions and finite , alone do not suffice.
Formalizing it. The result is proved on paper, with two steps delegated to earlier work "by mimicking" Lemma 1 and Theorem 2 of Stidham 1974. The indicator special case (with strictly increasing arrivals) is already proved on Prove2Me as queueing_general_littles_law (wenxinzhang). This mission asks for the general, signed, pathwise statement and its proof steps, a counterexample with an exactly computed time average , and the ensemble corollary.
The obvious argument, exchanging the time integral of with the sum over customers, gives , but a customer that has arrived by may contribute only part of its total by . The sandwich only bounds this loss; the hard step is showing that and have the same limit, which needs to compare at time with at a slightly earlier time. Without (ii) this fails, as the counterexample shows: customers there remain "open" for a window proportional to their index.
For signed the sandwich is not available directly, and the proof splits into positive and negative parts; the exchange of sum and integral then needs the finiteness of the parts on every .
All statements except Corollary 3 are about one fixed sample path; the paper's "with probability one" is the pathwise statement applied to almost every path, and Corollary 3 states this explicitly with a probability measure and almost-sure hypotheses.
Conventions:
Monotone with ; ties are allowed.Added hypotheses: milestones (3), the identity and (6) assume , which the paper derives from (2); Corollary 3 assumes is integrable, which its definition of the ensemble average presupposes.
A formalization in which sums only over arrived customers, or in which a non-integrable or has integral , would make the statements trivial or different; the definitions rule this out by summing over all customers and requiring integrability.
Needed infrastructure: Cesàro averages and counting functions of nondecreasing sequences, interchange of countable sums and integrals for locally finite families, and harmonic sums . The counting-function lemma (2) and the squeeze for and are reusable well beyond this mission. Proofs of any milestone are welcome independently.
Iterative methods for a system of linear inequalities stop at a vector that only almost satisfies the system: the violation is small but not zero. A user then needs to know that is close to an actual solution. Hoffman's 1952 paper (J. Res. Nat. Bur. Standards 49) gives the first quantitative form of this fact: the distance from to the solution set is at most a fixed multiple of the violation. The paper itself names one application: in Brown's method for solving games, the computed strategy vector approaches the set of optimal strategy vectors.
The result is now known as Hoffman's error bound and the constant as the Hoffman constant. It is a standard tool in convergence analysis, sensitivity analysis of linear programs, and the theory of error bounds.
Timeline.
Let be a real matrix with rows and let . The system (1) is for , briefly ; its solution set is , and the system is consistent if . The th half space is .
For a real number , if and otherwise; for a vector, is taken coordinatewise. So records by how much violates each inequality.
Hoffman measures sizes with a positive homogeneous function on : a continuous real function with (i) and only for , and (ii) for . Norms are examples, but need not be symmetric, subadditive or convex.
For a set of rows, is the matrix obtained from by replacing the rows outside by , and keeps the coordinates of in and zeroes the others. "Nearest" always refers to Euclidean distance. The set consists of the points outside the cone whose nearest point in that cone is the origin; is the cone spanned by the rows of with the origin removed.
Section 3 uses three norms: (largest absolute coordinate), (sum of absolute coordinates) and the Euclidean norm. With , is the largest absolute coordinate of a row in , and over probability vectors on , the value of the matrix game .
If is consistent and , are positive homogeneous, there is such that for every some solution satisfies
The constant is existential and fixed before ; no value is asserted. This is the weakest statement that carries the content and survives any later improvement of the constant.
Each is stated as in the theorem: for every there is a solution with the bound.
The result. The theorem converts a residual estimate into a distance estimate. Any scheme that drives to zero brings its iterates to the solution set at a linear rate in the residual. Linear convergence proofs for projection and first-order methods on polyhedral problems and stability results for LP solution sets build on it. Formulas (8)–(10) show that in the max and sum norms the constant can be read off the rows of through a matrix game.
Formalizing it. The theorem has been proved since 1952, and later papers give several alternative proofs. The mission formalizes Hoffman's own proof route, Lemmas 1–4, in Lean and Mathlib, and the explicit constants (8)–(10). Mathlib has Farkas-type results and projections onto closed convex sets in inner product spaces, but no error bound for linear inequality systems, and the Prove2Me library has no statement of Hoffman's theorem.
For a single , a bound is trivial: take the nearest solution and choose accordingly. The whole content is that one works for all , including far from and approaching along every direction. A compactness argument on alone fails, because the ratio is not a continuous function of on a compact set: the nearest solution and the set of active constraints jump as moves. Lemma 3 needs a positive lower bound on a set that is not obviously closed away from the origin; its closedness comes from Lemma 4, i.e. from Farkas' lemma. Since , are not norms, no argument using the triangle inequality or symmetry is available. For (8), a set can arise in Lemma 2 with (e.g. , in with ), contrary to an unnumbered remark on p. 265; the bound (8) is still true, but that remark cannot be used.
Fin k → ℝ, is Matrix (Fin m) (Fin n) ℝ, the system is A *ᵥ x ≤ b (componentwise), and is posPartVec y = fun i => max (y i) 0.IsPosHomogeneous (continuity, nonnegativity, vanishing exactly at , positive homogeneity); they are never specialised to norms in the goal or Lemmas 1, 3.dist on Fin n → ℝ is the sup distance and is not used.) Lemmas 2 and 3 take "a nearest point" as hypothesis; since the Euclidean nearest point of a closed convex set is unique, this is the page's "the nearest point".Finset (Fin m) of row indices; keeps all rows, with zero rows outside .⨆ i, |x i| and is ∑ i, |x i|; minima and maxima over finite index sets are ⨅/⨆ in ℝ, equal to the attained min/max on nonempty sets. is defined directly by (7) as a min over the simplex of a max, for nonempty , so no minimax theorem is needed. In (8), is the maximum over nonempty with and is when there is none (only when ). In , the page's summation range "" is read as ranging over the rows, since is indexed by rows.The quantifier order is part of the statement: a version with chosen after is trivially true and is not this theorem; likewise precedes and in Lemma 1 and precedes in Lemma 3.
Infrastructure a complete development needs: existence and the variational characterisation of the Euclidean projection onto a polyhedron in Fin n → ℝ; Farkas' lemma in cone form (published as LinearOptimization.farkas_cone_corollary); compactness of level sets of positive homogeneous functions. The projection and polyhedral-cone lemmas are reusable well beyond this mission. Proofs of any milestone, alternative proofs of the goal, and sharper or equivalent forms of the constants are welcome.
The restricted shortest path problem asks for a shortest route between two points of a network subject to a budget on a second additive quantity, such as travel time, cost or risk. It appears as the pricing subproblem of column generation for crew scheduling and vehicle routing, in quality-of-service routing in communication networks, and in scheduling, where Hassin's own §7 uses it for a single-machine problem. The problem is NP-hard (Garey and Johnson, 1979), so exact polynomial algorithms are not expected, and the natural question is how well it can be approximated in polynomial time.
Timeline.
Hassin's combination of an approximate decision test with a geometric search on the bounds is the pattern later schemes for resource-constrained path problems refine, which is why his first scheme is the subject of this mission.
A directed graph has vertex set , , and edge set . Following the paper, the vertices are numbered so that every edge has ; in particular the graph is acyclic. Each edge carries a positive integer length and a positive integer transition time . A path has length and transition time . For a nonnegative integer , a -path is a path from to with , and is the length of a shortest -path.
Fix . For a real , the rounded lengths are
Procedure TEST(V) deletes the edges with and answers NO if, for some integer , some – path in the remaining graph has transition time at most and rounded length at most ; otherwise it answers YES.
The Rounding Algorithm keeps bounds on OPT. Starting from initial bounds , Step 1 repeats while : with it sets if TEST(V) = YES and if TEST(V) = NO. Step 2 outputs a -path that is shortest for the rounded lengths . The bounds after passes are written .
If is a lower bound on the length of every -path, is a stage at which , and is a Step 2 output at , then
that is, . The initial upper bound is arbitrary.
The guarantee makes the Rounding Algorithm a fully polynomial approximation scheme: combined with the paper's running-time analysis, a -approximate -path is computed in time polynomial in the input size and . The two ingredients, an approximate decision test that answers "OPT " or "OPT ", and a geometric search on the ratio , are reused in later FPASs for constrained path, knapsack-type and scheduling problems; the milestones isolate them as separate statements.
The result has been proved since 1992 but, as far as a search of the platform and of Mathlib shows, none of it is machine-checked. This mission produces a checked version of the first scheme, stated for every stage at which the printed stopping test holds and every optimal Step 2 output. It also records, as a companion, that the printed Step 1 need not terminate when , and proves termination under .
The arithmetic of each step is short; the difficulty is in the combinatorial facts the page uses without proof and in the bookkeeping of a run. The rounding error of a path is at most only because a – path has at most edges, which follows from the numbering and must be derived for list-encoded paths. The YES case must cover -paths through edges that TEST deleted, which the rounding argument does not see. The bound update needs both bounds to stay positive so that is a meaningful test point, an invariant of the whole run rather than of one step. A tempting shortcut, assuming that LB is a lower bound on OPT at the stopping stage, would assume milestone 4; the goal assumes it only for .
The ellipsoid method decides questions about a convex set by maintaining an ellipsoid that contains the relevant part of and shrinking it step by step. Introduced for convex minimization by Yudin and Nemirovskii and by Shor in the 1970s, it became famous in 1979 when Khachiyan used it to show that linear programming is solvable in polynomial time. Grötschel, Lovász and Schrijver (Combinatorica 1 (1981)) observed that the method never needs an explicit description of : it only needs, for a query point , either a confirmation that is (nearly) in or a hyperplane (nearly) separating from . From this they derived that optimization and separation are polynomially equivalent for convex bodies, which in turn gives polynomial algorithms for problems with exponentially many constraints: matroid intersection, submodular function minimization, and the stable set problem in perfect graphs.
The engine of all of these applications is a single quantitative statement, Theorem (2.4) of the paper: with a weak separation oracle and with all numbers rounded to a fixed number of binary digits, a prescribed number of ellipsoid steps produces an -optimal point.
Timeline. 1976–1977: Yudin–Nemirovskii and Shor, the method for convex programming. 1979: Khachiyan, polynomial-time linear programming. 1981: Gács–Lovász publish a complete proof of Khachiyan's result with the explicit rounded update; Grötschel–Lovász–Schrijver state and prove the weak-oracle version, Theorem (2.4), and its combinatorial consequences; Bland–Goldfarb–Todd survey the method (Oper. Res. 29 (1981)). 1988: the monograph of Grötschel, Lovász and Schrijver (Springer) gives the full theory of weak oracles.
All norms are Euclidean: , and for a symmetric matrix is the largest absolute eigenvalue. is the closed Euclidean ball of radius about , and the set of points within distance of .
A convex body consists of a compact convex , , and with
A weak separation oracle with precision answers a query either with "", or with a vector , , such that for all .
Given an objective and an accuracy (with and ), set
Start from , . At step query the oracle at . If it answers "feasible", is a feasible index and ; otherwise . Put and
and obtain , by rounding , to binary digits, keeping symmetric. The ellipsoids are , and is the set of points of whose objective value is at least that of every feasible centre found before step .
In Lean, IsRoundedRun K c a₀ R δ p N x A feas a d records exactly these conditions, Kk is , and is the published LinearOptimization.ellipsoid (x k) (A k).
If is a feasible index whose centre is best among the feasible centres, , then
The statement is for every run, i.e. for every sequence of valid oracle answers and every admissible rounding.
Theorem (2.4) turns any weak separation procedure for a convex body into a weak optimization procedure, with a number of oracle calls and a numerical precision polynomial in , , , and . This is the "only if" half of the paper's Theorem (3.1), and through it the source of the polynomial algorithms of Chapters 4–6 of the paper and of the 1988 monograph. Its rounding analysis is what makes the method an algorithm on finite-precision numbers rather than an argument about exact real arithmetic.
The result is proved, and has been for over forty years. What this mission adds is a machine-checked proof of the rounded, weak-oracle version, including the error analysis that the paper compresses into "rounding errors can be estimated similarly". Related items already on the platform formalize exact-arithmetic ellipsoid methods: Bertsimas–Tsitsiklis's central-cut method for polyhedra (LinearOptimization.ellipsoid_method_correct, proved) and Bubeck's version for convex minimization with a first-order oracle (arXiv:1405.4980). Neither has a weak oracle, the inflated factor , or rounding.
For the exact update with factor and an exact separating hyperplane through the centre, containment and volume decrease are a classical computation. Here three perturbations interact. The cut is shifted by , so the retained half-ellipsoid is slightly larger than a half. The rounded matrix differs from by up to in norm, which could destroy positive definiteness if the smallest eigenvalue were not controlled from below, and Lemma (2.1)'s bound is what controls it. The containment must absorb both errors, and it is the inflation factor , chosen larger than the optimal one, that leaves room. The paper bounds the remainder term in (29) only by "similar methods"; making that bound explicit is the bulk of the work. The final step also needs the volume rate in (32), which is sharper than iterating Lemma (2.2) and requires the exact per-step volume ratio of the inflated update.
is Fin n → ℝ with Lebesgue measure. Since Lean's norm on Fin n → ℝ is the sup norm, the Euclidean norm is written out (euclNorm), and the bounds , are stated as quadratic-form (eigenvalue) bounds. uses the natural logarithm and the integer ceiling.
The runs generalize the page in three ways, each of which makes the theorems stronger: the oracle's answers are any answers valid for its specification; rounding is any symmetric value within entrywise; and data are real rather than rational.
The page's standing assumptions , , (p. 173) are hypotheses. Two hypotheses are added, because the page's , and are absolute numbers and the claims fail at extreme scales:
Neither is needed in (13) or (34).
A run predicate without the oracle clause would make Lemma (2.3) false, and one with exact equality instead of rounding would state a weaker theorem; the goal quantifies over every run, never over some run. Positive definiteness of the is a consequence (Lemma (2.1)), not a hypothesis: since Lean's inverse of a singular matrix is , assuming it would hide the lemma's content.
Out of scope: the paper's polynomial-time claims (Theorem (3.1) and its consequences), the bit length of the numbers, and the rationality of inputs, since no oracle-machine model with bit complexity exists in Mathlib or on the platform.
Reusable infrastructure: volumes of ellipsoids and of cone pieces, Sherman–Morrison-type inverses, and perturbation bounds for positive definite matrices. Contributions of these as separate lemmas are welcome.
Reflected Brownian motion on the orthant is the diffusion that arises as the heavy-traffic limit of open networks of queues. In a -station network the scaled queue-length vector lives in the nonnegative orthant ; in the interior it moves like a Brownian motion, and when a station empties the process is pushed back into the orthant in a direction determined by the routing of customers between stations. Harrison (1978) obtained such a limit for two queues in tandem, and Reiman (Open Queueing Networks in Heavy Traffic, Math. Oper. Res. 9 (1984)) showed that general -station open networks lead exactly to the class of processes studied here.
Classical constructions of reflected diffusions (Stroock and Varadhan 1971, Watanabe 1971) require a smooth boundary and a reflection direction varying continuously on it. The orthant has corners and the reflection direction jumps between faces, so those results do not apply. Harrison and Reiman (Reflected Brownian Motion on an Orthant, Ann. Probab. 9 (1981)) construct the process pathwise, following Skorokhod's one-dimensional approach, and derive its Markov property from the construction. The process has since become the standard object in the diffusion approximation of queueing networks.
Fix a positive integer . Vectors in are row vectors, indexed by . Let be a covariance matrix (symmetric, nonnegative definite), a drift vector, and a nonnegative matrix with zeros on the diagonal and spectral radius strictly less than one. is the nonnegative orthant.
Let be the space of continuous paths with the topology of uniform convergence on compact intervals, and the paths with . For , the Skorokhod problem asks for with, for every ,
nondecreasing with (7), and increasing only at times where (8). In matrix form, . Theorem 1 of the paper shows there is exactly one such pair, written , .
The process is obtained by feeding a Brownian path into this map. On a probability space let be a -dimensional Brownian motion with covariance matrix , drift and almost surely, with independent of the increments of . Let . Set and where , and on the exceptional null set. is reflected Brownian motion on with reflection matrix .
There is a family of Markov transition kernels on , depending only on , such that for every such , , :
Here (1)–(4) are (5)–(8) for the paths of , , . The kernel is chosen before the probability space and the initial law, which is what "stationary transition probabilities" means.
The milestones follow the proof of Theorem 1 on pp. 304–305:
Milestone 7 is the platform theorem Reiman84.QueueLength.lemma_1, posed as an open target by an earlier mission (Reiman 1984 cites it as its Lemma 1). It is referenced here and not posed again.
Corollary 1 is what makes a usable stochastic process: adaptedness and almost-sure uniqueness say is determined by the driving Brownian motion in a non-anticipating way, and the Markov property with time-homogeneous kernels is the starting point for the change-of-variable formula of §3, for generators, for stationary distributions, and for the heavy-traffic limit theorems in which appears as the limit. The pathwise map and its Lipschitz continuity are reused throughout queueing theory: the continuous-mapping argument for heavy-traffic limits rests on exactly the continuity (10) established here.
The results are classical, with complete published proofs. None of them has a machine-checked proof. Mathlib has the measure-theoretic layer (kernels, conditional expectation, independence) but no reflection maps, no construction of multidimensional Brownian motion with drift, and no Markov-process theory in continuous time. This mission provides a formal statement of the pathwise reflection theory and its probabilistic consequence on which such a development can build.
The pathwise part is a contraction argument, but the contraction is not in the original norm: the map need not be a contraction for any standard norm when only the spectral radius of is below one. The proof first changes coordinates by a positive diagonal matrix, and the right norm must be matched to the row-vector convention. The fixed-point characterization also has to be shown equivalent to the complementarity condition (8), which is where the zero diagonal of enters.
For Corollary 1, the difficulty is measure-theoretic. Adaptedness requires measurability of a path functional with respect to the uncompleted natural filtration, which uses (9) and (10) and the fact that continuous paths are determined by countably many coordinates. The Markov property requires the regeneration identity (11) together with independence of the post- increments of from , and a kernel that is jointly measurable and independent of the initial law. Conditioning on alone, without identifying the future as a fixed functional of and an independent Brownian motion, does not give a kernel that is the same for all .
Fin K → ℝ (paper index = Lean index ), with ; row vector times matrix is Matrix.vecMul. Paths are functions ℝ → Fin K → ℝ; only times are constrained.Reiman84.QueueLength.lemma_1. is PosSemidef.Reiman84.QueueLength.IsReflectionPair; (8) reads " is constant on every interval on which ". is IsCPlus; uniform convergence on compacts is UocTendsto; Brownian motion from with drift and covariance is IsDriftedBM.Out of scope: Theorem 2 (the change-of-variable formula, which needs stochastic integration), the necessity of spectral radius , and §§3–4. Useful contributions beyond the milestones include a construction of multidimensional Brownian motion with drift in Mathlib, the Skorokhod map as a function on , and general lemmas on measurability of continuous path functionals.
The proximal point algorithm is a way to find a zero of a set-valued monotone operator by repeatedly solving a regularized version of that operator equation. Its classical regularizer is quadratic, so the distance from one iterate to the next is Euclidean. In convex optimization, that geometry can be poorly matched to the domain: the natural iterates may be constrained to a positive orthant, a simplex, or an open set with a meaningful boundary. Eckstein's 1993 paper studies what happens when a Bregman function supplies the regularization instead. The convergence question matters because the later multiplier methods in the same paper are instances of this general iteration. Eckstein (1993) develops the general result before applying it to convex programs.
The result considered here is Theorem 1 of that paper. It concerns an existing infinite run: it states what such a run does, while Theorems 4 and 5 address conditions under which a run can be generated. This separation keeps the convergence assertion precise. The result is known mathematically; the mission asks for a Lean proof of its stated generality, including its alternative when the operator has no zero.
Work in a finite-dimensional real inner-product space , representing the paper's . A monotone operator associates a set of vectors with each point. It is monotone when for every and , and maximal monotone when its graph has no proper monotone extension. Its domain is ; a zero is a point with .
Let be open and a real function on . At , define the Bregman distance
It need not be symmetric and is generally not a metric. Definition 1 requires to be continuously differentiable on , strictly convex and continuous on , and to satisfy boundedness of both kinds of partial sublevel sets. Two sequential conditions connect convergence in to convergence of Bregman distances, including sequences approaching the boundary of . These six requirements together define a Bregman function with zone .
A Bregman proximal-point run uses positive parameters and a sequence satisfying
This is the inclusion form (4) of the paper's recursion (3). It permits set-valued and does not assert that a next iterate exists for arbitrary starting data. The model also uses the paper's standing domain condition .
The main target is Theorem 1. Assume that the positive parameters have a common positive lower bound and that one of the following conditions holds: (C1) , or (C2) for a proper lower semicontinuous convex extended-valued function . Then
The second line retains the paper's extra (C1) requirement. The standing inclusion has a different direction and role. The milestone list follows Lemma 1 and the three labelled steps of Theorem 1's convergence proof: the resolvent inequality, boundedness of the run when a zero exists, identification of every limit point as a zero, and convergence of the full run. The no-zero alternative remains in the goal because restating that conjunct as a separate milestone would add no independent target.
Theorem 1 says that the nonlinear iteration cannot remain bounded without approaching a zero under (C1), and that when a zero exists the whole sequence converges under either (C1) or (C2). This is stronger than saying only that accumulation points solve the operator equation. It supplies a common convergence result for the paper's later proximal minimization and multiplier algorithms, where the operator is often a subdifferential and the geometry comes from a nonquadratic . Eckstein (1993) gives those applications after the general theorem.
A formalization would add a reusable interface for Bregman functions with open zones, including their boundary behavior, and for proximal-point runs of set-valued maximal monotone operators. The published platform definitions of monotone operators and extended-valued convex analysis are reused. The new proof work is the Bregman resolvent estimate and the convergence alternative at Theorem 1's level of generality. No machine-checked proof of this specific theorem is claimed here.
The usual Euclidean proximal-point theorem does not apply directly after changing coordinates by : the transformed operator need not remain monotone, as the paper observes after Theorem 1. A proof must account for the nonsymmetric , the possible boundary of , and two distinct ways to identify a limit point as a zero. Under (C1), the point lies where the gradient is continuous; under (C2), the argument uses the subdifferential structure instead. The no-zero case has its own difficulty because boundedness would have to contradict maximal monotonicity without first assuming that a zero exists. The proof cites a closed-graph result for maximal monotone operators and a zero-existence fact for operators with bounded domain; those external facts are groundwork for solvers, not invented milestones.
Lean uses a finite-dimensional real inner-product space rather than a coordinate-fixed . The total function is constrained only on ; its gradient is evaluated only on the open zone . The Bregman distance is used on . Definition 1's condition (vi) explicitly places its first sequence in , the natural domain stated immediately after the definition. The run explicitly keeps every in and encodes recursion (3) using the equivalent inclusion (4). A positive lower bound on is expressed by one with for every .
The operator is a published set-valued operator object, with its published notions of monotonicity, maximality, domain, and zeros. The proper and convex extended-valued function in (C2) uses the published epigraph and subgradient definitions, with EReal able to express . Subdifferentials are built from those definitions. A limit point means a limit along a strictly increasing subsequence, and unboundedness means that the full set of iterates is not bounded. The proof step on p. 207 prints ; the formal Step 1 uses the standing condition , which is sufficient for the Bregman distance and also covers (C2).
The run relation cannot be satisfied by an arbitrary constant sequence: its inclusion must hold at every step, and a zero-free operator under (C1) triggers the unbounded conclusion. Nor does the theorem replace convergence by existence of one convergent subsequence. Reusable contributions include properties of the Bregman resolvent and maximal-monotone graph limits. Theorem 5's separate existence and minimization claims are outside this mission's core.
Every manufacturer who makes a part in batches faces the trade-off Ford W. Harris described in 1913: large lots spread the fixed set-up cost of an order over many pieces, but they also tie up money in stock that must be carried. Harris's article "How many parts to make at once" (Factory, The Magazine of Management 10(2), 1913, reprinted in Operations Research 38(6), 1990) resolved the trade-off with a closed formula, the square-root or economic order quantity (EOQ) formula. It is the starting point of deterministic inventory theory and is still taught as the first model of every operations-management course.
Timeline. Harris published the formula in 1913, without proof ("the solution of this problem involves higher mathematics"). The same formula was popularised by R. H. Wilson in 1934 and was for decades attributed to him. D. Erlenkotter traced it back to Harris (Operations Research 38(6), 1990, 937–946), and the article was reprinted in the same issue. Later work built stochastic (Q, r) models on top of it; Zheng (1992) compared the EOQ heuristic with the optimal (Q, r) policy.
A part is used at a regular rate of units per month (the movement). Each unit costs dollars (the unit cost), and each order costs dollars to set up. Parts are made in lots of units, the lot size. Under regular movement a lot of is delivered when the stock reaches nothing and is then used up at rate , so the stock at time (months, from a delivery) is the sawtooth
with the fractional part. Interest and depreciation on stock are charged at ten per cent a year, a rate the paper fixes.
Harris prices a unit in three parts:
The cost per unit is therefore
and the economic lot size is . In Lean these are stockLevel, interestPerPiece, costPerUnit and econLotSize in the namespace HarrisEOQ.Lot.
For ,
This is Harris's claim that the value of giving the minimum value to "reduces to the square root of (240MS divided by C)": is admissible, attains the minimum, and is the only lot size that does.
These justify the objective , not its minimization; the paper gives no argument for the minimization.
The result. The square-root formula gives the cost-minimising batch size in closed form from three observable numbers. Its consequences are the ones Harris draws: lot sizes grow only with the square root of demand (so consumption must quadruple to double a lot), the cost curve is flat near the optimum and asymmetric (erring small is worse than erring large), and at the optimum the set-up cost balances the variable carrying cost. Every later deterministic and stochastic lot-sizing model reduces to this one in its simplest case.
Formalizing it. The result is classical and proved in textbooks, but Harris's paper itself contains no proof. A formalization supplies the missing argument for the paper's exact objective, which differs from the textbook EOQ by charging interest on the set-up cost ( in the stock value) and by the fixed ten per cent rate. It also makes the paper's modelling step precise: the claim that the average stock is becomes a statement about a time average of a sawtooth function. To our knowledge none of these statements has a machine-checked proof on the platform; the EOQ items of Zheng (1992) concern a different model, with backorders.
The minimization is elementary calculus; the substance of the mission is fidelity. The objective must be the display as printed, with meaning , and the claim includes uniqueness, not only that is a minimizer. The average-stock milestone needs a genuine long-run average of a discontinuous periodic function over with not a whole number of cycles, which is where the integration and limit bookkeeping lies.
All quantities are real numbers; lot sizes are not restricted to integers (the paper's own optimum is 48.5). The hypotheses are not written on the page; they are implicit in the meaning of a usage rate, a price and a cost, and are added. Every quantifier over lot sizes is over . Time is measured in months, and the interest rate is fixed at ten per cent, so the constant appears as printed; the formula is not generalized to an arbitrary rate.
A trivializing formalization is ruled out: is defined as the printed display, not rewritten around ; the average stock is an integral of the stock level, never defined as ; and the goal does not quantify over all real , where Lean's convention would make a spurious minimizer.
The manufacturing interval and the safe stock minimum play no role in the formula and are not modelled. The examples' cost figures (0.188 cents, $0.00028, and so on) are not formalized. The development needs only Mathlib's real numbers, square roots, fractional parts, interval integrals and limits; contributions of proofs of any item are welcome.
Stochastic optimization asks for a decision in a set that minimises an expected loss when the distribution of the data is known only through a sample . The classical estimator, sample average approximation, replaces by the empirical distribution . Distributionally robust optimization instead minimises the worst-case expected loss over all distributions close to . Duchi, Glynn and Namkoong (arXiv:1610.03425v3; Math. Oper. Res. 46(3), 2021) take the neighbourhood to be an -divergence ball of radius and show that the robust optimal value is a calibrated upper confidence bound for the population optimum, in the spirit of Owen's empirical likelihood.
A confidence bound is useful only if the robust problem still estimates the right thing. Section 5 of the paper answers this: under essentially the conditions that make sample average approximation consistent, the robust optimal value converges to the population optimal value, and the robust minimisers approach the population minimisers. This mission formalizes that consistency result (contribution (iv), p. 3, and §5.1).
Let be i.i.d. random elements of a separable metric space with law , and let be the empirical distribution of . Let be lower semicontinuous on , with measurable for , and let be a nonempty closed feasible set, as in the paper's opening setup (p. 1).
The divergence generator is convex with ; Assumption A asks moreover that be three times differentiable near with and . For a distribution with weights on the sample points, . The robust objective and the population objective are
with radius parameter . Their solution sets are and (display (23)). The inclusion distance from a set to a set is (display (6)).
Assumption E asks for a measurable envelope with for all and for some . A class of functions on is Glivenko–Cantelli (Definition 2) if almost surely.
Let Assumptions A and E hold, let be nonempty and compact, and let be continuous on for every . Then, in outer probability,
Both conclusions belong to the goal. No rate is asserted; the statement survives any later sharpening.
The result. Corollary 1 shows that robustness against a -divergence perturbation of the data costs nothing asymptotically: the robust optimal value and its minimisers are consistent for the population problem. Together with the paper's coverage theorem, this justifies using the robust value both as a point estimate and as an upper confidence bound. Theorem 7 is stronger than what the corollary needs: it controls every reweighting in the ball uniformly over , which is the uniform law of large numbers for distributionally robust objectives, and it needs only slightly more than the first moment that sample average approximation needs.
Formalizing it. The results are proved in the paper; none is machine-checked. A formal development would supply a Glivenko–Cantelli notion for parametric loss classes, the bracketing argument behind Example 5 (a uniform strong law over a compact parameter set, not in Mathlib), and the passage from uniform convergence of objectives to convergence of optimal values and of argmin sets in the inclusion distance. The last two are standard steps of M-estimation and sample average approximation theory that are reusable well beyond this paper.
The obvious argument writes as a reweighting term plus the ordinary empirical deviation and handles the second by the Glivenko–Cantelli property. The reweighting term is the obstacle: the weights are not bounded uniformly in for every divergence, and a Cauchy–Schwarz bound would need a second moment of the envelope, which Assumption E does not provide. The exponent pair and the uniform control of Lemma 13 are what make moments enough.
For the solution sets, uniform convergence of to does not by itself place the minimisers of near those of ; compactness of and continuity of are needed to separate on the complement of an -enlargement of from its minimum. Measurability is a further obstacle: suprema over uncountable and over the divergence ball need not be measurable, which is why the paper works with outer probability and outer almost-sure convergence.
ξ : ℕ → Ω → Ξ on a probability space, measurable, mutually independent (iIndepFun) and identically distributed with ξ 0; is the law of ξ 0, and uses ξ 0, …, ξ (n-1) (0-based indices). The separable metric sample domain and lower semicontinuous loss from p. 1 are explicit in Theorem 7 and Corollary 1. Decisions live in EuclideanSpace ℝ (Fin d); ℓ x is measurable for each .ℝ → EReal satisfying the published IsPhiDivergenceFunction (never , finite on , , convex on ) plus the smoothness of Assumption A, stated on on an open interval around .probUncertaintySet f (1/n,…,1/n) (ρ/n), i.e. . Every supremum "over with " is read over , as in (4a).∀ᵐ, which requires the exceptional set to have outer measure zero; convergence in outer probability is for every with Mathlib's outer measure and no measurability hypothesis.Scheduling work on several identical processors creates a plausible expectation: completing tasks sooner, removing constraints, or adding a processor should not delay the overall finish. A fixed priority-list rule defeats that expectation. When a task becomes ready earlier, it can occupy a processor that would otherwise have run another task; that decision changes later availability. Graham gives explicit schedules in which changing only the list raises the finishing time from 12 to 14, removing two precedence constraints raises it to 16, shortening every task raises it to 13, or adding one processor raises it to 15. These examples establish that the effect is a property of the scheduling rule, rather than of a change in the total set of tasks. See Graham, §2, pp. 417–419.
This mission concerns the upper limit of that effect. An operations researcher comparing a list schedule before and after a change in available processors or task data needs a bound that survives all four changes at once. The result is also a compact benchmark for formalizing algorithms whose behavior depends on changing availability: the model must describe when tasks become ready, when processors are idle, and which ready task a processor takes next. Graham's Theorem 1, proved in the 1969 paper, supplies the bound.
There are tasks and identical processors. Each task has a positive processing time . A strict precedence order specifies tasks that must be completed first: means cannot start before ends. A priority list orders all tasks once each. It may place a successor before a predecessor, because the processor skips any task that is not ready. These conventions are those of Graham's system in §2, p. 416.
A schedule gives each task a processor and a start time . Once started, the task occupies that processor continuously on . Two tasks on one processor cannot overlap, while tasks may meet at an endpoint. Precedence means whenever . The finishing time is the largest completion time . The paper's list rule starts the first currently ready task in whenever a processor can take a task. A ready task that has not started cannot coexist with an idle processor. If one task starts while another ready task waits, the started task is earlier in .
The same task set is run a second time, with processing times , order , list , processor count , and finishing time . The data satisfy for every and . Thus the second run may have shorter tasks and fewer precedence relations; both lists may differ arbitrarily. Both runs obey the same list-scheduling rule Graham, §3, p. 419.
For , positive processing times in both runs, and the two list schedules just described, the target is Graham's Theorem 1:
The numerator and denominator refer to the actual runs, with potentially different lists and processor counts. The conclusion does not require the new schedule to finish earlier. Its factor permits the anomalies shown in §2 while preventing an arbitrarily large increase for fixed . The supporting targets follow the proof's numbered displays: a precedence chain covering idle times in the second run (1), an idle-time estimate for that chain (2), a comparison of its length with the first run (3)–(4), and the work-volume bound used in (5) Graham, pp. 419–420.
The theorem places a quantitative limit on the damage caused by a list rule after simultaneous changes in task durations, precedence, ordering, and capacity. When , the factor is ; when the first run has one processor, it is . The statement applies to every finite task set and every pair of lists, so it can be reused when a scheduling method produces a list without additional structural guarantees. Graham states that the bound is best possible, citing earlier examples; this mission formalizes the inequality in this paper and does not claim to formalize those external examples Graham, p. 420.
The result is proved in the source paper. The work here is to give its objects precise Lean definitions and to supply machine-checked proofs of the bound and its supporting claims. A formal development needs to account for continuous real start times, processor assignments, half-open execution intervals, and the behavior of the list rule when several tasks or processors become available together. The resulting model of a nonpreemptive list schedule and the basic volume and chain estimates can serve later formalizations of parallel scheduling. The present proposal contains statements and definitions; its theorem bodies are open proof obligations.
Total work alone does not control the anomaly: processors can be idle while precedence keeps available work from starting, and changing precedence can alter which tasks occupy the processors later. A direct comparison of corresponding task completion times between the two runs also fails in Graham's §2 examples. The central difficulty is expressing the second run's idle periods through work on a single precedence chain and then relating that chain to the first run's finishing time. In Lean, the chain and the time intervals must be represented without silently changing endpoint conventions or treating a ready but unstarted task as running.
Tasks are Fin r and processors are Fin n, with zero-based Lean indices corresponding to Graham's one-based subscripts. Processing times and start times are real. A priority list is a bijection between positions and tasks, so it contains every task exactly once and need not respect precedence. The order is strict. Feasible schedules are nonpreemptive and use half-open running intervals. The finishing time is a finite maximum of completion times; for no tasks it is defined as zero, while the ratio theorem assumes so its denominator is positive. Both processor counts are positive. The strict positivity of both time functions is inherited from the paper's convention.
The model captures Graham's rule by no unforced idleness and list priority. It does not encode the smaller-index tie rule for identical processors, since the tie affects only processor labels and not start times or . The covering-chain milestone represents Graham's set as times before when not all processors are busy; all-idle times before the finish cannot occur under the list rule. The idle-time milestone writes the total duration of empty tasks as using display (5). Natural-number subtraction is not used in the constants: and are real differences. The companion existence statement and a concrete two-task sanity check rule out a vacuous list-schedule predicate. Contributions can address that existence theorem, the chain construction, interval accounting, the volume bound, and the final ratio.
A martingale is a sum of increments that are uncorrelated with the past. For sums of independent random variables, sizes are compared through the sum of squares of the summands; for martingales the corresponding object is the square function
Comparing the size of with the size of is one of the basic tools of probability and of harmonic analysis: it underlies Khintchine-type inequalities, the theory of martingale transforms, the Littlewood–Paley theory of dyadic and Fourier series, and the Burkholder–Davis–Gundy inequalities used throughout stochastic calculus.
Timeline. Paley (1932) proved bounds for the square function of Walsh–Paley series, the dyadic model case. Marcinkiewicz and Zygmund (1937–38) proved the analogous inequalities for sums of independent mean-zero random variables. Burkholder (1966, Ann. Math. Statist. 37) proved them for general martingales, , together with the weak-type bound for . Burkholder and Gundy (1970) extended the comparison to functions of moderate growth by distribution function ("good-") inequalities, and Davis (1970) settled for . The 1973 Wald lectures formalized here re-derive the inequality from one elementary stopping-time identity (Lemma 2.1), with explicit constants.
Let be a probability space and sub--fields of . A martingale relative to is a sequence of integrable random variables , with -measurable and ; a submartingale has in place of .
With the convention , the difference sequence is (so ). Write
For the exit time (with ) is a stopping time; , , denote evaluation at the random index, with and .
In Lean these are dseq, sqFnN, sqFn, maxFnN, lpNormE, pNorm, exitTime, valAt and sqFnAt in the namespace BurkholderDFI.SquareFnLp.
For each there are positive constants , depending only on , such that every martingale satisfies
The goal asserts only existence of the constants, so that it does not depend on the particular numbers the paper's proof produces.
In attack order:
Here is the conjugate exponent, .
The result. Theorem 3.2 says that a martingale is bounded in exactly when its square function lies in , with comparable norms. It reduces questions about , whose increments interact, to questions about , a sum of nonnegative terms. Immediate consequences include the boundedness of martingale transforms with (unconditionality of martingale differences in ), Marcinkiewicz–Zygmund and Khintchine inequalities, and, by passing through dyadic martingales, Littlewood–Paley inequalities. Theorem 3.1 is the endpoint estimate: at the strong inequality fails, and weak type is what survives.
The formalization. The theorem is classical and proved; the remaining work is to machine-check it. Mathlib at the pinned revision contains no square function inequality for martingales (no occurrence of Burkholder's inequality or of a martingale square function in Mathlib/Probability); it has Doob's maximal inequality for nonnegative submartingales, optional stopping, and a.e. convergence of -bounded submartingales. The mission would add the stopping-time identity of Lemma 2.1, the weak-type bound with constant 3, the explicit constants and , and the general extrapolation lemma (1.3), each reusable on its own.
The obvious route, expanding by orthogonality, works only at . For no such identity exists, and interpolation from needs an endpoint estimate that is itself the hard part: is not bounded on . The paper obtains the endpoint from Lemma 2.1, whose content is an exact computation at the random time ; turning it into rigorous Lean requires handling evaluation at (where the a.e. limit enters), passage to the limit in stopped identities with only control, and integrability of the products . The upper bound is not a formal consequence of the lower one at the same exponent: it requires passing to the conjugate exponent .
f : ℕ → Ω → ℝ; martingales and submartingales are Mathlib's Martingale f ℱ P / Submartingale f ℱ P for a filtration ℱ : Filtration ℕ _ with ℱ k . The paper's is built into every definition, which never reads Lean's f 0. Mathlib additionally relates f 0 to ; this is no restriction, since any martingale relative to extends by .Type (universe 0).Infrastructure that a complete development needs and that is reusable beyond this mission: evaluation of a process at an -valued stopping time, the layer-cake formula for -valued , and conditional-expectation martingales with their difference sequences. Proofs of any milestone, in any order, are welcome.
Parallel processing poses a basic allocation question: given tasks of known lengths and several identical processors, how much time is lost when tasks are assigned by a simple list rule instead of an optimal allocation? The finishing time is the moment the last processor completes its work. For independent tasks, a list rule starts each next task on a processor that becomes free first. Such a rule is easy to execute, but the resulting allocation can be worse than the best partition of tasks among processors. Graham's 1969 paper studies precise worst-case ratios for this model. Its Theorem 3 asks what guarantee follows when the first tasks of the list are chosen among the longest and scheduled optimally before the remaining tasks are appended.
The paper also notes two endpoints of this family. With , the rule is ordinary list scheduling and has ratio at most . With , the longest tasks can start one per processor, giving ratio at most . Theorem 3 expresses these as instances of one bound, including the integer jump at each multiple of Graham, pp. 427–428.
There are independent tasks, indexed by , and identical processors, indexed by . Task takes a strictly positive time . A priority list contains every task exactly once. Its first tasks are of the longest tasks; equal lengths may be ordered either way. As a processor becomes available, it takes the next task in the list. Once started, a task runs without interruption. With no precedence constraints, every unstarted task is ready, so a processor runs its assigned tasks consecutively from time zero.
An assignment records the processor that executes each task. The load of processor is the sum of its assigned task lengths. The finishing time is the largest load, . For a list assignment, each task is assigned to a processor whose load from earlier list tasks is smallest at that step. If two processors are tied, either can be selected without changing the finishing time. For any assignment , let be the largest load contributed by only the first list tasks. The algorithm requires its own first assignments to minimize over all assignments ; the remaining tasks may occur in any list order.
Write for the smallest finishing time achievable for all tasks. The paper introduces it as the minimum over possible lists and later describes the same problem as minimizing the largest part sum over partitions of the task lengths Graham, pp. 421, 428. The formalization uses the partition or assignment form of .
For , when the first longest tasks have an optimal prefix schedule, Graham's bound is
Here is the greatest integer at most . The theorem also says the bound is best possible when is divisible by Graham, Theorem 3, p. 427. The equality examples are a separate companion statement in this mission.
The milestones state the finite-volume lower bound on , the case in which completing all tasks takes no longer than completing the first , and the paper's numbered inequalities (14), (15), and (16). They use for the greatest task length after the first positions. These are individual mathematical claims from the proof on p. 427, with their original wording and formulas recorded alongside the formal statements.
The theorem gives a quantitative tradeoff between work spent optimizing a prefix and the worst-case finishing time of the full list. Its denominator is , so the guarantee improves when the optimized prefix contains another full processor's worth of long tasks. The example at multiples of shows that the stated coefficient cannot be uniformly reduced for the algorithm as specified Graham, p. 427.
The result is proved in the paper. This mission's remaining work is a machine-checked proof of its exact statement and the source's intermediate inequalities. The published identical-machine makespan definition is reused, while the list-assignment rule, optimal prefix, and longest-remaining-task quantity are made explicit here. Those definitions can also support later work on list scheduling without precedence constraints. No machine-checked proof of Theorem 3 is claimed by this proposal.
An optimal schedule for the first long tasks does not make the entire list optimal: short tasks appended later can affect which processor finishes last. A bound based only on average total work ignores this final imbalance; a bound based only on the largest remaining task ignores how many long tasks every assignment must place together. The proof must relate both constraints to one finishing time while preserving the floor . Replacing that floor with the real quotient changes the claim, and allowing an arbitrary prefix arrangement loses the algorithm's required optimality.
Tasks and processors are finite indexed sets Fin r and Fin n; their zero-based indices correspond to the paper's one-based and . Task lengths are positive real numbers, and both and are positive. The list is a permutation, not merely a sequence that might omit or repeat a task. The condition is explicit because choosing tasks from requires it; the paper treats inside the proof and the case is covered by the theorem. There is no precedence relation in this mission.
The list rule is a predicate on assignments: each next task goes to a processor with least current load. It omits the paper's smaller-index tie convention, since tied identical processors can be interchanged without changing the finishing time. The first positions must contain longest tasks, and their assignment must minimize the prefix finishing time among all assignments of those tasks. Those conditions are part of the goal; the inequalities (14)–(16) are conclusions to establish, not assumptions of the goal. A separate existence statement and a checked concrete instance ensure the list predicate is satisfiable.
All maxima and minima range over finite nonempty processor or assignment sets. The optimum is a minimum over assignments, equivalent to the paper's minimum over lists in the independent-task model. The quantity is the largest duration outside the prefix when , and is defined as zero when none remains; statements using it require . Division is by and by . Lean's natural-number quotient represents ; real subtraction is used for coefficients such as . Contributions toward the finite load identities, the optimum-over-lists equivalence, and proofs of the listed bounds are within scope.
Network revenue management is the problem of selling several limited, perishable resources (seats on flight legs, hotel room-nights, machine hours) to customers who arrive over time and each want a fixed bundle of them. A seller who accepts every request early may run out of the resources that the most valuable later customers need, and a seller who is too cautious leaves capacity unsold at the end of the horizon. Airlines, hotels and car-rental firms solve instances of this problem daily (Talluri and van Ryzin, 2004).
The exact optimal policy is a dynamic program over the vector of remaining capacities, which is intractable for realistic networks. The standard remedy replaces the random demand by its mean, which gives a linear program, the deterministic LP (DLP), and turns its solution into an admission rule. Its value is an upper bound on what any policy can earn (Gallego and van Ryzin, 1997). Solving the LP once, at time zero, loses against that bound over a horizon of length . A natural improvement is to re-solve the LP as capacity is consumed.
Timeline of the re-solving question, as the source surveys it (Sec. 1, pp. 3–4):
There are customer classes and resources . Over the horizon , class- customers arrive according to independent Poisson processes with rates . Accepting a class- customer earns and consumes units of each resource ; is the bill-of-materials matrix and its -th column. The initial capacity vector is . A customer can be accepted only if componentwise, where is the capacity remaining at its arrival.
For a capacity-per-unit-time vector , let
The DLP value is .
The Frequent Re-solving policy (FR) divides the horizon into unit periods . At the start of period , with remaining capacity , it sets , computes an optimal solution of the LP with right-hand side , and during the period accepts each class- arrival with probability , subject to the capacity check. Its expected revenue is . The LP may have several optimal solutions; the results hold for every rule choosing among them.
There is a constant , depending only on , and , such that for every integer , every capacity and every choice of optimal LP solutions,
The content is the uniformity: does not depend on , so the bound holds whether capacity is scarce, abundant, or degenerate for the LP.
The result. Because bounds the expected revenue of every admissible policy, Proposition 3 says that FR loses at most against the optimal policy in every instance, degenerate or not. Re-solving therefore never does worse, in order, than solving once. Together with the lower bound on a degenerate instance (Proposition 2 of the same paper), it shows that the order is exact for FR. The nondegeneracy assumption of the earlier analysis cannot be dropped. The explicit form (milestone 5) bounds the loss by constants computable from .
Formalizing it. The result is proved in the source; no part of it is machine-checked. A formalization adds three things. It gives a precise model of an adaptive, randomized admission policy in a Poisson network, which other results on re-solving and bid-price policies can reuse. It gives a checked LP sensitivity bound. And it checks the paper's constants: the printed constant of Lemma 8 is wrong (see Formalization scope), and the mission states the corrected one.
The obvious argument compares FR with the DLP period by period: the LP that FR solves at time differs from the original only in its right-hand side, so the loss should be controlled by how far drifts below . Two things break a naive version of this. First, is a ratio whose denominator shrinks to , so fluctuations late in the horizon are amplified; a crude bound on the drift at each sums to more than . Second, FR's realized consumption is not the LP's target: the capacity check rejects customers, and the LP solutions depend on the whole past, so the consumption in different periods is not independent.
Uniformity in is the whole point. Arguments that rely on a margin between and the degenerate points of the LP, as in the nondegenerate analysis, give constants that blow up as that margin vanishes.
The source is arXiv:1802.06192v3, whose printed page numbers equal the PDF page numbers. Everything lives in the namespace ResolvingNRM.FRUpper.
piValue A r b lam of RLPBidPrice.Unbiased.Model (a real supremum, equal to the LP maximum for ).sel; every theorem quantifies over all selectors, with constants chosen before the selector.windowExp). FR's value is a backward recursion over periods (frTail), and expectations of functions of are a forward recursion (frStateExp).A trivializing formalization is ruled out. The constant is chosen before . FR is defined with every optimal LP solution, not only nondegenerate or vertex ones. The capacity check is kept arrival by arrival; without it, FR's expected revenue would equal the LP revenue it targets and the gap would be trivially small.
Contributions welcome on every milestone. The LP sensitivity bound (33) is a statement about linear programs alone and milestone 4 about real numbers alone; both are reusable outside this mission, as is the window model of a randomized admission policy.
Bibliographic details of the non-arXiv entries are those of the source's reference list (pp. 24–25).
On one processor, the completion time of a job normally depends on how much work precedes it. In the model of Browne and Yechiali (1990), waiting also changes the job's own processing requirement: a job that starts later takes longer. The sequence therefore changes both when each job starts and how long subsequent jobs must wait. This matters when the goal is a weighted completion cost, because a delay to one job can raise the completion costs of many others.
The paper gives an expected-makespan ordering for this linear deterioration model and, in Proposition 2, a sufficient condition under which the original job order minimizes weighted expected completion cost. The latter is the target of this mission. Related platform work on Delayed SWPT and the AvgCompletionSched family treats weighted completion scheduling without this job-specific linear deterioration. Their additive processing-time models do not supply the completion-time object used here.
There are jobs, all available at time zero, processed one at a time on a single machine without idle time or preemption. A schedule is a permutation of the jobs: is the job processed in position . The paper labels positions and jobs from to ; the Lean development labels them from to . The identity schedule processes jobs in label order.
For job , is its random initial processing requirement, its deterministic growth rate, and its waiting cost rate. If the job starts at time , its actual processing time is . Deterioration stops once processing starts. Write for the time at which the first scheduled jobs have all finished. The model sets and
in the paper's one-based position notation. Thus the completion time of the job in position is . Its cost is its own rate times that completion time, giving
All of these are random quantities until an expectation is taken. Equation (2) of the paper writes as a sum of the initial requirements multiplied by the later growth factors. Equation (8) substitutes that expression into . Both equations are included as milestones, stated along an arbitrary schedule by relabelling the jobs. The third milestone is the exact change in from swapping two adjacent jobs. These three statements are pathwise identities, so their mathematical content does not depend on a probability distribution.
The principal target is Proposition 2: if both sequences of job-indexed ratios are strictly increasing,
then, for every permutation ,
The first ratio compares an initial expected requirement with its growth rate. The second couples growth and the cost rate. The conclusion is global optimality over the paper's whole class of nonpreemptive, non-idling permutations. It does not assert that the identity order is the unique minimizer; strict input ratios do not by themselves justify a uniqueness claim.
The attack path records exactly the supporting statements printed in the paper: the closed completion-time formula (2), the weighted cost formula (8), and the unnumbered adjacent-interchange identity after (8). The milestone quotations preserve the paper's printed display, while the Lean statements use an arbitrary permutation where relabelling permits it. The interchange display has a multiplication dot before its second bracket; expansion for two jobs shows that the term is added. The formal statement records that correction, and the source quotation retains the printed symbol.
The proposition identifies a directly checkable pair of ordering conditions under which the natural job-label order solves a weighted stochastic scheduling problem. A condition involving only , enough for the paper's expected-makespan target, does not determine this weighted objective. The cost rates introduce another ordering requirement. The result gives a sufficient rule, not a characterization of every optimal schedule or of every parameter choice.
The mathematical result was published in 1990; this mission asks for its machine-checked formalization. A complete development will connect the processing-time recursion, the pathwise cost identities, and the expected optimality statement in Lean. The recursion and cost definitions can be reused for other finite single-machine problems in which a job's processing time depends on its start time. The milestone identities are also useful independently of the final sufficient condition, including for studying other choices of weights and ordering indices.
Sorting by expected initial requirement alone cannot settle the problem, because processing a job changes later start times and hence later processing times. Even sorting by the expected-makespan index leaves the cost rates unaccounted for. The value of an adjacent swap depends on the elapsed time before the pair and on the completion costs of jobs after the pair. It is not enough to compare the two jobs' own completion costs in isolation.
The source states the sufficient condition after its interchange display but does not present a full proof of the global claim. Closing the Lean goal requires connecting local comparisons to every schedule and handling the expected value of the recursively defined cost. The identities are finite, but their indices change between zero-based Lean positions and the paper's one-based display, especially at the first position and at an empty suffix.
Jobs are , and a policy is an equivalence permutation with equal to the job in position . Completion time is defined by the processing rule , not by the closed form (2). At positions beyond the jobs it stays constant, and theorems about the closed form restrict to . The total cost is defined from job-weighted completion times, not from equation (8). This keeps both identities substantive.
The proposition uses a probability space and the Bochner integral of the real-valued cost. Every is integrable, so its expectation and the finite linear combinations appearing in the cost are meaningful. Initial requirements are nonnegative at every outcome, reflecting the paper's standing positive-processing convention; strict positivity is unnecessary for the claim. Growth rates and cost rates are strictly positive. Those two assumptions make the printed ratios well-defined and support the ordering rule. The paper's common independence convention is not required for these expectations and is not assumed.
The two strict orderings are over the labels of jobs in , not positions of an arbitrary schedule. The conclusion compares with every permutation, not only with schedules obtained by one adjacent swap. The and cases are allowed: the order conditions have no pair to compare, and there is only one permutation. Solvers may contribute the finite-sum, interchange, and integrability facts needed to link the milestones to Proposition 2. The pathwise identities require no probability assumptions and can support later variants.