Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. A high-probability approximation guarantee is a separate claim requiring an explicit probability bound. The optimum includes entangled states. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A firm may know salary bounds and the ranking of positions without having a reliable sample of individual salaries suitable for least-squares estimation. Charnes, Cooper and Ferguson used that kind of partial information to estimate a salary formula from ratings assigned to job factors. Their 1955 paper gives a model in which weights respect the job hierarchy while the implied salaries approach specified salary levels as closely as possible. It then turns the sum of absolute deviations into a linear program that can be handled by the methods available for constrained optimization. The setting and transformation are in §§4–6 of the published paper.
The question here is a precise one: does the transformed program have the same optimal value and the same optimal salary weights as the original absolute-deviation problem? This matters because a linear-program solution should answer the compensation-estimation problem stated before the transformation, even though the transformed program has additional variables and a different feasible set. The mission also records the paper's seven-position numerical example, where the reported salary formula can be checked directly against the table of factor ratings.
There are rated factors and job levels ordered from highest to lowest. The rating is the amount of factor required at level , and is the nonnegative weight assigned to that factor. The estimated salary at level is
The salary formula applied to a person's factor amounts is . For the ranked positions, feasible weights satisfy the four parts of the paper's system (2): each ; the top-level salary is at most the ceiling ; successive salaries descend, ; and the bottom-level salary is at least the floor . These are one-sided ceiling and floor bounds. They do not force the fitted salaries to equal the bounds.
The firm specifies target salaries at a finite set of levels, which includes the ceiling and floor levels in the examples and may include intermediate levels. The absolute-deviation objective of (3) is
The original problem minimizes over the feasible weights. At a specified level, let . The split-variable program of (4)–(5) introduces with and minimizes . The split variables are constrained only for levels in . The salary constraints (2) continue to apply to . This is the paper's transformed linear program, with a feasible set that contains many choices of above the same weight vector Charnes, Cooper and Ferguson, §§4–5.
The main target is the paper's claim that the two problems have equal minimal values and that minimizers correspond §6, p. 143. In the formal statement, equal values are expressed by equality of attainable objective thresholds:
The goal also says that minimizes exactly when the triple formed from and the positive and negative parts of minimizes . Every LP minimizer projects to a minimizer of . These clauses give the value and solution correspondence the authors use when they call the two problems equivalent.
Three milestones follow the paper's exposition. First, every feasible weight vector has a split-variable lift with the same objective. Second, every transformed feasible point projects to an original feasible weight vector with no larger original objective. Third, the minimal values agree §§5–6, pp. 141–143. Each is recorded under the unnumbered sentence from which it was extracted; the paper has no numbered lemmas.
Two companion statements record other claims: opposite coefficient columns cannot both occur among selected independent simplex columns, and the Table I data have the reported optimum. For the latter, targets are 16 at , 10 at , and 4 at , measured in thousands of dollars. Equation (7) assigns weights , yielding the minimum deviation §7, pp. 145–148. A further companion checks the redundant ranking row.
The equivalence justifies using a linear-program output as an estimate for the earlier salary problem: the transformed objective reaches the same value, and its optimal weight vectors solve the original problem. The numerical claim supplies a fully specified instance with seven job levels and nine factors, including the exact fitted salaries. Without the correspondence, optimizing the enlarged variable set could give no assurance that its weights minimize the deviations the firm intended to measure.
The mathematical result was argued in the 1955 paper; this mission asks for a machine-checked formulation and proof of that known result. The statements compile as open Lean theorems, so compilation alone does not establish their truth. Closing them would add a reusable treatment of absolute-deviation objectives under finite linear inequalities and an exact certificate for the paper's worked example. The consistency claim in the appendix is a separate mission because it concerns perturbations of another linear program, not this transformation.
The split-variable program permits and to be simultaneously positive even when their difference is fixed. Consequently, simply identifying the two feasible sets would misstate the transformation: one has extra degrees of freedom. A proof must relate their objective values and then account for optimal solutions on both sides. The numerical example has a separate difficulty. Substituting the reported weights verifies a feasible objective of , but does not by itself rule out another feasible weight vector with a smaller deviation. The global lower bound is part of the companion theorem.
The Lean development represents factor and level vectors by functions on Fin n and Fin L, and sums explicitly over finite indices. Paper level 1 is Lean index 0; paper level is the final Fin L index. The assumption is explicit because both the top and bottom level are named. No sign, monotonicity, or boundedness assumptions are imposed on the ratings beyond what the paper states. The weights are componentwise nonnegative. Intermediate target salaries enter the objectives through but add no constraints to (2), matching the paper's treatment of .
A minimizer is a feasible point whose objective is no larger than that of every feasible point. The equality of minimal values uses the threshold formula above, so an empty feasible set cannot inherit a spurious real infimum. The transformed feasible set is exactly the split-variable system of (4)–(5); defining it as only the image of a chosen lift would make the principal comparison empty of content. The Table I constants are exact rational values in units of . The paper rounds some displayed salaries, while Lean records their exact fractions. The generic column-independence companion is stated for an arbitrary finite matrix, with the basis and zero nonbasic coordinates explicit.
The shared definition module provides the salary map, feasibility predicates, objectives, minimizers, and example data. A full development can contribute proofs of the three milestones, the main equivalence, the column claim, the numerical lower bound, and the redundant-row fact. The finite absolute-deviation and split-variable statements can also serve later formalizations with other linear constraints.
Minimum makespan scheduling on unrelated parallel machines asks for an assignment of jobs to machines, where job takes time units on machine , so that the largest machine load is as small as possible. In the three-field notation of Graham, Lawler, Lenstra and Rinnooy Kan (1979) it is . It models load balancing across heterogeneous processors, workers or production lines, and it is a standard test case for linear-programming rounding.
Lenstra, Shmoys and Tardos (FOCS 1987; CWI Report OS-R8714; Mathematical Programming 46, 1990) gave a polynomial 2-approximation algorithm for and showed that no polynomial algorithm achieves a ratio below unless P = NP. They also asked which restrictions on the processing times keep the problem hard. Their Section 5 answers this when only two distinct processing times occur:
Theorem 7 is the paper's last result and closes this classification. Its proof generalizes the reduction of Theorem 4, which handles the case , from 3-dimensional matching to -dimensional matching.
Machines are indexed by and jobs by . A schedule assigns every job to exactly one machine. The load of machine is , and the makespan is the largest load.
-dimensional matching. An instance is a ground set of elements and a family of -element subsets of . A matching is a subfamily with and ; its members are then pairwise disjoint.
The instance of Theorem 7. Fix natural numbers that are relatively prime. Build a scheduling instance with machines, machine corresponding to , and two kinds of jobs:
Every processing time lies in .
The instance of Theorem 4. For disjoint sets , , of the same size and triples , , there are element jobs, one per element of , and dummy jobs. Machine processes the element jobs of , , in one time unit and every other job in three time units. A 3-dimensional matching is a subfamily of triples covering .
For relatively prime and a family of -subsets of a -element set, the instance above has all processing times in , and
The result. Theorems 6 and 7 together say exactly which two-valued restrictions of are tractable. Up to scaling, the polynomial case is , and every other pair with is NP-hard. Theorem 4 is the base case. It also yields Corollary 1 of the paper: no polynomial -approximation with exists unless P = NP. Reductions of this "no idle time" kind are a standard template for hardness of restricted-assignment and two-value scheduling, a line still active in the study of the restricted assignment problem and of the "graph balancing" special case.
Formalizing it. The result is proved, in two short paragraphs. The proof leaves to the reader the construction of the schedule from a matching and the "easy number theoretic argument" behind the converse, and both become explicit here. The development also produces reusable pieces: a -dimensional matching definition over an arbitrary family of -sets, and two reduction instances built on the published load and makespan of MatousekLP.Scheduling.Schedule. To our knowledge no machine-checked proof of these reductions exists.
The forward direction is a direct construction. The converse is where care is needed. A schedule with makespan at most may a priori place an element job on a machine whose tuple does not contain it, at length , and may mix element and dummy jobs on one machine. Looking at one machine at a time does not exclude either: a single machine can carry such a mixed load below . What excludes them is a property of the whole schedule together with the arithmetic of and . The hypotheses are sharp for this step: for element jobs are cheaper on foreign machines, and for a load with becomes possible.
Fin m. Schedules are maps from jobs to machines. Load and makespan are those of the published MatousekLP.Scheduling.Schedule, with natural-number processing times cast to . The jobs are enumerated as Fin (q * n + p * (m - n)) (Theorem 7) and Fin (3 * n + (m - n)) (Theorem 4), element jobs first, through finSumFinEquiv.Fin (q * n) and the family is indexed by machines, so repeated tuples are allowed. The -partite structure of -dimensional matching is not imposed: the reduction does not use it, and statements over all families of -sets contain the -partite case. Theorem 4 keeps the tripartite structure, with triples of indices in Fin n × Fin n × Fin n.MatousekLP.Scheduling.Schedule (it bounds every load; it is attained when ), which are reusable across scheduling reductions.A solution of a scenario optimization program is chosen after observing finitely many uncertain constraints. Its future reliability depends on constraints that were not sampled. The usual advance question asks how many samples are needed to make every output reliable. Campi and Garatti instead ask what can be certified after solving the program, when the number of sampled constraints that actually determined its solution is visible. Their wait-and-judge result uses that observed number to set a violation threshold. This mission concerns their extension from convex programs in finite-dimensional spaces to programs over an arbitrary decision set, with no convexity requirement.
The generic extension matters when a dimension bound on the number of influential constraints is unavailable. A decision may be a combinatorial object, a function, or an element of an infinite-dimensional space. The paper allows the support count to range from zero to the full sample size , and its threshold includes the case of support constraints. The paper's Section 6 gives the model and its two probability guarantees.
Let be a set of decisions. A subset is the domain; a real function is the cost. An uncertain outcome belongs to a measurable space with probability measure , and imposes a constraint set . For a sample of independent outcomes, the program minimizes over that belongs to every sampled . The sample law is . There is no algebraic or topological condition on the feasible sets or on .
A fixed finite sequence of real tie-break functions is minimized lexicographically after the original cost. This selects one solution whenever the program has a selected minimizer. Assumption 1 requires existence and uniqueness for every finite sample, including the empty one. A sampled constraint is a support constraint if removing it changes this selected solution. The number of support constraints is . Assumption 2 says that, with probability one, keeping only the support constraints gives the same selected solution. Both assumptions are part of the source's generic setting; they are substantive restrictions even though the sets and cost are otherwise arbitrary.
The violation of a decision is . Thus is the probability that a fresh constraint rejects the computed solution. Since the solution and support count depend on the sample, the wait-and-judge event uses a threshold function evaluated at the observed count, . For each , the paper also uses a generalized distribution function . It need not have total mass one.
For any and any -valued on , let be the infimum of feasible values over real polynomials of degree at most satisfying
The goal is the paper's Theorem 3:
The polynomial value retains the full dependence on the chosen threshold function. The source prints an extraneous in Theorem 3's range for ; its generic setting and variational problem use .
For , the paper's Theorem 4 defines as the unique root of
With for and , its conclusion is
The terminal value is essential because the paper gives examples with and .
Theorem 3 makes the observed support count a usable statistic for assessing the solution's future constraint violation without a dimension bound. Theorem 4 turns it into a certificate at any chosen confidence parameter . The confidence threshold depends on the count seen after the program is solved. These statements do not claim that every generic program satisfies Assumptions 1–2; they say what follows for programs that do.
A formal development must make the statistical objects and the analytic value agree exactly: the solution must come from the feasible set and the fixed tie-break rule, the support count must record changes of solution, and must be the value of the derivative-constrained polynomial problem. The reusable outputs include the generic scenario model, its generalized violation distributions, and the finite moment and dual formulations. The statements are known results of Campi and Garatti; this mission asks for machine-checked proofs of those results and their selected intermediate claims.
The observed support count is data-dependent. Conditioning on therefore cannot be treated as conditioning on a fixed subset of sample coordinates. Symmetry across possible support subsets must agree with the selected solution under removal of nonsupport constraints. Assumption 2 is what rules out a degenerate change of solution when only support constraints remain. In the generic setting the possible count grows with , so the distributional characterization has one measure for every and moment equations for every sample size. The resulting infinite family must still be related to the finite degree- polynomial value in (31). No convexity or finite-dimensional geometry is available to supply a fixed support bound.
Lean represents the decision set by an arbitrary type , with a measurable structure only to state the paper's implicit measurability convention. Samples are functions Fin N → Δ with zero-based indices and product law Measure.pi. The published generic violation definition is reused. The domain, constraint family, cost, finite lexicographic tie-break, selected solution, support set, and are defined locally. A Nonempty S instance provides an unused fallback value to the total solution selector; Assumption 1 already implies that is nonempty.
The source takes measurability for granted in a footnote. Here the constraint relation is jointly measurable, every solution map is measurable, and each support event is measurable. These pins assign probabilities to the events the paper uses. The are finite measures on , so the paper's Stieltjes integrals are represented as integrals over or against those measures. The polynomial class means degree at most , matching the coefficients in (36). The value is a real infimum; a separate sanity proof gives a feasible polynomial and a zero lower bound on all feasible values.
The goal retains Assumptions 1–2 and states the actual tail bound. It does not assume the moment equations or a favorable value of , and no support count is fixed in advance. Contributions toward the distributional decomposition, the moment equations, the finite weak-duality inequality, the polynomial identity, and the explicit-root theorem are within scope.
A manufacturer launching a new product often depends on a single supplier for a critical component, and the supplier must build capacity before demand is known. The manufacturer usually knows more about demand than the supplier does: her sales force, market research and order history give her a forecast the supplier cannot verify, and she has a reason to inflate it, since more capacity costs her nothing if the supplier pays for it. Whether contracts can make forecast sharing credible, and at what cost to the supply chain, is the subject of Cachon and Lariviere, "Contracting to assure supply: how to share demand forecasts in a supply chain" (Management Science 47(5), 2001, doi:10.1287/mnsc.47.5.629.10486). Section 6.10 of G. P. Cachon's survey chapter Supply Chain Coordination with Contracts (Handbooks in OR & MS, Vol. 11, 2003) presents a simplified version of that model, and this mission formalizes it from the author's January 2003 draft.
The section separates two regimes. Under forced compliance the supplier must build exactly the capacity the contract specifies; under voluntary compliance he may build less. The section's conclusion is that forced compliance allows both coordination and credible forecast sharing, while voluntary compliance allows forecast sharing only at the price of under-investment in capacity.
Demand has one of two types with distribution function . The page assumes for , for (so demand has an atom at ), increasing and differentiable, and stochastic dominance for all . The supplier builds capacity at cost per unit; after demand is observed he produces at cost per unit; the manufacturer earns per unit of demand satisfied; unused capacity is worth nothing.
Expected sales with units of capacity are , and the supply chain's expected profit is
An optimal capacity maximizes over , and .
In an options contract buys options at each and pays for each option exercised. With her profit is and the supplier's is . The contract with share sets and . Under a wholesale price contract with price the supplier earns ; the price inducing capacity is with , and the manufacturer then earns .
With asymmetric information only observes . Let be the supplier's minimum acceptable profit, and define the shares
The low type offers the options contract with share and initial order , the high type the one with share and initial order . Assuming and :
the supplier earns from the low type and at least from the high type, and each initial order maximizes both firms' profits. The profit comparisons are stated between the contract profit functions, not between shares.
The goal shows that with forced compliance a high-demand manufacturer can share her forecast credibly through the terms of a coordinating contract rather than its form: both types use the same contract family, the supply chain is coordinated in every state, and the only cost of asymmetric information is that the high type may be unable to push the supplier down to his reservation profit. The voluntary-compliance milestones show the other side: once the supplier may under-build, only the wholesale price affects his capacity, and the resulting capacity is strictly below the integrated optimum. Together they explain why compliance regimes matter in capacity contracting.
The results are established on the page with short arguments; none has a machine-checked proof. Formalizing them requires the derivative of expected sales for a distribution with an atom, the first-order characterization of a concave maximizer on a half-line, and careful bookkeeping of the incentive constraints. The demand and profit definitions are reusable for other capacity-procurement and newsvendor-type models.
The incentive constraints look like arithmetic on shares, but the strict inequality needs : the low type's chain profit at the high type's capacity must be strictly below its optimum. The obvious argument via uniqueness of the maximizer is not available, because the page does not assume strictly increasing, so need not be strictly concave and may have a whole interval of maximizers. Likewise needs a strict comparison of integrals of distribution functions. In the voluntary-compliance part, the derivative of needs the density at , and fails when that density is .
Each demand law is a probability measure on and is Mathlib's cdf. is required to be differentiable only on , because the page's makes it jump at . is defined by the expectation , whose integrand is integrable because almost surely. Optimal capacities are passed as arguments characterized as maximizers over , never chosen; is footnote 46's assumption. Derivatives are HasDerivAt statements.
Hypotheses added relative to the page, all disclosed in the items: and in the goal (the page divides by and needs ); for the voluntary-compliance derivative (at it vanishes); and for the non-coordination result. The page's assumption is not needed and not imposed; its strict-concavity claim on p. 101 is not stated, because it would need strictly increasing. The prior does not enter any statement. The page's "separating equilibrium" is formalized by its defining incentive and participation conditions, not by a general signalling-game solution concept; a predicate that holds by construction of (for example ) is not an acceptable substitute for the profit inequalities. The fixed-fee condition of p. 105 is pure algebra on four numbers and is not included.
All definitions are local to the namespace CachonCoord.CapacityForecast. No platform theorem formalizes this model; the Snyder–Shen newsvendor definitions (SupplyChainTheory_contracts) and the revenue-sharing model of Cachon–Lariviere 2005 (RevShareCoord.*) concern different games and are not reused. Proofs of any milestone, and a sanity instance showing the model's hypotheses are satisfiable (for example demand with an atom at and an exponential tail, ), are welcome.
In most contracts of the supply chain coordination literature the transfer payments are fixed when the contract is signed: a wholesale price , a buy-back rate , a revenue share . Some settings need payments that respond to information arriving after signing, such as realized demand at several retailers and realized production output. Fixing the per-unit price in advance then fails twice: for some output realizations the retailers do not buy everything that was produced, and for others they want more than exists, so the supplier must ration, which invites strategic ordering and misallocation (Cachon and Lariviere, 1999).
Section 6.9 of Cachon's survey chapter Supply Chain Coordination with Contracts (Handbooks in OR & MS, vol. 11, 2003) studies an alternative after Kouvelis and Lariviere (2000): the supplier commits to hold an internal market for output after demand is observed, and pays her own production manager a fixed amount per unit of realized output. The model is a variant of Porteus and Whang (1991), who studied incentives between manufacturing and marketing managers in a firm. The section shows that this pair of mechanisms coordinates both the production decision and the allocation decision without the supplier observing either the demand shocks or the manager's effort.
This mission is part IX of a series formalizing the capstone results of that chapter.
One supplier employs a production manager and sells to two independent retailers. The constant demand elasticity is .
If retailer one receives the share of , total retailer revenue is
The optimal share is (Eq. (44)), and is revenue under it. The expected supply chain profit is , and the optimal effort solves the first-order condition (45).
In the decentralized system, if the per-unit price is , retailer 's profit is . The contingent price is
The manager is paid a fixed amount per unit of realized output. With , the payment is
and his expected utility is .
The goal has two parts.
The result shows that one mechanism handles two separate information problems. The market price is the shadow price of output. Charging it makes the retailers' independent orders add up to exactly the output and split it as the integrated firm would, and the supplier never needs to observe . Paying the manager the output-weighted expectation of that shadow price, a single number fixed in advance, aligns his marginal incentive with the supply chain's, and the supplier does not need to observe . The supplier breaks even on the market. Kouvelis and Lariviere (2000) show that in more general settings she breaks even or loses money, so any profit must come from fixed fees. The section therefore illustrates a general design principle: market-based transfer prices inside a firm, combined with linear output-based pay.
The derivations are short calculus on the page. Formalizing them pins down what the page leaves implicit: the range of efforts and allocations; the role of and of the integrability of the shock; the fact that each retailer's problem has a unique interior optimum only at a positive price; and how the realized output enters the expectation . To our knowledge none of these statements has been machine-checked before.
The deterministic part requires real-power calculus with a non-integer exponent . Strict concavity of has to be used on the closed interval , where the derivative blows up at the endpoints. The retailer's optimum has to be shown to be interior even though the profit at is defined.
The stochastic part requires pulling the effort out of the expectation, , pointwise in the shock, including at realizations with . The natural first idea, to differentiate under the expectation sign, is unnecessary but tempting. The obstacle it hides is that is undefined where , so the identity (46) only holds once is read as its limit at . Uniqueness of the manager's optimum depends on strict convexity of alone, since his payment is linear in .
All objects live in the namespace CachonCoord.InternalMarket. The deterministic file Revenue defines , (as the printed formula, not as an argmax), , and with real powers (Real.rpow). The file Model bundles a probability space with measurable and , the elasticity , and the cost . The cost is strictly convex and increasing on and has derivative at every . On top of these, Model defines , , the payment (46) (by its printed left side, not as the ratio it is claimed to equal), expected output and market revenue, and the manager's utility (from the payment scheme, not by the printed formula). Derivatives are HasDerivAt statements and optima are IsMaxOn over or .
The standing assumptions are those of the model paragraph on p. 92: risk neutrality and the distributional assumptions above. Added hypotheses, each disclosed in the item's Formalization Note:
The existence of an effort satisfying (45) is a hypothesis, as on the page. Clauses 1 of the goal are stated for fixed realizations, not as random variables.
A trivializing formalization would define as an argmax, or define the payment (46) as ; neither is done here. Outside and , Lean's real power returns junk values, and every statement restricts to that range. The companion claim that is the unique market-clearing price is not posed.
The formalization needs no infrastructure beyond Mathlib's real powers, convexity and Bochner integral. The concavity and first-order-condition lemmas for with may be reused for other constant-elasticity models. Contributions are welcome at any milestone; each is independent of the others except through the closed forms.
In a supply chain with stock at two locations, a supplier holds inventory that replenishes a retailer, and the retailer serves customers. Each firm sets its own inventory level to minimize its own cost. The retailer bears only part of the cost of customer backorders, and the supplier bears none of the retailer's holding cost, so their incentives differ. The resulting equilibrium generally differs from the policy that minimizes total cost. Cachon and Zipkin (Management Science 45(7), 1999) studied this game and proposed linear transfer payments that align the firms' incentives. In the chapter Supply Chain Coordination with Contracts (Handbooks in OR & MS, vol. 11, 2003, doi:10.1016/S0927-0507(03)11006-7), Cachon re-derives that analysis, adds a parameter that divides the retail-level costs between the firms, and answers two questions the original paper left open: whether the contracts allow an arbitrary division of cost, and whether the optimal policy is the unique equilibrium under the contracts. This mission formalizes the second answer, together with the analysis of the decentralized game and of the optimal policy that it rests on (§6.8 of the 2003 chapter, read in the author's January 2003 draft).
Two firms, a retailer and a supplier , each use a base stock policy: firm keeps its inventory position equal to its base stock level . A negative supplier base stock means planned backorders. Let and be the demands during the retailer's and the supplier's lead times. They are nonnegative with finite means , , and their distribution functions , are continuous, zero at , strictly increasing on and differentiable on . Holding costs are and , with . Each backorder at the retailer costs the retailer and the supplier per unit time. Write .
At retailer inventory level the expected on-hand stock is and the expected backorders are . The retail-level cost rates are , and . Because the supplier may stock out, the retailer's actual inventory level is , and every retail-level quantity is averaged accordingly:
With the supplier's inventory and backorders , the firms' costs and the chain's cost are
A pair minimizing is an optimal policy. A Nash equilibrium is a pair from which neither firm can lower its own cost by a unilateral change of its base stock.
Under a linear transfer the supplier pays the retailer (a negative amount is a payment the other way). The Cachon–Zipkin contracts with parameter are
If is optimal with and , then under the contracts
is a Nash equilibrium, and it is the only one. The goal contains no numerical constants. It holds for every demand distribution in the class and every in the range.
The goal says that a contract built from quantities both firms can measure, namely the retailer's inventory and backorders and the supplier's backorders, makes the system-optimal policy the only equilibrium. The firms therefore reach the optimum without coordinating on an equilibrium. The parameter splits the retail-level costs between the firms in any proportion up to . Milestone 2 shows the contract is needed: without transfers, decentralization is always strictly suboptimal when the supplier is charged for retail backorders. The transfers and are those of the single-location model (§6.7), even though the retailer's target fractile changes from to .
The results are proved in the source and in Cachon and Zipkin (1999), with informal derivative arguments. No machine-checked version is known. Formalizing them requires differentiating expectations of piecewise-linear convex functions of a random lead-time shortfall. The page's argument also assumes densities, which the formal statements avoid, and contains several printing slips (see below). These would be settled by a complete development.
The firms' costs are compositions: a convex single-location cost evaluated at the random level , which is concave in . The supplier's cost is therefore not obviously convex in ; its convexity at depends on the value of and on . Uniqueness is the hard part. Under the contracts the retailer's best response decreases, but the supplier's marginal cost along that best response, , is not monotone in general when is small, contrary to a literal reading of p. 84. A uniqueness argument has to show that it has at most one zero, not that it increases.
Demand laws are probability measures on with no mass below , finite means, and continuous distribution functions, zero at , strictly increasing on and differentiable on . These are the section's standing assumptions, together with and (footnote 34 excludes the zero cases). Expectations are Lebesgue integrals: , , and the two-location averages are defined by expectation, and the page's integral forms are consequences. Integrals against are written against the law of , so no density hypothesis is made. Base stocks range over all of , and "optimal" means minimizing over ; the existence of an optimum is a hypothesis, as on p. 77. Derivatives are stated with HasDerivAt. Independence of and , implicit on the page, enters only through the convolution of their laws in (38).
The contracted costs are defined from the firms' original costs and the transfer payment. Defining them by the closed forms (42)–(43) would make the identities trivial and is ruled out.
Corrected slips: (42) is stated with where the page prints (the difference does not depend on ). The retailer's single-location fractile on p. 79 is stated as , not the printed . The garbled display after (43) and the / slip in the best-response derivative are not reproduced. Not included: the contraction condition (34), the case split for the optimal policy (p. 84), the case , and the alternative schemes of §6.8.5 (Lee–Whang, Chen). Contributions of those, or of a reusable library for derivatives of , are welcome. The platform's Clark–Scarf items (InventoryControl_clarkScarf, ClarkScarf.Serial.*) concern periodic-review echelon policies and are not reused.
In 1983 H. W. Lenstra, Jr. proved that integer linear programming with a fixed number of variables is solvable in polynomial time (Lenstra 1983). The algorithm became one of the founding results of algorithmic geometry of numbers: it introduced the strategy of making a convex body "round" by a linear change of coordinates, and then either finding a lattice point in it or showing that the body is covered by few parallel lattice hyperplanes, which reduces the dimension by one.
The algorithm rests on two geometric facts, each with its own proof. The first (§1 of the paper, the companion mission Integer Programming with a Fixed Number of Variables 1) says that a round body that misses the lattice meets few lattice hyperplanes. This mission is the second (§2): an explicit construction of the rounding transformation. Starting from a simplex inside the polytope, the algorithm repeatedly swaps a vertex for a point of the polytope as long as this increases the simplex's volume by more than a factor . When no such swap exists, a linear map that makes the simplex regular also makes the polytope round, with an explicit roundness ratio .
Short timeline. Khachiyan's ellipsoid method (1979) made linear programming polynomial and supplied the subroutine that Lenstra uses to maximize linear functions on . Lenstra's algorithm (preprint 1981, published 1983) combined it with the lattice basis reduction of Lenstra, Lenstra and Lovász (1982). Remark (c) of the paper notes that rounding with a maximal-volume inscribed ellipsoid achieves the better ratio , but not by a polynomial algorithm for varying ; later work (Kannan 1987, Grötschel–Lovász–Schrijver 1988) refined the rounding step with ellipsoid methods.
Work in with the Euclidean length , and write for the closed ball. For points , the simplex volume is
where has column vectors .
Let be convex, and let with linearly independent. Choose linear functions with
Thus measures the height above the facet opposite . The stopping condition of the second stage is
The ratio is the factor by which the volume changes when is replaced by , so (16) says that no such swap enlarges the simplex by more than .
Let be a nonsingular linear map of such that span a regular simplex, meaning that all distances , , are equal. Let be its centroid and its convex hull. For , the paper defines
The proof of the LEMMA works in model coordinates. There is the hyperplane of , the are the standard basis vectors, , and .
Under (15) and (16), with making the simplex regular and its centroid, there are positive reals with
These are conditions (3)–(4) of §1 with .
The paper's own proof derives the goal from milestone 1 and the LEMMA at . At the constant cannot be improved by this argument.
The result. The theorem is the only place in the paper where the roundness constant is computed, and enters the bound on the number of lattice hyperplanes that the algorithm branches over. Remark (c) of the paper uses the exact LEMMA for other values of to obtain ( even) and ( odd). The LEMMA itself is a self-contained fact about the regular simplex. In Euclidean geometry it says how far the "volume- neighbourhood" of a regular simplex extends.
The formalization. The result is classical and proved in the paper. Nothing in it has been machine-checked: there is no regular simplex in Mathlib, and no formal result relates simplex volumes to barycentric coordinates in this form. The platform has the related ellipsoid rounding ConvexOptimization.lowner_john_polytope_rounding (the John-ellipsoid version with factor , by Shuze Chen) and its definition ConvexOptimization_IsLownerJohn. That is the alternative construction of Remark (c). It has a different constant and is not used here. This mission and its companion together give a formal account of the geometry behind Lenstra's algorithm. The algorithm itself is not formalized: its running time needs a machine model and an encoding that the paper does not fix.
There are two separate difficulties. The first is the translation in milestone 1. It needs the volume of a simplex with one vertex replaced to be identified with a barycentric coordinate, through a determinant identity, and it needs this identification to survive the linear map . The second is the transfer to the model. The paper's "similarity transformation" identifies with a hyperplane of and sends the regular simplex to the standard one. In Lean the vertex description (milestone 2), the radii (milestones 3–4) and must all be carried across this isometry up to scaling. The LEMMA is stated in , not in the model. The "straightforward analysis" behind milestone 2 is a vertex enumeration of a cube cut by a hyperplane, and its parity split is where sign errors appear.
EuclideanSpace ℝ (Fin n) and the model is EuclideanSpace ℝ (Fin (n+1)). Distances are Euclidean, never the sup norm. Vertices are indexed by Fin (n+1), matching .A supplier that sells through many competing retailers usually worries that competition among them pushes orders too high, because each retailer ignores the demand it takes from the others. Deneckere, Marvel and Peck (1997) identified the opposite failure. When the retail price is set by the market after demand is realized, retailers who hold too much stock in a weak market bid the price down, and anticipating this, perfectly competitive retailers order too little. The supplier then needs a contract that raises orders, and the classical justification for resale price maintenance (a price floor imposed on retailers) comes out of this model. G. P. Cachon's survey chapter Supply Chain Coordination with Contracts (Handbooks in OR & MS, Vol. 11, 2003) presents the model in §6.5.2 as a closed-form example. In it the supplier's best wholesale price contract is computed explicitly and compared with two contracts that recover the monopoly profit: resale price maintenance and a full-refund buy-back.
This mission is volume V of a series that formalizes the section capstones of that chapter, read in the author's 3rd draft (January 2003), pp. 53–58.
Fix . Industry demand is low or high, each with probability . If the retailers hold a total stock , the market clearing price is
Leftover inventory has no salvage value, and the supplier's production cost is zero.
Perfect competition means the retailers keep ordering until expected profit is zero. The competitive order is the with and on . The supplier earns .
The page's notation , , and is kept in Lean under the names q1, q2, supplierProfit, wStar.
With
the goal states four things:
The goal shows that in this model a wholesale price contract always falls short of the integrated profit, whatever . It also shows where the shortfall comes from: at the optimal wholesale price the low-state market price falls below the monopoly price (milestone 4). Restoring the monopoly profit therefore requires a mechanism that holds the low-state price at . Resale price maintenance and a full-refund buy-back both do this, so the section gives a closed-form efficiency argument for vertical restraints that are often treated as anticompetitive. The section also contrasts the buy-back with revenue sharing, which coordinates the single newsvendor (§6.2) but not this model.
The results are proved on the printed pages by elementary algebra. None of them has a machine-checked proof, and nothing on Prove2Me covers this model. The mission produces checked versions of the case analysis, including the tie and the two regimes of the competitive order. It also adds a reusable encoding of "perfect competition" as the first zero of aggregate expected profit.
Every statement reduces to one-variable inequalities, but the case structure is easy to get wrong.
All quantities are real numbers and throughout. The continuum of retailers enters only through the total order. No measure space of retailers is formalized, and footnote 26's multiplicity of individual equilibria is not stated. The sales rules under resale price maintenance (proportional allocation) and under the buy-back (price floor ) are written into the contract definitions, as the page describes them in words. The theorems use only .
The formulas , , and are definitions transcribed from the page. That they are the competitive order and the optimum is the content of the theorems. Defining or the competitive order by its closed form would trivialize the mission, so the competitive order is defined only by the zero-profit property and as a greatest element of the monopolist's feasible profits. The goal is stated over all real wholesale prices, so it also rules out profitable prices outside . Uniqueness of is not asserted at .
The chapter's standing assumptions used here are risk neutrality and full information, together with the model paragraph of pp. 53–54 (two equally likely states, zero salvage value, zero production cost). No platform definition is referenced: no published item formalizes this model.
A supplier selling through a retailer earns more when the retailer works harder at selling. Examples are a better shelf position, more knowledgeable sales staff, local advertising and keeping the display in order. These activities cost the retailer, raise demand, and usually cannot be observed or verified by the supplier, so no contract can be written on them directly. Chapter 6 of the Handbook of Operations Research and Management Science, Vol. 11: Supply Chain Management (G. P. Cachon, Supply Chain Coordination with Contracts, 2003) surveys contracts that align a retailer's decisions with the interest of the whole supply chain. Its §6.4 asks which of these contracts survive when the retailer also chooses such an unverifiable effort level.
The question goes back to the marketing literature on retail effort (Chu and Desai 1995, Desai and Srinivasan 1995, Desiraju and Moorthy 1997, Lal 1990, Lariviere and Padmanabhan 1997). It was taken up for newsvendor contracts by Taylor (2000), who showed that a sales rebate combined with a buy back restores coordination, and by Krishnan, Kapuscinski and Butz (2001), who let effort be chosen after demand is observed. This mission is the third in a series that formalizes the chapter's section capstones. It covers §6.4.1.
One supplier sells to one retailer for a single selling season. Before the season the retailer chooses an order quantity and an effort level . Effort costs him , where , and . Demand given effort has distribution function on , with and strictly increasing. Demand is stochastically increasing in effort: for . Units sell at the retail price and cost to produce. Goodwill costs, the salvage value and the retailer's own unit cost are zero. Expected sales and the integrated channel's profit are
Let maximize . A contract fixes the transfer the retailer pays the supplier, as a function of what the supplier can verify: the order and, for some contracts, sales or leftover units, but never effort. The contracts compared are the buy back , quantity flexibility , revenue sharing , the sales rebate and the quantity discount . Under each, the retailer's profit is his revenue less the transfer and .
The goal combines the section's negative and positive results.
the following hold for every . The retailer earns and the supplier earns . The retailer's marginal profit of effort equals the channel's. His optimal efforts are the channel's. 3. The optimal order. If maximizes , both firms' profits at effort are maximized by .
The milestones follow the section's own claims: the integral form of (p. 41); the first-order condition (18) for the chain-optimal effort; (19); the analogous strict inequalities for quantity flexibility () and revenue sharing (), and the reverse inequality for the sales rebate (, ); the two displays of under the quantity discount; and the fact that decreases in .
The result separates two jobs a contract does. To coordinate the order quantity, buy backs, quantity flexibility and revenue sharing all shield the retailer from part of the demand risk or take part of his revenue. The same shield dulls his incentive to raise demand, so each one leads him to under-invest in effort. The sales rebate pushes the other way, toward too much effort. The quantity discount works because the retailer keeps every unit of realized revenue and bears all of his own effort cost. The schedule then prices the order against expected revenue at the optimal effort, so the order is coordinated without touching the effort incentive. Because with free in , any split of the channel's optimal profit is attainable. The chapter extends this observation to retailers that also set price (p. 43).
The section's claims are proved on the page only in outline; several are introduced with "it can be shown". To our knowledge none has a machine-checked proof. Formalizing them requires differentiating expected sales in a parameter of the demand law. That step recurs throughout stochastic inventory and pricing models.
Most of the algebra is short. The substance is in the derivatives. is a differentiation under the integral sign. The strict inequalities need this integral to be strictly negative. That in turn needs to be integrable and negative on a set of positive length, which is why (and for the sales rebate) matters.
The natural reading "the quantity discount makes the retailer's joint optimum" is not what the page shows, and it fails in general. The page gives two partial statements: for each fixed the retailer's effort incentive is the chain's, and at his best order is . Since , the retailer can gain by moving and together when is small. The goal states exactly the two partial claims.
The Lean namespace is CachonCoord.EffortNewsvendor. A structure Model collects the data: and with ; a family of demand laws indexed by effort (probability measures on with finite mean, no atom at , strictly increasing distribution function); the effort derivative , negative for , ; and with and positive first and second derivatives for . is defined as an expectation, and its integral form is a milestone. Derivative claims are HasDerivAt statements at interior efforts . The inequalities assert that both derivatives exist.
The following hypotheses are standing assumptions or disclosed additions:
Revenue sharing and the sales rebate use §6.2's profit functions (pp. 21, 27) with this section's zeros, less .
The page prints the last term of as . With that sign the page's own displays and fail by . The formalization uses , under which both hold. is the explicit printed schedule with this correction. It is not defined as "a schedule with ", which would make the goal empty.
Not covered: the price-and-effort schedule at the bottom of p. 43, for which the page gives no argument. The cachon-2005 revenue-sharing effort results (RevShareCoord.Effort.*, deterministic revenue ) are a different model and are not referenced. Proofs of any milestone, and a reusable library for differentiating newsvendor expectations in a parameter, are welcome.
Strictly convex quadratic programs — minimize a positive definite quadratic subject to linear inequalities — are the subproblems solved at every iteration of successive quadratic programming (SQP) methods for nonlinear optimization, and they arise directly in least-squares estimation with constraints, portfolio selection and model predictive control. In SQP the unconstrained minimizer of the quadratic model is available at no cost, while a feasible point is not.
D. Goldfarb and A. Idnani (Math. Programming 27 (1983) 1–33) proposed a dual active-set method that exploits this asymmetry. It starts at the unconstrained minimizer, which is optimal for the problem with all constraints removed, and adds violated constraints one at a time while keeping the current point optimal for the subproblem defined by the current active set. No phase 1 is needed. The method, usually called the Goldfarb–Idnani algorithm, is the basis of widely used solvers (for example the quadprog package in R and QuadProg++), and the paper proves that it terminates finitely with a correct answer.
Earlier dual methods for quadratic programming include the modified-simplex methods of Lemke (Management Science 8 (1962) 442–453) and of Van de Panne and Whinston (1964), which the paper compares with its own in Section 7.
Fix , a vector , a symmetric positive definite matrix , an matrix with columns , and . The quadratic program (1.1) is
The gradient is . For , the subproblem keeps only the constraints indexed by ; is solved by . A set is linearly independent if the normals , , are.
For an independent , let be the matrix with columns , , and define
The multipliers are ; for a constraint with normal the infeasibility multipliers are ; a superscript denotes the same objects for .
An S-pair is an independent active set with for and optimal for . A V-triple has , independent, , for , and .
The dual algorithm starts from . In Step 1 it stops if is feasible; otherwise it picks any violated constraint . In Step 2 it moves along the primal direction and the dual direction with step , where is the largest step that keeps the multipliers nonnegative and makes constraint active. If both are infinite it reports infeasibility. A full step () adds and returns to Step 1. A partial step (), or a dual step (), drops a constraint attaining and repeats Step 2.
For every choice of the violated constraint and of the dropped constraint :
Theorem 3 is the correctness certificate of the Goldfarb–Idnani method: whatever rule an implementation uses to choose the entering and leaving constraints, it cannot cycle and its answer is right. In particular the infeasibility verdict is a proof that (1.1) has no feasible point, which matters in SQP where infeasible subproblems trigger a different branch of the outer method. The intermediate results (the operator identities, Lemma 1, Theorems 1–2) are the standard analysis of dual active-set methods for quadratic programming.
The result is proved in the paper; to our knowledge it has not been machine-checked. A formal development produces verified projector identities for and , a verified KKT characterization for equality-active subproblems, and a verified finite-termination proof for a nondeterministic algorithm with an explicit step relation. The platform already has a proved KKT sufficiency theorem for general convex programs (ConvexOptimization.kkt_sufficient_for_convex), stated over EuclideanSpace with general convex functions and gradient fields; it can serve as background for the sufficiency half of milestone 2, but it is not stated in this mission's matrix objects.
The obvious termination argument is that increases strictly at every iteration and there are finitely many active sets. It fails as stated: partial steps may leave unchanged (the dual steps of Step 2(c)(ii)), so is only nondecreasing between consecutive states. A termination proof therefore needs a measure that also decreases along steps that do not move . Any such argument relies on invariants (independence of , nonnegativity of the multipliers, along partial steps) that hold only on reachable states, and the operators and are meaningful only while those invariants hold. Correctness of the infeasibility verdict requires the dependent case (Theorem 2), not only Theorem 1.
Vectors are Fin n → ℝ, is Matrix (Fin n) (Fin n) ℝ with G.PosDef, is Matrix (Fin n) (Fin m) ℝ, and active sets are Finset (Fin m). Multiplier vectors are indexed by constraint index (Fin m → ℝ, zero off the active set), not by position in . Lean's matrix inverse returns for singular matrices, so every statement about and assumes and an independent active set (directly, or through an S-pair or V-triple).
The algorithm is the inductive relation Step on states step1 x A u, step2 x A p u⁺, stopOptimal x, stopInfeasible, with one transition per admissible choice of and . Infinite step lengths are separate transitions; a tie takes the full step, as the paper tests first. The running value of and the factorizations of Section 4 are not part of the state.
Explicit readings of the paper's words:
Step transitions from the Step-0 state, and every reachable state without a successor is a STOP whose verdict is correct (optimal for (1.1), or (1.1) infeasible);Property (2.10), printed , is false unless and is not formalized. Equality constraints (1.2), Section 4 (numerically stable implementation), Sections 5–6 (computations), Section 7 (comparisons) and the Appendix example are out of scope.
A trivializing formalization is ruled out: the goal quantifies over every run of the relation (not one selection rule, not "some run terminates"), the infeasibility verdict is about (1.1) itself, and the algorithm is a relation that always has a successor until a STOP, so correctness cannot hold because a run gets stuck.
Needed infrastructure: Schur-complement and projector identities for and ; first-order optimality for convex quadratics on affine subspaces with inequality multipliers; well-foundedness arguments for a nondeterministic relation. The operator identities and the KKT characterization are reusable for other active-set and SQP analyses. Contributions of proofs of any milestone, and of reusable lemmas about and , are welcome.
Minimum-cost circulation asks how to route flow around a directed network without accumulating flow at any vertex, while minimizing the total cost of the routed units. It is a basic network optimization problem: lower-bound and demand constraints in many flow models can be converted into circulation form. Goldberg and Tarjan's 1987 technical report develops a successive-approximation approach in which a local repair subroutine, refine, improves an approximately optimal circulation. The report was followed by a 1990 journal article; all theorem numbers and page citations in this mission refer to the 1987 report.
The mission isolates the generic form of refine, where an implementation may choose any applicable update at each step. Its question is whether every such choice sequence finishes after a controlled number of operations and returns a circulation with a stronger optimality certificate. The related Goldberg–Tarjan maximum-flow algorithm uses push and relabel operations with distance labels; here the labels are real-valued prices tied to arc costs. The authors' cycle-canceling work uses the same circulation network model and supplies published definitions reused in this development.
A circulation network has a finite vertex set and a symmetric set of directed arcs: whenever is an arc, so is . Let and , counting both orientations. Each arc has a real capacity and cost , with . A pseudoflow respects capacities and the paired-arc relation . Its excess is the sum of flow entering . A circulation is a pseudoflow with zero excess everywhere. The already published CycleCanceling.MinMean.Network supplies this network, its circulation predicate, and residual capacity . An arc is residual when this capacity is positive.
A price function changes an arc's reduced cost to . A pseudoflow is -optimal with respect to when every residual arc has reduced cost at least . A vertex is active when its excess is positive. An admissible arc is a residual arc of negative reduced cost. Refine takes an input circulation that is -optimal, saturates every arc whose reduced cost is negative, and then repeatedly applies an available update. A push sends flow from an active vertex along an admissible arc. A relabel raises the price of an active vertex with no outgoing admissible arc to the largest value permitted by -optimality. These rules are Figures 4 and 5, printed pages 18–19.
The supporting targets are the paper's progress and correctness results, its price bound, and the three operation counts. For any generic refine run from a -optimal circulation, Lemma 5.8 bounds each vertex's price increase by . Lemmas 5.9–5.11 bound the numbers of relabelings, saturating pushes, and nonsaturating pushes:
The goal combines the resulting bound on the number of updates with progress and correctness:
If the final state has an active vertex, another update exists. If no update applies, the final pseudoflow is a circulation and is -optimal with respect to its final prices. This is the explicit operation-count content behind the generic subroutine's analysis in Section 5. It does not claim a bound for a particular data structure or a complete minimum-cost algorithm.
The theorem gives an order-independent finite bound: the choice of which applicable push or relabel to perform cannot cause generic refine to run forever or stop with an active vertex. Its output is a circulation whose approximate-optimality tolerance has been halved. That output can serve as the next input in the successive-approximation framework. For integral costs, the report's Theorem 2.3 later turns a sufficiently small tolerance into exact minimum cost; that outer-loop result is outside this mission.
This mission specifies the generic cost-scaling state machine in Lean and poses its quantitative analysis as open formalization targets. The shared network and circulation definitions from the published Goldberg–Tarjan 1989 series are available, and a related generic maximum-flow theorem in the 1988 series has a machine-checked proof. Those results do not prove refine's price-based bounds. Contributions that establish the paper's progress, price, or counting statements for this state machine, and reusable facts about finite residual networks, advance the open goal.
A push respects a capacity, but it can create activity at another vertex; a relabel changes which arcs are admissible. Thus checking a single update does not bound an arbitrary sequence. The price bound also depends on the circulation and prices supplied at entry, not merely on the current pseudoflow being -optimal. Finally, a vertex with no admissible outgoing arc may appear to be stuck when the relabel minimum is over an empty set. Feasibility of the original circulation network is needed to establish that an active vertex still has a genuine next update. The operation bound requires accounting for the three update types across every possible choice sequence.
Vertices form a finite type, and capacities, costs, flows, and prices are real-valued functions. The network has symmetric ordered arcs and antisymmetric costs. There is no separate nonnegativity assumption on capacities; feasibility is supplied by the input circulation. The new is positive, so the entry circulation is -optimal before Figure 4 halves the error parameter. The run starts from the resulting saturated pseudoflow and records one applicable push or relabel per index . Counts classify those actual steps by the selected arc's residual capacity after a push. Termination is the negation of the paper's loop guard, not a definition that assumes zero excess.
The reduced-cost sign is , and relabel raises . This differs from the published 1989 epsilon-optimality definition, so only its network model is imported. The relabel relation requires an attained minimum over a nonempty set of outgoing residual arcs; it assigns no default value to an empty minimum. Loops may occur in the reused network model, but cost antisymmetry makes their reduced cost zero, so they cannot be push arcs. The explicit constants are the report's , , , and ; the goal sums the last three. The report's RAM-model running times are outside the formal statements. A definition that makes termination equivalent to conservation or assigns an arbitrary relabel price at an empty set would miss the target.
Many network design and production–distribution problems have economies of scale: shipping twice as much along an arc costs less than twice as much, because of fixed charges, set-up costs or volume discounts. Modelled as network flows, such problems ask for a flow of least cost when each arc cost is a concave function of the flow on the arc. Classical instances include the uncapacitated lot-sizing problem, the fixed-charge transportation problem, and the Steiner tree problem in graphs. Unlike linear costs, concave costs make the problem NP-hard in general, and the usual linear-programming arguments do not apply directly.
Erickson, Monma and Veinott (Math. Oper. Res. 12 (1987) 634–664) give the send-and-split method, a dynamic program that solves such problems in time exponential only in the number of demand nodes. Before the method can run, two questions must be settled: when does a minimum-cost flow exist at all, and can the arc costs be shifted so that they are nonnegative on flows? Theorem 1 of the paper answers both. This mission formalizes Theorem 1.
Timeline. Hirsch and Hoffman (1961) showed that a concave function bounded below on a polyhedron's extreme rays attains its minimum at a vertex; Rockafellar's Convex Analysis (1970, pp. 61, 343) gives the polyhedral form. Edmonds and Karp (1972) showed how to choose node potentials making linear arc costs nonnegative. Theorem 1 (1987) extends both to additive concave costs on uncapacitated networks.
A graph has nodes and a set of ordered pairs of distinct nodes, the arcs. A demand vector assigns a demand to each node (negative demands are supplies). A preflow is a nonnegative matrix carried by the arcs, and a flow for is a preflow with
inflow minus outflow equal to demand. A circulation is a flow for .
The flow cost is , where each is concave on and . A minimum-cost flow for is a flow whose cost is at most that of every flow for .
A preflow induces the subgraph of arcs with nonzero flow. An extreme flow is a flow whose induced subgraph is a forest (in the undirected sense; two antiparallel arcs form a cycle). A simple circuit is a directed cycle through at least two distinct nodes, with arc set ; a simple circulation is a circulation whose induced subgraph is a simple circuit. The slope at infinity is the limit of the right derivative of .
Two nodes are in the same strong component if chains (directed walks) join them both ways; a component is a sink if no chain leaves it. The augmented graph appends a node and an arc for exactly one node of each sink component. Its arc costs are on arcs inside strong components and arbitrary real numbers elsewhere; is the infimum of the costs of chains from to . For , the altered costs are .
The following are equivalent:
If moreover admits a flow and on arcs joining distinct strong components, where , they are equivalent to
and is real and satisfies .
The milestones are the statements the paper's proof rests on: the Hirsch–Hoffman extension (p. 638), , the bounds , the circuit-wise form of 4° ⇔ 5°, uniqueness of the extreme circulation, between strong components, and the two inequalities giving (all p. 639).
Theorem 1 decides existence of an optimum from the costs alone: conditions 4° and 5° do not mention the demand vector, so one test settles every demand pattern at once, and 3° guarantees the optimum may be sought among extreme (forest) flows, which is what the send-and-split recursion enumerates. Condition 6° is checkable by a shortest-chain computation, and 7° supplies node potentials that convert the instance into an equivalent one with nonnegative arc costs, the standing assumption of the paper's Theorem 2 and of its running-time analysis. For linear costs the theorem reduces to the familiar statement that a minimum-cost flow exists iff no simple circuit has negative cost.
The result is proved in the paper; it has not been machine-checked. The formalization adds a precise model of extreme flows over arcs (so that antiparallel arcs form a cycle), a treatment of slopes that may equal , and the Hirsch–Hoffman extension specialized to network polyhedra, which the paper cites rather than proves. Related platform items cover the linear, capacitated case: CycleCanceling.MinMean.minCost_iff_no_negative_cycle and CycleCanceling.MinMean.minCost_iff_exists_price (Goldberg–Tarjan), and LinearOptimization.positive_directed_cycle_of_circulation and LinearOptimization.network_basic_iff_tree on a different arc encoding.
The first idea, to argue as for linear costs by cancelling negative cycles, fails because concave costs are not additive along cycle decompositions: the cost of a flow is not the sum of the costs of its cycle and path components, and a circuit can be harmless at small flow and arbitrarily negative at large flow. Existence therefore depends on the asymptotic slopes , which may be , rather than on any finite cost evaluation. The implication from bounded rays to an attained minimum (Hirsch–Hoffman) requires identifying the vertices of the flow polyhedron with forest flows and its extreme rays with simple circulations. The potential step 6° ⇒ 7° needs a cost bound on arcs between strong components, where the concave cost is only controlled up to the total positive demand .
Nodes are Fin n; a graph is ArcGraph n, a Finset (Fin n × Fin n) of arcs without loops. Preflows are real matrices vanishing off the arcs; arc costs are functions , concave on Set.Ici 0 with value at (the paper's "without further mention" assumption, made a hypothesis). The augmented graph has nodes Option (Fin n), with none the node ; chain costs, and are EReal-valued.
The explicit readings of loose phrases are:
A formalization in which extreme flows are forests of a simple graph built from the support, in which chains are simple paths, or in which a chain of cost counts as a minimum would make 3°, 6° or the equivalence trivially or falsely true; all three are ruled out by the definitions. The running-time remarks, the computation paragraph and the linear-cost remark after the proof are not formalized. Contributions are welcome on the polyhedral side (vertices and extreme rays of ), on right derivatives of concave functions at infinity, and on walk costs with negative cycles; all are reusable beyond this mission.
A retailer or an airline chooses which products to offer, and customers choose among what is offered, or buy nothing. Choosing the offer set that maximizes expected revenue is the assortment problem, central to revenue management (Talluri and van Ryzin, 2004). It is NP-hard even for simple mixtures of logit models, so practice relies on heuristics. The most common one is the revenue-ordered assortments strategy: offer the products whose price is above a threshold, and pick the best threshold.
Berbeglia and Joret (arXiv:1606.01371) analyse this heuristic under every regular choice model, the broad class in which enlarging the offer set never raises the probability of choosing any given alternative, including not buying. They prove three approximation guarantees, then show that none of the three can be improved. This mission formalizes that last result, Theorem 3.4.
Timeline:
The products form a finite set . A system of choice probabilities gives, for every offer set and product , the probability that a customer buys . The no-purchase probability is . The model is regular if
Each product has a revenue . Offering earns , and .
Let be the distinct revenues, with , and . The heuristic earns
For an optimal let , , and the largest index with . Section 3 of the paper proves
For every and every there are a finite nonempty product set, a regular , revenues with exactly distinct values, and an optimal with , such that
So none of the bounds (A), (B), (C) stays true when multiplied by , for any number of distinct revenues.
The paper's witness has products with and . Product has revenue , and when and , and otherwise, for . The milestones follow the proof on pp. 10–11:
With Theorems 3.1–3.3, Theorem 3.4 closes the analysis: in terms of the parameters , and , revenue-ordered assortments are understood exactly under regular choice. It complements the hardness results of Aouad et al., which already show that no efficient strategy can do much better than (A) and (B) in general; Theorem 3.4 shows that the analysis of this particular heuristic is exact. The instance is also a concrete regular choice model in which the optimal offer set is far from every nested one.
On the formal side, the mission produces a reusable formal definition of regular discrete choice models, revenue-ordered assortments and the three bound quantities. These are shared, under other sub-namespaces, with the companion missions on Theorems 3.2 and 3.3. The result is proved in the paper. As far as is known it has not been machine-checked anywhere; the remaining work is formalizing the paper's proof, including the steps it leaves to the reader.
The proof is a construction, and the paper verifies most of it in a sentence each. The work lies in those sentences:
The naive witness, one instance per bound, does not help: the goal asks for one instance with exactly revenues on which all three bounds are nearly attained, for every .
C. The no-purchase option is not a product: is the derived quantity noPurchase P S. Offer sets are Finset C.IsRegular carries axioms (i)–(iv), with (i) and (iv) stated both for products and for the no-purchase option. Regularity at is essential: without it the guarantees fail.Finset.sup' over all subsets, including . is Finset.sup' over the threshold sets only, and needs Nonempty C.r, indexed by Fin k from : the Lean index is the paper's , and is a separate case. lives in WithBot (Fin k).𝓝[>] 0.Fin (k+1) × Fin (k+1). Its regularity is a theorem to prove, never a field assumed.Ruled out:
Contributions welcome: proofs of the milestones, especially (8), (9) and the optimality of , and general lemmas on sorted distinct values of a finite function.
A retailer that can display only some of its products must choose an assortment: the set of products offered to an arriving customer. Customers substitute: whether a given product is bought depends on what else is on the shelf. The assortment problem asks for the offer set that maximises expected revenue under a model of this substitution behaviour. It is a core problem of revenue management (Talluri and van Ryzin, Management Science 2004), and it is NP-hard already for a mixture of two multinomial logit models (Rusmevichientong, Shmoys, Tong and Topaloglu, POMS 2014).
The heuristic used most widely in practice is revenue-ordered assortments: sort the products by price and offer, for some threshold, every product priced at least that threshold. It is optimal under the multinomial logit model (Talluri and van Ryzin 2004) but not in general. Berbeglia and Joret (arXiv:1606.01371v3, 2019; Algorithmica 2020) give a tight analysis of its approximation ratio for every regular discrete choice model, a class that includes all random utility models. They prove three incomparable guarantees. This mission formalizes the third, Theorem 3.3, whose ratio depends on the purchase behaviour of an optimal assortment rather than on the prices. Companion missions in this series cover the price-ratio bound (Theorem 3.2) and the tightness of all three bounds (Theorem 3.4).
Let be a finite nonempty set of products. A system of choice probabilities gives, for every offer set and product , the probability that a customer offered buys . Buying nothing is the option , with . The model is regular when
Axiom 4 at says that enlarging the offer set never makes buying nothing more likely.
Prices are a function . Offering earns , and . Let be the distinct values of , and let for . The revenue-ordered strategy earns
For an assortment , the purchase profile is
the probability that a customer offered buys something priced at least . It is non-increasing in .
Let be optimal, , suppose , and let be maximum with . Then
The first inequality is the paper's sum-form factor, the bound that Theorem 3.4 shows to be tight. The second is the closed form .
Theorem 3.3 gives a guarantee that is independent of prices. The bound of Theorem 3.2 grows when prices are spread out. The bound is small whenever an optimal assortment sells its expensive products with probability comparable to its overall purchase probability. In §4 the paper combines it with a reduction from unit-demand pricing to derive, for example, the guarantee of uniform pricing for the unit-demand min-pricing problem (Corollary 4.8, originally due to Aggarwal et al.). Together with Theorems 3.1 and 3.2, it describes the performance of the most common assortment heuristic over the whole class of regular models, with no parametric assumption on customer behaviour.
The theorem is proved on paper. To our knowledge it has no machine-checked proof, and no regular choice model has been formalized on the platform. This mission produces the regular model as a reusable definition, a statement of Theorem 3.3 in which every hypothesis is explicit, and formal versions of the proof's identities and inequalities. The logarithmic step is asserted without proof in the source, so a formal proof of it completes the paper's argument.
Each step is elementary. The difficulty is bookkeeping. The revenue of has to be regrouped by distinct price levels rather than by products: several products may share a price, and counts values. The regrouping uses an Abel-type rearrangement with the boundary convention . Comparing with the purchase probability of needs regularity twice. First, axiom 4 for products passes from to . Then the no-purchase case passes from to . A proof that uses axiom 4 only for products fails at the second step, and the claim is false without it.
C with [Fintype C] [DecidableEq C]. The goal adds [Nonempty C], the paper's . Offer sets are Finset C, and is P : C → Finset C → ℝ. The no-purchase option is not a product: is the derived quantity noPurchase P S. IsRegular P carries axioms 1–4, including both no-purchase cases.Finset.sup' over all subsets. is Finset.sup' over the indices of the threshold sets only.level r i is for . purchaseProfile P r S i is for and otherwise, which builds in .Real.log, applied to .The following statements are trivial or false and are not this mission: a maximum over all subsets in place of ; regularity without its no-purchase case; a purchase profile taken from a non-optimal set while is still called the optimum; the logarithmic form alone; a specific choice model (MNL, Markov chain) in place of an arbitrary regular .
A complete development needs finite sums regrouped by the values of a function and an elementary logarithm inequality. The regular choice model and the revenue-ordered sets are shared with the other missions of this series and are reusable for any analysis of assortment heuristics. Proofs of any milestone are welcome. So are alternative arguments for the logarithmic step and a proof that is non-increasing.
Policy gradient methods optimize a parameterized policy of a Markov decision process by gradient ascent on its expected discounted return. They underlie much of modern reinforcement learning (REINFORCE, actor–critic methods, TRPO, PPO), yet the objective is non-concave in the parameters, and until recently even the most basic question was open: does exact gradient ascent, run on a finite MDP with the standard softmax parameterization, reach the optimal values at all?
Agarwal, Kakade, Lee and Mahajan (arXiv:1908.00261v5, JMLR 22(98), 2021) answer this in the affirmative. Their Theorem 5.1 shows that unregularized softmax policy gradient with a small constant step size converges to the optimal value at every state, provided the start distribution used for the gradient puts positive mass on every state. The result is asymptotic: no rate is given. Later work (Mei, Xiao, Szepesvári and Schuurmans, ICML 2020, arXiv:2005.06392) obtained an rate with constants that can be exponentially large, and the same paper by Agarwal et al. gives polynomial rates once a log-barrier regularizer is added (its Corollary 5.1) or once the natural gradient is used (its Theorem 5.3). Theorem 5.1 is the unregularized baseline for all of these.
A finite MDP consists of finite sets of states and of actions ( nonempty), a transition kernel , rewards and a discount factor . A policy assigns to each state a probability vector on . Its value is the expected discounted sum of rewards when actions are drawn from ; its state–action value is and its advantage is . For a distribution on states, , and the discounted state visitation distribution is . A policy is optimal if for every policy and every state ; .
The softmax policy with parameters is
Softmax policy gradient ascent with step size produces, from an arbitrary , the iterates
The Lean development names these softmaxPolicy, softmaxValue P r γ µ θ , and IsSoftmaxPGRun P r γ µ η θ for the update rule; PolicyValue, QFunction and IsOptimalPolicy are the published FoundationsML definitions, and valueAt, advantage and visitation are the series' shared layer.
If for every state and , then for every state
The goal states only convergence to the optimal values, with the paper's constants in the step-size bound; no rate is claimed.
The theorem establishes that the non-concavity of the softmax objective does not trap exact gradient ascent: from any initialization, the values of the iterates converge to at every state, not only on average under . It is the reference point for the rate results of the same paper (log-barrier regularization, natural policy gradient) and for the subsequent literature on softmax policy gradient rates and lower bounds. It also isolates the role of exploration in the start distribution: Remark 5.1 of the paper leaves open whether can be dropped.
The result is proved in the paper; to the knowledge of the mission authors none of it is formalized in Lean or any other proof assistant. A complete development would provide a machine-checked gradient formula for the softmax class, smoothness bounds for discounted values, and a monotone-improvement argument for policy gradient, each reusable for other parameterizations and other policy optimization methods.
The obvious route fails. The gradient domination property of the direct parameterization (Lemma 4.1 of the paper) would conclude from , but under softmax , so a vanishing -gradient says nothing once some action probabilities vanish, and the iterates do drive probabilities to zero while parameters diverge. A smoothness-based argument therefore gives only stationarity in the limit. The asymptotic analysis must instead track which actions keep positive limiting advantage, how the individual parameters move once the advantage signs are frozen, and why an action with strictly positive limiting advantage cannot coexist with the behaviour of the remaining parameters. Lemmas C.7–C.12 carry that bookkeeping; the limiting sets and the existence of the limits are themselves consequences of the pointwise monotone improvement of Lemma C.2, which needs its own smoothness bound.
Standing setting of §3: finite types S, A with decidable equality, A nonempty; IsFiniteMDP P r γ (a transition kernel, rewards in , ); IsDist µ. Parameters live in EuclideanSpace ℝ (S × A), so norms are and Mathlib's gradient is ; the coordinate of the gradient is . Logarithms do not appear. Conventions committed to:
PolicyValue πstar P r γ s for a policy πstar with IsOptimalPolicy πstar P r γ, optimal simultaneously at every state; it is not a real supremum over all functions.Tendsto … atTop atTop / atBot; "strictly increasing for " is StrictMonoOn on Set.Ici T1, with existentially quantified.The goal theorem does not assume the existence of limits, monotonicity of the iterates, or anything about the sets ; a formalization that did would assume the substance of the proof. Lemmas C.7 and C.11 (first part) carry the hypothesis of the paper's proof by contradiction, which no actual run satisfies once Theorem 5.1 is proved; they are steps of that argument.
A full development needs: differentiability of and the policy gradient theorem in the occupancy-measure form, the performance difference lemma, the descent lemma for -smooth functions, and Hessian bounds for the softmax map. Contributions to any of these, to the optional Lemmas C.8–C.10 and C.12 of the paper, or to the final contradiction argument are welcome.
Distributionally robust optimization replaces the average of a loss over a sample by its worst-case average over all distributions close to the sample. When closeness is measured by an -divergence, the worst case over a ball of radius around the empirical distribution is also the upper endpoint of a generalized empirical likelihood confidence interval. Empirical likelihood (Owen, 1988–2001) is the case ; the , Cressie–Read and other divergences give the rest of the family.
Duchi, Glynn and Namkoong (arXiv:1610.03425, Mathematics of Operations Research 46(3), 2021) show that these robust objects behave, to first order, like the sample mean plus a variance penalty. Their Lemma 1 is the scalar version of that statement and, in the authors' words (p. 7), an expansion "that essentially gives all of the major distributional convergence results in this paper": with the central limit theorem it yields the asymptotically exact coverage of empirical likelihood intervals for a mean, and its uniform extension yields the coverage results for optimal values of stochastic programs.
Timeline. Owen (1988, 1990) proved the calibration of empirical likelihood for means of i.i.d. data. Its extension to smooth -divergences is, as the paper notes (p. 6), essentially due to Baggerly (1998), Corcoran (1998) and Bertail, Gautherat and Harari-Kermadec (2014). Lam (arXiv:1605.09349) proved an in-probability version of the expansion below for . Namkoong and Duchi (2017, arXiv:1610.02581) proved a finite-sample, high-probability version for the divergence and bounded variables. Duchi, Glynn and Namkoong proved the almost-sure version for every smooth and for stationary ergodic data.
Let be convex and lower semicontinuous, as every divergence generator in the paper is. Assumption A asks that be finite on , three times differentiable near , with and ; the value may be .
Let be a sample with empirical distribution . A distribution is a weight vector with , and . The robust mean is
The sample mean is and the sample variance is (normalised by ).
A sequence of real random variables is strictly stationary and ergodic if the law of the path on is invariant under the left shift and every -invariant measurable set of paths has -measure or . Every i.i.d. sequence qualifies (Kolmogorov's – law), as do stationary Markov chains started in a unique invariant law and stationary mixing sequences.
Let be strictly stationary and ergodic with , let satisfy Assumption A and . Then almost surely
This is the paper's (8), " with a.s.", with taken to be the left-hand side. No rate is asserted, so the goal is not tied to any constant.
The result. The expansion says the robust mean is a variance-regularised mean, , up to , for every smooth divergence at once. Combined with the central limit theorem and Slutsky's lemma, it gives , the exact asymptotic coverage of generalized empirical likelihood intervals (the paper's Proposition 1 for ). The paper's uniform expansion (Theorem 2) and its coverage theorem for optimal values (Theorem 3) rest on the same mechanism. Because the statement is almost sure and allows stationary ergodic data, it also covers time series and simulation output.
Formalizing it. The lemma is proved in the paper; no machine-checked version of it, of (30), or of Lemmas 6–9 exists. A complete development would give the first formal link between -divergence balls and variance regularisation for general , and a formal almost-sure theory for empirical likelihood beyond the i.i.d. case. The -only finite-sample expansion of Namkoong and Duchi (2017) is posed, not proved, on the platform.
The obvious route is a second-order Taylor expansion of around inside the supremum. It fails because the optimal weights are close to only if no single observation is large compared with ; a heavy observation drives a weight to , where may be infinite and is not approximated by its Taylor polynomial. The argument has to sandwich the divergence ball between a quadratic ball and a Huber ball valid on all of , then show that the event "no observation of order " holds eventually almost surely, which under only a second moment and no independence needs a Borel–Cantelli argument for identically distributed variables (Lemma 7). The sample variance limit needs Birkhoff's pointwise ergodic theorem, which Mathlib does not yet contain.
Z 0 is the paper's and the -th sample vector is fun i : Fin n => Z i ω. Stationary ergodicity is IsStationaryErgodic: each Z i measurable and Mathlib's Ergodic for the left shift on the path law (which includes shift invariance). The mixing display on p. 7 implies this; the Lean hypothesis is the weaker standard notion named in the lemma.EReal, using the published IsPhiDivergenceFunction (convex on , finite on , , allowed); AssumptionA adds lower semicontinuity on (the paper's standing condition on divergence generators), three-times differentiability on an interval , , . The reading "finite on " follows the paper's remark that only the behaviour at is unrestricted.probUncertaintySet, and the supremum is a real sSup of a non-empty bounded set. Mean and variance are the published empMean, empVar.PalmQueueing.Ergodic.discrete_pointwise, for bijective flows), Borel–Cantelli (in Mathlib), and elementary convex analysis of the Huber function. The pointwise ergodic theorem and Lemma 7 are reusable well beyond this mission. Proofs of any milestone, and of the ergodic theorem for one-sided shifts, are welcome.Consensus asks processors, each holding an initial value, to agree on one value despite some of them failing. It underlies replicated databases, atomic commit and state-machine replication. Its solvability depends on the timing assumptions. With fully synchronous processors and communication, fail-stop faults can be tolerated for any . With fully asynchronous communication, Fischer, Lynch and Paterson showed that no deterministic protocol tolerates even one fail-stop fault (JACM 1985).
Dwork, Lynch and Stockmeyer (JACM 1988) introduced partial synchrony, a model between these two extremes. Message delays have an upper bound , but either the bound is unknown to the protocol, or it holds only from an unknown time on. For each fault type they found the exact number of faults that can be tolerated. This mission formalizes the lower bound for fail-stop faults: when the processors are synchronous and communication is partially synchronous, no consensus protocol tolerates faults once .
Timeline. 1985: Fischer, Lynch, Paterson, impossibility of consensus with one fail-stop fault under asynchrony. 1987: Dolev, Dwork, Stockmeyer, which combinations of synchrony assumptions admit consensus (JACM 1987). 1988: Dwork, Lynch, Stockmeyer, partial synchrony, with matching upper and lower bounds on resiliency for fail-stop, omission, authenticated Byzantine and Byzantine faults. The global stabilization time of the 1988 paper became a common liveness assumption for later fault-tolerant agreement protocols.
There are processors . Each processor holds an initial value . Each runs a deterministic protocol: a transition diagram over a possibly infinite set of states. In each state the next instruction is either , which puts message in 's buffer, or , which removes a set of messages from 's buffer and delivers it. The next state depends on the current state and, for a Receive, on . A step never both sends and receives. Each state may record a decision, and the first decision a processor records is final.
Real time is the ticks . A run fixes the initial values and, at each tick, which processors take a step and which messages each Receive delivers. A message is delivered only after the tick at which it was sent, only to its addressee, and at most once.
A protocol is a -resilient consensus protocol achieving weak unanimity if the following holds for every set of at least processors and every allowed run in which the processors of are correct and the others fail-stop. No two processors of decide differently (consistency). Every processor of decides (termination). If all initial values are and no processor is faulty, every decision is (weak unanimity).
For integers with
there is no -resilient consensus protocol achieving weak unanimity for binary values with fail-stop faults and synchronous processors. This holds for every positive when holds eventually, and when delta is unknown.
Split the processors into groups and with .
The result. Theorem 4.3 shows that the resiliency of the paper's fail-stop and omission protocols (Theorems 4.1 and 4.2) is optimal. It holds even under three restrictions: binary values, weak unanimity, and processors in perfect lock-step. Partial synchrony costs a majority of correct processors, whereas full synchrony costs nothing. The same scenarios give the authenticated Byzantine bound (Theorem 4.4). The halting remark of Section 4.2 rests on an argument of the same kind.
The formalization. The theorem is proved in the paper, and its proof is short. It is not machine-checked anywhere known to the mission. No message-passing model is on the platform. This mission supplies one: a step-level model with buffers, per-message timing, fail-stop faults and both partially synchronous communication models. It also gives a machine-checked impossibility on top of that model. FLP, Theorem 4.4 and the lower bounds of Section 6 are natural follow-ups on the same definitions.
The informal proof is an indistinguishability argument. Making it formal means comparing different runs of the same deterministic protocol. Two points need care.
First, the scenarios must be allowed runs. Scenario C holds messages between the groups back past . With delta unknown, this needs a larger than that delay. When holds eventually, is fixed before the protocol, and the protocol fixes and . So the delay is legal only for messages sent before the global stabilization time, which must therefore be placed after . Read literally, "every message between the groups takes more than steps" is not an allowed run in this model.
Second, "the processors of act exactly as they do in Scenario A" is a claim about whole runs. Two runs must agree on states, on which messages are in which buffer, and on when each message is delivered, tick by tick up to . With one-to-one sends and atomic steps, "delivered in exactly time 1" also needs a reading: a processor that sends at the next tick cannot receive at that tick.
All declarations live in the namespace DLSConsensus.LowerBound. Processor is the index of Fin N. Values are Bool. The protocol's state type and message type are arbitrary types in Type, finite or infinite. R.state i n is the state after tick . A message instance is identified in the run by its sender and send tick. A Receive hands the protocol each delivered message as (sender, content); the absolute send tick is not exposed.
Explicit readings and conventions:
Trivializing formalizations are ruled out. The model has allowed runs for every protocol, so Resilient is never vacuously true. Correct processors step at every tick, so termination does not fail for the wrong reason. Unanimity is the weak form, applied only when no processor is faulty.
Contributions welcome: a general simulation lemma (equal inputs up to a tick give equal states up to that tick), the construction of runs from a delivery schedule, and proofs of the scenarios. These parts are reusable for the other lower bounds of the paper.
The diameter of a polyhedron is the largest number of edges needed to travel between two vertices of its graph, its 1-skeleton. Whether this number is bounded by a polynomial in the dimension and the number of facets is a long-standing open question in polyhedral combinatorics; edge walks are the moves of vertex-following methods such as the simplex method, so the question bounds what any such method can achieve in the worst case. For fixed dimension, Larman proved in 1970 that the diameter grows at most linearly in , with a constant exponential in (Larman 1970).
Eisenbrand, Hähnle, Razborov and Rothvoß ask how much of the geometry of polyhedra such upper bounds actually use. They isolate a single combinatorial path property shared by the graphs of non-degenerate polyhedra and announce that the known upper bounds, Larman's among them, "continue to hold in the base abstraction" defined by that property (Dagstuhl abstract, p. 3). The next sentence of the abstract reads: "While the first bound is merely an adaption of the proof in [13], our proof of the second bound is much simpler than the one which was proved for polyhedra in [16]."
The held source is the five-page Dagstuhl extended abstract dated June 15, 2010, which states the results and proves none of them. The full proofs appear in Mathematics of Operations Research 35 (2010), 786–794 (journal article). The goal is an asserted theorem of the paper, not an open conjecture; the formal proof remains to be supplied.
Let and write for the family of its -element subsets. A graph in the base abstraction has a nonempty vertex set : every vertex is a -element set of labels, and distinct vertices carry distinct sets. The edges are arbitrary subject to condition i): for each there exists a path connecting and whose intermediate vertices all contain . Condition i) makes connected. The class of all such graphs is ; is called the dimension and the number of facets of the abstraction, and denotes the largest diameter of a graph in (p. 2).
The distance is the least number of edges of a path from to . The motivating example is the graph of a non-degenerate polyhedron (each vertex on exactly facets), each vertex labelled by its facets: two vertices are joined by a path inside the minimal face containing both, and every vertex of that path lies on the facets the two endpoints share (pp. 2–3). The class is not restricted to such graphs.
The abstract prints the bound as and states that it continues to hold in the base abstraction. The target is the pointwise form of :
In Lean this is the existence, for every pair , of a walk from to with at most edges. The statement quantifies over every graph satisfying the paper's definition, not over polyhedron graphs or a chosen family.
For fixed the bound is linear in , and it holds for a class defined only by finite sets and one path condition. Together with the almost-quadratic lower bound announced in the same paper, it shows what this one property of polyhedra can and cannot deliver: linear growth in for fixed dimension, but not a linear bound uniform in and . Since the graph of every non-degenerate polyhedron lies in (a separate mission of this series), the result also recovers a Larman-type bound for polyhedra, with constant .
Prove2Me already has proved polytope versions: Hirsch.larman_bound (the sharper constant for nonempty bounded -polytopes), Hirsch.larman_high_dimension, Hirsch.larman_layer_recursion, and Hirsch.tight_row_interval, the polytope form of the interval property that condition i) abstracts. They concern a different object, the vertex-edge graph of an -polytope, and are credited as prior work; none states the bound for every graph of . The platform definition Hirsch_clf (connected layer families) is a related abstraction in layered form and is not the graph class used here.
The class contains graphs with no geometric realization, so a proof cannot use convexity, faces as polyhedra, or linear-algebraic facts about vertices; only labels, intersections and walks are available. Condition i) guarantees a path preserving the common labels of two endpoints, but says nothing directly about the length of that path. Mere connectivity on -subsets of gives only the trivial bound , which is far from linear in . A linear bound in has to be extracted from condition i) alone, uniformly over all graphs of the class. The abstract describes its proof only as much simpler than Larman's for polyhedra and states no intermediate lemma, so the mission carries no milestones.
Fin n, labels ; only the number of labels matters.V : Finset (Finset (Fin n)) and the graph is G : SimpleGraph V; vertices are therefore distinct label sets, as in the paper. InB d n V G requires V.Nonempty, every vertex of cardinality , and CondI V G.CondI asks for a walk all of whose vertices contain . This is the source's path condition: a walk contains a path on a subset of its vertices, and the endpoints contain automatically.Hirsch.larman_bound is not claimed here.Trivializing formalizations are ruled out: labels are the vertices themselves (not an arbitrary labelling that could repeat), and condition i) is required for all pairs, not for one chosen path or only adjacent vertices. A proof only for polyhedron graphs, for graphs with extra structure, or with a larger constant leaves the goal open. Useful contributions include general lemmas about CondI and walk-length bookkeeping for SimpleGraph on a finite vertex type; these are reusable by the other missions of this series.
The diameter of a polyhedron is the largest number of edges needed to travel between two vertices of its graph. Bounding that number from the dimension and the number of facets is a central question in polyhedral combinatorics because edge walks are the discrete moves available to many vertex-based optimization methods. The Kalai–Kleitman bound gives a quasi-polynomial upper bound in these parameters. Eisenbrand, Hähnle, Razborov and Rothvoß ask how much of the geometry is needed to retain such a bound. They isolate one path property of polyhedron graphs and show that the upper bound persists for every graph satisfying it, including graphs that need not arise from a polyhedron (Dagstuhl abstract, pp. 1–3).
This mission concerns that extension of the Kalai–Kleitman bound. The held source is the five-page Dagstuhl extended abstract dated June 15, 2010. It states the result without its proof. The full proofs appeared in Mathematics of Operations Research 35 (2010), 786–794 (journal article). The goal is an asserted result of the paper, not an open conjecture; the formal proof remains to be supplied.
Let , and let be the family of its -element subsets. A graph in the paper's base abstraction has a nonempty vertex set . Thus each graph vertex is labelled by a distinct -element subset. The edges can be chosen freely subject to condition i): for every pair , there is a path from to u\cap v\mathcal B_{d,n}dn$ the number of facets of the abstraction (definition and footnote, p. 2).
The distance between two vertices is the minimum number of edges in a path between them. A graph's diameter is the largest of these distances, and is the largest diameter among graphs in . Condition i) is motivated by non-degenerate polyhedra: if a vertex lies on exactly facets, its tight facets provide a -element label, and two vertices can be connected inside the smallest face containing them. Every vertex on that path retains the facets common to the endpoints (pp. 2–3). This motivation does not restrict to a realizable polyhedron graph.
For positive dimension, the target is the pointwise form of the paper's assertion that the upper bound continues to hold in the base abstraction:
Equivalently, every pair has a connecting path with at most edges. Consequently . The statement covers every graph with the paper's labels and condition i), rather than a selected realization or a graph with extra geometric properties. The source prints the inequality for , its polyhedron-diameter notation, and says in the same sentence that it continues to hold for the base abstraction (p. 3).
The bound shows that a common-facet path property is enough to prevent arbitrarily large diameter once and are fixed. It extends an upper bound first attached to graphs of polyhedra to a class specified entirely by finite sets and graph paths. This locates a concrete portion of the polyhedral diameter theory within combinatorics. The same paper gives an almost-quadratic lower bound for the abstraction, so the path property alone does not imply a linear bound in (p. 3).
A machine-checked proof would connect a precise finite graph model with the real-exponent inequality, without relying on a polyhedron representation. Prove2Me already has a proved theorem called Hirsch.kalai_kleitman_bound for a bounded -polytope, with a different exponent , and a proved Hirsch.kalai_kleitman_recursion for that polytope model. It also has Hirsch.clf_endpoint_peeling for connected layer families. Those results concern different objects or bounds and are useful prior work, but none is a formalization of the present claim for all .
The class permits edges and vertex families with no geometric realization, so a proof cannot use metric or convexity properties of a particular polyhedron. Condition i) guarantees one path preserving the common labels of two endpoints; it does not directly bound that path's length. Connectivity by itself would be too weak: a connected graph on the allowed labels can have a long shortest path unless its labels and the path condition constrain it. The formal task is to obtain the claimed uniform length bound from that condition across all finite families of -sets. The Dagstuhl abstract calls the argument an adaptation of Kalai and Kleitman's proof but states no intermediate lemmas, so this proposal does not assign any in-source milestones (p. 3).
Lean represents by Fin n, with labels instead of ; only the number of labels matters. A vertex set is a Finset of Finset (Fin n), and a SimpleGraph has exactly those sets as vertices. This representation enforces distinct labels. InB d n V G requires to be nonempty, every label to have cardinality , and CondI for every ordered pair. The walk in CondI is equivalent to the source's path: repeated vertices can be erased, and the endpoints themselves contain . Nonemptiness and condition i) together give the source's connectedness. A path through all graph vertices without the common-intersection condition would be a weaker and inadmissible model.
The theorem takes , so the logarithm has its ordinary positive-dimension interpretation. The source does not print a logarithm base; the statement reads it as base two, following the cited Kalai–Kleitman convention. This interpretation is explicit in the theorem's prose and is an open source-reading question. The exponent is real: the path length is cast from a natural number to for comparison with . No floor is applied to the exponent. The theorem asserts a bounded walk for each pair; that avoids defining through a supremum with an artificial value for an empty class. At with , InB has no instance, as there are no -element labels; at , the bound is , consistent with a connected graph on at most labels.
The development needs reusable finite-set reasoning about common intersections, graph walks and their lengths, and real-logarithm bounds. Contributions establishing those facts for the paper's CondI model are within scope. A proof only for polyhedron graphs, for graphs with extra edge restrictions, or for a single chosen graph would leave the goal open.
Consensus asks processors, each starting with a value, to agree on one value although some of them may be faulty. It underlies replicated databases, atomic commitment and state-machine replication. Two classical models bracket the problem. In a fully synchronous system, with known bounds on message delay and processor speed, consensus is solvable for many fault types. In a fully asynchronous system, Fischer, Lynch and Paterson showed in 1985 that no deterministic protocol tolerates even one fail-stop fault (FLP, J. ACM 1985).
Dwork, Lynch and Stockmeyer (J. ACM 35(2), 1988, 288–323) introduced partial synchrony between these extremes: message delays are bounded, but either the bound is unknown, or it holds only from an unknown global stabilization time (GST) on. This model, and the GST abstraction in particular, became the standard assumption under which practical consensus protocols (Paxos-style and Byzantine fault-tolerant replication) are proved live. The paper determines, for each fault type, the largest number of faults that consensus can tolerate under partial synchrony. This mission formalizes its first positive result: for fail-stop and omission faults, processors suffice.
There are processors , an integer , and an arbitrary set of values; processor starts with .
In the basic round model (Section 3.1 of the paper), computation proceeds in rounds . In each round every processor sends messages, each message is either delivered in that round or lost, and every processor then performs a state transition on the messages it received. Losses are described by a predicate . A set of processors (the correct ones) and a round constrain it: every message sent at a round from a processor of to a processor of is delivered. Before GST any message may be lost, and messages from or to processors outside may be lost at any time. Processors outside follow the protocol but lose sends and receptions (omission faults, which include fail-stop faults).
Algorithm 1 (Section 3.2.1) works as follows. Every processor keeps a set , initially , attaches it to every message, and merges in every PROPER set it receives. A processor may hold locks, each a value with an associated phase number; is acceptable to if has no lock on a value other than . Phase belongs to when . Trying phase occupies rounds , , :
Lock-release phase is round : every processor broadcasts its locks , and a lock on with phase is released on receipt of some with and .
The correctness conditions (Section 2.4) for the set are consistency (no two decisions of processors in differ), termination (every processor in decides), and strong unanimity (if all initial values equal , every decision in is ).
For all with , every value type , all initial values, every with , every , every delivery pattern allowed for and , and every admissible choice of proposals,
This is the theorem as printed; it fixes no constants.
Theorem 3.1 shows that, against omission and fail-stop faults, partially synchronous communication costs nothing in resilience compared with a majority bound: suffices, and Section 4 of the paper shows that does not. The lock-and-release structure of Algorithm 1 (a value is decided only after a quorum locks it, and locks are released only on evidence of a later competing lock) recurs in later partially synchronous protocols, where safety must hold regardless of timing and liveness is obtained only after stabilization. The result separates the two concerns cleanly: consistency and strong unanimity hold in every run, while termination uses GST.
The result is proved in the paper; to the best of the available information it has not been formalized in Lean, and no distributed-computing model exists on Prove2Me. The mission produces a machine-checked model of the basic round model with a GST delivery guarantee, a full executable specification of Algorithm 1, and proofs of its safety and liveness. The paper's own proof of Lemma 3.3 is one line and the termination argument relies on "sufficient communication"; a formal proof must make these steps explicit.
The safety argument is an invariant over an unbounded number of phases with an arbitrary loss pattern: a lock on the decided value must be shown never to be released without being replaced by a higher lock on the same value, while competing locks on other values may exist at faulty or slow processors. The obvious argument ("after a decision, every later proposal must equal the decided value") is circular without a persistence statement for locks such as Lemma 3.2. Liveness requires reasoning about what every correct processor knows after GST (its PROPER set and the locks of the others), and it depends on processors sending lock-release and list messages even when these carry no locks or no acceptable values. Quorum counting with and must be carried out over distinct senders.
Fin N; the paper's is the processor of index . Rounds start at ; exec … 0 is the initial state and exec … r the state after round . Phases start at .pick : ℕ → Set V → V, required only to pick an element of every nonempty candidate set, and universally quantified in every theorem.DecidesAt p k v (owner of phase , proposed , at least acknowledgements in round ); consistency requires all such events of processors in to agree.A formalization in which a run cannot exist, the delivery constraint is unsatisfiable, the choice of proposals is fixed, or faulty processors are absent ( = all processors) would trivialize the theorem; the model here admits runs in which processors decide, and ranges over all sets of at least processors.
Reusable beyond this mission: the round-based message-passing model with a GST delivery guarantee and omission faults. Contributions of general lemmas about runs (monotonicity of PROPER sets, persistence of locks, quorum intersection over Finset) are welcome.
Large zero–one linear programs can contain constraints involving only a small fraction of their variables. Crowder, Johnson and Padberg study how to extract useful inequalities from one such row while solving the larger program. Their computational method identifies a violated inequality at a current linear programming solution, adds it, and resolves the relaxation. The mathematical question behind that step is whether a minimal cover inequality can be found by a separate optimization problem. The authors answer it in Section 2.3 of their 1983 paper, after developing cover and configuration inequalities in Section 2.2. Crowder, Johnson and Padberg (1983)
The target is a known result from that paper. It is a precise statement about a finite knapsack row and a point in the unit cube, independent of the paper's implementation and numerical experiments. The paper also discusses -configurations and lifting, which turn the identified inequalities into valid cuts involving additional row variables. Those statements supply the mission's milestones and make the separation result useful in its original setting. Crowder, Johnson and Padberg (1983), Sections 2.2–2.4
Fix a finite index set , positive rational coefficients for , and a rational right-hand side . A zero–one solution is a vector with each satisfying the single row
The model uses the support set for such a vector. A set is a minimal cover when its total coefficient exceeds , but removing any one member makes the total at most :
It yields the cover inequality for every feasible zero–one vector. The right-hand side is interpreted as a real number, so the expression also has its usual meaning when is empty.
A -configuration consists of , and an integer . The set itself fits the row, while is a minimal cover for every -element subset of . For any and -element , its inequality is . Crowder, Johnson and Padberg (1983), pp. 810–811
For a point , the separation problem asks for a cover minimizing , subject to the strict condition . This is problem (2.12). The set of attainable values is finite, but it is empty if the row has no cover. An optimal value is therefore asserted only when a least attainable value exists.
The goal is the paper's Section 2.3 equivalence:
where is the attained optimum of (2.12). A cover inequality cuts off precisely when its left-hand side exceeds . If there is no cover, (2.12) has no optimal value; the theorem does not assign it an artificial value. Crowder, Johnson and Padberg (1983), pp. 812–813
The milestones state the validity of (2.7) and every inequality in (2.9), the two assertions used in the separation equivalence, and the relaxed lifting claims of Section 2.4. For lifting, is the maximum integer objective value in (2.10), is the maximum in its linear relaxation, and . The claims are and validity after adding variable with coefficient . They concern attained optima, as the paper's “maximum” language requires. Crowder, Johnson and Padberg (1983), pp. 811, 814
The equivalence turns a geometric question about which cover inequality excludes into a finite optimization test with a numerical threshold of one. It identifies when a minimal cover cut exists for a row, while the validity milestones certify that the inequalities can be added without removing zero–one feasible points. The lifting claims explain how an inequality first written on a subset of variables remains valid as further variables enter it. These are the mathematical guarantees used by the paper's cutting plane procedure. Crowder, Johnson and Padberg (1983), Sections 2.2–2.4
The paper proves the separation equivalence and states the surrounding validity claims. This mission records their exact statements in Lean; its theorem proofs remain open. A complete development would add machine-checked proofs for the finite cover argument, configuration inequalities, and lifting validity. The resulting definitions of feasible supports, attained optimization values and intermediate inequality validity can also be reused in other finite knapsack formalizations.
Checking all subsets of directly grows rapidly with the row size. A separation result must relate a minimum over all covers to an inequality indexed by a minimal cover, while accounting for objective coefficients that may be zero when . The same boundary matters for lifting: the zero–one maximum is compared with a continuous relaxation, and rounding is justified by the integer coefficients of the current inequality. If the lifting problem is infeasible, neither maximum exists. Crowder, Johnson and Padberg (1983), pp. 812–814
Lean uses an arbitrary finite index type for , replacing the paper's indices . A zero–one vector is a finite support set. Row coefficients and are rational, as on p. 810; the point and separation values are real. The target asks only that lie in the unit cube. Although the paper obtains it as an optimum of the full LP relaxation (2.11), that additional property is not used in the row-level equivalence. No sign condition is imposed on .
The strict knapsack condition in (2.12) is retained. “Chops off” means strict violation of (2.7). “Optimal value” means membership and leastness in the attainable value set; for lifting it means membership and greatestness. Thus rows with no cover or infeasible lifting subproblem do not acquire a default zero optimum. The size expressions and are evaluated in the reals, so natural-number truncation cannot change them. Integer lifting coefficients and the floor of the relaxed optimum express the paper's “truncating to its integer part”; the feasible relaxed problem includes the zero vector, so this agrees with truncation toward zero there.
Validity during an intermediate lifting step ranges over feasible zero–one vectors supported in the current set . After adding , it ranges over support in . The final inequality covers the whole row when that set is . The development must preserve the full quantifier over every -subset in (2.8) and every and in (2.9); restricting these would weaken the paper's claim. Contributions proving the named milestones, adding concrete examples, or developing general finite optimization lemmas are in scope. The facet assertions attributed to Padberg are outside the target. A related lifted-cover facet statement already appears on the platform as NemhauserWolsey.partitioned_cover_lifting_defines_facet; its conventions and claim differ from this mission's validity results.
A manufacturing line can send the same job through several stations and return it to a station it visited earlier. Semiconductor fabrication is one example. Such a reentrant line has several customer classes at one server, and the server must choose which class to work on. A station may have enough capacity on average yet the line can still accumulate an unbounded queue under an unfortunate service rule. Dai and Weiss use deterministic fluid models to study this question: fluid represents large queues, and its motion exposes the long-run effect of the service rule. Their paper proves that two simple buffer priority disciplines have stable fluid models for every reentrant line satisfying the usual station load condition. This mission concerns Last-Buffer-First-Served, abbreviated LBFS. Dai and Weiss (1996).
The distinction between fluid and stochastic queue stability matters. Dai and Weiss cite an earlier theorem connecting stable fluid models to stable queueing disciplines under the stochastic assumptions of their introduction. The target here is their fluid theorem, Theorem 4.4, rather than a separate formalization of that stochastic implication. Dai and Weiss (1996), pp. 115, 119, 124.
There are classes, numbered in route order, and stations. Every unit of fluid enters class at rate one. On completing service in class , it becomes class ; after class , it leaves. The station serving class is . Different classes may share a station. The constituency of station is , and class has positive mean service requirement , so its service rate is . The nominal workload at station is . The paper assumes at every station. Dai and Weiss (1996), pp. 115–117.
For time , is the amount of fluid in class , and is the cumulative server time spent on that class. The flow equations say that class content equals its initial content plus completed service from the preceding class minus its own completed service. The first class receives the external unit-rate flow. Each remains nonnegative, each starts at zero and is nondecreasing, and the cumulative idle time of every station is nondecreasing. A priority rule adds a condition on when a server may reserve capacity for lower-ranked classes. These are the fluid equations of Definition 1.2 and §4. Dai and Weiss (1996), pp. 118, 122–123.
A priority ranking assigns a distinct rank to every class, with smaller rank meaning higher priority. For class , let contain the classes at the same station whose rank is at least as high as 's. In a preemptive-resume priority fluid model, capacity unused by may increase only when the fluid workload in is zero. Under LBFS, : a class later in the route has higher priority. Priority is compared within each station, even though the ranking is written globally. Dai and Weiss (1996), pp. 122–123, Definition 4.1.
Theorem 4.4 asks for stability of the LBFS fluid model for every reentrant line with positive service requirements and :
where . The same must work for every solution and every normalized initial configuration. This is exactly the fluid stability definition used by the paper. Dai and Weiss (1996), pp. 118–119, 124.
The milestones follow the paper's own intermediate statements. Lemma 2.2 treats a nonnegative absolutely continuous function whose derivative is negative whenever the function is positive. Proposition 4.2 identifies flow-rate relations at a regular point under a buffer priority rule. The proof of Theorem 4.4 records a uniform negative drift for total content and the explicit emptying time
The explicit time is stated for every initial fluid amount; normalization to one belongs only to the final stability theorem. Dai and Weiss (1996), pp. 120, 123–125.
The theorem gives a uniform finite clearing time for the LBFS fluid model whenever each station's nominal workload is below its capacity. It applies to any number of stations, any finite route, and any assignment of route stages to stations. This is stronger than checking a particular factory layout. The conclusion concerns every fluid solution, which matters because the defining equations need not determine a unique path. Dai and Weiss (1996), pp. 118–119, 124–125.
Formalizing the result requires a reusable interface for reentrant lines, service allocation, station workloads, and the priority complementarity condition, plus separate statements for the extinction criterion and priority flow rates. The theorem is proved in the 1996 paper; the remaining work in this mission is a machine-checked Lean proof of its fluid-model statement and of the listed milestones. The stochastic queueing theorem cited by Dai and Weiss is outside this mission's scope.
The load inequalities compare average work with available server time, but by themselves they do not specify which class receives service at an instant. Under other service rules, reentrant lines can amplify queued fluid despite every station being nominally underloaded; the same paper gives such an example. A formal proof therefore has to use the precise LBFS priority condition, not only the flow equations and the load inequalities. The regular-time argument must then yield a single bound valid across every possible fluid path. Dai and Weiss (1996), §§4–5.
Lean represents classes and stations by finite index types. Their indices start at zero: Lean class corresponds to paper class , and LBFS is Fin.revPerm. The paths and are functions on all real times, while the fluid equations and conclusions are imposed only for . The external arrival rate is one, as in the paper's normalization. The conditions that station idle capacity and priority-set unused capacity increase only when their relevant content is zero are expressed by constancy on each interval where that content stays positive. Service and fluid paths are not given extra continuity hypotheses; the fluid equations and monotonicity conditions provide the regularity used in the paper. Dai and Weiss (1996), pp. 116–119, 122–123.
The service requirements are explicit so has its intended value. The drift and emptying-time milestones explicitly assume , since their formula divides by the maximum station workload. The main theorem retains the universal quantification over lines; when , its normalization is impossible. A faithful solution predicate must include the priority condition (4.4), whose omission would change Theorem 4.4 into a false claim about all work-conserving policies. The definition layer, elementary real-analysis extinction lemma, and priority flow-rate relations are useful beyond this single stability theorem. Dai and Weiss (1996), pp. 117–125.
Network revenue managers sell access to limited capacity over time. An airline, for example, may have several products that use the same seat inventory, with some products earning more revenue than others. The decision to accept a request must be made when it arrives, before future requests are known. A standard way to guide that decision is to solve a deterministic linear program using expected demand, then use its optimal allocation as a probability of acceptance. As inventory changes, one can solve the program again. Bumpensanti and Wang study how often to do so, and show that frequent re-solving has a real limitation when the linear program is degenerate: on a particular instance its expected loss grows at least as the square root of the selling horizon. Bumpensanti and Wang, arXiv:1802.06192v3, Sections 3.1 and 5.1.
The same paper gives an infrequent re-solving policy with uniformly bounded regret and an upper bound of order for the frequent re-solving policy. The lower-bound result is the counterpart that identifies a case where that order cannot be removed by the frequent policy itself. It uses a two-class example small enough to expose the issue without other network complications. Bumpensanti and Wang, arXiv:1802.06192v3, Theorem 1 and Propositions 2–3.
There is one resource, initially with units of capacity, and two customer classes. Class arrives through an independent Poisson process of rate one. Accepting a customer uses one unit of capacity and earns price , where . Rejected requests earn nothing, and unused capacity has no terminal value. The higher-price class has priority in the deterministic allocation, but its realized demand is random. The horizon is a positive integer, divided into periods of length one. Bumpensanti and Wang, arXiv:1802.06192v3, Section 2, pp. 7–9, and Appendix C.1, p. 32.
At the start of a period with periods left and capacity , the deterministic linear program (DLP) chooses rates that maximize subject to and . In this instance its first coordinate is . The frequent re-solving policy (FR) accepts each class- request in that period with probability , provided capacity remains. It re-solves the DLP at the next period with the new capacity. This is Algorithm 2 specialized to the example. Bumpensanti and Wang, arXiv:1802.06192v3, Algorithm 2, p. 11, and Appendix D, p. 42.
The hindsight optimum knows the total demand from both classes at the end of the horizon and chooses the best feasible allocation using that information. Its expected value is ; the first argument is horizon length and the second is initial capacity. Let be the frequent policy's expected revenue. Since hindsight has more information, their difference is a regret benchmark. The formulation uses the paper's hindsight linear program, which is exact on this unit-consumption instance. Bumpensanti and Wang, arXiv:1802.06192v3, Eq. (3) and Definition 1, p. 9.
For every pair of prices , there are and such that, for all integer and every optimal DLP selector used by FR,
This specializes Proposition 2's existence statement to the explicit family in its Appendix C.1 proof. The constant may depend on the prices, but is chosen before the selector and the horizon. The benchmark is the hindsight value, as in the proposition. Bumpensanti and Wang, arXiv:1802.06192v3, Proposition 2, p. 18, and Appendix C.1, pp. 32–34.
The milestones record the optimal DLP allocation on the example and two clauses of Lemma 7. The latter estimate the probabilities that the high-price arrival count is moderately below its mean in the first third and moderately above its mean in the last third. With an integer phase length and , the first bound is
The third-phase bound uses the standard normal cumulative distribution function and the unrounded constant . Bumpensanti and Wang, arXiv:1802.06192v3, Lemma 7 and Eqs. (49)–(53), p. 40.
This result shows that solving the DLP every period does not, by itself, give a horizon-independent expected loss. The example has only one resource and two customer classes; the gap cannot be attributed to a large network. The paper's separate bounded-regret result uses a different re-solving schedule and acceptance rule, so formalizing this lower bound helps distinguish guarantees for the two policies. Together with the upper bound for FR, it identifies the square-root order as the relevant scale for this policy on the example. Bumpensanti and Wang, arXiv:1802.06192v3, Sections 4–5.
The mathematical proposition is proved in the cited paper; the Lean goal here remains an open theorem statement. Formalizing it requires precise interfaces for a Poisson arrival model, a capacity-limited randomized policy, a hindsight LP benchmark, and asymptotic lower bounds. Those interfaces can be reused in later revenue-management results, while the two-class instance gives a concrete check on the conventions.
The initial DLP solution allocates the average capacity to the high-price class. A simple intuition might therefore predict that repeated re-solving preserves capacity for that class. The remaining-capacity ratio, however, responds to realized arrivals; when the ratio rises above one, the re-solved LP assigns positive acceptance probability to the lower-price class. The policy then spends capacity before later high-price arrivals are known. The lower-bound analysis needs a path event that controls arrivals through the middle phase and a joint event involving the policy's accepted requests. Marginal Poisson counts alone do not determine those admissions. Bumpensanti and Wang, arXiv:1802.06192v3, Appendix C.1, pp. 32–34.
Lean uses Fin 2 for classes and Fin 1 for the resource. The general model takes positive Poisson rates, nonnegative prices and nonnegative consumption. On the lower-bound instance the rates and consumptions equal one, capacity equals , and prices satisfy . These are the operational standing assumptions of the paper's Section 2 and the positive-price reading used by the example. Optimal DLP ties are represented by quantifying over every selector. The LP value is the published RLPBidPrice.Unbiased.piValue definition, evaluated on nonnegative capacity vectors; the rate and capacity conventions make its real supremum well posed.
The window law superposes the independent class Poisson processes into a Poisson total count, independent class labels, and independent Bernoulli acceptance marks. A fold over ordered arrivals applies Algorithm 2's capacity check after every acceptance. The expected hindsight value sums over independent total demand counts, and the FR value is a backward recursion over the remaining unit periods. The target's is strictly positive and fixed before the horizon, so neither a zero constant nor a horizon-dependent constant can satisfy it trivially.
The two Lemma 7 milestones cover only and . Its continuous-time event and the joint admission event require a path probability space and are outside this draft. Equation (52) yields ; the printed rounds that value upward. The source proof divides into three exact integer-length phases, while Proposition 2 is stated for all sufficiently large ; this gap requires attention in a complete proof. The source here is arXiv:1802.06192v3, whose printed and PDF page numbers coincide.
Semiconductor wafer fabrication is the standard example of a reentrant line: every wafer follows the same long route through a set of machines, and visits several machines many times. Each visit is a separate processing step, and a machine with work waiting from several steps must choose which step to serve. Kumar (1993) proposed studying such lines through their buffer priority rules, and Lu and Kumar (1991) showed that a priority rule can make a line unstable even though every machine has spare capacity. The question is therefore not academic: a scheduling rule that looks reasonable can let queues grow without bound.
Dai (1995) reduced the positive Harris recurrence of a multiclass queueing network to the stability of a deterministic fluid model, and Dai and Weiss (1996) used this reduction to prove stability results for several reentrant lines. This mission formalizes their Theorem 4.3: under the First-Buffer-First-Served (FBFS) discipline, the fluid model of every reentrant line is stable whenever each station's nominal workload is below one. Kumar (1993) had proved the analogous statement for discrete deterministic systems.
Timeline:
A reentrant line has stations and classes. All fluid follows one route: it enters as class , becomes class when class is completed, and leaves after class . Class is served at station with mean service time , and . The constituency of station is , and its nominal workload is . The exogenous arrival rate is . The standing assumption of the paper is
A fluid model solution is a pair of paths , the fluid levels, and , the cumulative service time given to each class, such that for :
with ; each starts at and is nondecreasing; and the idle time of each station is nondecreasing.
A buffer priority discipline is a permutation of the classes; a class has priority over a class at the same station when . Write , , and . Under preemptive resume, may increase only at times when (condition (4.4)): a station never idles toward the classes of priority at least that of while any of them holds fluid. FBFS is , so earlier steps of the route have priority.
The fluid model is stable (Definition 1.3) if there is a time such that every solution with has for all .
For every reentrant line with and (1.7),
The goal asserts existence of an emptying time; it does not fix the value.
on, which gives the goal with an explicit constant.
Combined with Dai's theorem (Theorem 1.1 of the paper), Theorem 4.3 gives positive Harris recurrence of every multiclass reentrant line operated under FBFS, under the distributional assumptions of that theorem, whenever (1.7) holds. Since Lu–Kumar-type examples show that priority rules can destabilize a network with spare capacity, a rule that is provably stable on every reentrant line is a meaningful guarantee. FBFS, together with LBFS, is the basic positive case against which the instability examples in the same paper (Theorem 5.1) are compared.
Formalizing the result adds a machine-checked version of the fluid model with priority constraints, stated for an arbitrary line rather than a fixed network, and a checked explicit emptying time. The result is proved in the paper; no machine-checked proof is known. The rate identities of Proposition 4.2 and the extinction lemma are reused by the LBFS mission of this series.
The fluid model gives the paths only as nondecreasing functions subject to equations; nothing says they are differentiable. Every argument about rates holds only at regular times, and the conclusion must be integrated back through absolute continuity, which itself must be derived from the monotonicity conditions. The priority condition (4.4) is an "increases only when empty" condition; turning it into the rate identity (4.6) at a regular point requires continuity of the fluid levels and a careful local argument. The induction over classes needs uniform control of every earlier buffer for all later times, not only at one instant, so a pointwise reading of "buffer is empty" is not enough. Finally, the explicit constant requires bounding the content of buffer at time by the total content, which may have grown since time .
Fin K and Fin I, 0-based: the paper's class is Lean index .ℝ → Fin K → ℝ; every equation is imposed on only, and derivatives are taken at .ConstantWhile): the idle process is constant on every interval of on which the content stays positive. This is equivalent to the paper's Stieltjes integral form for continuous paths.Equiv.Perm (Fin K), FBFS is the identity; is .A trivializing formalization is ruled out: the goal uses the priority fluid model, not the work-conserving one alone (which would claim that every work-conserving fluid model is stable, false by Theorem 5.1), and a sorry-free witness shows that the FBFS solution predicate has solutions with , so stability is not vacuous.
Contributions welcome: the extinction lemma for absolutely continuous functions, the derivation of Lipschitz continuity from (1.10)–(1.12), and the rate identities of Proposition 4.2 are reusable beyond this mission.
Network revenue management decides, in real time, which customer requests to accept when every request consumes a bundle of scarce, perishable resources: seats on several flight legs of an itinerary, room-nights of a multi-night hotel stay, bandwidth on several links. The exact dynamic program is intractable for realistic networks, so practice and theory rely on heuristics built from a deterministic linear program (DLP) that replaces random demand by its mean. The question is how much revenue such heuristics lose.
The classical answer (Gallego and van Ryzin 1994, 1997; Talluri and van Ryzin 1998) is that solving the DLP once and following its solution loses over a horizon of length . Re-solving the DLP as capacity is consumed was long believed to help, and Jasin and Kumar (2012) proved that re-solving in every period has bounded loss if the DLP solution is nondegenerate. Bumpensanti and Wang (arXiv:1802.06192v3) showed that the nondegeneracy condition matters: frequent re-solving can lose on degenerate instances. They then proposed a policy, Infrequent Re-solving with Thresholding (IRT), whose loss is bounded by a constant independent of the horizon and of the capacities, with no nondegeneracy assumption. This mission formalizes that result.
There are customer classes and resources . Class- customers arrive as independent Poisson processes of rate on . Accepting a class- customer earns and consumes units of resource ; is the bill-of-materials matrix with columns , and is the initial capacity. A customer can be accepted only if componentwise, being the remaining capacity; leftover capacity is worthless at .
The DLP with right-hand side is
and is times its value at . The hindsight optimum is , where is the value of the same LP with capacity and the realized demands as upper bounds. It bounds the expected revenue of every non-anticipating policy, and the regret of a policy is .
A probabilistic allocation on a window accepts each class- arrival with a fixed probability when capacity allows. The IRT policy uses and re-solving times for , where . At it solves the DLP with right-hand side (remaining capacity over remaining time), obtaining . In the epochs it accepts class with probability if , else if , else ; in the last epoch it uses . The family re-solves times on the same schedule; is static probabilistic allocation (SPA), and follows until and then earns the hindsight optimum of what remains.
There is a constant such that for every horizon and every capacity vector ,
The constant is not fixed; the content is its independence of , of , and of the optimal LP solution chosen at each re-solve.
The result separates two design choices in re-solving heuristics: how often to re-solve and how to turn an LP solution into a control. It shows that re-solving only times, combined with rounding nearly-degenerate acceptance probabilities to or , is enough for bounded regret, and that the constant is uniform over all capacity-to-horizon ratios, so degenerate DLP solutions, which occur only at particular ratios, cause no loss of order. Since , it also shows that the hindsight optimum is within a constant of the optimal policy's value in this model.
The result is proved on paper but not machine-checked. A formalization would produce a reusable Poisson-arrival revenue-management model, a precise account of the regret decomposition over re-solving epochs, and an independent check of a proof with known gaps (see Difficulty). No part of it is formalized on the platform.
The obvious argument compares the policy with the DLP solution and controls the deviation of Poisson demand by its standard deviation; this gives only , because the DLP value exceeds the hindsight optimum by order and the lost sales accumulate. Bounded regret needs a comparison with the hindsight LP, path by path: the acceptances made before the last re-solve must remain extendable to a hindsight-optimal solution with overwhelming probability. This requires LP sensitivity of the hindsight solution to the random right-hand side, uniformly over the degenerate cases, and the printed proof's statement of it (Lemma 5) is false as printed: on a two-class, single-resource instance its interval for is empty. A correct argument needs a proximity bound for optimal LP solutions under a change of the demand bounds, summed over all classes, not only over . The analysis of the schedule (the sum over epochs in (13)) is elementary but the printed chain of inequalities on p. 30 uses a monotonicity that fails for large arguments.
All objects are in the definition item ResolvingNRM.IRT.Model. Classes are Fin n, resources Fin m, A : Matrix (Fin m) (Fin n) ℝ. LP values reuse piValue from the published RLPBidPrice.Unbiased.Model; the hindsight LP is over real , as in (3). Expectations are explicit sums of Poisson weights. A window of probabilistic allocation is represented by its Poisson count of arrivals, i.i.d. classes with law and independent Bernoulli acceptance coins, the standard representation for controls constant on the window. Policies are backward recursions over the re-solving epochs. Ties in the LP are left open: a policy takes an arbitrary optimal-solution selector, and every theorem quantifies over all selectors after its constants.
Conventions and deviations from the page, each disclosed in the item concerned:
A statement that lets depend on or , compares IRT with the DLP instead of the hindsight optimum, uses a fixed number of re-solves, or assumes a nondegenerate or vertex LP solution is trivial or a different theorem, and is ruled out by the quantifier order of the goal. The milestone has a sorry-free local check.
Welcome contributions: LP proximity results (Cook–Gerards–Schrijver–Tardos type), Poisson concentration, superposition and thinning of Poisson processes, and lemmas on expectations of LP values. The source is arXiv:1802.06192v3; its printed page numbers equal the PDF page numbers.