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.
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?
Missions I and II of this series showed that finite hypothesis classes are learnable, with and without the realizability assumption, by empirical risk minimization. Chapter 5 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) asks the converse question: is prior knowledge, in the form of a restricted hypothesis class, really necessary? Could there be a universal learner, an algorithm that, given enough examples from any distribution, outputs a predictor of low risk? The No-Free-Lunch theorem (Theorem 5.1) answers no: for binary classification with the 0–1 loss over a domain , for every learning algorithm and every training-set size smaller than there is a distribution on which the learner fails with probability at least , even though that distribution is perfectly predictable by some function , so that another learner (ERM over ) succeeds. The consequence for the framework is Corollary 5.2: over an infinite domain, the class of all functions is not PAC learnable. This is the first lower bound of the book and the reason the rest of it is about the complexity of hypothesis classes rather than about universal algorithms.
The framework is the UnderstandingML_Framework module of Mission I, cited as a reference. Binary classification over a domain uses examples in , hypotheses and the 0–1 loss, so the risk of under a distribution over is , computed as the integral of the 0–1 loss. A learner is a function from samples of each size to hypotheses, and a sample of size has the law . PAC learnability of a class (Definition 3.1) requires a sample-complexity function and a learner such that for every , every distribution over and every measurable labeling function realizable by , samples of size yield with probability at least .
Two conventions specific to this mission. The domain is assumed to have measurable singletons (the book's Remark 3.1 assumes away measurability issues); this makes the finitely supported distributions of the proof honest probability measures and makes every under them a genuine integral. And " smaller than " is written in the extended natural numbers, so that an infinite domain satisfies it for every .
Let be any learning algorithm for binary classification with respect to the 0–1 loss over a domain with measurable singletons, and let be a training-set size with . Then there exists a probability distribution over such that
Lemma B.1 (Appendix B). If takes values in and , then for every , , and consequently .
Equation (5.2). Under the hypotheses of Theorem 5.1 there are and a measurable with and .
Corollary 5.2. For an infinite domain with measurable singletons, the class of all functions is not PAC learnable.
Two further items: Exercise 5.1, the passage from an expectation of at least to a probability of at least of exceeding for a -valued variable; and Exercise 5.3, the -fold version of Equation (5.2), with bound when , and is nonempty.
The No-Free-Lunch theorem is the book's first impossibility result and the conceptual pivot of Part I: it shows that learnability is a property of the pair (hypothesis class, learner) and not of the learner alone, and it motivates the bias–complexity tradeoff of §5.2 and the VC-dimension of Chapter 6, whose lower bound (Theorem 6.7, the "only if" direction of the fundamental theorem) is proved by the same symmetrization argument. Corollary 5.2 is the statement that the class of all functions has infinite sample complexity, the negative half of the characterization of learnable classes.
Nothing here is machine-checked. The proof is combinatorial and elementary but has real content for a formalization: a finite subset of the domain, the labelings of , the uniform distribution on labeled by each of them, an exchange of a maximum, an average and a minimum over labelings and sample sequences, and a pairing argument on labelings that differ at exactly one unseen point. Lemma B.1 is a reverse Markov inequality for bounded variables that later chapters also use.
Lemma B.1 is Markov's inequality applied to and is the entry point; Exercise 5.1 is its instance with and , giving , together with the inclusion of in . Theorem 5.1 follows from Equation (5.2) and Exercise 5.1 once one knows that is, under the finitely supported , almost everywhere equal to a measurable function with values in ; the set is the intersection of the event with the finite support of , which is measurable because singletons are. Equation (5.2) is the heart of the mission. One picks of size (available because ), lets be uniform on labeled by the -th function extended by off , and computes as an average over the sequences of instances, which requires identifying as a finitely supported measure on sequences, that is, the product of finitely supported measures. The inequalities (5.4)–(5.6) exchange max, average and min and restrict to the unseen points, and the pairing argument shows that for each unseen point the average over of the indicator that errs on it is exactly . Exercise 5.3 is the same argument with , where at least points are unseen. Corollary 5.2 takes , , and a set of size in the infinite domain, and derives the contradiction from Theorem 5.1 via the identification of for uniform on labeled by with the true error of Definition 3.1, where is uniform on ; the case is handled separately with a single point.
The items are stated in the joint-distribution form of the book's Chapter 5, with over and the risk under the 0–1 loss, rather than in the form of Definition 3.1; Corollary 5.2 is the bridge and is stated with the framework's PACLearnable. Witness labeling functions are required to be measurable, because a non-measurable would make true by Lean's convention for non-integrable functions rather than by content. Clause (2) of Theorem 5.1 is stated in the inner form (a measurable set of probability at least inside the event) rather than as a lower bound on the outer measure of the event, which for a non-measurable event would be the weaker statement. The size condition uses ENat.card, so infinite domains satisfy it. Learners are deterministic functions of the sample; the book's argument goes through for randomized learners by averaging, but the framework does not model them.
Trivializing readings are excluded: the distribution must be a probability measure, the failing set must be measurable with an honest lower bound, and the witness must be measurable. Welcome contributions: the finitely supported product law on sequences, the averaging identity (5.3), and the pairing argument on labelings of .
Mission I of this series set up the statistical learning framework of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) and proved, in the book's Chapters 2 and 3, that finite classes are PAC learnable under the realizability assumption. Chapter 4 removes that assumption. Its idea is the one that organizes the rest of the theory: if the empirical risks of all hypotheses in are simultaneously close to their true risks , then minimizing over is nearly as good as minimizing over , whatever the distribution is. A sample with that property is called -representative (Definition 4.1), and a class for which representative samples are guaranteed at some sample size is said to have the uniform convergence property (Definition 4.3). Lemma 4.2 turns representativeness into a guarantee for ERM, Corollary 4.4 turns uniform convergence into agnostic PAC learnability, Hoeffding's inequality (Lemma 4.5) gives uniform convergence for a single hypothesis, and a union bound gives it for a finite class: Corollary 4.6, the capstone, says every finite class with a loss in is agnostic PAC learnable by ERM with sample complexity .
The framework is the UnderstandingML_Framework module of Mission I, cited here as a reference. A domain is a measurable space, hypotheses form a type with a class , and a loss is given. The risk is , the empirical risk on is , and a sample of size has the product law . A hypothesis is an ERM hypothesis for if it lies in and minimizes over ; a learner is a function from samples of each size to hypotheses, and an ERM learner returns an ERM hypothesis on every sample.
is -representative with respect to , and if for every . has the uniform convergence property with the function if for every and every distribution over , a sample of i.i.d. examples is -representative with probability at least . is agnostic PAC learnable with the function and the learner if returns hypotheses in and, for every , every and every , with probability at least over . As in Mission I, "with probability at least " is an upper bound on the outer measure of the failure event, "" is written as ", ", and sample-complexity functions are carried explicitly rather than as minimal functions.
Let be a finite hypothesis class, a domain and a loss function whose sections are measurable. Then
Lemma 4.2. If is -representative and is an ERM hypothesis for , then for every .
Corollary 4.4. If has the uniform convergence property with , then every ERM learner for is an agnostic PAC learner with the function , and is agnostic PAC learnable as soon as an ERM learner exists.
Lemma 4.5 (Hoeffding's inequality). For a probability measure , a measurable with almost surely and mean , and ,
Chapter 4 is where the book's account of learnability becomes distribution-free in the agnostic sense: nothing is assumed about beyond being a probability distribution, and the guarantee is relative to the best hypothesis in the class. Lemma 4.2 and Corollary 4.4 are the reduction that every later generalization bound in the book (VC dimension, Rademacher complexity, covering numbers, compression) plugs into: prove uniform convergence, get ERM learnability. Corollary 4.6 is the first instance, and its dependence, against the of the realizable case, is the standard illustration of the price of agnosticism. Hoeffding's inequality is stated in the form the book uses everywhere afterward, for the product law of one distribution, with an almost-sure range bound and the mean written as an integral.
Nothing here is machine-checked. Mathlib has no Hoeffding inequality for sums of i.i.d. bounded variables on a product measure in this form, so Lemma 4.5 is a genuine contribution; its proof in the book's Appendix B goes through Hoeffding's lemma on the moment generating function of a bounded centered variable and the Chernoff bounding method, both of which will be needed by the concentration results of later missions.
Lemma 4.2 is three inequalities on real numbers and is the intended entry point. Corollary 4.4 is Lemma 4.2 applied on the complement of the failure event of uniform convergence at : the failure set of the learner is contained in the failure set of representativeness, and outer measure is monotone. Hoeffding's inequality is the substantial item: one needs the moment generating function bound (Lemma B.7 of the book, by convexity of the exponential on ), independence of the coordinates under Measure.pi to factor the expectation of the product, Markov's inequality, and the optimization over ; the two tails are treated separately and added. The degenerate cases are genuine: for the bound is and the claim holds trivially, and for Lean's convention makes the bound again. Corollary 4.6 combines Hoeffding for each with a union bound over the finite class and an arithmetic step showing that gives ; the empty class makes the uniform convergence clause vacuous. The second and third clauses of the goal then follow from Corollary 4.4, the third by exhibiting an ERM learner, which exists for a nonempty finite class by choosing a minimizer of .
The four items live in the general loss framework, not the binary-classification special case, because the chapter is stated for an arbitrary loss; Mission I's IsRepresentative and HasUniformConvergenceWith already carry the chapter's definitions, so no new definition module is introduced. Losses in Corollary 4.6 are real-valued with the range condition for every and measurability of for , which is what the book's "" and Remark 3.1 give. The book's "" is stated as "the guarantee holds with the function ", the same convention as Mission I. In Corollary 4.4 the ERM clause is universal over ERM learners, matching "the ERM paradigm is a successful agnostic PAC learner" for every choice of minimizer; the existence of an ERM learner is a separate hypothesis for the learnability clause because a class with no minimizers on some sample has no ERM rule. Hoeffding's inequality is on i.i.d. coordinates of Measure.pi; the book's "" is the definition of rather than an assumption.
Trivializing readings are excluded: the failure events are bounded in outer measure, so measurability of the events is not a loophole; representativeness is required for every ; the sample-complexity functions are the book's, with ceilings. Welcome contributions: Hoeffding's lemma on bounded centered variables, the factorization of the moment generating function under Measure.pi, and a reusable union bound over a finite class.
Chapters 2 and 3 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (Cambridge University Press, 2014, doi:10.1017/CBO9781107298019), set up the framework in which the whole book asks what learning is. A learner sees a sample drawn independently from an unknown distribution over examples, chooses a hypothesis from a class fixed in advance, and is judged by its risk, the expected loss on a fresh example. The natural rule is Empirical Risk Minimization: pick a hypothesis that does best on the sample. Chapter 2 shows that ERM over an unrestricted class overfits, that restricting the class is what makes learning possible, and that a finite class never overfits once the sample is larger than (Corollary 2.3). Chapter 3 turns this into a definition, Probably Approximately Correct learnability with its sample-complexity function , restates the finite-class result as Corollary 3.2, and then generalizes in two directions that the rest of the book lives in: the agnostic model, in which no hypothesis need be perfect and the learner competes with the best hypothesis in the class, and general loss functions, which cover regression, multiclass prediction and unsupervised tasks. Chapter 4 adds the notion of an ε-representative sample and of uniform convergence, the tool by which the finite-class result extends to the agnostic case; its definitions are included here since they complete the framework.
A domain of examples, a class of hypotheses and a loss . The risk of under a distribution is and its empirical risk on is ; a sample is drawn i.i.d., ; an ERM hypothesis minimizes over ; a learning algorithm maps samples of each size to hypotheses. In binary classification the examples are with over and a labeling function, and the true error is ; the realizability assumption says some has . is PAC learnable if some sample-complexity function and algorithm guarantee, for all , all and all realizable , true error at most with probability at least from examples; agnostic PAC learnability with respect to a loss asks instead for for every distribution over .
Every finite hypothesis class is PAC learnable with sample complexity
by the ERM rule: for a nonempty finite class of measurable hypotheses there is an ERM learner satisfying the PAC guarantee with that sample-complexity function.
Corollary 2.3: under realizability, with examples, every ERM hypothesis has true error at most with probability at least .
Corollaries 2.3 and 3.2 are the first learning theorem of the book and the template for all later sample-complexity bounds: a bad hypothesis is consistent with an i.i.d. sample with probability at most , and a union bound over the class turns this into a guarantee that holds uniformly over all distributions and all realizable labelings. Everything that follows, uniform convergence for finite classes, the fundamental theorem for classes of finite VC dimension, structural risk minimization, replaces the count by a finer measure of the class's complexity but keeps the argument. None of this is machine-checked. The mission fixes on the platform the objects that the rest of the series uses without change: risks, empirical risks, the product law of a sample, the ERM relation, and the four learnability notions of Definitions 3.1, 3.4, 4.1 and 4.3.
The milestone needs that, for a fixed measurable hypothesis whose true error exceeds , the product law gives the event "zero empirical risk" probability at most ; this is the product structure of Measure.pi on the event that each labeled example lies in the measurable set where the hypothesis agrees with , followed by , the union bound over the finite class and the observation that under realizability every ERM hypothesis has zero empirical risk, so a bad ERM hypothesis is a consistent bad hypothesis. The goal packages this as a learner: existence of an ERM hypothesis for every sample (a finite nonempty class has a minimizer), and the arithmetic of the ceiling.
The framework is the book's, with the risk as a Bochner integral, the sample law as a product measure, ERM as a relation and learners as deterministic functions of the sample; failure probabilities are stated as upper bounds on the outer measure of the failure set, the strong form of "with probability at least "; the comparison with is written without an infimum. Sample-complexity functions are carried explicitly: the book's as the minimal such function is not defined, and "" is stated as "the learner satisfies the guarantee with the function ". Hypotheses and labeling functions are assumed measurable (Remark 3.1). The union bound (Lemma 2.2) is Mathlib's measure_union_le and is not an item. Hypotheses: , , finite (and nonempty for the learner to exist).
Trivializing readings are excluded: the milestone's failure event ranges over every ERM hypothesis, and the goal quantifies over all distributions, all realizable labelings and all . Welcome contributions: the product-law bound for a fixed hypothesis and the union bound over a finset, which every later mission of the series reuses.
Chapter 2 of Kearns and Vazirani, An Introduction to Computational Learning Theory (MIT Press, 1994, doi:10.7551/mitpress/3897.001.0001), gives a formal justification of Occam's Razor inside the PAC model. An Occam algorithm is judged not by the predictive power of its hypothesis but by how succinctly the hypothesis explains the sample before it: it must be consistent with the data and short, in the sense that its representation has fewer bits than the data it reproduces. The chapter's theorems say that, when the examples are drawn independently from a fixed distribution, such compression automatically yields prediction: a consistent hypothesis drawn from a small class is, with high probability, accurate on unseen examples. This turns the design of PAC learning algorithms into a combinatorial task, finding a short consistent hypothesis, and the chapter demonstrates the method three times: it shaves a logarithmic factor off the conjunction bound of Chapter 1, it learns conjunctions with few relevant variables through the greedy set-cover heuristic, and it learns Rivest's decision lists, a class strictly more expressive than -CNF and -DNF, by a greedy algorithm whose correctness is a one-line consequence of consistency.
The framework is that of Mission I: a measurable instance space, concepts as boolean functions, a target distribution , the product law of a sample of labeled examples, the error , and consistency of a hypothesis with a sample. Hypotheses may be represented by binary strings through a representation map, with size the bit length; an -Occam algorithm outputs a consistent hypothesis of size at most with . The set cover problem asks for a minimum subcollection of a collection of subsets of a finite universe that covers ; the greedy heuristic repeatedly picks the set covering the most uncovered elements. A -decision list is a sequence of conditions, each a conjunction of at most literals, with a bit attached to each and a default bit; it evaluates to the bit of the first satisfied condition. The greedy decision-list algorithm repeatedly finds a useful condition, one satisfied by some remaining examples all of which carry the same label, appends it with that label and removes those examples.
For a finite hypothesis class , a target , a distribution and , the probability that a sample of examples is consistent with some of error greater than is at most ; hence
makes this probability at most , and any algorithm that outputs a consistent hypothesis from has error greater than with probability at most .
Theorem 2.1 (an -Occam algorithm is a PAC algorithm, with explicit sample-size conditions in place of the constant ); the greedy set-cover bound of §2.3 ( and sets cover); the improved conjunction bound of §2.2; Theorem 2.3 (-decision lists are PAC learnable by the greedy algorithm, which never fails and whose outputs are consistent).
Theorem 2.2 is the single most used tool of the subject: every finite-class sample bound, including the ones for conjunctions, decision lists, -CNF and the discretized geometric classes, is an instance of it, and the Vapnik–Chervonenkis theory of Chapter 3 is its extension to infinite classes with the growth function in place of . Theorem 2.1 is the philosophical statement, that succinct explanation implies prediction, and its converse (Exercise 2.3, and more strongly the boosting theorem of Chapter 4) makes Occam learning equivalent to PAC learning. The greedy set-cover bound is Chvátal's classical approximation guarantee, used in the book for learning with few relevant variables and again in later chapters. Theorem 2.3 is Rivest's result, and its proof exhibits the pattern "consistency by construction plus a counting bound" in its purest form. None of these is machine-checked. Their formalization gives the platform the union-bound-over-a-finite-class argument once and for all, in a form that the later missions of this series reuse verbatim.
Theorem 2.2 requires that, for a fixed measurable hypothesis with error greater than , the product law gives the event "consistent with all examples" probability at most , which is the product structure of Measure.pi applied to the event that each coordinate lies in the set where agrees with ; the union bound over and the elementary inequality finish. Theorem 2.1 adds only the count of binary strings of length at most and arithmetic with real exponents. The set-cover bound is a discrete induction: an optimal cover of restricted to the uncovered elements has at most sets, so one of them, hence the greedy choice, covers a fraction; the covering clause needs the strict inequality . Theorem 2.3 needs that a run of the greedy algorithm never repeats a condition (its satisfied examples are removed), so outputs lie in an explicit finite class, that the first condition of the target list satisfied by a remaining example is useful, and that a complete run is consistent; the bound is then Theorem 2.2.
Everything is in the sample-complexity sense on the Mission I framework; running time is not modelled and "efficient" is dropped from every statement, which is recorded in the natural-language statements. Theorem 2.2's constant is with natural logarithms; Theorem 2.1's constant is replaced by three explicit sufficient conditions. Hypotheses in the finite class are required to be measurable. The greedy heuristic and the greedy decision-list algorithm are relations (any tie-breaking), and the theorems quantify over every run; the decision-list theorem is stated for every with the -conjunctions as conditions, so that its hypothesis is a -decision list rather than the expansion the book sketches for . The conjunction count is , including the empty concept that the elimination algorithm outputs on a sample without positive examples. The few-relevant-variables algorithm of §2.3 is not stated (its bound has an unspecified constant and on both sides). Hypotheses: , (and where must be nonnegative).
Trivializing readings are excluded: the bad-consistent event is over all of , the decision-list failure event ranges over every possible output, and the set-cover bound holds for every greedy run. Welcome contributions: the product-law bound for a fixed hypothesis, the union bound over a finset, the string-counting lemma, and the no-repetition lemma for greedy runs.
Chapter 1 of Kearns and Vazirani, An Introduction to Computational Learning Theory (MIT Press, 1994, doi:10.7551/mitpress/3897.001.0001), introduces Valiant's Probably Approximately Correct model, the framework for the whole book. A learner sees labeled examples of an unknown target concept drawn from an unknown but fixed distribution, and must output a hypothesis that, with probability at least over the sample, misclassifies a fresh example with probability at most ; the model is distribution-free, and the hypothesis is judged on the same distribution it was trained on. The chapter's three positive results are the templates for everything that follows. The rectangle game (Theorem 1.1) shows that an infinite class can be learned from a finite sample by exploiting the geometry of the error region. Conjunctions (Theorem 1.2) are learned by the elimination algorithm, whose analysis, a union bound over "bad" literals, is the prototype of every sample-size bound in the book. And 3-CNF formulae (Theorem 1.4) are learned by a change of variables that reduces them to conjunctions, which, set against the intractability of learning 3-term DNF as 3-term DNF (Theorem 1.3), is the reason the final definition of the model lets the hypothesis class differ from the concept class.
The instance space is a measurable space , a concept is a function , and the target distribution is a probability measure on . The error of a hypothesis is . A sample of examples is with the independent draws from ; a learning algorithm is a function from samples to hypotheses; it has the guarantee on a class if for every and every the probability that its hypothesis has error greater than is at most ; is PAC learnable using if for all some sample size and algorithm with hypotheses in achieve the guarantee. For a literal is a variable or its negation and a conjunction is a finite set of literals; the elimination algorithm starts from all literals and deletes every literal contradicted by a positive example. For the concepts are the closed axis-aligned rectangles and the tightest-fit algorithm returns the smallest rectangle containing the positive examples. A 3-CNF formula is a conjunction of clauses of at most three literals; the expansion records for each triple of literals the value .
Conjunctions of boolean literals are PAC learnable by the elimination algorithm: for every target conjunction, every distribution on and , the elimination hypothesis is consistent with every sample labeled by the target, and with
examples its error exceeds with probability at most ; hence conjunctions are PAC learnable using conjunctions.
Theorem 1.1 (rectangles by the tightest fit, ) and Theorem 1.4 (3-CNF formulae by elimination over the expanded variables, the hypothesis being itself a 3-CNF formula).
Theorem 1.2 is Valiant's original result and the first instance of the two ideas that organize the subject: a hypothesis that is more specific than the target never errs on negative examples, and the error of the hypothesis decomposes as a sum over a polynomial number of "bad" events, each of which is avoided with probability exponentially close to one. Theorem 1.1 is the first learning result for an infinite concept class and the seed of the Vapnik–Chervonenkis theory of Chapter 3. Theorem 1.4 is the first reduction between learning problems and, together with Theorem 1.3, the demonstration that the choice of hypothesis representation can separate tractable from intractable. None of these theorems is machine-checked. Formalizing them fixes, for the rest of the series, the framework in which the error of a hypothesis, the law of a sample and the learnability of a class are stated, so that the Occam, VC-dimension, boosting and noise results of later chapters can be stated on the same objects.
The elimination analysis needs that the hypothesis contains every literal of the target, that its error is at most the sum over its literals of , and that a literal with survives independent examples with probability at most ; the probabilistic content is the independence of the coordinates of the sample law, which is a product measure, and the inequality . The rectangle analysis is the four-strip argument, which for an arbitrary distribution, possibly with atoms, requires choosing the strip with the supremum of the heights at which the strip has weight at least and using the left-continuity of the weight in the height. The 3-CNF result transports the conjunction bound along the injective expansion: the pushforward of the sample law is the sample law of the expanded distribution, and the error of the composed hypothesis equals the error over the expanded variables. The deduction of PACLearnable from the explicit bounds is a choice of sample size.
The model is stated in the sample-complexity sense: algorithms are functions of the sample, and the guarantee bounds the outer measure of the failure set under the product law of the sample, which is the strong form of "with probability at least " and requires no measurability of the failure set. Running time, and hence "efficiently", is not modelled, and the hardness Theorem 1.3 is not stated; each theorem carries instead the explicit algorithm and the explicit sample bound of the book's analysis. Concepts on general instance spaces are required to be measurable in the guarantee. The cube is as functions Fin n → Bool; the expanded variables are indexed by the triples of literals, so is a Fintype.card. Rectangles are closed, possibly empty; the tightest fit of a sample without positive examples is the empty concept. Hypotheses: , ; the sample bounds are as printed, with natural logarithms.
Trivializing readings are excluded: the failure bound is uniform over all distributions and all targets in the class, consistency is asserted for every sample labeled by the target, and the learnability clause quantifies over all . Welcome contributions: the product-law bound , the union bound over literals, and the pushforward identity for the expanded sample.
The Vickrey-Clarke-Groves auction is the textbook mechanism for selling several objects at once: bidders report valuations for bundles, the auctioneer computes the welfare-maximizing allocation, and each winner pays the externality it imposes on the others. Truthful bidding is a dominant strategy and the outcome is efficient. Yet Ausubel and Milgrom (2006) catalogued its practical defects: revenue can be zero when the objects are valuable, revenue can fall when bidders or bids are added, losing bidders can profit by colluding, and a bidder can profit from false identities. Chapter 15 of Snyder and Shen's Fundamentals of Supply Chain Theory (2019) reproduces those examples and then gives the cooperative-game answer to when they cannot occur: the VCG payoff vector should lie in the core, the set of outcomes no coalition of auctioneer and bidders can improve upon, and it does so for every set of participants exactly when the coalitional value function is bidder-submodular. This mission formalizes that characterization, Theorem 15.3, together with the lemma and theorem leading to it.
Players are the auctioneer and bidders . A coalitional value function
assigns to each coalition the value it can create by trading among themselves: if the
auctioneer, who owns the objects, is not in , and otherwise the optimal value of the
auctioneer's allocation problem among the bidders of , each bidder receiving at most one
bundle and bundles disjoint (capValue). Two properties of are all the theory uses:
coalitions without the auctioneer are worthless, and adding players never lowers the value
(IsCoalitionalValue).
A payoff vector gives each player a payoff. It lies in the core of the game on a
coalition (InCore V S π) if the payoffs of sum to and no sub-coalition
is paid less than . The VCG payoff vector (vcgPayoff)
pays each bidder its marginal contribution , which is its valuation
minus its VCG payment, and the auctioneer the remainder. A core vector is bidder dominant
(BidderDominant) if every bidder weakly prefers it to every other core vector. is
bidder-submodular (BidderSubmodular) if each bidder's marginal contribution weakly
decreases as the coalition grows.
For a coalitional value function , the following are equivalent: (i) is
bidder-submodular; (ii) for every coalition the core equals
;
(iii) for every coalition , lies in the core of . This is
vcg_core_characterization.
That the combinatorial auction's is a coalitional value function; Lemma 15.1, the core is nonempty and each bidder's VCG payoff is the largest it receives at any core point; Theorem 15.2, the VCG vector is the bidder-dominant core point when it is in the core, and otherwise no bidder-dominant point exists and the auctioneer's VCG payoff is below every core payoff.
The English auction of Sect. 15.2, presented as a primal-dual interpretation of a linear program, and the combinatorial allocation problem of Sect. 15.3 carry no numbered results and are not targets.
Theorem 15.3 is the criterion an auction designer can check before running a VCG auction: when the bidders' valuations make bidder-submodular (for instance when objects are substitutes), the VCG outcome is a competitive outcome, its revenue meets the core benchmark, and none of the defects of Sect. 15.4.2 can arise; when they do not, Theorem 15.2 says the auctioneer's revenue is strictly below every competitive outcome. The result underlies the ascending package auctions proposed as VCG alternatives and the procurement auctions used in supply chains, such as the combinatorial reverse auctions of the chapter's case study.
None of these results has a machine-checked proof. The book proves all three. The formal treatment of the core and of marginal-contribution vectors is reusable for the cooperative-game models of cost allocation in supply chains.
The theorems are combinatorial statements about a function on finite sets, and the difficulty is entirely in the bookkeeping of coalitions. Lemma 15.1 needs the explicit core vector of its proof to be verified against every sub-coalition, which splits into cases on whether the sub-coalition contains the auctioneer and the distinguished bidder. The implication (i) (ii) telescopes marginal contributions along a chain of coalitions between a sub-coalition and , and the chain has to be built and its sum computed. The implication (iii) (i) is the delicate one: a failure of submodularity is a pair of nested coalitions, and the proof needs to extract from it a single-element step at which a bidder's marginal contribution increases, then show the two-bidder sub-coalition blocks the VCG vector. The obvious idea, that submodularity can be checked only on single-element extensions, is correct but must itself be proved.
Coalitions are finite sets of Fin (n+1) and payoff vectors are functions on all players; the
core and constrain only the players of , so vectors differing outside are
interchangeable. The core's budget equation sums over all players of the coalition, including
the auctioneer, which is what the book's proofs use although its displayed definition sums over
the bidders. The theorems take as any function with the two properties, and the auction's
is shown to have them; the VCG vector is defined by the formulas (15.23) and (15.24) rather
than through the payment rule, whose equivalence is the book's derivation. Bidder-submodularity
is stated for rather than proper inclusion, which changes nothing.
The definition module is shared by all five items. The single-item English auction as a primal-dual algorithm and the condition on individual preferences (substitutes) that implies bidder-submodularity are natural extensions on the same definitions.
Revenue management is practised by firms that compete: airlines matching fares while allocating seats, retailers ordering stock and then pricing to clear it, hotels protecting rooms for late high-paying guests. Chapter 8 of Talluri and van Ryzin's The Theory and Practice of Revenue Management (2004) surveys the economics behind these situations: monopoly pricing and mechanism design, the Coase problem, advance-purchase discounts, and oligopoly in quantities (Cournot), in prices (Bertrand, Bertrand–Edgeworth with capacities), in newsvendor capacities and in RM allocations. Most of its numbered results are quoted from the literature; what the book itself establishes is a family of equilibrium arguments built on Talluri's equilibrium graph: when each firm's best response moves monotonically with the rival's action, following best-response arcs must end in an equilibrium pair. This mission formalizes those arguments, with Proposition 8.3, existence of an equilibrium in offer sets under the multinomial-logit choice model, as the goal.
A two-firm game on finite chains of strategies has payoffs , best responses and
pure Nash equilibria (IsBestResponse1, IsNashEquilibrium); its equilibrium graph has
no crossing arcs (NoCrossing1) when best-response arcs , with
always have . The chapter's games are: the RM duopoly of Sect.
8.4.1.3, two firms with capacity and fares whose high-fare demand spills over
to the rival beyond its protection level (spilloverDemand), each firm answering with
Littlewood's protection level (littlewoodResponse); the duopoly newsvendor of Example
8.16 with effective demands (effectiveDemand); linear Cournot
(cournotPayoff); Bertrand–Edgeworth price competition with capacity per firm, linear
demand and efficient rationing (beSales, bePayoff, IsBEEquilibrium); the advance-purchase
model of Sect. 8.3.6 (peakLoadRevenue, advancePurchaseRevenue); and the one-period
offer-set game of Sect. 8.4.3.2, where a firm offering its first products earns
with
(OfferFirm, offerPayoff1, CaseI, CaseII).
If both firms are in Case I () or both in Case II ( on every complete
set), the offer-set game has a pure-strategy equilibrium in complete sets:
mnl_offer_set_equilibrium.
The equilibrium-graph lemma, monotone best responses for both firms give an equilibrium (Sect. 8.4.1.3); Proposition 8.1, Littlewood responses in the RM duopoly are monotone in the rival's protection level, and the resulting equilibrium of the RM duopoly game; Example 8.16, duopoly newsvendor capacities total at least the monopoly capacity; Example 8.15, the symmetric Cournot equilibrium and its price; Theorem 8.5 (i)-(ii), the pure-strategy Bertrand–Edgeworth equilibria; and the advance-purchase comparison of Sect. 8.3.6, and .
Not targets: Theorems 8.1-8.2 (the Coase problem, subgame-perfect equilibria of an infinite-horizon game, proofs in von der Fehr and Kühn), Theorem 8.3 (Harris–Raviv priority pricing, stated with a garbled price formula), Theorem 8.4 (existence via quasiconcavity, cited), Theorem 8.5 (iii), 8.6 and 8.7-8.8 (mixed-strategy and supergame equilibria of Kreps and Scheinkman and Benoit and Krishna), Proposition 8.2 and Proposition 8.4 (the dynamic offer-set game under condition (8.32), proved in Talluri's paper), and the Kreps–Scheinkman derivation of Sect. 8.4.1.6, which rests on Theorem 8.6.
The equilibrium graph is the chapter's own contribution: a bipartite picture of best responses on chains in which monotonicity, the absence of crossing arcs, forces an equilibrium. It is the finite, combinatorial form of the monotone comparative-statics route to Nash equilibrium (Tarski's fixed point on a chain), and it is what makes RM allocation games tractable: the two-class duopoly with Littlewood responses always has an equilibrium, and the offer-set duopoly does whenever the two firms face the same sign of , while Example 8.18 shows a best-response cycle when they do not. The Bertrand–Edgeworth, Cournot and newsvendor results are the benchmarks the book uses to interpret RM competition: capacity constraints soften Bertrand's zero-profit outcome, competing in allocations tends to raise total capacity above the monopoly level, and advance-purchase discounts dominate peak-load pricing as a self-selection mechanism. None of these has a machine-checked proof.
The lemma and the goal are fixed-point arguments on finite chains: the largest best response is a monotone map of the rival's index, the composition of two monotone (or two antitone) maps on a finite chain has a fixed point, and for the offer-set game the monotonicity itself must be extracted from the ratio structure as in the appendix's inequalities (8.A.3)-(8.A.5), separately in the two cases. Proposition 8.1 is a monotonicity of tail probabilities under the pointwise order of effective demands. Example 8.16 is a short probabilistic argument that needs the identity and the strict monotonicity of the tail. Theorem 8.5 requires computing efficient-rationing sales for every unilateral deviation from a symmetric profile, through the recursive definition of residual demand, and a quadratic inequality for upward deviations in part (ii). The advance-purchase item reduces to the identity and the strict decrease of the first-order-condition function.
Products, protection levels and complete sets are natural numbers; the offer-set game's strategies are the complete sets of the book, and its payoff is (8.31) up to the positive factor and the terms independent of both offer sets. Prices decreasing in the product index are a hypothesis, as the nested-by-revenue order of Sect. 8.4.3.2. The RM duopoly is modeled through Littlewood's response, as the book's appendix argues, rather than through expected revenues. Efficient rationing is defined recursively over the firms priced strictly below a given firm, with equal sharing among firms at the same price. Example 8.16 is stated with the equilibrium conditions (8.23) and the strictly increasing distribution of aggregate demand as hypotheses. The advance-purchase item takes the first-order conditions (8.13) and (8.15) and the book's uniqueness assumption as hypotheses, the latter as strictly decreasing in (the page prints "increasing", but its footnote identifies it with the monotone marginal-revenue assumption, which is decreasing in the waiting cost). Theorem 8.5 is stated for its pure-strategy parts (i) and (ii) only.
The vehicle routing problem asks for the cheapest set of delivery routes from a depot to a set of customers when each vehicle can carry only so much. It generalizes the traveling salesman problem, which is the case of a single vehicle of unlimited capacity, and it is the operational problem behind every distribution fleet. Exact methods reach a few hundred customers; the questions that shape fleet design are structural: how does the optimal routing cost compare with the cost of a single grand tour, and how does it grow with the number of customers? Haimovich and Rinnooy Kan (1985) answered both for unit demands by bounding the optimal cost above and below in terms of the optimal TSP tour and the average distance to the depot. Chapter 11 of Snyder and Shen's Fundamentals of Supply Chain Theory (2019) presents that result with its full proof as Theorem 11.6, and it is the goal of this mission.
Nodes are the depot and customers , with distances that are symmetric,
nonnegative and satisfy the triangle inequality (VRPMetric). Every customer has demand and
every vehicle capacity , so a route is a sequence of at most distinct customers,
served by one vehicle that leaves the depot, visits them in order and returns; its length is
routeCost c L. A solution is a family of routes visiting every customer exactly once
(IsVRPSolution), with total length solutionCost; the number of routes is free. The
optimal VRP value (vrpOpt c C) is the least total length, the optimal TSP value
(tspOpt c) is the least length of a single route through all customers, and
(avgDepotDist) is the average distance from the depot to a customer.
For every metric instance with customers and capacity ,
This is vrp_tsp_bounds.
The three steps of the book's proof: the radial bound , obtained route by route from the triangle inequality and the capacity; the routing bound ; and the iterated optimal tour partition bound (11.59), that for any tour through all customers some partition of its customer sequence into consecutive routes costs at most .
The chapter's other numbered results are not targets: Proposition 11.1 (state-space relaxation of the routing dynamic program) and Theorem 11.2 (the capacitated comb inequality, proof omitted, which needs the bin-packing function ), and Theorems 11.3, 11.5, 11.7 and Lemma 11.4 (almost-sure asymptotics of random instances and the location-based heuristic), whose proofs the book cites.
Theorem 11.6 is the quantitative link between routing and the two things a planner can estimate without solving anything: the TSP length, which grows like for random customers, and the average depot distance. It says that the VRP cost is the TSP cost plus a radial term per vehicle, and that this decomposition is exact up to a factor bounded by the capacity. The radial term explains Theorem 11.7, that the optimal cost grows linearly in for fixed capacity, and the tour partition heuristic in the proof is a practical route-first-cluster-second method with a provable guarantee. The bounds are the basis of the continuous approximation formulas used in strategic distribution design.
None of these results has a machine-checked proof. The book proves Theorem 11.6 in full. The formal treatment of routes as lists and of the averaging argument over rotations of a tour is reusable for the capacitated heuristics of Sect. 11.3.
The upper bound is an averaging argument that is easy to state and fiddly to formalize: for each of the rotations of the tour's customer sequence, the sequence is cut into blocks of , and one must count, across all rotations, how often each customer is the first or last of a block and how often each tour edge is cut. The counts, each, hold only after the rotations are indexed carefully, and the passage from the average to the best rotation needs the sum of the solution costs computed exactly.
The lower bound has two parts with different flavors. The radial part needs, for each route, that the closed route from the depot is at least twice the largest depot distance among its customers, which is the triangle inequality applied along the route, followed by an averaging step that uses the capacity. The routing part is a shortcutting argument: the routes of a solution concatenate into a closed walk that revisits the depot, and removing the repeated depot visits must not increase the length. The obvious idea, that a VRP solution is itself a tour, is false, and the shortcut has to be constructed.
Routes are lists of customers, solutions are lists of routes, and the feasibility predicate
requires nonempty routes of length at most avoiding the depot, with the concatenation of
all routes a duplicate-free list containing every customer. Costs use the closed walk through
the depot followed by the route. The optimal values are infima of finite nonempty sets of reals,
nonempty because singleton routes are feasible when . The ceiling is
Mathlib's Nat.ceil of the real quotient. The number of vehicles is unrestricted, as the
section assumes; the fixed-fleet version of the problem is not modeled.
The TSP value is defined as the least route cost over all orderings of the customers, so no separate tour model is needed and the mission does not depend on the TSP mission of this series.
The definition module is shared by all five items. Problem 11.18 (tightness of both bounds) and Theorem 11.7 for deterministic instance families are natural extensions on the same definitions.
A salesman must visit cities and return home by the shortest route. The traveling salesman problem is the prototype of combinatorial optimization: easy to state, NP-hard (Karp 1972), and solved to optimality on instances with tens of thousands of nodes by branch-and-cut. In a supply chain it is the core of every vehicle routing model and of the location-routing models of the chapters that follow. Chapter 10 of Snyder and Shen's Fundamentals of Supply Chain Theory (2019) covers the symmetric metric TSP, in which distances satisfy the triangle inequality: the cutting planes of branch-and-cut (comb inequalities), the construction heuristics with their worst-case guarantees, culminating in Christofides' (1976) 3/2-approximation, and the lower bounds of Little et al. and of Held and Karp (1970). This mission formalizes those results, with Christofides' theorem as its goal.
Nodes are with distances that are symmetric, nonnegative, zero on
the diagonal and satisfy the triangle inequality (IsMetric). A
tour is a visiting order of all the nodes, of length
with indices mod (tourLength); is the least tour length (optTourLength). A tour has
an edge set (tourEdges), and for a node set the counts of tour edges inside and leaving
(edgesWithin, edgesLeaving) are the sums and
of the integer programming formulation. A comb is a handle with an odd number of
pairwise disjoint teeth, each meeting both and its complement (IsComb); when every tooth
has exactly two nodes the comb is a 2-matching configuration.
The nearest neighbor heuristic always moves to a nearest unvisited node
(IsNearestNeighborTour); the nearest insertion heuristic grows a partial tour by inserting
the unvisited node nearest to it at the cheapest position (IsNearestInsertionRun, with
cycleLength and distToTour). The minimum spanning tree heuristic doubles an MST
(IsMST, graphWeight), takes an Eulerian tour of the doubled tree and shortcuts it,
visiting the nodes in order of first appearance (IsShortcut). Christofides' heuristic
instead adds to the MST a minimum-weight perfect matching on its odd-degree nodes
(oddNodes, IsMinMatchingOn) before taking the Eulerian tour. A 1-tree rooted at is a
spanning tree on the other nodes plus two edges at (Is1Tree); the revised distances
(revisedCost) define the Held-Karp bound.
For every metric instance, every minimum spanning tree , every minimum-weight perfect matching on the odd-degree nodes of , every Eulerian tour of and its shortcut ,
This is christofides_bound.
Theorem 10.1, the reduced-matrix bound ; Theorem 10.2, Proposition 10.3 and Theorem 10.4, the 2-matching and comb inequalities valid for every tour; Theorem 10.6, ; Theorem 10.7, ; Lemma 10.9, ; Theorem 10.10, Euler's theorem; Theorem 10.11, ; Lemma 10.12, the handshaking lemma; Lemma 10.15, the 1-tree bound; Lemma 10.16, the revised distance identities; Theorem 10.17, the Held-Karp bound. Theorem 10.5 (no constant-factor approximation unless P = NP), Theorem 10.8 and the second part of Theorem 10.6 (tightness instances), Lemma 10.14 (Euclidean tours do not cross), Lemma 10.18 (the integrality gap) and Theorem 10.19 (the Beardwood-Halton-Hammersley asymptotics) are not targets.
Christofides' bound was the best approximation guarantee for the metric TSP for over forty years, until the of Karlin, Klein and Oveis Gharan (2021), and it is the reference point against which every heuristic in the chapter is measured: nearest neighbor has no constant bound, nearest insertion and the MST heuristic achieve , Christofides . The comb inequalities are the cuts that make branch-and-cut work, and the Held-Karp bound is the lower bound that tells a practitioner how far a heuristic tour is from optimal. Theorem 10.1 is the historical bounding rule of the first branch-and-bound algorithm.
None of these results has a machine-checked proof. The book proves Theorems 10.2, 10.11, 10.13 and 10.17 and Proposition 10.3 and Lemma 10.9, cites Theorems 10.6, 10.7 and 10.10, and leaves Theorem 10.4 and Lemmas 10.12 and 10.16 as exercises. The formal infrastructure for tours, shortcutting and Eulerian walks is reusable for the vehicle routing chapter.
Christofides' argument has three steps and each has a formal obstacle. The MST bound is a spanning-path argument that needs the removal of an edge from a tour to yield a tree, in Mathlib's terms a connected acyclic subgraph of the complete graph. The matching bound is the subtle one: the optimal tour shortcut to the odd-degree nodes, of length at most by the triangle inequality, is an even cycle whose alternate edges form two perfect matchings on those nodes, the cheaper of which costs at most ; formalizing the decomposition of a cycle on an even node set into two matchings, and the shortcut's length bound, is the bulk of the work. The final step, that shortcutting an Eulerian walk does not lengthen it, is an induction along the walk using the triangle inequality on the skipped stretches, and it needs the first-occurrence order to be handled explicitly.
The obvious approach to the heuristic bounds, comparing the heuristic tour directly with the optimal tour, fails; every proof goes through a spanning tree. For nearest insertion the tree is Prim's, grown in the same order as the insertions, and the bound charges each insertion cost to a tree edge; for nearest neighbor the argument of Rosenkrantz et al. bounds the sum of the largest steps by for each and sums a geometric series, which is where the logarithm comes from.
The comb inequalities are counting arguments on degrees, but the general comb of Theorem 10.4 needs the case analysis of how a tour enters and leaves each tooth. Euler's theorem in the sufficiency direction is Hierholzer's construction, which is not in Mathlib.
Tours are permutations of Fin n, so a tour is an ordering rather than an edge set, and every
tie-breaking of a heuristic is covered by a predicate on its output rather than by an algorithm.
Graphs are Mathlib SimpleGraphs on Fin n; the multigraphs of the two tree heuristics are
represented by closed walks with prescribed edge multisets, and shortcutting is the
first-occurrence order along the walk's node sequence. All degree and edge-set computations use
classical decidability. Theorems on tours assume where a tour must have distinct
edges, otherwise.
Theorem 10.1 is stated for the reduction of the full off-diagonal matrix, because the book's upper-triangular version is false: a random metric instance violates it, since the last row and first column of a triangular matrix are empty and the two edges at a node need not be one row and one column entry. The full-matrix version is the statement of Little et al. It is stated for , because a one-node "tour" is a self-loop that no off-diagonal entry constrains.
Theorem 10.4 is stated with the comb inequality's right-hand side corrected to , the standard form. The book prints , which contradicts its own 2-matching special case (10.15) and is weaker by . The corrected statement implies the printed one.
The -tree root is an explicit node , the book's node . The nearest insertion run is a sequence of lists indexed by iteration, and the theorem compares the -th list's closed length with ; a run always exists, so the hypothesis is satisfiable.
The definition module is shared by all fifteen items. Theorem 10.8 and Problem 10.12 (tightness of the bounds of ), the second part of Theorem 10.6, and Lemma 10.18 on the integrality gap are natural extensions on the same definitions.
A retailer marking down a seasonal line, an airline raising fares as seats sell, a manufacturer pricing while restocking: each sets prices over time against a finite and changing inventory. Chapter 5 of Talluri and van Ryzin's The Theory and Practice of Revenue Management (2004) collects the structural theory of that problem. Without replenishment, the Bernoulli-arrival model of Gallego and van Ryzin (1994) gives a marginal value of capacity that falls with inventory and with time, hence prices that jump up at each sale and drift down between sales, and the deterministic fluid model bounds it from above. With replenishment, the model of Federgruen and Heching (1999) has a jointly concave and supermodular continuation value, from which the base-stock, posted-price policy follows: below a base-stock level order up to it and post a fixed price, above it order nothing and discount, more the higher the inventory. This mission formalizes those results with Proposition 5.3 as the goal.
Bernoulli demand (Sect. 5.2.2.2). One customer arrives per period with a random
willingness to pay; the firm's decision is the demand rate , the probability of a
sale at the inverse-demand price , with revenue rate
(revenueRate). The value function (5.12) is
, ,
(bernoulliValue), and (bernoulliDelta). The
deterministic model (5.1) maximizes over rates with
(deterministicValue).
Pricing with replenishment (Sect. 5.3.2). Inventory may be negative (backorders). In
period with inventory the firm orders up to at unit cost , chooses a
rate , sells the random demand
(additive, multiplicative or mixed noise), and pays the convex cost on ending inventory.
The value function (5.20) is
with the continuation value
(ReplPricing.value, contValue). Assumption 7.2, marginal revenue decreasing, is the
concavity of .
For every period, is jointly concave on , is
concave on , and has increasing differences in , the supermodularity
that the book states through its partial derivatives: replenishment_concave_supermodular.
Proposition 5.2, the marginal value of capacity in the Bernoulli model decreases in and in ; the upper bound of Sect. 5.2.2.3, the optimal deterministic revenue dominates the optimal expected stochastic revenue; and the base-stock, posted-price structure of Sect. 5.3.2.1, derived from Proposition 5.3: below the unconstrained optimum order up to it and use , above it order nothing and use a rate at least that is nondecreasing in the inventory.
Proposition 5.1 and Lemma 5-5.A.1 (the continuous-demand model without replenishment) are not targets; see the formalization scope. The deterministic sections (efficient prices, discrete price sets), the asymptotic optimality of the deterministic heuristic, the infinite-horizon stationary problem and the multiproduct and finite-population models carry no numbered results.
Proposition 5.3 is the structural core of joint pricing and inventory control: joint concavity makes the period problem a concave program, and supermodularity is what turns its solution into a policy, the base-stock, posted-price rule that Federgruen and Heching showed optimal and that later work on pricing with inventory builds on. Proposition 5.2 is the reason optimal dynamic prices in the stochastic single-item model rise at every sale and fall while inventory sits, the behaviour of Figure 5.5, and the deterministic upper bound is what justifies the fluid model as a benchmark and a heuristic, the pattern quantified in Table 5.6. None of these has a machine-checked proof; the replenishment result in particular needs the interplay of concavity, expectation and partial maximization on all of .
Proposition 5.2 is an induction whose step compares suprema over the rate interval, with the boundary condition breaking the recursion at and requiring . The deterministic bound is an induction on periods that uses the concavity of the deterministic value in the inventory (a concave program's value) to absorb the two branches of the Bernoulli recursion. The goal needs: integrability and continuity of under bounded noise; that the expectation of a concave function of an affine map is jointly concave, and its increasing differences from those of the concave integrand; that a partial supremum of a jointly concave function over the convex feasible set is concave in ; and the boundedness of the objective so that every supremum is a real number. The base-stock item is the segment argument that moves an unconstrained maximizer onto the boundary and a monotone comparative-statics argument on the supermodular objective, with maxima attained by continuity on the compact rate interval.
Periods are natural numbers with value t the value with periods to go, the
maxima are suprema, and the book's ranges are hypotheses. The demand is affine in the rate,
which is the additive and multiplicative models the book names; with a merely convex demand
(Assumption 5.1) the joint concavity of Proposition 5.3 fails when is not
monotone, and the noise has bounded support, strengthening Assumption 7.6. The
partial-derivative statements (iii)-(iv) are in difference form. Proposition 5.1 is not
formalized: its model (5.11) evaluates at negative inventories the model
does not define while truncating revenue at , and its Lemma 5-5.A.1 (joint concavity of
) is false as stated, its Hessian argument mistaking an indefinite matrix for a negative
definite one; a counterexample is in the mission's check. The deterministic model restricts
rates to , the rates the Bernoulli model can realize.
Every model in the earlier chapters of this series treats demand as the uncertain quantity and supply as given. Chapter 9 of Snyder and Shen's Fundamentals of Supply Chain Theory (2019) reverses the roles: demand is deterministic and the supplier fails. A disruption is a binary event, modeled as a two-state Markov process between up and down periods, during which nothing can be ordered. The chapter's thesis, from Snyder and Shen (2006), is that supply uncertainty is a mirror image of demand uncertainty: the optimal base-stock level has the same critical-fractile form as the newsvendor solution but with the fractile taken over the disruption-length distribution (Tomlin 2006), and consolidation, which pools demand risk, now does nothing to expected cost and multiplies its variance, the risk-diversification effect of Schmitt, Sun, Snyder and Shen (2015). The chapter closes with the reliable fixed-charge location problem of Snyder and Daskin (2005). This mission formalizes the chapter's theorems on disruptions, with the risk-diversification theorem as its goal.
A supplier that is up is disrupted next period with probability ; one that is down
recovers with probability . The disruption chain records when the supplier is up
and in the -th consecutive period of a disruption; its stationary distribution is
and (disruptionPmf),
with distribution function (disruptionCdf).
A single location faces demand per period, pays per unit held and per unit
backordered per period, and follows a base-stock policy: it orders up to in every up
period and nothing in down periods. In the -th period of a disruption it has
units on hand or backordered, so its cost is
(periodCost), and the expected cost per period is
(meanCost), with variance over the disruption state (varCost). The critical fractile
and , the smallest with , determine the
optimal level.
In the reliable fixed-charge location problem (RFLP), sites fail independently with
probability and each customer is assigned to a chain of facilities: its level- facility
serves it when the closer facilities are disrupted, until it is assigned to an emergency
facility that never fails and charges the penalty . The objective (9.61) is fixed
cost plus expected transportation cost, with coefficients
(rflpPsi, rflpCost) under the constraints (9.62)-(9.67) (RFLPFeasible).
For identical locations and the centralized location formed by merging them (demand ):
that is, an optimal single-location level scales to the optimal centralized level ,
the centralized expected cost at is times the single-location cost, and its variance is
times the single-location variance. This is risk_diversification.
Lemma 9.2, the stationary distribution and distribution function of the disruption chain; Lemma 9.4, that the optimal base-stock level is a multiple of ; Theorem 9.5, , as the least minimizer of ; and Theorem 9.10, that in every optimal RFLP solution consecutive backup assignments are ordered by cost. Theorem 9.3, the optimality of base-stock policies, is cited by the book to Song and Zipkin without a model of the policy space and is not a target; Proposition 9.1 and the multisupplier results of Sect. 9.4 are left for a later mission, as discussed below.
Theorem 9.5 is the supply-side newsvendor formula: it says exactly how much inventory buys protection against disruptions of a given length, and it underlies the disruption models used in practice for raw-material buffers. Theorem 9.9 is the chapter's central insight and the reason supply and demand uncertainty call for opposite strategies: pooling reduces expected cost under demand uncertainty but only redistributes risk under supply uncertainty, concentrating it. Its three identities are what a risk-averse planner needs to compare the two designs by a mean-variance criterion. Theorem 9.10 is what lets the RFLP be formulated without ordering constraints and solved by Lagrangian relaxation like the UFLP.
None of these results has a machine-checked proof. The book proves Theorem 9.5 and the identities behind Theorem 9.9, sketches Lemma 9.4, and leaves Lemma 9.2 and Theorem 9.10 as exercises. The formal treatment of the piecewise-linear cost and its finite differences is reusable for the yield-uncertainty and multi-supplier models of the same chapter.
The cost is an infinite series whose terms grow linearly in against a geometric weight, so every statement about it begins with summability, and the finite-difference identity requires exchanging a difference with a sum. Theorem 9.5 then needs the convexity and piecewise linearity of to pass from a sign condition on slopes at multiples of to a global minimum over all real , and the identification of the least minimizer needs the slopes to be strictly negative below . The obvious idea, treating the problem as a discrete newsvendor over multiples of , is only half of the argument: it does not by itself exclude non-multiple minimizers, which is what Lemma 9.4 asserts.
Lemma 9.2 is elementary but the stationary equations involve a series over all down states, and the proof must establish summability before manipulating it. Theorem 9.9's scaling identities are termwise, but the optimality transfer in part 1 requires the scaling to preserve minimizers, which follows from the cost identity holding for every .
Theorem 9.10 is an exchange argument on a binary program with layered constraints. The delicate case is the emergency facility: swapping it into a lower level is infeasible, and the correct move is to promote it and drop the later assignment, which changes the constraints for every higher level; the argument must show feasibility of the modified solution level by level.
The disruption distribution is given by Lemma 9.2's formula rather than defined as the stationary distribution, and Lemma 9.2 shows it satisfies the stationary equations; the theorems assume and , under which every series is a geometric series times a polynomial and is summable. The quantity enters Theorem 9.5 as a natural number characterized by and for , which exists since ; the conclusion asserts both optimality and leastness of among all real levels.
Theorem 9.9 is stated as the scaling of the single-location functions; the decentralized totals
and are the mean and variance of a sum of independent copies, which the book
asserts rather than derives, and are not modeled separately. In the RFLP, levels are indexed by
Fin m, the emergency facility is a designated index whose data satisfy the book's
conventions through the hypotheses, and demands are positive with , both needed:
with or backup assignments are free and any order is optimal.
The EOQ with disruptions (Proposition 9.1) is a renewal-reward derivation without a formal model of the renewal process in the book, and the multisupplier newsvendor of Sect. 9.4 (Lemma 9.6, Theorems 9.7 and 9.8) rests on differentiability conditions the book defers to Dada et al. and on a lemma it leaves as an exercise; both are natural extensions on the same definitions rather than targets here.
Choosing where to open distribution centers is the strategic decision that fixes a supply chain's shape for years. The basic model, the uncapacitated fixed-charge location problem (UFLP) of Balinski (1965), trades the fixed cost of opening sites against the cost of transporting demand from open sites to customers. It is NP-hard, yet routinely solved to optimality, and the reason is a fact about its relaxations: the LP relaxation is unusually tight, and Lagrangian relaxation, which Cornuejols, Fisher and Nemhauser (1977) brought to location problems, gives the same bound with a subproblem solvable by inspection. Chapter 8 of Snyder and Shen's Fundamentals of Supply Chain Theory (2019) develops the UFLP, its Lagrangian relaxation and Erlenkotter's (1978) DUALOC dual-ascent method, then the p-median problem with Hakimi's (1965) node-optimality theorem and the covering models. This mission formalizes the chapter's numbered results, with the equality of the Lagrangian and LP bounds as its goal.
Customers have demands ; candidate sites have fixed costs ; shipping
one unit from to costs . A solution opens sites () and assigns
demand fractions (, , ); its cost is
(uflpCost, UFLPFeasible). The optimal value is
(uflpOpt); relaxing to gives the LP relaxation with
value (uflpLP).
Lagrangian relaxation removes the assignment constraints and charges per unit of
violation. For fixed multipliers the subproblem (UFLP-LR) minimizes
over ,
binary, (lagrObjective, LagrFeasible), with value (zLR). It
separates by site: the benefit of opening is
(benefit), and is opened iff . The best bound is the Lagrangian dual
value (zLRbest).
DUALOC works with the condensed dual of the LP relaxation, whose variables satisfy
with . A dual solution and
a site set form a primal-dual pair (PDP) when these constraints are tight on and
every customer has a site in with ; the primal solution opens and
assigns each customer to its nearest open site (NearestIn, primalX, primalY).
For the p-median problem on a network, the customers are the nodes, is the shortest-path
distance between nodes, and a facility may sit at position along an edge of length
, at distance from node (NetPoint, netDist).
The p-center problem minimizes the largest distance from a customer to its nearest of
open sites; pCenterValue c p is its optimal value.
For every instance with at least one candidate site,
This is lagrangian_equals_lp.
Theorem 8.1, the closed form with its optimal solution; the bounds (8.16) and (8.19) ; Theorem 8.3, the variable-fixing tests; Lemma 8.4, the DUALOC duality gap ; Lemma 8.6, the characterization of complementary slackness violations; Theorem 8.7, Hakimi's theorem that some nodes are optimal among all -point sets; Lemma 8.8, the equivalence between the -center value being at most and a set cover of radius with at most sites. Proposition 8.5, which concerns the output of a specific procedure, is not a target.
Corollary 8.2 explains the behavior of every Lagrangian location code: the bound cannot beat the LP bound, so its value lies in the ease of the subproblem and in extensions to nonlinear location models (the location model with risk pooling of Chapter 12) where no LP is available. Theorem 8.1 is the subproblem solution those codes use; Theorem 8.3 is the variable-fixing device of Daskin, Snyder and others that shrinks branch-and-bound trees. Lemmas 8.4 and 8.6 are the analytical core of DUALOC, the method that made large UFLP instances solvable in the 1970s. Hakimi's theorem is the reason the -median problem is a discrete problem at all, and Lemma 8.8 is the reason -center problems are solved by bisection over covering problems rather than by their weak MIP formulation.
None of these results has a machine-checked proof. The book proves Theorems 8.1 and 8.3 and Lemma 8.6, cites Corollary 8.2 to Appendix D and Theorem 8.7 to Hakimi, and leaves Lemmas 8.4 and 8.8 as exercises. The formal treatment of the integrality property and of Lagrangian duality for a linear objective over a product of boxes is reusable for the p-median and capacitated variants the chapter goes on to discuss.
The goal is an LP duality statement in disguise, and the obvious idea, that is the dual function of the LP relaxation, is exactly what needs proof. Two facts must be established: that for fixed the subproblem over binary has the same value as over , because after the optimal is substituted the objective is linear in ; and that the supremum over of the resulting concave piecewise-linear function equals the LP minimum. The second is strong duality for a linear program, which Mathlib does not provide ready-made; it has to be obtained either through a Farkas-type argument or by exhibiting, for the LP optimum, a multiplier vector that attains it, which for this problem can be read off the LP dual. The book proves none of this; it invokes Lemma D.3.
The bounds (8.16) and (8.19) are easier but not free: the infima and suprema defining , and must be shown attained, which needs finiteness of the binary choices and compactness of the assignment polytope. Theorem 8.3 depends on the value of the subproblem with one variable forced, which is Theorem 8.1 applied to a modified instance. Hakimi's theorem needs a concavity argument in each point's position and a bookkeeping step, since moving several points to nodes may merge them and the result must still have exactly nodes. Lemma 8.8 is combinatorial and short once the -center value is identified with a minimum over -subsets.
Customers and sites are Fin n and Fin m; demands, costs and fixed costs are arbitrary
reals, as the book's formulations are, and the theorems that need it assume . Optimal
values are infima or suprema of the sets of attainable objective values, all of which are
nonempty and bounded under the stated hypotheses. The Lagrangian dual value is a supremum over
all real multiplier vectors, so Corollary 8.2 asserts in particular that the supremum equals the
attained LP value.
The DUALOC statements take the nearest-facility assignment as a function a with the
defining property, so ties are resolved by the hypothesis, and the complementary slackness
violation is written exactly as (8.51) with substituted. Hakimi's theorem is stated
for a family of points with repetition allowed, which is stronger than for a set. It assumes
what the book's network supplies: the node distances satisfy the triangle inequality, since they
are shortest-path distances, and every edge carrying a point is at least as long as the distance
between its endpoints. The argument needs both: they make the ends of an edge coincide with its
nodes, and without them a point on a short fictitious edge can beat every node. The
set covering value in Lemma 8.8 is expressed through the existence of a cover with at most
sites rather than as a natural-number infimum, whose value on infeasible instances would
falsify the equivalence.
The definition module is shared by all ten items. The Lagrangian relaxation of the -median problem (Sect. 8.3.2.2), the continuous knapsack subproblem of the capacitated problem, and Proposition 8.5 on the dual-ascent procedure are natural extensions on the same definitions.
A retailer facing uncertain single-period demand and buying from a supplier at a wholesale price orders less than the two of them together would want. The reason is not irrationality but incentives: the retailer bears the whole cost of unsold stock while the supplier collects a margin on every unit ordered, so each party marks up its own cost and the combined markup, Spengler's (1950) double marginalization, depresses the order. Pasternack (1985) showed that a buyback credit for unsold units, priced correctly, realigns the retailer with the chain, and Cachon (2003) surveys the contracts that followed. Chapter 14 of Snyder and Shen's Fundamentals of Supply Chain Theory (2019) develops this as a Stackelberg game on the newsvendor model: the supplier sets contract terms, the retailer sets the order quantity. This mission formalizes the chapter's seven theorems, with the buyback allocation theorem, which shows that buyback both coordinates the chain and can divide its profit in any proportion, as the goal.
Demand is a random variable with law on and mean . The retail price is
; the supplier's and retailer's per-unit costs are and with ;
lost sales cost the two parties goodwill penalties and with ; unsold
units salvage for (ContractData). With the expected
sales (expSales) and the expected leftover (expLeftover), a transfer
payment from retailer to supplier determines the two profits (retailerProfit,
supplierProfit),
whose sum (chainProfit) is independent of the
contract. The chain-optimal quantity maximizes ; the retailer's and supplier's
optimal quantities , maximize their own profits. A contract coordinates the
chain when , stated here as equality of the sets of maximizers, and is a
coordinating contract type when some choice of its parameters does this with both profits
positive.
The four contracts are their transfer payments. Wholesale price: . Buyback:
, the supplier crediting per unsold unit, with
and of (14.22). Revenue sharing: the retailer keeps a fraction of sales
and salvage revenue, , with of
(14.34). Quantity flexibility: the supplier reimburses the retailer's loss on
unsold units up to , , with
of (14.46). For buyback, is the
retailer's share of the chain profit (buybackShare), and (buybackB1,
buybackB2) are the credits at which one party earns everything.
Under buyback with at the chain-optimal , the retailer's profit is decreasing and the supplier's increasing in , with and
the supplier losing money for , both earning positive profit for , and
the retailer losing money for . This is buyback_allocation.
Equation (14.8), maximizes iff ; Theorem 14.1, the wholesale price contract coordinates iff , at which the supplier's profit is negative; Theorem 14.2, whenever ; Theorem 14.3, for IGFR demand the supplier's induced profit is unimodal; the identities (14.27) and (14.28), and its complement under buyback; Theorem 14.4, buyback with coordinates; Theorem 14.6, revenue sharing with coordinates; Theorem 14.7, quantity flexibility with makes optimal for the retailer.
The chapter's theorems are the analytical basis of contract design in newsvendor supply chains. Theorem 14.1 and 14.2 make double marginalization precise: coordination by price alone is possible only at a price the supplier rejects, and any acceptable price makes the retailer under-order. Theorem 14.3 is what lets the supplier optimize the wholesale price at all, and is the reason the IGFR class of Lariviere and Porteus (2001) is standard in the field. Theorems 14.4 to 14.6 show that buyback and revenue sharing coordinate and, through the share , that the chain profit can be split arbitrarily, so a coordinating contract can be made acceptable to both parties. Theorem 14.7 shows the limits: quantity flexibility coordinates the retailer but not necessarily the supplier.
None of these results has a machine-checked proof. The book proves Theorems 14.1, 14.3, 14.4, 14.5, 14.6 and 14.7 and leaves 14.2 as an exercise. The formalization of the fractile characterization and of the affine profit identities is reusable for the many contract types (sales rebates, quantity discounts) the chapter cites but does not analyze.
The wholesale price results are first-order conditions on concave functions, and the difficulty is entirely in the analysis: has derivative for every when is continuous, which is a differentiation under the integral that has to be carried out for a Lipschitz integrand and an arbitrary law, and the maximizers of the concave profit must then be identified with the solutions of the fractile equation, including existence by the intermediate value theorem. Theorem 14.1's "only if" direction requires that a coincidence of maximizer sets pins the fractile and hence the price, which is where strict monotonicity of enters.
Theorem 14.3 is the delicate one. The obvious approach, concavity of , fails:
the book stresses the function is not concave in general. The proof is a sign-change argument
on the derivative (14.16), which is times a bracket that IGFR makes decreasing,
minus a constant; one must show the derivative is positive near , eventually negative, and
crosses zero exactly once, and that the last needs both strictly decreasing and the
bracket positive at the crossing. Working with a density in Mathlib means relating the
withDensity law to the distribution function throughout.
The buyback, revenue sharing and quantity flexibility theorems are algebra once the right identity is found: is an affine function of with slope . The formalization must handle the boundary cases the book glosses over, where or and one party is indifferent among all quantities, so "the same maximizes" holds only in one direction. Theorem 14.5 also needs , a Jensen-type bound , for , and the ordering needs , which the book's proof does not isolate.
Demand is an arbitrary probability law on with finite mean, not assumed
nonnegative; the book's own examples use normal demand. Optimal quantities are maximizers over
all of (IsMaxOn … Set.univ), and coordination is the coincidence of maximizer
sets, with the degenerate endpoints of the parameter ranges stated as one-directional. Where the
book uses a density, continuity of the distribution function (NullSingletonClass) is assumed
instead, except in Theorem 14.3, where the density is explicit, continuous on
(so the exponential law is included), positive on , and IGFR on .
Strict monotonicity of on is never assumed, since it would rule out every
nonnegative demand law. Theorem 14.1 assumes and a positive chain
optimum, , both implicit in the book's proof.
The transfer payments are functions of and the profits are defined for every , so the
theorems compare values of one family of functions; the book's is with
Mathlib's cdf, and the quantity flexibility integral is an interval integral. Theorem 14.5
takes , and as hypotheses. Without positive goodwill costs
its strict inequalities and fail (at , ; at
, ).
The definition module is shared by all eleven items. The equivalence (14.42)-(14.43) of revenue sharing and buyback, the supplier's stationarity under quantity flexibility (Problem 14.11) and the allocation results for revenue sharing (14.40)-(14.41) are natural extensions on the same definitions.
Chapter 9 of Axsäter's Inventory Control opens with the observation that in a multi-echelon system it is not optimal to choose batch quantities installation by installation: the batch at one site is the demand pattern of the next site upstream. Even with constant customer demand the exact optimum can be complicated, and the book's Example 9.4 shows a four-stage serial system whose optimal batch at one stage alternates between two values over time. Roundy (1985, 1986) showed that this complexity can be avoided at a guaranteed price: restrict every batch quantity to be a power of two times a common basic quantity, nested from stage to stage, and the best such policy costs at most 2 % more than the optimum. The book presents the result for a serial system and remarks that the same approach handles assembly and distribution systems and, in Sect. 7.3.1.2, joint replenishments. It is the capstone of Chapter 9 and the multi-echelon payoff of the powers-of-two analysis of Chapter 7.
A serial system has installations; installation produces item from one unit of item , item is obtained from an outside supplier, and item 1 faces a constant, continuous final demand . Lead-times are zero, shortages are not allowed, production is instantaneous, and each batch quantity is constant over time. Installation has an ordering cost per batch and an echelon holding cost per unit and time unit, charged on the echelon stock (the stock at installation and everything downstream), so that the cost per time unit is the sum of single-item costs of the chapter 4 form,
The book first works out the two-level case, where the optimum has for a positive integer , the cost (9.9) is the EOQ cost with modified parameters and , and the best is found from by a rounding rule.
For stages, Roundy's constraints (9.16) require with nonnegative integers , so that every solution is nested. The relaxed constraints (9.18) require only ; they are implied by (9.16), the relaxed problem is convex with linear constraints, and its solution is computed by aggregating consecutive stages whose cost ratios decrease. Roundy's solution rounds to for a basic quantity , chosen as in Proposition 7.2.
For , , and any minimizer of over positive batch quantities satisfying (9.18), there exist and integers such that satisfies (9.16) and
The two-level results of Sect. 9.2.1: the equivalence of the installation and echelon cost forms (9.6) and (9.9); the optimal and cost (9.10)-(9.11) for a given ; the closed form and convexity of (9.12) and the real minimizer (9.13); and the integer rounding rule with its corollary that forces . For stages: existence of the relaxed optimum; the aggregation lemma, that forces ; that (9.16) implies (9.18), so the relaxed optimum bounds every powers-of-two policy from below; and that rounding to the nearest power of two times is monotone and lands within a factor .
The result itself. Roundy's theorem replaces an intractable lot-sizing problem by a closed-form computation with a provable 2 % guarantee, and the policies it produces are the nested, periodic schedules that production planning wants anyway. In Example 9.4 the rounding with is already within 0.7 % of the relaxed bound. The two-level analysis has its own use: the modified parameters and are what the Blackburn-Millen heuristic of Sect. 9.3.2 feeds to the Wagner-Whitin algorithm under time-varying demand, and the condition tells when a two-stage system collapses to one stage.
Formalizing it. The book proves the bound in a paragraph that leans on three earlier results:
Proposition 7.2 for the rounding, the Lagrangean relaxation for the lower bound, and the
aggregation algorithm for the structure of . Formalizing it makes explicit
what the paragraph glosses: that the multipliers vanish off tight constraints, that equal
quantities round to equal quantities, and that the comparison class is the class of nested
constant-batch policies. The published Proposition 7.2 (pot_two_percent) and the mean value
are cited as reference items. Nothing here is open; no statement has a
machine-checked proof yet.
The obvious argument, rounding item by item and invoking Proposition 7.2 for each, does not work: Proposition 7.2 bounds the rounded cost relative to each item's unconstrained optimum, and is generally not that optimum. The proof must pass through the Lagrangean relaxation (9.19)-(9.20), under which is the unconstrained optimum for the modified holding costs , apply Proposition 7.2 there, and transfer the bound back using complementary slackness: the multiplier is positive only where , and equal quantities round to equal quantities, so the correction terms vanish for both and its rounding. A solver therefore needs the KKT conditions for this convex program, or an equivalent direct argument through the aggregation structure (within an aggregate all quantities are equal and their sum is an EOQ problem). The two-level statements and the rounding lemma are elementary.
Stages are indexed by Fin N; the cost is serialCost A e d Q = ∑ i, eoqCost (A i) d (e i) (Q i)
with eoqCost imported from the chapter 4 definitions, and the two-level cost is
eoqCost (A1 + A2/k) d (e1 + k e2) Q1 by definition, so the published eoq_optimal and
eoq_cost_at_eoq apply to it directly. SerialNested and SerialPowerOfTwo are the constraints
(9.18) and (9.16) on consecutive indices; for both hold vacuously and the goal is
Proposition 7.2 for one item. potRound q Q is .
All theorems assume and positive batch quantities. The book says "nonnegative ordering and echelon holding costs"; strict positivity is needed for the relaxed problem to have a solution at all ( or sends the optimal to or ), and it is what the book's own examples satisfy. The relaxed optimum enters the goal as a hypothesis, with existence stated separately; uniqueness is not used. The constant is the exact .
Two readings are excluded. The bound is not against an arbitrary nested , for which it would be false, but against the relaxed optimum; and the comparison class is stated as nested constant-batch policies, the class the relaxed problem bounds directly, not the book's larger class of time-varying policies, which would need a dynamic model. The definitions are reusable for assembly systems and for the joint replenishment problem of Sect. 7.3.1.2, whose Roundy analysis is the same with a fictive item 0 of zero holding cost; contributions in that direction are welcome.
Every model in Chapters 5 and 6 of Axsäter's Inventory Control assumes at the outset that the ordering policy is of or type. Section 6.2 asks whether better policies exist and answers, for the case in which there are no ordering costs but every order must be a multiple of a fixed batch quantity , that none do: Proposition 6.1, "an policy is optimal", with a proof the book attributes to Chen (2000). For it is the optimality of an order-up-to- policy in the absence of ordering costs, and for continuous or Poisson demand it transfers to policies, which are then the same thing. The proposition is the one place in the book where a policy is compared against every feasible alternative rather than against other members of its own family, and its proof is short enough to be given in full, which makes it the natural capstone of Chapter 6.
Demand is compound Poisson: customers arrive according to a Poisson process with rate and each demands an integral number of units, with sizes independent and identically distributed with law on the positive integers, independent of the arrival process. The book's standing assumption that not all demands are multiples of some integer larger than one is kept. Writing for the -th arrival time, for the number of arrivals by time and , the total demand by time is .
The replenishment lead-time is constant and , the demand over a lead-time, has law . A holding cost and a shortage cost per unit and time unit are charged. There are no ordering costs, but all orders must be multiples of a given batch quantity and can only be triggered by customer demands. A policy is therefore any rule that decides at each demand epoch how many batches to order; with initial position the inventory position evolves as (Eq. 6.22), and .
The standard argument of Sect. 5.3.2 gives the cost rate at time as
the expected holding-plus-shortage cost rate of an inventory level (Eq. 6.20), which is convex in with as . The band cost is and denotes an integer minimizing . The policy orders, as soon as the position is at or below , the smallest number of batches that brings it above ; its position lives in the band from the first order on. The performance measure is the long-run average cost rate as .
Almost surely, (1) for every policy and every ,
and (2) the policy attains it:
Lemma 6.1, that is convex and minimized at the representative of in the band; the closed form of the position, until the first order and the band representative of afterwards; the uniform occupation of the band by the reduced process , the book's "the steady state distribution can be shown to be uniform", and its consequence that the long-run average of is ; Proposition 5.1 in the same ergodic form for the policy; and the two halves of the goal as separate statements.
The result itself. Proposition 6.1 is what licenses the two-parameter policies on which the rest of the book's single-echelon theory is built, and it does so for the practically important case of batch ordering (pallets, containers, production lots). Its proof also explains why the policy works: the only quantity a policy controls is the residue class of the inventory position modulo , which no policy can influence, and the position within that class, which the policy always sets to the cheapest possible value. The book extends the same reasoning to other cost structures and to periodic review.
Formalizing it. The proposition is a theorem about the class of all policies, and the book's proof is pathwise: Lemma 6.1 compares any policy with the reduced process instant by instant, and an ergodic statement about the reduced process does the rest. Formalizing it therefore forces the policy class, the demand process and the long-run average to be written down exactly, which the book never does. Nothing here is open; no statement has a machine-checked proof yet.
The pointwise comparison is elementary once Lemma 6.1 is available, and Lemma 6.1 is discrete convexity. The difficulty is entirely in the ergodic statement: that the reduced position (the band representative of ) spends a fraction of the time at each point of the band, almost surely. In discrete time this is the convergence of occupation frequencies for an irreducible random walk on with step law modulo , where irreducibility is exactly the aperiodicity assumption on , and the book's double-stochasticity argument (Eq. 5.33-5.34) identifies the uniform law as stationary. Passing to continuous time adds the exponential holding times: the time average is the arrival average weighted by i.i.d. holding times independent of the walk, which a strong law of large numbers turns back into the discrete statement. Mathlib has the strong law and the exponential law but no ergodic theorem for finite Markov chains, so that is the groundwork a solver must build. The naive route through the stationary distribution of the embedded chain at demand epochs is not enough on its own: for pure Poisson demand that chain is periodic, and the book itself notes it.
A CompoundPoissonDemand on a probability space packages the rate, the size law with
and the aperiodicity condition, and two sequences of random variables, the gaps and the sizes,
with their laws (expMeasure lam, the given pmf), independence within each sequence, and
independence between the sequences. Arrival times are partial sums of the gaps, count t is
the supremum of , and cumDemand n is the partial sum of the sizes. A policy
is a function m : ℕ → Ω → ℕ with no measurability requirement; ipPath and ipAt are the
position after the -th demand and at time ; rqIP and rqOrders are the policy,
with a theorem identifying rqOrders as a policy in the general sense. avgCost is
with for . The cost function
is sPolicyCost from the previous mission, applied to a DiscreteDemand that the hypotheses
tie to the process as the law of the demand in .
Conventions: , , ; is any minimizer of (it exists by
the divergence of , proved in the previous mission); is arbitrary. count and the
interval integral take junk values on the null set where arrivals do not tend to infinity, which
the almost-sure conclusions absorb. "" is stated as "for every ,
eventually ", avoiding a liminf on that could be junk.
Two readings that would trivialize the goal are excluded: the lower bound is over every rule, not over stationary or measurable ones, and the achievability half is a genuine limit, not a bound. The demand model and the occupation-frequency theorems are reusable for Proposition 10.1 and the batch-ordering models of Sect. 10.5; contributions establishing the ergodic theorem for irreducible chains on a finite cyclic group are welcome and would close most of this mission.
An policy has two parameters. Chapter 4 of Axsäter's Inventory Control chooses the batch quantity from a deterministic model, and Chapter 5 chooses the reorder point from a stochastic one with held fixed; the book presents this two-step practice as an adequate approximation. Section 6.1 asks what is lost by it and shows how to optimize both parameters jointly in one stochastic model. For discrete demand the answer, due to Federgruen and Zheng (1992), is an algorithm of remarkable simplicity: increase one unit at a time, keep the reorder point optimal along the way by a one-line rule, and stop at the first for which the cost goes up. The claim that this stopping rule finds the global optimum over all pairs is the capstone of Sect. 6.1.1.1 and the goal of this mission. The same idea is reused in the book for policies (Sect. 6.1.1.2) and, in continuous form, for normally distributed demand (Sect. 6.1.2).
An item is controlled by a continuous review policy with integral reorder point and batch quantity . Demand is discrete and stationary; the lead-time demand takes values in the nonnegative integers with probabilities and has a finite mean . The average demand per unit of time is . Costs are a holding cost and a shortage cost , both per unit and time unit, and an ordering cost per batch.
The building block is the cost of an policy that keeps the inventory position at a fixed integer . By the standard argument of Sect. 5.3.2 the inventory level a lead-time later is , and the average holding and shortage cost rate is (Eq. 6.3)
Under the policy the inventory position is uniformly distributed on (Proposition 5.1), so the total average cost rate is (Eq. 6.4)
and (Eq. 6.5), attained at an optimal reorder point . The ready rate links the cost to service: raising the reorder point by one unit changes the cost by (Eq. 5.60).
Let be the smallest batch quantity with and let be an optimal reorder point for . Then
The increment identity ; convexity of on together with as ; Eq. (5.60) and the convexity of in ; Eq. (5.61), that the largest with is optimal for its ; existence of an optimal for every ; the recursion (6.6)-(6.7), chosen by comparing with , and ; the equivalence and the monotonicity of that minimum in ; and the existence of some at which the costs stop decreasing.
The result itself. Joint optimization typically enlarges the batch and lowers the reorder point relative to the two-step procedure, and the book's Example 6.1 puts the resulting cost saving at a few percent. The Federgruen-Zheng procedure makes the exact joint optimum for discrete demand as cheap to compute as the two-step approximation, because each step of the recursion evaluates at two points. It is the exact benchmark against which the book's approximate techniques for normal demand (Sects. 6.1.2 and 6.1.3) are judged, and its structural core, that the optimal window of consecutive inventory positions grows one neighbour at a time, is the discrete-convexity fact behind the whole of Sect. 6.1.
Formalizing it. The mathematics is settled. What the mission produces is a Lean development in which the steps the book marks "evident" and "obvious" are separate statements: that the recursion preserves optimality, that the marginal cost of enlarging the batch is monotone, and that a minimum over exists at all. None of the statements has a machine-checked proof yet.
The obvious first idea, to argue that is convex in and stop at its first increase, does not work as stated: is a minimum over of a ratio and is not convex in general. What is true, and what the proof uses, is that the marginal cost is nondecreasing, because it equals the smaller of the two -values adjacent to the optimal window. Establishing the recursion (6.6) is where discrete convexity is needed: one must show that the best window of consecutive positions is obtained from the best window of by adding a neighbour, which fails for non-convex . The window sums are themselves convex in with increments , and the argument compares a competing window with the optimal one through the end terms. The remaining steps are finite algebra and an induction on from .
A DiscreteDemand is a function with ,
and a summable first moment; is a finite sum over , empty for
. The reorder point ranges over and the batch quantity over ,
with assumed in every statement because Lean's division by is . Convexity of a
function on is stated as nondecreasing increments, and divergence as
Tendsto g (cocompact ℤ) atTop.
enters the goal as a function CQ together with the hypothesis that CQ Q is the least
value of ; the stopping index is characterized by the two conditions
that define "the smallest with ", and by optimality at .
That these objects exist is the content of two separate items, so the goal is not vacuous: a
minimum over exists for every because , and the costs cannot decrease
forever because the average of the smallest values of tends to infinity. The
positivity of and is the book's setting and is assumed where it appears.
The uniform inventory position of Proposition 5.1, which needs the book's assumption that not all demands are multiples of an integer larger than one, is taken as given in the cost formula (6.4), as the book does; the proposition itself is the subject of the next mission of this series. The definitions are reusable for the optimization of Sect. 6.1.1.2 and for the multi-echelon batch-ordering results of Sect. 10.5; contributions formalizing the Zheng-Federgruen algorithm on top of them are welcome.
Chapter 4 of Axsäter's Inventory Control fixes the batch quantity from a deterministic model, and Chapter 5 asks the question that deterministic models cannot answer: with demand random and a replenishment lead-time , when should the next batch be ordered? Under a continuous review policy the answer is a single number, the reorder point , and Sections 5.3 through 5.9 are one sustained computation of what a given buys. The chapter's own capstone is Eq. (5.67): if backorders are charged at per unit and time unit and stock at , the cost-minimizing reorder point is exactly the one whose fill rate is . The book calls the relationship "even more striking" than its discrete counterpart, and it is used in practice in both directions: a backorder cost prescribes a service level, and a chosen service level reveals the backorder cost a planner is implicitly assuming (Eq. 5.68).
An order for a fixed batch quantity is triggered whenever the inventory position (stock on hand plus outstanding orders minus backorders) falls to the reorder point , and it arrives time units later. Demand is continuous and normally distributed; the demand over a lead-time has mean and standard deviation . Two modelling facts from the book are taken as the definition of the steady state. First (Sect. 5.3.1), the inventory position is uniformly distributed on ; the book proves this for compound Poisson demand (Proposition 5.1) and adopts it as an accurate approximation for continuous demand. Second (Sect. 5.3.2, Eq. 5.35), the inventory level a lead-time later is the inventory position now minus the demand in between,
with the two terms independent. The law of is therefore the image of the product of a uniform and a normal law under subtraction, and everything in the chapter is a functional of it:
The closed forms run through the standard normal loss function of Eq. (5.40), published with the newsboy mission and reused here, and through its integral, the second loss function of Eq. (5.64). Both are tabulated in the book's Appendix 2, and both recur in Chapters 6, 9 and 10.
For and any , a reorder point minimizes over if and only if
The biconditional carries both halves of the book's sentence: the stationary point is the optimum ("the optimal is obtained for ") and the optimum is stationary ("in the optimal solution we have ").
In the order the chapter builds them: Eq. (5.41), , with decreasing and convex; Eq. (5.39), the distribution function by conditioning on the inventory position; Eq. (5.42), its closed form ; Eq. (5.43), the density; Eq. (5.52), the fill rate ; Eq. (5.55), the expected backorders covered by one batch, and Eq. (5.54), that is the same fill rate; integrability of the cost rate and the mean ; Eq. (5.63), ; Eq. (5.64), the closed form of and ; Eq. (5.65), the cost ; Eq. (5.66), ; and the convexity of in .
The result itself. The reorder point is the one parameter of an policy that stochastic demand actually decides, and Eq. (5.67) says that deciding it by cost and deciding it by service level are the same decision, with an explicit dictionary between the two. That is why the book can present service-level constraints (Sect. 5.7) and shortage costs (Sect. 5.9) as interchangeable ways of specifying the same thing, and why it warns, immediately after Eq. (5.67), that the equivalence is only valid when is given: with an ordering cost and a joint optimization of and it fails, which is Chapter 6's problem.
The intermediate formulas have independent standing. Eq. (5.42) is the single expression from which every service measure of the chapter is computed, and Eq. (5.65) is the cost function that Chapter 6 extends by an ordering cost, Eq. (6.10), and optimizes iteratively. The second loss function returns in the periodic-review fill rate of Eq. (5.86) and in the two-echelon batch-ordering model of Sect. 10.5.
Formalizing it. Nothing here is open; the value is that the steady-state model becomes an explicit measure, so that formulas the book obtains by manipulating integrals whose existence it never questions become theorems about that measure. Integrability of the cost rate is a target of its own for exactly that reason. None of the statements has a machine-checked proof yet.
The obvious route is the book's, and it is not the hard part: once is known in closed form, every later identity is calculus on and . The work is upstream of that. The distribution function (5.39) is a conditioning argument over the product measure, a Fubini step in which the inner probability is a Gaussian tail; the density (5.43) is a derivative of a parameter-dependent integral; and Eq. (5.63) exchanges the order of two integrals over an unbounded region, which needs integrability of itself. The derivative (5.66) is then obtained from the closed form (5.65), not by differentiating under an expectation, which is what makes the goal reachable: is a smooth function of with an explicitly increasing derivative, and Eq. (5.67) follows from strict convexity together with the fact that the fill rate is a continuous, strictly increasing function of ranging over . A solver who starts from the expectation and tries to differentiate it directly will meet the kink of at and a dominated-convergence argument; the integrated route avoids both.
The inventory position is rqPosition R Q, Lebesgue measure conditioned on ; the
lead-time demand is newsboyDemand m s, Mathlib's gaussianReal m (s^2).toNNReal from the
newsboy mission, with and ; and rqLevel R Q m s is the pushforward of
their product under . Two lemmas in the definition file record that both
are probability measures when . The distribution function, ready rate and cost are the
measure of , the measure of , and a Bochner integral against this law.
Every statement assumes and . At the conditioned measure is the zero measure and every integral is , so a statement without the hypothesis would be true and empty; at the demand is a point mass and has jumps. The mean is unrestricted, as none of the formulas depends on its sign, and reorder points may be negative, which the book explicitly allows in Sect. 5.8. Costs and are positive in every statement that involves them, and is stated for because its closed form holds there.
Two trivializing readings are ruled out. The cost is not defined as a formula in but as an expectation, so the closed form (5.65) has content; and because Lean's Bochner integral of a non-integrable function is , integrability of the cost rate is stated as a theorem rather than assumed, otherwise a zero cost would make every reorder point optimal. The goal quantifies optimality over all real competing reorder points, not a neighbourhood.
A complete development needs Gaussian tail integrals, differentiation of parameter-dependent integrals, Fubini on a product of a bounded interval with the line, and the strict monotonicity of the Gaussian distribution function. The loss functions and and the inventory-level law are reusable across the rest of the series; contributions that establish the same identities for an arbitrary continuous lead-time demand with a finite mean, where Eqs. (5.39), (5.63) and (5.66) hold verbatim, are welcome.
Exact methods for the resource-constrained project scheduling problem — branch-and-bound over activity lists or over start-time assignments, and the lower-bound computations inside them — live or die by how much of the search space can be discarded before it is enumerated. The standard tool is constraint propagation: deducing, from the precedence, resource and time-window data, new precedence relations that every feasible schedule must satisfy, and tighter time windows for the activities. Brucker and Knust's Section 3.6 (doi:10.1007/978-3-642-23929-8) presents the family of interval consistency tests — input, output, input-or-output and their negations — that constraint-programming schedulers apply at every node of the search, following Carlier and Pinson (An algorithm for solving the job-shop problem, Management Science 35, 1989, doi:10.1287/mnsc.35.2.164) and Baptiste, Le Pape and Nuijten (Constraint-Based Scheduling, Kluwer, 2001, doi:10.1007/978-1-4615-1479-4). Every test is an instance of one theorem, Theorem 3.7, and its cumulative-resource analogue, Theorem 3.8. Those two theorems, and the tests as their corollaries, are this mission.
The instance is the RCPSP of mission I: activities with integer processing times , renewable resources with capacities and demands , and precedence arcs; a schedule is an integer start-time vector , feasible when it meets the precedences and never exceeds a capacity. Section 3.6 adds three things.
Relations. A conjunction holds in when . Two activities are parallel, , when they overlap for at least one time unit, and a disjunction is the negation of that: or . The instance carries a set of conjunctions and a set of disjunctions that every feasible schedule must satisfy; initially is the precedence relation and the pairs whose combined demand exceeds some capacity, and propagation adds to them.
Disjunctive sets. A set of at least two activities is disjunctive when any two of its members are related by a disjunction or a conjunction, so no two are ever processed together: the activities of a unit-capacity resource, the jobs of a single machine, the operations of one job in a shop. Its total processing time is .
Time windows. Each activity has a head and a deadline , and a feasible schedule has and . An activity starts first in a set when no activity of starts earlier, and ends last when none completes later.
For a cumulative resource the work of activity is and .
Let be a disjunctive set, , and proper subsets of with . If
then in every feasible schedule an activity from starts first in or an activity from ends last in .
If some nonempty has , no feasible schedule exists.
For nonempty and : if then for all ; symmetrically, if then for all .
For , : if then starts first in or ends last in , and when .
For a cumulative resource , and proper subsets of : if then an activity from starts first in or an activity from ends last in .
Theorem 3.7 is the single statement behind a whole toolbox. Every interval consistency test in the literature — the input and output tests that fix a new conjunction, the input-or-output test, the negation tests that only shrink a window — is the theorem with a particular choice of and , and the book's Section 3.6.4 derives them one by one. A propagation engine that applies these tests to a fixpoint is what makes branch-and-bound for the job shop and the RCPSP practical; Carlier and Pinson's solution of the 10×10 job-shop instance is the historical demonstration. Theorem 3.8 extends the same reasoning from disjunctive to cumulative resources by replacing "no overlap" with "at most units per time unit", the energetic-reasoning viewpoint that the rest of Section 3.6.5 develops.
The results are elementary and proved; formalizing them fixes, once, what "feasible" means in the presence of the relation sets and and time windows, on top of the RCPSP model of mission I. That layer is reusable: the start-start distance matrix of Section 3.6.2 and the symmetric-triple rules of Section 3.6.3 are statements about the same schedules and the same relations. Nothing here is on the platform or in Mathlib.
The obvious argument for Theorem 3.7 is the correct one, and its difficulty is in the bookkeeping. If no activity of starts first and none of ends last, the first starter is some and the last finisher some , and every activity of is processed inside . Since the activities of a disjunctive set are pairwise non-overlapping, their total length fits in that interval, contradicting (3.121). The formal work is the packing lemma: pairwise disjoint integer intervals inside an interval of length have total length at most , which requires ordering the activities by start time and an induction that Mathlib does not supply.
The subtle point is the restriction in (3.121). The book allows it because "an activity which starts first cannot complete also last" when there are at least two activities with positive durations. The formal statement reads "starts first" and "ends last" with , which makes the theorem true without a positivity hypothesis: when the restriction empties the index set, , the conclusion holds because cannot be both the unique first starter and the unique last finisher of a disjunctive set with two or more members. A solver should expect to handle that corner separately.
For the tests the extra step is turning "starts first" into a conjunction , which uses the disjunction between and together with positive processing times: with an activity could start at the same instant as without violating the disjunction, so the tests carry the positivity hypothesis that Theorem 3.7 itself does not need. Theorem 3.8 replaces the packing lemma by a work-counting lemma: over an interval of length a resource of capacity supplies at most units, and every activity of consumes of them.
Schedules are integer start-time vectors on Fin n, as in missions I and II, and a feasible
schedule of this mission is one that is FeasibleSchedule for the RCPSP instance (mission I),
respects the arcs of (RespectsArcs, mission II), satisfies the disjunctions of and lies
within the time windows; these four hypotheses are the book's "feasible schedule" in Section 3.6
and are carried on every statement, although the arguments use only the last two, or, for
Theorem 3.8, the resource constraint and the windows. The sets and are parameters, not
derived from the instance, since propagation enlarges them.
Every inequality "" is stated as the family of inequalities over the same index pairs. This is equivalent, avoids natural-number subtraction, and gives an empty index set the value the convention would: the hypothesis is then vacuous. "Starts first" and "ends last" use . Proper-subset hypotheses , are the book's; the first infeasibility test needs nonempty, and the input-or-output test needs .
A trivializing reading is ruled out on the disjunctive side by the nonemptiness hypotheses (an empty would make the infeasibility test's family vacuous and its conclusion false) and on the cumulative side by the observation that Theorem 3.8 with asserts infeasibility, which is the book's intended reading. Welcome contributions beyond the milestones: the input-negation and output-negation tests, the window-tightening rules of Section 3.6.4, and the SSD-matrix results of Section 3.6.2.
When several processors share a workload, the first question is how long the workload takes if it is spread out as well as possible. If a job may be interrupted and resumed later, possibly on another processor — preemption, the setting of operating systems, of communication links and of any resource that can be time-shared — the answer is a closed formula, and it is one of the oldest results in scheduling: McNaughton's wrap-around rule of 1959 (Scheduling with deadlines and loss functions, Management Science 6, doi:10.1287/mnsc.6.1.1) shows that on identical machines the optimal makespan is the larger of the longest job and the average load. Horvath, Lam and Sethi (A level algorithm for preemptive scheduling, Journal of the ACM 24, 1977, doi:10.1145/321992.321995) extended this to machines of different speeds, and Gonzalez and Sahni (Preemptive scheduling of uniform processor systems, Journal of the ACM 25, 1978, doi:10.1145/322047.322055) gave the fast algorithm with few preemptions. Brucker's Chapter 5 (doi:10.1007/978-3-540-69516-5) presents the level-algorithm version, and this mission formalizes the statements it proves about schedules.
There are jobs with processing requirements and uniform machines with speeds : running job on machine for a period of length performs units of its requirement, so the whole job would take time units there. Identical machines are the case .
A preemptive schedule is a finite list of pieces, each a job, a machine, a start time and a stop time. It is feasible for the data when every piece lies in , no two pieces on the same machine overlap, no two pieces of the same job overlap (a job is on at most one machine at any instant), and every job receives total work exactly over its pieces. Its makespan is the largest stop time; the completion time of job is the largest stop time of one of its pieces. A schedule is nonpreemptive when every job consists of a single piece.
Following Section 5.1.2 the data are sorted, and , with , and one writes , . For a set of jobs, if and otherwise: the largest combined speed that jobs can use at one instant.
The optimal makespan of is the bound (5.5):
in the sense that some feasible preemptive schedule has makespan exactly and no feasible preemptive schedule has a smaller makespan.
Every feasible preemptive schedule has makespan at least .
On identical machines, is a lower bound on the makespan and is attained by some feasible preemptive schedule.
The jobs can be scheduled preemptively within if and only if for every set of jobs.
For with nonnegative weights there is an optimal schedule without preemption.
Theorem 5.8 turns an optimization over an infinite family of schedules into a formula in the data, and the formula is tight in both directions: each of its terms is a resource bound that some schedule meets exactly. That is what makes preemptive makespan minimization one of the few parallel-machine problems that is solvable at all — its nonpreemptive counterpart is NP-hard (p. 124) — and it is why the preemptive relaxation appears as a bound inside branch-and-bound methods for the nonpreemptive problems.
Condition (5.8) is the form in which the result is reused. It is a Hall-type condition, one inequality per set of jobs, and it is exactly what Section 5.1.2 needs to prove Theorem 5.9, which decides by a maximum flow in an expanded network. Theorem 5.7 is the complementary statement for the other classical objective: for total weighted completion time preemption buys nothing, so the nonpreemptive solutions of Section 5.1.1 are optimal in the larger class too.
On status: every statement here is classical and proved, and the formalization adds a checked
model of preemptive schedules. Mathlib has no scheduling material, and the platform's
SchedulingAlgorithms series so far models only single-machine sequences (missions I, II, IV)
and two-machine permutation flow shops (mission III), none of which allow a job to be split. The
piece-list model of this mission is the first reusable object for preemptive and parallel-machine
problems, and the later sections of Chapter 5 — , — are stated in it.
The obvious first idea for the goal is to run McNaughton's rule with the speeds ignored. It fails on uniform machines: filling machines one after another does not respect the constraint that a long job on a slow machine is not done when a short job on a fast one is. The correct idea is the level algorithm — always process the jobs of highest remaining requirement on the fastest free machines, sharing machines among tied jobs — and the difficulty is in the analysis rather than the idea. The proof of Theorem 5.8 has to show that the schedule it produces ends exactly at one of the terms of : either no machine idles before the end, giving , or the machines finish in speed order with the first jobs busy from time , giving . Making that case analysis rigorous requires tracking that the order of remaining requirements is preserved over time (the invariant (5.6)) and that ties are broken consistently.
A second, formal difficulty is that the level algorithm's output is defined by continuous-time events (the next completion, the next time two levels coincide), so producing an explicit finite list of pieces with the required properties is itself a construction. Any proof must build a concrete schedule; "the infimum of makespans equals " is not the goal.
For the lower bound the trap is the opposite: it is tempting to argue only with total capacity , which gives but not . The latter needs the rule that a job is on at most one machine at a time, so that jobs run at combined speed at most ; a model that let a job be split across machines simultaneously would make the theorem false, and the definition of feasibility rules it out explicitly.
A schedule is a List of Pieces over jobs Fin n and machines Fin m, with real start and
stop times. Feasibility is the three-part condition of the Setting, disjointness of two pieces
meaning one stops no later than the other starts. Work is measured with the machine's speed, so
the same definitions cover identical machines as the constant speed . Pieces of length zero
and unsorted lists are allowed; both are harmless.
The sorted orders are hypotheses Antitone p and Antitone s, the speeds and requirements are
positive, and, where the book assumes it, . The book's normalization is
not assumed: every statement here is invariant under scaling all speeds, and the book uses the
normalization only for a running-time estimate. The bound is defined as the maximum of an
explicit nonempty finite set, so no supremum of an empty or unbounded set occurs; takes a
proof that so that is meaningful.
Two things are deliberately not stated. The level algorithm itself is not transcribed: Theorem 5.8 is stated as the existence of an optimal schedule of makespan , which is what its proof establishes. And Theorem 5.9, the flow characterization for , is left for a later mission, since it needs release times and the expanded network on top of this model.
A trivializing reading is excluded by the existential form of the goal and of Theorem 5.7: each asserts that an optimal schedule exists, not merely that any optimal schedule has a property. A proof of the goal has to construct a schedule; a proof of Theorem 5.7 has to construct a nonpreemptive one that beats every preemptive competitor. Contributions welcome beyond the milestones: a general lemma that a feasible schedule can be normalized to sorted, positive-length pieces, and a proof that (5.8) for the sets is equivalent to .
Cryptography before 1949 was a catalogue of ciphers and of the tricks that broke them. C. E. Shannon's Communication Theory of Secrecy Systems (Bell System Technical Journal 28(4):656–715, 1949) replaced the catalogue with a probabilistic model: a cipher is a family of invertible maps from messages to cryptograms, indexed by a key drawn from a known distribution, and the cryptanalyst's state of knowledge after an interception is the a posteriori distribution over messages. Part II of that paper asks when interception conveys nothing at all. The answer — perfect secrecy — is the origin of the one-time pad's security proof and of the modern habit of defining security as the indistinguishability of a posteriori from a priori beliefs.
This mission formalizes §10, Perfect Secrecy: the definition, the necessary and sufficient condition (Shannon's Theorem 6), the counting bound that the key set be at least as large as the message set, the cyclic system that attains the bound, the Latin-square description of the systems that attain it, and the entropy form of the constraint.
A finite secrecy system consists of three finite sets — the messages , the keys , the cryptograms — together with an enciphering map for each key . Each is non-singular, i.e. injective, so a receiver who knows the key deciphers unambiguously. The key is drawn from an a priori distribution , , and the message from an a priori distribution , , independently of the key.
Three derived quantities carry the theory. The key weight
is the probability that the cryptogram is given that the message is . The cryptogram probability is , the probability of obtaining from any cause. The a posteriori probability of the message after interception is , defined for cryptograms with .
A system has perfect secrecy when, for every a priori message distribution and every cryptogram that can occur, for all : interception leaves the cryptanalyst's probabilities unchanged. Quantifying over all a priori message distributions is Shannon's requirement that the equality hold "independently of the values of ".
Finally, and are the entropies of the message and key choices.
Equivalently, does not depend on : the total probability of the keys carrying to a given is the same as that of the keys carrying to the same . The goal fixes nothing about the sizes of the three sets, and no structure on the key distribution beyond normalization.
Theorem 6 is the structural fact behind every later statement in the section: the counting bound, the Latin-square description, and the entropy constraint are all read off from the independence of from . The counting bound and the entropy constraint are the precise sense in which unconditional secrecy is expensive — the key must be at least as uncertain as the message — and they are the reason practical cryptography moved to computational assumptions. The cyclic system supplies the matching construction, so the bound is sharp.
These results are classical and have textbook proofs; what this mission produces is a machine-checked development of them from a single explicit model of a finite secrecy system, including the model itself. Mathlib has extensive measure-theoretic probability and some information theory, but no formalization of Shannon's secrecy systems, of perfect secrecy, or of the results of §10. The shared definition layer — ciphers with injective enciphering maps, key weights, a posteriori probabilities, the perfect-secrecy predicate, finite entropy — is reusable for the rest of the paper: the equivocation results of §11–§13, unicity distance, and the ideal-system theorems of §16 all rest on the same objects.
The two directions of Theorem 6 are not symmetric. Sufficiency is a computation. Necessity has to extract, from a statement about a posteriori probabilities that only constrains cryptograms of positive probability and only for one distribution at a time, a statement about key weights alone; the useful instantiation is a distribution giving every message positive mass, and the cryptograms of probability zero must be handled separately rather than ignored.
The counting and Latin-square milestones are finite combinatorics, but the obvious argument — "for each message and cryptogram pick the key joining them" — needs the keys picked to have positive probability, and the model permits keys of probability zero; this is exactly where an argument that looks complete on paper leaves a gap in Lean. The entropy milestone is the hardest of the five: passes through the conditional entropies , and Mathlib's information-theoretic API is stated for measures rather than for finite weighted sums, so either a bridge or a self-contained development of finite conditional entropy is required.
Messages, keys and cryptograms are arbitrary finite types with decidable equality on cryptograms; probabilities are real-valued functions with explicit non-negativity and normalization hypotheses rather than PMF, so that all sums are finite sums. A cipher bundles the enciphering maps, their injectivity, and the key distribution. The a posteriori probability is a real quotient, so it evaluates to zero when the cryptogram has probability zero; every statement that mentions it carries the hypothesis that the cryptogram has positive probability. Entropy uses the natural logarithm, with vanishing at ; all inequalities are therefore in nats and are unaffected by the choice of base.
One trivializing formalization is ruled out explicitly: perfect secrecy is quantified over all a priori message distributions, not over one fixed distribution, and it is not vacuous — the cyclic milestone exhibits a family of ciphers satisfying it for every .
Contributions welcome beyond the milestones: finite conditional entropy and its chain rule as reusable lemmas, the equivalence of the present perfect-secrecy predicate with the statistical-independence formulation of message and cryptogram, and the extension of the model towards §11's equivocation , which is the next result of the paper to formalize.
Lagrangian mechanics is the standard reformulation of Newtonian dynamics used throughout physics: a mechanical system is described not by forces but by a single scalar function, the Lagrangian, and the equations of motion are the stationarity conditions of an integral of that function along a path. The organizing result of the theory is Noether's theorem: every continuous symmetry of the Lagrangian produces a quantity that is constant along every solution of the equations of motion. Conservation of momentum, of angular momentum, and of energy all arise this way, and the same statement — in field-theoretic form — underlies conservation laws in electrodynamics, general relativity, and the Standard Model.
This mission formalizes the Lagrangian chapter of David Tong's Classical Dynamics (University of Cambridge, Part II Mathematical Tripos), Section 2, in Lean 4. The finite-dimensional statement it targets is the one a physics student meets first, and it is the statement on which the field-theoretic versions are modelled.
The configuration space is ; a path is a map , written , and its velocity is the coordinatewise time derivative . A Lagrangian is a function
smooth in all arguments; Tong writes it .
The action of a path over is
A path is a motion (it solves Lagrange's equations, Tong eq. 2.43) when
both partial derivatives being evaluated at . The quantity is the generalised momentum conjugate to (eq. 2.44), and
is the Hamiltonian (eq. 2.47). A function of time is a constant of the motion when it takes the same value at all times (eq. 2.46).
A one-parameter family of paths is a map , , whose member is the path under study. It is a continuous symmetry of (eq. 2.52) when
the dot denoting .
If is a continuous symmetry of and the path solves Lagrange's equations, then
takes the same value at every time .
Noether's theorem is the statement that converts a structural property of a system — invariance under translations, rotations, or time shifts — into a number that does not change during the evolution. It is what licenses the use of conserved quantities as first integrals when solving mechanical problems, and it is the finite-dimensional prototype of the conservation laws that classify symmetries in field theory.
Formalizing it produces a small but reusable Lean development: a definition layer for
Lagrangians and their partial derivatives on , Lagrange's equations as a
predicate on paths, the action functional, and the notion of a constant of the motion.
Mathlib currently has the calculus these statements need — deriv, fderiv,
ContDiff, interval integrals and differentiation under the integral sign — but no
Lagrangian-mechanics layer built on top of it, so the definition layer of this mission
is itself a contribution. The results here are classical and completely proved in the
mathematical literature; what is missing is machine-checked proofs.
The physics derivations are three lines each, and all three lines are the ones that Lean does not grant for free. Tong's proof of Noether's theorem differentiates with respect to by the chain rule, exchanges with on , and then substitutes Lagrange's equations; in Lean, each of these steps requires the corresponding differentiability side conditions to be produced from the smoothness hypotheses, and the exchange of the two partial derivatives requires a symmetry-of-second-derivatives argument. The principle-of-least-action target additionally needs differentiation under the integral sign and the fundamental lemma of the calculus of variations (a continuous function integrating to zero against every smooth bump supported in vanishes there), neither of which is available in the exact shape needed.
The naive route — defining everything through fderiv on the product space and hoping
simp unfolds the chain rule — does not close these goals, because the partial
derivatives are taken in single coordinate slots and must be reassembled into a total
derivative along the path.
Conventions fixed by the Lean development and worth knowing before starting:
Fin n → ℝ for a fixed n : ℕ, and time is all of ℝ;
no interval restriction is imposed except in the action functional.derivs taken in a single slot, using
Function.update to vary one coordinate. Where a derivative fails to exist, deriv
returns 0; the smoothness hypotheses on L, on paths, and on families are stated
so that this junk value is never the content of a statement.HasDerivAt, so they assert the existence of
d/dt (∂L/∂q̇ᵢ) as well as its value.∀ t₁ t₂, F t₁ = F t₂, i.e. constancy on all of ℝ,
not merely a vanishing derivative.s-derivative vanishes for all s and t,
not only at s = 0.n = 0 is included in every statement; there it is trivially
true. It is not, however, a trivializing formalization of any target: for n ≥ 1 the
hypotheses are satisfied by standard systems (a free particle, a particle in a central
potential), so none of the statements is vacuous.Contributions welcome: proofs of any supporting target, reusable lemmas relating the
coordinate-slot derivs used here to fderiv on the product space, and worked
instances (translation invariance giving momentum conservation, rotational invariance
giving angular momentum) built on the same definition layer.
Periodic signals are the basic objects of audio processing, electrical engineering and the analytic study of partial differential equations, and the standard first-course tool for handling them is the Fourier series: a decomposition of a -periodic signal into sinusoids of frequencies . The identity that makes the decomposition quantitatively useful is Parseval's theorem: the average power of the signal equals the sum of the squared moduli of its Fourier coefficients, so energy can be accounted for frequency by frequency.
This mission formalizes the chain of results leading to that identity exactly as it is presented in the open-access undergraduate textbook Análise de Fourier — Um Livro Colaborativo (Esequia Sauter and Fabio Souto de Azevedo, orgs., UFRGS/REAMAT, 2022): the orthogonality relations of the trigonometric system (Teorema 3.2.1), the coefficient formulas (Teorema 3.2.2), the passage to the exponential form (§4.2), and the Parseval identity itself (Teorema 5.1.1).
Fix a period and write
For a real-valued integrable on the book defines the trigonometric Fourier coefficients (eq. 3.23)
and for a complex-valued the exponential coefficients (§4.2, eq. 4.8)
which for real satisfy . The average power of a -periodic signal is (Definição 5.1.1)
A trigonometric polynomial of degree (Definição 3.2.1) is
For and continuous and -periodic,
The book states the identity for a periodic function "representable by a Fourier series"; the mission fixes continuity as the concrete sufficient regularity hypothesis, which keeps the statement non-vacuous and true, and leaves the sum as an unordered sum over so that no summation order is smuggled in.
Parseval's identity converts an integral estimate into a coefficientwise one: it is the bridge between the time domain and the frequency domain, underlies the RMS computations of the book's own electrical-engineering examples (Exemplo 5.1.2), and yields closed-form evaluations of numerical series (the book's Exemplo 5.1.3 computes a series of reciprocal odd squares this way).
Mathlib already contains the abstract Hilbert-space form of the identity for the Fourier
basis on the circle AddCircle T. What this mission adds is the concrete, classroom-level
layer that an engineering or physics reader recognizes: coefficients written as interval
integrals of a function on with an explicit period , the real
form, the exponential form and the dictionary between them, and the orthogonality
relations as free-standing computations. That layer is reusable by any later mission in
this series (transformada de Fourier, equação do calor, equação da onda).
The obvious route — expand , substitute the Fourier series, and integrate term by term — is exactly the book's proof, and it is the step that a formal development cannot take for granted: interchanging the integral with an infinite sum requires a convergence theorem that the book explicitly places outside its scope (the remark after Definição 3.2.3), and pointwise convergence of the Fourier series of a merely continuous function is false in general. A complete proof must run through convergence rather than pointwise convergence, so the central task is to connect the interval-integral coefficients on with the Hilbert-space machinery for the circle, including the change of variables and the normalization of Haar measure.
The development commits to the following conventions, all fixed in the definition bundle so that every statement shares them:
The goal is not trivializable: the hypotheses (a positive period, a continuous periodic function) are satisfiable, and both sides of the identity are non-degenerate already for .
Useful infrastructure beyond the mission: the dictionary between the interval-integral
coefficients on and Mathlib's fourierCoeff on AddCircle T, and the
orthogonality relations as standalone integral computations.
The discrete Fourier transform (DFT) is the basic spectral tool of digital signal processing, numerical analysis and computational number theory: it turns a finite sample of a signal into its frequency content, converts convolution into pointwise multiplication, and underlies fast integer and polynomial multiplication. Computed straight from its defining sum, a transform of length costs arithmetic operations. The fast Fourier transform (FFT) is any method that computes the same values in operations, and the radix-2 Cooley–Tukey algorithm is the most widely used of them.
The history is long and worth stating precisely. Gauss used an equivalent divide-and-conquer scheme in unpublished work of 1805 on the orbits of Pallas and Juno, without any complexity analysis. Danielson and Lanczos (1942) published the doubling step — the even/odd splitting identity that the recursion rests on — for x-ray crystallography. Good (1958) gave the prime-factor algorithm for coprime factorizations. Cooley and Tukey (1965) published the general composite-size algorithm together with the analysis that made the method famous. What is not known is a matching lower bound: whether a DFT of length can be computed in arithmetic operations is open.
Fix a length and a sequence of complex samples , modelled as a function . The DFT of length evaluated at frequency index is
and the inverse transform of a spectrum is
Only the first samples enter the sum; the frequency index is an arbitrary natural number, and the transform is -periodic in it.
The radix-2 Cooley–Tukey algorithm is the recursion on the exponent , with :
where is the transform of the even-indexed subsequence and that of the odd-indexed one. The factor is the twiddle factor of the merge stage.
The arithmetic cost of that recursion is modelled by two counters. At the merge stage of a transform of points there are butterflies; each butterfly performs one twiddle-factor multiplication and two complex additions, and the two recursive calls are on points each:
The goal fixes no operation count and no rate: it asserts only that the recursion computes exactly the transform it is supposed to compute, at every frequency index, for every input. That is the statement an implementation's correctness rests on, and it stays true whatever the cost analysis of the algorithm turns out to be.
The milestones are the intermediate statements the source separates out: -periodicity of the transform in the frequency index; the Danielson–Lanczos even/odd splitting
Fourier inversion for ; the conjugate symmetry of the spectrum of a real input; and the closed forms and of the two cost recursions, with .
Fourier inversion and the splitting identity are the two facts that make the transform usable at all: the first says no information is lost, the second is the single algebraic step from which every Cooley–Tukey variant — mixed radix, split radix, iterative bit-reversed implementations — is assembled. The operation counts are what justify the claim that the algorithm is rather than : for they are the difference between roughly and roughly complex multiplications.
None of this is open mathematics; all of it is classical. What this mission produces is a self-contained machine-checked development of the radix-2 algorithm against an explicit definition of the DFT: a recursive algorithm, a proof that it agrees with the defining sum at every index, and a proof of its arithmetic cost. Mathlib carries Fourier theory for characters of finite abelian groups and for , but the mission is stated against the elementary sum above so that the statements can be read, and audited, without that background.
The obvious induction on does not close by itself. Unfolding the recursion gives the even and odd sub-transforms evaluated at the reduced index , while the splitting identity produces them at . Closing the gap needs periodicity of the length- transform in its frequency index — which is why periodicity is a milestone rather than a step inside the main proof. The second recurring obstacle is bookkeeping with the exponential: and are the only analytic inputs, but they must be applied under a finite sum with natural-number casts, where -subtraction and division by a cast that may be zero are easy to get wrong.
Sequences are total functions , not vectors of a fixed length: the length appears only as the range of the defining sum, so the transform of length ignores for . The frequency index ranges over all of , and the goal is asserted for every such index, not only for — the periodicity of both sides makes this the stronger, and cleaner, statement.
Degenerate inputs are inside the statements, not excluded by hypothesis. The length- transform is the empty sum ; division by the cast follows Lean's convention , which is why inversion carries the hypothesis and the splitting identity carries . The real-input symmetry is stated for , with -subtraction in .
There is no trivializing reading: the FFT recursion is defined without ever mentioning the DFT, the cost counters are defined by their own recursions, and every hypothesis in the list above is satisfiable.
A complete development needs: the geometric-sum evaluation of for an -th root of unity (for inversion), the even/odd reindexing of a sum over , and the periodicity computations above. All of these are reusable beyond this mission; the splitting identity in particular is the entry point for a mixed-radix or split-radix sequel.
The NRL Plasma Formulary is a standard desk reference of the plasma-physics community: a compilation of the formulas, constants and unit conversions used in daily practice. Its opening section, "Numerical and Algebraic" (p. 3 of the 2013 edition), collects the few purely mathematical identities the rest of the handbook leans on. Two of them are exact summation formulas rather than approximations, and the first is the Rothe–Hagen identity, quoted there as valid "for all complex , , except when singular" and attributed to H. W. Gould's work on binomial coefficient summations.
Unlike the handbook's numerical entries, this identity is a theorem with a precise hypothesis set, and it is exactly the kind of entry a reader takes on trust. It generalizes the Vandermonde convolution, it is the coefficient identity underlying the generalized binomial series, and it specializes to Abel's binomial theorem. Formalizing it turns one line of a reference handbook into a machine-checked statement and produces, as a by-product, a reusable Lean development of binomial coefficients with an arbitrary complex upper index.
For a complex number and a natural number , the generalized binomial coefficient is the falling factorial divided by a factorial,
with the empty-product convention . It is a polynomial in of degree , and it agrees with the usual binomial coefficient when is a natural number.
Fix complex parameters , , and, for , consider the Rothe factor
which is defined whenever . The factor in the denominator cancels against the leading factor of the falling factorial, so extends to a polynomial in and : and, for ,
Both forms occur in the literature; the mission carries both and asks for the comparison between them, because the quotient form is the one printed in the handbook while the polynomial form is the one that carries no side condition.
For complex and , provided and for every , and ,
This is the handbook's line, with its "except when singular" proviso made explicit as the three non-vanishing hypotheses.
in terms of the polynomial form above. This version holds for all complex , with no exceptional locus, and implies the printed form wherever the latter's denominators are non-zero.
The first is Pascal's rule for a complex upper index; the second is the Vandermonde convolution over , which is the case of the goal.
The identity is the convolution law of the generalized binomial series: the formal power series solving satisfies , so the goal is the statement read off coefficientwise (Graham–Knuth–Patashnik, Concrete Mathematics, §5.4). Consequences include Abel's binomial theorem, the Lagrange-inversion count of -ary trees, and ballot-type identities in lattice-path enumeration.
Mathlib provides the Vandermonde convolution for natural-number arguments (Nat.add_choose_eq), the ascending and descending Pochhammer polynomials, and Ring.choose for binomial rings; it does not contain the Rothe–Hagen identity in any form. The four statements of this mission are therefore new formal content, and the complex-upper-index binomial API they force is reusable well beyond the mission.
The identity is classical and has been proved many times since Rothe (1793) and Hagen (1891), with the modern treatment in Gould's papers; nothing here is open mathematics. What is missing is a machine-checked proof.
The obvious attack — induction on using Pascal's rule — does not close as stated: the summand is not Pascal-stable, since shifting by moves for every at once, and the induction hypothesis is about a different family. The standard proofs instead treat both sides as polynomials in and for fixed and , verify the identity on an infinite set of points where a combinatorial reading is available, and conclude by the identity theorem for polynomials; or they extract coefficients from the generalized binomial series via Lagrange inversion. Either route needs infrastructure: a two-variable polynomial-identity argument over , or a formal-power-series compositional inverse.
A second, more prosaic difficulty is the singular locus. The printed identity divides by for every , and in Lean division by zero returns zero rather than failing, so a formalization that drops the non-vanishing hypotheses states a different — and in general false — claim.
All statements are over . The generalized binomial coefficient is defined as an explicit product over Finset.range k divided by (k ! : ℂ), so holds definitionally and no Nat.choose coercion enters. Sums run over Finset.range (n+1), with the complementary index written as the truncated natural subtraction n - k; inside that range this is the ordinary , so the truncation convention is never exercised.
The proviso "except when singular" is formalized as three explicit hypotheses — for all , for all , and — rather than by relying on Lean's junk value for division by zero. These hypotheses are satisfiable (for instance , ), so the goal is not vacuous, and they constrain only denominators, so they do not trivialize the sum.
The singularity-free milestone commits to a total function rotheA defined by cases on , with value at ; the comparison milestone pins that function to the quotient form under the non-vanishing hypothesis, so the mission cannot be satisfied by proving facts about a differently normalized object.
Contributions welcome beyond the milestones: complex-upper-index binomial API (symmetry, negation , polynomiality in the upper index), and any formal-power-series development supporting Lagrange inversion.
This mission formalizes the group theory of J. A. Wolf's Growth of finitely generated solvable groups and curvature of Riemannian manifolds, J. Differential Geometry 2 (1968) 421–446 (doi:10.4310/jdg/1214428658), namely its §3 and §4. Wolf opens with the object of study: "If a group is generated by a finite subset , then one has the 'growth function' , where is the number of distinct elements of expressible as words of length on " (p. 421). Section 3 proves that a group with a finitely generated nilpotent subgroup of finite index "is of polynomial growth, and in fact "; section 4 proves that "a polycyclic group, either has a finitely generated nilpotent subgroup of finite index and thus is of polynomial growth, or has no such subgroup and is of exponential growth" (p. 421).
Applying Milnor's companion note, which is the complete mission Milnor: growth of finitely generated solvable groups on this platform, Wolf concludes "that a finitely generated solvable group, either is polycyclic and has a nilpotent subgroup of finite index and is thus of polynomial growth, or has no nilpotent subgroup of finite index and is of exponential growth" (p. 421). That is the Milnor–Wolf theorem, the goal here, and Wolf's Theorem 4.8. It prompted the question Wolf asks on p. 422, "whether every finitely generated group , which is not of exponential growth, necessarily has a nilpotent subgroup of finite index"; Grigorchuk's groups of intermediate growth (1984) answered it in the negative, and Gromov (1981) proved that polynomial growth alone does force a nilpotent subgroup of finite index.
Growth. For a finite subset of a group , the growth function counts
the elements expressible as words of length on , a word
having length (p. 426). The published MilnorWolf.growthFunction S m takes
this as the size of the ball Chou.wordBall S m, the set of products of at most factors from
. Wolf's two kinds of bound (p. 421) are polynomial growth of degree ,
, and exponential growth, with ; the
published predicates are MilnorWolf.HasPolynomialGrowthOfDegreeLE and
Chou.HasExponentialGrowth, the latter with , which is what Theorem 4.3 actually produces.
Both quantify over some finite generating set, and Wolf shows (p. 427, p. 434) that neither depends
on which one.
Growth exponents. For a finitely generated nilpotent with lower central series
, each factor
is finitely generated abelian with free part of rank ; Wolf's (3.3)
sets and . These are
MilnorWolf.growthExponentOne and MilnorWolf.growthExponentTwo.
Polycyclic groups. A solvable group is polycyclic if it satisfies condition (1) of
Proposition 4.1: "There is a normal series
with every quotient
finite or infinite cyclic" (p. 433), where a normal series, as in Kurosh, has each term normal in
the preceding one. This is MilnorWolf.IsPolycyclic. Solvable is Mathlib's
Group.IsSolvable.
The goal is Wolf's Theorem 4.8 (p. 438): "Let be a finitely generated solvable group. If has a nilpotent subgroup of finite index, then is polycyclic and of polynomial growth of degree . If does not have a nilpotent subgroup of finite index, then is of exponential growth."
The milestones are the results it rests on, in the paper's order. Section 3 climbs from two rescaling lemmas (3.4, 3.5) and the growth function of a free abelian group (3.6) through generating sets adapted to the lower central series (3.7) to the polynomial bounds for a finitely generated nilpotent group (3.2), then passes them to a group with a finite-index subgroup (3.11). Section 4 characterises polycyclic groups (4.1, whose one hard input is Hirsch's theorem, a milestone of its own) and proves the polycyclic dichotomy (4.3). Milnor's Theorem, already proved on this platform, appears as a reference milestone: it is what carries 4.3 from polycyclic to solvable, and Wolf notes on p. 437 that "J. Milnor extended the scope of Theorem 4.3 by proving [10] that a finitely generated nonpolycyclic solvable group must be of exponential growth."
Theorem 4.8 is the first growth dichotomy: within finitely generated solvable groups there is nothing between polynomial and exponential, and the polynomial side is exactly the almost nilpotent one. It is the result Gromov's theorem generalises in one direction and Grigorchuk's groups bound in the other, and the reason a group of intermediate growth can be neither solvable nor elementary amenable, which is how those groups were first placed outside both classes. Chou's Theorem 3.2, in the mission Chou: elementary amenable groups, extends exactly this statement to elementary amenable groups and cites both halves.
Section 3 also has independent value. The polynomial bounds with the explicit exponents and from the lower central series are sharper than the usual textbook statement that a finitely generated nilpotent group has polynomial growth, and the pieces along the way are reusable: the growth function of in closed form, and the fact that polynomial growth of a given degree is inherited from a finite-index subgroup.
The hard milestone is the second half of Theorem 4.3, that a polycyclic group with no nilpotent subgroup of finite index has exponential growth. Wolf proves it through Proposition 4.4, which passes to a Malcev completion and reads the eigenvalues of the induced Lie algebra automorphisms; that machinery is not in Mathlib and is not part of this mission. A route that avoids it: a polycyclic group acts on a free abelian factor of its chain by integer matrices, so either some element has an eigenvalue off the unit circle, and then the separation argument of Wolf's p. 437 applies verbatim with that factor in place of the Lie algebra, or every eigenvalue of every element lies on the unit circle, and then Kronecker's theorem, which Mathlib has, makes them all roots of unity, so a finite-index subgroup acts unipotently and is nilpotent. Wolf records in the "Added in Proof" (p. 445) that "B. Hartley recently sent me a manuscript consisting of an alternate proof that a polycyclic group without nilpotent subgroups of finite index is of exponential growth."
Theorem 3.2 is long rather than deep: the lower bound (3.8) and the upper bound (3.9), (3.10) are two inductions along the lower central series, each carrying explicit word-length bookkeeping, and both need the adapted generating sets of Lemma 3.7, in the corrected form stated here: as printed, the lemma fails when a lower-central factor has torsion. Mathlib has no polycyclic groups, so Proposition 4.1 starts from nothing; it also lacks Hirsch's theorem and P. Hall's finite presentability results, which is why Hirsch is stated here as its own milestone rather than assumed.
No new definitions: every notion is taken from the published bundles Chou_Growth and
MilnorWolf_Growth, so the statements here are directly comparable with those of the Chou and
Milnor missions. Growth is measured on closed balls, Chou.wordBall S m being the products of at
most letters from and its cardinality, finite because is a
Finset. "Not of exponential growth" is the negation of an existential, so it is a statement about
every finite generating set.
Conditions (8) to (11) of Proposition 4.1, Proposition 4.4 and the Lie-theoretic apparatus of §4, and the Riemannian geometry of §2, §5 and §6, are outside this mission; Proposition 4.1 is stated here with its first seven conditions, which are the ones §4 uses. Hirsch's theorem is cited, not proved, by Wolf, and appears as a milestone under its own source (Proc. London Math. Soc. 44 (1938) 53–60) rather than as an omission. Cheeger's and Hartley's sharpenings, recorded in Wolf's "Added in Proof", are not included.
No hypothesis is vacuous: the free abelian groups witness Proposition 3.6 and Theorem 3.2, a polycyclic group with no nilpotent subgroup of finite index exists (the semidirect product for a hyperbolic , which is Wolf's own example of the exponential case), and the lamplighter group is finitely generated solvable and not polycyclic, so Theorem 4.8's second alternative is not empty either. Contributions welcome: proofs of any milestone, and the general library results they need, such as polycyclic groups and Hirsch's theorem.