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.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
The number of successes in many rare, roughly independent trials is approximately Poisson. This law of small numbers is used for counts of rare events in reliability, insurance, epidemiology, queueing and random combinatorics. A quantitative version says how large the error is. For independent Bernoulli trials with success probabilities and , Le Cam (1960) showed that the error in total variation is of order . When all are small this tends to zero, but it does not say what the leading part of the error is.
L. H. Y. Chen's 1975 paper (Ann. Probab. 3, 534–545) adapted Charles Stein's method for normal approximation to the Poisson case. The result is now called the Stein–Chen method. The paper's §2–§4 give first-order error bounds for dependent (mixing) trials. Its §5, "A refinement", goes one order further for independent trials. It identifies the first-order correction explicitly and shows that what remains is of order . Kerstan (1964) had obtained a similar expansion by a different method. Chen's version comes from iterating the basic identity of the Stein–Chen method. This mission formalizes §5.
Timeline:
Let be independent random variables on a probability space, each taking only the values and , with success probabilities . Put
For a bounded real function on the nonnegative integers, the Poisson expectation is
the mean of under the Poisson law with parameter . The Stein equation is . For its solution is
Write and . Chen's second-order operator is
For another parameter , and apply the Stein solution and the operator with parameter to the function .
In Lean: poissonExp, stein, delta, shiftL, stU, prob, lam, lamExcept, W, Wi, all in the namespace PoissonDepTrials.SecondOrder.
If are independent, and , then for every with ,
The paper writes the constant as "an absolute constant not greater than ". The formal goal fixes at that value, which is the same statement.
In order: the Stein solution (2.3)/(2.5); the difference identity (3.6); Lemmas 3.1, 3.2, 3.3 and 3.5 (bounds on and ); the first-order identity (5.8) ; Lemmas 5.1 and 5.2 (dependence of Poisson expectations on the parameter); Lemmas 5.3–5.5 (bounds on , and ); the bound (5.9),
and the closing inequality .
The theorem gives an explicit first correction to the Poisson approximation of a Poisson-binomial law, with a remainder of the next order. When all equal , the first-order error is replaced by the remainder , which is smaller by the factor . The correction term is a functional of the Poisson law alone, . It can be evaluated without knowing the distribution of . The method of proof applies the basic identity twice. The paper notes that further iteration gives expansions to any order.
On the formal side, Mathlib has the Poisson distribution but no Stein–Chen machinery and no quantitative Poisson approximation. The theorem has, as far as is known, no machine-checked proof. This mission produces the Stein solution and its standard bounds (Lemmas 3.1–3.5), which are reusable by any Stein–Chen argument. It also produces the parameter-perturbation estimates of Lemmas 5.1–5.2 and a complete second-order expansion. Missions 1 and 2 of this series formalize the first-order bounds of §4 under a mixing condition. They share the Stein-solution layer.
The first-order bound needs only that is uniformly small (Lemma 3.4). A second-order bound needs more. After the first application of the identity, the error has to be expanded again. That requires control of the iterated operator with a different parameter , because is approximately Poisson with mean , not . The bound on (Lemma 5.5) grows linearly in . Applying the uniform bounds of §3 throughout loses a factor and produces an error of order instead of . The linear growth has to be paired with the variance of . The averaging over pairs in the final step uses the condition , which keeps every comparable to .
Conventions committed to in Lean:
X : ℕ → Ω → ℕ. Each is measurable with values in almost surely. for and , which is the paper's own padding convention (p. 535). Independence is iIndepFun (fun i => X i) P over all of ℕ. Because the padding variables are constants, this is equivalent to independence of .Hypotheses added relative to the page, each disclosed in the item's Formalization Note:
The random indices that the paper introduces to shorten notation in (5.8)–(5.9) are not formalized. The same quantities are written as finite sums over indices.
Ruled out: the second-order term must be the operator built from the Stein solution exactly as on p. 543. A free function, or evaluated at the junk value , would empty the theorem.
Welcome contributions include:
Finite-horizon Markov decision processes ask which decisions minimize accumulated cost over a specified number of stages. In a stationary process, the same costs and transitions apply at every stage. This compact input can describe a horizon much larger than the state set, so a method that processes all stages one by one may take time exponential in the length of the written horizon. Papadimitriou and Tsitsiklis identified this issue while comparing sequential and parallel algorithms for decision processes. For the deterministic stationary case, their Theorem 5 states an NC classification, supported by a finite structural description of a cheapest long walk. Papadimitriou and Tsitsiklis (1987)
The structural description is the subject of this mission. It connects a policy optimization problem to bounded-length graph objects and an exact cost identity. This is useful independently of a particular model of parallel computation: it says which shorter walk and cycle costs determine the answer even when the horizon is very large. Papadimitriou and Tsitsiklis (1987), p. 447
Let be a finite nonempty set of states, with , and fix an initial state . At each state , a finite nonempty set contains the available decisions. A decision has a certain successor state and a real cost . The model is stationary: these data do not depend on time. The corresponding directed graph has one arc for each decision. It may have loops and parallel arcs, because distinct decisions can share endpoints. This is the deterministic graph translation made in §3 of the paper. Papadimitriou and Tsitsiklis (1987), pp. 444–445
A policy is a function of both state and time. Starting at , it produces . In the convention of the paragraph before Theorem 5, horizon means decisions and therefore a walk with arcs. Its cost is
A walk records the states and the decision arc used at each step; states may repeat. A simple path has no repeated state. A simple cycle has positive length, returns to its starting state, and has no other repeated state. A closed walk may repeat states internally and need not be a simple cycle. The distinction matters because the structural claim uses a simple cycle, whereas the computation in the target identity uses a cheapest closed walk of a chosen length.
The first milestone identifies with the minimum cost of a -arc walk from . The next milestones record a decomposition into a simple path and simple cycles, the restriction on cycles repeated more than times, and the existence of a cheapest walk with a short prefix and one repeated simple cycle. These are claims in the paragraph preceding Theorem 5, with corrections to the printed exchange and its connectivity justification documented in the formal statements. Papadimitriou and Tsitsiklis (1987), p. 447
For and , let be the cheapest -arc walk from that visits . Let be the cheapest closed -arc walk at . Only choices for which these walks exist are included. The mission's goal is
The bound is the paper's finite compression claim. The divisibility condition makes an integer number of cycle copies. The goal states an exact value, with the inner minima taken over genuine walks and the outer optimum still taken over all policies. Papadimitriou and Tsitsiklis (1987), p. 447
The identity replaces an optimization over arbitrarily many time-dependent policy decisions with costs of walks having fewer than arcs and closed walks of at most arcs. It gives the mathematical statement that must hold before the paper's proposed parallel calculation can be trusted. It also applies when several different decisions have the same endpoints, because each decision remains a separate weighted arc. Papadimitriou and Tsitsiklis (1987), pp. 445, 447
The paper proves the result informally and states the NC classification. The mission seeks machine-checked proofs of the graph and cost statements, including the printed argument's delicate boundary cases. The local proposal contains open Lean theorem statements, not proofs. Reusable outcomes include a decision-walk representation, a cycle decomposition that preserves the multiset of arcs, and finite-horizon policy-to-walk equivalence. A related published result, TropicalLA.exists_repeat, detects repetition for dense max-plus matrices; it does not state this weighted multigraph decomposition or the min-cost identity.
The obstacle is preserving both walk feasibility and the exact number of arcs when repeated cycles are rearranged. A cycle may be the only connection to other parts of a walk, so deleting its last copy can invalidate the remaining sequence. The printed exchange paragraph also reverses the cost-improving direction and appeals to a no-ties perturbation without carrying it through the bounded-prefix conclusion. Those issues affect the claimed bound; merely knowing that a long walk repeats a vertex does not establish the target identity. Papadimitriou and Tsitsiklis (1987), p. 447
Lean represents and each as finite types and uses real costs. The decision sets are nonempty, making policies and arbitrarily long walks available. Policies depend on state and time, as in §2. A walk stores its decisions as well as its states, so loops and parallel arcs are represented. Cycle decompositions preserve endpoints, length, cost, and the multiset of decision arcs. A loop is a simple cycle of length one. Time starts at zero, and an -arc walk has states at indices .
The paper's general finite-horizon definition sums costs from through , while the Theorem 5 paragraph explicitly asks for a -arc walk. This mission follows the latter convention: decisions occur at . The goal also imposes , which the printed loop leaves implicit, and uses a closed walk for because that is what the length- graph calculation computes. It does not assume distinct walk costs. The condition is retained from the paper even though related identities may hold in other ranges. Papadimitriou and Tsitsiklis (1987), pp. 444, 447
Theorem 5's NC membership, processor and parallel-time bounds, the membership-in-P discussion, log-space reductions, PSPACE membership, and Corollaries 1–2 are outside this mission. Mathlib does not supply the PRAM and complexity-class framework those claims require. The target is the exact cost identity behind the algorithm. Defining the optimum directly as the right-hand minimum, restricting policies to stationary policies, or allowing an empty policy class would trivialize or change it. Contributions proving the milestones, the goal, or reusable walk and cycle facts are welcome.
A sum of many rare events is approximately Poisson. For independent Bernoulli trials this is the classical law of small numbers, and its quantitative form goes back to Prohorov (1953) and Le Cam (1960): if are independent with , then the law of is close to the Poisson law with mean , with an error controlled by . Many applications need the same conclusion for dependent trials: runs and clusters in sequences, exceedances of a stationary time series, matches in DNA sequences, extremes of mixing processes.
Louis H. Y. Chen's 1975 paper adapted Charles Stein's method for normal approximation (1970, published 1972) to the Poisson case and obtained explicit error bounds for sums of dependent Bernoulli trials under mixing and -dependence. The technique, now called the Stein–Chen method, became the standard tool for Poisson approximation, through Arratia, Goldstein and Gordon (1989) and Barbour, Holst and Janson, Poisson Approximation (1992).
Timeline:
Let be a probability space and Bernoulli random variables, possibly dependent, with success probabilities . Put
For a real function on the nonnegative integers, the Poisson expectation of is
the mean of under the Poisson distribution with parameter . The quantity to be bounded is for all with ; its supremum over such is twice the total variation distance between the law of and the Poisson law.
Dependence is measured by Ibragimov's mixing condition. Write for the -algebra generated by and for that generated by . The sequence satisfies (4.1) with a nonincreasing sequence if, for all and every event ,
Thus bounds how much knowledge of the first trials can change the probability of an event determined by trials at distance at least . A sequence is -dependent if and are independent whenever ; then (4.1) holds with for , and independent trials are the case .
For every and every with ,
The parameter is free: it trades the local term against the mixing term .
The milestones follow the paper's proof:
The theorem bounds the distance to the Poisson law by quantities a user can compute or estimate: the variance of , the , and the mixing rate. When the trials are weakly dependent and individually rare, , is small, and the bound is small. It recovers Le Cam's independent-case bound up to the constant and extends it to -dependent and -mixing sequences. The expansion (2.6) and the bounds on the Stein solution in §3 are reused throughout the later literature on the Stein–Chen method.
The results of this paper are proved on paper; none of them is formalized in a proof assistant. Mathlib has the Poisson distribution, conditional expectation, independence and regular conditional distributions, but no Stein–Chen identity, no bounds on the Stein solution, and no covariance inequality for -mixing sequences. This mission produces all three, and the companion missions of this series (Theorem 4.2, an order- bound, and Theorem 5.1, a second-order refinement for independent trials) rely on the same objects.
The identities (2.2), (2.6) and (4.7) are finite manipulations, and the bounds of §3 on are elementary real analysis. The main difficulty is the transfer of the mixing condition from events to functions. Condition (4.1) bounds conditional probabilities of single events almost surely, with a null set that depends on the event. Lemma 4.2 needs a bound on for an arbitrary bounded function of a past vector and a future vector ; this requires a regular conditional distribution of given and one null set that works for all events at once (Lemma 4.1). That step uses that is a standard Borel space, and it fails for an argument that handles one event at a time. Lemma 4.3 then needs care with the independent copy and with the three-block decomposition.
All objects are defined in PoissonDepTrials.MixSqrt.Setting. The conventions are:
StandardBorelSpace.Added hypotheses: in the identity (2.6) and in Lemmas 3.3, 3.4 and (2.5), because divides by ; and in Lemmas 4.2 and 4.3, because (4.1) concerns lags of a sequence starting at . The goal has no hypothesis : at every trial vanishes almost surely and both sides are zero.
The goal does not mention , or ; it is stated only in terms of , , the , , , and . The mixing condition is required to hold with a nonincreasing tending to , so it cannot be satisfied vacuously.
Reusable infrastructure includes the Stein–Chen identity (2.2), the bounds on the Stein solution (Lemmas 3.3, 3.4), and the covariance inequalities for -mixing sequences (Lemmas 4.2, 4.3), which apply beyond Poisson approximation. Proofs of any milestone are welcome, as are proofs of the companion results from the goal.
Two parties who can cooperate for mutual benefit must still agree on how to share the benefit. In The Bargaining Problem (Econometrica, 1950) John Nash asked which agreement two rational bargainers of equal skill should reach. His answer is not a model of haggling: it is a list of conditions any reasonable rule should satisfy, together with a proof that exactly one point of the set of feasible agreements is compatible with them. That point maximizes the product of the two parties' utility gains. Known as the Nash bargaining solution, it is the reference point of cooperative bargaining theory. Economics, operations research and networking all use it: in supply contracts, in wage bargaining, and in fair bandwidth allocation, where maximizing a product of gains becomes maximizing a sum of logarithms (proportional fairness).
Timeline:
A bargaining problem is a pair . Here is the set of utility pairs the two players can reach by agreement, including lotteries over agreements. is the disagreement point, the utilities of no cooperation. As in the platform goal, is compact and convex, and some has and (both individuals could gain). Write for the set of such pairs.
A bargaining solution is a map from to . Nash requires:
The paper has no separate INV axiom. It normalizes the disagreement utility to and notes that each utility is then determined only up to a positive multiple (p. 158), so the solution must not depend on that choice.
The goal is the platform theorem NashBargaining.nash_bargaining_solution_unique, posed by
Nickrobbins95 and currently Open. This mission references it and does not restate it. It
asserts that there is a solution such that a solution satisfies selection, INV, SYM, IIA and
PAR if and only if , and that for every
Nash's paper proves the necessity half: a solution satisfying the conditions must select the maximizer of the Nash product. The sufficiency half, that the maximizer map satisfies the five conditions, is not argued in the paper. It must be supplied by whoever closes the goal.
Two further items formalize the paper's examples: the Bill–Jack barter, whose solution is the vertex reached by exactly one exchange, and trade with money, where the solution gives equal money profits.
The Nash product characterization is used, mostly without proof, wherever a "fair" split of a cooperative surplus is needed. Examples are generalized Nash bargaining in supply-chain contracting and labour economics, the proportional-fairness criterion in network rate control, and the Nash-in-Nash models of bilateral negotiations. Many papers that build on it apply it to a specific feasible set. They therefore rely on the necessity direction, which is the step that makes the maximizer the unique answer rather than one answer among several.
The result has been proved since 1950, while the referenced Prove2Me goal remains Open. This mission supplies the milestones of Nash's own argument in the encoding of that goal, so that the necessity direction can be assembled from them. Sufficiency remains as separate work. The two examples are small, concrete checks of the solution concept.
Each step is elementary. The difficulty is in keeping the bookkeeping honest across the normalizations. The axioms are stated on the class , and a solution is a function on a subtype. Every application of INV, SYM or IIA therefore needs a membership proof for a transformed set: the image of under an affine map, or the enclosing square. It also needs the disagreement point to be carried along. The tempting short cut is to argue "without loss of generality and ". That is exactly what INV licenses, but only after compactness, convexity, the point where both gain, and the location of inside the square have been re-established for each transformed problem. Uniqueness of the maximizer also needs care at the boundary of the quadrant, where the product vanishes.
Utility pairs are ℝ × ℝ, with u.1 player 1's utility and u.2 player 2's. Milestones 1–5 work
at , the paper's normalization. Milestone 6 has a general and the goal's encoding.
Milestones 1–5 make the following readings explicit:
Milestone 6's five hypotheses are copied verbatim from the goal, and its conclusion is the goal's last conjunct for the given . It does not restate the goal: it has no existence claim and no "if and only if".
Trivializing formalizations are ruled out. The point where both gain is a hypothesis wherever uniqueness is claimed; without it a segment on an axis has many maximizers of . The square is a concrete set, not "some symmetric compact convex set", and the solution's properties are quantified over the goal's class , which is nonempty.
The examples need finite sums, convex hulls of finite sets, and extreme points, all in Mathlib. Contributions are welcome on each milestone and on the sufficiency half of the goal.
Related platform work treats other bargaining models. These are Rubinstein's alternating-offers
game (RubinsteinBargaining.PEP) and the Chatterjee–Samuelson sealed-offer double auction
(ChatterjeeSamuelson). Neither is used here. The von Neumann–Morgenstern utility theorem behind
the normalization is formalized as TheoryOfGames.Utility.utility_existence_uniqueness.
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.
Many decision problems in control, finance and engineering must hold against an uncertain parameter whose distribution is unknown, while samples of (measurements, historical records, simulations) are available. The scenario approach replaces the uncertain constraint by the constraints of the observed samples and solves the resulting convex program. The open question is then how robust its solution is: with what probability does a new, unseen violate it?
The classical answer, due to Calafiore and Campi (doi:10.1007/s10107-003-0499-y, 2005; doi:10.1109/TAC.2006.875041, 2006) and sharpened by Campi and Garatti (doi:10.1137/07069821X, 2008), is an a-priori bound: it depends only on and the dimension , and it is tight for the worst problems. It is conservative for the many problems whose solution is determined by far fewer than samples. Campi and Garatti's wait-and-judge theorem (doi:10.1007/s10107-016-1056-9, Math. Program. 2018) replaces it by an a-posteriori certificate: after solving, count the samples that actually determine the solution and certify the solution at a level that depends on that count.
Timeline:
The decision variable is . A problem consists of a cost vector , a convex domain , convex constraint sets indexed by in a probability space , and convex tie-break functions . Given an i.i.d. sample with , the scenario program is
Ties are broken by minimising among the minimisers, then , and so on; the resulting solution is .
The variational problem (10) is: for a function ,
For every -valued , under Assumptions 1 and 2,
The level is evaluated at the observed number of support constraints. The goal fixes no particular , which keeps it stable under any later choice of levels.
Theorem 1 turns the number of support constraints, which is observed after solving, into a confidence statement that holds uniformly over all convex problems and all distributions. With Theorem 2's choice of , a user who finds support constraints obtains a level comparable to that of a -dimensional problem, which is far below the a-priori level for dimension . The classical bound (2) is recovered as Corollary 1, so Theorem 1 contains the earlier theory.
The result is proved in the paper. As far as is known, it has no machine-checked proof. A formalization produces:
The obvious approach bounds the probability for each value of separately by a binomial tail, then sums. This fails: the event is not known in advance, and summing the individual bounds over loses the uniformity that makes the result useful. The paper instead characterises every convex problem by the -tuple . It then maximises (17) over all tuples satisfying the infinitely many moment conditions (18), which is a generalized moment problem in measures, and solves it by duality.
Two steps carry most of the work. One is the almost-sure identity , which depends on the precise interplay of Assumptions 1 and 2 with the tie-break. The other is passing from the polynomial dual problems to the variational problem (10), which needs a density argument in . The bound itself is quoted from the earlier literature; it needs a Helly-type argument adapted to the lexicographic tie-break.
EuclideanSpace ℝ (Fin d) with its Borel σ-algebra, and samples are Fin N → Δ, indexed from . is a probability measure and is the product measure.ContDiffOn ℝ d on , with derivatives taken within . is a real infimum over a set that is nonempty () and bounded below by .ENNReal.ofReal.Ruled-out trivializations:
Contributions welcome:
Measure.pi;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.
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.
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 .
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.
The chromatic number of a graph is the least number of colours in a proper vertex colouring. Determining it for a typical graph was, in the words of the paper, "one of the best known and most studied unsolved problems in the theory of random graphs". For the dense random graph with fixed edge probability , the clique number had been known precisely since the 1970s, but the chromatic number was known only up to a factor of .
Timeline:
Let , let , and let . For a fixed real , the random graph includes each of the pairs of vertices as an edge independently with probability . A graph on with edges thus occurs with probability . A property of graphs holds for almost every if its probability tends to as .
Put and . Write for the natural logarithm and for the integer part of , and set
is slightly larger than the independence number of , which is about .
Supporting objects: is the expected number of -cliques of , and is the same with for . is the maximal number of pairwise edge-disjoint subgraphs, and is the number of subgraphs that share no edge with any other . Finally .
Both bounds are part of the goal. The companion statement for almost every is a separate item.
Theorem 4 settles the first-order asymptotics of for constant : . It shows that the trivial lower bound is asymptotically tight. It also shows that greedy colouring, which uses about twice as many colours, is far from optimal. The method also became standard: concentration of a cleverly chosen packing variable, combined with the edge-exposure martingale. It reappears in Łuczak's extension to sparse random graphs and in the later literature on the concentration of .
The theorem has been proved since 1988 and is textbook material (Bollobás, Random Graphs; Alon–Spencer, The Probabilistic Method). As of this mission it has no machine-checked proof in Mathlib. A formal proof would add:
SimpleGraph (Fin n);The natural first attempt is to colour greedily and to control the independence number of every large vertex set by a union bound. It fails. The probability that a fixed set of vertices has no independent set of size about is not small enough to beat the sets. The second moment method gives only a polynomially small failure probability, and that is what limits earlier results to a constant factor.
The paper needs a failure probability of order for the absence of a large independent set. Two difficulties block this:
Replacing by the edge-disjoint packing number restores the Lipschitz property. The price is a lower bound on , which requires the count of "isolated" cliques and a delicate estimate of the overlap sums . These estimates depend on being within of the clique number, so the asymptotics of and of the binomial coefficients must be controlled uniformly in .
Fin n, graphs are SimpleGraph (Fin n), and is given by explicit finite sums: the weight , probabilities and expectations. No measure is built for the random graph. "Almost every" is Tendsto (fun n => P_n) atTop (𝓝 1). Lemma 1 alone is stated on an arbitrary probability space with a Mathlib Filtration and Martingale.Asymptotics.IsLittleO. Hypotheses on -indexed sequences hold for all large , because cannot hold for small .chromaticNumber, which is finite on Fin n and converted to ℕ. are integers built with Int.floor and Real.logb d. For small they take junk values that no asymptotic statement depends on.SimpleGraph (Fin n);Contributions to any of these are welcome, as are independent proofs of the deterministic milestones (greedy colouring, the final inequality, the complement identity).
The simplex method solves a linear program by walking along the edges of the feasible polyhedron, from vertex to vertex. However cleverly a pivot rule chooses its steps, it cannot reach the optimum in fewer steps than the graph distance from the starting vertex. The largest possible graph diameter of a polyhedron therefore bounds from below the worst-case number of pivots of every pivot rule, and whether that diameter is polynomial in the size of the problem is one of the basic open questions of linear optimization (Klee–Kleinschmidt 1987).
Timeline.
A polyhedron in is the solution set of finitely many linear inequalities,
It may be bounded or unbounded, and empty. Its vertices are its extreme points. Two distinct vertices are adjacent when the segment is an edge of , a one-dimensional face; unbounded one-dimensional faces (rays) are not edges. The graph consists of these vertices and edges, and its diameter is the largest graph distance between two vertices. Kalai and Kleitman write for the largest diameter of the graph of a -dimensional polyhedron with facets.
For a set of row indices, the relaxation is the polyhedron obtained from by ignoring the inequalities with index outside . A walk of steps is a sequence of points in which each step stays put or crosses an edge; "diameter at most " means that any two vertices are joined by such a walk, which includes connectivity of the graph.
Stated for polyhedra given by inequalities: for all and all , , the graph of is connected and has diameter at most . No nonemptiness, boundedness or full-dimensionality is assumed.
The bound is polynomial in for each fixed , and overall. Before it, every bound was exponential in or subexponential in . It remains, up to improvements of the exponent, the best known upper bound on the diameter of polyhedra, and thus the best known limit on how badly an optimal pivot rule must behave. Its proof is also the template for the later abstractions of the problem (connected layer families, subset partition graphs) in which the polynomial Hirsch question is studied.
The bounded case is already formalized on the platform: Hirsch.kalai_kleitman_bound states the theorem for nonempty bounded polytopes and is Proved, together with the bounded forms of the recursion (Hirsch.kalai_kleitman_recursion), of the facet step (Hirsch.facet_reduction, Hirsch.facet_walk) and of the zero-row reduction (Hirsch.diamLE_of_nonzero_rows), and the one-step relaxation lemma Hirsch.relaxation_no_new_neighbours. Kalai and Kleitman state Theorem 1 for all polyhedra: their introduction contrasts unbounded polyhedra (where Hirsch fails) with bounded ones. This mission formalizes the theorem as the paper states it, including unbounded polyhedra, where the bounded proofs do not apply as written. The combinatorial abstraction of the same bound (EHRR10.KalaiKleitman.diameter_le_kalai_kleitman, for the Eisenbrand–Hähnle–Razborov–Rothvoß model) is a different object and is not reused.
The bounded argument relies on compactness: faces are polytopes, every relaxation used in the induction is again a polytope, and the facet of a polytope is a polytope of one dimension less. The relaxation contains and is typically unbounded even when is bounded, and for an unbounded polyhedron a face on a facet hyperplane can be unbounded or have no vertices at all. Each step must therefore hold for general polyhedra: that a shortest walk in between two vertices of the ball uses only edges of , and that the graph of a face, identified with a polyhedron in , sits inside . The "maximal positive number " of the paper need not exist, and the proof must handle the two cases (no radius qualifies; every radius qualifies) separately. Zero rows are allowed in the goal and must be removed before the recursion applies, since a zero row with is tight everywhere.
Lean represents as EuclideanSpace ℝ (Fin d) and the polyhedron as Hirsch.Hpoly a b with a : Fin n → ℝ^d, b : Fin n → ℝ, from the published definition Hirsch_model, which also supplies adjacency Hirsch.Adj (the segment is an extreme subset) and the diameter predicate Hirsch.DiamLE. The mission commits to these explicit readings:
∀ a b, DiamLE (Hpoly a b) N over inequalities in . This is equivalent to the facet formulation, since a -dimensional polyhedron is cut out by its facet inequalities and a polyhedron given by inequalities in has dimension at most and at most facets.Real.logb 2), the power is the real power, and the integer bound is its floor ⌊·⌋₊, which is equivalent because distances are natural numbers.Fin n.A statement with a boundedness or nonemptiness hypothesis, with the graph diameter measured by a distance function whose value on unreachable pairs is , or with the bound read with Nat.log or the natural logarithm, is not the target. Contributions welcome: proofs of the general-polyhedron facet step and of milestone 3, a general zero-row reduction, the arithmetic of milestone 6, and the base cases and .
A retailer that decides which products to display, an online platform that decides which items to show in a recommendation slot, and an airline that decides which fare classes to open all face the same problem: the set of options offered changes what customers buy, and the substitution pattern is not known in advance. The multinomial logit (MNL) model is the standard model of this substitution in revenue management (Talluri and van Ryzin 2004), and optimizing the offered set under a known MNL model is a classical, efficiently solvable problem (e.g. Rusmevichientong, Shen and Shmoys 2010, for a capacity constraint).
The MNL-Bandit asks what happens when the MNL parameters are unknown and must be learned from the purchases themselves, while revenue is being earned. Earlier approaches (Rusmevichientong, Shen and Shmoys 2010; Sauré and Zeevi 2013) separate exploration from exploitation and need the gap between the best and the second-best assortment to be known. Agrawal, Avadhanula, Goyal and Zeevi (Oper. Res. 2019, arXiv:1706.03880) give a single upper-confidence-bound policy whose regret is of order up to logarithmic factors, with no such knowledge. This mission formalizes that result, Theorem 1 of the paper.
There are products with known revenues . At each time the seller offers an assortment from a family of feasible subsets of , and one customer either buys a product or buys nothing (). Given , the choice follows the MNL model with attraction parameters and :
independently of the past. The expected revenue of is . The family is described by totally unimodular constraints, with the incidence vector of , totally unimodular and integral (cardinality constraints are the main example). A policy chooses from the past choices, and its regret is
The seller knows and but not .
Algorithm 1 works in epochs: epoch offers one assortment repeatedly until a customer buys nothing. Let be the number of purchases of in epoch , the number of the first epochs that offered , and the average of over those epochs. The algorithm forms the upper confidence bounds
starting from , and offers next the assortment in that maximizes .
Under Assumption 4.1 (every , and is closed under taking subsets) there are absolute constants such that for every instance and every horizon ,
The constants are not fixed: the goal asserts the order of the regret, which is what the paper claims.
The milestones follow the proof in Appendix A of the paper:
Theorem 1 shows that learning the choice model costs only revenue, with no dependence on how separated the instance is. The paper also proves a lower bound of order under a -cardinality constraint (its Theorem 2), so for small the bound is optimal up to logarithmic factors. The epoch device used here reduces the analysis of a choice model with substitution to unbiased i.i.d. estimates of each .
The result is proved in the paper (Appendix A, with the concentration bounds in Appendix D). It has not been machine-checked. A formal proof would also settle several printed slips that the formalization had to repair (listed under Formalization scope). The concentration bounds for geometric variables, Theorem 5 and Corollary D.1, are useful outside this mission.
The estimates are counted in epochs whose assortments are chosen adaptively from earlier estimates, so they are not independent a priori. The paper's argument that they are i.i.d. geometric with mean has to be made rigorous for an adaptive policy. The variables are unbounded, so the standard Chernoff–Hoeffding bounds for bounded variables do not apply, and the number of samples is random, which requires a union bound over all its possible values. Finally, the regret is a sum over customers while the analysis is per epoch, and the two are linked through the expected epoch length under a random number of epochs and a horizon that cuts the last one.
Fin N; a choice is none (no purchase) or some i. The parameter is normalized to , as the paper allows. Algorithm 1 is deterministic, so a history of horizon is a sequence of choices with the product law , and every expectation is a finite sum. The revenue is the published definition ChoiceCDLP.MNL.mnlObjective v r 1 S.The paper's own proofs are in its Appendices A and D.
Online bipartite matching asks an algorithm to assign arriving requests to resources it cannot reassign later. In display advertising, the requests are page views (impressions) and the resources are advertisers who have bought a fixed number of impressions in advance; each impression must be served immediately or lost. In the adversarial model, Karp, Vazirani and Vazirani (STOC 1990) showed that the RANKING algorithm achieves a fraction of the optimum in expectation, and that no online algorithm does better. Advertising systems, however, have historical traffic data, which motivates the i.i.d. model: the impression types are drawn independently from a distribution that is known in advance.
Feldman, Mehta, Mirrokni and Muthukrishnan (arXiv:0905.4100, FOCS 2009) were the first to beat in this model, with an algorithm that achieves with high probability. Their Section 3 asks the complementary question: how close to can any online algorithm get when the distribution is known? Their Theorem 3 answers that the expected approximation factor of every online algorithm is bounded strictly away from , already on a graph with six vertices. Later work in the same model (Manshadi, Oveis Gharan and Saberi, SODA 2011, arXiv:1007.1673) sharpened both the algorithmic and the hardness side.
An instance consists of a bipartite graph between a finite set of advertisers and a finite set of impression types, a distribution on , and a number of arrivals. In this mission is the uniform distribution on . Online, impressions arrive one at a time; their types are independent draws from . When impression arrives, the algorithm must immediately either assign it to an advertiser with that has not yet been used, or leave it unassigned. Each advertiser can be used at most once, and decisions are final.
A deterministic online algorithm decides what to do with arrival from the types seen so far; it knows , and , but not the future. A randomized online algorithm is a probability distribution over deterministic ones. is the number of impressions the algorithm assigns on the arrival sequence . is the size of a maximum matching of the realization graph, which has one node per arrival , joined to every advertiser adjacent to : the most impressions that could have been assigned with hindsight. The expected approximation factor of an algorithm is
the expectation taken over the algorithm's randomness and the arrivals.
The 6-cycle instance has , and , with the uniform distribution and . The family consists of disjoint copies of the 6-cycle, with the uniform distribution on its impression types and arrivals.
On the 6-cycle, every randomized online algorithm satisfies
and there are a constant and a threshold such that for every and every randomized online algorithm on ,
The second part is the paper's "there exists a family of instances with for which no algorithm can achieve an expected approximation of ", stated on the paper's own family. It leaves unspecified: Appendix B estimates through approximate counts, and a sharper constant would not invalidate the goal.
Theorem 3 sets the ceiling against which algorithms in the i.i.d. model are measured. It rules out an online algorithm with expected factor arbitrarily close to , even though the distribution is known and the instance is tiny, so a constant-factor gap between online and offline matching is intrinsic to the model and not an artefact of adversarial arrivals. The paper's positive results ( for the Suggested Matching algorithm, for Two Suggested Matchings) sit between and this ceiling.
The single-instance bound has a short counting proof. The family statement is argued in the paper only in outline: Appendix B approximates the fractions of copies receiving , , or more impressions, assumes the most favourable outcome on each, and reports the resulting ratio as approximately . A machine-checked proof of the family statement would turn that sketch into a theorem with an explicit constant. To our knowledge neither part has been formalized before.
The single-cycle bound reduces to a finite check, but the paper's "without loss of generality (from the symmetry of the 6-cycle)" hides the cases the algorithm can choose: assigning the first impression to either neighbour, or not assigning it at all. Each case needs its own bad continuation. The passage from deterministic to randomized algorithms is an averaging step.
The family bound is harder. On the algorithm sees all arrivals in all copies and may coordinate its decisions across copies, so the per-copy loss of the single cycle does not transfer by independence. Moreover the target is the expectation of a ratio, , not a ratio of expectations: a bound on the expected loss must be combined with concentration of the number of copies that receive exactly three impressions, and with a lower bound on that holds with high probability. The approximations ", , " of Appendix B have unquantified errors and cannot be used as they stand.
The model is formalized for general finite and with uniform arrivals. Arrival sequences are functions Fin n → I. A deterministic online algorithm is a function that receives the time , the prefix of the first types (Fin t → I) and the current type, and returns an advertiser or none; it cannot read later arrivals. A proposal of a non-adjacent or already used advertiser leaves the impression unassigned, so the encoding covers all online algorithms, including ones that skip an impression while a neighbour is free. A randomized online algorithm is a probability distribution (PMF) on the finite type of deterministic algorithms; by Kuhn's theorem this is equivalent to fresh random choices at each step. is the maximum size of an injective, edge-respecting partial assignment of arrivals to advertisers. The expected approximation factor is a finite average over all arrival sequences, weighted by the algorithm distribution.
The explicit instantiations of the paper's asymptotic wording are as follows:
Lean's division sets . A formalization of the form "there is an instance on which every algorithm has expected factor at most " would be satisfied trivially by a graph without edges, where ; the statements here are on the paper's explicit instances, where every impression type has an adjacent advertiser and on every arrival sequence.
A complete development needs finite case analysis on runs of online algorithms, averaging over mixed strategies, and, for the family, concentration inequalities for occupancy counts (Azuma or McDiarmid, both available on the platform) together with bounds on maximum matchings of disjoint unions. The online-algorithm model and the averaging lemmas are reusable for other lower bounds in the i.i.d. model. Proofs of either milestone, and independent proofs of the family statement with any explicit , 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.
Policy gradient methods adjust a policy by following derivatives of its expected reward. A common expectation is that a small gradient indicates a policy close to optimal. For discounted Markov decision processes, that interpretation can fail when a policy rarely reaches the states where reward is available. Agarwal, Kakade, Lee, and Mahajan study this obstruction as part of their analysis of optimality and distribution shift in policy gradient methods. Their chain example makes the obstruction quantitative: even derivatives of several orders can be exponentially small while the value gap grows with the chain length. Agarwal et al., §4.3 and Proposition 4.1.
The example isolates a specific issue for local optimization. A parameter change at an early state affects reward only after the agent has passed through many intermediate decisions. A local derivative therefore measures the behavior of a policy under its own visitation pattern, which can be very different from the visitation pattern of an optimal policy. This mission states the resulting separation with explicit constants rather than treating “vanishing gradients” as a qualitative description.
A discounted Markov decision process has a finite set of states, a finite set of actions, a transition probability for each state and action, a reward in , and a discount . The value of a policy is the expected sum of discounted rewards when the process starts in state and follows . An optimal policy has value at least as large as every other policy at every state. These conventions are those of §3 of the paper and its unnormalized infinite-horizon value definition. Agarwal et al., §3, pp. 9–12.
The central model is a deterministic chain with states and four actions. At the process moves to . At each interior state , action moves forward to , while move backward to . State is absorbing. The only positive reward is , and . This is Figure 2 and the transition matrix in equation (27). Agarwal et al., Figure 2, p. 11, and (27), p. 50.
The direct policy parameter has three free coordinates at each interior state: the probabilities assigned to . The probability of is their complement. Write for this policy expression and for its value from the starting state. The paper studies parameters whose free coordinates lie strictly between zero and one and whose forward-action coordinates satisfy .
The goal is Proposition 4.1. For , every such , and every nonnegative integer satisfying , it asserts the multilinear operator-norm bound
The same statement compares this policy with an optimal policy:
Both clauses and their constants are part of the target. The derivative order includes whenever the displayed threshold admits it. Agarwal et al., Proposition 4.1, p. 16.
Three supporting targets follow the appendix's attack path. First, equals the entry of the resolvent , where . Second, equation (32) gives the derivative of any entry of in one forward probability. Third, the appendix separately bounds the optimal value below by and above by . A companion theorem records Lemma 3.1: a five-state deterministic example has a value function that is nonconcave in both the direct and softmax parameterizations. Agarwal et al., Appendix B.2, pp. 51, 54, 59; Lemma 3.1, p. 11.
The proposition supplies an explicit family in which local derivative information, even at orders growing with , is small at policies with a large value gap. It limits what a guarantee based only on finding a point with small low-order derivatives can imply about global policy quality. The paper uses this example to motivate attention to state visitation and distribution mismatch in its positive results. Agarwal et al., §4.3, pp. 16–17.
The mathematical result is proved in the cited paper. The remaining work is a machine-checked development of the chain model, its value and resolvent identities, the higher derivative estimates, and the value-gap inequality. The reusable parts include finite-state discounted value calculations, differentiation of a matrix inverse, and operator-norm estimates for multilinear derivatives. The statements in this proposal are proof targets; they do not themselves claim that those proofs have been formalized.
A policy can have a small gradient simply because it almost never reaches the rewarding state. The obvious inference from a near-zero gradient to near-optimal value therefore fails in this model. The technical difficulty is quantitative: each differentiation of a resolvent entry produces terms involving several entries, and the operator norm combines all mixed partial derivatives. The bound must remain exponentially small after that combination, uniformly over every derivative order allowed by the threshold. The second clause must simultaneously show that a policy taking the forward action reaches the reward often enough to create a large value gap. Agarwal et al., Appendix B.2, pp. 54–59.
States are Fin (H + 2) and actions are Fin 4; the parameter space is EuclideanSpace ℝ (Fin H × Fin 3). Its norm is the Euclidean norm, so the norm of the iterated Fréchet derivative is the paper's multilinear operator norm. The first and last states have no free policy parameters. All four actions at induce the same transition to , and the parameterized policy chooses at both boundary states. The resolvent is the matrix inverse of ; its milestone statements are restricted to interior probabilities , where that inverse is nonsingular.
The displayed coordinate assumptions of Proposition 4.1 do not require the three free probabilities at a state to sum to at most one. The Lean goal retains exactly those assumptions. Its value expression is still determined by the forward probabilities, because every other action has the same backward transition and only the absorbing state yields reward. This prevents an added simplex constraint from silently narrowing the proposition. A constant function or a free value variable cannot replace the chain value: is computed from the concrete transition and reward arrays.
The development uses the published finite-state transition-kernel, policy, occupation, value, and optimal-policy definitions. Contributions needed for a proof include stochasticity of the chain, geometric-series evaluation of its absorbing reward, nonsingularity and differentiation of its resolvent, and estimates that pass from mixed partial derivatives to the Euclidean operator norm. For the companion example, direct parameters lie in the product of action simplices, with positive discount; at zero discount its value is constant and the nonconcavity claim would be false.
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.