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?
Assembly systems — components purchased from outside, assembled into subassemblies, and those into an end product facing random customer demand — are the standard model of material requirements planning under uncertainty. Rosling's paper (Oper. Res. 37(4), 1989) shows that, under a cost assumption, the optimal policies of such a system are those of an equivalent series system, so that the Clark–Scarf decomposition of serial systems (Clark and Scarf, 1960) applies to assembly systems.
The cost assumption of the main results requires every echelon holding cost to be positive. In §4 Rosling replaces it by a weaker Generalized Assumption (GA), which allows some echelon holding costs to be negative, and then argues with Theorem 4 that GA "covers all cases of practical interest for a long-run analysis". Part (i) of Theorem 4 is the first step of that argument: when GA(i) fails strictly for some item, the model is degenerate, because its minimal cost is . This mission formalizes that statement.
There are items ; item is the end item. Every item has exactly one immediate successor with , and , so the items form a tree rooted at the end item. Write for the set of all successors of , for the set of all its predecessors, and for its immediate predecessors. Item has a lead time , and its total lead time is , ; the items are indexed so that .
Time runs in periods . The demands for the end item are independent, identically distributed, nonnegative, with a density and a finite mean . In period a policy chooses the echelon inventory positions after ordering as functions of the demands already observed. The position before ordering is , and the echelon stock on hand after arrivals is ; positions referring to periods before are read off given initial data . Problem P asks for a policy satisfying
that minimizes
where is the echelon holding cost of item , the backlogging cost, the installation holding cost of the end item, the discount factor and the density of the demand over periods.
The quantity of interest is the discounted echelon holding cost of item and its predecessors,
GA(i) asks it to be positive for every item.
If for some item
then the minimal cost of Problem P is unbounded below: for every real there is a feasible policy whose cost is a real number less than .
Theorem 4(i) explains why the Generalized Assumption is the natural boundary of the theory: a strict violation of GA(i) makes Problem P meaningless, since no policy is optimal and the infimum is . Together with parts (ii) and (iii) of Theorem 4 it reduces every case of interest to systems satisfying GA, for which Rosling's series-system results apply. The quantity in the condition is the natural "net value of stockpiling" of a subsystem, and the same exchange — buy more of a subsystem early and hold it forever — is the basic perturbation behind many optimality arguments for multi-echelon systems.
The result is proved in the paper, in a few lines. To our knowledge neither Theorem 4 nor the assembly model of Problem P has been machine-checked. A formalization adds a precise statement of what "the minimal cost is unbounded below" means for a stochastic infinite-horizon problem with an extended-real cost, and the definitions of the assembly model — product tree, total lead times, echelon positions, history-dependent policies, constraint (3) and objective (2) — which other statements of the same paper need.
The algebra of the cost increase is a geometric series. The work lies elsewhere. First, the one-more-unit policy must be shown feasible for every item of the subsystem in every period, including the boundary items: the successor of , whose constraint loosens, and predecessors with zero lead time. Second, the cost of a policy is an expectation of an infinite discounted sum whose terms have no sign; the cost increase can only be added to a cost that is finite, and the argument needs a feasible policy of finite cost to start from, which the paper takes for granted. Third, for the end item the extra units also change the expected backlog term of (2), which the printed display omits, so the end item needs a separate bound.
Measure.infinitePi) of a probability measure on with , Lebesgue, integrable and .In the extended reals, : a policy whose positive and negative cost parts are both infinite gets the value . The goal therefore asks for policies of real cost below every bound; a formalization that only exhibits a policy of cost would be trivially true and is ruled out. Milestone 2 is stated for , where the backlog term is unchanged.
Needed infrastructure: lower Lebesgue integrals of discounted sums under the infinite product measure, linearity of the cost under a deterministic perturbation, and the finiteness of the cost of the "never order" policy (whose decisions decrease linearly in the accumulated demand). Contributions of general lemmas on discounted costs of history-dependent policies under infinitePi are welcome and reusable.
A committee that chooses one alternative by voting would like a procedure under which nobody gains by misreporting their preferences. Gibbard (Econometrica 41, 1973) and Satterthwaite (J. Econ. Theory 10, 1975) showed that, once at least three outcomes are possible, the only voting procedures with this property are dictatorial. The theorem is the starting point of the theory of strategy-proof mechanisms and of implementation theory.
Most proofs, including the main argument of Satterthwaite's paper, assume strict ballots: no voter is indifferent between two distinct alternatives. Real ballots, and most economic models of preferences, allow indifference. The last section of Satterthwaite's paper carries the theorem over to ballots that are arbitrary weak orders, by decomposing a voting procedure into a tie-breaking function followed by a strict voting procedure. This mission formalizes that extension.
Timeline. Gibbard (1973) proved the impossibility for game forms; the 1974 discussion paper formalized here proved it for strict ballots by induction on the number of voters (Theorem 1), allowing the range of the procedure to be a proper subset of the alternatives, and extended it to weak orders (Theorem 1′). Later short proofs (Barberà 1983; Benoît 2000; Reny 2001) also treat strict ballots.
A committee is a finite set of individuals and a finite set of alternatives. A weak order on is a complete and transitive relation, with read " is preferred or indifferent to "; its strict part is iff and not . The weak orders form . A strong order is a weak order with no indifference between distinct alternatives; the strong orders form . A ballot set is .
A voting procedure is a map . Its range is , with . A strict voting procedure is a map .
is strategy-proof if there are no ballot set , individual and ballot with
For a strict procedure, ballot sets and substituted ballots are strong orders.
is dictatorial if some individual exists such that, for every ballot set , the outcome is among the -maximal elements of : for all .
A tie-breaking function is a map that keeps every strict preference: if then implies . It is regular if there are fixed strong orders such that every indifference , is broken as breaks it.
For and , every strategy-proof voting procedure on weak-order ballots is dictatorial:
The converse fails once indifference is admissible: a dictator's ties may be broken by a manipulable rule, such as a Borda count of the other ballots (pp. 10–11). The goal is therefore a one-way implication.
The result shows that allowing voters to express indifference does not escape the Gibbard–Satterthwaite impossibility: the dictatorial conclusion survives, and only the equivalence is lost. It is the form of the theorem most directly applicable to economic environments, where preference domains usually contain indifference, and the decomposition of Lemma 9 is the device by which strict-ballot results are transferred to weak-order ballots throughout §6 of the paper, including the weak-order version of Arrow's theorem.
The theorem is proved and classical. What is not yet available is a machine-checked proof of the weak-order version with a range that may be a proper subset of the alternatives. The strict, full-range case is proved on the platform (AGT.gibbard_satterthwaite, on strict total orders with a surjective rule); the strict case with an arbitrary range of size at least three is the goal of the companion mission on strict committees. This mission adds the decomposition of Lemma 9 and the extension to indifference.
The obvious route is to restrict a strategy-proof to strict ballot sets, apply the strict theorem, and conclude. Two steps fail. First, the restriction's range may a priori be smaller than , so the hypothesis need not transfer. Second, knowing that is dictatorial on strict ballot sets says nothing directly about ballot sets with indifference: one needs, for each , a strict refinement of with , and the refinement of one individual's ballot may depend on the others' ballots. Lemma 9's second sentence is exactly the existence of such refinements, and the tie-breaking function it produces is generally not regular.
Lean commits to the following conventions, all in the definitions file StrategyProofArrow.WeakGS.Basic:
ι and A; and are their cardinalities. The theorems state or as printed, and where the paper's standing committee assumption is all that applies (Lemma 9). is automatic.Set.range v.A trivializing formalization would measure manipulation by the weak relation instead of its strict part, which makes "strategy-proof" nearly unsatisfiable and the goal vacuous; the definitions use the strict part, and a sorry-free check confirms that a strategy-proof procedure with range of size 3 exists.
A complete development needs the strict Gibbard–Satterthwaite theorem with partial range (milestone 1) and the refinement construction of Lemma 9. The weak-order and tie-breaking vocabulary is reusable for the weak-order Arrow theorem of the companion mission. Proofs of any milestone, and alternative proofs of the goal that bypass Lemma 9, are welcome.
A d.c. program minimizes a difference of two convex functions. Many nonconvex problems of practical interest have this form: every function with a locally Lipschitz gradient on is d.c., the class is closed under finite sums, products and finite suprema, and constrained problems enter through indicator functions. Pham Dinh Tao and Le Thi Hoai An (SIAM J. Optim. 8 (1998)) use this structure to build the DCA, an algorithm for the trust-region subproblem , a basic step of trust-region methods in nonlinear optimization. The algorithm rests on a duality theory for d.c. programs, which §3.1 of the paper sets out. This mission is the global half of that theory.
Timeline.
Let with its canonical inner product , and identify the dual space with . Functions take values in . A function is in if it is convex, lower semicontinuous, never , and finite at some point. Its effective domain is , and its conjugate is
For , the subdifferential is the set of with for all . For the -subdifferential is
Given , the d.c. program and its dual are
with the convention . Throughout, the paper assumes the inclusions
and denote the solution sets of (P) and (D).
For every ,
The result. Theorem 3.1(i) characterizes global minimizers of a nonconvex function by inclusions between convex objects. It is a certificate of global optimality that uses only convex analysis. Parts (iii) and (iv) say that a solution of either program yields a solution of the other through a subgradient. This is the mechanism of the DCA, which alternates , . The paper notes that condition (i) is hard to use in an algorithm and that the DCA rests on local conditions instead. The global condition remains the reference statement that the local theory and the DCA approximate.
Formalizing it. All results here are classical and proved on paper. Parts (iii) and (iv) are proved in references the paper cites, not in the paper itself. None of them has a machine-checked proof on the platform. The mission provides a Lean layer for d.c. programming on : the convention-respecting difference, the -subdifferential, the standing assumptions, and the primal and dual solution sets. Missions II and III of the series reuse this layer for local optimality and for the convergence of the DCA.
The paper's proof is short, but each step uses a fact that needs separate work. The duality requires the biconjugation for , and an exchange of two infima in the extended reals under the convention . The step (7) ⇔ (8) has a hidden case: a point of . Ruling it out needs for , a nontrivial property of lower semicontinuous proper convex functions. The obvious approach, computing with real numbers, fails because , , and all take the value , and the extended-real arithmetic of Lean does not follow the paper's convention.
EuclideanSpace ℝ (Fin n). Functions are EReal-valued.ThreeOpSplitting.ConvexRates.IsProperClosedConvex, is InertialFB.IFB.IsSubgradient, and the conjugate is CondatPD.FinDim.conj, an extended-real supremum over all of .dcSub, which returns when the first term is . , and are defined through it.intrinsicInterior, and the "in this case" inclusions into and .EReal-valued functions on EuclideanSpace in the conventions of CondatPD.FinDim.conj, nonemptiness of -subdifferentials, and the extended-real infimum exchange. These are reusable well beyond d.c. programming.An arbitrator who must choose among collective options for a group of players usually does not know the players' private characteristics. The arbitrator can only ask, and a player who expects to profit from a false answer may give one. Before designing any procedure, the arbitrator therefore needs to know which expected-payoff allocations can be reached at all once strategic misreporting is taken into account.
Myerson (1979) answers this for Bayesian collective choice problems with finitely many types. Restricting attention to mechanisms that simply ask each player for their type, and that make honest answers optimal, loses nothing: every expected-payoff allocation that any mechanism can produce in equilibrium is already produced honestly by such a direct mechanism, and conversely. This is the revelation principle in the form used throughout Bayesian mechanism design. It is what makes incentive-compatibility constraints the starting point for auction design, bilateral trade, and the bargaining solution in the second half of the same paper.
Timeline. Gibbard (1973) gave the dominant-strategy form of the principle. Rosenthal (Review of Economic Studies, 1978) studied arbitration of two-party disputes under uncertainty; Myerson notes that Theorem 2 could be derived as a corollary of Rosenthal's Theorem 3. Dasgupta, Hammond and Maskin (1979) gave general Bayesian implementation results in the same year. Myerson's Theorem 2 states the principle as an equality of interim payoff sets over all finite response sets. Myerson (1982) later extended it to principal–agent problems with moral hazard.
A Bayesian collective choice problem has a nonempty finite set of players , a nonempty finite set of types for each player, a nonempty finite set of collective choices, utilities depending on the choice and on the true type profile , and a probability distribution on type profiles. With the marginal of type , a player of type assigns the conditional probability to profiles with , and to the others.
A choice mechanism on response sets (nonempty finite sets of possible answers) is a function with for every response profile . On the standard response sets , the payoff of type who reports while the others are honest is
The mechanism is Bayesian incentive-compatible if for all . Its honest allocation is the vector with coordinates , indexed by the disjoint union of the . The incentive-feasible set is
On general response sets, a response plan is a probability distribution over for each type . Plans give type the payoff
They form a response-plan equilibrium for if no type of any player gains by switching to any other response plan . The equilibrium-feasible set collects over all choice mechanisms , on all nonempty finite response sets, and all response-plan equilibria for .
Both inclusions are asserted for every Bayesian collective choice problem. says equilibrium behaviour under any mechanism can be replicated honestly by an incentive-compatible direct mechanism. says honest reporting is itself an equilibrium of every incentive-compatible mechanism.
The result. Theorem 2 reduces a search over all communication protocols, an unbounded family of response sets and mixed reporting behaviours, to a finite system of linear inequalities in on a fixed finite domain. Combined with Theorem 1 of the paper, which shows is a nonempty compact convex set, it justifies applying a bargaining solution to rather than to some larger, ill-defined set of attainable outcomes. The same reduction underlies the use of incentive constraints in optimal auctions, bilateral trade and correlated-type mechanism design.
Formalizing it. The result is classical and its proof is short, but it is a statement about all finite response sets at once, and the equality of two sets of payoff vectors is sensitive to the conventions: which plans are allowed as deviations, where the conditioning happens, and whether the induced mechanism is a genuine probability distribution. A machine-checked version pins these down. To our knowledge no formal proof of this finite Bayesian revelation principle exists. The platform has related, unproved items in other models: MechanismDesign.Robust.revelation_principle (Börgers, Prop. 10.2, on a countable Harsanyi type space with PMF lotteries; one inclusion, outcome equivalence) and single-agent, quasi-linear and dominant-strategy revelation principles from the same book. None of them is the statement here.
The mathematics consists of finite sums, but the bookkeeping is the obstacle. Milestone 1 requires exchanging a sum over response profiles with a product over players and using that each plan sums to one. Milestone 2 requires recognizing a lie in as a particular whole response plan in : the plan that, at every type, behaves as type would. Because vanishes off , only its value at matters. For milestone 3, a mixed deviation from honesty has to be bounded by the best pure misreport, a convex-combination argument over . Identifying the side of the goal also needs instances on an existentially chosen family of types.
All objects live in MyersonBargaining.Revelation. Players form a nonempty finite type ι; types A i, choices C and response sets S i are nonempty finite types in Type. Mechanisms and plans are real-valued functions with the probability constraints as predicates (IsChoiceMechanism, IsResponsePlan), event first and condition second: π c s, σ i s a. Allocation vectors are functions on Σ i, A i. The paper's loose phrases are read as follows:
S : ι → Type and its instances;The product in (12) is printed with ; it is formalized with , as the paper's own induced mechanism on p. 66 uses. Milestone 1 is stated for arbitrary response plans, not only for equilibria. Section 6's numerical example is not formalized.
A trivializing formalization is ruled out explicitly: fixing in , restricting deviations to pure plans, or stating only would each change the theorem, and none is done.
A complete development needs finite sums over dependent product types (Fintype.piFinset, Finset.prod_univ_sum), Function.update on dependent families, and nothing beyond Mathlib. The two definition modules (the model and the response-plan objects) are reusable by any finite Bayesian mechanism-design formalization. Proofs of any milestone, alternative proofs via Rosenthal's argument, and cleaner restatements as lemmas about stochastic matrices are welcome.
Many quantities in operations research accumulate over time in a system that periodically starts afresh: the cost incurred by an inventory system that returns to the same stock level, the work completed by a server between successive moments it empties, the reward collected by a machine between repairs. The basic question about such a quantity is its long-run rate: does the amount accumulated by time , divided by , settle down, and to what?
W. L. Smith's 1955 paper Regenerative stochastic processes (DOI 10.1098/rspa.1955.0198) introduced the class of cumulative processes to answer this question, and §5·3 of the paper proves the answer, Theorem 7, which Smith calls "the ergodic theorem": the long-run rate equals the expected accumulation per cycle divided by the expected cycle length. In later textbooks this is the renewal–reward theorem, the standard tool for computing long-run averages of regenerative systems in queueing, inventory and reliability models.
Timeline. Doob (1948) proved the strong law for renewal counting processes (Trans. AMS 63). Smith (1955) defined cumulative processes by conditions (C1)–(C2) and proved Theorem 7 under a first-moment condition on the variation per cycle, together with central limit theorems (Theorems 9–10) for the same processes.
Fix a probability space .
A renewal process is a sequence of independent, identically distributed, non-negative random variables that are not zero with probability one, i.e. . Write . In this mission the delay is , the regeneration epochs are , and the counting variable
is the number of regenerations in (the paper's "greatest integer such that "). The forward variable measures how far is from the regeneration epoch .
Let be a real-valued process with . Its cycle increments are , , and . On a path of bounded variation on every finite interval, the variation process is the total variation of the path over ; the cycle variations are , and .
The process is a cumulative process when
If is a cumulative process, , , and , then
The statement fixes no rate and no constant; it is the exact limit of the paper.
The ergodic theorem turns a question about a whole sample path into a question about one cycle. Once a system is shown to regenerate, its long-run average cost, throughput or utilization is the ratio of two one-cycle expectations, which can often be computed in closed form. This is how long-run averages are evaluated for -type queues, inventory policies and alternating-renewal reliability models, and it is the first step in average-cost analyses of regenerative Markov decision processes. Lemma 8, with , also controls the error term in Smith's central limit theorem for cumulative processes.
The result is classical and proved. As far as the platform and Mathlib are concerned, it is not formalized: Mathlib has the strong law of large numbers for i.i.d. sequences (ProbabilityTheory.strong_law_ae) but no renewal counting process, no renewal strong law, and no renewal–reward theorem. A complete development gives machine-checked versions of all three, stated for real time and for cycle lengths that may vanish with positive probability.
The obvious argument writes as and applies the strong law to each factor. This fails in two places. First, is not a sum of whole cycles: the cycle containing is only partly completed, and its contribution has to be shown negligible. The increment does not control it, because may oscillate inside a cycle and return; it is the variation that bounds the partial contribution, which is why the hypothesis is on rather than on . Second, the strong law is a statement about a deterministic index , while here the index is random and depends on the cycle lengths, which need not be independent of the increments. Transferring almost-sure convergence through the random index requires almost surely, which in turn uses .
Time is real: every limit is along in (Filter.atTop on ℝ), and "with probability one" is an almost-everywhere statement placed outside the limit. Random variables are real-valued. The renewal process is the structure IsRenewalProcess (cycle lengths measurable, mutually independent, identically distributed, non-negative everywhere, ); and are explicit hypotheses holding at every sample point. Moments are Bochner integrals guarded by integrability hypotheses: is integrability of , is integrability of . The positivity is never assumed; it follows from .
The count is a cardinality; on the null event where infinitely many epochs lie below it takes the value , and finiteness is never assumed. The variation process is Mathlib's eVariationOn of the path over , set to on paths that are not of bounded variation, exactly as the paper prescribes.
Condition (C1) is read literally: only the increments are i.i.d., and no independence between cycle lengths and increments is assumed. In addition the cycle variations are assumed identically distributed; the paper's notation presupposes this. The statement is not trivialized by a stronger model: taking to be a Lévy process, or a deterministic multiple of , would make the theorem immediate and is not what is formalized.
Two misprints of the paper are corrected in the formal statements and kept in the verbatim milestone text: (5·3·4) prints the limit as , which must be ; and the proof bound (5·3·1) uses alone, where the interval also meets cycle .
Needed infrastructure: a renewal counting process in continuous time with its strong law; a lemma that almost-sure convergence of a sequence passes to a random index tending to infinity; the comparison for paths of bounded variation. All three are reusable well beyond this mission (renewal–reward arguments, regenerative simulation, average-cost Markov decision processes). Contributions of any milestone, and of these general lemmas as separate theorems, are welcome.
Weighted voting models assign a coalition a win when its combined vote reaches a quota. The Shapley value measures a player's contribution by averaging the change it makes when added to every possible predecessor coalition. This is straightforward to define for a finite list of voters, but a voting body may contain a few major holders and a very large population of individually small holders. A calculation made for a finite approximation should then have a stable meaning as the small holdings are divided more finely. Milnor and Shapley's oceanic game gives that question a precise form and asks whether its major-player values agree with the limits of finite weighted majority games. Milnor and Shapley, RAND RM-2649 (1961).
The question matters whenever a finite voting model is used to represent a diffuse electorate or ownership base. Without a continuity result, the measured power of a major voter could depend on how an otherwise identical mass of minor votes was artificially split. The memo's Theorem 1 establishes the required stability under an explicit small-weight condition. The result is a known theorem from the 1961 memorandum; the task here is its Lean formalization, including the mathematical objects that make its statement meaningful.
Fix a finite set of major players, with nonnegative weights . The ocean is a continuum of individually insignificant voters represented by the unit interval , with total weight . A coalition's vote is its major-player weight plus times the Lebesgue measure of its oceanic part. It wins when that vote reaches a quota . The formal development uses Fin m for and real weights; the underlying voting rule is the one in §2 of the memorandum. Milnor and Shapley, §2.
To assign a value to a major player, insert each major player independently and uniformly into the ordered ocean. A position vector lies in the cube . Write and . Major player is pivotal when the predecessor weight is below the quota and adding reaches it, in the memo's weak-boundary form
The oceanic major-player value is the probability of this event. Since the insertion positions are uniform, it is also the -dimensional Lebesgue volume of the corresponding set . Equalities at boundary positions have zero volume. Milnor and Shapley, (2.3)–(2.4), pp. 4–5.
At stage , the finite approximation has the same major players, followed by minor players with nonnegative weights . Its quota and major weights are and . A coalition has value one if its weight is at least , and zero otherwise. The finite-game value is the Shapley value of that coalition function. The published Shapley-value definition is reused for this general finite-game object; only the quota game and its oceanic limit are defined for this mission. Milnor and Shapley, Appendix (A.1), (A.4).
The principal target says that if quotas and major weights converge, the total minor weight tends to , and every minor weight becomes small, then each major-player value converges:
This is Theorem 1, equations (3.1)–(3.2), of the memorandum. Its conclusion refers to the pivotal-probability definition of above. Milnor and Shapley, Theorem 1, p. 6.
The milestone list follows three statements present in the source: equation (3.4) partitions by the predecessor set ; equations (3.5)–(3.6) give the volume of each part as a one-variable integral with clamped endpoints; and Appendix (A.1)–(A.3) states the finite-game limit as a sum of those integrals. Their shared expression is
The appendix's limit statement concerns ; Theorem 1 concerns . Both are separate targets in the formalization. Milnor and Shapley, §3 and Appendix.
The theorem makes the major-player value independent of a particular fine division of the minor vote, provided the total minor weight and the other parameters converge as stated. The same oceanic game can therefore stand for many finite approximating sequences. The integral expression also gives a precise comparison point between finite Shapley values and the geometric definition by pivotal volume. Milnor and Shapley, §1 and Theorem 1.
The mathematical result is proved in the cited memorandum, and its appendix recapitulates a limit theorem from the preceding work in the series. The formalization work is to state and prove these known claims over Lean's finite index types, Lebesgue measure, integrals, and limits. Reusable components include the quota-game characteristic function and the interface between a finite Shapley value and a changing number of minor players. The mission does not claim that the historical theorem is open, nor that these target statements already have machine-checked proofs.
The number of minor players changes with , so the finite Shapley sum does not have a fixed set of coalitions. Merely taking a limit term by term in that sum does not justify its limit: the number and weights of the terms also change. The condition that the largest minor weight tends to zero controls a triangular family of games, while the oceanic definition is a measure of a geometric pivotal event. Matching the two descriptions requires care at the quota boundaries and at intervals that may be empty. These are the central issues represented by the appendix milestone and by equations (3.4)–(3.6). Milnor and Shapley, §3 and Appendix.
The Lean model uses Fin m for major players and Fin (n l) for minor players at stage , concatenated with majors first. It uses a real-valued quota characteristic function, the published finite Shapley-value definition, and product Lebesgue volume on the cube for uniform insertion positions. The predecessor relation is strict, , exactly as in §2; the complementary cell relation is weak. The pivotal inequalities follow (2.4), and the oceanic value is defined from their volume. Defining it as would make the comparison demanded by Theorem 1 empty, so that equality remains a theorem-level obligation.
The source defines oceanic games with , , and . The finite approximants are read as weighted majority games with nonnegative weights; that condition is explicit in Lean. No sign condition is imposed on the stage quotas , since (3.2) states none (only the limit satisfies ). The statement does not impose the footnote's upper bound because Theorem 1 only concerns major-player values, which are zero in a null game. An empty minor list is permitted at an early stage. Rather than taking the maximum of an empty list, Lean says that for each , all minor weights are eventually at most ; with nonnegative weights this is the paper's vanishing-maximum condition. A positive limiting ocean weight also excludes an eventually empty minor population.
The integral in (A.3) is a set integral over the stated intersection of closed intervals, so an empty intersection contributes zero. For (3.5), the endpoints are clamped to . The condition ensures is nonnegative before it is represented as a natural-number exponent. Contributions that strengthen the measure-theoretic partition, the cell-volume computation, or the varying-population finite limit are within scope; a proof may use other intermediate lemmas while keeping the sourced target statements unchanged.
A retailer deciding which variants of a product to carry (colors, sizes, flavors) trades the extra sales that variety brings against the inventory cost of stocking many low-volume items. van Ryzin and Mahajan (Management Science 45(11), 1999) gave the first model that couples a multinomial logit (MNL) choice model of consumer substitution with newsvendor inventory costs, and showed that the resulting assortment problem has a simple structure. Their paper is a standard starting point of the assortment-planning literature in operations management: the "popular set" structure it proves is the benchmark that later work on assortment optimization under MNL demand (with capacity constraints, dynamic substitution, or other choice models) compares against.
This mission formalizes the paper's first main result, Theorem 1, together with the facts its proof rests on.
A store offers a subset of the variants of a category. Each variant has an MNL preference , and the option of buying nothing has preference . A customer facing buys variant with probability
Variants are labelled so that , and the most-popular sets are .
The retailer sells at price and buys at unit cost , with , and stocks units of each variant before the season. The critical fractile is , with the standard normal distribution function. Two models of aggregate demand are considered, both with store volume :
The assortment problem is for or .
For Lemma 1, fix and let be the preference of a variant added to it: , and are the numerators of the profit after the addition, and , .
For each demand model there is a most-popular set that is optimal among all assortments:
The paper prints for both models. In the independent model the empty assortment can be the unique optimum (when , for instance at small ), so is allowed there; the trend-following range is the printed one.
The search over assortments is a priori a search over subsets. Theorem 1 cuts it to the nested sets , so the optimal assortment is found by comparing numbers. The result is not obvious: the paper's example (, , ) shows that can beat , so the best assortment of a given size need not be the most popular one, and yet the overall optimum is always a most-popular set. The structure is used in the paper's own comparative statics (how optimal variety moves with price, store volume and the no-purchase preference) and its comparison of fashion categories under majorization, which are the other two missions of this series.
The theorem is proved in the paper; nothing here is open. To our knowledge no part of it, nor the closed-form normal newsvendor optimum (7), has a machine-checked proof. Formalizing it fixes the edge cases the printed statement glosses over (the empty assortment, the boundary) and produces reusable pieces: the normal newsvendor profit formula and Mangasarian's ratio criterion for quasiconvexity.
The obvious argument, "add variants in order of popularity", fails because adding a variant both brings new sales and cannibalizes the shares of the others, and the inventory term is concave in the shares, so profit is not monotone or submodular in in any simple sense. The proof instead compares a set with the sets obtained by removing its least popular member or exchanging it for a more popular outside variant, and needs the profit after adding a variant of preference to be quasi-convex in . That quasi-convexity is not visible from (7) directly; it requires rewriting the profit as a ratio with affine and proving convex, which in turn needs concavity of . The exchange argument must also handle ties among the , which the printed proof passes over. Milestone 1 needs the derivative of the normal newsvendor objective and the identity , neither of which is in Mathlib in this form.
Fin n, 0-based: the paper's variant is index , is the set of indices below , and the paper's is the first entry v ⟨0, _⟩. The no-purchase preference is a separate real v0, never a variant. Preferences are strictly positive and the sorting is the hypothesis Antitone v.gaussianReal 0 1; a separate theorem states and uniqueness.Real.rpow, so . At this keeps (7) correct (), but then fails; that one clause carries . The goal keeps .max · 0. In (11), multiplies both terms; the printed (11) has it on the sum only, which would break unless .Needed infrastructure: the normal loss function and the first-order condition for the newsvendor under gaussianReal; quasiconvexity of convex-over-positive-affine ratios; concavity of weighted geometric means. The newsvendor and quasiconvexity pieces are reusable well beyond this mission. Proofs of any milestone, and alternative routes to Theorem 1 that avoid Lemma 1, are welcome.
Burn-in is the final reliability test of integrated circuits: boards loaded with chips are held in an oven at elevated temperature for a minimum specified time, so that marginal devices fail before shipment. An oven holds several boards at once, and a load may stay in the oven longer than its specification but never shorter. Lee, Uzsoy and Martin-Vega (Oper. Res. 40(4), 1992) model such an oven as a batch processing machine and study the resulting scheduling problems. Burn-in is often the bottleneck of the test stage, which is why throughput (makespan) and due-date performance on several ovens in parallel are of practical interest.
This mission covers the paper's makespan result for parallel ovens. On ordinary identical parallel machines, Graham (SIAM J. Appl. Math. 17, 1969) proved that the LPT rule (list the jobs longest first and give each to the machine that frees up first) has worst-case ratio on machines. The paper shows that the same factor holds for batch machines once the jobs are first grouped into full batches of the longest jobs.
There are jobs with processing times , all available at time , and identical batch processing machines. Each machine processes up to jobs at the same time. A batch is a set of at most jobs processed together; once started it cannot be interrupted or joined, and its batch time is that of its longest job,
A schedule forms the jobs into disjoint nonempty batches covering all jobs, assigns each batch to a machine, and runs every machine's batches back to back from time . The makespan is the largest machine load, the total batch time on a machine. The problem of minimizing it is written , and denotes its optimal value, over every way of forming batches (any sizes up to , any grouping) and every assignment. For it is the classical problem .
Algorithm BLPT.
is the resulting makespan.
For the optional lateness result, each job also has a due date . The maximum lateness of a schedule is , is its value under BLPT, its optimum and .
It is claimed for every run of BLPT, whatever order the algorithm gives to equal processing times and equal batch times.
Proposition 3 gives a constant-factor guarantee for a strongly NP-hard problem. The guarantee does not depend on , whereas arbitrary batch list scheduling only gets (Proposition 1 of the same paper). For one machine the factor is , so BLPT is then exact. Proposition 2 is a structural statement: it fixes the batch composition of an optimal schedule before any assignment decision. It turns the batch problem into an ordinary parallel-machine problem, so other results for transfer as well. Proposition 5 carries the guarantee over to maximum lateness, measured relative to because may be negative.
All results are proved in the paper, Proposition 3 by a one-line appeal to Proposition 2 and Graham. This mission produces machine-checked versions of the reduction and the bound. Graham's LPT bound itself is not formalized anywhere on the platform. Its proof here is a reusable result about the published list-scheduling definitions, independent of batching.
The obvious argument is "batch as in Step 1, then apply Graham". It has two gaps. First, ranges over all batchings, and an optimal schedule need not use full batches or consecutive jobs. The exchange argument behind Proposition 2 has to move jobs between batches, possibly on different machines, without increasing any machine's load. Ties among equal processing times also have to be handled, since the claim is made for every longest-first ranking. Second, Graham's bound is not on the platform and has to be proved. It is a finite combinatorial statement, but its known proofs are not short. Proposition 5 additionally needs the bound for sub-instances formed by a prefix of the batches.
Jobs are Fin n, 0-based. Processing times are real, p : Fin n → ℝ with 0 < p j; due dates (Proposition 5 only) are d : Fin n → ℝ with 0 ≤ d j. A batching is a list of nonempty, pairwise disjoint Finsets of size at most B covering every job. The batch time is the maximum of p over the batch.
Machine loads, assignments, the per-batching optimum and list scheduling reuse the published definitions NumStochOpt.ListScheduling.ListSchedule (firstAvailable, lsLoads, listMakespan) and NumStochOpt.ListScheduling.Makespan (machineLoad, makespan, optMakespan) from the Rinnooy Kan–Stougie mission, applied to the sequence of batch times (padded with zeros beyond the last batch, which these definitions never read). is the infimum of optMakespan over all valid batchings, never only over the consecutive ones of Step 1, which would assume Proposition 2.
Explicit readings of the paper's phrases:
p;List.toChunks B of that list;Proposition 5 adds the hypothesis , which the paper's proof uses but does not print. It also makes positive, so the printed ratios are well defined. Running times and the paper's other algorithms are out of scope.
A statement with restricted to consecutive batches, a sorry-free bound obtained from a degenerate or empty-job reading, or a BLPT fixed to one convenient tie-break would trivialize or weaken the goal and is ruled out by the statements as posed. Welcome contributions: Graham's LPT bound on the published list-scheduling definitions (reusable for any work), the exchange lemma behind Proposition 2, and the permutation invariance of optMakespan under reordering of items.
A finite graph has distances defined by the lengths of its shortest paths. Representing those distances inside a normed vector space lets geometric language describe a combinatorial object, but the number of coordinates required can depend sharply on the graph. The isometric dimension asks for the smallest dimension of any real normed space that preserves every graph distance exactly. Linial, London, and Rabinovich study this invariant alongside metric embeddings and algorithmic uses of graph geometry in their 1995 paper. The cube is a useful test case: its vertices already have an obvious coordinate description, while the theorem must show that no different norm compresses those exact distances into fewer coordinates.
The paper's Section 5.3 relates isometric dimension to the rank of a matrix recording vertex distances in a maximum norm. It then computes the dimension of an even cycle and uses an isometric cycle inside the cube. These are known results of the paper, not an open conjecture. The mission isolates the rank characterization, the cycle calculation, and the cube calculation as reusable formal targets.
For a finite connected simple graph , let be the minimum number of edges in a path from to . A norm on is nonnegative, vanishes only at zero, satisfies , and obeys . An isometric embedding is a map such that for every pair of vertices. The number is the least for which some norm and some such map exist. The paper states the more general metric-space definition in Definition 2.1 and adopts connected graphs as the standing convention in Section 5.1 (pp. 218–219, 229).
The -cube has binary strings as vertices. Two strings are adjacent when exactly one coordinate differs. Its graph distance is the Hamming distance, the number of differing coordinates. For , the even cycle has vertices in cyclic order, each adjacent to its two neighbors. A graph is an isometric subgraph of when its distances between its own vertices agree with their distances in .
An real matrix implements when the maximum absolute coordinate difference between rows and is , for every pair. The number of columns is allowed to vary; the matrix rank is its ordinary linear-algebraic rank. This is the matrix object in Theorem 5.7, p. 232.
The first main intermediate target is the rank characterization
The next is the even-cycle result, stated for :
The goal is Corollary 5.12, p. 233, for every positive integer :
The milestone list also records the isometric-subgraph lower bound, the nonsingularity of the distance matrix of a path, an isometric embedding of the cube into , and an isometric inside the cube. The paper's proof of the corollary names the last two facts in consecutive sentences (p. 233).
The upper bound says the familiar binary coordinates suffice: the cube embeds in with all distances preserved. The lower bound is stronger than a claim about that particular norm or embedding. It rules out every real normed space of dimension below , regardless of its norm. The even cycle provides a separate exact dimension calculation, while Theorem 5.7 gives a matrix-rank way to study other finite graph metrics. These statements separate the graph invariant from whichever embedding happens to be easiest to draw (Section 5.3, pp. 232–233).
The paper proves these claims mathematically. The remaining formalization work is to build machine-checked proofs of their precise statements, including the finite-dimensional norm interface, graph-distance calculations, implementing matrices, and the rank lower bound. The definitions of normed realization and implementing matrix can be reused for other graphs; the path-distance determinant can be used independently of graph embedding questions. The mission's theorem files are open proof targets, not claims that these proofs have already been checked in Lean.
Placing binary cube vertices in gives an immediate candidate for an upper bound, but it cannot by itself exclude embeddings into lower-dimensional spaces with a different norm. The lower bound has to control all norms. Theorem 5.7 converts that unrestricted geometric question into a rank statement for every implementing matrix, and Proposition 5.10 supplies the exact cycle dimension needed by the cube argument (pp. 232–233).
The paper's printed proof of Proposition 5.10 first obtains only , then says a more careful analysis yields without spelling it out. That final rank step is a genuine proof obligation for solvers; the stated proposition and its use in Corollary 5.12 are retained exactly (p. 233). The path-distance matrix cited in that proof is nonsingular when its size is at least two; size one would be a zero matrix.
Lean represents an arbitrary -dimensional real normed space by a norm function on Fin d → ℝ. This includes every finite-dimensional real normed space up to a choice of coordinates. The isoDim definition takes the least natural-number dimension admitting an isometric embedding, with equality of distances for every vertex pair. The graph metric comes from SimpleGraph.dist; connectedness is explicit where the paper assumes it. The cube is the graph on Fin m → Bool with Hamming-distance-one adjacency, and is Mathlib's cycleGraph (2 * m). The goal assumes ; its case is direct, while the cycle milestones use . A zero-dimensional cube consists of one vertex and is covered by the auxiliary upper-bound statement, though the goal follows the paper's positive-dimensional convention.
An implementing matrix has arbitrary finite column count. Instead of taking a maximum over an empty index set, the formal definition requires all column differences to be bounded by the graph distance and a column to attain that distance for distinct rows. This agrees with the paper's maximum formula whenever columns are present and handles a one-vertex graph with zero columns. Matrix rank is taken over ; the path-distance matrix has entries for indices . The infimum over achievable dimensions or ranks is a minimum, since these are nonempty subsets of for finite connected graphs. No asymptotic or bound occurs in these targets, so there is no hidden constant to instantiate.
The statements require genuine norm axioms and exact graph distances. Allowing a seminorm, assuming the desired dimension bound, or replacing the cube by a path would empty the main claim. Useful contributions include the cube-distance calculation, the path determinant, an exact even-cycle lower bound, and the general rank characterization. The paper makes no running-time claim for these particular results; no algorithmic complexity assertion is included.
In online prediction, a learner makes a forecast before seeing the next label. A collection of other forecasters may offer useful advice, but the learner need not know beforehand which forecaster will perform well. Littlestone and Warmuth's Weighted Majority Algorithm (WM) gives a deterministic way to combine such advice. Its guarantees hold for every finite sequence of instances and labels, including sequences chosen without any probability model. That worst-case setting is useful when the reliability of the forecasters can change or when no data-generating distribution has been justified. The paper develops WM and several variants; this mission isolates its basic mistake bound. Littlestone and Warmuth, 1994.
A finite pool has members, each of which predicts either or on every trial. The true label on trial is , and member predicts . The master prediction is . Pool members may themselves be learning algorithms, so their predictions may reflect all earlier labels. The mission treats their prediction vectors and the labels as arbitrary finite sequences; no independence or stationarity is assumed.
Each member begins with a strictly positive real weight . Before trial , let be its current weight. For , let be the sum of weights of members predicting . WM predicts the value with the larger backing total. When the two totals tie, either binary prediction is allowed. After the label is revealed, WM changes weights only if its own prediction was wrong. On such a trial, each member that predicted the wrong label has its weight multiplied by a fixed factor with ; every other member retains its weight. If WM predicted correctly, every weight stays as it was. This is the version of the algorithm stated in §1 of the paper. A footnote there says the bounds also apply to the variant that updates on every trial. Littlestone and Warmuth, 1994, p. 215.
Write for the total pool weight at a trial boundary. Thus and after trials. Let count the trials with . The default initial weights in the paper are all one, but its Theorem 2.1 permits arbitrary positive initial weights. Littlestone and Warmuth, 1994, pp. 220–221.
The two milestones state the weight facts used immediately before and within Theorem 2.1. First, on each trial where WM errs,
Across the whole sequence, with master mistakes, the corresponding estimate is
The goal is the paper's Theorem 2.1, retaining its explicit constant:
The logarithm base is immaterial because the same base occurs above and below the fraction. The paper explicitly uses this convention for ratios of logarithms. The positive-final-weight condition represents the paper's statement that the displayed logarithmic bound is vacuous when all weight has vanished, which can happen for . The whole-sequence weight estimate remains meaningful in that case. Littlestone and Warmuth, 1994, pp. 220–221.
The result limits the mistakes of a master predictor without assigning probabilities to the predictions or labels. It relates a visible property of the run, the reduction of total weight, to the number of master errors. Later bounds in the paper use this starting point to compare WM with an individual pool member and to analyze related algorithms; this mission fixes the initial, exact-constant result on which those comparisons rest. The case includes the paper's Halving Algorithm interpretation when initial weights are equal. Littlestone and Warmuth, 1994, pp. 215, 221–222.
The mathematical theorem is proved in the 1994 paper. The remaining task here is to represent its algorithm and finite-sequence bound in Lean and supply machine-checked proofs. A complete development would give later formalizations a reusable finite-pool voting and weight-update model, along with a checked potential estimate. The local draft statements compile; their proofs remain open. A separate, sorry-free local check constructs a run for every finite prediction and label sequence with a nonempty pool and valid weights and parameter, so the quantified run relation has witnesses.
The master can be wrong even when some pool members are right, and members may change their predictions over time. Counting one member's errors therefore does not directly control the master's error count. The exact contraction constant also depends on which side of a weighted vote the master chose, including the permitted tie case. When , a single mistake can erase all weight backing the wrong label, so the logarithmic expression must be interpreted with care if no positive weight remains. These are features of the stated algorithm, rather than assumptions about how the sequence was generated.
The formalization indexes pool members by Fin n and trials by Fin T. Booleans represent binary predictions and labels; weights and are real. A WM run is a relation on the full sequence of weights and master predictions, admitting every choice at a tied vote. Its update rule changes weights only after a master mistake, scales exactly the members that disagreed with the label, and leaves all other weights unchanged. Theorems require and strictly positive initial member weights. The goal additionally requires , while the two weight inequalities permit . Natural logarithms instantiate the paper's common-base logarithm convention. Finite sums and a finite mistake count match the paper's finite-sequence convention.
The statement ranges over arbitrary pool predictions and labels, so it cannot be satisfied merely by selecting an easy input sequence. The run relation allows both legal outcomes of a tie; selecting one favorable tie rule would weaken the target. The sorry-free run-existence check also rules out a vacuous theorem caused by an inconsistent update relation. The paper's update-on-every-trial variant, its member-specific corollaries, and its later algorithms are outside this mission's goal.
A completed formalization needs finite sums of real weights, cardinalities of finite sets of mistake trials, a finite induction over trial boundaries, and real logarithm inequalities. The run definition and the first two bounds can be reused in the later parts of this paper's formalization. Contributions that prove the exact stated milestones or supply supporting facts about legal runs and nonnegative weights are within scope.
Semiconductor burn-in tests hold several jobs in an oven at once. A production planner must decide which jobs share each oven run and in what order those runs take place. A job may become available only after earlier manufacturing steps, and a due date marks when its test should finish. The planning objective here is to minimize how many jobs finish after their due dates. Lee, Uzsoy, and Martin-Vega studied this batch scheduling problem and gave a dynamic program for the case of equal processing times and compatible release and due-date orders (Lee, Uzsoy, and Martin-Vega 1992, §4, pp. 770–771).
There are jobs and one batch processing machine with capacity . Job has release time , due date , and processing time . In the main problem every processing time equals a common value . A batch is a nonempty set of at most jobs. Its processing time is the longest processing time among its members; it begins only after all its jobs have been released and the previous batch has finished. Processing is uninterrupted. A schedule is an ordered list of disjoint batches that covers every job. Each batch starts at the earliest time allowed by these conditions.
The completion time of job in schedule is the completion time of its batch. A job is on time when and tardy when . Write and let be the minimum of over all valid complete batch schedules. Tardy jobs still belong to a schedule and consume machine time. An on-time batch is one whose every member is on time.
For the structural lemmas, agreeable release times and due dates mean that implies . For the dynamic program, jobs are indexed so that both and are nondecreasing. A batch is in batch-EDD order relative to later batches when no job in it has a later due date than a job in a later batch. A batch of consecutive jobs contains exactly an index interval. These are the paper's Lemmas 4 and 5 and Definition 1 (pp. 767, 770).
Lemma 4 asserts that some optimum has an initial list of wholly on-time batches in batch-EDD order, followed by batches containing only tardy jobs. Lemma 5 asserts that some optimum has every wholly on-time batch made of consecutive indexed jobs. These are existence statements about schedules of all jobs; neither restricts the feasible schedules over which is defined.
Let be the table defined by Algorithm DP3 for the first jobs and a selected count of on-time jobs. Its boundary values are and for . For , it takes the minimum of and the eligible transitions that append a batch of jobs, . A transition uses and is eligible when that completion time does not exceed . The main target is
The maximum includes zero, which is always feasible in the table. The printed range begins at one and has no value when every job is tardy. This is the corrected boundary reading of the displayed answer on p. 771 (source).
The paper also gives a variant for jobs available at time zero, with nondecreasing processing times and due dates. Its transition replaces the release-time maximum and common by . The corresponding correctness statement is a further milestone (p. 771).
The structural results connect the optimization over arbitrary complete batch schedules to the restricted arrangements represented by the table. DP3 correctness then identifies the number of tardy jobs from finite table entries, including instances with no on-time job. The variable-time extension covers the related case where each job has its own duration but all jobs are available together.
The paper proves these results informally; this mission leaves their Lean proofs open. A complete formalization would supply reusable definitions of batch schedules, release-limited completion times, tardy-job counts, and a finite dynamic program with an explicit infinite value. The machine-checked statements and the local instance check establish the interface for that work, while the structural and correctness theorems remain solver targets.
The objective ranges over every valid batching and every processing order. The table examines an indexed prefix and places the last on-time batch among consecutive jobs. Establishing that the table's choices preserve the full optimum requires the existence statements in Lemmas 4 and 5. Reordering jobs is delicate because delaying a batch can change release feasibility and can make an earlier on-time job late. Equal due dates also require care: a due-date order alone need not put the latest release of a proposed batch at its last index.
Jobs use Fin n, with index zero representing the paper's job 1; the table's is a prefix length. Data and completion times are natural numbers, matching the paper's integer-data setting; in the table is WithTop ℕ. The schedule model uses nonempty batches of cardinality at most , pairwise disjointness, and complete coverage. A batch starts at the maximum of its latest release and the preceding completion time. This earliest-start convention is sufficient for minimizing the regular tardy-job objective. The empty job set is included: its empty schedule has zero tardy jobs.
The strict implication makes the paper's loose “agreeable” condition precise without forcing equal due dates for tied release times. For the recurrence, both release times and due dates are nondecreasing in job index, including their ties. This ensures that is the last batch's latest release and its earliest due date. The variable-time version similarly indexes by nondecreasing processing times and due dates, so the last job gives the batch duration. The table uses a minimum over exactly the paper's range , with an empty range giving . Zero is included in the final maximum. Tardy jobs are scheduled in the underlying optimum; defining the optimum as an on-time subset or defining the table as that optimum would erase the two structural claims.
This mission covers correctness only. The paper's running-time statement and the bisection procedure are outside the formalization because they would need a specified computational cost model. The paper's FBEDD remark for this objective is also excluded: a three-job instance contradicts it. Contributions to the open theorem proofs, schedule-existence facts, and reusable batch scheduling lemmas are welcome.
In a two-machine flow shop, each of jobs is processed first on machine and then on machine , and the order of the jobs is to be chosen. For the makespan (the finishing time of the last job), Johnson (1954) gave an exact sorting rule. For the sum (equivalently, the mean) of the completion times, no such rule is known: the problem is NP-hard in the strong sense (Garey, Johnson and Sethi, 1976), and exact methods search the sequences implicitly.
Ignall and Schrage (1965) were among the first to apply branch and bound to sequencing. They view the sequences as the leaves of a tree of partial sequences, keep a list of partial sequences ranked by a lower bound, and always extend the most promising one. For the two-machine mean-completion-time problem they introduced a lower bound, built from two relaxations (one where machine is the bottleneck, one where machine is), that became the template for many later flow-shop bounds.
There are jobs; job has processing time on machine and on machine . A sequence is a permutation of the jobs, processed in that order on both machines with every operation started as early as possible. The completion time of job is the time machine finishes it, and the objective is .
A node is a partial sequence of jobs; is the set of the jobs not in it; is the last job of and its completion time; () are the completion times of the jobs of . For an ordering of ,
and for an ordering of ,
and are their minima over all orderings of , and the lower bound of the node is
The procedure starts with a list holding only the empty node. A step removes the first node, creates one child for every unscheduled job by appending it, and inserts the children into the list ranked by (a new node goes before old nodes with equal bound). It stops the first time the first node of the list is terminal, i.e. has scheduled jobs, so that its last job is forced.
For all real data, (i) the procedure reaches a list whose first node is terminal, and (ii) whenever that happens, the sequence formed by and its one unscheduled job satisfies
The goal is the correctness of the paper's algorithm for the two-machine problem: the sequence it returns is optimal, not merely good, and it returns one for every input. The lower-bound milestones are the paper's own justification of its bound, and the sorting milestones show that the bound is computable in per node rather than by a minimization over orderings.
On the formal side, no item on the platform treats flow-shop lower bounds or branch and bound over sequences; the nearest is the branch-and-bound mission for jointly constrained biconvex programs (BiconvexProg.BranchBound, Al-Khayyal and Falk 1983), an unrelated algorithm over boxes. The paper's arguments are short and informal ("it should be evident"); the formalization makes explicit that the bound holds for every order and every input, which the paper derives only by analogy with . The published definitions of Johnson's as-soon-as-possible schedule (from the Johnson 1954 missions) are reused for the completion times.
The two halves of the bound are relaxations of different kinds. ignores waiting on machine ; ignores idle time on machine after its first job of and replaces that job's machine- time by the smallest one. The paper's description of as "the sum of the completion times" when is not an identity, since replaces ; only the inequality is true, and it has to be proved for the given order directly. The sorting claims are rearrangement inequalities, with the coefficient decreasing in the position.
The goal is a statement about all sequences, while the procedure only ever looks at the nodes on its list, whose length changes at every step. The tempting one-line justification, that the first terminal node has the smallest bound, says nothing by itself about sequences that are not descendants of nodes still on the list, nor about whether the bound of a terminal node is the value of its sequence; and termination of the search has to be shown, not assumed.
Fin n (the paper's shifted to ); processing times are arbitrary reals, with no sign condition; all statements are true without one.asapC2 (referenced definition JohnsonFlowShop.TwoStage.asapStart2). The objective is the sum of the completion times; the paper's mean differs by the fixed factor .Proofs of any milestone, and reusable lemmas on as-soon-as-possible two-machine schedules (completion times of a prefix, monotonicity in the start time), are welcome.
Kelso and Crawford's 1982 Econometrica paper studies a labor market in which firms hire sets of heterogeneous workers at individually negotiated salaries. Their existence results for the core and for competitive equilibrium, and the convergence of their salary-adjustment process, all rest on one hypothesis about each firm's technology, the gross-substitutes condition (GS): raising some workers' salaries never makes a firm drop a worker whose salary did not change. The condition has since become central to matching with contracts, ascending auctions and the theory of discrete convexity (Hatfield and Milgrom 2005; Fujishige and Yang 2003). It is defined through the firm's demand correspondence rather than through the production function, so its economic content is not obvious.
Section 6 of the paper explains that content. Its first result, Theorem 6, says that when workers are alike in production, (GS) is exactly the familiar requirement of nonincreasing returns to workers. This mission formalizes Theorem 6, the two halves of its proof, and the companion claim that with two heterogeneous workers (GS) is equivalent to subadditivity.
Fix a finite set of workers and a single firm. Its production technology is a function ; is the gross product when the firm hires the set . A salary vector assigns to each worker the salary the firm must pay to hire him or her. The firm's net profit is
and is demanded at , written , if it maximizes over all subsets of (problem (A) of the paper). The technology satisfies (GS) if for all salary vectors and every there is with
Workers are alike in production when the product depends only on how many are hired: for some . The workers remain distinct individuals, since their salaries can differ. The function has nonincreasing returns to workers (DR) if
A technology is subadditive if for disjoint .
In the Lean development these are profit, IsDemanded, GrossSubstitutesOn y Set.univ, DR (Fintype.card W) ybar and Subadditive y, in the namespace KelsoCrawford.Returns.
For every ,
then violates (GS). 3. Two workers (p. 1500), off the goal's path: if and , then satisfies (GS) if and only if is subadditive, that is .
The result itself. Theorem 6 gives a production-side reading of (GS): restricted to identical workers it is nonincreasing returns, so (GS) can be viewed as the generalization of that convexity condition to heterogeneous workers. The paper uses this reading to explain why something like (GS) is needed for existence: without it the core and the competitive equilibrium may fail to exist, as the example of Section 6 shows (mission 7 of this series). The two-worker claim locates the boundary further: with two workers (GS) is subadditivity, while with three or more subadditivity is no longer enough.
Formalizing it. Nothing of this paper was on Prove2Me before this series. Theorem 6 is a proved result in the paper. This draft provides compiling Lean statements of both directions, with (GS) in the paper's own form (real salary vectors and the set ), and of the two-worker characterization; their proofs remain open. A completed mission would provide machine-checked proofs of those statements. The statements fix the boundary conventions exactly (which are constrained, what happens with zero or one worker), which the informal argument leaves implicit. The definitions of profit, demand and (GS) are the same as in the other missions of the series (1–5 and 7), so proofs here are reusable there.
For (DR) (GS), the natural argument sorts workers by salary and observes that a profit-maximizing firm hires the cheapest workers. With ties among salaries this description is not literally true (any cheapest workers will do), and after a salary increase the new optimal size and the new ranking change at once; showing that some new maximizer keeps every worker whose salary stayed fixed requires a careful exchange argument rather than a monotone comparison of indices. For the converse, a single failure of (DR) must be turned into an explicit pair of salary vectors; the construction must make one worker strictly demanded before the change and strictly undemanded after it, which requires controlling every competing set, not only the sets of the critical sizes and . The two-worker characterization requires a case analysis over the four candidate demands at every salary pair, including ties.
Workers form an arbitrary finite type W with m = Fintype.card W; a technology is a function Finset W → ℝ, and "alike in production" is the technology fun C => ybar C.card with ybar : ℕ → ℝ. Salaries are arbitrary real vectors W → ℝ, and (GS) is required on all of (Set.univ), the continuous version that Theorem 6 is about. A discrete market can satisfy (GS) on its salary grid while its continuous version does not, so the discrete version is a different statement and is not targeted here. (DR) is written for natural numbers with 1 ≤ w and w + 1 ≤ m, so that w - 1 never truncates. For it is vacuous, and no lower bound on is imposed. Neither (MP) nor (NFL), , is assumed in Theorem 6: the paper uses neither, and adding them would weaken the theorem. The two-worker claim keeps the paper's normalization and uses its general definition of subadditivity over disjoint pairs.
A trivializing formalization would restrict (GS) to a single salary vector, quantify demand over a subfamily of sets, or replace "some demanded set contains " by "the given set does", and is ruled out by the definitions above, which follow the paper's (A) and (GS) word for word. The read-out of the goal as two milestones is the paper's own split of its proof.
Infrastructure needed: finite sums over Finset, sorting of a finite salary vector, and elementary facts on concave sequences. Contributions that would be reusable beyond this mission include a general lemma that concave functions of cardinality yield gross-substitutes demand, and the link between (GS) and M-concavity of set functions (Murota's gross-substitutes axioms are on Prove2Me as Shuze Chen's DiscreteConvex_MConvexFunctionsC_MNatGS, a related but different object: one price per good and integer bundles). Proofs of either direction, of the two-worker claim, or of intermediate lemmas are welcome.
An optimization problem often changes when a parameter changes: a price rises, a constraint expands, or a strategic environment shifts. Comparative statics asks whether the optimal choice moves in a predictable direction. The usual numerical tools, such as derivatives, can be unavailable when choices form a discrete set or the objective is neither smooth nor concave. Milgrom and Shannon's Monotonicity Theorem gives a condition expressed entirely through order and preference comparisons. It applies to individual optimization problems and supplies the order argument used later in their paper for games with strategic complementarities.
Their 1994 paper moves beyond cardinal conditions such as supermodularity and increasing differences. Those conditions imply useful comparative statics, but they can change under a strictly increasing transformation of the objective even though every argmax set stays the same. Quasisupermodularity and single crossing describe the comparisons that actually govern the argmax. The theorem characterizes these conditions through the behavior of optimizers over all constraint sets, rather than giving only a sufficient test. The historical relationship and the claims in this paragraph are described in Milgrom and Shannon, Sections 1–2.
Let be a lattice: a partially ordered choice set in which every two choices have a meet and a join . Let be a partially ordered parameter set and an objective. For any constraint set , define the possibly empty maximizer set
The strong set order, written , compares subsets of the lattice by requiring and for every and . It can compare feasible sets as well as sets of optimizers. On singleton sets it agrees with the order on . It also holds vacuously if either set is empty; it is reflexive at exactly when is a sublattice. These are the paper's conventions on page 159.
A function is quasisupermodular if, for every , both
hold. The single crossing property of in requires, whenever and , that a weak or strict preference for over at remains respectively weak or strict at . The strict version sends even a weak preference at to a strict one at . These definitions are given on pages 160 and 162.
The main target is Theorem 4 on page 162:
The milestone list records the two necessity claims and the sufficiency claim separately, using the three corresponding passages of the paper's proof. The goal keeps both directions together. It imposes no restriction on which subsets may be used as constraints.
Corollary 1 characterizes quasisupermodularity alone through monotonicity as the constraint set changes, with no varying parameter. Corollary 2 says that the maximizers over a sublattice themselves form a sublattice. The reflexivity remark identifies when holds. Theorem 4′ uses the strict single crossing property and a nondecreasing feasible-set correspondence to conclude that every selection of maximizers is nondecreasing. These nearby results share the definition layer with the main theorem and give distinct targets for the formal development.
The equivalence turns an order property of an entire family of optimization problems into two properties of the objective. In particular, its converse shows that if every feasible-set comparison produces monotone maximizers, then quasisupermodularity and single crossing are forced. This matters for problems where an analyst can reason about choice behavior more directly than about algebraic properties of . The corollaries also separate the effects of constraints and parameters and describe the structure of the optimal-choice set. The paper develops these consequences on pages 162–163.
The theorem is proved in the paper. The remaining work here is a machine-checked Lean proof of the ordinal characterization, its two directions, and the adjacent consequences. Published Prove2Me definitions already encode the strong set order, and its Topkis series covers related cardinal hypotheses such as supermodularity and increasing differences. This mission adds the paper's quasisupermodularity and single crossing predicates and seeks formal proofs of the distinct ordinal results. The separate characterization and linear-perturbation results of the same paper are targets of the other missions in this series.
The obstacle is the interaction of two orders. An increase in changes preferences, while an increase in changes which choices can be compared. A pointwise claim that an optimizer rises does not follow from either order condition alone, particularly when maximizers tie or are incomparable. The main theorem concerns sets of maximizers under the strong set order, so both the meet and join of optimizers at two parameter–constraint pairs must land in the correct maximizing sets. Conversely, observing monotonicity for one fixed feasible set cannot establish quasisupermodularity; the equivalence relies on monotonicity across every constraint set. The weak and strict preference clauses have different roles, so replacing either by the other changes the target. These are the distinctions visible in Theorem 4 and its proof.
Lean represents with Lattice, with PartialOrder, and in curried form. No finiteness, total order, topology, measurability, or maximizer-attainment hypothesis is imposed. The paper's product order for product lattices is Lean's usual componentwise order. The imported Supermodularity.Lattices.InducedSetOrder is exactly the paper's strong set order, including its behavior on empty sets. The definition argmaxOn returns the set of points in whose objective value bounds every value attained in ; it may be empty.
Quasisupermodularity is encoded with a reusable set argument but applied to Set.univ in every theorem here, so the property concerns the whole lattice. Single crossing compares strictly ordered choices and strictly ordered parameters and preserves both weak and strict preferences. ArgmaxMonotone compares weakly ordered parameters and all constraint sets under the strong set order. Theorem 4′ encodes a selection on an arbitrary domain where maximizers actually exist; it makes no global existence assertion. For Corollary 2, an arbitrary parameter is fixed and its objective is written .
These choices rule out easy specializations that would change the theorem: taking to be a chain, restricting quasisupermodularity to a selected feasible set, demanding nonempty argmax sets, or dropping strict preference clauses. The reusable development consists of the maximizer-set definition, the two ordinal predicates, and their relation to the published strong set order. Contributions proving the goal, its three proof-direction milestones, the corollaries, and the selection theorem all fit this scope.
In a strategic game, each player evaluates a change in their own strategy using that player's own payoff. These incentives need not point in a common direction. A potential game is a case in which one real-valued function records every player's payoff change under a unilateral deviation. This common function lets questions about incentives be expressed as questions about one object on the space of strategy profiles. Monderer and Shapley's 1996 paper introduced several kinds of potential and gave a local characterization of the exact kind. The characterization is the subject of this mission.
The local test matters because the defining condition appears to require finding an unknown potential on the entire profile space. Theorem 2.8 says that a condition on four-step cycles already determines whether such a function exists, even when individual strategy sets are infinite. The paper compares this characterization with the familiar idea that a conservative field has zero integral around closed curves; here the “integral” is a finite sum of payoff changes along unilateral deviations (Monderer and Shapley, pp. 130–131).
Let be a finite set of players. For each player , let be a strategy set, and let be the set of pure strategy profiles. The payoff of player is a function . If , the notation means the profile obtained by replacing only player 's strategy with . The strategy sets themselves are not required to be finite in this section of the paper (p. 127).
An exact potential is a function such that, for every , every opponents' profile , and every ,
A game admitting such a function is an exact potential game. The paper uses the shorter term “potential game” for this class when the adjective is clear (pp. 127–128, equation (2.2)).
A path is a sequence in which each step changes exactly one player's strategy to a different value. Write for the unique player who moves from to . The path sum of the payoff vector is
The path is closed when . It is simple closed when, in addition, the vertices are pairwise distinct. Its length is , the number of steps and the number of vertices before the final return. These definitions follow pp. 128, 130–131.
For a game with finitely many players, Theorem 2.8 asserts the equivalence of all four claims:
The last condition is a local criterion, but the goal keeps the full four-way equivalence of the published theorem, p. 131. The milestone list follows five claims in its Appendix A proof: vanishing path sums from a potential, path independence, construction of a potential from vanishing closed-path sums, the local exchange of two different players' moves, and the reduction from all closed paths to length-four simple cycles (pp. 138–139).
Corollary 2.9 expresses the length-four test directly as a zero sum of payoff changes around four corners obtained by varying two players' strategies. Lemma 2.7 says that two exact potentials for the same game differ by one additive constant. Both are included as supporting statements from the same definition layer, although they are not milestones in the attack path for Theorem 2.8 (pp. 130–131).
Theorem 2.8 turns existence of a global function into a test on local cycles. Corollary 2.9 makes those cycles visible in payoff tables: fixing all but two players, the alternating sum around each two-player rectangle must vanish. For finite strategy sets this gives a direct finite collection of conditions; for infinite strategy sets the theorem remains a mathematical characterization without claiming a finite algorithm (Monderer and Shapley, p. 131).
The original paper proves these statements. The formalization work is to represent games, paths, path sums, and the four-way equivalence in Lean, then supply machine-checked proofs. The present mission contains compiled statements with open proofs. Its definition modules are also reusable for the paper's other results about potentials, improvement paths, and congestion games.
The challenging direction is that zero sums on simple length-four cycles force zero sums on every closed path. A closed path may repeat vertices and may involve more than two players. A direct appeal to the local condition does not cover such a path. The Appendix A argument uses changes to a path's sequence of deviators, and its informal treatment of adjacent moves by the same player leaves a boundary case: the two moves can cancel, so replacing them by one move would create a null step, which the definition of a path excludes. A formal proof must account for this case while preserving the paper's exact statement (pp. 138–139).
Lean represents the finite player set by a finite type and a profile by a dependent function . Strategy sets remain arbitrary types. The operation is a one-coordinate update. A finite path stores vertices and its deviator at each of the steps; the step condition determines that deviator uniquely. Closed paths of length zero are allowed and have sum zero. The paper prints , the number of players, as the upper limit of the path sum on p. 130, although its summands are indexed by path steps. The Lean definition sums over all steps, as the surrounding definition and later equations require.
The four-cycle hypothesis quantifies only over simple closed paths of exactly four genuine steps. It is not replaced by all four-step walks or by cycles with null or simultaneous deviations. The goal retains all four clauses rather than only its shortest equivalence. Corollary 2.9 explicitly requires the two varying players to be distinct; this is implicit in the paper's four-corner construction. No finite-strategy assumption is imposed on Theorem 2.8, Corollary 2.9, or Lemma 2.7.
The development needs ordinary finite sums, dependent functions, coordinate updates, and finite-indexed paths. Its path and potential definitions are intended as an interface for later work. Contributions proving any of the five source-backed milestones, the goal, or the two related statements are within scope.
How likely is a sum of independent random variables to exceed a large level ? If the summands have exponential moments, the classical answer is a Bernstein- or Hoeffding-type bound, exponentially small in . Many quantities met in statistics, queueing, insurance mathematics and the analysis of algorithms have only finitely many moments, and then no exponential bound can hold: the tail of the sum is at least as heavy as the tail of the largest summand. The Fuk–Nagaev inequality is the standard answer for this situation. It bounds by a polynomial term, which accounts for one summand being large, plus a Gaussian term, which accounts for the bulk of the sum.
The inequality was proved by D. Kh. Fuk and S. V. Nagaev in 1971 (Fuk–Nagaev 1971). S. V. Nagaev's survey of 1979 in the Annals of Probability states it as Theorem 1.3 and gives a complete proof, together with its corollaries (1.23) and (1.24). The form (1.24), , is the version quoted in the later literature on heavy-tailed sums, empirical processes and high-dimensional statistics, where it is the usual replacement for Bernstein's inequality under polynomial moments.
Let be independent real random variables on a probability space, with distribution functions , and let . Fix a level , truncation levels (positive numbers), and a number .
The truncated summands are if and if , with sum . The paper writes , and for sums of truncated means, second moments and absolute moments of order , the arguments being the truncation levels. The three used here are
For , and , write and define
Finally and .
In Lean these are the definitions S, Xt, St, muY, B2Y, AY, Atplus, Bn2, P4, P5, P6 of NagaevLD.FukNagaev.Setting.
Suppose , , and . Write (1.4) for and (1.6) for . Then
and if (1.6) holds together with or , then . The page prints the last case as "if, instead of (1.6), …"; the proof on p. 752 proves it "if, in addition", and this is what is stated.
The milestones follow the proof: the truncation inequality (1.8); the exponential Chebyshev bound with factorisation (1.9); Lemma 1.4, the cumulant bounds (1.10) and (1.11) for a variable bounded above, with the intermediate estimates (1.13) and (1.16); the bounds (1.17) and (1.18) for ; the equivalence of (1.4) with ; (1.19), under (1.4); under (1.6); and (1.20), .
Corollary 1.7 (1.23): for , , ,
Corollary 1.8 (1.24): for , , ,
Theorem 1.3 makes no assumption on the summands beyond independence and finiteness of the truncated moments; no centring, no identical distribution, no bound on the summands. The free parameters , , let a user trade the polynomial term against the Gaussian term. Corollary 1.8 is the form used for moment bounds of sums (-th moment inequalities of Rosenthal type follow by integrating it in ), for maximal inequalities, and for concentration of empirical processes indexed by heavy-tailed classes.
The result has been proved since 1971 and is not open. As far as a search of the Prove2Me catalog and of Mathlib shows, it has not been formalized: Mathlib has the exponential Chebyshev bound and the moment generating function of independent sums, but no tail inequality for sums of heavy-tailed summands. This mission produces a checked proof of the theorem in the paper's exact form, of the cumulant bound of Lemma 1.4, and of both corollaries with their explicit constants and .
The obvious argument, Chernoff's bound applied to , fails at once: without exponential moments is infinite for every . Truncating the summands repairs this, but the bound then depends on the choice of the exponent , and no single choice works for all parameters. The proof splits into cases according to the relative position of three numbers, and the minimisers , of two convex functions, and every case needs its own estimate of the cumulant of a variable bounded above. The bookkeeping of strict and non-strict inequalities across these cases is exactly what (1.7) and (1.7a) assert, and the printed text has a misprint at that point.
The corollaries need a separate step: Corollary 1.7 requires , which follows from centring only because truncation removes positive mass, and Corollary 1.8 requires combining the Chebyshev bound for with the truncated moment so that the two polynomial terms add to exactly .
X : Fin n → Ω → ℝ on a probability space, measurable and mutually independent (iIndepFun); index stands for the paper's . , , and are hypotheses ( follows from the others when ).variance is outside . On the page an infinite second moment makes each bound trivial; in Lean it would be replaced by and the statements would become false.cond_1_4, which includes the case , and (1.6) is cond_1_6, which requires . For the two are exact complements. If , and the exponential term of (1.23) take the page's limiting value , and so does the exponential term of (1.24) when ; Lean's would otherwise make them .Semiconductor wafer fabrication lines are reentrant: a wafer returns to the same photolithography or etching station many times along its route, so the parts competing for a machine are at different stages of completion. In such a line, a local dispatching rule decides at every machine which waiting part goes next, and the question is whether a given rule keeps the line stable whenever there is enough capacity. Lu and Kumar (IEEE TAC 36(12), 1991) showed that the answer depends on the rule. Some natural buffer priority rules make the line unstable even when every machine has spare capacity (their Example 1; see also Kumar and Seidman 1990). Two rules are proved stable for every route: first buffer first serve (FBFS) and last buffer first serve (LBFS).
LBFS serves at each machine the waiting part that is closest to completion. It is the "pull" rule of the two, and the one closer to practice: it minimizes work in progress in many settings and coincides with earliest due date when parts arrive in due-date order. This mission formalizes the paper's LBFS results, §V. The sibling mission (FBFS, §IV) treats the other policy on the same model.
Timeline:
A nonacyclic flow line has service centers; center has identical machines, each processing one part at a time. Every part follows the same route through buffers : in buffer it waits at center , then needs units of uninterrupted processing on one machine of that center. A center may serve several buffers.
Parts are released into ; part is released at time and exits at time , when its service at ends. Finitely many parts may be present at time , in any buffer, some already in service. With the number of releases in , the arrivals are bursty with rate and burst if
The work per machine that one part brings to center is , and the load is with . The capacity condition is (3). Also , and is the maximum per-machine work brought to a center by a part in , counting only buffers (6).
Scheduling is nonidling (a machine idles only if every buffer of its center is empty) and nonpreemptive, and a machine takes the part at the head of a buffer. Under LBFS, a machine takes a part from only if every buffer of its center with is empty. The number of parts in the system at time is .
Under (1) and (3), for every with ,
Here is the explicit constant of the delay estimate. The paper prints the second bound as ; its proof establishes the form above, which is the one posed.
The delay estimate behind the goal, in the order of its proof:
for a part that finds parts in the system on release.
Then the Pipeline Property , order preservation (parts exit in the order they enter), and the recursion (14) for the number in system along successive exit times. A further item states that LBFS is stable in the sense of §II: every delay is bounded.
Theorem 2 says the delay of a part under LBFS grows with the number of parts ahead at rate : the line behaves like a pipeline whose speed is set by its bottleneck center, although parts revisit centers. Theorem 3 converts this into a bound on work in progress that holds for all time, with an asymptotic bound that does not depend on the initial state. Together they give stability of LBFS for every route and every burst size, with explicit constants. This is a deterministic, sample-path result: no distributional assumption on arrivals is needed. Its constants are explicit, so they can be evaluated for a given line.
The results are proved in the paper; none is formalized. The mission produces a machine-checked model of a multi-server reentrant line with nonidling, nonpreemptive, head-of-buffer buffer-priority dispatch, together with Theorems 2 and 3 on it. The model carries over to the other policies of the paper (FBFS, least slack, earliest due date).
The obvious argument fails because under LBFS parts released later do interfere with a part : they occupy machines nonpreemptively at the low-priority buffers must still pass. So the delay of cannot be bounded by the work ahead of it alone. The paper's estimate is an induction from the end of the line backwards over the truncated systems , nested with an induction on the position of in its buffer. The constant is recomputed at every level from , so is halved at each level. A formal proof must also handle what the paper treats informally:
All declarations are in the namespace ReentrantScheduling.LBFS.
WithTop ℝ, with ⊤ meaning never, so a run need not serve every part, and the theorems assert that parts are served. A formalization with real-valued start times would assume every part is served, which is half of what stability asserts.Set.encard, never Set.ncard, which would count an infinite set as and make the capacity rule vacuous.The model is reusable for other dispatch rules on reentrant lines. Proofs of any milestone are welcome, as are lemmas on admissible runs (FIFO within buffers, finiteness of ).
Not posed here:
QueueingStability.LuKumar.theorem31;Most stochastic programs that arise in practice, such as two-stage stochastic linear programs with recourse, have far too many scenarios to be solved exactly. The standard remedy is sample-average approximation: draw independent observations of the random data, replace the expectation by the sample mean, and solve the resulting deterministic problem. A candidate solution found this way, or by any heuristic, comes with no guarantee. To judge it one needs a bound on its optimality gap , and estimating is routine; what is missing is a lower bound on the unknown optimal value .
Mak, Morton and Wood (Oper. Res. Lett. 24 (1999)) show that the optimal value of the sample-average problem supplies exactly this: its expectation never exceeds , and it can only move closer to as the sample size grows. The result requires almost no structure of the problem, and it underlies the batch-means confidence intervals on the optimality gap used throughout the stochastic programming literature, including the single- and two-replication procedures of Bayraksan and Morton (2006).
Timeline.
Let be a random vector with distribution on a measurable space , let be a deterministic feasible set, and let . The stochastic program is
Let be independent and identically distributed (i.i.d.) from the distribution of , defined on a probability space . The sample-average problem of size is
Its optimal value is a random variable. All the are built on the same sequence: uses its first terms and its first . Throughout, is assumed to exist for every .
For the proof structure the mission also uses the leave-one-out values
the sample-average optimal values of the subsamples of size of the first observations.
stated in the Introduction (p. 48) as the paper's main claim, with no assumption on or on beyond the existence of the relevant expectations and of optimal solutions.
Theorem 1 turns any sampling-based solver into a source of statistical lower bounds on : averaging independent replications of gives a confidence interval for a lower bound, and display (9) combines it with an upper-bound estimator into an estimator of the optimality gap that is nonnegative by construction. Theorem 2 justifies increasing the sample size: the bias is nonincreasing in . Both results are used, often without proof, in the analysis of sample-average approximation and of the gap-estimation procedures built on it.
The results are proved, in this paper and in textbooks (e.g. Shapiro, Dentcheva and Ruszczyński, Lectures on Stochastic Programming). To our knowledge none of them is machine-checked. On Prove2Me, a special case of Theorem 1 under continuity, compactness and a square-integrable envelope is posed but unproved (SolutionQuality.SRP.display1_negative_bias), and the wait-and-see inequality is proved for finitely many scenarios in an extended-real model (StochasticProg.ValueOfInfo.prop1_ws_le_rp_le_eev). This mission states the general versions, for arbitrary feasible sets and integrable costs, on a measure-theoretic i.i.d. model.
Theorem 1 is short on paper; in a formal setting its difficulty is bookkeeping: minima over arbitrary sets and expectations of possibly non-integrable functions both need explicit hypotheses to mean what the paper means. Theorem 2 is harder. The natural first attempt compares and on the same sample path, but no pathwise inequality holds in either direction: one extra observation can raise or lower the sample-average optimum. The monotonicity holds only in expectation, so any argument must use the joint law of the infinite i.i.d. sequence, including the law of its subsequences, and measurability of as a function of the sample path.
The model is the published definition file SolutionQuality.SRP.Setting: decisions lie in EuclideanSpace ℝ (Fin d), is a probability measure on , the sample is an i.i.d. sequence ξ : ℕ → Ω → Ξ (the paper's is ξ (i-1)), and , , and the optimality gap are its optValue, saaValue, gapEstimate and optGap. The mission adds skipIndex, the leave-one-out value looValue and the path law pathLaw.
Committed conventions:
sInf), and expectations are Bochner integrals. Both take the value on bad inputs, so every statement carries the hypotheses that keep them genuine:
These hypotheses are disclosed in each statement and are satisfiable: a sanity instance with a singleton satisfies all of them. A formalization that dropped the integrability of , or that allowed , would make the goal false or vacuous, and one that assumed continuity and compactness would restate the special case already on the platform; neither is in scope.
A complete development needs: the expectation of a sample mean under an i.i.d. law; the identification of the law of fun j => ξ (skipIndex i j) · with Measure.infinitePi (fun _ => μ) (Mathlib's iIndepFun_iff_map_fun_eq_infinitePi_map); and the averaging identity behind the leave-one-out decomposition. The reindexing lemma for i.i.d. sequences is reusable well beyond this mission. Proofs of the milestones, and alternative arguments for Theorem 2, are welcome.
A job shop is the basic model of a factory floor in which every job follows its own route through the machines. Minimizing the time at which the last job is finished (the finish time, or makespan) is one of the central problems of deterministic scheduling theory, and the question of which special cases admit efficient algorithms has organized much of the field since the 1950s.
For two machines the picture is sharp. Jackson (1956) showed that a two-machine job shop in which every job has at most two operations is solved by a simple rule extending Johnson's flow-shop algorithm (Jackson, Naval Research Logistics Quarterly 3, 1956; Conway, Maxwell and Miller, Theory of Scheduling, 1967, p. 105). Once a single job may have three operations, the non-preemptive problem becomes NP-complete: Lenstra, Rinnooy Kan and Brucker showed this for jobs with one nonzero task each and one job with three (Annals of Discrete Mathematics 1, 1977; a 1975 Mathematisch Centrum report is the paper's reference [1]). Gonzalez and Sahni (Operations Research 26(1), 1978) extended this boundary to preemptive schedules, in which a task may be interrupted and resumed later: even then the two-machine problem is NP-complete, already when only two jobs have three nonzero tasks. This mission formalizes that reduction, Lemma 5 together with Corollary 2 of their paper.
Timeline:
A job shop has processors and jobs . Job is a finite sequence of tasks; task of job must be processed on a given processor for time units, and for every job, task can begin only after task has been completed. Schedules start at time . A preemptive schedule assigns to every task a finite set of time intervals on its processor, of total length , such that intervals on the same processor do not overlap and every interval of task begins after task of the same job is completed. A non-preemptive schedule processes each task in a single interval. If is the time at which job is completed, the finish time is .
PARTITION: a multiset of nonnegative integers has a partition if some index set satisfies .
From , with , the paper builds the two-processor job shop with jobs:
Each processor carries load exactly . In Lean, the instance is JS a : JobShopLTAS.Core.Instance 2 (n + 2), a schedule is S : Schedule (JS a) (a finite set of pieces), and the predicates are S.IsPreemptive, S.IsNonPreemptive and S.FinishedBy (5 * T a).
For every and every ,
The result places the boundary of tractability for two-machine job shops exactly: at most two operations per job is solvable in , while two jobs with three operations make the problem NP-complete, and allowing preemption does not help. The same instance serves both schedule types, because its optimum is in either model exactly when a partition exists.
The theorem is classical and fully proved on paper; no machine-checked proof is known to exist. Formalizing it requires a precise model of preemptive schedules, which the paper treats informally, and makes explicit an argument (the "no idle time" step of Lemma 5(b)) that the paper compresses into a few sentences. The schedule model built here is shared with the other job-shop missions of this series.
Direction (a) is a concrete schedule and is bookkeeping. Direction (b) is the substance. The tempting argument "each processor has load , so a schedule of finish time has no idle time, hence some set of short jobs fills exactly on " is incomplete for preemptive schedules: the short jobs may be split into many pieces spread over the whole horizon, and , the set of short jobs that touch during , is defined by pieces rather than by whole tasks. Making the counting argument rigorous requires measuring idle time on each processor across arbitrary finite unions of intervals and tying the amount of processing done on before to the completed first tasks on .
Fin 2 with , ; jobs and tasks are 0-based, so the paper's job is job n and job is job n + 1.JobShopLTAS.Core.Instance. Schedules are finite sets of pieces (task, start, end) with positive length, following the paper's footnote 1 (p. 40). A task of length zero has no pieces and is completed when its predecessor is; it never blocks a processor.∀ j, S.jobFinish j ≤ τ; "finish time " is the existence of a job finishing after ; "finish time " in Lemma 5(a) is together with a job finishing at exactly .A multicommodity flow problem asks to route many source–sink demands through one capacitated network at the same time. Its min-cut (sparsest cut) is the smallest ratio, over all cuts, of the capacity crossing the cut to the demand separated by it. Routing is always limited by every cut, so the max-flow never exceeds the min-cut. For a single commodity the two are equal (Ford–Fulkerson); for many commodities they are not, and the size of the gap governs a large family of approximation algorithms for graph partitioning, layout and routing problems.
Leighton and Rao (J. ACM 46 (1999), extended abstract FOCS 1988) proved that for uniform problems, where every pair of nodes demands one unit, the gap is at most (their Theorem 2). This mission formalizes the other half: Section 2.1 of the paper, A bad example, which shows that the is necessary. On a 3-regular expander graph the max-flow is a factor smaller than the min-cut, so Theorem 2 cannot be improved beyond the constant.
Timeline. Ford and Fulkerson (1956) and Elias–Feinstein–Shannon (1956): single-commodity max-flow equals min-cut. Hu (1963): equality for two commodities. Leighton and Rao (1988, journal 1999): uniform and product problems have an gap, and expanders show it is tight. Klein, Agrawal, Ravi and Rao (1990) and later Linial–London–Rabinovich (Combinatorica 1995) and Aumann–Rabani (1998): an gap for general demands with commodities, tight by the same expander example.
Let be a finite set of nodes. A network assigns a capacity to every pair, symmetric and zero on the diagonal. For with complement , the cut capacity is the total capacity of the pairs with one end in and the other in .
In the uniform multicommodity flow problem (UMFP) every pair of distinct nodes is a commodity with unit demand. Its max-flow is the largest fraction such that units of every commodity can be routed simultaneously without exceeding any capacity (concurrent flow). Its min-cut is
Section 2.1 takes a 3-regular -node graph with unit edge capacities, so that is the number of edges between and , and assumes that is a -edge-expander:
for a constant . Families of such graphs exist for a sufficiently small (Margulis 1973; a random 3-regular graph has the property with high probability). Throughout, is .
For a 3-regular -edge-expander with unit capacities and ,
This is the final display of §2.1 (pp. 794–795), with the floor that the argument actually supports (see Formalization scope). It leaves the expander family unspecified: it holds for every graph with the two properties.
Theorem 1 (p. 795) states that for any there is an -node UMFP with . It is stated twice: conditionally on a family of 3-regular -expanders (the form §2.1 proves), and unconditionally, with one constant for all .
The result shows that the max-flow min-cut gap of Leighton and Rao's Theorem 2 is tight up to the constant, and, through the same example, that the bound for general demands is tight. Every approximation algorithm that rounds a multicommodity flow, or its dual, to a cut loses a factor in the worst case for this reason; improving on it, as Arora, Rao and Vazirani did (J. ACM 2009) with an approximation for sparsest cut, requires a stronger relaxation than the flow LP.
The result is classical and proved. To our knowledge it has no machine-checked proof. Formalizing it requires the concurrent-flow LP, the uniform sparsest cut, graph distance balls in bounded-degree graphs and a counting argument that converts path lengths into capacity usage; each of these is reusable. The unconditional Theorem 1 additionally needs the existence of bounded-degree expanders on every number of nodes, which is a substantial formalization project in its own right.
The min-cut bound and the ball bound are elementary. The central step is milestone 4: turning "the shortest path of a commodity has at least edges" into "the commodity uses at least units of capacity". In an arc-flow formulation a commodity is a conservation-respecting function on arcs, not a set of paths, so the step needs either a path decomposition of each commodity's flow or a weak-duality argument with unit edge lengths. The obvious attempt, summing the conservation equations directly, gives only the net flow across one cut and loses the factor .
The unconditional Theorem 1 is hard for a different reason: the paper cites the existence of 3-regular expanders and does not prove it, and the theorem asks for every , including odd , where no 3-regular graph exists.
Nodes are a Fintype with decidable equality and . A network is a symmetric nonnegative real capacity function with zero diagonal; the unit-capacity network of a simple graph has on edges and elsewhere. Commodities are ordered pairs , , each with demand (the paper's footnote 2), so each unordered pair carries one unit; a flow is a nonnegative arc flow per commodity, and both directions of an edge share its capacity. The max-flow is the supremum of feasible fractions. The min-cut ranges over nonempty proper only: at or the ratio is , which Lean reads as and which would make .
Conventions and added hypotheses:
Nat.log 2 n), a different constant in the same .SimpleGraph.IsRegularOfDegree 3.The hypotheses of the goal are satisfiable: the 3-cube () is 3-regular and a -edge-expander. Contributions welcome: the arc-flow path-length lemma, the ball bound for bounded-degree graphs, and an existence theorem for 3-regular expanders.
Solving a system of nonlinear equations , with continuously differentiable, is a basic task in numerical analysis and optimization: it is the inner step of interior-point and sequential quadratic programming methods, of implicit time-stepping for differential equations, and of equilibrium computations in operations research. Newton's method converges fast near a solution at which the derivative is invertible, but from a poor starting point it may fail. Trust region methods are a standard globalization: each step minimizes the norm of the local linear model over a ball , and the radius is shrunk or enlarged according to how well the model predicted the actual decrease of (Moré and Sorensen 1983; Dennis and Schnabel 1983, §6.4).
Eisenstat and Walker (1994) developed a general global convergence theory for inexact Newton methods, in which steps only reduce the linear model's norm by a factor and must also give sufficient decrease of . Their §4, Application 1, shows that this theory also covers trust region methods. This mission formalizes that application.
Let be a finite-dimensional real vector space with an arbitrary norm (the paper's ; the norm need not be Euclidean), and continuously differentiable with derivative . For a point and a step , the actual reduction and predicted reduction are
A point is a stationary point of if for every : no step decreases the norm of the linear model. A point is a limit point of if every ball around contains for infinitely many .
Algorithm TR is given , , and . At iteration it sets and picks a step
While , it replaces by for some and picks a new by (4.5). Then , and the next initial radius satisfies if , and otherwise. The algorithm does not break down if it generates an infinite sequence of iterates.
If Algorithm TR does not break down, then
and if is a limit point with invertible, then
The statement has no constants, and it holds for every choice the algorithm leaves open: the minimizer in (4.5), the factors , and the new radii.
An extra item, Corollary 3.6, states that such a sequence with divergent has , where (or if ).
Theorem 4.4 is a global convergence result that assumes neither bounded level sets, nor the existence of a solution, nor an inner-product norm. It separates two conclusions: without any regularity, the only possible accumulation points are stationary points of ; at an accumulation point where is invertible, the method finds a solution, converges to it, and eventually takes the full Newton step. The paper assumes only continuous differentiability, which does not by itself give a quadratic convergence rate. Lemmas 4.2 and 4.3 are local facts about minimizers of the linear model's norm over a ball and apply to any method that uses such steps.
The result is proved in the paper. As far as we know, none of it is formalized: Mathlib has the Fréchet derivative, the inverse function theorem and invertible continuous linear maps, but no trust region or inexact Newton convergence theory. This mission produces machine-checked versions of the paper's statements for an arbitrary norm, together with a reusable vocabulary (actual/predicted reduction, stationary points of , model minimizers, trust region runs) for later formalizations of trust region and Levenberg–Marquardt type methods.
The obvious argument shows that decreases, so it converges, and then tries to conclude that the predicted reductions tend to zero. That step fails without control on the radii: if , small predicted reductions say nothing about stationarity, and the steps could shrink while the iterates still wander. The central difficulty is to show that near a non-stationary or regular limit point the radii stay bounded away from zero, while at the same time proving that the whole sequence converges to that limit point, not just a subsequence. Under an arbitrary norm the model minimizer is not unique and the model norm is not smooth, so arguments based on gradients of do not apply.
E; is fderiv ℝ F, and "continuously differentiable" is ContDiff ℝ 1 F.IsTRRun. Iteration records the number of while-loop passes, the factors , and trial steps , each a minimizer of (4.5) for its radius. Trials fail the test , and trial passes it. "Does not break down" is the existence of such a run. Any minimizer in (4.5) may be chosen.MapClusterPt. "Sufficiently near and sufficiently large" is: there exist and such that the property holds for with . "Whenever is sufficiently large" is ∀ᶠ k in atTop.(fderiv ℝ F xstar).IsInvertible. is ContinuousLinearMap.inverse, which is the true inverse for all large .¬ Summable.IsTRRun forces neither, and it has a run with nonzero steps (for on ).Needed infrastructure: the continuity of near an invertible point (Lemma 1.1 of the paper), a uniform linearization bound near a point (Lemma 1.2), and the telescoping argument of Theorem 3.5. These are reusable well beyond this mission. Contributions are welcome on each milestone separately, and on general lemmas about minimizers of over a ball.
A flexible manufacturing system routes several part types through a set of machines; a machine that switches from one kind of part to another must spend a set-up time first. Each machine has to decide, in real time and from local information only, which of its waiting buffers to work on and for how long. Long runs waste little time on set-ups but starve other buffers; short runs do the opposite.
Kumar and Seidman (IEEE TAC 35(3), 1990) showed in §III of the paper that natural distributed rules (clearing policies, which keep processing a buffer until it is empty) can be unstable when parts revisit machines, even though every machine has enough capacity. Their §IV gives a sufficient condition for a subclass of such rules to be stable, which is stricter than the capacity condition. §V, the subject of this mission, asks for something stronger: a simple, distributed mechanism that a supervisor can add to any scheduling policy and that makes the system stable whenever the capacity condition alone holds.
Timeline. Perkins and Kumar (1989) proved that the capacity condition is sufficient for the existence of some stabilizing policy, and that every clear-a-fraction policy is stable on acyclic systems. Kumar and Seidman (1990) gave the instability examples for nonacyclic systems and the universal supervisor formalized here.
There are part types and machines. Part type arrives at rate and follows a route of operations; operation is done by machine and takes per part. Parts awaiting operation wait in buffer , with level . Machine serves , and switching from to costs . Flows are continuous: a machine processing a nonempty buffer drains it at rate , the output feeds instantly, and a machine on an empty buffer passes its inflow through. Each machine works in runs: a set-up, then a processing phase on one buffer.
The load of machine and the capacity condition are
The system is stable if for every buffer.
The supervisor picks with
and thresholds . It truncates every processing run of at ; it keeps a first-come first-served queue of the buffers that are not being processed and whose level exceeds ; when a run ends and , the head of is processed next, for exactly unless it clears earlier. When is empty the underlying policy is free. Write (26) and , the backlog of part type for machine .
Under (1), (24) and , every supervised trajectory, from every initial state, satisfies
The bound is allowed to depend on the trajectory; no uniformity in the initial state is claimed.
The theorem separates two concerns of real-time scheduling. The underlying policy can be tuned for performance (low set-up overhead, short buffers) without any stability analysis; the supervisor guarantees stability under exactly the condition that is necessary for it. The mechanism is distributed: each machine uses only its own buffer levels. With it enforces FCFS with truncated runs; with large and it never intervenes on a policy that is already stable, so the degree of intervention is tunable. Combined with the §III instability examples, it shows that instability of clearing policies is a design defect that a local safeguard removes.
The result is proved in the paper; to our knowledge it has no machine-checked proof. This mission produces a formal model of continuous-flow manufacturing systems with set-up times and runs, a formal definition of the supervisor, and the four parts of Lemma 1 as reusable statements about it. Part 3) is stated with a corrected hypothesis (see Formalization scope).
The underlying policy is arbitrary, so no structure of the trajectory between interventions can be used: the policy may idle on empty buffers, switch at will, and re-select a buffer as soon as its run is truncated. The natural approach of bounding the total work at a machine fails, because work arrives at machine from upstream machines whose behaviour depends on itself through re-entrant routes, so a machine-by-machine argument is circular. A further difficulty is that the supervisor acts only on buffers above their thresholds, so a buffer can be ignored for as long as it sits at or below ; any bound has to account for the time spent below the threshold and for repeated re-entries into , with a set-up paid at each.
Fin P, machines Fin M, buffers Σ p, Fin (n p); paper index is Lean index . Time is real with . Set-up times satisfy : a set-up is paid only on a switch. No transport delays or assembly, as in the paper.Contributions welcome: proofs of the Lemma 1 parts, and lemmas on the model (Lipschitz continuity of levels, monotonicity of a buffer's level while it is not processed).
Exponential tail bounds for sums of bounded martingale differences (Bernstein, Bennett, Hoeffding, Freedman) are the workhorses of probability, statistics and learning theory. They bound how far a martingale can travel in a given amount of conditional variance. The converse question is just as basic: how much conditional variance does a martingale need before it reaches a given level? An answer controls the time a martingale spends below a barrier, and it is the ingredient that turns the upper half of a law of the iterated logarithm into the lower half.
David A. Freedman's paper On Tail Probabilities for Martingales (Ann. Probab. 3 (1975) 100–118) derives both kinds of result from a single observation: the exponential process is a supermartingale and a submartingale. The first gives the inequality now called Freedman's inequality (Theorem (1.6)/(4.1)); the second gives Theorem (1.8), the subject of this mission, a lower bound on the Laplace transform of the conditional variance accumulated up to the first crossing of a level. From (1.8) the paper derives Corollary (1.9), the tail bound , Lévy's theorem that almost surely on (Corollary (4.5)), and, through a separate analytic argument, the lower-tail bound (1.10).
Let be a probability space and an increasing sequence of sub--fields of . Let be real random variables with measurable with respect to , satisfying the standing condition (1.1):
The conditional variance of the -th step is . The partial sums are and the intrinsic time is , with .
For a real , let (positive for ), and .
A stopping time is a random variable with values in such that for every ; it is uniformly bounded if everywhere for some integer .
Fix a level . The crossing time is the least with , and if there is none. The crossing variance is
the total conditional variance the process needs to cross the level if it crosses, and otherwise the total conditional variance , which may be infinite.
For every and ,
with the convention .
The result. Theorem (1.8) says that the Laplace transform of cannot be small, so cannot be large: a bounded martingale difference sequence crosses any level after a finite amount of conditional variance with high probability. The paper turns this into the explicit tail estimate (1.9), into Lévy's theorem that a bounded martingale with divergent conditional variance is almost surely unbounded above and below, and, combined with the upper bound (4.8) on the same Laplace transform, into the lower-tail estimate (1.10) that gives the lower half of the law of the iterated logarithm for martingales in intrinsic time. Example (4.3) of the paper shows the theorem fails when the increments are only bounded below, so the two-sided bound in (1.1) is needed.
Formalizing it. The result is classical and proved in the paper; to the best of current knowledge it has no machine-checked proof. Mathlib has conditional variance, stopping times and optional stopping for bounded stopping times, but no reverse moment-generating-function inequality such as (3.7), no submartingale property for exponential processes in intrinsic time, and no crossing-time variables valued in . The mission produces these, with the conventions at infinity made explicit, as a base for the remaining results of the paper (Corollary (1.9), Corollary (4.5), the lower-tail bound (1.10)).
The obvious route is optional stopping at itself. It fails: is unbounded and may be infinite with positive probability, and Proposition (3.6) holds only for uniformly bounded stopping times. The argument must stop at , use the overshoot bound (which relies on ), and pass to the limit in a way that sends the integrand to on ; the limit exchange needs in and . A second obstacle is the one-step inequality (3.7): it is a lower bound on a moment-generating function, valid for random variables bounded only from below, where may be infinite; the usual convexity bounds go in the opposite direction.
The source is the published Annals of Probability article (a scanned copy); all page numbers are the journal's.
Conventions. Increments are a sequence X : ℕ → Ω → ℝ used from index ; is never read. Measurability is " is -strongly measurable for ", and the two parts of (1.1) are assumed almost surely. is Mathlib's condVar of given ; under (1.1) every is square-integrable, so this is a genuine conditional variance and no square-integrability hypothesis is added to the martingale statements. Stopping times are Ω → WithTop ℕ (⊤ is ). is WithTop ℕ-valued and is -valued (ℝ≥0∞), built from the nonnegative parts of the , which agree with almost surely. The integrand of the goal is the function that equals on and on ; replacing it by , which is on , would formalize a strictly weaker statement and is ruled out. In (3.7), where need not be integrable, the expectation is a lower Lebesgue integral in , and is assumed square-integrable so that is finite.
Corrected misprints. Definition (1.2)(e) prints ; is read as . The display in (4.2) prints the last factor without its expectation sign; the is restored.
Ranges. The goal uses and as in (1.2) and (1.7); (3.6), (3.7) and its two cases are stated for as on p. 107.
Lemma (3.1) ( is increasing), used in Case 2, is posed in the companion mission on Freedman's inequality and not here. Contributions welcome: proofs of the milestones, a general lemma that is a submartingale, and Corollary (1.9) as a follow-up.
In a birth-and-death population model, an expected population curve does not determine the amount of random variation. Births and deaths can occur frequently while nearly canceling in the mean, or one of the two rates can vanish while giving the same mean. This distinction matters when a prescribed growth curve is used to model a population: two processes can agree on their expected size at every time and differ substantially in their uncertainty. In §6 of Kendall's 1948 paper, the question is posed directly: among time-varying birth and death rates giving a fixed mean curve, which choice minimizes the variance of the population size?
Kendall cites Arley's observation for constant rates with the same positive net growth. His §6 moves from that special case to an arbitrary prescribed mean curve and identifies a unique minimum-fluctuation rate pair. The paper also gives a logistic-growth example, connecting the stochastic rate choice to a familiar deterministic population law. The historical result is proved in the paper; this mission concerns its Lean formalization, including the exact time-dependent variance comparison and uniqueness claim.
The process starts with one ancestor. At time , each member gives birth at rate and dies at rate ; the rates are nonnegative. Let be the population size and its expectation. Kendall works with the population probabilities and their generating function rather than constructing sample paths. This mission likewise uses his explicit formulas for the mean and variance, so that the comparison has a precise real-valued expression.
Define the integrated net death rate and the fluctuation by
Kendall's equations (13) and (14c) identify and for the one-ancestor process. A pair is admissible here when both rates are continuous and nonnegative on . It has mean when for every . In particular, the initial value is . These definitions let the mission quantify over every admissible rate pair with the prescribed mean.
For a positive continuously differentiable mean curve, write . The minimum-fluctuation rates are and . When the mean decreases, only deaths occur; when it increases, only births occur; when it is locally constant, both rates are zero. This is Kendall's equation (56), expressed without first naming intervals of monotonicity.
The goal is the simultaneous variance bound
The statement also establishes that is admissible and has the required mean. Its uniqueness clause says that if one admissible pair has the same variance as the candidate at every nonnegative time, then its two rates equal the candidate rates at every nonnegative time. Equality at only one selected time does not express Kendall's claim. The formal milestones record the fixed rate difference (55), the integral decomposition displayed in §6, and the nonnegative excess in variance that precedes (56). A companion statement covers the logistic example (58)–(60): for and , has minimum-fluctuation death rate zero and birth rate .
The result distinguishes mean growth from population risk. Fixing fixes the mean curve, but it leaves room for births and deaths that offset one another. Kendall's theorem determines the lowest variance compatible with the given curve and specifies the rate pair attaining it. The uniqueness statement identifies a model, rather than only a numerical lower bound. His logistic example shows the choice concretely: positive logistic growth is realized by a purely reproductive process in the minimum-fluctuation model.
The paper already derives these formulas. A complete formalization would connect the exact variance expression to a universal optimization claim over continuous nonnegative rate functions, and it would verify that equality throughout time identifies the rates. The definitions of the integrated rate, mean condition and variance functional can also support the other results in Kendall's paper. This proposal uses a local copy of because the geometric-solution mission is being drafted in parallel and its definition has not been published for import.
The constraint imposed by a given mean fixes the difference but not either rate separately. The variance is an integral over the full past, multiplied by a term involving that same integrated difference. Consequently, a pointwise observation about the current sum does not by itself state the required comparison of variances over every time horizon. The equality case is also global: a single time's variance cannot generally identify the rates at all earlier times. The formal result must keep the shared mean condition, the variance integral and the quantifiers over both rate pairs and all nonnegative times aligned.
The Lean development represents rates and the prescribed mean as functions . Every stochastic claim is restricted to ; the integrals are oriented interval integrals from zero. Both rates are continuous on all of and nonnegative on nonnegative time. The mean is , positive on all of , and equals one at zero. Extending the regularity and positivity assumptions to negative time makes the total functions defining , and continuous without changing any comparison on . These are explicit convenience assumptions beyond Kendall's wording. No denominator is used without the positivity assumption.
Kendall presents (56) after assuming that positive time splits into decreasing, increasing and constant intervals of . The goal uses positive and negative parts of and therefore covers any positive curve, including one without such a partition. On each of Kendall's three types of interval the formula agrees with his stated rates. The variance functional is exactly the last expression in (14c); its identification with the variance of the geometric population law is treated in the companion geometric-solution mission. The local statements do not construct a Markov process. The minimum is taken over all admissible continuous nonnegative rate pairs with the prescribed mean, not merely over the two candidate functions or over pointwise values of .
The development needs real differentiation, continuity, exponentials and interval integrals from Mathlib. Contributions that relate the explicit functional to the population law, prove the comparison and its equality case, or extend the regularity regime while preserving Kendall's claim are within scope. The logistic example provides a concrete instance of the general result.
A recurring task in martingale theory is to compare a sum of nonnegative random variables with the sum of their predictable projections : the conditional expectation of each term given the information available one step earlier. Such comparisons are the step that turns a statement about the conditional square function of a martingale into a statement about the martingale itself, and they recur in the proofs of the Burkholder–Davis–Gundy inequalities and of their conditional variants.
In his 1971 Wald Memorial Lectures, published as Distribution Function Inequalities for Martingales (Burkholder 1973), D. L. Burkholder proves two such comparisons for a function applied to the sums. For convex of moderate growth, the sum of predictable projections is controlled by the sum itself, up to a constant (Lemma 16.1, the "convexity lemma", §16). For concave , §20 proves the reverse comparison, with the explicit constant . This mission is the concave case, Theorem 20.1.
The same section derives Theorem 20.2 from it: for a martingale and concave , . For the concave powers , , that bound had been proved by another method in Burkholder, Davis and Gundy 1972. Comparisons of the same kind between an increasing process and its compensator were later systematized as the Lenglart domination principle (Lenglart 1977).
Let be a probability space and a non-decreasing sequence of sub--fields of . In Lean this is a probability measure P together with a filtration ℱ : Filtration ℕ mΩ, ℱ k .
Let be nonnegative measurable functions on , with values in . They need not be integrable, and they need not be adapted: is only -measurable. For a nonnegative function the conditional expectation always exists as an -measurable function with values in , determined up to null sets by for . Put
and, for , the partial sums , over .
A function is concave as above in the paper's sense if it is non-decreasing and continuous on , , it satisfies the growth condition for , and it is concave on . Concavity alone already gives . Examples: for , , .
For a martingale with differences (), the maximal function is and the conditional square function is .
for every concave as above and all nonnegative measurable . The constant is universal: it does not depend on , on the growth constant , on the probability space or on the .
For a martingale and concave as above,
It is posed as a separate theorem and is not a milestone of the goal.
Theorem 20.1 holds without any integrability and without adaptedness, so it applies to arbitrary nonnegative sequences. With it compares the square function of a martingale with : for concave , . Together with the Burkholder–Davis–Gundy comparison of and , this is one route from the conditional square function to the maximal function in the range of exponents , where the convex methods of the rest of the paper do not apply. Theorem 20.2 is the result of this kind that the paper states.
The paper proves Theorem 20.1 in about half a page. As far as is known, neither Theorem 20.1 nor Theorem 20.2 has been formalized in any proof assistant. Mathlib provides the -valued conditional expectation (condLExp), filtrations, stopping times and Lebesgue integrals of extended nonnegative functions. It has no comparison theorem of this type between a sum and its predictable projections. A formal proof would therefore add a new, reusable tool to Mathlib's discrete-time martingale library, one that an eventual formal Lenglart inequality or conditional BDG inequality would need.
The obvious first idea is Jensen's inequality for conditional expectations. For concave it gives term by term, but of a sum is not the sum of the 's, and summing the termwise bounds loses the comparison. Another first idea, comparing and (which are equal by the tower property), handles only linear , and both sides may be infinite.
The content lies in two places. The first is the truncated inequality for , where neither nor is integrable in general and the comparison must hold level by level. The second is the passage from the truncated family to an arbitrary concave . It needs a representation of concave through the truncations , including the cases and and a possibly infinite right derivative at (as for ). Both steps must be carried out in arithmetic.
ℝ≥0∞-valued; expectations are lower Lebesgue integrals ∫⁻. The conditional expectation is Mathlib's condLExp (notation P⁻[z | ℱ k]), never the Bochner P[z | ℱ k]. The Bochner version is on non-integrable functions and would make the goal false (take ).z (k+1) is and is paired with ℱ k , so is conditioned on , as in the paper. z 0 is unused.IsPhi Φ c for an arbitrary constant c, together with IsConcavePhi Φ: concavity of on , read through real values. This is honest because IsPhi forces to be finite on finite arguments. The growth condition is required for every , which is equivalent to (6.1) by continuity. The paper's exclusion of is dropped, since the conclusion is trivial there.l : ℝ≥0).Martingale f ℱ P. It reads f n only for , with the paper's convention . Mathlib's extra constraint on f 0 is no restriction, since every martingale of the paper extends by .condLExp for indicators of -sets, monotone convergence for condLExp, and the integral representation of a concave non-decreasing with as a mixture of the functions plus a linear part. The last is reusable well beyond this mission. Contributions to any of these are welcome.