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?
A seller with limited stock can charge a high price while demand is strong and lower the price before the selling season ends. The timing depends on how many units remain: a markdown that is sensible with ample stock may be premature when only one unit is left. Feng and Gallego studied this decision when each price generates a Poisson demand stream and only one price change is allowed. Their 1995 paper proves that the optimal decision has a threshold in remaining time for every inventory level. This mission formalizes their markdown theorem, including its value-function representation, rather than just the existence of a switching rule.
The model is a finite-inventory revenue problem, relevant when an unsold unit loses its value at the end of a season. It is also a continuous-time stopping problem: the seller observes actual sales and may react to them. A fixed calendar date for the markdown cannot describe all of those decisions. The paper treats the markdown case separately from the markup case, because the order of prices, arrival rates and revenue rates reverses the behavior of the switching boundary. The present mission concerns the markdown case alone.
Let be the initial stock and the time to go. The seller first charges price and may change once to a lower price . Demands at the two prices are independent Poisson counts with positive rates and . A lower price produces more arrivals, so and . Feng and Gallego also assume that lowering the price increases the revenue rate: . There is no salvage payment for inventory left when time expires. These conventions come from §2 and the case split on pp. 1375–1376.
Write for the observed sales count at the initial price by time . If the price changes at deterministic time , let be the expected total revenue. The count after the change is independent of , and their sum has Poisson mean . The optimal value allows the switch time to depend on the counts observed so far. An admissible lies between zero and , is a stopping time for the history of , and occurs before stock is exhausted almost surely. At , is the revenue from charging immediately. The paper defines these quantities in §3, pp. 1377–1379.
The goal is Theorem 1, p. 1380. It asserts a strictly increasing sequence of inventory-dependent thresholds. When , switching immediately earns the optimal value; when , a correction is added:
The theorem specifies the correction, rather than leaving it as an arbitrary difference of values. It starts with . For , set , where is the Poisson-tail expression from §4.1. The threshold is the first nonnegative zero of . A function satisfies for positive time and ; is zero below and equals at and above it. If is the first zero of , the theorem also gives and for .
Three supporting targets match the source's attack path. Equation (17) differentiates immediate-switch revenue. Lemma 2 gives the zeros and one sign change of in the markdown case. Lemma 1 identifies a value function through differential inequalities and its stopping payoff. Each is recorded with its page-level statement in the milestone list.
The threshold sequence turns an adaptive stopping problem into a state rule: inspect remaining inventory and time to go, then compare time with the corresponding threshold. The value representation supplies the expected-revenue quantity on both sides of that comparison. Strict increase means a larger stock requires a larger remaining-time threshold before charging the higher initial price is worthwhile. These are the conclusions of Theorem 1, already proved in the paper.
The work here is a Lean statement and eventual machine-checked proof of that known result. The current theorem items are open proof targets. Formalizing the model gives reusable Poisson-tail revenue expressions and a continuous-time stopping-value interface; Lemma 1 can also serve other Poisson-driven stopping problems once proved. A checked proof would establish that the threshold representation and the optimal stopping value agree under the stated assumptions, including boundary cases that informal notation leaves implicit.
The obvious comparison of two fixed switching times misses the information contained in the sales path. The switch decision can change after each observed arrival, while the threshold for inventory depends on the correction at stock . Showing that every such comparison is organized by one increasing threshold requires more than differentiating the fixed-switch revenue. The paper's appendix handles the interaction between the sign of , the recursive correction, and the stopping-value verification; these are distinct formal targets pp. 1387–1388.
The printed verification lemma and one word of Lemma 2 require care. Lemma 1 omits boundary and regularity conditions needed by its proof. Lemma 2 calls the zero sequence “bounded,” although its thresholds tend to infinity; the usable claim is that they stay above a positive lower bound. The formal statements expose these corrections and retain the rest of the source's conclusions.
Lean represents the first demand stream by a counting process built from independent exponential interarrival times. The terminal revenue after a switch is expressed using the Poisson law of the sum of the two independent counts. The stopping class records the count-generated history, bounds the stopping time by the horizon, and requires stock to remain at stopping almost surely. Its expected payoff uses the number sold before stopping and the immediate-switch value for the unsold stock. Prices and rates are positive, the markdown ordering and revenue-rate inequality are explicit, and the probability measure is named explicitly even though the exponential-interarrival law already entails it.
The paper uses nonnegative real time, inventories indexed by positive integers, and zero salvage. Lean uses a real supremum for the value and a real infimum for each threshold; the admissible payoff is bounded and measurable, and every threshold-defining zero set is asserted nonempty. The ODE is expressed with an actual derivative at positive time. The auxiliary Poisson-tail definition maps a negative mean to zero, but all model applications have nonnegative means. The threshold construction, its ODE, and the equality with the stopping value are all conclusions of the goal, so none is an assumed solution.
For Lemma 1, the formal target adds the initial-time and zero-stock boundary values, domination of terminal revenue, and local Lipschitz regularity in time. The first three conditions are used in the source's own proof or reformulation; local Lipschitz regularity makes its integral calculation valid. Contributions may establish the Poisson-tail calculus, the sign and threshold results, the verification theorem, or the complete markdown theorem. The referenced arrival-process definition is shared infrastructure; the two-price revenue and stopping model are specific to this paper.
Temporal-difference (TD) methods learn to predict an eventual outcome from the differences between successive predictions rather than from the difference between each prediction and the final outcome. Sutton's 1988 paper Learning to predict by the methods of temporal differences introduced the TD() family and gave the first convergence proof for a TD method; before it, as the paper notes (p. 23), "no TD method has ever been proved stable or convergent to the correct predictions". TD learning is now the core of policy evaluation in reinforcement learning, and later analyses (Dayan 1992, Tsitsiklis and Van Roy 1997) start from the setting fixed here.
Timeline:
An absorbing Markov chain has a finite set of nonterminal states, a finite set of terminal states and transition probabilities (, ) with . Let be the matrix . "Absorbing" means that every sequence terminates with probability one; for a finite chain this is .
A sequence starts in a nonterminal state drawn from a distribution , follows the chain through nonterminal states until it enters a terminal state , and then produces a scalar outcome drawn from a distribution with finite mean . Let . The ideal prediction of state is the expected outcome from ,
The learner does not see states, only an observation vector for each , and predicts linearly, . Linear TD(0) with weight updates after each sequence keeps fixed during a sequence and then sets, with ,
Sequences are experienced independently; is the weight vector after sequences. Let be the expected number of visits to in one sequence, , and the matrix with columns .
For every absorbing chain, start distribution , outcome laws with finite means and linearly independent , with every , there is such that for and every ,
The threshold is existential, as in the paper; no explicit value is fixed.
Theorem A.1 (Neumann series under ); (5) the ideal predictions; (7) ; the mean recursion ; Theorem A.2 ( nonsingular); Theorem A.3 (); the Lemma of p. 27; positive definite; the eigenvalues of have positive real parts; and for small .
Theorem 3: under repeated presentations of a finite training set, batch linear TD(0) converges (deterministically) to the maximum-likelihood predictions , with its two supporting steps ( and ). Theorem 1: linear TD(1) and Widrow–Hoff produce the same per-sequence weight changes.
Theorem 2 shows that a bootstrapping method, which learns from its own earlier predictions, is not biased by them in the limit: in expectation it reaches the same predictions as supervised (Widrow–Hoff) learning. Theorem 3 says more: on a fixed data set, TD(0) converges to the predictions that would be exact if the maximum-likelihood model of the process were correct, which differs from the least-squares answer Widrow–Hoff converges to. Together they are the formal basis for preferring TD to Monte-Carlo targets in multi-step prediction.
The results are proved on paper, and not formalized in Lean. A formalization adds a precise model of the experience (i.i.d. sequences of an absorbing chain with terminal-dependent outcome laws), the integrability facts the paper leaves implicit, and a correct proof of the positive definiteness of , whose printed argument has a gap (see below). The matrix lemmas (Neumann series under ; real-part positivity of eigenvalues of for symmetric and positive definite in the non-symmetric sense; the step-size threshold) are reusable for other linear stochastic-approximation analyses.
The obvious argument writes as a linear function of and observes that the iteration matrix is a contraction for small . Two steps of this fail as printed. First, the paper proves that is positive definite through the Lemma of p. 27 with a weakened notion of diagonal dominance (weak in every row, strict in one), under which the Lemma is false; with the standard notion, is in general not strictly diagonally dominant (a row with that cannot leave in one step has row sum ). A correct proof combines weak dominance with reachability of every state from the support of , which is where enters. Second, is not symmetric, so a small does not make a contraction in the Euclidean norm; the argument goes through its eigenvalues, and turning eigenvalues of modulus below one into is a spectral-radius argument. The probabilistic step is also not free: is a polynomial in random sequences of unbounded length, and its integrability and the factorization need independence across sequences.
States are finite types N (nonempty) and T; the chain is the structure AbsorbingChain with blocks pN, pT and the field . Observation vectors are x : N → Fin K → ℝ with LinearIndependent ℝ x; is Matrix (Fin K) N ℝ. A sequence is an Episode (list of nonterminal states, terminal state, outcome); IsEpisodeStream states measurability, mutual independence (iIndepFun) and the law . Expectations are Bochner integrals, and the goal asserts integrability of , so a non-integrable junk value cannot satisfy it. is defined as an expectation (a sum over sequences), not as , so (7) is not circular. "Positive definite" is the paper's footnote 6 ( for real , no symmetry), not Mathlib's Matrix.PosDef.
Trivializations ruled out: the hypothesis is the paper's own discarding of never-visited states (without it the goal is false: an unvisited state's weight never moves); N is nonempty and sums to one, so the hypotheses are satisfiable and the goal is not vacuous; the sequences cannot be arbitrary random variables or a fixed sequence, since their law is pinned to , and ; is chosen before , and the probability space; and the update is per sequence, not the intra-sequence variant of §5.
Corrected slips: "For each nonterminal state " (p. 24) means terminal; the diagonal-dominance definition of p. 27 is replaced by the standard one; (p. 28) means . Not formalized: the variance and TD() conjectures of p. 29, §4.3, and the extension claims of §5.
Related open goals on this platform (different models, credited, not re-posed): SuttonBartoRL.BatchTD.batch_td_converges_to_certainty_equivalence (tabular, discounted analogue of Theorem 3), and SuttonBartoRL.LinearTD.keyMatrix_posDef, posDef_of_row_col_sums, expected_td_update (continuing discounted chain with stationary , where every row sum of is positive). Contributions of any milestone, of general matrix lemmas, and of reusable infrastructure for i.i.d. episode streams are welcome.
A postman, a snowplough or a street sweeper must traverse every street of a district and return to the depot. When some streets are one-way, the street network is a mixed graph: some edges are directed and must be traversed in a prescribed direction, the others are undirected and may be traversed either way. The first question about such a route is whether a closed route exists that traverses every street exactly once, an Euler tour of the mixed graph. When one exists, it is an optimal postman route; when none exists, the postman problem asks which streets to repeat.
J. Edmonds and E.L. Johnson treat this question in §6 of Matching, Euler tours and the Chinese postman (Mathematical Programming 5, 1973), the paper that solved the undirected Chinese postman problem by matching. Section 6 gives an algorithm that finds an Euler tour in any mixed graph that is connected, of even degree and symmetric, and §7 uses it for the mixed postman problem.
Timeline.
A mixed graph has a finite set of nodes and a finite set of edges. Each edge meets two distinct nodes; several edges may meet the same pair of nodes. Some edges are directed: an edge directed away from node toward node must be traversed from to . In Lean an edge has a tail, a head (distinct) and a Boolean directed; for an undirected edge the order of the two ends carries no meaning.
If is connected, even and symmetric, then for every node
The goal contains two classical theorems as special cases. With every edge undirected it is Euler's theorem for connected even multigraphs. With every edge directed it is the theorem that a connected balanced digraph is Eulerian. The milestones connect the two cases: an orientation reduces the mixed case to one the Rule can handle. The Rule itself is the van Aardenne-Ehrenfest–de Bruijn construction, which underlies the BEST theorem counting Euler tours. Milestone 5 decides whether the mixed postman problem has any feasible solution. The mixed postman problem is the standard model for routing on one-way street networks.
All results here are proved in the paper, so none is open. No Lean proof of any of them in this form is known. Mathlib's Eulerian walks are for simple graphs; it has no multigraph or mixed-graph Euler theorem, no directed Euler theorem and no arborescence-based traversal. The mission produces these, together with a reusable vocabulary of mixed multigraphs, walks that respect directions, and arborescences given by parent edges.
The obvious approach to the goal is to forget the directions and apply Euler's theorem. This fails because the tour it produces may traverse a directed edge backwards. Orienting all undirected edges at once also fails: an arbitrary orientation of the undirected edges need not keep every node balanced.
The difficult part of the Rule is showing that the greedy traversal does not get stuck before using every edge. It cannot stop at a node other than because of the degree conditions. The hard step is showing that no edge is left unused when it stops at . The answer depends on the ordering condition: without the arborescence edge last at every node, the Rule can return to with edges still unused. The assignment step needs an invariant: the orientation must keep every node symmetric while it extends a spanning structure of directed edges.
Fintype V, Fintype E). Parallel edges are allowed, including a directed and an undirected edge on the same pair. Loops are excluded (tail e ≠ head e), following the paper's standing setting of §2 (p. 91: edges meet two different nodes). Edges are a type, not a relation on nodes, so parallel edges stay distinct in every walk.Contributions are welcome at every level: proofs of the milestones, a direct proof of the goal, and general lemmas about mixed multigraph walks.
A matching in a graph is a set of edges no two of which share a vertex. Finding a matching of maximum cardinality is one of the basic problems of combinatorial optimization: it models pairing tasks (workers to shifts, kidney donors to recipients, players to rounds), it is a subroutine of algorithms for the travelling salesman and Chinese postman problems, and it was the first problem shown to need more than linear programming over the obvious constraints to be solved exactly.
For bipartite graphs, König's theorem (1931) gives a min–max formula: the maximum size of a matching equals the minimum size of a set of vertices meeting every edge. In general graphs this fails already for a triangle, where a single edge is a maximum matching but two vertices are needed to meet all three edges. Jack Edmonds' paper Paths, trees, and flowers (1965) gave both a polynomial-time algorithm for maximum matching in general graphs, the blossom algorithm, and, as a by-product of its analysis, the correct min–max theorem for general graphs.
Timeline.
A graph is a finite set of vertices and a finite set of edges, each edge meeting exactly two distinct vertices, its end-points. Several edges may join the same two vertices; this is needed because shrinking creates parallel edges. A matching is a set of edges no two of which meet the same vertex; a vertex is exposed if it meets no edge of . "Maximum" refers to cardinality.
An odd set is a set of vertices with an odd number of elements. Its capacity is
A one-vertex set covers the edges meeting its vertex; a set of vertices covers the edges with both end-points in it. An odd-set cover is a family of odd sets such that every edge is covered by some member, and its capacity-sum is .
The proof uses the following objects of §3–§4 of the paper. An alternating path is a simple path whose edges alternate between and the non-matching edges . An alternating tree is a tree whose vertices are split into inner and outer vertices, every edge joining an inner to an outer vertex and every inner vertex meeting exactly two tree edges; it is planted if restricted to the tree is a maximum matching of the tree whose one exposed vertex (the root) is exposed in , and Hungarian if its outer vertices are adjacent only to its inner vertices. A blossom is an odd circuit on which is a maximum matching, leaving one vertex exposed; with a stem (an alternating path from an exposed vertex ending in a matching edge at ) it forms a flower. Shrinking a vertex set replaces it by a single vertex , deletes the edges inside and keeps all other edges; and denote the result for a blossom .
It is stated as: there are a maximum matching and a minimum odd-set cover with .
The matching-duality theorem gives a certificate of optimality: a matching and an odd-set cover of equal size prove each other optimal, and the blossom algorithm produces both. It is equivalent to the Tutte–Berge formula , it contains König's theorem as the case where all members of the cover are singletons, and it is the cardinality case of Edmonds' description of the matching polytope by odd-set constraints, which underlies weighted matching, -matching and the polyhedral approach to combinatorial optimization.
The theorem has been proved since 1965, with several independent proofs (via Tutte's theorem, via the Gallai–Edmonds decomposition, via linear programming). Mathlib contains Tutte's perfect-matching theorem for simple graphs, but neither the Tutte–Berge formula nor odd-set covers, alternating trees, blossom shrinking or Berge's augmenting-path theorem in a multigraph setting. This mission produces a machine-checked version of Edmonds' statement together with the lemmas of his algorithmic proof (4.12, 4.14, 4.15, 4.17), which are the correctness core of the blossom algorithm.
Weak duality and Berge's theorem are elementary. The difficulty is the strong direction. The obvious argument, a search for augmenting paths from an exposed vertex, fails because an alternating search tree in a non-bipartite graph can close an odd circuit, after which a vertex is reachable both by an even and by an odd alternating path; a naive search either misses augmenting paths or must back-track exponentially. The proof therefore has to work in shrunken graphs, whose vertices are nested sets of original vertices, and transfer maximality and covers back through every shrinking (4.12–4.15). Keeping track of nested blossoms, of the identity of edges under shrinking and of the parity bookkeeping of 5.8 is the main formal burden.
EdmondsMatching65.Polyhedron.Graph V E (a map from edges to unordered pairs of distinct vertices) with finite V, E; parallel edges are allowed and loops are not. Matchings are Finset E. Maximum and minimum are by cardinality, stated with explicit comparisons rather than sSup/sInf.Finset (Finset V); repeating a member only adds capacity, so this does not change the minimum. The capacity of a singleton is , not .Reusable beyond this mission: the multigraph shrinking construction, blossom sets, alternating and Hungarian trees, and Berge's theorem in the multigraph setting; these are shared with the companion mission on the invariance of the dual (Gallai–Edmonds). Proofs of any milestone, and alternative proofs of the goal (e.g. through Mathlib's Tutte theorem), are welcome.
Stochastic dual dynamic programming (SDDP), introduced by Pereira and Pinto in 1991, is the standard method for multistage stochastic linear programs with many stages, such as hydro-thermal scheduling and long-term energy planning. It approximates each stage's expected future cost from below by the maximum of finitely many linear functions (cuts), built from LP dual solutions at sampled states, and alternates a forward simulation pass with a backward cut-generation pass. Practitioners stop the method when a simulated upper bound is close to the lower bound . Whether this procedure converges at all is the question of this mission.
Timeline:
There are stages. Stage has a decision in , costs , a matrix and, for , a matrix coupling to the next stage. At stage the constraint is . For the right-hand side is random: , where takes values with probabilities , independently across stages. The expected cost-to-go is defined backwards from :
and is the problem [LP1]. Assumption (A4) says every stage problem met along the way has a nonempty, bounded feasible region.
The approximate problem [AP] replaces by over the cuts generated before iteration ; its value is . A scenario fixes one outcome per stage . Each DOASA iteration (i) samples one forward scenario and solves [AP] along it, giving states ; (ii) for runs the Cut Calculation Algorithm (CCA): it solves [AP] at for the outcomes in a backward sample , stores optimal extreme-point dual solutions in a collection , picks for every outcome the best stored dual, and averages them into a new cut on . DOASA-N instead traverses a fixed list of scenarios in every iteration.
If, with probability 1, every scenario prefix is followed by the forward pass jointly with each outcome being in the backward sample infinitely often (property J), then with probability 1 every DOASA run has an iteration after which the cuts no longer change, the policy they induce is optimal for [LP1], and
The theorem justifies SDDP, AND, ReSa and CUPPS as exact methods: on a finite scenario tree, sampling-based cutting-plane schemes reach an optimal policy and a tight lower bound after finitely many iterations, almost surely. The finiteness argument (Lemma 1) is the template for later finite-convergence proofs of SDDP variants.
The paper's proofs are informal. No part of this development is machine-checked, and the printed statement of Theorem 4 is false (see below), so a formal proof also settles exactly which sampling hypothesis is enough. The finite-cut lemma and the cut-validity milestone are reusable for any Benders-type multistage method.
The obvious argument goes: cut sets stabilize (Lemma 1), and every scenario and every outcome is sampled infinitely often, so the limiting cuts must be exact. The last step fails. A cut at a state is exact only if, for every outcome, a dual that is optimal at that state has been collected. Sampling the forward scenario and the backward outcomes infinitely often, but separately, does not ensure this. Lemma 1 itself is also delicate: the dual vectors grow in dimension with , so the collection of extreme-point duals can be infinite even though the cut coefficients take finitely many values. The algorithm's choices (extreme-point duals, ties among best duals) must be handled for every run, not for a convenient one.
Stages are numbered with variable dimensions per stage. B t is the paper's , the matrix multiplying in stage . Value functions are real infima, used only on reachable states. Iterations are numbered from in Lean. Explicit choices, each recorded in the item statements:
A trivializing encoding, in which cuts are arbitrary valid hyperplanes, duals are taken for all outcomes, or the sampling hypotheses directly assume exactness of the cuts, is ruled out: the run relation transcribes CCA steps 1–3 as printed.
A complete development needs LP weak and strong duality (published on the platform as LinearOptimization.lp_weak_duality and LinearOptimization.lp_strong_duality, in their own encoding), finiteness of the set of extreme points of a polyhedron, and the almost-sure intersection of finitely many events (Mathlib). Contributions to any milestone, to the proof that J holds for independent sampling, and to the counterexample showing FPSP and BPSP are insufficient are welcome.
The number of successes in many rare trials is approximately Poisson. For independent trials the quality of that approximation was quantified by Le Cam in 1960: if are independent Bernoulli variables with , and , the total variation distance between the law of and the Poisson law with mean is bounded by a constant multiple of , and by a constant multiple of when . Many applications have dependent trials: occurrences of a pattern in a sequence, exceedances of a high level by a stationary process, failures in a system with local interactions. L. H. Y. Chen's 1975 paper extended Charles Stein's method of normal approximation to the Poisson case and obtained explicit bounds for dependent trials. The approach became known as the Stein–Chen method, and is now the standard tool for Poisson approximation of dependent counts.
Timeline.
This mission formalizes the order- bound of that paper, Theorem 4.2.
Let be a probability space and let be Bernoulli trials: random variables with values in and . Following the paper, set for and . Put
For a bounded real function on the nonnegative integers, the Poisson expectation is
the mean of under the Poisson law with parameter . The quantity of interest 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 (4.1). Let . There must be a non-increasing sequence such that for all and every event ,
A sequence is -dependent when and are independent for all . It then satisfies (4.1) with for .
The proof works with the partial sums , , and . It also uses the Stein solution , the solution for of .
For every and every with ,
The bound involves only the law of through , the success probabilities, the window and the mixing rate. The window is free, so the statement covers every trade-off between local dependence and mixing.
The milestones follow the paper's proof:
Theorem 4.2 gives an error of order times the excess variance , plus a mixing remainder. When the trials are nearly uncorrelated, and the bound is small even though is large. This is the regime where the companion Theorem 4.1, which carries a factor , is weaker. The independent case recovers Le Cam's order with constant 10. The -dependent case gives explicit Poisson limit theorems for scan statistics and pattern counts.
All results of the paper are proved there, and the proofs are elementary apart from the measure theory of Lemma 4.1. To our knowledge none of them has a machine-checked proof. Mathlib has the Poisson distribution and conditional expectation, but no Stein–Chen bound and no mixing inequality of Ibragimov's type. A formal proof would give the first checked quantitative Poisson approximation for dependent trials. It would also give reusable covariance inequalities for -mixing sequences (Lemmas 4.2 and 4.3).
Most of the work is bookkeeping, and it is heavy. Identity (2.2) needs a telescoping over windows whose ends can fall outside . (4.15)–(4.18) need to be compared with with explicit constants.
The genuinely probabilistic step is the decoupling of Lemma 4.2. Condition (4.1) controls conditional probabilities of events. Lemma 4.2 needs a bound on conditional expectations of functions of a whole random vector. Passing from one to the other requires a regular conditional distribution that is uniformly close to the unconditional law on a set of full measure (Lemma 4.1). The naive route, applying (4.1) to each level set of a simple function, loses a factor that grows with the number of levels and does not give the constant .
The bound (4.16) applies Lemma 4.4 to a subsequence of the trials. This uses the fact that dropping variables preserves (4.1) with the same , because is non-increasing.
A trivializing formalization is ruled out. Measurability of the trials is part of the definition, because otherwise conditional expectations in (4.1) collapse to . The goal mentions only , , , , , and . It does not mention or any milestone quantity.
A complete development needs the Stein solution and its bounds, a Bernoulli-sum calculus over integer
windows, regular conditional distributions on standard Borel spaces, and the mixing covariance
inequalities. The last two are reusable beyond this mission. Contributions to any milestone are
welcome, as are alternative proofs of Lemma 4.2 through Mathlib's condDistrib.
Sampling uniformly from a bounded region can be difficult when direct transformation of a familiar random variable is unavailable and rejection sampling spends most of its trials outside the region. Robert L. Smith studied procedures that move within the region: from the current point, choose a direction, form the line set through that point inside the region, and choose the next point uniformly on that line set. The resulting sequence is a homogeneous Markov chain. The Random Directions Algorithm, later commonly called hit-and-run, is a central instance of this construction. Smith's 1984 paper establishes conditions under which the chain approaches the uniform distribution even when its initial point is fixed rather than sampled uniformly (Smith 1984, pp. 1298–1301).
For simulation, the initial point is usually chosen because it is known to be feasible. The question is therefore whether the distribution after many moves forgets that particular choice. A stationary distribution alone does not answer this: stationarity describes what happens if the chain already starts with that distribution. Smith's Theorem 2 gives the stronger, pointwise starting-state statement for the class of symmetric mixing algorithms satisfying his two regularity assumptions (Smith 1984, p. 1301).
Let be the state region and its finite, nonzero content measure. In Smith's geometric setting, is a bounded -dimensional measurable region in , and is -dimensional content; at , content is counting measure. A Markov transition kernel assigns to every current point a probability of entering a measurable set on the next move. For the associated chain , the -step transition probability is .
The uniform law is . Smith's Assumption (a) gives a measurable transition density relative to :
For a symmetric mixing algorithm, the paper states that this density satisfies for all . Assumption (b) says for all such pairs. These are pointwise conditions, including states of zero -measure. A nonempty measurable set is closed if for every . The chain is indecomposable in the paper's sense when it has no two disjoint closed sets (Smith 1984, pp. 1299–1300).
Lemma 1 asserts that is stationary: for every measurable . Lemma 2 excludes two disjoint closed sets. Both are direct prerequisites of the goal. Smith's Theorem 1 also establishes uniqueness of the stationary distribution and almost-sure convergence of empirical visit frequencies under a stationary start; it is described in the source, but its trajectory-level formalization is outside this proposal (Smith 1984, p. 1300).
The mission goal is Smith's Theorem 2. For every and every measurable ,
This is the paper's explicit meaning of strongly mixing. The milestone list also records the proof's stated nonperiodicity condition: for every , the -step transition law has no two disjoint closed sets. It is a target in its own right because it concerns all higher-step kernels, not only the one-step chain (Smith 1984, p. 1301).
Theorem 2 makes the uniform law the limiting distribution of the sample at time , for any fixed feasible initial point. The paper's Theorem 1 supplies a different guarantee about long-run empirical frequencies under a stationary start, although it is not a target of this proposal. Smith later specializes the framework to the Random Directions Algorithm and gives a quantitative rate under additional geometric conditions; that rate is the subject of the companion mission (Smith 1984, pp. 1303–1304).
These results are proved in the paper but the declarations in this proposal are theorem statements with sorry, not machine-checked proofs. A completed formalization would turn the paper's measure-theoretic claims into reusable statements about general measurable state spaces and kernels. The normalized content law, the density interface, and closed-set predicate can be reused when studying other Monte Carlo kernels with the same hypotheses.
The main obstacle is the jump from stationary behavior to convergence from every starting point. Symmetry identifies the candidate stationary law, and strict positivity limits how the chain can split into closed parts, but neither sentence by itself establishes the claimed limit of . The distinction matters especially at starting points in -null sets: an almost-everywhere starting-state result would leave out precisely the universal claim in Theorem 2. The paper appeals to a general-state Markov-chain convergence result for this step (Smith 1984, p. 1301).
Lean uses a measurable type as the whole region , a finite measure with , a Markov kernel , and an extended-nonnegative density . The density is jointly measurable and is linked to by the integral identity above; symmetry is pointwise, and positivity is added only for Lemma 2 and Theorems 1–2. This abstract representation retains the hypotheses those results use without fixing a particular Euclidean dimension. It covers the counting-content case as well as continuous content, although it does not construct the geometric direction-and-chord algorithm. The Random Directions kernel belongs to the companion mission.
The uniform law is normalized by . Finiteness and nonzero total content prevent a meaningless inverse or an empty probability space. The -step law is the published MarkovChainCLT.iterKernel. Theorem 2 quantifies over every , rather than -almost every , and uses setwise convergence on each measurable . No invariance, uniqueness, minorization, or convergence premise is added to the goal. Detaching from would empty out the substantive assertion. Formal contributions can target the density-to-invariance argument, the closed-set conditions, and the general-state convergence theorem needed for the goal. The paper's separate pathwise Theorem 1 remains an appropriate later extension.
Convex minimization often has a simple objective but no useful closed form for its minimizer. A proximal method replaces one difficult minimization by a sequence of regularized minimizations. The familiar quadratic regularizer treats all directions through a Euclidean norm. In applications with nonnegative variables, entropy-like geometry can be more natural: a step can be penalized by a Bregman distance generated by a strictly convex function. Chen and Teboulle studied a proximal minimization algorithm with this geometry and established a rate in objective values together with convergence of the iterates under the paper's assumptions. Their analysis also removed a bounded-below assumption used in an earlier treatment and allowed step sizes whose sum diverges even if individual steps approach zero (Chen and Teboulle, 1993, pp. 539–540).
This mission records the complete theorem of that paper, rather than only its rate when a minimizer is known to exist. The distinction matters because a proper convex objective can have an infimum of or a finite infimum that it never attains. The rate against each comparison point remains meaningful in those cases, and the theorem's value convergence does not presuppose a minimizer.
Let be a finite-dimensional real normed space, the nonempty effective domain of a proper lower semicontinuous convex objective, and its finite restriction. Its value outside is . Thus is an extended-real number that may equal , and is the set of minimizers, possibly empty.
A Bregman function with zone is a function on the closure of an open set . It is continuously differentiable on , strictly convex and continuous on , and satisfies the bounded partial-level-set and two sequential conditions of Definition 2.1 (Chen and Teboulle, 1993, p. 539). Its distance-like expression is
It is nonnegative and zero exactly when , but need not be symmetric or satisfy a triangle inequality. The zone contains the relative interior of . Starting from and positive steps , a PMD run selects minimizing over , for . Write . The paper calls this proximal minimization with D-functions (Chen and Teboulle, 1993, pp. 539–540).
For every and every finite comparison point , the goal includes
If , then in the extended reals, including when . This is Theorem 3.4's inequality (20) and its ensuing value-convergence claim (Chen and Teboulle, 1993, p. 542).
For every , the same rate gives
When and , the entire sequence converges to a point of . The displayed bound is (21), and convergence of the iterates is the final clause of Theorem 3.4. The milestone list follows the authors' statements: the three-point identity, nonnegativity of the distance, Lemma 3.2, and the three parts of Lemma 3.3. Display (17) is an additional supporting theorem item (Chen and Teboulle, 1993, pp. 539–542).
The rate compares a PMD iterate with any admissible point, so it gives a finite-horizon certificate even before an optimal point is identified. If a minimizer exists, substituting it gives an explicit objective-gap bound. With divergent cumulative steps, the theorem identifies the limiting objective value without assuming that value is finite. Its final clause goes further: when the optimum is attained, the points themselves converge, not merely their objective values (Chen and Teboulle, 1993, p. 542).
The mathematical result was proved in 1993. The formalization task is to state and prove it in Lean with the extended objective, full Bregman-function conditions, and sequence limits visible to later developments. The three-point identity is already posed as a separate public platform theorem from a later mirror-descent treatment; this mission reuses that statement. The remaining statements here are proof obligations, not claims of completed machine-checked proofs. Their definition layer can also support analyses of other nonquadratic proximal algorithms.
The direct one-step minimization comparison alone does not yield the global estimate with and the exact weighted distance terms of Lemma 3.3(iii). It also does not settle convergence of the points: decreasing objective values can coexist with several cluster points. The Bregman function's bounded partial level sets and sequential conditions are needed to rule out that behavior. A further issue appears when : replacing the infimum by a real number, or assuming a minimizer to define it, removes a case that Theorem 3.4 explicitly covers. The original paper separates these issues across Lemmas 3.2–3.3 and Theorem 3.4 (Chen and Teboulle, 1993, pp. 540–542).
Lean uses a finite-dimensional real normed space in place of ; none of the statements depends on a chosen Euclidean inner product. A derivative is a continuous linear functional, and its value on a vector represents the paper's gradient pairing. The Bregman distance is the already-published definition with the derivative at its second argument. The paper's is represented by a total function whose values outside are unused. Strict convexity on includes convexity of . The last sequential condition explicitly requires its first arguments to lie in , the domain where the paper defines .
The extended objective is a nonempty convex domain , a real-valued restriction , and an extended-real function equal to off . Lower semicontinuity applies to that extended function. The infimum is taken in the extended reals; it cannot silently become zero when the values are unbounded below. A PMD run is a predicate on an existing sequence, recording a minimizer in at each step. This makes explicit the existence consequence for which the paper assumes the gradient of has full range; it does not define iterates by a choice operator. Every Bregman distance differentiates at a point of , where is . The rate starts at , so and no finite value is demanded of . No lower bound on is imposed. Contributions proving the milestone inequalities, the extended-real value limit, the Bregman-function examples, and the compactness step for iterate convergence are within scope.
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 .