Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Online matching describes allocation when requests must be answered as they arrive. A matching decision uses only the edges revealed so far and cannot be revised when later requests appear. In the bipartite setting studied by Karp, U. Vazirani, and V. Vazirani, the arriving vertices are girls and the possible partners are boys. Even when the full graph has a perfect matching, a fixed greedy priority can leave many girls unmatched. The paper introduced RANKING, which randomly chooses the boys' priority order once and then uses that order for every arrival.
The question is quantitative: how many pairs does RANKING guarantee in expectation against a graph and an arrival order chosen before its random ranking? The paper's target is a fraction approaching of the pairs in a perfect matching. Its printed Theorem 1 concerns an auxiliary algorithm called EARLY; the RANKING statement follows the intended chain through Lemmas 3 and 5. The original EARLY analysis has a gap for general upper-triangular matrices, so this mission states the RANKING target and the earlier, unaffected lemmas separately. This distinction matters because an assertion about EARLY would be a different formalization target.
A bipartite graph has a boy side and a girl side , each with vertices. An edge means that boy may be paired with girl . A matching is a collection of edges in which no boy or girl occurs twice. The standing hypothesis for the performance guarantee is that the graph has a perfect matching: some bijection from boys to girls selects an edge for every boy. The graph is otherwise arbitrary.
Girls arrive in a predetermined order. When girl arrives, only her incident edges are revealed. RANKING first chooses a uniformly random permutation of the boys. For each arriving girl, it selects the highest-ranked adjacent boy who is still unmatched, if one exists. Write for the final matching. The expected size is the finite average over all rankings. The guarantee must hold for every graph and every predetermined arrival order; relabeling girls lets the formal statement fix their order to .
The paper also uses a dual rows-arrive view. Boys arrive in an order and choose among eligible girls, whose priority order is fixed. This is the same greedy rule with the sides exchanged. For its triangular reduction, the columns are numbered and column has highest priority. An upper-triangular matrix with unit diagonal is a graph with every edge and with an edge only when . On such a graph, the auxiliary algorithm EARLY declines to match row if column is already covered by EARLY's own matching. For any matching , denotes the indices for which both row and column are covered.
For every , one threshold must work for every size and every graph with a perfect matching:
This is the uniform lower-bound reading of the paper's target. It does not prescribe a finite- additive constant. The mission goal is the RANKING assertion drawn from the paper's Theorem 1 and Lemmas 3 and 5. The six milestones formalize the paper's Lemmas 1–5 and the corollary to Lemma 4, in their source order. They cover the side-exchange identity, arbitrary refusal algorithms, the triangular reduction, the matching-count identity, its expected form, and the pointwise comparison with EARLY.
The guarantee gives a concrete worst-case floor for a simple randomized allocation rule: as the graph size grows, RANKING matches at least an asymptotic fraction of the pairs available in a perfect matching, in expectation. The order is selected before the random permutation, matching the paper's performance measure. The lower bound remains meaningful on sparse graphs and does not rely on a density assumption. The original paper also studies the limit on what any randomized online algorithm can guarantee; that upper-bound result is treated in a separate mission.
A formal development here would provide reusable finite definitions for online greedy matching, arbitrary state-dependent refusal, fixed-order duality, and uniform expectation over permutations. The goal is a theorem statement awaiting a machine-checked proof; compiling the draft declarations verifies their Lean syntax and types, not their truth. The local mission separates the valid early structural statements from later statements whose published EARLY argument does not justify them on general upper-triangular graphs.
The random permutation does not make the fate of different vertices independent. Matching one girl removes a boy who might be essential to a later girl, so a per-arrival probability estimate cannot simply be added across all arrivals. The dual and triangular views capture useful structure, but turning that structure into a uniform bound for every graph is the main obstacle. In particular, reasoning about EARLY as if its matched-column set had the same monotonicity as unrestricted RANKING fails on some upper-triangular matrices. A proof of the goal must establish the RANKING guarantee without treating those later EARLY statements as available facts.
Boys and girls are both Fin n; an adjacency matrix is a relation between them. A published predicate represents a perfect matching as an edge-preserving bijection. The generic greedy run processes arrival times in increasing order and interprets a smaller priority index as higher rank. It makes a new matching decision only from the current matching and the arriving vertex. RANKING's returned edges are consistently ordered as (boy, girl), even though girls arrive. The dual run has rows arriving in an arbitrary permutation and takes column as highest priority in Lean's zero-based numbering. EARLY's refusal test consults the matching constructed by EARLY itself.
All expectations are finite averages over Equiv.Perm (Fin n), scaled by . The formal claim is with a perfect matching, the displayed lower bound. Placing before preserves the worst-case meaning. The perfect-matching condition is essential: the empty graph cannot satisfy a positive linear guarantee. The triangular matrix in Lemma 3 retains every diagonal edge, so a zero matrix cannot witness the reduction. These conventions rule out vacuous versions of the goal and reduction.
The definitions of partial matching, covered vertices, greedy run, RANKING, EARLY, and uniform average are part of the mission. A complete proof may build further finite counting and permutation machinery; such lemmas can be shared beyond this paper. Contributions toward the six milestone statements, the goal, and faithful supporting results are in scope. Lemmas 6–12 and the printed EARLY Theorem 1 are outside this mission because their analysis depends on claims that fail for some matrices allowed by their surrounding assumptions.
Deterministic machine scheduling was one of the first application areas of the theory of NP-completeness. After Cook (1971) and Karp (1972) showed that a large family of combinatorial problems are polynomially equivalent, Brucker, Lenstra and Rinnooy Kan set out to locate the boundary between the polynomially solvable and the NP-complete scheduling problems. Their report Complexity of Machine Scheduling Problems (Mathematisch Centrum, Report BW 43/75, 1975; journal version in Annals of Discrete Mathematics 1, 1977) introduced the four-field notation that, in refined form, is still the standard classification of scheduling problems, and proved NP-completeness of the "easiest" hard problems by explicit reductions.
Single-machine problems with due dates sit right at that boundary. Minimizing the maximum lateness is solved by Jackson's earliest-due-date rule (1955), and minimizing the number of late jobs by Moore's algorithm (1968). Theorem 4 of the report shows that small changes to these problems — one release date, job weights, or due dates turned into deadlines under a weighted completion-time objective — make them NP-complete, by reduction from KNAPSACK. This mission formalizes four of those reductions, parts (b), (c), (e) and (f) of Theorem 4.
Timeline, as far as this mission is concerned:
A single-machine instance consists of jobs . Job needs units of processing on the machine , has a weight , a release date and a due date ; all data are nonnegative integers. A schedule assigns to each job a starting time such that the occupied intervals of distinct jobs are disjoint. Idle time is allowed; a job with occupies an empty interval. The completion time is , the lateness is (possibly negative), and is if and otherwise. The criteria are
The problem class is written in the field: by default every ; allows a nonzero release date for the last job only; fixes unit weights; admits only schedules that meet every due date. A problem is turned into a yes/no question by asking whether a schedule with value exists.
KNAPSACK (Theorem 2(b) of the report): given positive integers , is there a subset with ? Write .
A problem is reducible to , , if every instance of can be transformed in polynomial time into an instance of whose answer is the same.
as polynomial-time many-one reductions between languages of binary strings.
For positive with , and the paper's constructions:
The result. Combined with the NP-completeness of KNAPSACK, the four reductions show that the four problems are NP-hard (in the ordinary sense; they admit pseudo-polynomial algorithms). Part (c) shows that Jackson's rule cannot be extended to a single nonzero release date unless P = NP; part (f) does the same for Moore's algorithm; part (e) explains why weights are essential in the late-jobs problem; part (b) shows that deadlines turn the weighted completion-time problem, solved by Smith's ratio rule without them, into a hard one. These are entries of the complexity tables that every later scheduling classification builds on.
Formalizing it. The reductions are classical and proved on paper, in a few lines each: for (c), (e) and (f) the report gives only the construction and a figure. None of them has a machine-checked proof. A complete formalization supplies the explicit equivalence over all feasible schedules (including schedules with idle time and arbitrary processing order), the handling of the inputs the proof sets aside by "we may assume that ", and the polynomial-time computability of the constructions in a Turing-machine model.
Each equivalence has an easy direction: a subset with sum gives the schedule "jobs of , then , then the rest" (Figures 4 and 7 of the report). The other direction must rule out every feasible schedule, not only the idle-free ones in the displayed order. The report gives no argument for this direction in (c), (e) and (f), and for (b) only a computation for idle-free schedules of one shape. The equivalences are false outside in some cases (for (c), any makes every schedule on time), so the goal's reduction must treat those inputs separately.
The heavier part is polynomial-time computability: the reduction must be a function on strings, computed by a one-tape Turing machine within a polynomial number of steps, that parses a binary-coded KNAPSACK instance, computes and the threshold (for (b), a sum of products), and writes the coded scheduling instance — and maps malformed strings outside the target language.
Fin n (0-based; is the last index), with in each target language. Starting times are natural numbers: Section 3 computes them from processing orders on integer data, and since all criteria here are regular and release dates survive left shifts, real starting times give the same yes-instances. Feasibility requires disjoint occupied intervals, including empty intervals when . Idle time is allowed. Lateness is an integer.CookPvsNP.PolyReducible from the published definition CookPvsNP_defs. The alphabet and binary number codes are those of the published definition ProjSchedTW.Complexity.Encoding (Neumann, Schwindt and Zimmermann); its SUBSET SUM language is not reused because it admits zero sizes, while the paper's KNAPSACK is over positive integers.Parts (a), (d) and (g)–(j) of Theorem 4 are formalized in other missions of this series.
Many combinatorial optimization problems ask for the largest value of a linear objective over discrete feasible solutions. A linear program over the convex hull of those solutions has the same optimum, so one approach is to describe that hull by inequalities. For matching, for example, inequalities support efficient optimization; for other problems, the full family can be very large. A generator of violated inequalities offers a different interface: given a proposed point, it either certifies hull membership or produces one valid inequality that the point violates. Karp and Papadimitriou asked what the existence of an efficient generator implies for the underlying decision problem. Their answer is Theorem 2 of the technical report.
The report appeared as MIT/LCS/TM-154 in 1980 and later in SIAM Journal on Computing in 1982. Its first theorem addresses a small facial description whose inequality family belongs to NP. This mission concerns its second theorem, where the inequalities may be generated on demand in polynomial time. The conclusion is stronger: the decision language itself belongs to P. The report derives an NP-complete consequence as Corollary 2, conditional on the unresolved equality P = NP. The published article gives the later bibliographic record; all numbering here follows the technical report.
A combinatorial optimization problem consists of a binary input language , a nonnegative integer dimension , and a set of feasible vectors for each . The report requires polynomial-time recognition of , of correctly sized pairs , and of feasible pairs . An instance adds an integer objective . Its threshold decision language is
Write for the convex hull of the feasible vectors. A generator receives and a rational vector . It returns “O.K.” exactly when belongs to the hull. Otherwise it returns an integer vector and integer for which while for every . The family contains every triple that occurs as some output. It is a facial description because its inequalities describe the hull exactly. The generator is small if one polynomial bounds every coefficient in every output by in absolute value. Its running time is measured on the full encoded query, including every rational coordinate. These definitions are from §§2 and 4 of the report.
The goal is the report's stated implication:
It allows any c.o.p. satisfying Definition 1, including an empty feasible set or dimension zero. It does not assert P = NP; that consequence needs the additional hypothesis that is NP-complete. The goal is supported by five source claims: the output family is facial; feasibility of system (4) is equivalent to membership in ; Lemma 4 bounds the distance from a rational point to a small hyperplane; its Corollary extends the bound to a real point on a flat; and Lemma 5 controls distance to a flat after one more hyperplane is added. The system (4) target is
The distance targets use the report's parameter and the bounds and , exactly as printed on pp. 12–13.
Theorem 2 turns an efficient separation interface into an efficient test for the threshold language. Consequently, if a c.o.p.'s decision language is NP-complete, a small polynomial-time generator would imply P = NP, as the report's Corollary 2 says. This gives a complexity barrier to a whole class of proposed cutting-plane interfaces, independently of how many inequalities the complete description contains. The result concerns the worst-case running time and output coefficient size; it does not rule out useful generators without those guarantees. Karp and Papadimitriou also point out positive applications to problems already known to be in P.
The mathematical theorem was proved in the report. The mission asks for a machine-checked version of that known result, with explicit interfaces for the generator, coefficient bounds, and the underlying complexity class. The local platform catalog already contains Cook's Turing-machine definitions and a reusable binary-integer encoding; it also contains point-to-hyperplane distance results and a Gram-determinant distance result in other settings. Theorem 2 and these particular source claims are new formalization targets here. The distance and encoding interfaces can serve later missions about separation oracles and bit complexity.
Calling the generator once does not by itself decide whether the objective threshold is attainable: the point supplied to it may be outside the hull, and a single returned inequality says only that this point is excluded. Repeatedly asking at an unchanged point may return the same inequality. The report must also control very small separations, coefficient sizes, and finite precision when an iterative linear-feasibility procedure uses the oracle. Lemmas 4 and 5 quantify the geometric gaps and movement that such a procedure needs. Its Lemmas 2, 3, and 6 address the surrounding perturbation, volume, and iteration arguments; Lemma 6 explicitly relies on another analysis for the finite-precision bound. These are substantive proof obligations even though their statements are not all separate milestones in this proposal. See §4 of the report.
The report's footnote uses for the rationals. Thus , the hull, and system (4) live in . Euclidean distances are evaluated after casting coordinates into ; a hyperplane distance is the quotient , and distance to a flat uses Euclidean infimum distance. The report does not define “affinely independent hyperplanes”; this mission reads it as linear independence of their normals, which ensures a common flat. Small hyperplanes have nonzero normals, avoiding a zero denominator.
The alphabet is . Binary tuple codes contain , an explicit vector dimension, and every integer; a rational coordinate contains its reduced numerator and denominator. The generator's string function must match the mathematical oracle on every valid query and be polynomial time in the complete code length. A malformed string is outside . The source's arbitrary polynomial bound is written for one exponent fixed before all instances. For the bit-length parameter , the printed logarithms of possibly nonpositive and are read as ceiling logarithms of absolute values, with and the printed terms retained. The source's formula remains relevant to the eventual proof of Theorem 2, although no system is a separate draft item here.
Every oracle answer must separate the queried point and remain valid on all of ; these obligations prevent an arbitrary function from satisfying the goal. The c.o.p. structure retains all three polynomial-recognition conditions of Definition 1. The paper's displayed “min” in (3) is inconsistent with its threshold language and surrounding maximization formulas; uses the printed . The typed source's “” in Lemma 4 is read as the already named point .
Contributions can develop the rational-hull equivalence, the two quantitative hyperplane lemmas, the finite-precision ellipsoid procedure underlying Lemma 6, or the perturbation and volume claims. The complexity substrate is Cook's one-tape model of P and NP, and the binary integer codec is the published ProjSchedTW_Complexity_Encoding definition. The geometry lemmas are phrased so that existing Mathlib Euclidean-space results can be reused without changing the source's rational optimization domain.
Deterministic machine scheduling asks how to process a set of jobs on a set of machines so that an overall criterion, such as the time at which the last job finishes, is as small as possible. In the early 1970s many such problems had efficient algorithms (Johnson's rule for the two-machine flow shop, Smith's ratio rule for a single machine, Lawler's rule under precedence constraints), while others resisted every attempt. The report of Brucker, Lenstra and Rinnooy Kan (Mathematisch Centrum, 1975; journal version in Annals of Discrete Mathematics 1, 1977) drew the line between the two groups systematically. It fixed the four-field notation that the scheduling literature still uses, and it proved NP-completeness of the "easiest" hard problems by explicit reductions in the sense of Karp.
The first family of reductions in the report, Theorem 3, concerns the simplest machine environment beyond a single machine: two identical machines. It shows that already there, minimizing the makespan and minimizing the total weighted completion time are as hard as PARTITION. These two reductions are simplified versions of reductions given by Bruno, Coffman and Sethi (1974), reference [3] of the report.
PARTITION. Given positive integers , decide whether there is a subset of with
Write for the total.
Two identical machines. There are jobs and two machines . Job has a processing time and a weight , and must be processed without interruption on one machine of its choice; all jobs are available at time . A schedule assigns to every job a machine and a starting time ; its completion time is . A schedule is feasible if no two jobs on the same machine are processed at the same time, i.e. the intervals on each machine are pairwise disjoint. Idle time is allowed. Two criteria are considered:
The problems and ask for a feasible schedule minimizing the respective criterion.
Reducibility. Following Section 2 of the report, each problem is replaced by its recognition version: given an instance and a threshold , is there a feasible schedule with value ? A problem is reducible to , written , if every instance of can be transformed in polynomial time into an instance of with the same answer. Instances are written as words over a finite alphabet, with every number in binary.
Both reductions use the same instance shape: jobs with .
every feasible schedule with this assignment has value at least . 3. The identity for . With ,
The result. Since PARTITION is NP-complete (Karp 1972), Theorem 3 shows that both problems are NP-hard with only two machines and a single operation per job; their recognition versions are NP-complete. Together with the single-machine and shop results in the rest of the report, it places the boundary of tractability in deterministic scheduling. The makespan problem became a standard source problem for later hardness proofs and a standard target for pseudo-polynomial algorithms and approximation schemes. The weighted completion time result contrasts with the single-machine case, which Smith's ratio rule solves in polynomial time.
Formalizing it. The theorem is classical and fully proved on paper; the report prints the constructions and, for (b), a short calculation. To our knowledge no machine-checked proof exists. The mission produces (i) a precise model of nonpreemptive schedules on two identical machines with integer start times and idle time allowed, (ii) the two yes-instance equivalences with the paper's rational thresholds, (iii) the ordering-independence statement for behind part (b), and (iv) the polynomial-time computability of the reductions in a Turing machine model. Part (iv) is the formal content of "reducible" and is missing from the paper.
For part (a) the mathematics is short. The paper treats it as evident; a formal proof must still handle schedules with idle time and the case of odd , where is not an integer.
Part (b) rests on the claim that, when , the value does not depend on the order of the jobs on a machine. For a single machine without idle time this is a symmetric double sum. A recognition-problem proof also needs the converse direction: no schedule with idle time beats the non-idle one, so every feasible schedule with assignment has value at least . The paper cites this rather than proving it.
The step the paper leaves out entirely is polynomiality. The constructions copy the input and compute or , and in a one-tape Turing machine model with an explicit polynomial time bound this needs binary arithmetic (sums, products, a floor) carried out on the tape. It also needs a decoder that rejects malformed words and lists containing a zero. This is routine in principle but long in practice.
Fin n and machines Fin 2 (machine 0 is ). Starting times are natural numbers. Section 3 of the report computes them from processing orders on nonnegative integer data, and both criteria are regular, so real starting times would give the same yes-instances. Processing times may be zero; a zero-length job occupies the empty interval. Schedules may contain idle time.CookPvsNP.PolyReducible from the published definition CookPvsNP_defs (Cook's one-tape Turing machines, polynomial-time many-one reductions). The alphabet BSym and the binary code encNats are reused from the published ProjSchedTW.Complexity.Encoding (Neumann, Schwindt and Zimmermann). Its PARTITION language is not reused, because it allows zero sizes.BSym, which every mission of this series needs and which is reusable for other reductions on the platform.Many network-design and production-planning problems ask for a cheapest way to route a commodity from supply points to demand points when the cost of an arc grows less than proportionally with the amount sent: setup charges, economies of scale, and fixed-plus-linear costs all give concave arc costs. Minimizing a concave function over the flow polytope is NP-hard in general, and the classical linear-cost machinery (potentials, negative-cycle tests) no longer applies. Erickson, Monma and Veinott (Math. Oper. Res. 12 (1987)) gave the send-and-split method, a dynamic program over subsets of the demand nodes that solves the uncapacitated problem in time polynomial in the number of nodes and arcs and exponential only in the number of demand nodes. It contains as special cases the Dreyfus–Wagner recursion for Steiner trees in graphs (Networks 1 (1971)), and the paper applies it to concave-cost production, inventory and network-design problems (§6).
Timeline. Zangwill (1968) solved minimum-concave-cost flows on special networks by dynamic programming. Dreyfus and Wagner (1971) gave the subset recursion for Steiner trees with positive arc lengths. Erickson, Monma and Veinott (1987) extended the subset recursion to arbitrary uncapacitated networks with additive concave arc costs and arbitrary real demands, proved that the minimum costs of the subproblems form the greatest solution of the resulting equations (Theorem 2), and showed it is the only solution when every simple circulation has positive cost.
A network consists of a directed graph with nodes and arcs , ordered pairs of distinct nodes, together with a real demand vector . A preflow is a nonnegative matrix supported on ; a flow for is a preflow with inflow minus outflow equal to at every node. Each arc has a cost function , concave on with , and the cost of a preflow is . A minimum-cost flow is a flow whose cost is at most that of every flow. A simple circulation is a circulation equal to some on the arcs of a simple directed circuit and elsewhere.
The demand nodes are . For let . The subproblem keeps the demands of the nodes in , sets all others to zero, and subtracts at node ; is its minimum cost, when it has no flow. Let if and the reversed arcs if , with sending cost , read as when . The send-and-split equations for an array are
with for , and if , otherwise, for (3).
If there is a minimum-cost flow for , then
for all and . If moreover every simple circulation has positive cost, then every -or-real solution equals .
In attack order: the subproblem alternative (a minimum-cost flow or no flow, p. 640); equation (1); inequalities (4), (5), (6) (p. 641); for (p. 641); satisfies (1) and (2) (p. 642); and two generic statements about Bellman's equations (2)′ for minimum-cost chains in a graph with nonnegative, respectively positive, simple circuits: the minimum chain costs form the greatest solution and are nondecreasing in the arc costs, and with positive circuits the solution is unique (p. 642).
Theorem 2 is the correctness theorem of the send-and-split method: it says that solving equations (1)–(3) by increasing , with a shortest-chain computation for each , yields the true subproblem minimum costs, in particular the optimum of the original problem. Its uniqueness clause identifies when the equations alone determine the answer, and the counterexample on p. 641 (zero costs on a strongly connected graph) shows that the positivity hypothesis cannot simply be dropped. The same structure underlies the Steiner-tree recursion.
The theorem is proved in the paper; to our knowledge none of it is formalized. This mission supplies Lean definitions of uncapacitated concave-cost flows with extended-real minimum costs and the send-and-split equations, and poses the correctness theorem as a proof goal. The two Bellman milestones are general facts about minimum-cost chains with -or-real values and are reusable well beyond this paper. Related items on the platform are credited, not reused: the Dreyfus–Wagner Steiner recursion DreyfusWagner.Steiner.steinerLength_recurrence and DreyfusWagner.Steiner.optimal_decomposition (the special case of undirected positive lengths), and BellmanRouting.PolicySpace.routing_equation_unique (uniqueness of the routing equation on a complete graph with positive real times).
The equations (2) mix two minima: sending the whole demand across one arc, and splitting at the current node. Showing that satisfies them requires that some optimal flow of every subproblem has a tree-like structure, which in turn rests on the existence theory for concave-cost flows (an optimum is attained at an extreme flow whose support is a forest). Showing that is the greatest solution requires an induction on in which, for fixed , equation (2) is a shortest-chain system whose arc costs to an auxiliary node depend on the solution at smaller sets; comparison then needs monotonicity of minimum chain costs in the arc costs, including arcs whose cost drops from . The naive attempt to prove uniqueness by iterating (2) fails without the positivity hypothesis, because zero-cost circuits admit spurious solutions.
Nodes are Fin n; arcs are a Finset (Fin n × Fin n) with no loops; arc costs are functions assumed concave on Set.Ici 0 with at arcs (the paper's standing assumption, stated as a hypothesis). Minimum costs, sending costs, splitting terms and solutions take values in EReal; the empty infimum is , as on the page.
Explicit readings of the paper's phrases:
The definition of is the infimum over flows, never the equations themselves; a formalization defining by (1)–(3), or omitting the condition on solutions, or dropping the clause that is itself a solution, would make the theorem trivial or false and is ruled out. Arrays are compared only on admissible sets. The graph structure of (2)′ is the platform definition BertsekasSPGraph. Running-time bounds, the planar refinements of §4 (Theorem 3) and the capacitated reduction of §5 are out of scope. Proofs of any milestone, and a formalization of the paper's Theorem 1 that the proofs rely on, are welcome.
In airline and hotel revenue management a firm sells a fixed stock of a perishable resource (seats on a flight leg, rooms on a night) over a finite selling horizon, and in each period decides which fare classes to open. Customers do not buy a fixed fare: they choose among the fares on offer, or leave. Talluri and van Ryzin (Management Science, 2004) formulated this single-leg, choice-based problem as a dynamic program over the time remaining and the units remaining.
Practical revenue management systems rarely offer arbitrary sets of fares. They use nested controls: fares are opened from the most expensive downwards, so the open set is always "every fare above some threshold". Whether restricting to such revenue-ordered offer sets is natural depends on how the optimal threshold moves as the state changes. For mixtures of multinomial logit models, Rusmevichientong, Shmoys, Tong and Topaloglu (Production and Operations Management, 2014, Theorem 6) showed that the best revenue-ordered threshold moves monotonically in both the remaining capacity and the remaining time.
Berbeglia and Joret (arXiv:1606.01371v3, §5, Theorem 5.1) extend these two monotonicity properties to every regular discrete choice model, the class that contains essentially every model used in revenue management, including all random utility models. This mission formalizes that result.
A finite nonempty set of products is sold. For a choice set and a product , is the probability that a customer offered buys ; the no-purchase probability is . The system is regular when (i) all these probabilities are nonnegative, (ii) for , (iii) , and (iv) whenever , for every and for the no-purchase option .
Each product has a revenue . Let be the distinct revenues. For the revenue-ordered assortment is ; a larger index gives a smaller set, .
In the multi-period model one customer arrives per period. With periods remaining and units left, the firm offers some . The values of the revenue-ordered dynamic program are
when or , and . The optimal revenue-ordered index is the smallest maximiser,
and is the marginal value of capacity.
For every and ,
More units left give a weakly larger optimal offer set; more periods left give a weakly smaller one. The paper states the theorem for , ; the horizon and the capacity only bound and , so the goal is stated for all .
Milestones 5–7 are asserted or cited in the paper, not proved there; milestones 6–7 are stated for this restricted dynamic program, which is the one the paper applies them to.
The theorem says that a firm restricted to revenue-ordered offer sets can implement its policy as a nested booking control: as seats sell out, the threshold fare can only rise, and as departure approaches with seats in hand, it can only fall. This is the structure that standard revenue management systems already assume, and Rusmevichientong et al. point out that such monotonicity can be used to implement them. The paper's contribution is that the property depends only on regularity of the choice model, not on its multinomial-logit form.
Formalizing it adds a machine-checked statement of the single-leg choice-based dynamic program over a general choice model, a precise account of the tie-breaking rule (the smallest maximiser), and machine-checked versions of the two marginal-value monotonicity facts that the paper cites from Talluri and van Ryzin rather than proves. To our knowledge none of these statements has been formalized in any proof assistant; the paper's proofs are informal.
The paper's proof is short, but two of its steps are not proved there. The marginal-value inequalities are imported from Talluri and van Ryzin, whose dynamic program optimises over all offer sets; here only the revenue-ordered sets are available and the empty set is not, so those proofs have to be redone for this program, and the bound is needed to keep each stage's shifted problem well behaved. The claim itself is justified on the page only by an informal sentence.
The second subtlety is tie-breaking. The monotonicity is about the smallest optimal index. Several indices can be optimal at once, and the comparison of Lemma .1 transfers optimality of one index from one shift to another only through Lemma 2.1, that is, through the no-purchase case of the regularity axiom. Without that case the statement fails.
C; choice probabilities are P : C → Finset C → ℝ, defined on all pairs. The no-purchase option is not a product: its probability is the derived quantity noPurchase P S = 1 − ∑_{x∈S} P x S.IsChoiceSystem P is axioms (i)–(iii); IsRegular P adds axiom (iv) for products and for the no-purchase option. Milestones 5–7 assume only axioms (i)–(iii), as the paper says suffices; Lemma .1, (16), (18) and the goal assume regularity and .level r ℓ is for , topRevenue r is , and roSet r ℓ is as a Finset. The paper's sorting of products () is notation only and is not used.Finset.sup', and the minima defining and are Finset.min' over sets proved nonempty.Formalizations that would trivialize the statement are ruled out: the dynamic program maximises over the revenue-ordered sets only, never over all subsets (that is Talluri and van Ryzin's program); is the smallest maximiser, never the largest; and , , and the choice model are arbitrary, never fixed.
The definitions (regular choice model, revenue-ordered assortments, the restricted dynamic program) are reusable for other results on nested policies. Proofs of the cited Talluri–van Ryzin lemmas for this program are especially welcome, as they are the part the paper leaves to the literature.
A retailer who controls both inventory and price can respond to a supply contract in two ways. A contract that induces the right order quantity at a fixed price may change the retailer's incentive to raise or lower that price. For a one-season supply chain, Cachon's chapter compares familiar contracts under price-dependent demand and identifies a price-contingent buy-back, also called a price-discount contract, that aligns both decisions. The mission concerns §6.3 of the author's January 2003 third draft, on printed pages 33–38. Those page and equation numbers belong to the draft and may differ from the typeset chapter.
One risk-neutral supplier and one risk-neutral retailer have full information before a single selling season. The retailer chooses a nonnegative stocking quantity and a retail price from an admissible price set ; the price stays fixed during the season. Demand has a probability law that depends on . Write for its distribution function, for expected sales, and for mean demand. Demand is nonnegative, has a finite mean and, in the chapter's regular setting, its distribution function increases with demand level and has a positive price derivative at positive demand levels. Higher prices thus lower demand in the stochastic order used by the chapter. The price set is nonempty and open so an admissible price optimum has an interior first-order condition.
The supplier's unit cost is , the retailer's unit procurement cost is , and is total unit cost. Their goodwill penalties for unmet demand are and , with . An unsold unit has salvage value at the retailer. The integrated channel's expected profit is
A buy-back contract charges a wholesale price for each ordered unit and pays the retailer for each unsold unit. A revenue-sharing contract charges a wholesale price and gives the retailer a fraction of sales and salvage revenue. In this section the supplier offers the terms and the retailer chooses . The profit formulas use the chapter's convention that a positive transfer goes from retailer to supplier.
The goal is the price-contingent buy-back on p. 35, with :
In the chapter's zero-goodwill case, , every feasible then gives the retailer and the supplier . The same retailer profit is obtained from revenue sharing with and . Thus every existing maximizer of the integrated profit maximizes each firm's profit under the contingent buy-back. At the retailer is indifferent; at the supplier is indifferent.
The milestones follow the chapter's printed claims in attack order:
The result identifies a contract schedule under which the same quantity-price pair is best for the integrated channel and for the two firms' reported profit functions. It also explains the relation between a buy-back whose terms vary with the chosen price and a revenue-sharing arrangement. In the zero-goodwill setting, both allocate every realized choice's expected channel profit in fixed shares. The general-goodwill identity shows the additional mean-demand terms that matter when the retailer controls price.
The source presents these results analytically; this mission asks for Lean proofs of the stated price and profit relationships. A published Prove2Me definition already supplies expected sales and mean demand for a single demand law, and the model here applies those functions to each price's law. The earlier open theorem RevShareCoord.Single.price_quantity_coordination (from Cachon and Lariviere's revenue-sharing paper) treats deterministic revenue and a simpler cost convention. It is an overlap in theme, but its statement does not include price-indexed demand, salvage value, retailer cost or the contingent buy-back terms, so it is not posed again here. The new model can support further price-dependent contract comparisons in the chapter.
The obstacle is that matching the retailer's quantity incentive at a fixed price can change the retailer's price incentive. The buy-back rate required by the fixed-price coordination equations depends on ; a fixed buy-back contract therefore does not generally align both choices. Revenue sharing with goodwill penalties has a similar price dependence. The integrated profit need not be concave or unimodal in , so a price first-order condition by itself does not establish coordination. The chapter assumes a finite integrated optimum exists and treats the price condition as necessary, not sufficient.
Lean represents price-dependent demand as a family of probability measures on , one for each price in . Each admissible law is supported on nonnegative demand, has no atom at zero and has an integrable identity function, so is a genuine finite expectation. Sales are defined by , using the published SupplyChainTheory_contracts definition; they are not defined by the equivalent CDF integral. The admissible decisions are exactly and . Unit costs and goodwill penalties are nonnegative, each admissible price exceeds , and , as in the model of §6.2. The chapter's standing risk-neutrality and full-information conventions appear in the use of expected profit with the same demand laws available to both firms.
There is a material qualification. With price-dependent demand, may change with . The printed first-order condition (14) and the p. 36 inference from to a joint optimum omit that effect when goodwill penalties are positive. Price first-order and optimality statements here therefore use , a case explicitly discussed in the chapter; general-goodwill claims are limited to algebraic identities. The printed p. 36 equality of price derivatives under revenue sharing also misses its factor , which the formal statement restores. The contingent buy-back terms are defined by the chapter's linear formulas, not by a property that hard-codes coordination. The algebraic statement permits parameter values that may violate economic buy-back bounds such as ; those bounds need separate checks when selecting a contract.
Two first-order statements, (15) and (16), compare price derivatives; they take the derivative of expected sales in price as a hypothesis, and (15) also takes differentiation under the integral sign of as a disclosed regularity hypothesis. For the quantity discount, the statement claims what the page shows, undistorted prices for each and optimality of given , not joint optimality of for the retailer. The page's claim that revenue sharing with goodwill coordinates only with is not stated, for the mean-demand reason above.
A trivializing formalization is ruled out: no contract term is defined by the profit identity it should satisfy, the demand family cannot be replaced by a single law, and the optimal pair is a hypothesis about the integrated profit, not a chosen witness.
Reusable contributions include the price-indexed demand family, the expected-profit model with five contract types, and the price-maximizer statements. Proofs of the first-order milestones need Fermat's interior-extremum theorem on the open price set and, for (15), positivity of an interval integral; the identities need the expectation algebra of and , including .
Polyhedral combinatorics attacks a combinatorial optimization problem by replacing its finite set of feasible solutions with the convex hull of that set and describing the hull by linear inequalities. Once such a description is known, the problem becomes a linear program, and linear programming duality supplies optimality certificates. For matchings, matroids and network flows this programme succeeded completely (Edmonds' matching polytope is the classical example). For the traveling salesman problem, set covering and integer programming, decades of work produced large families of valid and facet-defining inequalities but never a complete list.
R. M. Karp and C. H. Papadimitriou asked whether the failure is accidental. Their answer, in the MIT technical report On linear characterizations of combinatorial optimization problems (MIT/LCS/TM-154, February 1980; journal version SIAM J. Comput. 11 (1982) 620–632), is that for NP-complete problems a usable complete description cannot exist unless NP = co-NP. This mission formalizes the first of their two complexity results, Theorem 1, together with the steps of its proof and its Corollary 1.
A combinatorial optimization problem (c.o.p.) consists of a set of inputs, a function assigning to each input a number of variables , and for each a set of nonnegative integer vectors, the feasible solutions. The three languages , and must be recognizable in polynomial time. An instance is a pair with and , and the decision problem of is
Write for the convex hull of over the rationals. A facial description of is a set of triples , with , and , such that for every and every
It is small if for some polynomial every component of every triple has absolute value at most , so that each coefficient has polynomially many bits. The statement means that the language of the triples of is in NP: membership of a listed inequality has short, checkable proofs.
Theorem 1 converts a question of polyhedral combinatorics into one of complexity theory. Corollary 1 then says that for the traveling salesman problem, Hamiltonian circuit, set covering, integer programming and every other c.o.p. with an NP-complete decision problem, no complete linear description of the hulls has both polynomially sized coefficients and polynomially verifiable membership, unless NP = co-NP. This explains why the search for complete descriptions of such polytopes has not succeeded and why research on them turned to partial descriptions and separation. The companion result of the same paper (Theorem 2, the subject of the second mission in this series) treats separation routines and P instead of facial descriptions and co-NP.
The result itself is proved, by a short argument in the paper. To our knowledge it has no machine-checked proof. Formalizing it requires connecting three things that the platform holds only separately: Cook's Turing-machine classes P, NP and co-NP (published as CookPvsNP_defs), linear programming duality over the rationals (Farkas' lemma is published, e.g. LinearOptimization.farkas_inequality_form_fintype, for real matrices), and polynomial-time arithmetic on binary-encoded rational data, such as solving a nonsingular integer linear system. The last ingredient, a polynomial-time verifier built from a polynomial-time recognizer, is reusable for every co-NP or NP membership proof on the platform.
The mathematical content of Theorem 1 is the duality chain (i)⇔(vi): the "no" answer is certified by inequalities of and a basic dual solution. Two points make the formal proof harder than the paper's page suggests.
First, the duality chain needs care at its edges. When is empty the chain (iii)⇔(vi) can fail, so the verifier must also accept a different certificate (an infeasibility certificate from at most triples), while milestone 4 carries the hypothesis . Pointedness of the hull, which follows from , is what guarantees linearly independent rows.
Second, "Algorithm B clearly runs in polynomial time" hides a complete complexity argument on Cook's one-tape machines: parsing the input, testing and with the recognizers of Definition 1, guessing the matrix within the size bound given by smallness, invoking the NP verifier of times, and solving exactly over with polynomially bounded bit sizes (Cramer's rule bounds the numerators and denominators of ). The certificate must be of length polynomial in the input, which uses the uniform polynomial in the definition of "small". The naive certificate, a single optimal vertex of the hull, does not work: it proves a "yes" answer, not a "no".
All definitions live in the namespace KarpPapadimitriou.Facial. Strings are List Bool; is a set of Fin (n z) → ℤ with nonnegative entries; is convexHull ℚ of its image in Fin (n z) → ℚ, because the paper's "R" denotes the rationals (footnote, p. 3). Tuples are coded over the four-letter alphabet of the published ProjSchedTW_Complexity_Encoding, integers in binary, vectors prefixed by their length so that codes are uniquely decodable. P, NP, co-NP and NP-completeness are the published CookPvsNP_defs; and the triple language of are sets of codes, so strings encoding no triple lie in the complement of , as in Algorithm B's step (i). The three polynomial-time conditions of Definition 1 are fields of the structure COP.
Explicit readings of the paper's loose phrases:
Printed slips: display (3) reads "min" while and the proof maximize; Algorithm B's step (v) reads "" for . Both are formalized in the corrected sense.
A trivializing formalization is ruled out: the goal quantifies over every c.o.p. and every small facial description, with complements taken over all strings, and no hypothesis restricts or beyond Definition 1 and the definitions of p. 4–5. Claim 1 (p. 9), announced without proof, is not part of the mission.
Contributions welcome: proofs of the four milestones (milestone 4 is an exercise in rational LP duality on finite systems), a reusable library of polynomial-time integer and rational arithmetic on Cook's machines, and the closure of NP under polynomial-time reductions across alphabets that Corollary 1 needs.
A minimum-cost circulation is a way to send flow around a directed network while respecting capacities and paying a cost per unit on each arc. It is a basic form of network optimization: a minimum-cost flow with prescribed supplies and demands can be reduced to a circulation problem, and the circulation formulation exposes the residual arcs on which a flow can be improved. Goldberg and Tarjan's successive-approximation method relaxes exact optimality by an error parameter and repeatedly reduces that error. Its ordinary stopping rule for integer costs depends on the largest cost. For arbitrary real costs, including irrational costs, a decreasing positive error need never cross a fixed numerical cutoff. The strongly polynomial loop in their 1987 technical report, later published in Mathematics of Operations Research instead tests the smallest error parameter appropriate to the current circulation and stops when it is zero.
This mission formalizes the number of refinement calls made by that loop. It builds on the related Goldberg–Tarjan 1988 max-flow and 1989 minimum-mean cycle-canceling series: those develop different algorithms for network flow, while the published 1989 circulation and approximate-optimality definitions provide this mission's common network model. The result here concerns successive approximation and its fixed-arc progress measure.
The vertex set is finite, with , and is a symmetric set of directed arcs, with . Symmetry means that brings too. Each arc has a real capacity and a real cost ; costs obey . A circulation obeys , , and conservation of flow at every vertex. Its total cost is half the sum of over directed arcs, since each unordered edge appears twice. A minimum-cost circulation costs no more than any other circulation of the network.
The residual capacity is . For a price function , the report writes the reduced cost as . A circulation is -optimal with respect to when every residual arc has reduced cost at least . It is -optimal if some price function works, where . The tight error is the least such error. A circulation is -tight when it is -optimal but fails to be -optimal at every . This includes attainment at .
An arc is -fixed if all -optimal circulations carry the same flow through it. Write for the set of these arcs. Theorem 4.2 supplies an arc-fixing criterion from a large absolute reduced cost. Lemma 4.4 says that when a positive tight error falls by a factor of , becomes strictly larger. Both are numbered results on printed pages 16–17 of the source report's journal counterpart.
The goal is the circulation-level form of Theorem 4.5. Begin with a circulation and a sequence whose positive-error steps satisfy the contract of Figure 3: if , the next circulation is -optimal. With the report's standing and , the target is
The milestone list contains the already proved complementary-slackness characterization of minimum cost (Theorem 2.2), the cross-parameter arc-fixing result (Theorem 4.2), and strict growth of fixed arcs (Lemma 4.4). The report states Theorem 4.5 as iterations when each refinement decreases error by a constant factor. The target makes explicit the factor two used by the paper's refinements and the resulting finite count.
The theorem gives a bound on the number of refinement calls that depends on the number of vertices and arcs, not on the magnitude, precision, or integrality of the costs. It gives an exact minimum-cost circulation rather than an arbitrary small-error approximation. This distinguishes the real-cost loop from an integer-cost stopping rule based on . The bound counts refinement calls only; the report analyzes the work within particular implementations separately.
The published 1989 definitions and the complementary-slackness theorem already have machine-checked status on the platform. Theorem 4.2, Lemma 4.4, and this iteration theorem are the open formalization targets. A complete development will connect the tight error to residual-cycle structure, establish that its infimum is attained for circulations, and prove that zero tight error implies minimum cost. The mission thereby makes the fixed-arc argument reusable for other circulation algorithms that lower an approximate-optimality parameter.
Repeatedly dividing a positive real error by two gives errors approaching zero, but it does not by itself produce a finite step with zero error. The missing finite progress is structural: an arc must become fixed after enough reductions, and only finitely many arcs exist. Proving that fixedness is strict is delicate because it compares all circulations at two different error levels, not just two consecutive flows. Theorem 4.2 is the quantitative bridge between a price certificate for one flow and agreement of an arc across every sufficiently accurate flow. At the boundary , the printed wording of Lemma 4.4 would require to be a proper subset of itself, so its positive-error regime must be made explicit.
The Lean network uses CycleCanceling.MinMean.CircNetwork with a finite vertex type, a finite symmetric arc set, and real-valued capacities, costs, and flows. Off-arc values of these functions are irrelevant. The report assumes on printed page 5; the theorem binders express it as and . The arc count is for ordered arcs, exactly as the report defines . No integrality, rounding, or bounded-cost hypothesis is imposed. A feasible initial circulation is required because Figure 3 starts from one; infeasibility detection is outside this target.
The reused 1989 definitions write reduced cost as . Substituting for gives the report's , so existential price certificates, -optimality, and absolute reduced-cost conditions agree. The tight error is represented by a real infimum; proving that it is attained is part of the work. The set is filtered from and includes only arcs whose flow is shared by all -optimal circulations. The halving run computes its error from the current circulation; it does not take an unrelated error sequence. Once that error is zero, the loop has returned and later sequence entries are unconstrained. These choices exclude a vacuous or artificially fixed error parameter and a preselected optimal flow.
The explicit reading of the report's asymptotic count is halvings per factor- reduction and at most such blocks, giving refinements. This is a statement about refinement count, not a RAM-operation bound. Contributions on Theorem 4.2, the residual-cycle characterization of positive tight error, the fixed-arc strictness lemma, and the final finite counting argument all support the goal. The circulation, price, and fixed-arc infrastructure can be reused beyond this particular implementation.
A retailer that can display only some of its products must choose an assortment: the set of products offered to an arriving customer. Customers substitute: whether a given product is bought depends on what else is on the shelf. The assortment problem asks for the offer set that maximises expected revenue under a model of this substitution behaviour. It is a core problem of revenue management (Talluri and van Ryzin, Management Science 2004), and it is NP-hard already for a mixture of two multinomial logit models (Rusmevichientong, Shmoys, Tong and Topaloglu, POMS 2014).
The heuristic used most widely in practice is revenue-ordered assortments: sort the products by price and offer, for some threshold, every product priced at least that threshold. It is optimal under the multinomial logit model (Talluri and van Ryzin 2004) but not in general. Berbeglia and Joret (arXiv:1606.01371v3, 2019; Algorithmica 2020) give a tight analysis of its approximation ratio for every regular discrete choice model, a class that includes all random utility models. They prove three incomparable guarantees. This mission formalizes the third, Theorem 3.3, whose ratio depends on the purchase behaviour of an optimal assortment rather than on the prices. Companion missions in this series cover the price-ratio bound (Theorem 3.2) and the tightness of all three bounds (Theorem 3.4).
Let be a finite nonempty set of products. A system of choice probabilities gives, for every offer set and product , the probability that a customer offered buys . Buying nothing is the option , with . The model is regular when
Axiom 4 at says that enlarging the offer set never makes buying nothing more likely.
Prices are a function . Offering earns , and . Let be the distinct values of , and let for . The revenue-ordered strategy earns
For an assortment , the purchase profile is
the probability that a customer offered buys something priced at least . It is non-increasing in .
Let be optimal, , suppose , and let be maximum with . Then
The first inequality is the paper's sum-form factor, the bound that Theorem 3.4 shows to be tight. The second is the closed form .
Theorem 3.3 gives a guarantee that is independent of prices. The bound of Theorem 3.2 grows when prices are spread out. The bound is small whenever an optimal assortment sells its expensive products with probability comparable to its overall purchase probability. In §4 the paper combines it with a reduction from unit-demand pricing to derive, for example, the guarantee of uniform pricing for the unit-demand min-pricing problem (Corollary 4.8, originally due to Aggarwal et al.). Together with Theorems 3.1 and 3.2, it describes the performance of the most common assortment heuristic over the whole class of regular models, with no parametric assumption on customer behaviour.
The theorem is proved on paper. To our knowledge it has no machine-checked proof, and no regular choice model has been formalized on the platform. This mission produces the regular model as a reusable definition, a statement of Theorem 3.3 in which every hypothesis is explicit, and formal versions of the proof's identities and inequalities. The logarithmic step is asserted without proof in the source, so a formal proof of it completes the paper's argument.
Each step is elementary. The difficulty is bookkeeping. The revenue of has to be regrouped by distinct price levels rather than by products: several products may share a price, and counts values. The regrouping uses an Abel-type rearrangement with the boundary convention . Comparing with the purchase probability of needs regularity twice. First, axiom 4 for products passes from to . Then the no-purchase case passes from to . A proof that uses axiom 4 only for products fails at the second step, and the claim is false without it.
C with [Fintype C] [DecidableEq C]. The goal adds [Nonempty C], the paper's . Offer sets are Finset C, and is P : C → Finset C → ℝ. The no-purchase option is not a product: is the derived quantity noPurchase P S. IsRegular P carries axioms 1–4, including both no-purchase cases.Finset.sup' over all subsets. is Finset.sup' over the indices of the threshold sets only.level r i is for . purchaseProfile P r S i is for and otherwise, which builds in .Real.log, applied to .The following statements are trivial or false and are not this mission: a maximum over all subsets in place of ; regularity without its no-purchase case; a purchase profile taken from a non-optimal set while is still called the optimum; the logarithmic form alone; a specific choice model (MNL, Markov chain) in place of an arbitrary regular .
A complete development needs finite sums regrouped by the values of a function and an elementary logarithm inequality. The regular choice model and the revenue-ordered sets are shared with the other missions of this series and are reusable for any analysis of assortment heuristics. Proofs of any milestone are welcome. So are alternative arguments for the logarithmic step and a proof that is non-increasing.
Policy gradient methods optimize a parameterized policy of a Markov decision process by gradient ascent on its expected discounted return. They underlie much of modern reinforcement learning (REINFORCE, actor–critic methods, TRPO, PPO), yet the objective is non-concave in the parameters, and until recently even the most basic question was open: does exact gradient ascent, run on a finite MDP with the standard softmax parameterization, reach the optimal values at all?
Agarwal, Kakade, Lee and Mahajan (arXiv:1908.00261v5, JMLR 22(98), 2021) answer this in the affirmative. Their Theorem 5.1 shows that unregularized softmax policy gradient with a small constant step size converges to the optimal value at every state, provided the start distribution used for the gradient puts positive mass on every state. The result is asymptotic: no rate is given. Later work (Mei, Xiao, Szepesvári and Schuurmans, ICML 2020, arXiv:2005.06392) obtained an rate with constants that can be exponentially large, and the same paper by Agarwal et al. gives polynomial rates once a log-barrier regularizer is added (its Corollary 5.1) or once the natural gradient is used (its Theorem 5.3). Theorem 5.1 is the unregularized baseline for all of these.
A finite MDP consists of finite sets of states and of actions ( nonempty), a transition kernel , rewards and a discount factor . A policy assigns to each state a probability vector on . Its value is the expected discounted sum of rewards when actions are drawn from ; its state–action value is and its advantage is . For a distribution on states, , and the discounted state visitation distribution is . A policy is optimal if for every policy and every state ; .
The softmax policy with parameters is
Softmax policy gradient ascent with step size produces, from an arbitrary , the iterates
The Lean development names these softmaxPolicy, softmaxValue P r γ µ θ , and IsSoftmaxPGRun P r γ µ η θ for the update rule; PolicyValue, QFunction and IsOptimalPolicy are the published FoundationsML definitions, and valueAt, advantage and visitation are the series' shared layer.
If for every state and , then for every state
The goal states only convergence to the optimal values, with the paper's constants in the step-size bound; no rate is claimed.
The theorem establishes that the non-concavity of the softmax objective does not trap exact gradient ascent: from any initialization, the values of the iterates converge to at every state, not only on average under . It is the reference point for the rate results of the same paper (log-barrier regularization, natural policy gradient) and for the subsequent literature on softmax policy gradient rates and lower bounds. It also isolates the role of exploration in the start distribution: Remark 5.1 of the paper leaves open whether can be dropped.
The result is proved in the paper; to the knowledge of the mission authors none of it is formalized in Lean or any other proof assistant. A complete development would provide a machine-checked gradient formula for the softmax class, smoothness bounds for discounted values, and a monotone-improvement argument for policy gradient, each reusable for other parameterizations and other policy optimization methods.
The obvious route fails. The gradient domination property of the direct parameterization (Lemma 4.1 of the paper) would conclude from , but under softmax , so a vanishing -gradient says nothing once some action probabilities vanish, and the iterates do drive probabilities to zero while parameters diverge. A smoothness-based argument therefore gives only stationarity in the limit. The asymptotic analysis must instead track which actions keep positive limiting advantage, how the individual parameters move once the advantage signs are frozen, and why an action with strictly positive limiting advantage cannot coexist with the behaviour of the remaining parameters. Lemmas C.7–C.12 carry that bookkeeping; the limiting sets and the existence of the limits are themselves consequences of the pointwise monotone improvement of Lemma C.2, which needs its own smoothness bound.
Standing setting of §3: finite types S, A with decidable equality, A nonempty; IsFiniteMDP P r γ (a transition kernel, rewards in , ); IsDist µ. Parameters live in EuclideanSpace ℝ (S × A), so norms are and Mathlib's gradient is ; the coordinate of the gradient is . Logarithms do not appear. Conventions committed to:
PolicyValue πstar P r γ s for a policy πstar with IsOptimalPolicy πstar P r γ, optimal simultaneously at every state; it is not a real supremum over all functions.Tendsto … atTop atTop / atBot; "strictly increasing for " is StrictMonoOn on Set.Ici T1, with existentially quantified.The goal theorem does not assume the existence of limits, monotonicity of the iterates, or anything about the sets ; a formalization that did would assume the substance of the proof. Lemmas C.7 and C.11 (first part) carry the hypothesis of the paper's proof by contradiction, which no actual run satisfies once Theorem 5.1 is proved; they are steps of that argument.
A full development needs: differentiability of and the policy gradient theorem in the occupancy-measure form, the performance difference lemma, the descent lemma for -smooth functions, and Hessian bounds for the softmax map. Contributions to any of these, to the optional Lemmas C.8–C.10 and C.12 of the paper, or to the final contradiction argument are welcome.
Policy gradient methods optimize a decision rule by changing the parameters that determine its action probabilities. In reinforcement learning, the objective is the expected total reward collected over time. Once a policy is restricted to a feature-based class, the best policy may be less effective than the unrestricted optimum. A useful guarantee must therefore compare the computed policy with a chosen comparator and account for both the limits of the features and the error in estimating an update direction. Agarwal, Kakade, Lee and Mahajan give such a guarantee for a version of the natural policy gradient method that fits action values with linear features, called Q-NPG (Agarwal et al., §6.2).
The result matters when a policy has far fewer parameters than there are state-action pairs. A bound phrased only for exact action values or an unrestricted policy class would leave out the errors introduced by fitting from samples and by moving the fitting distribution from the states of a comparator to the states visited by the current policy. Theorem 6.1 keeps those effects visible as separate terms. It also avoids assuming that the comparator is an optimal policy; the comparator can be a policy selected for an application or a benchmark within a restricted class.
A discounted Markov decision process has a finite state set S, a finite nonempty action set A, transition probabilities P(s'|s,a), immediate rewards r(s,a) in [0,1], and a discount factor γ in [0,1). A policy π assigns a probability distribution over A to every state. The value V^π(s) is the expected sum of discounted rewards from s, and V^π(ρ) averages this value over an initial state distribution ρ. The action value Q^π(s,a) starts by choosing a in s and then follows π. Its advantage is A^π(s,a)=Q^π(s,a)−V^π(s). These are the unnormalized value conventions of §3, pp. 9–12.
For each state-action pair, fix a feature vector φ(s,a) in Euclidean d-space. The log-linear policy with parameter θ assigns probability proportional to exp(θ·φ(s,a)):
The Q-NPG fitting loss is the mean squared error of predicting by under a state-action distribution . Q-NPG uses an approximate minimizer w of this loss under its current on-policy measure and updates θ by ηw. The distribution ν specifies the initial state-action pair for that measure. At time zero, the pair is drawn directly from ν; the given initial action is executed before later actions follow the current policy. These definitions are (19)–(20) of §6.2, pp. 27–28.
The comparison policy π⋆ has discounted state visitation distribution . The paper's transfer measure pairs those states with a uniform action from A. The excess risk measures how much worse an approximate fitting direction is than an exact constrained minimizer under the current on-policy measure. The transfer error measures the exact minimizer's loss under . A relative condition number κ bounds, in every feature direction, the covariance quadratic form under by κ times that under ν (Assumptions 6.1–6.2, pp. 28–29).
The goal is Theorem 6.1, p. 29. Starting with θ⁽⁰⁾=0, taking T positive updates with step size , bounding feature norms by B and update norms by W, and assuming the expected excess and transfer errors are at most and , respectively, it asserts
The expectation encloses the minimum: each random run may have a different best iterate. The claim gives a finite-horizon comparison with π⋆ even when π⋆ is not globally optimal.
The milestones are the paper's performance-difference identity (Lemma 3.2), smoothness of bounded-feature log-linear policies (Remark 6.7), the deterministic NPG regret lemma (Lemma 6.2), and the two displayed bounds that control transfer and estimation terms ((25) and (26)). Together they connect the MDP's value comparison with the two statistical errors in the goal. Each milestone states a source result rather than a weakened surrogate.
The theorem separates three quantities that can vary independently in an application: the number of iterations, the statistical quality of the update direction, and the mismatch between the comparator's visited states and the fitting distribution. If both errors vanish, the displayed bound decreases with T at a square-root rate. With imperfect features, the transfer term shows the remaining performance limit. With finite-sample fitting, the excess-risk term shows how estimation quality affects the policy value. This is an agnostic statement because the comparator need not belong to a globally complete policy class (Agarwal et al., Theorem 6.1 and discussion, pp. 29–30).
The paper proves these claims mathematically. This mission asks for machine-checked proofs of the same statements in Lean, including the probabilistic expectation and the exact constants. The reusable parts are the state-action visitation distribution with a prescribed initial action, the log-linear policy and its smoothness property, the least-squares loss, and the deterministic regret lemma. Those objects can support other policy-gradient analyses with different fitting guarantees.
The update direction minimizes a loss under the distribution generated by the current policy, while the value comparison uses states visited by a different policy. The two distributions need not agree, and prediction error under one cannot simply be substituted for error under the other. The relative condition number controls the feature geometry of this shift, while the transfer error separately measures how well an exact on-policy fit predicts under the comparator's measure. Random approximate minimizers add a further layer: the bound concerns the expectation of the best iterate in each run, rather than a deterministic iterate chosen in advance. These are the obstacles identified around Assumptions 6.1–6.2 and the proof of Theorem 6.1.
The Lean development uses finite state and action types, as in the paper's §3 standing setting. It imports published definitions of transition kernels, policies, occupation probabilities, value and Q-functions, and defines this paper's advantage, discounted visitation, log-linear class and fitting loss on top of them. Parameters and features lie in EuclideanSpace ℝ (Fin d), so the norm is the Euclidean norm used by the paper. A general probability space carries the random update directions and exact constrained minimizers; their measurability and boundedness make the displayed loss expectations integrable.
The action type is nonempty so that the uniform action distribution exists. B and W are positive and T is positive, because the prescribed step size divides by and the result minimizes over . The comparator is assumed to be a policy, with no optimality hypothesis. The nonnegative condition number is represented by its quadratic-form upper-bound property for every direction. This avoids undefined real ratios when a covariance form vanishes and includes the finite coefficient in Assumption 6.2. The value and loss expressions are calculated from P, r, π and φ; they are not free variables. The Q-NPG parameter sequence is defined by the update rule from θ⁽⁰⁾=0. In particular, the goal does not assume the regret lemma or either of the two statistical inequalities that the proof must establish.
The paper notes that some §6 results extend beyond finite state or action spaces. This mission fixes the finite case inherited from §3. Contributions that prove the source milestones, establish the required summability and integrability facts, or generalize the development to larger measurable spaces are useful; a generalization must keep the same statistical and comparator conventions.
Many counting problems in probability, combinatorics and statistics ask for the law of the number of occurrences of rare, weakly dependent events: long head runs in coin tossing, matching segments between two DNA sequences, isolated vertices or small subgraphs in a random graph, clusters of points in a scan statistic. Chen's 1975 adaptation of Stein's method gives an explicit error bound for approximating such a count by a Poisson law. Arratia, Goldstein and Gordon (Ann. Probab. 17 (1989) 9–25) recast it in terms of a neighbourhood of dependence for each event. In this form the error bound needs only the first two moments of the indicators whenever each event is independent of the events outside its neighbourhood. The paper's examples (head runs, DNA sequence matching, birthday-type problems) made this form standard in applied probability.
The paper has two main results. Theorem 1 bounds the distance between the law of the total count and a Poisson law; it is essentially contained in Chen (1975). Theorem 2, which the authors describe as new, is a process version. It compares the joint law of all the indicators, that is, where the events occur, with a Poisson process. Theorem 3, a corollary, compares a dependent family of events with an independent family having the same marginal probabilities. This mission formalizes Theorem 2, the finite-dimensional bound it is derived from, the steps of its proof in §6, and Theorem 3.
Let be a probability space and an index set. For let be a Bernoulli random variable, , with
For each fix a set with , the neighbourhood of dependence of . Put and
Roughly, measures the size of the neighbourhoods, the expected number of neighbours of an occurrence, and the dependence between an event and the events outside its neighbourhood. In many applications is independent of , so .
The dependent Bernoulli process is , a random element of . The Poisson process on with intensity is with the mutually independent and Poisson with mean .
Distances are measured in the paper's total variation norm,
which is twice the usual total variation distance.
The bound has no dependence on and no assumption on beyond countability (which the setting forces).
The result. Theorem 2 says that when , , are small, the set of indices at which the dependent events occur is close in law to a Poisson process with the same intensity. The bound covers every event about the locations, not just the total count. It is in the strong total variation norm and needs only moment information when . Theorem 3 turns this into a decoupling statement: a dependent family of rare events is almost indistinguishable from an independent family with the same marginals. The process bound is the form used when the positions of rare events matter, for example in the distribution of the location of the longest match in sequence comparison and in scan statistics.
Formalizing it. The results are proved in the paper; none is machine-checked. A formal development would give a Lean statement and proof of a Chen–Stein bound with explicit constants, for countable index sets and arbitrary dependence. It would also include the coordinatewise Stein operators on and the bounds on their solutions, which are reusable for other multivariate Poisson approximations. A companion mission formalizes Theorem 1, including Lemma 1 (the bounds on the one-variable Stein solution) on which milestone 2 rests.
The total variation distance between two laws on cannot be bounded coordinate by coordinate, because the are dependent. The one-variable Stein equation controls only the law of a single integer-valued statistic. The paper passes through finite-dimensional block sums and replaces the coordinates one at a time. At each replacement the error has to be charged to the terms of indexed by the current block, so that the total over all blocks reproduces without a factor . Two further points need care. First, the bound is the only one available for differences in a coordinate other than the one being replaced; this is why the constants are larger than in Theorem 1. Second, the infinite index set requires a limiting argument from finitely many blocks to the full process.
MarkovChainCLT.tvDist (supremum over measurable sets of ). Dropping the factor would make the goal twice as strong and false in general.tsums, equal to the true sums almost surely. A partition is a surjection (Fin d), so Lean's coordinate 0 is the paper's coordinate .Needed infrastructure: product measures and independence on , Poisson laws (Mathlib's poissonMeasure), conditional expectation, and a one-variable Stein bound (Lemma 1). Contributions of proofs of any milestone, of the general step of §6, and of the one-dimensional Lemma 1 are welcome.
Counts of rare events often look Poisson even when the events are dependent. For example, a local pattern in a random graph can overlap another copy of the pattern, so the corresponding occurrence indicators are not independent. The useful question is quantitative: how far is the distribution of the total count from a Poisson distribution with the same mean? Arratia, Goldstein and Gordon give a bound in terms of three quantities that can be estimated from neighbourhoods of dependence. Their 1989 paper applies the Chen–Stein method to the count and then to the full point process. This mission concerns the count bound, Theorem 1.
The authors explain that the result is essentially contained in Chen’s earlier work, while their one-variable proof prepares the process result in Theorem 2. The bound remains useful as a precise statement of the dependence conditions under which the Poisson approximation works. The process theorem belongs to the companion mission.
Let index Bernoulli indicators , each taking values in on a probability space with law . Write , and let
For each , choose a dependence neighbourhood containing . The neighbourhoods need not be symmetric, and the theorem imposes no independence condition: dependence on indicators outside is measured directly. Define and
The remaining quantities use conditional expectation. Let , and let be the sigma algebra generated by all outside . Put
Conditioning on the count retains less information than conditioning on all far indicators, so . Let have the Poisson law with mean . The paper defines as twice the usual supremum over events: .
The goal is the complete four-clause statement of Theorem 1, including its strict final inequality:
The intermediate targets are the Stein-operator inverse identity, the bound on a telescoping term, display (11) relating the approximation error to , and the two clauses of Lemma 1. The goal keeps the coefficients and both forms of fixed, as the paper states them.
The result reduces a distributional approximation question to local sums of probabilities and conditional-dependence errors. When , and are small, the entire law of the count is close to its Poisson comparison law, and the probability of no occurrence has its own sharper bound. The latter is useful whenever a model asks whether at least one rare event occurs. The result applies without demanding exact independence outside the chosen neighbourhoods; the residual dependence appears in .
The paper proves these results. The formalization task is to give the known estimates machine-checked statements and proofs with the constants and probability conventions exposed. Mathlib supplies the Poisson measure and conditional expectation, while the mission adds the paper-specific neighbourhood sums and Stein operators. The formalized theorem can be reused for count approximations in other dependent-indicator models once those models supply bounds on the three error quantities. No machine-checked proof is claimed here: the theorem items are proposed targets with sorry bodies.
A first approximation based only on misses overlapping event pairs. Bounding pair dependence through alone also misses dependence between one indicator and the aggregate of far indicators. The authors' third term measures that remaining effect by conditional expectation. The proof must control the Stein solution uniformly while preserving its precise constants; replacing that control with a qualitative bound would not recover Theorem 1. In the countably infinite setting, the sums and conditional expectations also require careful handling of convergence and measurability. The proof of Lemma 1 is attributed in the paper to Barbour and Eagleson; it is a substantive target here rather than an assumed bound.
The Lean index type is countable. Under the paper's assumptions and , only countably many indices can exist, so this representation retains the stated probabilistic setting. Indicators are measurable natural-number-valued functions with values at most one. The parameter is a positive real equipped with the exact HasSum statement for the probabilities. The Poisson law is Mathlib's poissonMeasure at converted to a nonnegative real parameter.
The sums defining use extended nonnegative reals, so divergence becomes rather than the real tsum default zero. The random counts and use natural-number tsum; their divergent-input default can occur only on a null set under the finite-mean hypotheses and therefore does not change their laws. Measurability of these counts follows from countability and measurability of each indicator. The far-field sigma algebra is generated by the measurable indicators, and the formalization checks that it lies below the ambient sigma algebra, avoiding a default-zero conditional expectation. The paper's total variation norm is exactly 2 * MarkovChainCLT.tvDist, with the factor two retained.
The source writes a strict final inequality without discussing infinite error sums. The Lean statement conditions that single strict clause on ; otherwise both sides can be infinite and strict comparison is false. The other three clauses allow infinite bounds, as the source does. Lemma 1 fixes the Stein inverse at zero exactly as the paper chooses and uses explicit pointwise sup-norm bounds over all nonnegative integers. Display (11) allows , a strengthening of the displayed case. These choices rule out loss of the norm's factor two, disappearing divergent sums, default-zero mapped measures or conditional expectations, and an unannounced independence assumption.
A reentrant line is a queueing network in which every customer follows one fixed route but may return to a station after visiting another one. A manufacturing line can have this pattern when a product revisits the same machine at different processing stages. A station can then have little nominal workload and still face unstable queues under an unfortunate service order. Dai and Weiss studied this gap between nominal capacity and fluid stability for reentrant lines in their 1996 paper. The four-class line associated with Lu and Kumar is their sharp example: its behavior changes at a simple cross-station inequality that is different from either station's ordinary workload constraint.
The paper establishes several positive stability results for other disciplines and networks, then gives an exact boundary for the Lu–Kumar line. Here the exact boundary is the focus. The result concerns fluid models, deterministic large-scale approximations of queue trajectories. It does not assert positive Harris recurrence or transience of the underlying stochastic network in both directions. The paper cites Dai's earlier implication from a stable fluid model to a stable stochastic discipline, but the converse was still open in its concluding discussion (Dai and Weiss 1996, pp. 119 and 133).
There are four customer classes, encountered in order . Classes and use station ; classes and use station . Each class has a positive mean service time and service rate . The external arrival rate is normalized to one. The nominal workloads are and , both assumed strictly below one. These assumptions say that each station has enough average capacity for its own stages, but they leave the scheduling decision unresolved.
At time , is the amount of class- fluid, and is the cumulative service time devoted to that class. The fluid equations balance the inflow and outflow of each class. Outside fluid enters class at unit rate; completion of class feeds class until class exits. Service times and idle times are nondecreasing, and a station's idle time can increase only when its total queue content is zero. A pair with these properties is a work-conserving fluid solution.
The Lu–Kumar priority discipline gives class priority over class at station , and class priority over class at station . Its fluid model adds the priority complementarity condition: service capacity available to a priority prefix can be unused only when that prefix has no immediate workload. For either model, fluid stability means that some common time empties every admissible solution with , with all queues remaining zero for . Instability is the negation of this statement; it does not require every solution to diverge.
Theorem 5.1 and Remark 1 give two connected classifications, under , , and :
The first clause captures the paper's existence of an unstable work-conserving policy: on the unstable side, the named priority discipline supplies one; on the other side, every work-conserving fluid model is stable. The second clause records the particular policy classification stated in Remark 1. Equality belongs to the unstable side: the paper exhibits a periodic nonempty solution there (Dai and Weiss 1996, pp. 125–127).
The milestones follow the paper's own statements and proof claims. The real-analysis extinction criterion of Lemma 2.2(ii) and the maximum-of-components criterion of Lemma 3.2 provide the stability language. Display (3.2), already available as a proved platform theorem, identifies the derivative of an attained maximum at a regular point. The priority condition (4.4) implies the ordinary work-conserving condition (1.13). The unstable half records one first cycle, one solution with every scaled cycle, and instability of the priority model. The stable half records the authors' explicit parameter choice, the two linear Lyapunov conditions, and stability of every work-conserving fluid solution.
The threshold says that the two station-load inequalities alone do not characterize stability of all work-conserving service orders. The extra inequality determines when the entire work-conserving fluid class is stable; its failure admits a concrete priority discipline with a nonempty trajectory. At the boundary , growth need not be strict: periodic fluid behavior already defeats finite-time stability. The result therefore distinguishes the paper's global stability region from the larger parameter region in which both stations are nominally underloaded (Dai and Weiss 1996, Remark 1, p. 125).
A machine-checked development would give reusable definitions for a four-stage reentrant fluid model, its priority complementarity condition, and the precise unit-initial-state notion of stability. The local Lean statements in this proposal compile, but their proofs remain open. The published maximum-derivative fact is the one already proved platform component used by this mission. The other milestones identify the mathematical work needed to formalize the known 1996 result, rather than presenting the result as a new open conjecture.
The ordinary load test controls how much service each station needs on average, but it does not control which class receives service when several buffers at a station are nonempty. In the Lu–Kumar priority discipline, serving a high-priority downstream class changes the future arrival pattern seen by the other station. Thus a direct argument from and to queue extinction fails. On the stable side, checking a single station's workload is also insufficient: its content may fall while earlier-stage fluid continues to feed it. The paper formulates two linear components and a finite maximum; the challenge is to obtain a uniform negative drift whenever that maximum is positive, including times when one station is empty and the other determines the active component (Dai and Weiss 1996, pp. 126–128).
Classes and stations are Fin 4 and Fin 2, with zero-based Lean indices: paper class is Lean index . The fixed station map is . Service times remain real parameters with explicit positivity hypotheses. Paths are total functions of real time, while equations and conclusions apply only on . The external arrival rate is one, and initial size is the sum , since class contents are nonnegative. The nominal-load assumptions are the two strict inequalities in (5.1). The named priority ranking is a permutation; it encodes only the station-local comparisons that matter.
Conditions (1.13) and (4.4), printed as complementarity or “increases only when empty,” use an equivalent interval-constancy condition in Lean. No extra Lipschitz or continuity assumption is placed on solutions: the fluid equations and monotone capacity constraints are intended to supply that regularity. Derivatives at regular points are represented with HasDerivAt. Lemma 2.2(ii) uses the non-strict bound , the version used by the paper's applications, although its displayed hypothesis prints . The p. 127 line involving prints ; (5.3) fixes the intended coefficient as .
The goal uses Definition 1.3 exactly: one uniform emptying time for all solutions of unit initial content. An impossible solution predicate, or an instability claim that only asks for a nonzero state at time zero, would not represent the paper's theorem. The mission needs finite-index sum and maximum infrastructure, absolute continuity and almost-everywhere differentiation on nonnegative time, plus elementary algebra of service rates and the cycle scaling. These components can be reused in later fluid-network missions. Contributions that preserve the source's hypotheses and boundary case are welcome.
A multiclass queueing network can be unstable even when every station has enough capacity on average: the queue lengths grow without bound although each server's nominal load is below one. Kumar and Seidman, Lu and Kumar (1991) and Rybko and Stolyar (1992) exhibited such networks under simple priority disciplines. This raised the question of which networks are stable under every reasonable policy, and which policies are stable in every network. Dai (1995) reduced the stability of a queueing network to the stability of its deterministic fluid model, so that the question becomes one about solutions of a system of linear equations and inequalities.
Dai and Weiss (1996) use this reduction to study reentrant lines, the model of semiconductor wafer fabrication in which a single route visits the same machines many times. Section 6 of their paper treats Kelly-type lines, in which every visit to a station has the same mean service time. Kelly (1979) showed that such networks with exponential service times are stable under FIFO and have a product-form stationary distribution. Theorem 6.1 shows that with two stations, and a route that never visits the same station twice in a row, stability holds under every work-conserving policy, not only FIFO. This mission formalizes that theorem.
A reentrant line has stations and classes . Fluid enters class at rate , moves from class to class on service, and leaves after class . Class is served at station with mean service time and rate . The constituency of station is and its nominal workload is . The traffic condition (1.7) is for every .
A fluid model solution is a pair : is the fluid in class at time and the cumulative service time given to class by time . They satisfy, for ,
with nondecreasing, and the idle time , where , is nondecreasing. The solution is work-conserving if increases only at times when station holds no fluid. The immediate volume of station is .
The line is of Kelly type with station means if for every class . Its routing has no immediate feedback if for every . A set of fluid solutions is stable (Definition 1.3) if there is a such that every solution in the set with is empty from time on.
For a two-station Kelly-type reentrant line without immediate feedback that satisfies (1.7), the work-conserving fluid model is stable: there is with
for every work-conserving fluid solution . The number of classes is arbitrary, of either parity, and the route may start at either station.
The milestones follow the proof on p. 130 and the two general lemmas it uses: the extinction criterion of Lemma 2.2 (ii); the derivative of a maximum at an active index, display (3.2), already proved on the platform; the piecewise-linear Lyapunov Lemma 3.2; the drift identity for , with ; the comparison ; and the verification that meet the hypotheses of Lemma 3.2 with .
The result. Theorem 6.1 gives a class of networks in which stability needs no knowledge of the scheduling policy: any policy that never idles a server with work waiting is stable whenever the nominal loads are below one. For queueing networks this is the property usually called global stability. Through Theorem 1.1 of the paper (Dai 1995, Theorem 4.3) the fluid statement implies positive Harris recurrence of the corresponding multiclass queueing network under every work-conserving head-of-the-line policy. The paper's Remarks 2 and 3 show the boundary: with immediate feedback (the line with all means ), or with three stations, a Kelly-type line can be unstable. A two-station Kelly-type line without immediate feedback is a unidirectional ring with one customer type, so the theorem is a special case of the ring-network result the paper proves as Theorem 6.2. That result is an open goal on the platform (ProcessingNetworks.GlobalStability.ring_globally_stable, Dai and Harrison's Theorem 8.24) in a different encoding of the fluid model.
Formalizing it. The theorem is proved in the paper, and the mission formalizes that proof. No machine-checked proof of the result, or of the Lyapunov lemmas it uses, is known to exist. The mission also produces reusable pieces: a fluid model of reentrant lines in the paper's own formulation, an extinction lemma for absolutely continuous functions, and the max-of-linear Lyapunov lemma, which the paper uses again in §§3 and 5.
The obvious Lyapunov function, the total workload, does not work: a work-conserving policy may starve a station while the other one is busy, so the total content need not decrease. The paper's components each decrease at the constant rate while station is busy. When station is idle, can grow, and the argument then needs the comparison , which requires the alternating route. The analytic difficulty is the passage from these pointwise statements to extinction. Fluid paths are only Lipschitz. The maximum need not be differentiable where the maximum switches, and the drift statements hold only almost everywhere. Lemma 2.2 (ii) and the derivative-of-a-maximum fact (3.2) make this step rigorous. The proof for odd is not printed ("can be proved similarly"), and the formal goal covers it.
All objects live in the namespace DaiWeissFluid.KellyType. The conventions are fixed as follows.
Fin K, Fin I). The paper's class is Lean k - 1.ℝ → Fin K → ℝ, and every equation is imposed for only. Derivatives are taken at via HasDerivAt.The goal must not be trivialized. It quantifies over all work-conserving solutions with , and this set is nonempty: a sorry-free witness with is checked locally. Neither the Kelly-type hypothesis nor the absence of immediate feedback may be dropped (Remark 2), nor may the goal be generalized beyond two stations (Remark 3). Restricting it to even , or to a route starting at station 1, would weaken it.
Contributions welcome: proofs of the general Lemmas 2.2 (ii) and 3.2, which apply across the whole series; the drift identity, which is pure algebra from (1.8); the continuity facts for fluid paths (Lipschitz bounds from (1.10)–(1.12)); and the final assembly.
Single-machine scheduling with precedence constraints asks for an order in which one machine processes jobs while respecting prescribed comparisons between them. For the objective of minimizing total weighted completion time, the structure of the precedence order can influence the quality of approximation algorithms. Ambühl, Mastrolilli, Mutsanas, and Svensson connect one such approach to coloring a graph built from the order's incomparable pairs. A bounded number of colors would make a certain class of coloring-based guarantees uniform over the class of precedence orders. Their Theorem 4.3 shows that canonical interval orders have no such uniform bound for this particular graph. Ambühl et al., §4.2, p. 658
An interval order is a partial order whose elements can be represented by closed real intervals, with one element strictly before another when the first interval ends before the second begins. Interval orders are a familiar restriction of general precedence systems. The paper distinguishes them from semiorders, represented by intervals of equal length, for which it reports a three-element realizer bound and a corresponding scheduling guarantee. The chromatic obstruction here explains why that particular bounded-color route cannot be extended uniformly from semiorders to all interval orders. It does not assert that every scheduling approach to interval orders fails. Ambühl et al., §§3–4.2, pp. 656–658
For an integer , let be a linearly ordered set with points. The canonical interval order has one element for every pair of distinct points in , viewed as the closed interval . For two such intervals, write when or the right endpoint of is strictly less than the left endpoint of . Thus intervals that touch at an endpoint remain incomparable. The formalization represents each interval by its two-element endpoint set, and its order relation is equivalent to this endpoint rule. Ambühl et al., §4.2, p. 658
For any partial order on a ground set , an ordered incomparable pair is with neither nor . Both and are vertices when and are incomparable. A linear extension of is a linear order on the same elements that contains all comparisons of . It reverses if it places before . The graph has the ordered incomparable pairs as vertices. Two distinct vertices form an edge when no linear extension reverses both, while each singleton can be reversed by some linear extension. This singleton condition is the minimality clause in the paper's definition through its hypergraph of incomparable pairs. Ambühl et al., §2.1, p. 655, §3, p. 656
A proper -coloring assigns one of colors to every vertex of so that endpoints of an edge have different colors. The graph's chromatic number is the least positive number of colors that works, when the graph is nonempty. The mission uses the equivalent predicate that no proper map into a fixed -element color set exists once is large enough. This also gives a clear interpretation at .
The goal is Theorem 4.3: for each fixed integer , all sufficiently large canonical interval orders have incomparable-pairs graphs with chromatic number greater than . With , the Lean target is
The paper states as an integer. Its negative cases are immediate from nonnegativity of chromatic numbers; the target states the substantive range. The threshold may depend on , while and are constructed from rather than supplied as arbitrary objects. Ambühl et al., Theorem 4.3, p. 658
Two assertions from the theorem's proof serve as milestones. First, is nondecreasing as increases. Second, for four endpoints , the vertices and are adjacent in . They are recorded with their wording and provenance from §4.2. A separately published theorem on hypergraph Ramsey numbers is included as a reference because the source uses that theorem in its large- argument. Ambühl et al., proof of Theorem 4.3, p. 658
The result provides a precise structural limitation: across the canonical interval orders, the chromatic numbers of cannot be bounded by one constant. The graph is a specific graph of ordered incomparable pairs, distinct from other graphs that can be associated with a scheduling instance. Thus the conclusion addresses the bounded-color approach attached to this graph, without asserting an algorithmic impossibility for interval-order scheduling. The paper contrasts this limitation with the bounded-realizer situation for semiorders. Ambühl et al., §§3–4.2, pp. 656–658
The theorem is proved in the 2011 paper. The remaining work in this mission is a machine-checked development of its definition layer, its two stated supporting assertions, and the unbounded-color conclusion. The partial-order property of is already proved in the definition file; the three theorem statements are open proof targets in the proposal. A completed formalization would also give reusable components for finite interval orders, ordered incomparable pairs, and coloring arguments in dimension theory.
A pair of intervals overlapping or touching is easy to recognize as incomparable, but graph adjacency has a stronger meaning: it quantifies over every linear extension of the entire partial order. A local test based only on the four displayed intervals would silently change the graph. Likewise, the fact that two vertices have different endpoint descriptions does not by itself make them adjacent. The formal argument must connect the canonical interval representation to the global extension-based edge condition, then show that a bounded coloring cannot persist as the endpoint set grows. Ambühl et al., proof of Theorem 4.3, p. 658
The endpoint set is Fin n, hence indexed rather than the paper's ; the shift preserves order. Elements of are exactly two-element subsets of this set. The order relation includes equality and strict separation of endpoint sets and is proved to be a partial order. The graph is defined for an arbitrary binary relation so it can be reused, but every target here applies it to the concrete partial order . Vertices are ordered incomparable pairs, and adjacency retains both singleton reversibility and failure of simultaneous reversibility. Defining adjacency directly from the desired four-point pattern would trivialize the target and is excluded.
Colorable n k means existence of a proper function from all vertices of to Fin k. For an empty graph, zero-colorability is allowed by this representation. The theorem therefore includes a threshold and quantifies over every ; the assertion itself forces the threshold past any empty-graph exceptions. The formal target uses natural ; the paper's negative integer values need no separate theorem. No asymptotic notation or unspecified constants occur. The source's Ramsey number is not hard-coded into the goal, because the source asserts existence of a suitable threshold, not that the least threshold equals that value.
The printed adjacency justification names an alternating-cycle pair set different from the two adjacent vertices in the preceding sentence. The milestone formalizes the adjacency assertion itself and records the printed explanation verbatim for review; it does not turn the mismatched pair set into a hypothesis. The mission needs finite order embeddings, linear extensions, graph colorings, and a finite Ramsey theorem. The existing published Ramsey theorem is referenced as a reusable result. No scheduling approximation algorithm, polynomial-time statement, or numerical scheduling guarantee is formalized in this mission.
This completed entry lowers the sufficient exponent cutoff for the sharp diagonal Hlawka formula from 90 to 87. The goal is already proved in Lean on Prove2Me: for every real p ≥ 87, the foundation's cyclic constant K_p is the least constant that works for every triple of complex coordinate vectors in every finite dimension.
The statement includes arbitrary unequal-norm and zero triples, as well as dimension zero. It uses the foundation's unchanged definitions and combines admissibility with uniform optimality. This concerns complex diagonal matrices; it does not claim the corresponding result for general matrices or settle the conjecture for all p ≥ 2.
The campaign template is instantiated with value 87. Both items reference the existing accepted theorems.
The proof extends the accepted cutoff-90 Lean development by BrunoDCDO, adapting Ezzeri Esa's construction and analytic argument. The contributions at cutoffs 89, 88 and 87 were submitted by moona3k.
For p ≥ 88, the proof uses the accepted cutoff-88 result. On 87 ≤ p ≤ 88, it retains the localization, box-convexity and cyclic-averaging argument, with confinement parameter q₀ = 5351/15000, an improved cyclic witness (3/(4p))^(1/p), sharper Taylor estimates and exact rational polynomial certificates.
The foundation established cutoff 256; the supplied argument was formalized at cutoff 90. The subsequent accepted results extend the same formula to cutoffs 89, 88 and 87. This entry records the proved cutoff 87 on the campaign timeline; the campaign's cutoff-85 mission remains open.
The 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. The question is how large a comparison constant is needed to make this inequality hold.
This mission asks whether the best possible constant for complex diagonal matrices, already proved in Lean for every real , also holds for every real . This is an open problem: no proof is known. The constant is the one from the foundation mission: the largest comparison constant required by the cyclic family of three diagonal matrices. Because the accepted cutoff-87 theorem already covers every , the new work is the range from 85 to 87.
The cutoff came down from 90 to 87 in a day, through moona3k's proofs at 89, 88 and 87. The 89 proof reran the cutoff-90 argument with sharper, second-order estimates. A numerical model of that argument with retuned constants puts its limit between about 86.6 and 87.5: two of its steps pull the same parameter in opposite directions, and below that point no setting satisfies both. So reaching 85 is expected to need a new idea, not just tighter numbers. The goal theorem below gives the exact statement.
This is an entry in the sharp diagonal Hlawka campaign, which asks for the smallest cutoff at which the same formula holds. Any proof for a cutoff of 85 or lower also settles this mission.
The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh’s Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.
79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source libraryMaximum pressure policies schedule a stochastic processing network by choosing, at each decision time, an allocation of processors to activities that maximizes a linear "pressure" built from the current buffer levels and the network's input-output matrix. Dai and Lin (Oper. Res. 53(2), 2005) prove that such policies are throughput optimal: they stabilize the network whenever any policy can. The policies descend from the back-pressure rule of Tassiulas and Ephremides (IEEE TAC 37(12), 1992) for wireless networks and are now standard in switching, manufacturing and data-center scheduling.
The general theory lets a processor split its capacity among several activities at once. In many systems this is impossible: a machine works on one job type at a time. Section 7 of the paper shows that with this restriction Harrison's static planning LP no longer characterizes stability, and Section 8 shows that forbidding preemption can make a maximum pressure policy unstable. Both difficulties disappear for one structural class, the reversed Leontief networks, in which every activity needs exactly one processor. This mission formalizes the two lemmas that make that class work: extreme allocations are integral (Lemma 1), and a maximum pressure allocation is found processor by processor (Lemma 3).
A network has buffers , where Buffer is the outside world and are the internal buffers; activities ; and processors . The resource consumption matrix has if activity requires processor and otherwise. The constituency indicator records that activity processes buffer . An input activity processes only Buffer ; a service activity never processes Buffer . Each processor runs input activities only (an input processor) or service activities only (a service processor). Each activity has a mean processing requirement , rate , and a routing matrix .
The input-output matrix is
An allocation is with for every processor and for every input processor; is the set of allocations, its set of extreme points, and the allocations with integer coordinates. For a buffer-level vector , the network pressure is and the activity pressure is , with for the idle Activity .
The network is reversed Leontief if each activity requires exactly one processor. The possible activities of processor are for an input processor and for a service processor. Under an integer allocation , is the activity processor works on, or if is idle.
For a reversed Leontief network, and ,
A further supporting item, not a milestone, states the decomposition of an allocation along one processor (proof of Lemma 1, p. 215).
The result. Lemma 1 says that, in a reversed Leontief network, the maximum pressure policies of the processor-splitting theory are automatically non-processor-splitting, so the paper's throughput optimality theorem holds in the setting where machines cannot be shared. Lemma 3 says that the maximization over the (exponentially large) set decouples into one small maximization per processor: each processor picks an activity of largest activity pressure among its own options. This separability is what makes the nonpreemptive version of the policy well defined and is the key step towards Theorem 9 (throughput optimality of nonpreemptive maximum pressure policies). It also covers multiclass queueing networks with alternate routes (§9.1), which are reversed Leontief.
Formalizing it. Both lemmas are proved in the paper; to our knowledge neither is machine-checked. The mission produces a reusable Lean model of the allocation polytope of a processing network with input processors, its integer and extreme points, and the activity and network pressures. The integrality of is a total-unimodularity-type fact for a block structure that is not available in Mathlib in this form.
The pressure is linear, so maximizing over equals maximizing over ; the substance is the description of . The polytope is not a box: input processors carry equality constraints and service processors inequality constraints, and in general networks (an activity needing several processors) contains fractional points, as the paper's example in §7 shows. The step that fails for general networks is the decomposition of a fractional allocation along a single processor: it needs every activity of that processor to use no other processor. In Lean, extreme points must be handled through Mathlib's Set.extremePoints, and the argmax over must keep track of the idle option, which exists for service processors and not for input processors.
Indices are 0-based: internal buffers Fin I, buffers with Buffer Fin (I+1) (Buffer is 0, internal buffer is i.succ), activities Fin J, processors Fin K. The idle Activity is none : Option (Fin J), with activity pressure and unit vector . is Set.extremePoints ℝ 𝒜. "Maximizes the pressure over " is stated by domination ( for all ), never through a supremum. is defined by choice of an activity of at level ; it is used only for , where it is unique.
The standing assumptions of §2 are carried as one hypothesis: and are –, constituencies are nonempty, every activity is an input or service activity and needs a processor, processors are input-only or service-only, at least one input activity exists, and . Two disclosed additions: every input processor has at least one activity (otherwise (2) is infeasible and ), and (needed for ). The goal keeps as on the page; two milestones drop it, which strengthens them.
A trivializing formalization would make empty or give input processors an idle option; both are excluded: is the extreme-point set of the real polytope , which is nonempty for a reversed Leontief network under the standing assumptions, and the idle option belongs to only for service processors, as in (60).
Contributions welcome: proofs of the milestones, a general lemma that – points of a subset of the unit cube are extreme, and the separable description of extreme points of products of simplices, which is reusable beyond this mission.
Second-order stochastic dominance constraints let a decision maker require that a random outcome of a decision be preferred to a fixed benchmark outcome by every risk-averse expected-utility maximizer, without choosing a utility function in advance. Dentcheva and Ruszczyński introduced optimization under such constraints in Optimization with stochastic dominance constraints (SIAM J. Optim., 2003), for the case where the decision enters the outcome linearly (the pure-dominance case). Their follow-up paper, Optimality and duality theory for stochastic optimization problems with nonlinear dominance constraints (Math. Program., 2004), allows the decision to affect many random outcomes in a nonlinear, concave way, and derives optimality and duality theory in which the Lagrange multipliers of the dominance constraints are utility functions.
In applications (portfolio selection against a benchmark index is the paper's own example in §6) the probability space is a finite set of scenarios. Section 5 of the paper specialises the theory to that case. This mission formalizes that section: the reduction of the dominance constraints to finitely many inequalities, and the optimality and duality theorems (Theorems 6 and 7) in which the multipliers become piecewise-linear concave utilities.
There are scenarios with probabilities , , and benchmark constraints, indexed by ; . A decision ranges over a convex set . For each scenario , is the objective contribution and the th outcome, all concave. The benchmark has realizations . Write .
The second-order dominance of a finitely distributed (realizations ) over on an interval reads
The split-variable problem (38)–(41) is
for all , , over and . The Slater condition asks for and satisfying the dominance constraints (39) with for all .
The utility set consists of the functions that are concave, nondecreasing, piecewise linear with break points only at the , and zero on . With multipliers for the splitting constraints , the Lagrangian is
Multipliers of the inequalities (39) generate the utility (46). The dual functional is (47).
Under the Slater condition, optimal for (38)–(41) implies that there are and with
conversely, these conditions together with feasibility imply optimality.
Theorem 6 says that, for finitely many scenarios, the infinite-dimensional multiplier of the general theory (a concave utility in a cone of functions, Theorem 2 of the paper) can always be taken piecewise linear with kinks exactly at the benchmark's realizations. The multiplier space becomes finite-dimensional, is a polyhedral cone, and the dual problem of Theorem 7 is a finite-dimensional convex program. The paper's decomposition (49)–(51) of the dual functional and its numerical method in §6 rest on this. Lemma 2 is the standard reduction that makes dominance against a finitely distributed benchmark a finite set of polyhedral constraints, used throughout the later literature on dominance-constrained portfolio optimization.
The results are proved in the paper; none of them is formalized. The mission produces machine-checked statements of the finite-scenario theory, a Lean model of the utility set and of the correspondence between nonnegative multipliers and piecewise-linear utilities, and a Kuhn–Tucker theorem for concave programs with polyhedral constraints and a relative-interior Slater point.
The obvious route to Theorem 6 is to invoke a Kuhn–Tucker theorem. The available formal versions require every inequality constraint to hold strictly at the Slater point and range over all of . Neither fits: the dominance constraint at the smallest realization has right-hand side and a nonnegative left-hand side, so it can never hold strictly, and may be lower-dimensional (a simplex), so only its relative interior is available. The polyhedral structure of (39) must be used, as in Rockafellar's Theorem 28.2. The second obstacle is the converse direction of the multiplier–utility correspondence: a utility in must be written as a nonnegative combination of the kinks , which requires handling repeated realizations and the one-sided slopes at each break point.
Fin N → ℝ; , , are Fin m → Fin n → ℝ; expectations are finite sums and positive parts are max t 0. No measure theory is used.intrinsicInterior ℝ Z, not the topological interior. In the Slater condition only the splitting constraints are strict; the dominance constraints hold non-strictly.EReal supremum.ConvexOptimization.slater_strong_duality, Boyd–Vandenberghe §5.3.2) assumes a strict Slater point for every constraint and no set constraint, so it does not cover milestone 4.A processing network must decide which activities receive scarce processor capacity while jobs move among buffers. Such decisions matter in manufacturing, service systems, and switches: one activity can consume several processors at once, and a job can be routed to another buffer after processing. A policy that sees current buffer levels but does not need to know arrival or routing rates is easier to operate when those rates are difficult to estimate. Dai and Lin's 2005 paper studies whether a maximum pressure policy, which uses the buffer vector and an input-output matrix, can stabilize every network that is stabilizable in their model. Their Theorems 1 and 2 give, respectively, a necessary planning condition for any stabilizing policy and a sufficient condition for maximum pressure under the extreme-allocation-available assumption. Dai and Lin (2005)
Here pathwise stability means that each internal buffer grows sublinearly in time almost surely. This is a rate statement about sample paths. It does not assert positive recurrence of a Markov chain, nor does it require a stationary distribution. The paper allows general primitive processing and routing processes with almost-sure long-run averages. Dai and Lin (2005), §§2–4
There are internal buffers, activities, and processors. Buffer represents the outside world. The matrix records resource use: when activity requires processor . The matrix records which buffers an activity processes. An input activity processes Buffer ; a service activity does not. Input processors serve only input activities and must be fully used, while all processors have at most unit capacity.
For activity , the processing requirements have mean and the routing counts have long-run matrix . Write . The input-output matrix is
Positive means activity consumes net material from internal buffer ; negative means it produces net material there. An allocation assigns nonnegative activity levels subject to the processor capacity bounds and the equality for every input processor. The finite set consists of the extreme points of this allocation set. At buffer vector , allocation has network pressure . The maximum pressure rule chooses an allocation of greatest pressure among the currently feasible members of . Feasibility depends on jobs actually available to each constituent buffer. Dai and Lin (2005), §§2–3
The extreme-allocation-available assumption (EAA) says that for every nonnegative , a pressure maximizer in can be chosen whose constituent buffers all have positive levels. It links the static pressure maximization to the jobs that a policy can process. The static planning LP asks for activity fractions and a service-processor load such that , every input processor has load one, and every service processor has load at most . Dai and Lin (2005), p. 202
The goal is Theorem 2. For a network satisfying EAA and run by a preemptive, processor-splitting maximum pressure policy, LP feasibility with implies
The milestones follow the paper's route from stochastic paths to deterministic fluid limits. A fluid limit is a uniform-on-compact limit of along positive scales . The milestones state that fluid limits satisfy (14)–(18), weak stability of the corresponding fluid model transfers to pathwise stability (Theorem 3), maximum pressure adds (52)–(55) and (20) (Lemmas 5 and 4), quadratic fluid energy obeys (22)–(23), and LP feasibility with EAA makes the maximum-pressure fluid model weakly stable (Theorem 4). Dai and Lin (2005), pp. 203, 213–214
Theorem 2 identifies a policy whose almost-sure buffer growth rate vanishes whenever the planning LP permits load at most one and EAA holds. Together with the paper's necessary condition in Theorem 1, it characterizes the feasibility boundary for this policy class under EAA. Its scope includes networks in which an activity uses multiple processors and processes multiple buffers simultaneously. It does not claim that all such networks satisfy EAA. Dai and Lin (2005), Theorems 1–2
The result is proved in the 2005 article. This mission asks for a machine-checked proof of that known theorem and its selected intermediate claims. The Lean statements are open draft targets. Reusable outcomes include a model of cumulative routing and service counts, a uniform-on-compact fluid-limit interface, and the weak-fluid-stability transfer theorem for networks without a Markov assumption.
Maximizing pressure over the static allocation polytope does not by itself describe an executable service policy. An allocation can demand work from an empty buffer. EAA addresses the existence of a maximizing allocation supported by positive buffer levels, but the stochastic policy acts on actual jobs and completion times. The proof must connect those discrete, pathwise decisions to the limiting differential equation (20). At a regular fluid time, the maximum-pressure equation is decisive; away from regular times, derivatives need not exist. The fluid model therefore carries a time qualifier that cannot simply be dropped. Dai and Lin (2005), pp. 201–203, 214
The Lean model uses finite index types for buffers, activities, and processors. Internal buffers are Fin I; Buffer 0 is the zero index of Fin (I+1), and an internal buffer maps to its successor index. Activity and processor labels use zero-based Fin. Time is real but all network equations are asserted for nonnegative time. The shared Bell–Williams Paths definition supplies the renewal count in and uniform-on-compact distance using the norm. The completion count is required finite wherever the network equations convert it to a natural number; this prevents infinity from becoming a zero count. Bell and Williams (2001)
The network standing assumptions record binary incidence matrices, nonempty constituencies, processor coverage, activity types, and an input activity. Two refinements are explicit: each input processor has an activity, so its mandatory unit allocation is feasible, and , so is defined as the intended positive rate. Routing counts are cumulative and nonnegative. Their row sums are constrained only for buffers an activity processes: the printed sentence requiring the same sum for every buffer conflicts with its immediately preceding statement that the count vanishes when the activity does not process that buffer. The corresponding rows of sum to one for processed buffers and vanish for unprocessed buffers, as follows from (4). Dai and Lin (2005), pp. 199–200
The policy predicate records allocation-time decomposition (49)–(51) and the non-employment consequence of Definition 1 used in (56)–(58). It checks feasibility of a competing extreme allocation through the paper's threshold at every time of the interval. Individual job states and tie breaking are outside the pathwise interface. The goal retains EAA, the exact bound, and all network and policy equations, so an empty allocation set or an unconstrained service path cannot make the target automatic. Contributions formalizing the finite extreme-point set, fluid-limit compactness, Lemmas 4–5, and the weak-stability transfer are welcome.
Infinite-horizon dynamic programs, including discounted Markov decision processes, stochastic games and semi-Markov models, are usually analysed through a single equation: the optimal return solves the optimality equation , where maximizes the one-step return over decisions. Denardo's 1967 paper (SIAM Review 9(2), 165–177) separated the argument from the particular model. It isolated two properties of an abstract return , contraction and monotonicity, and showed that the standard conclusions follow from them alone. The examples of §8 of the paper cover Howard's discounted model, Shapley's stochastic games and Blackwell's, Jewell's and Fox's models.
The plain contraction assumption (each one-step operator shrinks distances by a factor ) fails in models where the process stops only from a subset of states, or where discounting acts only after several transitions. §5 of the paper handles these with the N-stage contraction assumption: only steps of a policy need to contract, while one step only needs to be nonexpansive. This mission formalizes that section. Its companion mission (part 1 of the series) formalizes the plain contraction case.
Timeline:
Let be a set of points. Each point has a decision set . A policy picks a decision at every point, so the policy space is . Let be the bounded real functions on with the metric ; is complete. Write when for every .
The return assigns a real number to each point , decision and . It defines two kinds of operators on :
and both are assumed to map into . An operator on has modulus or less when for all .
Under these assumptions is a contraction, so it has a unique fixed point , the return function of . The optimal return is . The auxiliary operator is .
Under the monotonicity and N-stage contraction assumptions:
The mission also contains two consequences that are not milestones: is optimal for the mathematical programs s.t. and s.t. (§6, p. 171), and a policy is optimal exactly when it attains at every point (§7, p. 173).
Theorem 4 lets models whose one-step operators are not contractions use the contraction-mapping theory of dynamic programming. Under its hypotheses the optimality equation has exactly one bounded solution, and that solution is the optimal return. Successive approximation converges geometrically from below (part (e)). Lemma 2 shows that is the least with and the greatest with . This gives the linear-programming formulation of finite Markov decision processes (Program I) and the policy-improvement argument of §6. The characterization reduces the search for optimal policies to the decisions that attain the maximum in the optimality equation.
The results are proved in the paper. The work of this mission is to formalize them, in the abstract form that Mathlib does not have: monotone operators on bounded functions that are contractive only after steps, with suprema taken over arbitrary, possibly infinite, decision and policy sets. No machine-checked proof of Theorem 4 or of Lemma 2 is known. The closest formal statements, Propositions 4.1–4.2 of Bertsekas and Shreve under their Assumption C, concern a different model (extended-real costs, nonstationary policies) and are themselves unproved formally.
The obvious argument would apply the Banach fixed-point theorem to . That does not work: under the N-stage assumption, need not be a contraction. The paper gives an example (p. 170) with , , where has modulus for every . The supremum over decisions does not commute with composition, so the contraction of each says nothing directly about . The paper therefore works through the auxiliary operator , which is a contraction. The hard step is to show that , the supremum of the policy returns, is a fixed point of . This is the second half of Lemma 2(a), an -argument that uses both monotonicity and the modulus- bound on .
Part (e) holds only for . It is not a contraction property of on all of .
lp (fun _ : Ω => ℝ) ⊤ (as BFun Ω), and its dist is . The order is pointwise (PLe).IsPolicyOperator, IsMaxOperator and IsNStageSupOperator. Every supremum, including (IsOptimalReturn), is a genuine least upper bound (IsLUB). sSup/⨆ are never used, so no junk value can make a statement trivial.ModulusLE B c. NStageContractionAssumption H N c holds , , ModulusLE (H δ)^[N] c and ModulusLE (H δ) 1, with and independent of .v with , the paper's §5 definition. is the conclusion (a), never a hypothesis.IsNStageSupOperator H N E. The milestone Theorem 4 (a)–(c) proves that such an operator exists. is never defined as a fixed point of or . The goal asserts that the pointwise least upper bound of exists in and is the unique fixed point of both.A complete development needs the Banach fixed-point theorem for iterates (Mathlib's ContractingWith, applied to ), suprema of families of real numbers, and induction on iterates. The §3 observation and Lemma 1 are reusable for any monotone operator family on bounded functions. Contributions to every milestone and to the two §6–§7 consequences are welcome.
A stochastic processing network (Harrison 2000) models a system in which processors carry out activities and each activity draws jobs from one or more buffers. Manufacturing lines, call centers with cross-trained agents, and data switches all fit this model. A central question is which scheduling policies are throughput optimal, meaning they stabilize the network whenever any policy can.
Dai and Lin (Oper. Res. 53(2), 2005) show that maximum pressure policies are throughput optimal. These policies generalize the back-pressure rule of Tassiulas and Ephremides (1992) for wireless and switch networks, and at each moment they choose the allocation that maximizes a linear "network pressure". Their main theorem (Theorem 2) has one structural hypothesis, the extreme-allocation-available (EAA) assumption (Assumption 1). It holds for many familiar networks and fails for some (§6.2 gives a counterexample). Theorem 6 identifies a broad class where it always holds: strict Leontief networks, in the sense of Bramson and Williams (2003). This mission formalizes that theorem.
A network has internal buffers , an outside Buffer , activities and processors .
The input-output matrix is
An allocation gives the level at which each activity runs. The allocation set consists of the allocations with for every processor and for every input processor. Write for the set of its extreme points, the extreme allocations. For a buffer-level vector the network pressure is . Buffer is a constituent buffer of if .
Assumption 1 (EAA). For every there is with such that for every constituent buffer of .
A network is strict Leontief if every service activity has exactly one buffer in its constituency, denoted .
The result. Theorem 2 of the paper states that, under EAA, a maximum pressure policy is pathwise stable whenever the static planning problem has a feasible solution with . Theorem 6 removes the EAA hypothesis for strict Leontief networks. In that class maximum pressure is therefore throughput optimal with no further structural condition. The class includes multiclass queueing networks with alternate routes and networks of input-queued data switches (§9), so Theorem 6 is the step that turns the abstract main theorem into a statement about these concrete systems.
Formalizing it. The theorem is proved in the paper and, to our knowledge, has no machine-checked proof. Formalizing it fixes the exact standing assumptions of the model, several of which the paper uses without stating (see below). It also yields a reusable Lean vocabulary for stochastic processing networks with input activities: from (5), the allocation polytope with the input-processor equality (2), extreme allocations, network pressure and EAA. The companion missions of this series on maximum pressure policies build on the same vocabulary.
The naive argument stops at "take a maximizing extreme allocation". A maximizer may run a service activity whose buffer is empty, in which case EAA fails at . Removing such activities gives , which has the right support and pressure but is in general not extreme. The pressure inequality depends on the sign pattern of , which holds only because every service activity has a single buffer. In the network of §6.2 this sign pattern fails and so does EAA. Returning from to an extreme allocation without losing the support property needs a convex-geometry argument about the polytope . In Lean this means relating Set.extremePoints of a compact polyhedron to maximizers of a linear functional and to supports.
Indexing. Internal buffers are Fin I. Buffers including Buffer 0 are Fin (I+1), with Buffer as 0 and internal buffer as i.succ. Activities and processors are 0-based.
Standing assumptions (§2), one predicate Network.Standing.
Disclosed additions to the page.
Conventions.
Set.extremePoints ℝ 𝒜.sSup. Without attainment the statement would be vacuous.Trivializing formalizations ruled out. EAA must not be weakened to a supremum over a possibly empty , and Buffer must not be counted as a constituent buffer. Either change would make the goal trivially true or impossible.
Infrastructure. Solvers need two results:
IsCompact.extremePoints_nonempty and Krein–Milman;Both are reusable beyond this mission. Contributions proving them as general Mathlib-style lemmas are welcome.
Stochastic processing networks (Harrison 2000) model manufacturing lines, data switches, call centers and multiclass queueing networks in one framework: jobs wait in buffers, activities process jobs from one or several buffers at once, each activity may need several processors simultaneously, and routing after service may depend on the activity used. A central control question is which dynamic policy keeps such a network stable whenever any policy can.
Dai and Lin (Oper. Res. 53(2), 2005) answer it with maximum pressure policies, a generalization of the back-pressure policy of Tassiulas and Ephremides (1992) for wireless networks. At each decision time the policy picks an extreme allocation maximizing a linear "network pressure" in the current buffer levels; it needs no arrival-rate information. Their main result (Theorem 2) is pathwise stability whenever Harrison's static planning LP has a feasible solution with . The proof goes through the fluid model: a deterministic, continuous analogue of the network whose stability implies stability of the stochastic system.
This mission formalizes Theorem 5 of the paper, the strong form of the fluid-level result: under a strict load condition and a mild structural assumption, every solution of the maximum pressure fluid model empties in finite time, uniformly over bounded initial states. Fluid stability in this sense (Definition 4) is the property that the standard fluid-limit machinery (Dai 1995) turns into positive Harris recurrence of the stochastic network.
The network has buffers , where Buffer is the outside world and are the internal buffers, activities and processors .
The input-output matrix is . An allocation is with for every processor and for every input processor; is the set of allocations and the set of its extreme points. The network pressure of at buffer level is .
The static planning LP asks for and with , for service processors and for input processors. Assumption 1 (extreme-allocation-available, EAA) says that for every some maximizer of over has on all its constituent buffers. Assumption 2 says there is with componentwise.
A fluid model solution is a pair of paths , buffer levels and cumulative activity times , satisfying (14)–(18): (written out over buffers), , input processors always busy, every processor's busy time at most elapsed time, and nondecreasing with . A time is regular if both paths are differentiable there. Under a maximum pressure policy the solution also satisfies (20): at each regular ,
for every solution of (14)–(18) and (20). The constant depends on the network only.
The result. Theorem 4 of the paper gives only weak stability (a fluid model started empty stays empty) under , which suffices for pathwise stability. Theorem 5 gives a uniform emptying time under , the hypothesis that standard arguments (Dai 1995; Dai and Meyn 1995) need to conclude positive Harris recurrence and moment bounds for the stochastic network. The emptying-time bound is explicit and linear in the initial fluid level.
Formalizing it. The theorem is proved in the paper; to our knowledge no machine-checked proof exists. The closest formalized result on Prove2Me is ProcessingNetworks.BackPressure.bp_maximal_stability (Dai and Harrison's book, Theorem 9.12), which uses the same Lyapunov idea in a different model: exogenous arrival rates, the planning problem , no input activities and no Buffer 0. The present mission formalizes the Dai–Lin model with input processors, where the planning LP has and the equality constraints (2). The definitions file (network, , , pressure, fluid model, (20)) is shared in content with the other missions of this series.
Each algebraic step is short; the work is in the analysis. The obvious route reads as an ordinary differential inequality and integrates it. That requires the inequality almost everywhere, but it is only available at regular points. So one needs: Lipschitz continuity of and on from (16)–(18), almost-everywhere differentiability (Rademacher), and a comparison argument for an absolutely continuous function, , whose derivative bound holds only where . The step "by (20)" also needs the maximum over to dominate every allocation in . That is the vertex property of a bounded polyhedron, which in Lean means compactness of plus a Krein–Milman type argument. The published Dini-derivative extinction criterion ProcessingNetworks.LyapunovCriteria.dini_extinction_criterion (Dai–Harrison Lemma 8.11) is a possible tool for the last step, applied to .
Fin I, buffers as Fin (I+1) with Buffer 0 the index 0 and internal buffer i the index i.succ, activities Fin J, processors Fin K.ℝ → (Fin n → ℝ) constrained only at . Derivatives are deriv, used only at regular points.IsGreatest of the set of pressures over , so the maximum is attained and an empty cannot pass through a junk supremum. is Mathlib's Set.extremePoints.Network.Standing. Two disclosed additions are needed for the objects to make sense: every input processor has an activity, and . The row sums of are not imposed.Contributions of reusable lemmas are welcome, in particular almost-everywhere differentiability of Lipschitz paths on , the vertex property of bounded polyhedra, and extinction of nonnegative absolutely continuous functions with on .