Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A minimax theorem asserts that, for a function of two variables,
Such equalities are the basis of zero-sum game theory, of Lagrangian duality in optimization, of robust optimization, and of minimax lower bounds in statistics and online learning. Maurice Sion's 1958 paper On general minimax theorems proved the version most often cited today: and convex subsets of topological vector spaces, one of them compact, quasi-concave and upper semicontinuous in , quasi-convex and lower semicontinuous in .
Sion's theorem itself is already machine-checked: Mathlib's Sion.minimax proves it, following the elementary argument of Komiya (1988), and the platform holds it as FamousTheorems.sion_minimax_theorem. Sion's own proof is different. It runs through an open-cover form of the Knaster–Kuratowski–Mazurkiewicz (KKM) theorem, a Helly-type fact about points in low dimension, and a lemma about minimal finite covers (Lemma 3.3). That route has not been formalized. This mission formalizes its ingredients, with Lemma 3.3 as the goal.
Timeline:
Let be a real topological vector space: a real vector space with a topology for which addition and scalar multiplication are continuous. A set is convex if it contains the segment between any two of its points. The convex hull of a set is the smallest convex set containing it.
A real function on a convex set is quasi-concave on if every superlevel set is convex, and quasi-convex if every sublevel set is convex. It is upper semicontinuous (u.s.c.) on if every strict sublevel set is open in the topology inherits from ; lower semicontinuous (l.s.c.) is the mirror notion.
Let be a finite set, a real number, and a real function on . Say that has property P if for each there is a with , and that is minimal for P if no proper subset of has P.
An -dimensional simplex with vertices is the convex hull of affinely independent points.
Let be nonempty and convex, finite, and quasi-concave and u.s.c. on for each . If is minimal for P, then
The lemma makes no compactness or finite-dimensionality assumption on ; that generality is what lets Sion apply it on the convex hull of a finite set inside an arbitrary topological vector space.
Sion's Theorem 3.4 and the Corollary on p. 174 (the minimax theorem) enter the mission as the existing, proved platform item FamousTheorems.sion_minimax_theorem.
Lemma 3.3 is a finite, one-sided statement that already contains the full strength of the quasi-concave case: a finite family of "threats" , none of which can be dropped, can be beaten simultaneously by one point . On p. 174 Sion derives the minimax theorem from Lemma 3.3 and Lemma 3.3′ by reducing open covers to minimal finite ones, alternately on each side. Theorem 3.1 is an open-set KKM theorem with a convexity condition on complements, a covering principle of independent use in fixed-point theory and equilibrium existence. Remark 3.6 shows that the semicontinuity hypotheses are not decorative.
On the formal side, the minimax theorem is proved in Mathlib by another route, so nothing in this mission is needed to know that Sion's theorem is true. What the mission adds is the infrastructure of the original proof: a KKM-type theorem (absent from Mathlib and from the platform), a Helly-type statement about points, and the minimal-cover lemma. None of these has a machine-checked proof today. A formalized open KKM theorem is reusable for Fan's lemma, for Gale–Nikaido–Debreu type existence results and for other covering arguments.
The obvious approach to Lemma 3.3 is induction on , using quasi-concavity to combine points that are good for subfamilies. It fails because quasi-concavity gives control over superlevel sets only, so the union of two "bad" sets is not controlled, and nothing forces two partial witnesses to have a common improvement on the segment between them. The lemma is genuinely topological: without upper semicontinuity it is false (Remark 3.6 exhibits the resulting failure of the minimax equality).
The topological content sits in Theorem 3.1. Neither Mathlib nor the platform has a KKM theorem (the platform has Brouwer's fixed-point theorem), and the passage from the classical closed-set KKM theorem to the open-set form, and from a simplex inside a possibly non-Hausdorff topological vector space to the standard simplex, both need care: the topology induced on a finite-dimensional subspace need not be the Euclidean one.
[AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E], the class of Mathlib's Sion file. No Hausdorff or finite-dimensionality assumption is made. The paper never names the ambient space; "convex set" is read as a convex subset of such a space.QuasiconcaveOn, QuasiconvexOn, UpperSemicontinuousOn, LowerSemicontinuousOn, all relative to the set or .Finset ι; values off are irrelevant. Minimality is "no strict sub-Finset has property P".Module.finrank).EReal; "cannot be removed nor appreciably weakened" is informal and omitted.Contributions welcome: a formal KKM theorem (closed and open versions), Theorem 3.2 from Mathlib's Convex.helly_theorem, and proofs of the milestones in any order.
Markets for indivisible goods, in which each participant owns one unit and wants one unit (houses, kidneys in paired donation, dormitory rooms, school seats), cannot be analysed with the convexity assumptions of classical general equilibrium theory. Shapley and Scarf (1974) introduced the housing market to ask whether the two central solution concepts of exchange economies survive indivisibility: the core (allocations no coalition can improve upon by trading among itself) and competitive equilibrium (allocations supported by prices at which every trader optimizes within his budget). Their paper (doi:10.1016/0304-4068(74)90033-0) gives two proofs that the core is nonempty. The first (Section 4) shows that the associated game without side payments is balanced and invokes Scarf's theorem; that is the companion mission of this series. The second (Section 6) is a constructive argument the authors attribute to David Gale, the top trading cycles method, which also produces competitive prices. This mission formalizes the second.
Timeline.
A finite set of traders each brings one indivisible good; "item " is the good of trader . Preferences are a real matrix : trader prefers item to item when and is indifferent when . Ties are allowed, and only comparisons matter.
An allocation is a bijection ; trader receives item . For a coalition , an -permutation reshuffles the items of among the members of . The allocation is a core allocation if there is no nonempty and -permutation with for every .
Prices are competitive for if each trader , selling his own item for , can afford , i.e. , and no item with is better for him than .
For , a top trading cycle for is a nonempty whose members can be arranged in a cycle so that each likes the good of at least as well as any other good in . A top-trading-cycle partition is
with a top trading cycle for and each a top trading cycle for . In Lean the partition carries stage : N → Fin p and the successor map next : N → N.
For every market and every top-trading-cycle partition with successor map , the allocation is a core allocation, and for every choice of prices
on the goods of it is competitive. The paper asserts that "a set of competitive prices exists"; its argument works for every such choice, and the goal states that.
For the matrix the unique competitive payoff is at equal prices, while the allocation with payoff is a core allocation that is competitive at no prices.
The result gives the existence of a core allocation of every housing market by an explicit construction, and shows that this allocation is competitive, so the competitive solution is nonempty even though goods are indivisible and preferences may have ties. The Section 7 example shows that the inclusion of competitive allocations in the core is strict in general. Under strict preferences, the outcome of the construction is the basis of the matching-market literature: uniqueness of the strong core (Roth–Postlewaite), strategy-proofness (Roth), and the school-choice and kidney-exchange mechanisms built on top trading cycles.
The mathematics is classical and proved. The formalization adds a machine-checked statement of the weak-preference version with the paper's strict blocking notion and its price argument, which existing formal developments do not cover. The closest platform items are AGT.house_core_unique, the strict-preference refinement (Roth–Postlewaite: with strict preferences and weak blocking the core is exactly one allocation), and the school-choice items SchoolChoice.TTC.*. Neither is this statement: the first assumes strict total orders and a different blocking notion, under which the core can be empty once ties are allowed, and says nothing about prices; the second concerns another model with priorities.
Each step is short on paper; the work is in the bookkeeping. The cycle allocation must be shown to be a bijection of from the stage-by-stage cycle structure; the "chain of best-liked goods that eventually must come back to some earlier element" must be turned into a cycle whose members each get a best good in , with ties handled by a choice rather than by a unique top choice; and the first-stage argument must be carried out with the coalition's reshuffling restricted to its own goods. A tempting shortcut, assuming strict preferences or using a union of cycles at a stage, proves a different statement and is ruled out by the definitions.
N with decidable equality; no nonemptiness is assumed (the empty market has the empty partition). The matrix A : N → N → ℝ has no hypothesis, so ties are allowed.σ : N → N rather than zero-one matrices. This loses nothing: a coalition in which all members are strictly better off gives each member exactly one item of the coalition (owning nothing is ranked below everything), and an allocation leaving a trader without an item is blocked by that trader alone.next, every member reaching every other by iterating next. A one-trader cycle with next i = i is allowed (footnote, p. 114).A convex program is useful in practice only if its optimal value responds reasonably to small changes in the data. Lagrangian and Fenchel duality theory makes this precise: the dual problem attains its optimum and has no duality gap exactly when the primal value function does not fall off infinitely steeply under small perturbations. A constraint qualification is a checkable condition on the data that guarantees this good behaviour; Slater's condition (a strictly feasible point) is the best-known example in finite dimensions.
R. T. Rockafellar's 1967 paper Duality and Stability in Extremum Problems Involving Convex Functions (Pacific J. Math. 21 (1967) 167–187) develops Fenchel-type duality for the problem of minimizing in general locally convex spaces. It introduces the notion of a stably set problem, shows that stability is equivalent to strong duality with an attained dual optimum (its Theorem 3), and gives in Theorem 1 a general sufficient condition for stability. Theorem 1 is the infinite-dimensional analogue of Slater's condition and is the form in which the result is usually applied: one exhibits a single point where is finite and is finite and continuous.
Timeline. Fenchel (1951) proved the duality theorem for in under relative-interior conditions. Brøndsted (1964) and Moreau (1966–67) extended conjugate duality to paired locally convex spaces. Rockafellar's 1967 paper (this mission) added the linear map , the perturbation function , the notion of stability, and Theorem 1. The perturbational approach was later systematized in Rockafellar's Conjugate Duality and Optimization (SIAM, 1974).
Let and be real locally convex Hausdorff topological vector spaces and a continuous linear map. Let and .
and its perturbations are : minimize , for . The perturbation function is , so . is consistent if .
Suppose there exists such that is finite at and is finite and continuous at . Then
The neighbourhood is left unspecified, as in the paper.
The result. Combined with the paper's Theorem 3, Theorem 1 yields: if is finite at some where is finite and continuous at , then , with the dual maximum attained. This is the standard sufficient condition for Fenchel–Rockafellar duality in infinite dimensions, used in calculus of variations, optimal control, and the convex analysis of integral functionals. The continuity half of Theorem 1 says that the optimal value depends continuously on translations of the constraint data near the unperturbed problem, a basic sensitivity statement.
Formalizing it. The theorem is proved (1967) and appears in many textbooks, but there is no machine-checked version on this platform. Mathlib contains continuity criteria for real-valued convex functions on open sets of normed or finite-dimensional spaces (ConvexOn.continuousOn_tfae, ConvexOn.continuousOn_interior), but nothing for extended-real-valued convex functions on general topological vector spaces, no perturbation function, and no notion of a stably set problem. A complete development would provide reusable infrastructure: the epigraph-interior continuity criterion for -valued convex functions and the elementary calculus of one-sided directional derivatives.
The obvious argument says: is continuous at , so is bounded above near , hence is continuous at and its directional derivatives are bounded. Two steps of this fail without care. First, the passage from "bounded above near a point" to "continuous" requires convexity of (Lemma 2 of the paper, proved in the companion mission) and a continuity criterion valid in an arbitrary topological vector space, with values in ; the normed-space proofs in Mathlib do not apply. Second, may take the value , and the derivative may be in some directions; the bookkeeping of extended-real arithmetic (where is not defined mathematically and is given a junk value in Lean) has to be done honestly. Finally, upper bounds on must be converted into lower bounds, which is where the second inequality of (4.6) enters; an upper bound alone does not give stability.
All values are in Lean's EReal. Convexity is convexity of the epigraph with real second coordinate (the paper's definition, p. 170); concavity is convexity of . Properness is stated as in the paper. The perturbation function is the EReal infimum ⨅ x, f x - g (A x - z); under properness the undefined form never arises. The directional derivative (4.3) is the lower limit of the difference quotient along , which equals the paper's limit whenever it exists (always, for convex with finite). "Unstably set" quantifies over all neighbourhoods of and all real , with allowing . "Stably set" is together with "not unstably set", so is stably set, as the paper says on p. 176. Continuity is with respect to the order topology of EReal, and "continuous at " is continuity of itself at that point, not of its restriction to .
The paper's standing setting (§3) includes dual spaces , the adjoint and the conjugates . Neither Theorem 1 nor its proof uses them, so they are omitted and the theorem is stated for every pair of real locally convex Hausdorff spaces, which includes every paired setting. The lower and upper semicontinuity of and are standing hypotheses of the paper and are kept, although the proof does not use them. Inequality (4.6) is stated for an arbitrary convex function finite at , the generality in which the paper invokes it. No statement was repaired.
A definition of "stably set" that already presumed finiteness or continuity of near , or that tested the derivative only in a fixed set of directions, would make the first conclusion of Theorem 1 trivial; the definition used here is the paper's p. 175 definition verbatim, applied to an arbitrary function . The definitions are local to this mission; the companion missions on Theorem 3 and Theorem 6 of the same paper define the same objects in their own namespaces. Contributions are welcome on the milestones in any order, and in particular on a general continuity criterion for extended-real-valued convex functions on topological vector spaces, which is reusable well beyond this mission.
The Euclidean traveling salesman problem asks for the shortest closed route through a finite set of points in the plane. Even when the points are placed independently and uniformly in a square, finding an individual shortest route is computationally difficult. A separate probabilistic question is whether the optimal length varies much from one random sample to another. In Chapter 11 of Talagrand's 1995 paper, this question motivates a concentration theorem for the tour length and for other geometric functionals with the same local regularity property.
The result is useful because a bound on fluctuations can be applied without computing the distribution of the optimal tour length. It separates the typical size of the length, which may need other geometric estimates, from the chance of a substantial deviation. The paper develops a more general concentration method for product spaces; the geometric chapter shows how its estimates can control an optimization problem whose response to changing one sample point depends strongly on the local configuration.
Let , and let be independent points uniformly distributed in , with . A configuration is the finite set ; repeated sample locations are represented once in . For any finite , write for the length of a shortest closed tour visiting every point of . The tour length of the random sample is . The empty set and a singleton have tour length zero.
The main theorem concerns a functional on all finite subsets of . A level dyadic square has side . Say that has regularity constant when, for every finite and every finite , if a point of lies within Euclidean distance of , then
The first inequality is monotonicity under adding points. The second limits the added cost when the new points lie in a small square near an existing point. Lemma 11.2.1 says that the shortest tour functional has this property with a universal constant. In particular, the functional in the main theorem is not an arbitrary real function on samples: it must obey this condition for every admissible square and pair of finite sets.
A median of is any real number for which both and are at least one half. The theorem applies to every median. This convention avoids selecting one median when the distribution has more than one.
For the intermediate geometric estimates, is the largest integer with . Given a deviation parameter , is the integer selected by the criterion (11.1.9) after the paper sets the auxiliary Poisson intensity to . The number counts level squares that contain at most distinct sample points. An isolation weight records the largest scale between and at which the square containing contains at most sample points, and equals if no such scale exists.
For each fixed , there is a constant , independent of and , such that every measurable with the regularity property above satisfies, for all ,
This is Theorem 11.2.2, the goal. Its constant may depend on the fixed regularity constant . Lemma 11.2.1 makes the tour length a direct instance. The milestone list also includes the quantitative sparse-square estimate of Proposition 11.1.4, the isolation-weight bound of Proposition 11.2.3, and the deterministic insertion estimate of Proposition 11.2.5. These retain the paper's specified thresholds and the dependency of their constants.
For , the result supplies a tail bound whose scale does not grow with the number of sample points. It says that the shortest tour length lies near a median with a Gaussian-form upper bound on the probability of a deviation. It does not identify the median or give an algorithm for finding the optimal tour. The abstract form also covers other finite-set functionals once their local regularity condition is established.
The paper proves these claims in ordinary mathematics. This mission asks for machine-checked proofs of the stated concentration, geometric occupancy, and tour-insertion results. The reusable outputs include a finite-set model of Euclidean tours and a precise interface for local regularity; the dyadic occupancy and isolation-weight definitions can support later sections on other geometric structures. No machine-checked proof of these specific chapter results is claimed here.
A naive bounded-differences estimate treats the effect of changing a sample point as if a single fixed worst-case insertion cost applied everywhere. That loses the paper's uniform fluctuation scale: a point can be unusually isolated, and its insertion cost can be much larger than the cost near a typical dense cluster. The central problem is to keep track of those irregular locations while retaining a bound uniform in . The chapter's dyadic-square counts and isolation weights make this difficulty explicit in the statements.
Points are pairs of real coordinates constrained to , represented as functions on Fin 2. Their distance is the Euclidean distance, defined explicitly; the default norm on a Lean function space would give a different metric. The random sample is a product of coordinatewise uniform probability measures. is the set of distinct sampled locations, so ties have a defined value. Tour length is the minimum cyclic tour cost over the finite set, using the published generic metric-TSP tour model as its base.
Dyadic squares are closed in the local regularity condition. For the single square assigned to a point in the definition of , the implementation uses half-open cells, with the right endpoint assigned to the final cell. This resolves only grid-line ties, which have probability zero under the stated sample law. Counts use distinct locations, as does the paper's set . All probability inequalities are compared in the extended nonnegative reals. The event bound is written with ENNReal.ofReal; a negative formal lower bound represents the paper's trivial probability lower bound. The main theorem explicitly assumes measurability of the sample functional, following the paper's convention that all relevant functions are measurable. Theorems in Section 11.1 retain and ; the main theorem covers every .
The formalization must not replace the square's uniform law by an arbitrary distribution, use a supremum-norm tour, or place the existential constant after or . Contributions toward the goal may develop measure-theoretic facts about the product law, finite Euclidean tours, dyadic occupancy bounds, or the insertion estimate. Those interfaces have uses beyond this chapter.
Bin packing asks for the minimum number of unit-capacity bins into which a list of items with sizes in can be packed. It is one of the basic NP-hard problems of combinatorial optimization and operations research, and its stochastic version, where the item sizes are random, has a large literature (Coffman and Lueker, Probabilistic Analysis of Packing and Partitioning Algorithms, 1991). A first question about the random optimum is how strongly it concentrates around its typical value.
A short history of that question, as Talagrand recounts it on p. 151 of the source:
This mission formalizes that chapter.
Let and . A point is a list of item sizes. A packing into bins is a map with for every bin . The bin packing number is the least for which a packing exists ( bins always suffice; when ).
Further notation, as in Lean (TalagrandConc.BinPacking):
l2Norm);levelSet);U, V, convexDist);secondMoment);IsMedian).For every median of and every with ,
The goal keeps the paper's explicit constants , and .
The result. Theorem 6.5 shows that the random optimum fluctuates on the scale rather than . For small items () this is much sharper than the martingale bound, and it is the scale of the fluctuations of , which is a lower bound on . Chapter 6 is also the first application in Part II of the paper, and its scheme recurs in the later chapters: a deterministic lemma relating the functional to of a level set, a tail bound for an auxiliary factor, and Theorem 4.1.1 to finish.
Formalizing it. The result is proved (Talagrand 1995; Rhee 1994 by another route). No machine-checked proof is known to exist: the platform has no random bin packing statement and no general- form of Talagrand's convex distance inequality. A complete development gives a checked concentration bound for an NP-hard combinatorial optimum, plus a bin-packing layer (the optimum as a minimum over assignments, Lemma 6.1, monotonicity in the item set) that other formalizations can reuse.
The obvious route is a bounded-differences argument: changing one item changes by at most one. That route yields only the exponent , because it cannot see that small items change little. Replacing the Hamming geometry by one weighted by item sizes is the point. The weights depend on the point itself, so no fixed weighted Hamming distance works. The convex hull distance controls every weighting at once, and the resulting factor is random and must be controlled separately (Lemma 6.3). In Lean, the further difficulty is the probabilistic input: Theorem 4.1.1 / Eq. (4.1.2) for a general (non-finite) is not available, and the convex-hull minimax step (Lemma 4.1.2) behind Lemma 6.2 must be formalized too.
unitInterval. Coordinates are Fin N (0-based). is Measure.pi (fun _ : Fin N => μ) for μ : Measure unitInterval with IsProbabilityMeasure μ. No density is assumed.sInf {k : ℕ | IsPacking x k}, an exact minimum over assignments Fin N → Fin k, not a heuristic such as First Fit. Zero-size items are allowed, as in the paper.ℝ≥0∞ with the Euclidean norm written out ( for an empty set; Mathlib's default norm on Fin N → ℝ is the sup norm). Lemma 6.2 is stated in ℝ≥0∞.ℝ≥0∞-valued. Every event in the statements (, ) is Borel. The paper's measurability convention matters only inside the proofs.sInf.In 1952 Herbert Robbins asked how a statistician should draw a sample sequentially from two populations when the goal is the largest possible expected total, not a test or an estimate after the fact (Robbins 1952). This is the problem now called the two-armed bandit, and Robbins' paper is the usual starting point of the multi-armed bandit literature that underlies clinical-trial allocation, adaptive experimentation and online recommendation (Lattimore and Szepesvári 2020).
Robbins illustrated the problem with two coins. His first concrete rule, "stay on heads, switch on tails" (later known as win-stay, lose-shift or play the winner), uses only the outcome of the last toss, yet its long-run loss relative to an observer who knows the better coin is at most per toss, against for a rule that ignores the outcomes. The same rule was studied again in clinical-trial design as "play the winner" (Zelen 1969).
Timeline. 1952: Robbins computes the operating characteristics of the stay-or-switch rule and of the outcome-blind rule for two coins, and shows that a greedy rule with sparse forced sampling attains for arbitrary populations with finite means (Section 2). 1969: Zelen proposes the play-the-winner rule for clinical trials. 1985: Lai and Robbins give the logarithmic lower bound on regret and rules that attain it (Lai and Robbins 1985).
Two coins and have unknown head probabilities and , with . A head pays \1x_i\in{0,1}iS_n=x_1+\dots+x_nn0A(1-\alpha)\delta_0+\alpha\delta_11B(1-\beta)\delta_0+\beta\delta_1$.
A sampling rule chooses the coin for each toss from the outcomes of the earlier tosses. Two rules are studied.
Write for the probability of heads on the -th toss under the rule in use, and for the expected average payoff of the first tosses. The paper's two parameters are
so that is the expected payoff per toss of an observer who knows the better coin. Following the paper, and are assumed not both and not both ; then .
Under ,
and for every admissible pair of coins
with equality at and at (Eqs. (6), (8) and the text after (8), p. 531).
The result. The goal quantifies how much an extremely simple adaptive rule recovers. A rule blind to outcomes loses up to half a dollar per toss; one bit of memory cuts the worst case to about . Robbins used this comparison to argue that the sequential design problem has nontrivial, computable answers, and to motivate the forced-sampling rule of the same section, whose loss tends to . The closed forms (3)–(6) are the exact operating characteristics of the four-state Markov chain that generates.
Formalizing it. The results are classical and elementary on paper, but none of them has a machine-checked proof. The mission produces a verified chain from the canonical bandit measure to an explicit long-run payoff: the head probability of a fixed toss is computed from the law of the whole trajectory, the recursion is derived from the rule's kernels, and the Cesàro limit closes the argument. The same pattern applies to any finite-memory bandit rule, and the coin bandit and the two rules are reusable test cases for the platform's bandit library. No platform theorem states , its recursion or its loss; other two-state models on the platform (a Markov-renewal gain rate, an MDP gadget) are different objects.
The recursion (2) is a statement about the trajectory law, not about a Markov chain given in advance: the chain has to be extracted from the Ionescu–Tulcea construction of the bandit measure, where the coin of toss is a deterministic function of toss and the payoff is drawn from the chosen coin's law. The head probability alone is not a Markov chain: depends on the joint law of coin and outcome at toss , so a naive one-step argument on does not apply, and the affine form of (2) is a property of this particular rule. The maximization in (8) is over a two-dimensional region whose maximizers lie on the boundary or , and the excluded corners are exactly where the formula breaks down.
The bandit is the published BanditAlgorithm.StochasticBandit 2; the rules are policies of the published type BanditPolicy 2, and probabilities and expectations are taken under the published infinite-horizon measure banditTrajMeasure, whose coordinate is toss . Head probabilities are elements of unitInterval. The conventions committed to are:
The asymptotic loss is stated as the limit of ; defining by its closed form would make the goal a tautology. Likewise, the head probabilities are computed from the law of the rule on the coins: positing a sequence that satisfies (2) would drop the probabilistic content.
A complete development needs: the one-dimensional marginals of banditTrajMeasure (the law of coordinate given the prefix), the joint law of (coin, payoff) at each toss, linearity of expectation for bounded payoffs, a Cesàro-mean lemma, and a short two-variable optimization. The trajectory-marginal lemmas are reusable for every bandit mission on the platform; contributions that prove them in general are welcome.
An experimenter can draw observations from two populations and , one at a time, and wants the sum of the observations to be as large as possible. The populations might be two treatments, two seed varieties or two manufacturing processes; their means are unknown. Each draw both earns a reward and tells the experimenter something about the population it came from. This is the two-armed bandit problem. Herbert Robbins posed it in its modern form in his 1952 address to the American Mathematical Society, Some aspects of the sequential design of experiments, the paper usually credited with founding the field.
Section 2 of that paper asks a basic question (display (12), p. 532): is there any sampling rule whose average reward per draw approaches the larger of the two means, whatever the populations are? Robbins answers yes, for any two populations with finite means, using one explicit rule: forced sampling along a sparse schedule, greedy choice otherwise. This mission formalizes that answer.
Timeline:
Population has distribution function and population has , with expectations
assumed to exist, i.e. to be finite (display (1), p. 529). Nothing else is assumed about and .
A sampling rule draws one at a time; the population of the -th draw may depend on , and given that choice is a fresh draw from the chosen population. Write . The loss of after draws (display (9), p. 531) is
the average shortfall per draw compared with someone who knows the better population and samples only from it.
The forcing schedule (display (13), p. 532) is a pair of disjoint, strictly increasing sequences of positive integers
of density zero: the fraction of the integers that are an or a tends to .
The rule : at draw , sample if is an , sample if is a , and otherwise sample if the mean of the previous observations from is strictly larger than the mean of the previous observations from , and if it is not (a tie goes to ).
For every pair of populations with finite means and every forcing schedule,
The goal is about the specific rule and every schedule, not about the mere existence of a rule. It contains no rate and no constant, so it stays valid when the rule is analysed more finely.
The goal follows from (15) by the definition (9); the paper's chain is (14) ⇒ (15) ⇒ (16).
The result. The theorem answers question (12) and shows that "learning while earning" costs nothing in the long run, per draw, under no assumption beyond finite means: no bounded support, no variance, no parametric family. It is the first consistency result for an adaptive allocation rule, and it fixes the benchmark later refined by logarithmic-regret theory. In modern terms, a forced-exploration greedy policy has regret on every two-armed bandit with integrable rewards.
Formalizing it. The paper gives no proof; it says the results "can be shown". A machine-checked proof records the argument in full. The platform already has finite-horizon regret bounds for -greedy with bounded rewards (FoundationsRL.Bandits.epsilon_greedy_regret_bound), consistency in the stronger Lai–Robbins sense as a definition (ConsistentBanditPolicy), and a forced-sample tail bound for the Lasso bandit (BastaniBayati.LassoBandit.forced_sample_estimator_tail). None of these covers a deterministic greedy rule, almost-sure convergence, or unbounded rewards with only a first moment, and none of them proves (14)–(16).
The obvious argument is: each population is sampled infinitely often because of the forced draws, so each running mean converges by the strong law, so greedy eventually picks the better population, and the forced draws are negligible. Two steps are not routine.
First, the strong law applies to i.i.d. sequences, while the observations from arrive at random, history-dependent times. The values seen from have to be identified, in law, with an i.i.d. sequence that is independent of the times at which they are used.
Second, passing from (14) to (15) needs uniform integrability of , and only first moments are available. No second moment is assumed, so variance bounds are not available.
When greedy need not settle on either population; the statement must hold anyway, and an argument that waits for greedy to "lock in" does not cover this case.
The populations are a published two-armed BanditAlgorithm.StochasticBandit 2. is arm 0 and is arm 1; and are banditArmMean. A rule is a published BanditPolicy 2, and is the integral against the published infinite-horizon law banditTrajMeasure, whose coordinate is the paper's draw . Explicit readings of the paper's phrases:
Integrable. This is the only assumption on the populations: the class of the paper is left arbitrary, and is allowed.#({1,…,n} ∩ (range a ∪ range b)) / n → 0 in . The sequences are infinite and 0-indexed (a 0 = 1, b 0 = 2).∀ᵐ under the trajectory law, and "lim" is Tendsto … atTop along .Trivializing formalizations are excluded. Without integrability the means and expectations are junk zeros; this is ruled out by the integrability hypothesis. Replacing by "there exists a rule" would weaken the goal to (12). Finite forcing sets would make the statement false.
The needed infrastructure is a representation of the adaptive sampling process by per-population i.i.d. reward sequences, the strong law along random subsequences, and a uniform-integrability argument for averages under only a first moment. All three are reusable for other forced-exploration and greedy policies. Contributions of these general lemmas as separate theorems are welcome.
Linear programming asks for the best value of a linear objective subject to linear equations and inequalities. Primal-dual interior-point methods seek feasible primal and dual solutions while keeping every constrained coordinate positive. The resulting pair has a measurable gap between its objective values, so an algorithm can stop when the gap is below a chosen precision. Mizuno, Todd, and Ye studied methods that adjust the length of each step according to the current point. Their technical report gives a predictor–corrector algorithm whose worst-case iteration count grows on the scale of the square root of the number of variables times the requested precision parameter Mizuno, Todd, and Ye, Cornell ORIE Technical Report No. 944, pp. 6–9.
The result matters to readers who need a mathematical guarantee for an adaptive step rule. The algorithm takes one predictor step that reduces the gap and then one corrector step that recenters the pair. Its step length is defined by remaining inside a specified neighborhood, rather than by a fixed schedule. The theorem connects that local rule to a global termination bound.
Fix an integer of variables, an arbitrary number of equality constraints, a real matrix , and vectors and . The primal problem minimizes over , . Its dual problem maximizes over , . The dual slack is . The development reuses a published general-form LP model and specializes it to this pair.
The strictly feasible pairs are the pairs satisfying the two feasibility systems for some dual multiplier , with every coordinate of and strictly positive. The multiplier is allowed to vary with the pair. Write , , and for the vector of ones. The duality measure is . For , the Euclidean central-path neighborhood is
The search direction at with parameter solves the three equations , , and . A step of length yields . Algorithm 1 begins in . It takes a predictor direction with to the greatest step whose entire path remains in , then takes one full corrector direction with . The resulting pair starts the next iteration. The algorithm stops when ; its starting gap is at most report, pp. 4 and 6–7.
For every real precision parameter , every run following Algorithm 1 from an allowed starting pair reaches the stopping threshold at some iteration with
The paper states the iteration order as . The explicit ceiling records the count given by its proof without allowing an unspecified constant to depend on the LP instance report, Theorem 1, pp. 8–9.
The supporting targets are equations (4)–(5), Lemma 1(a), Lemma 2(a)–(b), Lemma 3, Lemma 4, and the contraction displayed in the proof of Theorem 1. They cover the duality measure along a step, bounds on the scaled second-order term, preservation of the inner neighborhood, the predictor step length, and the per-iteration reduction. The milestone list follows the order in which these facts enter the report's analysis report, pp. 4–9.
Theorem 1 gives a stopping guarantee for a fully specified adaptive predictor–corrector method on a feasible primal-dual LP pair. In particular, the requested precision can grow while the iteration bound scales with , rather than with , in this neighborhood model. It also gives a quantitative reason to track two neighborhoods: the predictor may leave the inner one, while the corrector brings the iterate back for the next round.
The report proves this mathematical claim, but this mission does not assert that its proof has already been machine checked. A completed formalization would supply reusable Lean definitions for strictly feasible LP pairs, Euclidean centrality, search directions, and algorithmic step relations. Solvers may formalize the report's argument or another proof of the same statements; the audited goal and milestones fix the mathematical contract.
The predictor direction is aimed at reducing the duality measure, but a long step can move the componentwise products away from their common average or make a coordinate nonpositive. The corrector recenters the pair, yet its effect must be controlled in the same Euclidean neighborhood. A gap decrease alone therefore does not imply that another iteration can be taken. The central difficulty is to establish both a nonzero admissible predictor length and preservation of strict feasibility and centrality under the full corrector step.
Vectors are functions on Fin n, and is a finite matrix. The report's indices correspond to Lean indices . The norm in and in Lemmas 1–2 is explicitly : Lean's default norm on functions is a supremum norm. All powers of two use real exponents, and is natural logarithm. The hypothesis gives meaning to ; no sign condition on is imposed, since for the starting pair already meets the stopping test.
The source's “largest” predictor step is represented as an attained greatest element of the admissible set, with admissibility required throughout the step interval. Some interior points have admissible intervals without a greatest member. In particular, at there may be no continuing run under this literal algorithm rule; the goal retains and makes this limitation explicit. The denominator in Lemma 4 can vanish. The formal lower bound uses its limiting value in that case, avoiding a zero returned by Lean's total division. The separate contraction milestone assumes , because its printed lower bound on the predictor length fails at .
The definitions keep primal feasibility, an existential dual multiplier, coordinatewise strict positivity, and the three direction equations visible. A sequence is constrained by the transition relation whenever its gap exceeds ; values after stopping play no role. These conditions exclude trivial encodings in which the gap threshold is built into the run or centrality is measured with the wrong norm. The remaining work includes Euclidean finite-sum estimates, positivity along steps, and the iteration-count argument. The LP specialization and norm infrastructure can be reused in further interior-point developments.
Manufacturers of perishable goods must decide how much inventory risk to leave with retailers. A retailer who pays for every ordered unit may order less than is best for the manufacturer and retailer together; a generous return policy changes that incentive. Pasternack studies this question in a single-period setting, with a fixed selling price, uncertain demand and goodwill costs when customers cannot be served. The article identifies two familiar endpoint policies that fail: no returns, and unlimited returns reimbursed at the full wholesale price. It then investigates partial credit as a way to align the order decisions. Pasternack (1985)
The target here is the article's paired Theorems 1 and 2. They concern one retailer and one manufacturer, and their conclusion is about the order quantity the retailer chooses. The model does not ask the retailer to choose the selling price, nor does it compare realized profits for one particular demand outcome. The value of the result lies in ruling out two whole classes of pricing and return terms before considering how to divide the gains from a coordinated channel. Pasternack (1985), pp. 169–171
A manufacturer produces at unit cost and charges the retailer a wholesale price . The retailer orders units before observing demand , then sells at a fixed retail price . Unsold units have salvage value . A return policy gives the retailer a credit for a fraction of the order: permits no returns and permits returns of every leftover unit. The retailer incurs goodwill cost for each unmet unit of demand; the manufacturer bears the additional cost , and is the total goodwill cost. The paper assumes and . Pasternack (1985), pp. 169–170, (1)–(2)
Demand is described by a density on the nonnegative reals and distribution function . From the same order and demand outcome, the paper computes three expected profits: for an integrated company store, for the independent retailer, and for the manufacturer. Their definitions are equations (3), (6) and (8). An optimal order maximizes the relevant expected profit over nonnegative . The paper calls the channel coordinated when the retailer chooses a system-optimal order, as if the manufacturer operated the store directly. The formal model compares the sets of all such optimal orders, so it also handles a distribution whose CDF is flat over an interval. Pasternack (1985), pp. 170–171, (3), (6), (8)–(10)
The integrated company's optimal-order equation (5) supplies the benchmark:
The retailer's optimal-order equation (7) includes both and . Substituting the integrated benchmark gives equation (10), the common comparison used for the two endpoint policies. The first three milestones formalize these conditions, including existence of an integrated optimum. The last two milestones record the separate calculations in the appendix for full-credit returns and no returns. Pasternack (1985), pp. 170–171, 175
The mission goal combines Theorems 1 and 2 as the article does immediately after stating them. With or with , every system-optimal order fails to be retailer-optimal:
The disjointness claim is read separately for each endpoint policy. It says more than merely finding one order on which the firms disagree: neither endpoint policy can induce the retailer to choose a system optimum. Pasternack (1985), Theorems 1–2 and following paragraph, p. 171
The result separates a policy that reimburses all unsold stock at full wholesale price from one that offers no return option. Both may be simple to administer, but neither aligns the retailer's stocking choice with the integrated company's choice under the article's cost ordering. The result makes the paper's subsequent search for partial-credit terms substantive: the coordinating policy lies away from these two endpoints. It does not say that either endpoint always gives a loss, or that a retailer cannot make a profit. The claim concerns the order that maximizes expected channel profit. Pasternack (1985), pp. 171–172
The known result is proved in the article, but its definitions and theorem statements have not been machine-checked as part of this mission. Formalization gives a reusable account of the paper's piecewise expected profits, feasible order quantities and return fraction, and makes explicit the conditions under which the endpoint conclusions hold. Related proved platform statements include Snyder and Shen's wholesale coordination and wholesale under-ordering. They are not imported: their contract data require , while Pasternack's retailer has no separate own unit cost and the article does not require nonnegative salvage value.
The claim is sensitive to the demand model. If demand is deterministic, its CDF has a jump, and an order exactly equal to demand can be optimal under both the integrated profit and unlimited full-credit returns. The paper assumes a demand density; continuity of the CDF is therefore material to Theorem 1. Flat parts of a continuous CDF pose a different issue: a theorem identifying just one optimum would lose some orders, so the milestone conditions identify whole sets of maximizers. Pasternack (1985), p. 170, definition of and (4)–(7)
The no-return case also depends on the meaning of the manufacturer's additional goodwill cost. The paper names as a cost but does not print a separate nonnegativity inequality. If it were allowed to be negative, the appendix's contradiction with could disappear. The formalization states , along with , and identifies this convention openly. Pasternack (1985), pp. 170, 175
Lean uses a probability measure supported on with finite first moment in place of a named density . The theorems assume that has no atoms, giving the continuous CDF needed by the paper's first order conditions. The profit definitions retain the piecewise formulas of (3), (6) and (8), including the thresholds and . Adjacent pieces agree at their boundaries. The fixed retail price and the fraction match the paper's setting. The cost ordering is split between fixed costs and an admissible policy, because the theorem compares particular policy choices.
Only is feasible. An optimal-order predicate includes this membership as well as maximality, and coordination compares complete argmax sets. The goal explicitly asserts that a system optimum exists, preventing a vacuous conclusion about orders when there are none. At the retailer profit is independent of , so the goal quantifies over every credit without imposing an unused bound on it. The denominator is positive under and . Contributions that develop the optimal-order characterizations, the substitution identity, or the endpoint contradictions within these conventions directly support the goal.
A manufacturer of a perishable good (newspapers, magazines, bread, seasonal fashion, printed books) sells through a retailer who must commit to an order before demand is known. Unsold units lose most of their value; unmet demand costs goodwill. When the retailer alone bears the risk of leftovers, it orders less than an integrated firm would, and the channel as a whole earns less. This inefficiency is the double marginalization of the newsvendor problem, and return policies, under which the manufacturer buys back unsold units, are the instrument publishers and other suppliers of perishable goods actually use against it.
Barry Alan Pasternack's paper Optimal Pricing and Return Policies for Perishable Commodities (Marketing Science, 1985) was the first to show, in a single-period newsvendor model, which return policies restore the integrated firm's order quantity. It became the starting point of the literature on supply-chain contracts: buy-back contracts are now a textbook chapter (Cachon 2003; Snyder and Shen, Fundamentals of Supply Chain Theory), and the paper's result is the standard example of a contract that coordinates a channel while letting the two firms split the profit.
A manufacturer produces at unit cost . A retailer sells at the fixed retail price . Leftover units are salvaged at per unit. Each unit of unmet demand costs the retailer a goodwill penalty and the manufacturer an additional penalty ; write . The data satisfy .
The manufacturer chooses a policy : the retailer pays per unit ordered and may return up to the fraction of its order for a credit per unit. The paper assumes
Demand is random with distribution function . Three expected profits are defined as functions of the order : , equation (3), the profit of a company store in which the manufacturer sells directly; , equation (6), the independent retailer's profit under the policy; and , equation (8), the manufacturer's profit when the retailer orders . An optimal order for a profit function is a maximizing it over . The policy coordinates the channel when the retailer's optimal orders are exactly the company store's optimal orders: the decentralized channel then produces the integrated firm's quantity.
The Lean development uses the same letters: Costs carries ; Costs.Admissible K c1 c2 R is (1)–(2) with ; EPT, EPR, EPM are (3), (6), (8); IsOptimalOrder and Coordinates are the two notions just defined; is cdf D for a demand law D.
A policy which allows for unlimited returns at partial credit will be system optimal for appropriately chosen values of and . Precisely, for every price with there is a credit with
such that the policy coordinates the channel for every continuous demand distribution on with finite mean. The credit is chosen before, and independently of, the demand law.
The result. Theorem 3 says that a buy-back contract with full returns at a partial credit aligns the retailer's incentives with the channel's, and that the coordinating credit depends only on costs. The second point carries the paper's practical conclusion: a manufacturer selling one product to many retailers with different demand distributions can post one price and one return credit and still have every retailer order its system-optimal quantity. The one-parameter family of coordinating pairs then splits the channel profit between the firms. The companion mission (Optimal Pricing and Return Policies for Perishable Commodities II) formalizes the negative results, Theorems 1 and 2: neither full credit with unlimited returns nor a no-returns policy coordinates.
Formalizing it. The paper's proofs are first-order conditions and a short algebraic argument. A machine-checked version adds three things. It makes the analytic content explicit: existence of the system optimum, global optimality of the first-order conditions for an arbitrary atomless demand law, and the quantifier structure "one credit for all demand laws". It repairs a gap: the printed argument for establishes only , which suffices only when , although the claim holds for all . And it gives a reusable newsvendor layer with returns. Related results are proved on Prove2Me in a different model: Snyder–Shen's SupplyChainTheory.buyback_coordinates (Theorem 14.4) and SupplyChainTheory.buyback_profit_identities. They are not referenced here, because their contract data require a retailer cost , which excludes Pasternack's retailer (no own cost), and because they fix the buy-back price and derive the wholesale price, with no range claim.
The algebraic core, milestone 5, is short. The work sits in the analytic milestones. Differentiating under the integral sign in (3) and (6) needs the integrands' piecewise structure and the absence of atoms; the global-maximum claim needs concavity of the expected profits on , including the boundary . Coordination is a statement about sets of maximizers, not about one first-order condition: when is flat at the critical fractile, the optimal orders form an interval, and showing that the retailer's maximizers coincide with the system's requires the monotonicity of the retailer's marginal profit, strict where increases. The naive reading "both first-order conditions hold at " proves one inclusion only.
Demand is a probability measure D on with D (Iio 0) = 0 and finite mean (IsDemand), and is cdf D. The paper's density is the hypothesis NullSingletonClass D (no atoms), imposed on each theorem that uses it. The expected profits are Lean integrals of the paper's piecewise integrands, written with if. The goodwill costs satisfy , implicit in the paper. is a fraction in . Optimal orders are maximizers over that are themselves . Coordination is equality of the retailer's and the company store's sets of optimal orders. The denominator is positive under these assumptions, so no division is degenerate.
The goal is not the algebraic statement "there is solving (11)": that is milestone 5. A formalization of Theorem 3 must conclude Coordinates, a statement about the maximizers of the actual profit functions (3) and (6), and must place the quantifier over demand laws inside the existence of .
A complete development needs: differentiation of parametric integrals with piecewise-linear integrands, concavity of the newsvendor profit, the intermediate value theorem for continuous distribution functions, and the critical-fractile characterization. The newsvendor layer (milestones 1 and 2) is reusable for any single-period contract model. Proofs of the milestones, alternative proofs (for example via the identity under (11), which also removes the no-atoms hypothesis), and the profit formulas (12)–(14) at the coordinated optimum are all welcome.
Simulation, Monte Carlo integration and randomized algorithms consume long streams of numbers that should behave like independent uniform draws. A deterministic generator with finite state is eventually periodic, so its period is the first figure of merit: a stream cannot be longer than its cycle. G. Marsaglia and A. Zaman, A new class of random number generators (Ann. Appl. Probab. 1 (1991)), introduced the add-with-carry and subtract-with-borrow generators. They keep machine words plus one carry bit, use only additions or subtractions of words, and still reach periods such as when the base is near (p. 465). The paper's mechanism for this is number-theoretic: the generated digits are the base- digits of a fraction written backwards, so the period of the generator is the period of a repeating base- expansion, i.e. the multiplicative order of modulo .
Generators of this family were used widely in the following decades (Lüscher's RANLUX generator in lattice field theory is built on subtract-with-borrow), and later work showed that they are equivalent to linear congruential generators with modulus (Tezuka, L'Ecuyer and Couture 1993). This mission treats the add-with-carry generator. A companion mission treats subtract-with-borrow.
Fix a base and two lags and with . A state (or seed vector) is
where each is a base- digit and is the carry bit. The digit is the oldest one. The add-with-carry map (p. 465) is
and the generated sequence of a seed is . Reading off the last digit of each state gives a digit stream obeying , with the carry updated at each step. The two trivial seeds are and . The modulus of the generator is
For and , the -th base- digit of after the point is . The order is the least with , and is a primitive root of a prime when .
Let be prime, and let be any seed other than the two trivial seeds. Then is a periodic point of and
This is the italic summary of p. 472 ("whatever the seed vector, except for the two trivial seeds, the add-with-carry and subtract-with-borrow sequences become periodic after a few iterations of the generating function, and the periods are the order of the base for the appropriate modulus"), with the claim of §4.2 (p. 467) and its proof (p. 468). The goal fixes no particular , , and does not assume that is a primitive root. When it is, the period is , the value announced in §2.
The result. The goal reduces the period of the generator, a property of a dynamical system on states, to the multiplicative order of one residue. That is the computation the paper performs in §6 to certify its recommended generators, and it is how one chooses : search for primes and check the order of . Milestone 5 is stronger than the goal. It needs no primality and identifies the whole output stream, not only its period, with the expansion of a fraction. That identification is what later work used to relate carry generators to linear congruential generators with modulus . Milestone 6 answers the paper's "periodic seed" puzzle: it says exactly which seeds lie on their own cycle.
Formalizing it. The results are proved in the paper, the general §4.1 facts are classical, and the method-specific rules of §4.5 (milestone 6) are stated there without proof. None of it is machine-checked on Prove2Me or, to our knowledge, in Mathlib, which has orderOf and ZMod but no theory of base- expansions of rationals. The mission produces a checked link from a concrete integer recurrence to modular arithmetic. That link can serve as a template for other carry-based and lagged generators.
The obvious argument says the digit recurrence is linear, so the period divides something like the order of a companion matrix. This fails because of the carry: is not linear over , and the state does not live in a group in any evident way. The link to the order of modulo goes through an identity between a finite digit string and a fraction (milestone 5). Stating it with exact indices is itself delicate: the digits run in reverse order, the fraction depends on the string's length, and the trivial seed , whose digits are those of , has to be excluded.
A second difficulty is the preperiod. A seed need not lie on its own cycle (p. 472), so the period must be measured after the transient. Bounding that transient by (milestone 4) and characterising the periodic seeds (milestone 6) are separate combinatorial facts about the carry. The paper states the second without proof.
CarryRNG.AWC. Lags are a structure Lags with fields r, s and proofs of and . A state is a structure with digits x : Fin r → Fin b and carry c : Fin 2, so holds by typing. Lean index is the paper's : x 0 is (the digit the step drops), and the partner digit is index . step is defined directly from the two-case formula of p. 465, not through . The digit stream out is one-based: the seed digits for , then the last digit of . digit b m k j is the exact integer formula above, used for only.Function.minimalPeriod. It is at non-periodic points, so the goal's equation with the positive also asserts periodicity. A divisibility or inequality form would be vacuous and is not used. For digit sequences, "period " is stated as " is a period iff ".minimalPeriod along an orbit. Proofs of any milestone are welcome, as are primality and order certificates for milestone 8 as separate lemmas.A single processor receives jobs over time, each with a known amount of work, and may interrupt a job at any moment to work on another. Which rule should decide what to process? For the number of jobs waiting or in service, the answer is the Shortest Remaining Processing Time (SRPT) rule: at every moment, work on the job in system that is closest to completion. Its optimality is pathwise. It holds for every sequence of arrival times and processing times, not on average under a probabilistic model, so it applies to any single-server queue whatever the distribution of interarrival and processing times. By Little's law it also minimizes mean response time, which is why SRPT and its approximations are the reference policy in the analysis of size-based scheduling for web servers and networks (Harchol-Balter et al., 2003).
Timeline:
An arrival stream is a sequence of pairs , , of real numbers: is the arrival time and the processing time of job . A schedule is a family of measurable functions , with meaning that the processor works on job at time . No job is processed before it arrives ( for ), and the processor works on at most one job at a time.
The remaining processing time of job at time is
and its completion time is
or if the job never receives its processing time. The set of jobs in system at time is , and is its cardinality.
A schedule follows SRPT if, at every time with , the processor works on a job with for all . Ties may be broken arbitrarily.
For every locally finite arrival stream, every SRPT schedule and every schedule of the same stream,
The goal has no constants and no distributional assumptions. It is the statement quoted on p. 687 and concluded at the end of the PROOF on p. 689.
All five come from the PROOF on p. 689. They compare an original schedule with a revised schedule .
The result. The goal is a sample-path dominance. Each consequence for averages follows by taking expectations or time averages: SRPT minimizes the mean number in system and, through Little's law (Little, 1961), the mean response time in every G/G/1 queue with known job sizes. It makes SRPT the benchmark against which other preemptive disciplines, size-based or size-oblivious, are measured.
Formalizing it. The statement has been proved on paper since 1968 and given a complete proof in 1978. No machine-checked proof of it is known to this mission. A formalization contributes three things: a precise continuous-time model of preemptive single-server schedules with measurable service indicators and possibly infinite completion times; checked proofs of the exchange steps of the 1968 letter, each of which needs a hypothesis the letter leaves implicit; and a checked proof of the pathwise optimality theorem itself.
The letter argues that a non-SRPT schedule contains an interval on which SRPT is violated, and that swapping service on that interval improves the schedule. The first step fails for measurable schedules. A schedule can violate SRPT on a set of positive measure that contains no interval (a fat Cantor set), or only on a null set. So the "interval of non-SRPT behaviour" need not exist, and a single interchange does not turn an arbitrary schedule into an SRPT one. Repeating interchanges also gives no obvious termination or limit argument, because the improvements can accumulate at a point. The goal therefore cannot be reached by formalizing the letter's induction literally. The milestones are the letter's local claims, which are true under the hypotheses stated with them. The goal needs an argument that compares an SRPT schedule with an arbitrary one at every time directly.
All declarations live in the namespace SchrageSRPT.Opt. Jobs are indexed by ℕ from , and times, arrival times and processing times are real. A schedule is δ : ℕ → ℝ → ℝ with values in , each δ n measurable, before arrival, and at most one job served at a time. The letter's is stated as "two served jobs are equal", not as a series. Assumption (I) of the letter (the arrival stream does not depend on the discipline) is encoded by comparing schedules of one fixed stream. Assumption (II) (preemption wastes no work) is the formula for , which has no setup term. Completion times take values in WithTop ℝ, with for a job that never completes. A job is in system on . is Set.ncard, and the goal assumes local finiteness ( is finite for every ) so that it is a genuine count. SRPT is the verbal rule of p. 687, required at every .
Two encodings would trivialize the goal, and both are ruled out. The displayed condition of p. 688 (" for implies ") is satisfied by the schedule that never works, so it is not used as the definition of SRPT. The competitor class is every schedule of the stream: it is not restricted to work-conserving schedules, to finitely many jobs, or to schedules in which every job completes.
The milestones add disclosed hypotheses that the letter uses silently:
The counting milestone uses the half-open interval, since the letter's closed right endpoint is a slip.
A complete development needs:
All of this is reusable for other continuous-time preemptive scheduling results. Contributions are welcome in particular for this infrastructure, for proofs of the milestones, and for a complete proof of the goal.
Weighted voting bodies often combine a few large blocs with a mass of small, unorganized voters: shareholders' meetings with a handful of large holders and a dispersed float, legislatures with party blocs and independents. The Shapley value measures each participant's voting power as the probability of being pivotal — the one whose arrival first turns a losing coalition into a winning one — when participants arrive in a uniformly random order. For many small voters this computation becomes a combinatorial problem whose size grows with the number of voters.
Milnor and Shapley (RAND RM-2649, 1961; revised as Mathematics of Operations Research 3(4), 1978) replaced the small voters by a continuum, the ocean, and obtained explicit formulas for the power of the large voters. The memorandum is the second of a RAND series on values of large games; the first (L. S. Shapley and N. Z. Shapiro, Values of Large Games, I: A Limit Theorem, RM-2648, 1960) proves the limit theorem for finite games with many small players on which the oceanic model rests. This mission formalizes the part of the memorandum that leads to explicit closed forms for the values of interior oceanic games (§2, §4, §5).
There are major players with weights , and . The ocean is the interval with Lebesgue measure, carrying total weight . In the oceanic game with quota , a coalition wins when the weight of its major players plus times its share of the ocean is at least .
The random order is modelled by a uniform random point of the cube : major player is inserted into the ocean at position , and is the set of major players placed before position . Player is pivotal when
and the value of player is the probability of (2.4), i.e. the volume of the set where it holds. The combined value of the ocean is (2.5).
With the quota as a variable, has values , , and the pivot location is a random, nondecreasing, piecewise linear function of with expectation . Adding a major player of weight gives the game .
The game is interior when
that is, the ocean alone wins and the major players together lose. With , define for , the analogous product over for , and the integers , , i.e.
In an interior game, with ,
Both identities are part of the goal. The values do not depend on within the interior range.
Further items, not milestones: the Corollary (5.5), Theorem 3 (averaged over all quotas, each value equals the player's share of the total weight), Theorem 4 (small players behave like ocean), and (5.8) with its footnote ( is the nearest integer to and counts derangements).
Theorem 6 turns the voting power of the large blocs, a priori a probability over a continuum of orderings, into a finite multilinear polynomial in the ratios . Table 1 of the memorandum lists the cases , and the theorem gives every . Its coefficients are signed derangement numbers. The Corollary (5.5) states that a major player's value per vote equals the ocean's value per vote in the game without that player.
The memorandum's arguments are short and partly heuristic: "E commutes with the derivative", the disjointness of the pivot sets is "obvious", and the induction for Theorem 6 relies on the symmetry of the value in the major players, which is never stated. A formalization makes each of these steps precise, including the measure-zero exceptions and the quota ranges. To our knowledge none of these results has a machine-checked proof; Mathlib has the Lebesgue measure on cubes, interval integrals and derangement numbers, but no game-theoretic value with a continuum of players.
The values are volumes of regions of cut out by inequalities whose shape depends on the order of the coordinates, so a direct computation splits into order cells, with the quota entering each. The paper's route avoids this by passing through the random function , Theorem 2 and the Lemma; that route needs differentiation under the integral sign for a function that is only piecewise linear in , with kinks at random locations, and an exact bookkeeping of the interval of integration when the quota approaches the ends of . Theorem 6 is then an induction on that uses Theorem 5 for every player in turn, so it also needs the invariance of under a relabelling of the major players.
Fin m ( is allowed; then ). The probability of an event is the Lebesgue volume of its intersection with ; no probability space is built.HasDerivAt), and for the Lemma, as on p. 14.Fin.snoc as index Fin.last m.A complete development needs: measurability of the pivot sets and of in , the structure of as a piecewise linear function of , differentiation of , and invariance of the values under permutations of the major players. The pivot-set and infrastructure is reusable for the companion mission on limits of finite weighted majority games. Contributions of any of the milestones, of the symmetry lemma, and of the non-milestone items are welcome.
An isometric model of a graph assigns vectors to vertices so that vector distances reproduce shortest-path distances exactly. The choice of norm matters: a graph that needs many Euclidean coordinates may admit a smaller realization under a different norm. Linial, London, and Rabinovich used this freedom to study the dimension of graph metrics and related geometric questions in their 1995 paper on graph embeddings (Linial–London–Rabinovich, 1995). The complete graph is the first calibration point for the invariant. Every two distinct vertices are equally far apart, so the question becomes how many pairwise equidistant points an arbitrary real normed space of dimension can contain.
The answer is a sharp base-two logarithm. It separates the role of dimension from the particular shape of a norm's unit ball. In particular, a cube equipped with the supremum norm supplies many equidistant vertices, while no norm in the same dimension can accommodate more. Establishing both directions gives a reference case for more complicated graph metrics in the paper's Section 5.
A finite pseudometric space has a finite point set and a distance that is symmetric, vanishes on the diagonal, and satisfies the triangle inequality. Distinct points may have distance zero, as the paper explicitly allows. A norm on is nonnegative, vanishes only at the zero vector, is absolutely homogeneous, and satisfies the triangle inequality. It induces the distance between vectors.
An isometric embedding of into a -dimensional normed space is a map with for every pair. The isometric dimension is the least for which such a norm and map exist. The norm may depend on and ; it is part of the realization rather than a fixed background choice. Lemma 5.1 of the paper states that every -point metric space has an isometric realization in , so this least dimension is taken over a nonempty set (Linial–London–Rabinovich, p. 229).
The complete graph has an edge between every pair of distinct vertices. Its shortest-path distance is zero from a vertex to itself and one between distinct vertices. An isometric realization of is therefore a collection of points whose pairwise distances are exactly one. The paper's Section 5 treats connected graphs, so this mission takes . Its convention is that every logarithm has base two.
The foundational target is the paper's finite embedding statement:
It establishes the domain on which the least-dimension definition has its intended meaning. The remaining milestones isolate the geometric assertions used for complete graphs: a difference-body inclusion, separation of the interiors of certain convex-hull translates, and a cardinality bound for equilateral points in .
The goal is Proposition 5.4 (Linial–London–Rabinovich, p. 231):
The lower bound applies to every real norm on . The upper bound has the more specific target . Both inequalities, including and dimension zero, are part of the mission.
The equation determines the optimal dimension for an equilateral finite metric space when the norm is unrestricted. It also bounds the size of an equilateral set in every -dimensional real normed space by , with equality attainable by vertices of a binary cube under the supremum norm. For graph metrics, it gives a precise baseline against which dimension bounds for trees, cubes, and other connected graphs can be compared. The surrounding section of the paper uses the same geometric vocabulary for those other families (Linial–London–Rabinovich, Section 5).
The mathematical result is proved in the 1995 paper. This mission asks for machine-checked Lean proofs of the specified statements. The local declarations presently encode open proof obligations; compilation checks their types and imports, but does not establish the theorems. A completed development would provide a reusable interface for finite isometric dimension and for equilateral configurations under arbitrary finite-dimensional norms.
The easy direction uses points of a binary cube. The difficult direction must hold uniformly over every possible norm, whose unit ball need not be round or smooth. A direct coordinate count cannot assume that vectors have bounded entries in a prescribed basis. The paper formulates its argument through the convex hull of an equilateral configuration and a comparison of translated sets (Linial–London–Rabinovich, p. 231). Its printed volume line also leaves a degenerate case: if that convex hull has zero volume in the ambient space, cancellation of gives no numerical bound. A complete formal proof must account for such configurations without weakening the theorem to full-dimensional sets.
The Lean representation of is the function space Fin d → ℝ. A norm is an explicit function with all norm axioms, including definiteness and absolute homogeneity. Isometric dimension takes the infimum over dimensions admitting such a norm and an exact distance-preserving map. The complete graph is Mathlib's ⊤ : SimpleGraph (Fin n); its graph distance is converted to a real number. This distance is the discrete zero-or-one metric. The lower bound quantifies over every explicit norm. The cube milestone uses the supremum norm on finite real coordinate vectors. Convex hulls and interiors use the standard topology of this finite-dimensional vector space, which every norm induces.
The formal goal assumes , matching the paper's connected-graph convention; remains included, with dimension zero. The logarithmic expression is Nat.clog 2 n, the ceiling of the base-two logarithm, rather than a floor or a real logarithm. The source uses no unspecified asymptotic constant in Proposition 5.4 or its listed milestones. The empty point space is allowed in the general finite embedding lemma; its pairwise claim is vacuous, while the nonempty cases carry the intended content. The dimension definition is only used for realizable finite distances, so a totalized infimum's value on an unrealizable function has no role in the target.
The exact norm axioms and exact distance equality prevent shortcuts through seminorms, truncated distances, or a weaker distortion bound. The cardinality theorem retains lower-dimensional affine configurations; assuming positive ambient volume would discard part of the result. A complete development needs finite pseudometric geometry, the supremum norm, convex hulls and interiors, and a dimension-sensitive measure argument. Those components are useful beyond this graph. The paper's independent results on degrees, trees, cubes, and other graph families, as well as algorithmic running-time claims elsewhere in the article, are outside this mission.
In 1975 P. Brucker, J. K. Lenstra and A. H. G. Rinnooy Kan classified a large part of deterministic machine scheduling by computational complexity, using the then new theory of NP-completeness of Cook and Karp. Their report, Complexity of Machine Scheduling Problems (Mathematisch Centrum, Amsterdam, 1975; published in Annals of Discrete Mathematics 1, 1977), gives for many problems either a polynomial algorithm or a polynomial reduction from a known NP-complete problem. It drew the boundary between easy and hard scheduling problems that later surveys and the standard three-field classification build on.
This mission covers four reductions of the report's Theorem 4 that concern shops with several machines. A flow shop processes every job on machines in this order; a job shop lets each job follow its own route. For two machines and no further constraints, the flow shop is solved by Johnson's rule (Johnson, 1954) and the job shop with at most two operations per job by Jackson's extension of it (1956). The four reductions show that these positive results stop exactly where one more feature is added: one job with a nonzero release date, tree-shaped precedence constraints, a third operation per job, or a third machine.
A general shop instance has jobs and machines . Job consists of operations; its -th operation runs on machine for time units, and the tuple is the job's machine order (a machine may occur more than once). Each job has a release date , and some pairs of jobs carry a precedence constraint .
A schedule gives every operation a start time. It is feasible if no operation of starts before ; the operations of each job run in the order , each after the previous one completes; two operations on the same machine never overlap; and implies , where is the completion time of and the starting time of . The makespan is .
In the report's notation , means a flow shop and a job shop; may contain (only the last job has a release date), tree (the precedence graph is a branching: no directed cycle, and either every indegree or every outdegree is at most one) and (at most operations per job). The recognition version of a problem asks, for an instance and a number , whether a feasible schedule with exists.
KNAPSACK asks, for positive integers and , whether some has . A problem is reducible to () if every instance of can be transformed in polynomial time into an instance of with the same answer.
Each part is a polynomial-time many-one reduction between languages of binary strings. The other six parts of Theorem 4 (single-machine problems) belong to other missions of this series.
For positive with , and for each of the paper's four constructions with its threshold ,
with for (i), for (j), for (g) and for (h). The milestones are stated directly about the printed constructions, in the order (i), (j), (g), (h) of the report.
With the NP-completeness of KNAPSACK (Karp, 1972), the goal makes the four problems NP-complete. As the report notes, (i) and (j) together with the elementary reductions of its Theorem 1 make the general job shop NP-complete for every fixed . Parts (g) and (h) show that Johnson's two-machine algorithm admits neither release dates nor precedence constraints in general. Because KNAPSACK can be solved in pseudo-polynomial time, these results establish NP-hardness in the ordinary sense only; strong NP-hardness of some of these problems came later (Garey, Johnson and Sethi, 1976, for the three-machine flow shop).
The results are proved in the report; no machine-checked proof of any of them is known to exist. A formalization adds explicit constructions and complete equivalence proofs where the report is brief: in (h) it proves one inequality and states that the rest "is analogous to that of reduction (g)", and the forward directions are given by figures. It also produces a reusable formal model of general shops with integral start times, release dates, precedence and repeated machines.
Polynomial-time computability of the constructions is routine in principle but laborious in Cook's Turing-machine model, which is the setting of the goal: binary arithmetic for , and , and parsing of the KNAPSACK code.
The mathematical difficulty is the reverse direction of each equivalence. The report's arguments are phrased in terms of "a processing order on " and treat the jobs before and after an extra job as two blocks. A formal proof must derive such an order from arbitrary start times and must handle every interleaving, including idle time and the case where the extra job's operations do not fit the printed pattern. In (j) the printed bound for the case contains a minimum of two quantities whose justification is left to the reader. In (h) the printed case uses , so the positivity of the data matters, and the remaining cases are only said to be analogous to (g).
Jobs are Fin n and machines Fin m, both 0-based. A job's operations form a list of (machine, processing time) pairs, so machine orders may repeat machines, as in (i) does. Start times are natural numbers. The report computes schedules from processing orders on integer data, the makespan is a regular criterion, and release dates and precedence survive shifting operations left, so integral start times lose no value. is stated as for every ; no maximum over an empty set is formed. Precedence is between jobs: every operation of starts no earlier than . A branching is an acyclic precedence graph in which every indegree is at most one or every outdegree is at most one; the report's "either … or" is read for the whole graph. Job-shop classes require at least one operation per job. A flow-shop job has exactly the operations , with times allowed to be zero.
The following readings of the report are made explicit. "Reducible" is Karp reducibility, CookPvsNP.PolyReducible from the published definitions CookPvsNP_defs. The languages are over the four-letter alphabet with binary numbers of the published definition ProjSchedTW.Complexity.Encoding. Its subsetSumLang allows zero sizes, while the report's KNAPSACK is over positive integers, so KNAPSACK is defined locally with positivity in the language. "We may assume that " becomes a hypothesis of every equivalence; the goal's reduction must still handle the other inputs. The printed "value " of the forward directions is read as "", as Section 2 defines the recognition version. The remark that (h) is analogous to (g) becomes the full equivalence for (h). An instance outside the problem's class is not in its language. NP-membership is not part of the goal.
The formal two-stage flow-shop models of Johnson's paper (JohnsonFlowShop.TwoStage.IsFeasible) and the job-shop model of Jansen, Solis-Oba and Sviridenko (JobShopLTAS.Core.Instance) use real start times and have neither release dates nor precedence. They were consulted, but the model here is local.
Ruled out as trivializing: a goal without the polynomial-time condition (the bare equivalence of yes-instances), a target language that accepts instances outside the class, and equivalences about some instance rather than the printed construction.
Contributions are welcome on any milestone, on a general lemma that turns a feasible schedule into a processing order per machine, and on polynomial-time computability of list arithmetic in the Turing-machine model, which every reduction of this series needs.
Discounted Markov decision problems are solved in practice by two classical schemes. Value iteration (successive approximations) is cheap per step but contracts the error only by the discount factor per step, which is slow when is close to . Policy iteration (Howard, 1960) converges in few steps, but each step solves a linear system for the value of the current policy. Puterman and Brumelle (Mathematics of Operations Research, 1979) showed that policy iteration is Newton's method applied to the optimality equation.
Puterman and Shin (Management Science 24, 1978) interpolated between the two schemes: replace the exact policy evaluation by steps of successive approximation. This is modified policy iteration of order . For it is value iteration; as it approaches policy iteration. The paper proves that every order converges and bounds its rate. The scheme remains a standard algorithm in dynamic programming (Puterman, Markov Decision Processes, Wiley 1994, §6.5), and it appears in reinforcement learning as "optimistic" or "generalized" policy iteration.
Timeline. Howard (1960): policy iteration for finite problems. Puterman–Brumelle (1979, circulated earlier): policy iteration as Newton–Kantorovich iteration, and the support inequality for the optimality operator. van Nunen (1976) and van Nunen–Wessels: convergence of related value-oriented methods in a different framework. Puterman–Shin (1978): convergence of modified policy iteration of every order from a starting point with , and the rate bound formalized here.
is a set of states with a -algebra. A family of policies is given. Each is a transition operator: a Markov kernel assigning to each state a probability distribution on . Each policy also has a one-period reward , and the rewards are uniformly bounded: . The discount rate satisfies .
is the Banach space of bounded measurable functions with . A kernel acts on by . For linear on , .
The optimality equation is
The paper assumes throughout that the maximum in (1) is attained for every , by a single policy at every state.
For , the truncated Neumann series is . Modified policy iteration of order runs the recursion
where attains the maximum in (1) at . A solution of exists and is unique. denotes a policy attaining the maximum at . The proofs also use the operators and the set .
If and , then for every
The mission also contains four further theorems that are not milestones: Corollary 2 (asymptotic rate at most when ), Proposition 2 (monotonicity in the order ), the representation (6) , and Proposition 1 (policy iteration as Newton's method).
The result. Bound (8) gives two guarantees. Every order of modified policy iteration converges at least as fast as value iteration, with factor per step. Once the improving policies stabilize near an optimal one, the factor approaches , the factor of value-iteration steps. This justifies spending cheap evaluation sweeps per policy improvement instead of solving a linear system. It also underlies the analysis of the many later variants: action elimination, asynchronous and approximate versions, and optimistic policy iteration in reinforcement learning.
Formalizing it. The theorems are proved on paper. As far as the platform's library shows, none of them is machine-checked: existing items cover value iteration and exact policy iteration for finite state spaces. This mission formalizes the whole chain on general measurable state spaces with Markov kernels, including the support inequality and the comparison operators . Corollary 2 is stated as an upper bound only, because the equality printed on the page fails in degenerate runs (see the item's note).
The obvious route to a rate is the contraction argument for value iteration: is monotone and a -contraction, so its iterates converge geometrically. For that argument does not transfer to the map . The truncated series is taken for the policy chosen at the current point, so the map changes with , and it is not monotone in general. The van der Wal–van Nunen example on p. 1133 of the paper shows that iterates of a higher order need not dominate those of a lower order from the same start. Moreover, without the condition the iterates need not even increase. A rate for (4) is therefore not a corollary of a fixed-point theorem for a single operator.
Formally, a second layer of difficulty is the setting itself. Everything happens in the space of bounded measurable functions on a general measurable space. So every operator applied to an iterate must be shown to preserve boundedness and measurability, and the maxima over policies are suprema over an arbitrary index set.
The Lean development (namespace ModPolicyIter.Conv) represents:
P i : Kernel S S with a measurable reward c i, ;IsBM (measurable and bounded), with supNorm v = ⨆ s, |v s|;The standing assumptions of §2 are carried by the model fields; items using a maximizer assume either global attainment (MaxAttained) or an explicit maximizing policy. A run of (4) is a sequence of functions paired with a sequence of policies, each policy a maximizer at the current iterate. Only is assumed; that later iterates lie in is part of the proofs.
Deviations from the page, all disclosed in the items:
The goal must not be trivialized by assuming , the support inequality, the sandwich of Corollary 1, or anything about . These are milestones to be proved, and none of them is a hypothesis of the goal.
Reusable infrastructure includes Markov kernels as operators on bounded measurable functions (positivity, , measurability of ), completeness of , and the Banach fixed point theorem on . The first of these serves any discounted dynamic-programming mission on general state spaces. Contributions of any milestone, or of helper lemmas about these operators, are welcome.
Many problems in statistics and engineering ask for the level at which an unknown function takes a prescribed value : the dose at which a fraction of subjects respond, the setting at which a noisy device reaches a target output, the -quantile of a distribution that can only be probed by yes/no experiments. When the function can only be observed through noisy measurements, classical root-finding does not apply. Robbins and Monro (Ann. Math. Statist. 22 (1951) 400–407) proposed a recursive procedure that uses one noisy observation per step and proved that it converges in mean square. The paper started the field of stochastic approximation, which today underlies stochastic gradient descent, temporal-difference learning and adaptive control.
Timeline. Robbins and Monro (1951) prove mean-square convergence for bounded responses under conditions (5′) or (33)–(35). Kiefer and Wolfowitz (1952) adapt the scheme to finding a maximum. Blum (1954) proves almost-sure convergence under weaker moment conditions. Dvoretzky (1956) gives a general convergence theorem covering both schemes. Later work (Robbins and Siegmund, 1971; Ljung, 1977; Kushner and Clark, 1978; Benaïm, 1999) develops the supermartingale and ODE methods.
To each real level corresponds a random response with distribution function , and the regression function is
The responses are bounded: there is with for all (condition (4)). Fix constants and positive step sizes . The Robbins–Monro process starts at an arbitrary constant and sets
so is a fresh response observed at the current level . The quantity of interest is the mean squared error .
A sequence is of type if
is the standard example. The proof also uses , and .
If is of type , (4) holds, and is nondecreasing with and , then, whatever ,
Theorem 1 (p. 404: the same conclusion under (5′), for and for ); convergence in probability under the hypotheses of Theorem 2 (p. 401); the quantile estimator of §4, (48); and (30), that gives a sequence of type .
Theorem 2 is the first convergence theorem for a recursive root-finding procedure under noise. It shows that a procedure using no knowledge of or of the noise distribution, beyond a monotone crossing and a positive slope at the root, is consistent. Section 4 turns it into a distribution-free consistent estimator of a quantile from response/nonresponse data, the up-and-down designs of bioassay and sensitivity testing. Its step-size conditions, with a divergence condition, remain the standard conditions for stochastic gradient methods.
The theorem has been proved since 1951 and strengthened many times. As far as is known it has no machine-checked proof, and Mathlib has no stochastic approximation theory. Formalizing it requires conditional laws given by Markov kernels, integration against a composition of a measure with a kernel, and deterministic series arguments. A finished formalization would be a base for formalizing the almost-sure theorems (Blum, Robbins–Siegmund) and the ODE method.
The obvious argument fails at one step. Monotonicity of and a positive derivative at do not give a uniform positive lower bound on the slope : away from the slope can decay to , for example when is bounded, as (4) forces. So the drift towards is not uniformly strong, and the newcomer's first idea, a uniform contraction , is not available under (33)–(35). This is why the theorem needs the divergence condition (26), which is stronger than , and not only (6). On the formal side, the expectations come from integrating against the joint law of , and they need integrability bounds before any identity can be used.
Everything is in the namespace RobbinsMonroSA.Conv, over a probability space with IsProbabilityMeasure P. Indices are 0-based: Lean's x 0, a 0 are the paper's , , and Lean's bigA … n is the paper's . The committed conventions are:
Kernel ℝ ℝ with IsMarkovKernel H (each is a probability law, measurable in ).0 < C ∧ ∀ x, H x [-C, C] = 1. It is a hypothesis of every item that mentions an expectation, and it is what keeps the Bochner integrals defining , , and from defaulting to .HasDerivAt M M' θ with 0 < M'.The standing assumptions of §3, (4), (5) and (6), are hypotheses of Lemma 1, Lemma 2 and the displays of §3 whose proofs use them. In Theorems 1 and 2, (5) follows from (5′) or from (33)–(34), and (6) is part of "type ".
The goal cannot be trivialized. It mentions neither , , nor any constant, and the process must satisfy (8) for every . Without (8), would be arbitrary and the statement false; with it would be deterministic.
Contributions welcome: proofs of the milestones, reusable lemmas on integrating against μ ⊗ₘ κ, and a proof that satisfies (26).
Prediction with expert advice asks a master algorithm to combine the binary predictions of a pool of prediction algorithms, trial after trial, so that it makes few more mistakes than the best member of the pool, without any probabilistic assumption on the data. Littlestone and Warmuth's Weighted Majority Algorithm WM (Littlestone and Warmuth 1994) keeps a weight per member, predicts with the weighted vote, and multiplies the weights of the wrong members by a factor after each of its own mistakes. Its mistake bound is of order , where is the number of mistakes of the best member on the whole sequence.
That bound compares the master with a single fixed member. In many applications the member that predicts well changes over time: one algorithm is accurate for a while, then a second one, then a third. Against a shifting target of this kind, WM can do badly, because the weight of a member that was wrong for a long time has become so small that it takes many mistakes to recover it. Section 3 of the paper introduces the variant WML, which never decreases a weight that is already small relative to the total, and proves that it pays only a logarithmic cost per change of target. This was the first result of what is now called tracking the best expert; it was later refined by Herbster and Warmuth's Fixed-Share algorithm (Herbster and Warmuth 1998).
Timeline. 1989: a conference version of the paper appears at FOCS. 1994: the journal version, the source of this mission, gives Lemma 3.1 and Theorem 3.1 in their present form. 1998: Herbster and Warmuth's Tracking the Best Expert generalizes the shifting bound to other loss functions.
A run takes place over trials . In trial each member of the pool predicts , the master predicts , and the label is revealed. The predictions of the pool and the labels are arbitrary.
The master keeps weights , the weights at the beginning of trial . Let be the total weight and the total weight of the members predicting . WML has parameters and :
With this is WM. Write for the number of mistakes of the master and
which lies in for the stated parameter ranges.
Split the sequence into consecutive segments , with trials in , and let be the smallest number of mistakes any single pool member makes on . If and every initial weight is at least times the total initial weight, then
The partition is arbitrary and unknown to the algorithm; the bound holds for all partitions simultaneously.
The single-segment case, , together with the statement that the weight floor survives the run: if every initial weight is at least times the total, then
and every final weight is at least times the total final weight.
On every mistake trial, .
The result. Theorem 3.1 shows that an online algorithm with no knowledge of when or how often the best predictor changes can compete with the best sequence of predictors, at a price of mistakes per segment. The with says that a segment never costs more than its length. The bound is the template for later tracking and adaptive-regret results in online learning and for algorithms whose weights are kept bounded away from zero.
Formalizing it. The result is proved in the paper; no machine-checked proof of a shifting-target bound exists on Prove2Me or, to our knowledge, in Mathlib. This mission produces a formal model of WML in which ties are arbitrary (a run is a relation, so the bounds cover every tie-breaking rule), the per-mistake contraction, the single-sequence bound with its preserved invariant, and the segment bound. The model of trials, majority votes and mistake counts is reusable for the other algorithms of the paper.
The standard argument for WM compares the decrease of the total weight with the final weight of the best member. For a shifting target this fails twice. First, the best member of a later segment may have been wrong during all earlier segments; under WM its weight has shrunk by per mistake, and the master has to make many mistakes before that member regains influence. Second, the floor that prevents this also prevents some wrong members from being penalized, so the total weight shrinks by less on each mistake than under WM. The statement has to control both effects at once, and the per-segment accounting has to restart from whatever weights the previous segments left behind. A natural first idea, applying the single-sequence bound to each part of an arbitrary (interleaved) partition, does not work: for interleaved subsequences the inequality is false, and the theorem is about consecutive segments.
The pool is Fin n with ; trials are Fin T; binary values are Bool; weights are real, w : ℕ → Fin n → ℝ, with w t the weights at the beginning of trial , w 0 the initial and w T the final weights. A run is the relation IsWMLRun β γ x ρ w lam; it fixes positive initial weights, the majority rule with arbitrary ties, and the update, whose threshold is strict and uses the total weight at the beginning of the trial. Logarithms are natural logarithms; the base cancels in every ratio. The minimum over the pool is an infimum in ℕ over Fin n. Segments are given by monotone boundaries b : Fin (k+1) → ℕ with b 0 = 0 and b (Fin.last k) = T; empty segments are allowed and contribute .
The paper allows for the algorithm, but then the bounds read . In Lean, n / 0 = 0, so the bounds assume ; the contraction milestone holds for and is stated so. The hypothesis is kept as stated in the paper, not replaced by . A trivializing formalization, such as fixing the tie-breaking rule, dropping the strict weight test, letting the floor hypothesis be unsatisfiable, or allowing interleaved subsequences (which makes the goal false), is ruled out: a run exists for every input from every positive initial weights, and equal initial weights satisfy the floor.
Contributions welcome: proofs of the three statements, and lemmas on restricting a WML run to a block of trials, which the goal needs and which apply to any segment-wise analysis.
Minimizing the total completion time of jobs on a single machine is one of the oldest problems in scheduling theory. When every job is available at time , processing the jobs in order of nondecreasing processing time is optimal (the shortest-processing-time rule), so the problem is solved by sorting. Release dates, times before which a job may not start, change the picture. In their 1975 report Complexity of Machine Scheduling Problems (Mathematisch Centrum Report BW 43/75; journal version in Annals of Discrete Mathematics 1, 1977), Brucker, Lenstra and Rinnooy Kan used the then-new theory of NP-completeness (Cook 1971, Karp 1972) to map which classical scheduling problems are polynomially solvable and which are NP-complete. Theorem 4 of that report lists ten problems to which KNAPSACK reduces. Part (a) shows that total completion time on one machine is already hard when a single job has a nonzero release date and all weights are equal.
The result is a sharp boundary. With all release dates zero the problem is easy; with one nonzero release date it is NP-complete. It is a standard entry in the complexity classification of single-machine problems that later surveys (Lawler, Lenstra, Rinnooy Kan and Shmoys, 1993) and the scheduling-complexity databases build on.
An instance of KNAPSACK consists of positive integers and ; with , it has a solution if for some .
In the scheduling problem there are jobs and one machine. Job has a processing time , a weight and a release date , all nonnegative integers. A schedule assigns each job a starting time ; the job completes at , and no two jobs are processed at the same time. The problem written in the paper's notation is the class of instances in which every weight is and every job except the last one, , has release date . Its recognition version asks, given such an instance and an integer , whether some schedule has .
A problem is reducible to (written ) when every instance of can be transformed in polynomial time into an instance of with the same answer. The paper's construction maps (with and ) to an instance with jobs in four groups , , and , with processing times , , and , the release date , and threshold , where , , , , are explicit polynomials in , , and .
stated as CookPvsNP.PolyReducible knapsackLang sumCLangMult: a polynomial-time computable map on binary strings that sends codes of solvable KNAPSACK instances, and only those, to codes of yes-instances of the scheduling problem.
Together with the NP-completeness of KNAPSACK (Theorem 2(b), quoted from Karp), Theorem 4(a) shows that is NP-complete; with general release dates the problem is then NP-hard as well. The hardness here is in the ordinary sense: the construction is polynomial only in the multiplicity encoding (see below), and the reduction is from KNAPSACK, which has a pseudo-polynomial algorithm.
The result is proved on paper. A formalization adds a machine-checked complexity reduction whose correctness proof is a sequence of delicate counting estimates with large explicit constants; the paper closes the converse with "as is easily seen", and the forward computation and claims (C), (D) contain displayed identities that a formal proof must verify exactly. The definitions (single-machine schedules with release dates, the schedule of a processing order, the multiplicity encoding) are reusable for the other single-machine reductions of the same paper and for later classification results.
The forward direction is a direct computation. The converse is where the difficulty lies: a schedule with is arbitrary, may contain idle time, and may interleave the groups. Such a schedule must be shown to be rigid (claims (A)–(D)), and the claims are statements about every schedule, not about a convenient one. Each step compares sums of the form against with an additive slack smaller than , so the constants must be tracked exactly; an estimate that loses a single breaks the argument. Extracting the knapsack subset at the end requires recognizing which jobs fill and why their extra lengths sum to exactly .
For the goal, the polynomiality of the reduction is not automatic: the constructed instance has and jobs, which is exponential in the length of the binary KNAPSACK input. The paper's Remark (p. 23) resolves this by encoding groups of identical jobs by their cardinality and one copy of their data, and the formal statement adopts that encoding.
CookPvsNP.PolyReducible from the published definition CookPvsNP_defs (polynomial-time many-one reducibility in Cook's machine model). Numbers are coded in binary over the four-letter alphabet BSym with encNats from the published definition ProjSchedTW.Complexity.Encoding (Neumann, Schwindt and Zimmermann's formalization); its own subsetSumLang allows zero entries, so KNAPSACK over positive integers is defined here.Fin n, 0-based; the groups , , and are index ranges. Starting times are natural numbers: the paper computes them from processing orders on integer data (Section 3), and claim (D) is false for real starting times.CookPvsNP model.A single machine must process jobs, each with a processing time and a deadline, and some jobs must be finished before others may start. The first question of any planner is whether the deadlines can be met at all. Without precedence constraints the answer is classical: Jackson's rule (J. R. Jackson, 1955, reported by W. E. Smith, 1956) says that all jobs can be completed on time if and only if they are completed on time when sequenced by earliest deadline first. Precedence constraints break this rule, because the earliest-deadline order may put a job before one of its required predecessors.
E. L. Lawler and J. M. Moore (Management Science 16 (1969) 77–84) repair the rule by replacing each deadline by a modified deadline that accounts for the deadlines of the job's successors. Their §2 Theorem says that a single sequence, the one in increasing order of modified deadlines, decides feasibility. They use it as the first step of their dynamic programming method for sequencing with deadlines and precedence constraints: because the sequence does not depend on processing times, the jobs to be scheduled on time can always be taken in this one fixed order.
There are jobs . Job has a processing time and a deadline . A sequence lists every job exactly once; the machine starts at time and processes the jobs in the order of , one after another, without idle time. The completion time of job is the sum of the processing times of and of all jobs before it in . Job is on time in if .
Precedence constraints are a partial order on the jobs (reflexive, antisymmetric, transitive). If and , job must precede job ; such a is a successor of , and every job counts as one of its own successors. A sequence is consistent with if no job appears before a job that must precede it. The jobs are numbered so that implies .
For a number the modified deadline of job is
the earliest deadline among and its successors, plus a tie-breaking term. The paper takes to be "a small number"; here that means and whenever .
Let be the sequence in which increases. Then
The Theorem reduces a question over all sequences consistent with to the evaluation of one sequence, and the sequence depends only on the deadlines and on , not on the processing times. This independence is what the paper's later sections rely on: it lets a subset-selection dynamic program (Eq. (1) of the paper) process jobs in a fixed order. Without precedence constraints ( the identity) the Theorem is Jackson's rule. The operational form, "always take next, from among the available jobs, a job which has a successor with the earliest possible deadline", is a list-scheduling rule of the same kind as the backward rule of Lawler (1973) for .
The result has been proved on paper since 1969. As far as is known it has no machine-checked proof. This mission produces a formal proof of the Theorem and of the exchange step behind it, stated on the same sequence and completion-time model as the platform's existing single-machine scheduling missions.
The obvious argument is the exchange argument for Jackson's rule: swap an adjacent pair that is out of order and check that nothing becomes late. Two things fail without care. First, the swap must not violate precedence; this is why the deadline of a job is replaced by the minimum over its successors. Second, after the swap, job completes when job used to complete, but need not be at least : one must find a successor of that is later in the sequence, on time, and due no later than . That step uses the smallness of : with a large the tie-breaking term outweighs a difference of deadlines, and the Theorem fails (three jobs without precedence, , , ). Finally, the exchange step must be turned into a terminating transformation of an arbitrary feasible sequence into , a bubble-sort argument over lists.
Fin n, 0-based: the Lean job j is the paper's job , and the tie-break is . Processing times and deadlines are real.MooreLateJobs.Shared.IsSchedule and MooreLateJobs.Shared.completionTime (a duplicate-free list of all jobs; start at time , no idle time). Idle time never helps meet a deadline, so this loses nothing. Consistency with is the published LawlerPrec.MinMax.IsFeasible.insert j {k | ρ j k}, which is nonempty; for the reflexive of the paper this is ("considering a job to be one of its own successors").Related platform items: Jackson's rule for unrestricted jobs is already posed as MooreLateJobs.NumLate.jackson (Moore 1968) and is not re-posed here; Lawler's theorem is posed as LawlerPrec.MinMax.sequencing_theorem. Contributions welcome: general list-exchange lemmas (adjacent swaps, bubble-sort termination toward a sorted list) are reusable well beyond this mission.
The Kolmogorov–Smirnov statistics measure how far the empirical distribution of a sample lies from a hypothesised distribution. They are the standard goodness-of-fit test for continuous data, and their tail probabilities are the basic tool for confidence bands around a distribution function. A test is only usable at a fixed sample size if those tail probabilities are controlled for every , not just in the limit.
Timeline.
Let () be independent, identically distributed real random variables with a continuous distribution function . The empirical distribution function is
and the centred, normalised empirical process is . The statistics are
In Lean the sample is X : Fin n → Ω → ℝ, independent (iIndepFun X P) with common law μ (HasLaw (X i) μ P), is cdf μ, and the statistics are Dplus μ X, Dminus μ X, Dtwo μ X. The parameter is written l.
The proof works with Smirnov's point probabilities , whose sum over is , with Csáki's density of the first passage of a Brownian bridge at level , and with the ratio .
For every and every , with ,
Here is the minimum. The constant in front of the exponential is the point of the theorem; the threshold on is the paper's.
The milestones follow the proof in the paper's order of attack:
The equality in law of and , Comment 1 ((1.4) whenever ), the reduction , and Corollary 1:
The result. Theorem 1 and Corollary 1 give non-asymptotic Kolmogorov–Smirnov bands with the asymptotic constants, and , which cannot be improved because of the limit laws. Corollary 1 is the form in which the DKW inequality is quoted throughout statistics and learning theory: confidence bands for distribution functions, sample-size calculations for quantile estimation, and as a building block in bandit and empirical-risk analyses. Comment 1 says that the one-sided test is never anti-conservative at levels up to 50%, whatever the sample size.
Formalizing it. The result is proved on paper but not machine-checked. A formal development would give a verified, constant-explicit DKW inequality that downstream statistical results can import as a black box instead of carrying an unspecified . The milestones also produce reusable pieces: Smirnov's exact law of the one-sided statistic, the Brownian-bridge first-passage integral, and a family of explicit elementary inequalities. The proof uses computer-checked numerics ((2.15), Lemma 2, ); turning those into checked certificates is part of the work.
The obvious route is to compare the exact sum (2.3) term by term with the integral (2.4). The local comparison is only nearly true: a corrective factor is needed, and it is largest on the tail, where the crossing time is close to . Controlling that factor uniformly in while keeping the leading constant exactly is what forces the delicate constants (, , , ). For small the analytic bounds are too weak, and the proof closes the gap with a Lipschitz bound on plus a finite numerical check over a grid; neither half suffices alone.
Conventions:
Fin n; is cdf μ with Continuous (cdf μ) assumed, as in Theorem 1.ENNReal.ofReal of the bound. Each supremum defining a statistic is of a function with values in , hence a genuine real supremum.Additions and corrections relative to the page, each disclosed in its item: the printed slips in (2.1) (range of ), (2.8) (swapped numerators) and Proposition 2(i) ("" for nonincreasing) are corrected; Claim 2 carries the hypothesis , without which the corrected claim is false; Lemma 3 uses strict inequalities ; Comment 1 makes the implicit explicit; (2.14) carries Proposition 2's standing range , .
The goal does not mention , , , the case split at , or the computer check; a formalization of the goal through those objects, or with the threshold read as a maximum instead of a minimum, would be a different and weaker statement.
Infrastructure a complete development needs: the empirical process of an i.i.d. sample and its reduction to the uniform law by the probability integral transform; Smirnov's exact one-sided law (a ballot-type combinatorial identity); Gaussian-type integrals on ; elementary but delicate real inequalities; and certified interval arithmetic for the numerical steps. The first two are reusable for any work on empirical processes. Contributions on any milestone are welcome, in particular formal proofs of (2.3), of the numerical steps, and of the companions.
Alan S. Manne's Linear Programming and Sequential Decisions (Management Science 6(3), 1960, pp. 259–267) is the first formulation of an infinite-horizon, average-cost sequential decision problem as a linear program. The illustration is a single-item inventory problem, but the construction, with unknowns indexed by a state and a decision and constraints expressing statistical equilibrium, became the standard state–action frequency linear program of Markov decision processes. Later LP approaches to average-cost Markov decision processes, including constrained ones, build on it.
Timeline of the LP approach to average-cost problems:
A positive integer bounds inventory accumulation; the stock levels are . At the start of a month the initial stock is observed and a production quantity is chosen; the available stock is . The month's demand is independent of everything else and has law . Backlogs are excluded, so the terminal stock is , which becomes the next initial stock. A finite set of admissible pairs , all with and containing for every , lists the decisions available at each stock level. Costs are three arbitrary real functions: of the initial stock, of the production quantity, and of the shortage level.
A stationary randomized decision rule is a conditional probability of producing at stock , supported on admissible pairs. It makes the initial stock a Markov chain. A statistical equilibrium of is a stationary distribution of that chain: the law of the terminal stock equals the law of the initial stock, (2). The expected monthly cost (1) of in the equilibrium is
the expectation taken under the joint law of (initial stock, production, demand).
The linear program has one unknown per admissible pair, the joint probability of (initial stock , production ). Its constraints are , (4) , and the equilibrium equations
and its objective (9) is with the cost coefficients (10)
The companion equation (8.0) for has right-hand side and is omitted from the constraints. A feasible is decoded into and .
The paper labels no theorem or lemma. The goal is assembled from §1 (third paragraph), §3 (N.B.), §4 (last two paragraphs), §5 and §7 (3), and every milestone is cited by section, display, table or footnote.
Assume for every admissible pair. Then the linear program has an optimal solution, and for every optimal solution , with decoding , is a stationary randomized rule, is a statistical equilibrium of , and
for every stationary randomized rule and every statistical equilibrium of .
The result turns an infinite-horizon control problem into a finite linear program. Equilibrium joint laws of (state, decision) under stationary randomized rules are exactly the feasible points of a polytope, and the average cost is linear on it. Consequences include computability by the simplex method; an economic reading of the dual variables (Manne's footnote 5 interprets them as the relative advantage of starting at a given stock level, related to Bellman's functional equation); and, in later work, the treatment of side constraints, which dynamic programming handles poorly.
The result is classical and proved in the paper (largely by inspection of the definitions). It has not been formalized. The formalization adds three things. First, a precise statement of what is optimized when the chain of a rule is not irreducible: the paper's §7 (3) concedes that a "decomposable" optimum makes the equilibrium depend on initial conditions, and the goal resolves this by optimizing over (rule, equilibrium) pairs. Second, an explicit treatment of the stock levels the equilibrium never visits, where the paper's quotient is undefined. Third, a machine-checked numerical example whose LP is derived from the general definitions, not entered by hand. Derman's later irreducible-case version exists on the platform as a separate open statement; this mission covers Manne's irreducibility-free version on state-dependent action sets.
Each step is elementary; the work is bookkeeping across three descriptions of the same object. The equilibrium is defined through the transition kernel of the controlled chain, the LP through the displayed sums over with conditions and , and the cost through the joint law of three variables. Identifying them needs a reindexing of the admissible pairs by stock level, the interchange of a finite sum with an infinite sum over demands, and . The naive argument "the LP constraints are the equilibrium equations, so the LP optimum is the optimal rule" skips two points. The constraints omit (8.0), so equilibrium at stock level must be recovered from (4) and the bound . And the decoding fails at unvisited stock levels unless a default action is supplied. Existence of an LP optimum requires compactness of the feasible polytope, not just its nonemptiness.
All statements live in the namespace ManneLP.Equilibrium. Conventions:
Finset (ℕ × ℕ) with and every ), a demand law with and HasSum p 1, and costs , . The shortage level is an integer; no convexity, sign or monotonicity of the costs is assumed.tsums; the demand is not assumed bounded. The goal and the cost identity assume the expected shortage cost at each admissible pair is finite (absolutely summable), which the page takes for granted.Trivializing formalizations are ruled out: equilibrium is not defined as (8) (which would make milestone 2 vacuous), (8.0) is not a constraint (which would make milestone 3 vacuous), the cost is not defined as (which would make milestone 5 and the goal's cost clause definitional), and the optimality comparison ranges over all rules and all of their equilibria, not over irreducible chains or pure rules.
Contributions welcome: proofs of the milestones and the goal; computations of the §6 example from the general definitions; reusable lemmas on stationary distributions of finite stochastic matrices and on the existence of LP optima over compact polytopes.
The simplex method and every other edge-following linear programming algorithm moves from vertex to vertex of the feasible region along its edges. The number of steps such an algorithm needs in the worst case is at least the combinatorial diameter of the feasible polyhedron: the largest distance, counted in edges, between two of its vertices. Klee and Walkup introduced the two functions that measure this worst case, for polyhedra and for bounded polyhedra of dimension with facets, and wrote that "represents, in a sense, the number of iterations required to solve the 'worst' linear program of inequalities in variables using the 'best' edge-following algorithm" (Klee and Walkup 1967, p. 54).
The Hirsch conjecture, reported by Dantzig in 1963, asserted . Its diagonal cases and are the general and the bounded -step conjectures.
Timeline.
A polyhedron in is a nonempty set ; a polytope is a bounded polyhedron. is a -polyhedron with facets when it has nonempty interior and none of the inequalities is redundant; then the rows are in bijection with the facets, and row is tight at exactly when lies on the -th facet. The vertices of are its extreme points. Two vertices span an edge when the segment is an extreme subset of . A path of length is a sequence of edges , and is the least length of a path from to . Then
is simple when every vertex lies on exactly facets. A face is itself or the intersection of with a supporting hyperplane, never ; its dimension is that of its affine hull. A -path from to is a sequence of faces with , , and . A -dimensional Dantzig figure is a -polyhedron with facets and two vertices such that exactly facets are incident to and the other to . A -polytope has property A when it has between and facets and the following holds: if its facets are split into two classes of at most facets each, and both sets , of vertices all of whose facets lie in , respectively , are nonempty, then some vertex of is joined to some vertex of by a path of length at most .
In two halves: every -polytope with facets satisfies for all vertices , and some -polytope with facets has two vertices with .
The result. By the paper's reductions, for a given is equivalent to the bounded Hirsch bound for every . So 4.3 gives for all , which is the column of the paper's Fig. 2. Since Santos's counterexample, the smallest with is a well-defined open number. This theorem was the first to show it is at least ; later computer-assisted work treated further small cases, including the bounded -step case (Bremner and Schewe 2011). Santos's construction starts from exactly the reduction to Dantzig figures (the "strong -step theorem" for spindles) that this paper uses.
Formalizing it. The result has been proved since 1967; no machine-checked proof of exists. The platform has the Hirsch bound in dimension (Hirsch.dimension_three_bound, Hirsch.klee_three_dimensional_bound), the Klee–Walkup wedge reduction at the level of inequality descriptions (Hirsch.balanced_hpoly_transfer), products (Hirsch.diamLE_prod) and Santos's counterexample. The mission adds the facial-path calculus of §3 and the property-A argument of §4. Both are reusable in any later formal treatment of small -step cases.
The obvious approach, a direct case analysis of -polytopes with facets, is out of reach: there are far too many combinatorial types, and nothing bounds the search. The paper first reduces to simple polytopes, and the reduction itself (2.8) rests on a perturbation lemma (2.6) whose proof is deferred to a separate paper by Walkup: simplicity must be gained without shrinking any distance. The facial-path results then pass between bounded and unbounded figures through truncation and the wedge (3.1), and a statement about all unbounded -dimensional figures is what yields one about bounded -dimensional ones. Finally the -face must be shown to have property A. That property fails for some simple polytopes of classes and (p. 69), so 4.2 depends on the dimension being and on the facet count being at most . Its proof uses Euler's relation and Balinski's theorem that the graph of a -polytope is -connected (posed on the platform as Balinski61.Connectivity.disjoint_paths_between_vertices).
Polyhedra are Hirsch.Hpoly a b with a : Fin n → EuclideanSpace ℝ (Fin d); edges and walks are Hirsch.Adj and Hirsch.Reach from the published Hirsch_model and Hirsch_walk. The conventions are:
Hirsch.Reach P L x y, a walk of steps that may stand still. is an upper bound for every polytope plus a witness, never a supremum of reals. A version proving only the upper bound, or only the lower bound, is not the goal.Fin (2 * d) rows.Set.encard.The paper cites two inputs without proving them: Lemma 2.6 (Walkup's simple perturbation) and Balinski's theorem. A complete development needs face lattices of H-polyhedra, wedges and truncations, and the planar-graph arguments of 4.2. The face and facial-path layer is reusable for the companion mission on and for other diameter problems. Contributions are welcome at every milestone, including proofs of 2.6.
Labor markets match workers to firms, and the terms of each match (the salary) are negotiated along with the match itself. A firm's output depends on the whole team it hires, so a firm cares about sets of workers, not individual workers one at a time. Kelso and Crawford (1982) asked when such a market has a stable outcome, the core, in which no firm and group of workers can agree on terms that all of them prefer, and when a simple decentralized auction finds one.
Their answer is the gross-substitutes condition: raising some workers' salaries never makes a firm withdraw an offer from a worker whose salary has not risen. Under it, an ascending process in which firms make offers and workers reject all but their favorite reaches a core allocation. This condition became the standard hypothesis for the existence of Walrasian equilibrium with indivisible goods (Gul and Stacchetti 1999), it is the hypothesis behind matching with contracts (Hatfield and Milgrom 2005), and the process is the ancestor of ascending auction designs.
Timeline.
There are finitely many workers and firms , with at least one firm. Worker 's utility of working for firm at salary is , strictly increasing and continuous in . Firm 's gross product from hiring the set is , and its profit at the salary vector is
is the set of profit-maximizing . Each pair has a starting salary . The assumptions (p. 1486) are (MP) for ; (NFL) ; and (GS): if and , some contains .
In the discrete market with unit , firm may pay worker only , . An allocation sends each worker to a firm at a salary ; it is individually rational (D1) if and every firm's profit is nonnegative. It is a (discrete) core allocation (D3) if it is individually rational, pays permitted salaries, and no firm , set and permitted salaries satisfy for all and .
The salary-adjustment process (pp. 1488–1489), verbatim:
R1. Firms begin facing a set of permitted salaries . Permitted salaries at round , , remain constant, except as noted below. In round zero, each firm makes offers to all workers; this is costless by (MP).
R2. On each round, each firm makes offers to the members of one of its favorite sets of workers, given the schedule of permitted salaries . That is, firm makes offers to the members of , where maximizes . Firms may break ties between sets of workers however they like, with the following exception: Any offer made by firm in round that was not rejected must be repeated in round . By (GS), the firm sacrifices no profits in doing this, since (by R4) other workers' permitted salaries cannot have fallen, and the salary of a worker who did not reject an offer remains constant.
R3. Each worker who receives one or more offers rejects all but his or her favorite (taking salaries into account), which he or she tentatively accepts. Workers may break ties at any time however they like.
R4. Offers not rejected in previous periods remain in force. If worker rejected an offer from firm in round , ; otherwise . Firms continue to make offers to their favorite sets of workers, taking into account their permitted salaries.
R5. The process stops when no rejections are issued in some period. Workers then accept the offers that remain in force from the firms they have not rejected.
"The salary-adjustment process R1–R5 converges in finite time to a discrete core allocation in the discrete market for which it is defined." Formally, under the assumptions above:
Theorem 1 gives the existence of a core allocation in every discrete market satisfying (MP), (NFL) and (GS), with no convexity of production and arbitrary complementarity within the limits of (GS). It is the step from which the paper derives the existence of a strict core allocation of the continuous market (Theorem 2, by letting the unit shrink), and with additional no-ties assumptions the firm-optimality of the process's outcome (Theorem 4) and the comparative statics of entry and exit (Theorem 5).
The result is proved in the paper and has been reproved in more general settings; it has no machine-checked proof known to us. Nothing of this paper was on Prove2Me before this series. Related platform work, credited but not reused: the Gale–Shapley deferred-acceptance development (GS62CollegeAdmissions.*, proved), the no-money ancestor of this process; and the Shapley–Shubik assignment game (AssignmentGame.CoreLP), whose core the process approximates when production is additively separable. Neither states anything about this process. This mission is mission 1 of a series of seven on the paper: 2 (strict core of the continuous market), 3 (one-sided coalition formation), 4 (firm-optimality), 5 (comparative statics), 6 (gross substitutes and decreasing returns), 7 (a market without a core). Each states its own model.
The process is quantified over all tie-breakings, so no single computation settles it; the statements are about every sequence of rounds consistent with R1–R5. Two points carry the content. First, R2 imposes a constraint that may not be satisfiable: a firm must repeat its unrejected offers and choose a profit-maximizing set. Without (GS) no such set need exist and the process is not defined. Second, the core property at the stopping round compares the outcome with coalitions using salaries the process never reached; the comparison is with salaries on the discrete grid only, and it is false if coalitions may use salaries below or off the grid. Termination is not automatic either: the process may continue after a round without rejections, salaries are real numbers, and no bound on the number of rounds is given.
Lean representation, in namespace KelsoCrawford.Process:
Market W F carries u, y, σ; workers and firms are finite types, with [Nonempty F] (the paper's ; with no firms and some worker no run exists).Allocation assigns every worker to a firm (no unemployment, as in the paper's ).GrossSubstitutesOn (M.y j) (M.gridVectors δ j) for each firm: the discrete (GS), since the paper notes that a discrete market may satisfy (GS) while its continuous version does not.M.grid δ .Run records salaries, offers and tentative choices per round; IsRun is R1–R4, Stopped is R5's "no rejections", outcome is R5's allocation.Explicit readings of the paper's phrases:
The existence of a run is part of the goal: without it, statements about all runs would be vacuous. Fixing a tie-breaking rule would turn the statements into claims about a single run and is ruled out; so are the strict core D2 (false here because of ties at the grid) and an integer grid below (false for improving coalitions). Proofs of the milestones and reusable infrastructure for ascending processes are welcome.
A many-server queue in which customers arrive at the epochs of a renewal process and are served for exponential times is the basic model of a telephone exchange, a call centre, or a bank of identical machines. Its continuous-time queue-length process is not Markovian unless the arrivals are Poisson, so Erlang's birth–death formulas for M/M/s do not apply. In 1953 D. G. Kendall showed how to analyse such systems by the method of the imbedded Markov chain: observe the system only at the arrival epochs, where the number of customers present does form a Markov chain, and read the equilibrium behaviour off that chain (Kendall 1953).
Timeline:
Customers arrive with independent inter-arrival times of law on and mean , . There are servers and a single queue served first come, first served. Service times are independent of one another and of the input, negative-exponential with mean , . The relative traffic intensity is .
The state of the imbedded chain at an arrival epoch is the number of persons found ahead (waiting or in service) by the arriving customer. Its transition matrix of eq. (8) is given in three blocks, written with the death-process probabilities of (9)–(10), the probabilities of (11)–(12), and the Poisson probabilities of (13)–(14):
The key function is
The queue size met by an arrival is . The waiting time is, given , the sum of independent exponential variables of mean .
When the chain has a limiting distribution , and with the root of in and ,
with both conditioning events of positive probability. The goal fixes no constant beyond those the theorem names: and are determined by , and .
Theorem IV says that, whatever the input law and the number of servers, the part of the equilibrium waiting-time law away from zero is exponential and the part of the queue-size law away from zero is geometric, both governed by the single number . All equilibrium quantities of GI/M/s (Theorems II–III and the delay distribution) then reduce to computing from a one-dimensional equation and the finitely many 's from a triangular linear system. This is the standard textbook treatment of G/M/c queues and the template for many later matrix-geometric results.
The results are proved in the paper, partly by appeal to Feller's theory of denumerable chains and to "tedious but elementary" verifications. None of them is machine-checked. The mission formalizes the paper's chain of argument: the explicit transition matrix, its stochasticity, the reduction of the invariance equations, the passage from a summable invariant vector to the limiting distribution, and the computation of the laws of and from it. The single-server special cases are posed separately on the platform (QueueingFundamentals.GM1.arrival_point_geometric, GM1.waiting_time_cdf, GM1.arrival_point_means, GM1.mean_waiting_times, FosterQueues.GIM1.gim1_classification); they do not cover .
The obvious route is to guess the geometric tail and check it against the balance equations. For this works, but the rows of the block involve the convolution integral (11), and the equations for couple the geometric tail to the boundary terms . Showing these are solvable, and that the row sums of the three-block matrix equal one, requires handling (11) explicitly. The second obstacle is the limit theorem itself: an invariant vector does not, by itself, give . That step needs Feller's dichotomy for irreducible aperiodic denumerable chains, which Mathlib does not provide. Finally, the conditional waiting-time law requires summing an Erlang mixture with geometric weights in closed form.
The queue process itself is not formalized. The chain is defined by its transition matrix (8)–(14), and by the Erlang mixture of p. 349, as the paper derives both by a modelling argument. A chain is any TransitionMatrix P of the published Markov-chain vocabulary with P.p = gimsMatrix s A b; states are -based. "Ergodic" is Feller's: Aperiodic ∧ PositiveRecurrent. The limiting distribution is asserted as Tendsto (P.stepProb n i j) atTop (𝓝 (π j)) for all , not as a stationary vector. The input law satisfies the published IsInterarrivalLaw A a⁻¹ (a probability measure carried by , integrable, mean ), and is the published serviceProb A (s/b) n. Conditional laws are stated multiplied out, together with positivity of the conditioning probabilities. Every series identity is stated with HasSum.
Trivializing formalizations are ruled out: is tied to on rather than free; is the limiting distribution of , asserted to exist, not a probability vector handed to the statement; the conditioning events are asserted to have positive probability; the matrix is the GI/M/s matrix, not the GI/M/1 one; and the 's of Theorems II–III are characterized by the invariance equations, never defined from .
A complete development needs: Feller's limit theorem for irreducible aperiodic positive recurrent chains (reusable well beyond this mission), Foster's sufficiency criterion (referenced, open), Fubini for the stochastic-matrix identities, parametric interval integrals for the block , and Erlang distribution functions. Contributions to the general Markov-chain milestones are as welcome as those specific to GI/M/s.