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?
Scheduling jobs on parallel machines under precedence constraints is the core model of project and parallel-processing scheduling: a job may start only after its predecessors have finished. Two criteria dominate the literature, the makespan (when does the last job finish?) and the total completion time (how long do jobs wait on average?). Knowing that one criterion is at least as hard as the other lets a hardness proof for one transfer to the other without a new reduction from a combinatorial problem.
Brucker, Lenstra and Rinnooy Kan's report Complexity of Machine Scheduling Problems (Mathematisch Centrum, 1975; later in Annals of Discrete Mathematics 1, 1977) collected the complexity status of the standard scheduling problems and stated a set of elementary reductions among them as Theorem 1. Part (l) reduces makespan to total completion time for identical machines with precedence constraints and bounded processing times.
Timeline.
An instance has jobs , a number of identical machines, a processing time for each job, and a precedence relation on the jobs: means that may start only after has completed. Each job is one operation, processed without interruption on any one machine. For a constant , the class requires for every job and an acyclic precedence relation.
A schedule assigns to every job a machine and a starting time ; the completion time is . It is feasible if two jobs on the same machine never overlap and implies .
Following the paper, each optimization problem is replaced by its recognition version. Problem asks, for an instance and a threshold , whether some feasible schedule has . Problem asks, for an instance of the same class and a threshold , whether some feasible schedule has (all weights ).
is reducible to , written , if every instance of can be transformed in polynomial time into an instance of with the same answer.
For every constant ,
The result. Theorem 1(l) makes the total completion time problem at least as hard as the makespan problem in the same class. Combined with Ullman's NP-completeness results and Theorem 1(b) (reducibility transfers NP-completeness), it shows that minimizing on identical machines with precedence constraints is NP-complete, already for two machines with and for unit processing times on machines. These are two rows of the paper's Table III.
Formalizing it. The result is proved on one page of a typewritten report; no machine-checked version exists. The mission produces a scheduling model for identical machines with precedence constraints, binary languages for the two recognition problems, and the reduction in Cook's Turing-machine model. The proof's displayed bounds contain a misprinted index range, which the formal statements correct.
The two criteria are not monotonically related: a schedule with a smaller makespan can have a larger total completion time than one with a larger makespan. So the obvious reduction, keeping the instance and asking for , is not an equivalence: a no-instance of can have a schedule with small total completion time. The instance has to be changed so that the total completion time is governed by the makespan, and the comparison of the two thresholds must be exact, including the strict inequality on the "no" side, which depends on integral completion times and positive processing times.
The main formal difficulty lies in the reduction itself. A polynomial-time Turing machine must decode the binary instance, check that it belongs to the class (including acyclicity of the precedence relation), compare with , and write out an instance with additional jobs and a quadratic-size precedence matrix. The size of that output is polynomial only because is a constant: a version with part of the input would make exponential in the input length.
Fin n, Fin m). Starting times are natural numbers; Section 3 derives all times from processing orders on nonnegative integer data, and both criteria are regular. "" is written as " for every ".CookPvsNP_defs; numbers are written in binary with the alphabet and code encNats of the published definition ProjSchedTW.Complexity.Encoding (Neumann, Schwindt and Zimmermann's encoding). The unit-time model ResourceScheduling.Chain.Model (Błażewicz, Lenstra and Rinnooy Kan) has the same feasibility conditions but unit processing times and real start times, so the model here is defined anew.In a no-wait flow shop every job passes through the machines in the same order, and once it has started it may never wait between two machines. The constraint comes from processes in which the material changes state if it is left standing, such as hot metal rolling, chemical and food processing, and some pharmaceutical lines; see the survey of Hall and Sriskandarajah (doi:10.1287/opre.44.3.510). The question of how hard it is to schedule such a shop well is the question this mission formalizes.
Brucker, Lenstra and Rinnooy Kan settled it for the case in which the number of machines is part of the input. In their report Complexity of Machine Scheduling Problems (Mathematisch Centrum, 1975; journal version in Annals of Discrete Mathematics 1, 1977, doi:10.1016/S0167-5060(08)70743-X), Theorem 5 reduces DIRECTED HAMILTON PATH to the no-wait flow shop. Both minimizing the makespan and minimizing the total completion time are thereby NP-complete.
Timeline.
There are jobs and machines. Job needs processing time on machine . Write
for the time job spends on its first machines. Because a job never waits, a schedule is determined by the start times . The operation of on occupies , and job completes at . A schedule is feasible when no two distinct jobs occupy the same machine at the same time. The delay
is the least gap that lets follow on every machine.
A directed graph on has a Hamilton path if its vertices can be ordered with every .
From the paper builds an instance with jobs and machines. Each ordered pair of distinct jobs is assigned a middle machine , and the partial sums are perturbed from by or on the machines and just before the machines , depending on whether the pair is an arc. The parameters satisfy and .
where is polynomial-time many-one reducibility between the binary-coded recognition languages.
The result. Theorem 5, together with the NP-completeness of DIRECTED HAMILTON PATH, places both no-wait criteria among the NP-complete problems once is part of the input. The Gilmore–Gomory algorithm for two machines therefore cannot be extended to arbitrary unless P = NP, and heuristics and exact exponential methods for no-wait shops are justified. The reduction also gives a structural fact of independent use: every directed graph can be realized, up to two arc-weight values, as the delay matrix of a no-wait flow shop.
Formalizing it. The result has been proved for fifty years; to our knowledge no machine-checked version exists. This mission produces a checked no-wait flow shop model, a checked travelling-salesman reformulation of it, the correctness of the paper's construction, and a polynomial-time reduction in an explicit Turing-machine model. It also records a gap in the printed proof: the ordering the paper calls easy to construct does not exist for .
Three steps are not routine.
Jobs and machines are -based (Fin n, Fin m); cum p ℓ i is the paper's , and the machine indices are the paper's -based indices. Start times are natural numbers, and release dates are . Section 3 computes times from processing orders on integer data, and every criterion is regular, so real start times would not change the yes-instances. A zero-length operation occupies the empty interval. is stated as for every job. The delays, the partial sums of the construction and its processing times are computed in . The instance uses their conversion to , which is exact by milestone 4. The threshold of Theorem 5(b) is compared in , as printed.
The paper's loose phrases are made explicit as follows:
Directed graphs are Boolean adjacency matrices. A graph with or vertices has a Hamilton path, and a one-vertex graph has a Hamilton circuit iff it has a loop.
The goal is CookPvsNP.PolyReducible from the published definition CookPvsNP_defs, with polynomial time measured on Cook's one-tape Turing machines. Instances are coded with the alphabet BSym and binary code encNats of the published ProjSchedTW.Complexity.Encoding (Neumann, Schwindt and Zimmermann). A graph is coded as followed by its adjacency matrix; a flow-shop instance as , , the matrix and the threshold .
Stating only the equivalences 6–7 and calling the result "reducible" would drop polynomiality; the goal therefore asserts PolyReducible. The target languages contain exactly the no-wait flow-shop instances, with no waiting allowed, so the reduction cannot land in a looser problem. The parameters always carry , .
Contributions are welcome at every level:
An online matching algorithm must commit to each assignment when a request arrives, before it sees later requests. This limitation arises whenever waiting for the full instance is impossible: an available resource can be assigned to a current request or saved for an unknown future request. The quality of the assignment is measured by how many requests can be matched. The central question is how much the lack of future information costs, even when an algorithm uses randomness. Karp, U. Vazirani, and V. Vazirani studied this question for bipartite graphs and proved an asymptotic ceiling of for the expected fraction matched by any randomized online rule on graphs with a perfect matching (Karp, Vazirani, and Vazirani, 1990).
The paper also analyzes RANKING and gives a matching asymptotic guarantee from below. This mission concerns the separate upper-bound result: the existence of hard instances for every algorithm. The upper bound matters independently of any particular proposed rule. It says that improving an algorithm's decisions cannot remove the worst-case loss due to decisions made before all columns are revealed. Its quantifiers make the adversarial model precise: the graph is selected with knowledge of the algorithm, before that algorithm's random choices are made.
There are boys, represented by rows, and girls, represented by columns. A bipartite graph records which boy and girl pairs may be matched. The graph is assumed to contain a perfect matching: some bijection between the two sides uses only edges of . This assumption supplies an offline benchmark of matches. Without it, a graph with no edges would make every upper bound on matching size empty of content.
Girls arrive one at a time. On arrival, the algorithm learns the edges incident to that girl, chooses an as-yet-unmatched adjacent boy, or declines to match her. A choice cannot later be changed. The paper labels columns so that they arrive in the order . A deterministic algorithm can base its action on the neighborhoods revealed so far. A randomized algorithm can additionally use internal random choices. Its performance is the minimum, over a graph with a perfect matching and a preselected arrival order, of its expected number of matches; the expectation is over its own randomness (Karp, Vazirani, and Vazirani, 1990, p. 352).
The paper's hard family begins with the complete upper-triangular graph , where row is adjacent to column exactly when . Its columns arrive from largest to smallest. Relabeling the rows by a permutation gives an instance that still contains a perfect matching. The algorithm RANDOM takes an eligible boy uniformly whenever at least one is available. Write for RANDOM's expected number of matches on , beginning with no matched rows (Karp, Vazirani, and Vazirani, 1990, p. 357).
For every , there is one threshold such that, for every and every randomized online algorithm on rows and columns, a graph with a perfect matching satisfies
The threshold is uniform over algorithms. The graph may depend on . This is the quantified upper-bound reading of Theorem 2's (Karp, Vazirani, and Vazirani, 1990, Theorem 2).
Lemma 13 identifies the average size produced by any deterministic greedy algorithm on a uniformly permuted with RANDOM's expected size on . Lemma 14 bounds the worst-case performance of every randomized algorithm, including non-greedy algorithms, by that value. Lemma 16 identifies the value itself by the two-sided limit
Together these statements give the finite-instance comparison and the asymptotic value named in the goal (Karp, Vazirani, and Vazirani, 1990, Lemmas 13, 14, 16).
Theorem 2 limits what any randomized online matching rule can guarantee under the paper's oblivious-adversary performance measure. Since the hard graph always admits a perfect matching, the gap from is caused by the order of information and the required irrevocable decisions. The statement applies to the entire algorithm class, rather than comparing two selected procedures. It therefore provides the ceiling against which the paper's lower guarantee for RANKING is measured.
Formalizing the result requires a reusable description of finite online algorithms, their visible histories, and expected matching size. It also requires a definition of uniform random choice from currently eligible rows with an explicit empty-choice case. The 1990 result is proved in the paper; the statements in this mission are targets for machine-checked proofs, not claims of an existing formal proof. The model can support later statements about other matching rules and hard-input distributions without changing the meaning of an online decision.
For a fixed graph, an algorithm can be designed around the graph's particular perfect matching, so one hard graph cannot simply be announced in advance for all deterministic algorithms. The theorem instead has to bound each randomized algorithm against a graph selected for that algorithm. Even then, checking the triangular graph against one rule does not establish a universal bound: different rules can respond differently to the same revealed neighborhoods. The crucial mathematical obstacle is a comparison across all such rules while preserving the restriction that future columns remain unseen. A further asymptotic step is needed to determine RANDOM's value on the triangular family, including both sides of the claim in Lemma 16.
Both sides are Fin n. An edge set is a subset of row-column pairs. The published perfect-matching predicate is reused: it asks for a bijection whose every selected pair is an edge. The paper's one-based column order is represented by zero-based order ; arrival number zero is the largest column. A deterministic rule receives only the neighborhoods of columns that have arrived, including the current column. A randomized rule is a probability mass function on the finite set of deterministic rules, allowing arbitrary correlations among its choices. The expected size is a finite sum over that mass function.
RANDOM is represented by the conditional-expectation recursion for uniform choice among eligible rows. If none is eligible, the column remains unmatched and there is no division by zero. For , the matching and RANDOM value are zero; the main theorem is eventual in and Lemma 16's value at zero does not affect the limit. Lemma 16 uses a two-sided limit. The paper's in Theorem 2 is stated as with before the algorithm, so the error is uniform across algorithms. A hard graph must contain a perfect matching; dropping this condition would let the empty graph satisfy the inequality trivially.
Useful contributions include finite probabilistic averaging, the greedy comparison, analysis of the recursive RANDOM value, and a proof joining Lemmas 14 and 16 into the uniform goal. The history and matching-run definitions are reusable for other finite online bipartite matching statements. The two numbered claims inside the paper's proof of Lemma 13 and its later remarks are outside the mission's curated milestone list.
A newsvendor retailer who may order twice faces a tradeoff. Ordering late lets the retailer use a better demand forecast. Ordering early lets the supplier produce more cheaply, with longer procurement lead times and no overtime labor. Fisher and Raman (1996) document such forecast improvements between ordering epochs in fashion apparel. A decentralized supply chain must balance cheap early production against well-informed late production, and it is not obvious that a simple contract can induce both firms to strike the balance an integrated firm would choose.
This mission formalizes §6.6 of G. P. Cachon's survey chapter Supply Chain Coordination with Contracts (Handbooks in OR & MS, Vol. 11, 2003), read in the author's January 2003 draft. The section builds on Donohue (2000), who studied the same two-mode production problem under forced compliance. The chapter's model lets the supplier operate under voluntary compliance: she may deliver less than the retailer orders, and she may produce more in period 1 than was ordered. The question is whether a buy back contract with one wholesale price per ordering epoch still coordinates the supply chain.
A demand signal with density and distribution function is observed once before the selling season. Given , demand has distribution function , continuous and strictly increasing on . Demand is stochastically increasing in the signal: for . Expected sales are . Period 1 is before the signal and period 2 is after it. The retailer's total order is after period 1 and after period 2. The supplier's unit production cost is in period , with , where is the retail price. Salvage values and goodwill costs are zero.
The supply chain's period-2 objective is
and maximizes it over . The supply chain's expected profit is .
Under the buy back contract the retailer pays per unit ordered in period , and the supplier refunds per unsold unit. The retailer's period-2 profit is , and his period-1 profit is . The supplier's period-2 profit and her period-1 profit , as functions of the stock she holds, are given in the mission's Profits definition.
For with
the identities
hold, so the supply chain's optima in both periods are the retailer's optima (with equivalence for ). In addition,
The result shows that the buy back contract, which coordinates the single-period newsvendor, extends to a setting with a forecast update and two production modes, even when the supplier is free to under-deliver or to stockpile. Profit can be divided arbitrarily through . Coordination also forces the supplier's margin on expensive late production below her margin on cheap early production, which contradicts the intuition that the better-informed late order should command a premium. Milestone 7 rules out stranded inventory: under the coordinating terms the supplier never stocks more than the retailer ordered in period 1.
These results are established on paper in Cachon's chapter. No machine-checked version is known. The identities are algebraic. The supplier's production result needs differentiation of an expectation over the signal across the moving threshold .
The retailer's identities reduce to algebra once the contract terms are substituted, and the margin comparison is one line. The substantive steps are the derivative formulas (27) and . The obvious move, differentiating inside the expectation term by term, fails because the period-2 optimum has a kink at . The integrand switches between two regimes, and the switch point moves with . The supplier's period-1 profit is not differentiable at ; only its right derivative is negative at . Turning the page's derivative statements into the global claim that is her unique optimum needs a monotonicity argument on both sides of .
The conditional law is a measurable family of probability measures on supported on , each with a finite mean, a continuous distribution function, and a distribution function strictly increasing on . The signal has a measurable density with , and demand has a finite unconditional mean. These standing assumptions follow the chapter's p. 7 newsvendor model, together with the measurability needed for expectations over the signal. makes the critical ratio lie in . Expected sales reuse the platform definition SupplyChainTheory.expSales (from SupplyChainTheory_contracts).
The optimum is a hypothesis-carried selection maximizing over . It is never an arbitrary function: a formalization that let be unconstrained would make a statement about meaningless orders. The thresholds enter as solutions of (26) whose existence is assumed where the page assumes it. Optimal order quantities are taken over and . Derivatives are stated with HasDerivAt (or HasDerivWithinAt for the right derivative at a kink).
Three corrections of the print are disclosed in the item notes:
Contributions are welcome on all milestones. A lemma that differentiates with a density-driven threshold would be reusable beyond this mission.
Minimizing total weighted tardiness on a single machine, written , is one of the basic problems of deterministic scheduling. A job that finishes after its due date is penalized in proportion to its lateness and its weight. Practitioners use this criterion to model penalty clauses and customer priority. In the theory it was a reference problem for branch-and-bound methods and dominance rules throughout the 1960s and 1970s.
Close relatives are easy: with equal weights and a common due date, shortest-processing-time order is optimal. Whether the weighted problem admits a polynomial algorithm was open until the report of Brucker, Lenstra and Rinnooy Kan in 1975. Their Theorem 4(d) shows that KNAPSACK reduces to it, so the problem is NP-hard. The unweighted case is listed there as open (Section 5) and was settled only later by Du and Leung (1990).
Timeline:
A KNAPSACK instance consists of positive integers and . It is a yes-instance if some subset satisfies . Write and .
An instance of consists of jobs. Job has a processing time , a weight and a due date , all nonnegative integers, and every job is available at time . A schedule gives each job a start time , and no two jobs may overlap on the machine. Job completes at and has tardiness . The instance with threshold is a yes-instance if some schedule satisfies . A processing order determines the schedule without idle time, in which .
Reducibility (Section 2 of the paper) is polynomial-time many-one reducibility between the recognition versions. A polynomial-time Turing machine must map codes of KNAPSACK instances to codes of scheduling instances so that yes-instances map exactly to yes-instances.
The paper's construction has jobs: for , , , ; for each of the dummy jobs, , , . The threshold is , with and . The proof is phrased in terms of , the amount by which the -th job of the order misses the common due date.
stated as CookPvsNP.PolyReducible SchedComplexity.OneMachine.knapsackLang wtLangMult. The scheduling side uses the multiplicity encoding of the paper's Remark (p. 23), in which a class of identical jobs is written once together with its cardinality.
Each milestone is a statement of the paper's proof (pp. 20–21) about the construction above, for every admissible :
The theorem places among the NP-hard problems, so (unless P = NP) the research on it has to aim at enumerative methods, pseudopolynomial algorithms or approximation, not at an exact polynomial algorithm. Together with the companion reductions of Theorem 4, it drew the boundary between easy and hard single-machine problems that the later classification of Lageweg, Lawler, Lenstra and Rinnooy Kan made systematic.
The result is proved in the paper, and Lawler's later strong NP-hardness proof supersedes it. No machine-checked proof is known to exist. A formal proof adds three things. It makes the paper's "it is easily seen" steps and the encoding argument of the Remark explicit. It produces a reusable single-machine tardiness model with processing orders. It also fixes a gap in the printed construction: the printed need not be an integer.
The equivalence is not a local exchange argument. The threshold must separate orders with from all others, and the objective is a quadratic function of the order. The orders with can still differ in by the cross terms and by how the late jobs are arranged. The construction therefore needs a slack that absorbs these terms, and a scale large enough that a nonzero always costs more than the slack. Keeping exact track of every constant, including and , is where errors creep in.
Polynomiality is a second, separate difficulty. The construction has jobs, which is exponential in the binary length of the KNAPSACK input. The goal holds only for the encoding of the Remark, and a solver must also produce an explicit polynomial-time Turing machine.
Fin n, numbered from ; a processing order is Equiv.Perm (Fin n) with π i the paper's . posCompletion p π k is the paper's for the 1-based position .CookPvsNP.PolyReducible from the published CookPvsNP_defs. Codes use the alphabet BSym and the binary numerals encNats of the published ProjSchedTW.Complexity.Encoding (Neumann, Schwindt and Zimmermann's encoding). KNAPSACK is restricted to positive integers, so that encoding's subsetSumLang is not reused.The integer linear programming feasibility problem asks, for an integer matrix and , whether some satisfies . It is NP-complete, so no algorithm polynomial in the length of the data is expected. H. W. Lenstra, Jr. (Math. Oper. Res. 8 (1983) 538–548) showed that the picture changes when the number of variables is fixed: the problem is then solvable in polynomial time. The proof is a short argument from the geometry of numbers, and it became the starting point of lattice methods in integer programming, including Kannan's improved algorithm and the later flatness-based branching schemes.
Lenstra's introduction (p. 538) describes the idea as transforming the problem into an equivalent one in which "either the existence of a vector satisfying is obvious; or it is known that the last coordinate of any such belongs to an interval whose length is bounded by a constant only depending on ." This mission formalizes the geometric statement behind that dichotomy, §1 of the paper.
Timeline. For , Hirschberg and Wong and Kannan gave polynomial algorithms in special cases, and Scarf treated the case completely; the case of general fixed was conjectured by Hirschberg–Wong and Scarf (as recounted on p. 538). Lenstra's paper (received 1981, published 1983) settled the conjecture. Its lattice reduction step uses the algorithm of Lenstra, Lenstra and Lovász (1982). Kannan (1987) later reduced the dependence on to .
Work in with the Euclidean length , and write for the closed ball with centre and radius .
A lattice is for a basis of . Its determinant (the as columns) is the volume of the parallelepiped and does not depend on the basis. Hadamard's inequality (6) says . A basis is reduced in Lenstra's sense if, for a constant depending only on ,
Singling out , let be the hyperplane spanned by the other vectors, the lattice inside it, and the distance of to . Then : the lattice lies on a family of parallel hyperplanes at successive distance .
In the paper, is bounded with positive volume, and a linear map makes it "round":
with depending only on . Then if and only if for , a lattice with basis .
Let be a basis with (7), numbered so that , and let satisfy (3) and (4). Then
where is the number of hyperplanes , , that meet (finiteness included).
The goal leaves and free, so it remains valid for any reduction algorithm and any rounding procedure; the companion mission (Integer Programming with a Fixed Number of Variables 2) supplies , and the LLL algorithm supplies .
The result. The goal is the branching step of Lenstra's algorithm. It says that a lattice-point-free convex body that is well rounded is "flat" in the lattice direction dual to : only boundedly many lattice hyperplanes meet it. The search for a lattice point in dimension therefore reduces to fewer than searches in dimension , which with fixed gives polynomial running time. Sharper forms of the same dichotomy, such as Kannan's bounds, are the basis of later lattice-based integer programming algorithms.
Formalizing it. The results are classical and proved on paper; to our knowledge none of the statements of §1 is machine-checked. Hadamard's inequality (6) is in Mathlib (Orientation.abs_volumeForm_apply_le). The published platform theorem KannanLattice.Core.exists_lattice_point_near_projection (Kannan 1987, Proposition 4.2) proves a stronger form of (8) and (10), with Gram–Schmidt lengths in place of ; for , (10) is the published QFS.exists_lattice_mem_closedBall. What remains is the "base times height" identity (11) relating a full-rank determinant to the distance of a vector from a hyperplane, the spacing bound (12), the count of hyperplanes meeting a ball, and their assembly. This is one of the two geometric ingredients of Lenstra's polynomial algorithm; the algorithm itself and its running time are not formalized.
The argument is short on paper, and each step is "clear" there. The work lies in connecting three descriptions of the same geometry that Mathlib keeps apart: the determinant of a coordinate matrix (), the metric distance of a point to a subspace (), and the -dimensional volume of . Identity (11) needs exactly this bridge, and (12) needs Hadamard's inequality for the lower-dimensional lattice inside a hyperplane of , not for a full-rank matrix. Bounding the number of hyperplanes meeting a ball needs the normal direction of and the fact that the hyperplanes are apart along it. A tempting shortcut is to define as the length of the last Gram–Schmidt vector and as the product of Gram–Schmidt lengths: that turns (11) into a tautology and is ruled out below.
EuclideanSpace ℝ (Fin n), so norms are Euclidean and balls round; is Metric.closedBall p z with as a hypothesis where the paper writes a ball.b : Fin (k+1) → ℝⁿ, = b (Fin.last k) and = b ∘ Fin.castSucc. "Basis for " is linear independence of the vectors over , and is the published KannanLattice.Core.lattice b, the -span.latDet). is Metric.infDist from to the span . , for which the paper writes no formula, is the published KannanLattice.Core.latticeDet (the product of Gram–Schmidt lengths of , the -volume of their parallelepiped).hitIndices b p R; is its cardinality, its finiteness is part of every conclusion (the cardinality of an infinite set is in Lean), and is computed in .Welcome contributions: the bridge between Matrix.det of a basis and products of Gram–Schmidt lengths (reusable for any lattice development), Hadamard's inequality for a family of fewer than vectors, and the count of lattice hyperplanes meeting a ball.
A retailer can keep too little inventory even when its own stocking decision is optimal. In the single-location model of Cachon, Supply Chain Coordination with Contracts (2003), the supplier suffers a cost when the retailer has backorders, but the retailer does not bear that part of the cost. The supplier and retailer therefore prefer different base-stock levels. Section 6.7 asks whether payments tied to expected inventory and backorders can make the retailer choose the level that minimizes their combined cost. The result also describes how the contract divides that cost between the firms.
The model concerns a continuing operation with repeated replenishment opportunities and backordered demand. A base-stock policy keeps the retailer's inventory position at a chosen level by replacing units as demand occurs. Cachon reduces the cost calculation for such a policy to the distribution of demand over one replenishment lead time. That reduction allows the coordination question to be stated with one real stock-level decision rather than a full inventory trajectory. The chapter presents this model as a building block for its two-location system in §6.8 Cachon (2003).
Let denote lead-time demand, the amount demanded while the retailer waits for replenishment. It is nonnegative and has a finite mean , distribution function , and density . At inventory level , expected inventory is and expected backorders are , where . The section assumes and a strictly increasing differentiable on nonnegative levels. These assumptions place the optimum above zero.
The retailer pays holding cost and its own backorder cost . The supplier pays a further backorder cost . All three cost rates are positive. Thus and are the firms' costs, while is the channel cost. Write . Because demand is backordered rather than lost, the section treats the sales rate as constant across the stock decisions and compares costs alone Cachon (2003), §6.7.1.
The proposed contract pays the retailer from the supplier, where and are transfer rates. A positive rate is a subsidy; a negative rate charges the retailer. For a parameter , the contract sets and . The retailer's contracted cost is its original cost minus this transfer; the supplier's contracted cost is its original cost plus it. The parameter describes a family of printed contract rates and is not itself a payment term Cachon (2003), p. 74.
The milestones establish the two expectation identities, the channel's cost formula and strict convexity, the channel's critical ratio, the retailer's lower uncontracted stock level, and the retailer's cost after the printed transfer. In the notation above, the channel optimum is unique and satisfies
the uncontracted retailer has its own unique optimum with . Three further statements of §6.7.1 complete the section: the signs of the transfer rates over the family (, with exactly for , and ); the decomposition
and the equivalence with the newsvendor model: with lead-time demand as newsvendor demand, retail price and wholesale price , the newsvendor retailer's profit , with expected sales , equals . The mission goal is the coordinating identity of Eq. (33), together with the unique optimality it implies:
Consequently, the retailer's contracted cost has the same unique minimizer as the channel cost. At each stock level the retailer's contracted cost is strictly increasing in , which is the page's statement that the retailer's share of the cost increases with . The result does not prescribe one fixed allocation of cost: each in the stated interval gives a contract with the same coordinated stock level and a different retailer share Cachon (2003), Eq. (33), p. 74.
The theorem identifies an explicit transfer that corrects an incentive gap created by the supplier's backorder cost. Without it, the retailer sets stock according to , while the channel's stock decision uses . Under the contract, the retailer bears the fraction of total cost at every stock level, so its decision agrees with the integrated channel's decision. This conclusion connects a decentralized cost objective to the base-stock target used in the next section's two-location analysis Cachon (2003), §§6.7–6.8.
The chapter proves these claims informally; this mission asks for machine-checked Lean proofs of the expectation identities, convexity and optimality claims, and the contract identity. Its reusable output is the precise treatment of expected positive-part inventory and backorders under a demand law with finite mean. The local definitions may also support later formalizations of inventory contracts. Expected sales in the newsvendor comparison is the published SupplyChainTheory.expSales (definition SupplyChainTheory_contracts), referenced rather than redefined. The existing proved SupplyChainTheory.chain_optimal_fractile concerns a single-period newsvendor profit objective; its critical ratio is related mathematically but belongs to a different model and is not substituted for Eq. (31).
The algebra of the transfer rates is short, but the unique-optimum claim depends on more than algebra. It requires expected inventory and backorders to match the distribution formulas, the cost to have the required curvature at nonnegative levels, and the optimum to occur at a positive level. A formal statement that defines the retailer's contracted cost directly as would erase the coordinating claim. The negative-stock region also matters: since demand is nonnegative, expected inventory vanishes there and cost is affine rather than strictly convex. The formulation must keep strict convexity on the range where it holds while still identifying the unique optimum among all real stock levels.
Lean represents by a probability measure on supported on , with an explicit integrable first moment. The density is a measurable nonnegative function whose induced measure is the demand law; the cdf is continuous, strictly increasing on , equals zero at zero, and has that density as its derivative at positive levels. These are the section's distribution assumptions. The positive rates are fields of one model, and are defined by expectations. This rules out accidental zero values from nonintegrable real integrals. The cost functions are constructed from the expected inventory and backorders; the transfer is constructed from the two printed rates. The identities in Eqs. (28)–(33) are theorem targets, not definitions.
Stock levels are real, including negative levels, because the section does not explicitly restrict the decision set. The formal result states strict convexity on nonnegative levels and uniqueness of the cost minimizers over all real levels. The page's sentence that for all fails at , where ; the formal statement asserts with strict positivity exactly for . The contract range is exactly ; would make every retailer stock level cost-equivalent. The transfer sign is positive from supplier to retailer, as on p. 73. Risk neutrality and full information are the chapter's standing conventions. The continuous-review state process, supplier capacity, and proof that a base-stock policy attains the displayed long-run average are not modeled; the mission formalizes the section's explicit lead-time-demand cost reduction. Contributions that establish integrability, distribution identities, strict convexity, and critical-ratio optimality are all needed for closure.
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.