Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A 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.
Density functional theory (DFT) is the computational method behind a large fraction of present-day electronic-structure calculations in condensed-matter physics, quantum chemistry and materials science. Its appeal is a drastic reduction in dimension: instead of an -electron wavefunction living on , one works with the one-particle density on . That reduction is not a modelling approximation; it is licensed by two theorems of Hohenberg and Kohn (1964), for which Walter Kohn shared the 1998 Nobel Prize in Chemistry. Every statement in this mission comes from the two Hohenberg–Kohn theorems and the identities the source text uses to set them up.
Timeline. The Thomas–Fermi model (1927) introduced density-only energy expressions but is known not to bind molecules (Teller, 1962). Hohenberg and Kohn (1964) proved that for non-degenerate ground states the external potential is fixed by the ground-state density, and that the exact energy functional is minimized at that density. Kohn and Sham (1965) turned this into a practical scheme by reproducing the density with non-interacting orbitals. Levy (1979) replaced the Hohenberg–Kohn functional, defined only on ground-state densities, by a constrained-search functional defined on all -representable densities.
Fix an electron number. The objects are:
Two functionals act on these. The universal part is the expectation value of the kinetic-energy and electron–electron-interaction operators, which do not depend on the system. The external part is the expectation value of the external potential, and the identity that makes DFT possible is that it depends on only through its density:
The total energy is . A state is a ground state of when it minimizes , and a nondegenerate ground state when it is the strict minimizer. A density is -representable when it is the density of a nondegenerate ground state of some potential.
with equality exactly when , the ground-state density of . Part (1) is the source's Corollary 1 — the density determines every ground-state property; part (2) is its Theorem 2.
The supporting statements are the density-determines-the-state half of Theorem 1, the potential-is-determined-up-to-a-constant half of Theorem 1, the well-definedness of the universal functional , the variational principle, the Levy constrained-search identity, the identity on , and the normalization of a Kohn–Sham density built from orthonormal orbitals.
The Hohenberg–Kohn theorems are what justifies computing with rather than : without Theorem 1 the density would not carry enough information to determine the system, and without Theorem 2 there would be no variational principle to minimize. They are also the reason the exchange–correlation functional is a well-posed object of study: it is the unknown part of a functional that the theorems guarantee exists.
Formalizing them contributes a reusable variational core — ground states, universal functionals, -representability, constrained search — plus two genuinely analytic statements about : the density-pairing identity for the external energy and the "a.e. nonvanishing eigenfunction forces the potential difference to be constant" lemma. The latter two are where the mathematical work lies, and both are stated here over the concrete configuration space , not in the abstract model.
The reductio that proves Theorem 1 is short, and it is short in Lean too. The difficulty of DFT as mathematics sits elsewhere, and this mission isolates it:
sInf has to be handled.The variational layer is stated over an abstract model carrying the data actually used by the Hohenberg–Kohn argument: wavefunctions, potentials, densities, a universal functional , a density map, and an external-energy pairing. No Hilbert-space structure is assumed there, because the argument uses none; what it uses is that does not depend on and that the external energy sees only through . The two analytic milestones are stated concretely instead, on over , with .
Conventions fixed in Lean: energies are real; "nondegenerate ground state" means strict
minimizer, so degenerate ground states are outside the scope of every statement that
mentions it, exactly as in the source's caveat that the original theorems hold for
non-degenerate ground states; -representability quantifies over nondegenerate ground
states only; the Hohenberg–Kohn functional takes the junk value off the
-representable set, so statements about it always carry the representability hypothesis;
the Levy functional is an sInf, which is on an empty fibre.
The statements are not trivially satisfiable: the model has no hypothesis forcing the wavefunction set to be empty or the ground states to be unique, part (1) of the goal quantifies over every real-valued observable, and part (2) asserts an equality case, not merely an inequality. Contributions of the two analytic milestones are the most valuable: they need marginal-density machinery over product spaces that is reusable for any many-body formalization.
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.
The Schrödinger equation is the equation of motion of non-relativistic quantum mechanics: it determines how the state of an isolated quantum system evolves in time. Its time-independent form is an eigenvalue equation whose eigenvalues are the energies the system can have. The single most elementary illustration that this eigenvalue problem forces energies to be discrete is the particle in a one-dimensional box, also called the infinite potential well: a particle of mass confined to an interval by walls of infinite potential energy. It is the first worked example in essentially every introduction to quantum mechanics, and it is the model in which "quantization" can be derived in a few lines from a boundary-value problem for an ordinary differential equation.
This mission is the first in a series formalizing the mathematical content of the Schrödinger equation. It targets exactly the particle-in-a-box computation: that the admissible energies are for positive integers , and nothing else.
Fix three positive real constants: the reduced Planck constant , the mass , and the width of the box. A stationary state of energy is a function such that
together with the regularity needed to state it — is continuous on and twice differentiable at every interior point — and the Dirichlet boundary conditions imposed by the infinite walls,
Inside the box the potential vanishes, which is why only the kinetic term appears; outside the box the potential is infinite and the wave function is identically zero, which is what forces the two boundary values. A stationary state is non-trivial if for at least one ; the trivial solution is excluded because a physical state must be normalizable to unit probability.
Write for , and for the corresponding unnormalized eigenfunction.
This is the weakest statement that carries the physical content: it fixes no eigenfunction, no normalization and no phase, only the set of admissible energies.
The last two give the converse direction — every really occurs — and the normalization constant that turns into a unit vector of .
The result itself is the standard textbook derivation: confinement plus the time-independent Schrödinger equation yields a discrete spectrum, with a strictly positive ground-state energy (no state of zero energy exists) and level spacing growing like . As a piece of mathematics it is the computation of the Dirichlet spectrum of the one-dimensional Laplacian on an interval, which is the model case for spectral theory on domains.
What the mission adds is a machine-checked version of both halves of that derivation, in a form that later missions in this series can import: a reusable predicate for "stationary state with Dirichlet boundary conditions", the classification of the solutions of with one boundary zero, and the quantization step. Mathlib contains the ordinary-differential-equation uniqueness results and the trigonometric API needed, but does not contain this boundary-value classification.
The physics derivation writes down the general solution and is done. Formally, that step is the whole problem: one must prove that every twice-differentiable solution of on an interval has this form, rather than assume it. The usual route is a uniqueness theorem for the associated first-order system applied to the difference of and an explicit sine solution, which requires converting the second-order scalar equation into a system and supplying a Lipschitz estimate. Two further traps: the sign case must be excluded separately (hyperbolic solutions with two zeros are identically zero), and the equation is assumed only on the open interval, so the values at the walls are reached by continuity rather than by evaluating the equation there.
Wave functions are complex-valued functions of a real variable, ; energies, , , are real. Derivatives are the ordinary derivative of a complex-valued function of a real variable, the second derivative being the derivative of the derivative. The equation is imposed pointwise on the open interval only, with continuity on the closed interval and differentiability at interior points; nothing is assumed about outside , so the junk values of the derivative outside the box never enter a statement. The constants are hypothesized strictly positive, so no division by zero occurs in .
The goal is not vacuous: the supporting target exhibiting shows that its hypotheses are satisfiable for every , so the mission cannot be closed by proving that no non-trivial stationary state exists. Conversely the non-triviality hypothesis cannot be dropped: solves the boundary value problem for every real .
Contributions welcome: the ODE classification lemma (solutions of on an interval), orthogonality of the in , and the finite-well and harmonic-oscillator analogues, which are planned as later missions in this series.
A nucleus whose proton number or neutron number equals one of — the magic numbers — is markedly more tightly bound than the semi-empirical mass formula predicts, and markedly more stable against decay. The empirical evidence for closed nuclear shells at and protons and at neutrons was assembled by Maria Goeppert Mayer in 1948 (Phys. Rev. 74, 235), and explained in 1949 by adding spin–orbit coupling to the shell picture (Phys. Rev. 75, 1969); the shell model that grew out of this work earned Goeppert Mayer and Hans Jensen a share of the 1963 Nobel Prize in Physics.
The textbook first step toward these numbers is purely combinatorial: approximate the nuclear force by an isotropic three-dimensional quantum harmonic oscillator, count the degenerate states at each energy level, double the count for spin, and accumulate. This mission formalizes exactly that step — including its well-known failure — from the Derivation section of the Wikipedia article Magic number (physics).
For the isotropic three-dimensional harmonic oscillator the energy depends only on the sum of the three quantum numbers, so the states at level are the triples of nonnegative integers summing to — the weak -compositions of . Write
Each state accommodates two nucleons of the same kind (two spin orientations), so the shell at level holds
nucleons, and filling every shell of level below takes
nucleons. A shell closure — hence a predicted magic number — is a value . Finally, denotes the seven most widely recognized magic numbers.
The mission's goal collects the content of the derivation:
together with the comparison against : the values lie in ; the magic number is never of the form ; and is produced by the count although .
The positive half of the statement explains three of the seven magic numbers from nothing but degeneracy counting: , and are exactly the first three oscillator shell closures. The negative half is the reason the shell model needs more physics: the oscillator count misses altogether and predicts , which is not magic. Historically this gap is what spin–orbit coupling was introduced to close, and it is the precise sense in which "the correct formula for predicted magic numbers fundamentally relies on spin-orbit coupling".
As a formalization target the mission is small and self-contained: it fixes a reusable Lean model of oscillator shell filling (levels, degeneracies, spin doubling, cumulative capacity) and the stars-and-bars count behind it, against which later, more physical refinements — spin–orbit corrections, the empirical magic-number list — can be stated.
The mathematics is elementary; the work is in the counting and in the negative claims. The degeneracy is stars and bars for three boxes, most directly obtained by fibering over the first coordinate and summing . Asserting that no gives is not a finite check: it needs the closed form together with monotonicity of to rule out every above the range where is computed, since .
Everything is over and finite. The level set is a Finset (ℕ × ℕ × ℕ) cut out of the box by the equation , so its elements are ordered triples: permutations of the same multiset are distinct states, as the physics requires. Spin enters only as the literal factor in , not as an extra coordinate. The cumulative count runs over levels , so and ; the -th predicted magic number is , not . Binomial coefficients are Nat.choose, and the closed forms are stated in the division-free shape to avoid truncated natural-number division. The set of magic numbers is a hard-coded Finset ℕ transcribing the seven numbers listed by the source — it is a datum, not a derived object, and no claim in this mission asserts anything about nuclear stability itself.
The statements about and are what keep the mission from being a pure identity check: quantifies over all , and is a membership fact about the transcribed list.
A convex combination expresses a point as a weighted average of other points. Such representations connect geometric sets with finite lists of coordinates and coefficients. A point in a convex hull may initially be described using many generators, even when the ambient space has small dimension. Carathéodory's theorem gives a bound depending only on that dimension. Grünbaum presents this result as a basic theorem of convexity in Convex Polytopes, §2.3, Theorem 5, printed page 15 (the supplied source PDF, page 33).
Fix a natural number . Real -space consists of vectors with real coordinates. Let be any subset of this space. A convex combination of points of is a finite sum of those points multiplied by nonnegative real coefficients, with the coefficients adding to one. The convex hull is the set of all such combinations; equivalently, it is the smallest convex set containing .
The generating set can be finite or infinite. It need not be closed, bounded, or convex. Membership of a point in its convex hull is the sole geometric assumption. The theorem concerns exact equality of vectors, so the representation is not an approximation or a limiting expression.
For every , find points and real numbers satisfying
This is the complete target of Theorem 2.3.5. The witnesses may depend on , , and . No single selection of points must work for every point of the hull. Repeated points are permitted, and some coefficients may be zero. Thus the fixed list of positions can express a combination that uses fewer distinct points.
The result gives a finite certificate for membership in a convex hull whose length is controlled by dimension rather than by the size of the generating set. In the plane it gives three positions, and in three-dimensional space it gives four. Infinite generating sets remain within the same statement: once a particular hull point is chosen, only finitely many generators are needed for its certificate.
The mission asks for a formal proof of this known mathematical result in its fixed-length formulation. Its content is the existence of points and normalized coefficients together. Supplying coefficients without ensuring that their points lie in , or supplying a finite representation without the dimension bound, would leave part of the target unestablished.
The definition of the convex hull guarantees a finite representation but does not directly fix its length at . The dimension bound must hold while preserving nonnegativity, normalization, membership in the original generating set, and exact equality with the selected point. None of these constraints can be replaced by a condition on nearby points or on the closure of .
The coordinate model is Fin d → ℝ. Both the point list and the coefficient list are indexed by Fin (d + 1), corresponding to the source indices from zero through . The convex hull, finite sums, and real scalar multiplication have their standard mathematical meanings. No additional geometric definition is needed.
Dimension zero has one position in the representation. If is empty, its convex hull is empty, so there is no hull point to represent. A singleton generating set and sets contained in a proper affine subspace are allowed. Neither strict positivity of the weights nor affine independence of the selected points is required. The target does not assert uniqueness of a representation.
Branko Grünbaum, Convex Polytopes, second edition, Springer, 2003, Chapter 2, §2.3, Theorem 5, printed page 15; supplied source.pdf, page 33.
A convex set contains the segment joining any two of its points. For a bounded closed convex set in finite-dimensional real space, extreme points describe the set through convex combinations. An extreme point cannot lie strictly between two distinct points of the set. Allowing unbounded sets introduces a second ingredient: directions in which one can move indefinitely while remaining in the set.
This mission concerns that second ingredient and its interaction with extreme points. A closed convex set is line-free if it contains no entire straight line. It may nevertheless contain rays and be unbounded. Its characteristic cone consists of directions v for which x + t v stays in the set whenever x belongs to the set and t is nonnegative. For a nonempty closed convex set, checking one basepoint gives the same cone as checking every basepoint. Thus the cone records the directions of recession without singling out an origin inside the set.
The goal is Grünbaum’s Theorem 2.5.6:
for every line-free, closed convex set K in real d-dimensional space. The plus sign denotes Minkowski addition: all sums of one point from each set. The equation says that every point of K is a recession vector plus a finite convex combination of extreme points. Conversely, each such sum belongs to K. There is no topological closure around the convex hull in this equation.
A ray illustrates the two ingredients. Its endpoint is its only extreme point, while its characteristic cone supplies every nonnegative displacement along the ray. A singleton has only itself as an extreme point and has zero characteristic cone. A whole straight line shows why the line-free hypothesis matters: it has no extreme points and cannot be recovered from their convex hull by this formula.
The ambient dimension is arbitrary and finite; the set need not be full-dimensional or polyhedral. The characteristic cone is defined using all basepoints, so its value on the empty set is the whole ambient space. Since the empty set has no extreme points, its convex hull and the displayed Minkowski sum are empty, and the equation remains valid. This convention extends the formula without asserting that the book defines a characteristic cone at an absent basepoint.
The source is Branko Grünbaum, Convex Polytopes, second edition (2003), §2.5, Theorem 6, printed page 25 (PDF page 43). The characteristic cone and line-free condition appear on printed page 24 (PDF page 42); extreme points are defined in §2.4 on printed page 17 (PDF page 35). These definitions supply the vocabulary for the single representation goal.
A quantum computer manipulates superpositions of many degrees of freedom, and every gate it applies is imperfect. Before 1996 it was widely argued that this fragility is fatal: the accuracy demanded of each elementary operation appeared to grow with the length of the computation, so that arbitrarily long computations would require arbitrarily perfect hardware. The discovery of quantum error-correcting codes, of fault tolerant syndrome extraction, and of transversally encoded operations changed that picture, but the first fault tolerant schemes still required the error per operation to shrink as the computation grew.
Knill, Laflamme and Zurek, Resilient Quantum Computation: Error Models and Thresholds (arXiv:quant-ph/9702058), together with the independent work of Kitaev and of Aharonov and Ben-Or, removed that requirement: they exhibited a fixed threshold value such that any physical error rate below it permits arbitrarily accurate encoded computation, at an overhead that is only polylogarithmic in the length of the computation. Their paper is also the one that pushes past independent stochastic noise: its thresholds are proved for quasi-independent error models, which accommodate coherent over-rotation and weak residual couplings between neighbouring qubits.
This mission formalizes the quantitative engine of that paper: the concatenation recursion, the error-model bounds it is applied to, the threshold it produces, and the resulting overhead.
Fix a physical implementation in which each gate, state preparation and idle memory step carries an error location. A noisy network with error locations indexed by a finite set is described through an error expansion; each summand fails at a set of locations, and the model constrains how probable simultaneous failures are.
Write for the underlying probability measure and for the event that location has failed. Two models from Section I.B of the paper are used here.
The fault tolerant construction of Section I turns physical qubits into encoded qubits: each encoded gate is a transversal operation preceded by fault tolerant recovery networks built from the -qubit Steane code. The analysis of Section II declares an encoded gate failed according to an explicit combinatorial rule, and shows that a failure requires two failures among a set of minimal pairs of physical error locations. Consequently one level of encoding maps a failure parameter to .
Iterating this reduction is concatenation. Define the level- failure parameter by
written in the Lean development. Let bound the number of qubits and time steps at the level below that are consumed by one encoded gate, so that one computational gate at level costs physical resources.
For , , , and every gate count and target failure probability with , there exists a level with
The first clause is resilience: a computation of encoded gates can be made to fail with probability below any prescribed . The second is the cost: the overhead per computational gate is polylogarithmic in , with exponent . The threshold itself is the hypothesis ; no numerical value is hard-coded, so the statement survives any improvement of the paper's count and of the resulting bounds and .
The milestone list covers the closed form of the concatenation recursion and its threshold form ; convergence below threshold; the failure bounds and for a network under the two error models; the criterion under which ; and the overhead estimate .
The threshold theorem is the reason large-scale quantum computation is regarded as a physically meaningful goal rather than an idealization: it converts an engineering requirement that scales with the problem size into a fixed, size-independent accuracy target, and it fixes the currency — threshold value and overhead exponent — in which every later architecture is compared. The quasi-independent models matter separately: they show the conclusion does not depend on noise being stochastic, which is what rules out the objection that coherent over-rotations invalidate the stochastic analysis.
The paper's own argument is a physics-style derivation: a circuit-level construction, a combinatorial count of failure-inducing pairs of error locations, and a recursion. This mission formalizes the recursion, the probabilistic bounds and the resulting threshold and overhead statements. It does not formalize the circuit-level content — the -qubit code, the cat-state syndrome extraction networks, transversality, or the count itself; these enter the formal statements as the parameters and . No machine-checked proof of the full threshold theorem, in the sense of a verified fault tolerant circuit construction, is known to the author of this proposal; formalizing the quantitative layer is a prerequisite for one.
The obvious route to "errors vanish under concatenation" is to iterate the bound and observe the doubly exponential decay. That step is the easy half, and the milestone list makes it explicit. What the naive argument silently assumes is exactly what Section II must establish: that the level- failure events again obey a quasi-independent bound, with simultaneous encoded failures bounded by rather than merely each single failure bounded by . This is why the paper's failure declaration is defined backwards in time and demands disjoint pairs of contributing locations. A formalization that bounds only single-gate failure probabilities cannot close the induction.
The second difficulty is bookkeeping at the edges: the recursion is stated for a failure parameter that is a probability in one model and an operator strength in the other, and the overhead bound involves a real exponent and a ceiling, whose interaction with the degenerate cases and has to be handled rather than assumed away.
All parameters are real numbers: , and the gate count is a natural number cast to . levelError is defined by recursion on the level and is total, so it is meaningful for every real ; the threshold hypothesis appears explicitly as where it is needed.
The two error models are predicates on a measure on a measurable space, a Finset of error locations, and a family of failure events, with values in ENNReal; they quantify over all subsets of the location set, matching the paper's "at a given many error locations". The network failure bounds are stated for , the probability that some location fails.
The goal is not vacuous: the hypotheses , , , are simultaneously satisfiable (for instance , , , , ), and the conclusion asserts a strict inequality together with a quantitative overhead bound, so it cannot be discharged by a degenerate reading. Degenerate inputs are inside the statement rather than excluded: , and the case , are covered by the and must be handled.
A complete development needs only Mathlib's real analysis (Real.log, Real.logb, Real.rpow, Nat.ceil) and the measure-theoretic union bound; nothing quantum is required by the formal statements. Contributions strengthening the milestone list towards the circuit level — a formal model of error locations in a network, of the induced next-level error model, or of stabilizer-code recovery — are welcome as further targets.
Quantum computations are performed on physical devices whose elementary operations are never exact: every gate, every idle qubit, every time step is subject to decoherence, damping and systematic inaccuracy. Without protection these errors accumulate and destroy the computation. In 1997 Dorit Aharonov and Michael Ben-Or proved that this can be overcome: as long as the error rate — the probability, per location per time step, that a fault occurs — is below a fixed positive threshold, an arbitrary quantum circuit can be simulated reliably with only polylogarithmic overhead (arXiv:quant-ph/9906129). This threshold theorem is the reason large-scale quantum computing is regarded as physically possible in principle, and the number it produces is the target every hardware programme is measured against.
The engine of the proof is not quantum mechanical but combinatorial. A circuit is encoded, then the encoded circuit is encoded again, times over. The locations of the resulting circuit are organised into a tree of nested rectangles, and the computation survives precisely when the set of faulty locations is sparse in a recursive sense. The mission formalizes that engine: the recursive sparseness calculus of §7.4–7.6 and §8.2 of the paper, which converts a constant error rate below the threshold into a doubly exponentially small failure probability.
Fix two natural numbers: , the number of locations in a rectangle, and , the number of faulty sub-rectangles a rectangle tolerates (in the paper , where is the number of errors the code corrects and is the spread of a fault). A -rectangle is a single location of the circuit, and an -rectangle consists of many -rectangles. A fault pattern of an -rectangle records, for each of its locations, whether a fault occurred there.
Following Definition 18 of the paper, a fault pattern is -sparse by recursion on : at level it is sparse when the location carries no fault; at level it is sparse when at most of the constituent -rectangles carry a pattern that is not -sparse. Under independent probabilistic noise of rate each location is faulty with probability , independently; write for the probability that the pattern of an -rectangle is -sparse, and for the probability that it is not.
Two thresholds appear. The threshold condition for probabilistic noise (Definition 19) is
and the threshold condition for general noise (Definition 21) is
The corresponding thresholds are and : every positive below them satisfies the respective condition.
The goal is the quantitative core of Theorem 10. Below the threshold there are constants such that for every circuit size and every accuracy some recursion depth satisfies both
The first inequality says that, over all rectangles of the simulated circuit, the probability that any of them carries a non-sparse fault pattern is below ; the second says that the overhead per simulated location, , is polylogarithmic in — the cost claimed in Theorem 10.
The milestones build up to it: the two threshold conditions hold below the respective thresholds, the exponent gap of equation 7.5 exists, the base case , the union-bound recursion , Lemma 10 itself (), and the analogous recursion 8.8–8.10 governing the bad part in the general-noise analysis.
Lemma 10 is where a constant error rate becomes a vanishing one. Each level of concatenation only has to improve reliability slightly, because the improvement compounds doubly exponentially in the number of levels; this is exactly why constant-rate noise can be tolerated while Shor's earlier scheme needed a polylogarithmically small rate. The same recursion, with in place of and an extra factor of , controls the trace norm of the bad part of the fault-path expansion in the general-noise model (§8.2), which is how the result is extended from probabilistic errors to decoherence, damping and systematic inaccuracy.
Formalizing this part of the paper yields a reusable, model-independent statement: nothing in the milestones mentions density matrices, so the sparseness calculus can later be plugged into a formal model of noisy quantum circuits, or reused for classical concatenated fault tolerance. What this mission does not do is formalize the circuit-level statement of Theorem 10 — that requires a full Lean model of quantum circuits with mixed states, fault-tolerant procedures, and the code constructions of §3–§6, and is deliberately out of scope here.
The obvious approach — bound the failure probability by a union bound over all fault sets of size and iterate — is exactly right, but the iteration is where the work is. The recursion only produces the doubly exponential decay once the threshold condition is converted into the strict exponent gap of equation 7.5, and the induction has to keep alive to reuse that gap at every level. In the general-noise recursion there is a second trap: the factor exceeds , so the recursion is not contracting termwise, and one needs to bound it by .
On the probabilistic side, the statements are about a genuine product distribution on an exponentially large sample space, not a recursively defined real number: the union-bound step must be carried out over the actual set of fault patterns, where independence across the sub-rectangles is what makes the product bound valid.
Fault patterns are a type defined by recursion on the level: is the booleans and is the functions from the sub-rectangles to ; every level is a finite type with decidable equality. Sparseness is a decidable predicate following Definition 18 verbatim. The noise distribution is given by the weight of a pattern, the product over all locations of (faulty) or (clean), and the sparseness probability is the sum of these weights over the sparse patterns — an honest finite product measure, so no hypothesis is built into the definitions and each statement carries the range hypotheses it needs.
Two conventions are worth flagging. First, the thresholds are formalized as and ; the paper prints the exponent as in equations 7.4 and 8.6, which is inconsistent with its own threshold conditions 7.3 and 8.5, and is the exponent for which the paper's claim "any satisfies the threshold condition" is true. Second, Lemma 10 is stated with rather than the paper's strict , because at the two sides are equal.
Nothing here is vacuous: all hypotheses are satisfiable — for instance , , satisfies every hypothesis of the goal — and the goal quantifies over all circuit sizes and all accuracies, so it cannot be discharged by a degenerate choice. A complete development needs only real analysis, finite sums and binomial counting from Mathlib. Contributions that generalise the branching factor to a per-rectangle bound , or that connect the calculus to a formal model of noisy circuits, are welcome.
A Padé approximant is the "best" approximation of a function near a point by a rational function of prescribed numerator and denominator degrees. The idea goes back to Georg Frobenius (1881), who studied relations among the convergents of a power series, and was developed systematically by Henri Padé in his 1892 thesis. Unlike a truncated Taylor polynomial, a rational approximant can reproduce poles, and it often converges where the Taylor series does not; this is why Padé approximants are standard tools in numerical computation, in the resummation of divergent perturbation series in physics, and — through the "ad hoc methods inspired by Padé theory" — in Diophantine approximation and transcendence proofs.
The theory rests on one structural fact, stated in the source as a single sentence: when it exists, the Padé approximant is unique as a formal power series for the given and . That sentence hides the two theorems this mission asks for — that a suitable pair of polynomials always exists, and that any two such pairs define the same rational function.
Fix a field and a formal power series
Given integers and , one looks for a rational function
whose Maclaurin expansion agrees with that of through order , i.e.
This is denoted .
Written this way the condition is nonlinear in the unknowns and presupposes . The classical device, due to Frobenius, is to linearize: instead of asking that vanish to order , one asks that
A pair satisfying these three conditions is what this mission calls a Padé pair of type for ; it is the predicate every statement below is phrased with. The linearized problem is a homogeneous linear system, so it is always solvable, whereas the original ratio problem is not: the linearized solution may have , in which case no normalized of the displayed shape exists (the " entry of the Padé table is defect"). The two formulations coincide exactly when .
The goal theorem is the conjunction of existence and uniqueness for the linearized problem, over an arbitrary field , for all :
Statement (U) is the precise content of "the Padé approximant is unique": the two pairs need not be equal — they may differ by a common polynomial factor — but they determine the same element of , and hence the same formal power series wherever the quotient is defined.
The milestones are: existence (E); uniqueness (U); the equivalence between the linearized condition and agreement of Maclaurin expansions when ; the Bézout form used by the extended-Euclidean computation of the approximant; the normalization of the denominator to constant term ; and the two worked examples given in the source, namely for and for .
The result itself. Existence and uniqueness are what make the Padé table — the doubly indexed array — a well-defined object, and therefore what make every identity among its entries (the block structure of the table, the Frobenius identities, Wynn's -algorithm and the cross rules) meaningful. Every computational route to the approximant, including the extended-Euclidean route recorded in the source, computes the approximant only because of (U).
Formalizing it. Mathlib has formal power series, polynomials, truncation, and the inverse of a power series with invertible constant term, but no Padé theory: there is no predicate for the condition and no existence or uniqueness statement. This mission adds the linearized predicate and the two structural theorems, which is the minimum foundation on which the Padé table, the block theorem, and convergence results such as Nuttall–Pommerenke could later be built. The results are classical and have textbook proofs; the contribution here is the machine-checked development, not new mathematics.
Neither theorem is deep, but both have a specific step where the obvious approach fails.
For existence, the naive route — solve for , then read off — requires knowing that the homogeneous system for the coefficients of given by the equations "coefficients of of vanish" has a nonzero solution. That is a rank argument about a rectangular Toeplitz-like matrix, and the work in Lean is in packaging it as a linear-algebra statement rather than in the mathematics.
For uniqueness, the one-line argument is to divide: from and conclude . This is invalid, because need not be invertible modulo (its constant term may vanish) and is not a domain. The correct argument compares , whose left side is divisible by while its right side has degree at most ; the difficulty is the degree bookkeeping, not the algebra.
A solver should also note that (U) is not the claim , which is false — rescaling, or a common factor, gives distinct pairs.
The development is over an arbitrary field F (the definition itself only needs a commutative ring), with f : PowerSeries F, and P Q : Polynomial F. Conventions fixed in Lean, and worth reading before starting:
Polynomial.degree ≤ (m : WithBot ℕ), so the zero polynomial satisfies every bound; in particular is allowed and is excluded by an explicit hypothesis.PowerSeries F through the canonical coercion.PowerSeries.exp ℚ and supplied as an explicit series .Contributions of further Padé material — the Padé table, defect entries, the block structure, or the -algorithm — are welcome as follow-up missions built on this predicate.
A two-stage stochastic linear program chooses a first-stage decision before uncertain coefficients are known and then uses recourse variables to repair the decision after the data are observed. The resulting expected recourse cost is central to existence, stability, and numerical methods: if it can be infinite, an apparently feasible model may still have no meaningful expected objective; if it is differentiable with a continuous gradient, deterministic smooth optimization methods become available on the feasible first-stage domain. Chapter III of Peter Kall's Stochastic Linear Programming develops these properties for fixed recourse. This mission packages two complete results from that development: Theorem 12 on continuous differentiability and Theorem 15 on the exact finiteness criterion under complete recourse.
Theorem 12 is the goal. Theorem 15 is retained as a separate source theorem from the same expected-recourse setting, not as a lemma asserted to prove Theorem 12. Keeping both statements makes the distinction between the general feasible-domain regime and the stronger complete-recourse regime explicit.
Fix a deterministic matrix (W\in\mathbb R^{m\times p}). A random data point is a triple (d=(A,b,q)), where (A\in\mathbb R^{m\times n}), (b\in\mathbb R^m), and (q\in\mathbb R^p), with arbitrary joint probability law μ. For a first-stage vector (x\in\mathbb R^n), the pointwise recourse value is the extended-real linear-program value
The extended-real convention records an infeasible recourse problem as (+\infty) and an unbounded-below problem as (-\infty). The recourse domain is
Thus (K) requires almost-sure feasibility but does not assume complete recourse and does not exclude a value of (-\infty). The signed extended expectation follows Kall's equation III.(8): it is the integral of the positive part minus the integral of the negative part. A separate real-valued expected-recourse adapter integrates (Q(x,d).\mathrm{toReal}); the target uses that adapter only after explicitly concluding almost-sure finiteness and integrability, so totalization at infinities does not hide a divergent cost.
The shared moment condition is exactly the disjunction from Theorem 10 and Corollary 11: all coordinates of (A,b,q) are square integrable; or (q) is almost surely constant while (A,b) are integrable; or (A,b) are almost surely constant while (q) is integrable; or all three random coefficient ranges are bounded. No independence or finite-support hypothesis is imposed.
Finally, (W) has complete recourse when every right-hand side (z\in\mathbb R^m) admits a nonnegative (y) satisfying (Wy=z). This is stronger than membership of one decision in (K), but it does not by itself prevent an unbounded-below recourse cost.
Assume one of the four moment alternatives, assume the signed expected recourse is strictly above (-\infty) at every (x\in K), and assume the joint law μ is absolutely continuous with respect to Lebesgue measure on the full finite-dimensional coefficient space. Then the pointwise recourse value is finite almost everywhere and its real projection is integrable for each (x\in K). Moreover, there is a continuous field of linear functionals (g(x)) such that
including boundary points of (K). In Lean this is stated by ContinuousOn g K together with HasFDerivWithinAt for the expected-recourse function at every point of (K). It is not weakened to differentiability only on the interior, and it does not add complete recourse.
Under complete recourse and one of the same four moment alternatives, for an arbitrary fixed (x\in\mathbb R^n),
The left side means that the signed extended expectation equals a real number, not merely that a totalized real integral returns a value. The right side requires feasibility of the dual inequalities almost surely; it does not require attainment or optimality. This full equivalence is the mission's supporting milestone.
Theorem 12 supplies a smooth expected objective on the entire source feasible domain under an absolutely continuous data law. That conclusion is stronger than convexity or local Lipschitz continuity: it provides a continuously varying derivative while retaining boundary points and the random dependence of all coefficient blocks. The explicit finiteness and integrability clauses make clear when the real expected objective faithfully represents the extended-real model.
Theorem 15 separates two different well-posedness questions. Complete recourse guarantees primal feasibility for every residual, while almost-sure feasibility of the dual inequalities is exactly what prevents the expected value from escaping the real line under the stated moment conditions. Omitting either direction would lose the source's characterization.
Both results are established in the 1976 book; the staged Lean theorem declarations contain proof placeholders. Completing them would give machine-checked versions of the source statements using reusable definitions for equality-constrained nonnegative linear-program values, pointwise recourse, expected recourse, complete recourse, the signed expectation, and the four moment regimes.
For differentiability, a pointwise optimal solution or dual vector need not vary continuously when the active basis changes. Absolute continuity removes coefficient configurations lying on relevant exceptional hyperplanes only after a measure-theoretic argument, and the conclusion must hold relative to a possibly closed feasible domain rather than only on an open set. One must also prove finiteness and integrability before using the real-valued expectation; simply differentiating the totalized toReal expression would not establish the source theorem.
For finiteness, complete recourse handles feasibility but not unbounded negative cost. The dual system is random through (q), and the equivalence concerns almost-sure existence of a dual-feasible vector together with a signed extended expectation. Assuming dual feasibility or integrability of the recourse value at the outset would make one direction circular.
All coefficient spaces use finite Fin indices and real scalars. The law is an arbitrary probability measure on the joint product (A,b,q). The density premise for Theorem 12 is ambient absolute continuity with respect to the product Lebesgue volume; it is not a density on an unspecified lower-dimensional support. Consequently, some constant-coordinate moment branches may be incompatible with that density premise, matching the reviewed ambient interpretation rather than silently changing the measure space.
The feasible domain uses (Q(x,d)<+\infty) almost surely and includes its boundary. The signed expectation preserves positive and negative infinities. Theorem 12 assumes it is above (-\infty) on (K) and concludes the conditions needed for the separate real integral. Theorem 15 adds complete recourse but no density, independence, finite support, pre-assumed dual feasibility, or pre-assumed value integrability. Its decision (x) remains arbitrary.
The mission reuses the platform definitions of LPValue, PointwiseRecourse, ExpectedRecourse, and CompleteRecourse. The book-local Kall1976 namespace contains only the expression-essential data type, feasible domain, signed expectation, moment disjunction, and the two reviewed theorem statements. Contributions may add analytical, measure-theoretic, or linear-programming lemmas needed for proofs, but may not replace the signed expectation by a totalized real value, restrict Theorem 12 to the interior, or weaken Theorem 15 to one implication.
An exclusion system models particles moving among sites under the rule that each site is either vacant or occupied. A move exchanges the occupation variables at two sites, so particle number is conserved. On a countably infinite site set, however, the formal sum of all possible exchanges need not automatically determine a well-defined Markov evolution. Individual rates can be continuous and bounded while infinitely many potential exchanges remain active. Chapter 8, Section 3 of Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, gives conditions under which this formal operator closes to the generator of a conservative Feller semigroup Ethier--Kurtz, Theorem 3.6.
This mission states that theorem with its complete weighted two-site domain and its finite-coordinate core. It does not replace the countable system by a finite Markov chain, collapse the ordered-pair generator sum, or substitute the neighboring spin-flip theorem. Spin flips change particle number one coordinate at a time; exclusion moves exchange two coordinates and conserve it.
Let S be a countable type of sites. A configuration is a function η : S → Bool, where false and true relabel vacancy and occupation. The product topology is induced by the discrete topology on Bool. The Lean space C(S → Bool, ℝ) consists of continuous real-valued observables on this compact configuration space and carries the uniform norm.
For sites i and j, exclusionExchange i j η swaps η i and η j and leaves every other coordinate unchanged. When i = j, the exchange is the identity. For an observable f, its two-site exchange variation is
The theorem assigns a continuous nonnegative rate c i j to every ordered pair and a nonnegative real dominating weight γ i j. Both families are symmetric, the diagonal rates vanish, and c i j η ≤ γ i j. The rows of γ are summable with one uniform upper bound, which is the Lean form of equation (3.27).
Rate dependence on the configuration is controlled through a different operation. spinFlip k η toggles the single coordinate k, and spinVariation (c i j) k measures the resulting uniform change in the rate. Equation (3.28) requires these single-site influences to be summable and bounded by K * γ i j, with one constant K for all pairs. The influence condition therefore deliberately uses single-site flips even though the dynamics itself uses two-site exchanges.
The pre-generator graph implements equation (3.29). Its domain is exactly the continuous observables satisfying
where the sum is over ordered pairs and has no factor of one half. For (f,g) in the graph, the continuous output satisfies
The goal is Theorem 3.6 in full. Every observable in the weighted domain has a continuous image in the graph. The graph closure in the product uniform-norm topology is single-valued and equals the derivative graph of a strongly continuous contraction semigroup. The semigroup preserves nonnegative functions and the constant function one, expressing the conservative Feller conclusion.
The last clause retains the source's cylinder core. Restrict the initial graph to observables determined by finitely many coordinates: there is a finite set F such that configurations agreeing on F receive the same value. The closure of that restricted graph equals the entire closed generator graph. Generation, the full weighted domain, and the core remain one target because they are conclusions of the same source theorem.
The theorem turns an infinite formal exchange sum into a closed Markov generator on continuous observables. The conclusion is stronger than pointwise convergence of the series: it identifies the whole generator domain through a derivative biconditional, provides positivity and conservativity, and establishes a finite-coordinate class from which the closed graph can be recovered.
The result is proved in the textbook. The formalization target is its precise Lean statement, including symmetry, zero diagonal, domination, the uniform row bound, the single-site influence bound, the weighted ordered-pair domain, graph closure, Feller generation, and cylinder core. Reusable infrastructure consists of the book-wide contraction-semigroup predicate and the already shared single-site flip and variation definitions; the exchange, exchange variation, and weighted graph are specific to this model.
A naive finite-state jump-process argument does not apply. Countability and a uniform row bound do not turn the full ordered-pair collection into a finite set of moves. Pointwise notation for the exchange series also does not by itself prove that the result is continuous, that the graph closure is single-valued, or that finite-coordinate observables form a core. The weighted two-site domain and the configuration-influence condition are therefore essential parts of the theorem rather than optional regularity assumptions.
The spin-flip and exclusion models cannot be interchanged. A coordinate flip creates or removes occupation and is measured by a one-site domain. An exclusion move conserves occupation by swapping two coordinates and requires the γ-weighted two-site variation domain. Only the rate-influence hypothesis uses the shared one-site variation.
The Lean statement allows empty, finite, and countably infinite S, matching the source's countability assumption without adding nonemptiness. Bool is an exact two-state encoding of {0,1}. Real suprema define both one-site and two-site uniform variations over the nonempty compact configuration space. Explicit Summable hypotheses prevent divergent real tsum expressions from being silently totalized.
The graph records a continuous output equal to the actual pointwise ordered-pair series. Its first conclusion ensures that this representation does not shrink the stated weighted domain. Closure is taken in C(S → Bool, ℝ) × C(S → Bool, ℝ). The semigroup is real-time indexed, while its laws and bounds are imposed for nonnegative times. No finite-site restriction, finite-total-rate replacement, factor of one half, exchange-based substitute for the influence bound, or weakened core statement is admitted.
Chapter 4's framework (formalized in this series' 04-framework mission) solves the online
covering-packing pair only in the restricted setting a(i,j) ∈ {0,1}, b(j) = 1 — every
constraint is an unweighted "cover me with at least one of these" condition. Chapter 14 delivers
the promise made at the very start of the survey (p. 115: "we show how to extend the ideas we
present here to handle general (non-negative) values of a(i,j) and b(j)"): fully general
non-negative coefficients, normalized so every constraint reads ∑_i a(i,j)x(i) ≥ 1. This
mission formalizes both halves of that generalization — the packing scheme (Theorem 14.1, with a
matching lower bound, Lemma 14.2, showing an extra additive term is unavoidable) and the covering
scheme (Theorem 14.3, the goal).
Fix a finite set I of primal (covering) variables with positive costs c(i), and a finite set
J of dual (packing) variables/covering constraints, with a(i,j) ≥ 0 for every pair (Fig. 14.1).
The packing scheme (Section 14.1) is parameterized by a target competitive ratio B > 0: on each
new dual variable y(j) and its coefficients a(i,j), the algorithm increases y(j) continuously
and each x(i) by an explicit exponential increment function until the new primal constraint is
satisfied, achieving B-competitiveness for the packing objective at the cost of an additive
O(log(a_i(max)/a_i(min))) term (beyond the multiplicative O(log n)) in how much each dual
constraint can be violated — qualitatively different from Chapter 4's purely multiplicative
O(log d) bound, and Lemma 14.2 proves this additive term cannot be removed. The covering scheme
(Section 14.2) instead works in phases: each phase assumes a doubling lower bound α(r) on OPT
and "forgets" its primal/dual variables once the primal cost exceeds α(r), restarting with
α(r+1) = 2α(r) — a structurally different mechanism from Chapter 4's direct algorithms, needed
because with general coefficients a single monotone run can no longer be analyzed via one
potential function alone.
Theorem 14.3 (the goal, p. 253): for any B > 0, the phase-based covering scheme (each
constraint normalized to ∑_i a(i,j)x(i) ≥ 1/B) is competitive with an explicit ratio
8 log(2n)/B, taken directly from the proof's own final displayed chain,
2α(r) ≤ 4α(r-1) ≤ (8 log(2n)/B) Y(r-1) ≤ (8 log(2n)/B) OPT (p. 253-254) — the theorem's own
statement only gives O(log n/B), so this explicit constant is this mission's own
instantiation from the proof, not an independent derivation and not a transcription of a
displayed theorem-level formula (flagged, per this series' explicit-constants rule).
Two milestones, in attack order:
B-competitive, and violates each dual
constraint by at most the book's own exact displayed bound
c(i)·2log(1 + n·a_i(max)/a_i(min))/B (Claim (3) — the exact constant the proof establishes,
not the theorem headline's O(·) simplification).log(a(max)/a(min)) term of Theorem 14.1 is necessary.This chapter is the survey's demonstration that the primal-dual framework's core technique survives its most natural generalization, at the price of an explicit extra term the chapter also proves is unavoidable — a tight characterization, not merely an upper bound. Every other online covering/packing chapter in this survey (set cover, routing, ad-auctions, bounded allocation) is technically a special case of this chapter's general model; Chapter 4's restricted framework is the pedagogical entry point, and this chapter is where the general theory actually lives. No formal development of the general packing-covering problem was found on the platform as of 2026-09-20; this mission is the first.
Two distinct obstacles, mirroring this chapter's own two schemes. First, Theorem 14.1's proof
(p. 249-251) establishes its per-round primal/dual derivative inequality via a direct calculus
argument (differentiating the explicit increment function) — formalized here as a hypothesis
(hX_le_BY) standing for that calculation, not reproduced, since the goal is a faithful
statement of the resulting competitive ratio, and the increment function's own exponential form
is transcribed in the theorem's docstring but the differentiation itself is out of scope. Second,
Theorem 14.3's phase-based mechanism is genuinely stateful across an unbounded number of phases
(each phase resets its own primal/dual variables while the LP's actual variables retain the
running maximum) — modeling this process explicitly is comparable in complexity to Chapter 13's
level-based algorithm, and this mission makes the same scope choice: the mechanism's output
(the resulting cost/profit relationship, hX_le_ratio) is taken as a hypothesis standing for the
book's own Claims (1) and (3) combined, rather than constructed phase-by-phase.
GeneralInstance I J bundles Fig. 14.1's fully general LP data (a(i,j) ≥ 0, c(i) > 0) —
restated locally (not importing 04-framework's CoveringInstance) per this series' rule against
cross-draft imports, even though this chapter is the direct generalization of that one.
aMax/aMin are the per-variable (not per-instance) maximum and minimum-non-zero coefficients
Theorem 14.1 needs. harmonicNum is restated locally (duplicated from 13-bounded-allocation's
own definition, for the same no-cross-draft-import reason). Both goal-adjacent theorems use this
series' weak-duality "competitive against any feasible comparison solution" pattern
(04-framework, reused as a convention, not re-derived): Theorem 14.1 against any feasible
packing comparison (matching that it concerns the packing side), Theorem 14.3 against any
feasible covering comparison (matching the covering side). Welcome contributions: completing
the three sorrys (Theorem 14.1's calculus argument, Theorem 14.3's phase-based mechanism
constructed explicitly, and Lemma 14.2's direct summation argument, which is the most tractable of
the three to actually prove), and formalizing the sanity check that both schemes reduce to
Chapter 4's Algorithm 1/2/3 when a(i,j) ∈ {0,1}, b(j) = 1 (checked by hand in SELF_REVIEW.md,
not as a Lean lemma).
Network routing is one of the paradigmatic applications of the online primal-dual method:
requests for bandwidth between a source and target arrive one at a time, and the algorithm must
commit bandwidth to paths without knowing future requests. Chapter 4 already gave a simple
(3, O(log n))-competitive routing algorithm as an illustration of the general framework. This
chapter asks for something qualitatively stronger: a uni-criteria (1, O(log n))-competitive
algorithm — one that routes the full optimal bandwidth (no loss on the throughput side at all),
paying only in a bounded edge-capacity violation. The chapter shows this exact-throughput
guarantee is achievable, and is moreover the key building block for several other routing
objectives (fair routing, max-min fairness) built on top of it in Section 9.2 — a (1, O(log n))-competitive algorithm composes into those richer objectives in a way a merely
constant-factor-lossy algorithm does not.
Fix a graph , , , with integer edge capacities . Routing requests arrive online, each demanding one unit of bandwidth between a source and target; in the splittable model (this chapter's comparison class), a request's bandwidth may be divided across multiple paths. A -competitive algorithm routes at least of the maximum possible bandwidth while guaranteeing every edge's load (bandwidth allocated divided by capacity) is at most . The chapter's generic algorithm (Section 9.1) maintains, for each of copies of the graph (copy keeping only edges of capacity at least , each capped at ), a primal-dual pair matching Chapter 4's own routing LP (Fig. 9.1, identical to Fig. 4.2): a request is routed on the shortest path (by the copy's current primal edge-lengths ) if that length is below , multiplicatively updating on the path's edges; otherwise, subject to a capacity-limited fallback rule, on an arbitrary feasible path.
Theorem 9.2 (goal, p. 204): the algorithm is (1, O(log n))-competitive with respect to all
splittable routing solutions — exact throughput (ratio 1), edge load at most O(log n).
Lemma 9.1 (milestone, p. 202-204): a single copy 's own guarantee, which Theorem 9.2's proof composes across all copies: the algorithm accepts at least (the maximum splittable bandwidth achievable in , out of the requests introduced to it) and incurs load on every edge of .
This is the survey's demonstration that the online primal-dual method, in its most basic form (a single accumulating dual sum driving a multiplicative primal update, exactly Chapter 4's framework), scales to a genuinely harder bicriterion objective once composed across a carefully constructed family of graph copies — the copies are what let the algorithm avoid ever needing to reason about which of the exponentially many - paths to consider, reducing routing to a sequence of independent shortest-path computations. The chapter's own Section 9.2 builds a coordinate-wise-competitive fair-routing algorithm directly on top of Theorem 9.2 (not formalized here), and its Notes section places -competitiveness as "a crucial non-trivial step" the chapter needed before those richer objectives became tractable at all. No prior formalization of online routing, splittable or otherwise, was found on the platform as of 2026-09-20 (search below).
This is the most algorithmically intricate chapter in this series: the algorithm processes each
request against every one of graph copies, each copy running its own instance of the
Chapter-4-style primal-dual update, and Theorem 9.2's own proof composes Lemma 9.1's per-copy
guarantee via a combinatorial backward induction (partitioning the offline-optimal solution's
paths into groups by bottleneck capacity, and showing group by group that the algorithm's
cumulative routed bandwidth across the top levels dominates the cumulative optimal bandwidth in
those groups) together with a separate geometric argument bounding how many copies any single
edge can meaningfully appear in. Fully modeling the copy construction, the request-routing
process, and both composition arguments from first principles was judged to exceed this mission's
time budget without sacrificing the faithfulness of what does get stated (per CAPTAIN_BRIEF.md
rule 6). Instead: Lemma 9.1 is formalized via the two facts its own proof isolates as doing the
real work — a weak-duality contradiction bound (stepB ≥ M − uMin) and the step-(1c) fallback's
own greedy-fill rule for part (i); the multiplicative-update invariant x(e,j) ≤ 2 for part (ii),
whose consequence — the exact constant 2 + 6·log₂n — is re-derived from scratch in this mission
(the displayed equation this derivation depends on was garbled by the PDF's text extraction; it
was confirmed against the actual typeset page image before drafting, see SELF_REVIEW.md).
Theorem 9.2 then composes Lemma 9.1 across copies via two explicit, clearly-labeled hypotheses
standing for the book's own backward-induction accounting and edge-multiplicity argument,
respectively — genuine mathematical content this mission does not re-derive, named honestly as
hypotheses rather than silently assumed away or approximated by a weaker statement.
No shared data structure was introduced: every quantity in both theorems (bandwidths, capacities,
loads) is a plain real-number hypothesis-level parameter, since neither theorem's own content
needs a reusable instance record (unlike the packing/covering CoveringInstance of
04-framework, this chapter's per-copy quantities are consumed once each, not threaded through a
family of algorithms). per_copy_guarantee (Lemma 9.1) takes the weak-duality bound, the
step-(1c) fill rule, and the x(e,j)≤2 invariant as hypotheses and derives both parts of the
lemma's conclusion by real algebra (a sign case-split for part (i); Real.logb/rpow manipulation
for part (ii)). routing_competitive (Theorem 9.2) takes Lemma 9.1's guarantee (universally
quantified over the copy index J, a general Fintype) plus the two composition hypotheses
described above, and derives the bicriterion conclusion by summation, transitivity, and scaling.
This correctly rules out the trivializing formalization in which the composition hypotheses are
strengthened to directly assert the theorem's own conclusion (each is a strictly weaker,
independently-motivated fact — the backward-induction accounting identity and the geometric
edge-multiplicity bound — checked in MODERATION_NOTES.md against this exact failure mode).
Reals throughout; Real.logb 2 for log₂. Welcome contributions: completing the two sorrys
(Lemma 9.1's part (i) is short algebra; part (ii) needs Real.rpow/Real.logb lemmas; Theorem
9.2's is transitivity/summation once its hypotheses are in hand), and — the natural follow-on —
formalizing the copy construction and the backward-induction/edge-multiplicity arguments
hquota/hload_aggregation currently stand in for, which would upgrade them from hypotheses to
theorems in their own right; Section 9.2's coordinate-wise-competitive fair-routing algorithm
(Theorem 9.3) and the matching lower bound (Lemma 9.5) are further natural follow-ons.