Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. A high-probability approximation guarantee is a separate claim requiring an explicit probability bound. The optimum includes entangled states. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Network revenue management is the problem of selling several limited, perishable resources (seats on flight legs, hotel room-nights, machine hours) to customers who arrive over time and each want a fixed bundle of them. A seller who accepts every request early may run out of the resources that the most valuable later customers need, and a seller who is too cautious leaves capacity unsold at the end of the horizon. Airlines, hotels and car-rental firms solve instances of this problem daily (Talluri and van Ryzin, 2004).
The exact optimal policy is a dynamic program over the vector of remaining capacities, which is intractable for realistic networks. The standard remedy replaces the random demand by its mean, which gives a linear program, the deterministic LP (DLP), and turns its solution into an admission rule. Its value is an upper bound on what any policy can earn (Gallego and van Ryzin, 1997). Solving the LP once, at time zero, loses against that bound over a horizon of length . A natural improvement is to re-solve the LP as capacity is consumed.
Timeline of the re-solving question, as the source surveys it (Sec. 1, pp. 3–4):
There are customer classes and resources . Over the horizon , class- customers arrive according to independent Poisson processes with rates . Accepting a class- customer earns and consumes units of each resource ; is the bill-of-materials matrix and its -th column. The initial capacity vector is . A customer can be accepted only if componentwise, where is the capacity remaining at its arrival.
For a capacity-per-unit-time vector , let
The DLP value is .
The Frequent Re-solving policy (FR) divides the horizon into unit periods . At the start of period , with remaining capacity , it sets , computes an optimal solution of the LP with right-hand side , and during the period accepts each class- arrival with probability , subject to the capacity check. Its expected revenue is . The LP may have several optimal solutions; the results hold for every rule choosing among them.
There is a constant , depending only on , and , such that for every integer , every capacity and every choice of optimal LP solutions,
The content is the uniformity: does not depend on , so the bound holds whether capacity is scarce, abundant, or degenerate for the LP.
The result. Because bounds the expected revenue of every admissible policy, Proposition 3 says that FR loses at most against the optimal policy in every instance, degenerate or not. Re-solving therefore never does worse, in order, than solving once. Together with the lower bound on a degenerate instance (Proposition 2 of the same paper), it shows that the order is exact for FR. The nondegeneracy assumption of the earlier analysis cannot be dropped. The explicit form (milestone 5) bounds the loss by constants computable from .
Formalizing it. The result is proved in the source; no part of it is machine-checked. A formalization adds three things. It gives a precise model of an adaptive, randomized admission policy in a Poisson network, which other results on re-solving and bid-price policies can reuse. It gives a checked LP sensitivity bound. And it checks the paper's constants: the printed constant of Lemma 8 is wrong (see Formalization scope), and the mission states the corrected one.
The obvious argument compares FR with the DLP period by period: the LP that FR solves at time differs from the original only in its right-hand side, so the loss should be controlled by how far drifts below . Two things break a naive version of this. First, is a ratio whose denominator shrinks to , so fluctuations late in the horizon are amplified; a crude bound on the drift at each sums to more than . Second, FR's realized consumption is not the LP's target: the capacity check rejects customers, and the LP solutions depend on the whole past, so the consumption in different periods is not independent.
Uniformity in is the whole point. Arguments that rely on a margin between and the degenerate points of the LP, as in the nondegenerate analysis, give constants that blow up as that margin vanishes.
The source is arXiv:1802.06192v3, whose printed page numbers equal the PDF page numbers. Everything lives in the namespace ResolvingNRM.FRUpper.
piValue A r b lam of RLPBidPrice.Unbiased.Model (a real supremum, equal to the LP maximum for ).sel; every theorem quantifies over all selectors, with constants chosen before the selector.windowExp). FR's value is a backward recursion over periods (frTail), and expectations of functions of are a forward recursion (frStateExp).A trivializing formalization is ruled out. The constant is chosen before . FR is defined with every optimal LP solution, not only nondegenerate or vertex ones. The capacity check is kept arrival by arrival; without it, FR's expected revenue would equal the LP revenue it targets and the gap would be trivially small.
Contributions welcome on every milestone. The LP sensitivity bound (33) is a statement about linear programs alone and milestone 4 about real numbers alone; both are reusable outside this mission, as is the window model of a randomized admission policy.
Bibliographic details of the non-arXiv entries are those of the source's reference list (pp. 24–25).
On one processor, the completion time of a job normally depends on how much work precedes it. In the model of Browne and Yechiali (1990), waiting also changes the job's own processing requirement: a job that starts later takes longer. The sequence therefore changes both when each job starts and how long subsequent jobs must wait. This matters when the goal is a weighted completion cost, because a delay to one job can raise the completion costs of many others.
The paper gives an expected-makespan ordering for this linear deterioration model and, in Proposition 2, a sufficient condition under which the original job order minimizes weighted expected completion cost. The latter is the target of this mission. Related platform work on Delayed SWPT and the AvgCompletionSched family treats weighted completion scheduling without this job-specific linear deterioration. Their additive processing-time models do not supply the completion-time object used here.
There are jobs, all available at time zero, processed one at a time on a single machine without idle time or preemption. A schedule is a permutation of the jobs: is the job processed in position . The paper labels positions and jobs from to ; the Lean development labels them from to . The identity schedule processes jobs in label order.
For job , is its random initial processing requirement, its deterministic growth rate, and its waiting cost rate. If the job starts at time , its actual processing time is . Deterioration stops once processing starts. Write for the time at which the first scheduled jobs have all finished. The model sets and
in the paper's one-based position notation. Thus the completion time of the job in position is . Its cost is its own rate times that completion time, giving
All of these are random quantities until an expectation is taken. Equation (2) of the paper writes as a sum of the initial requirements multiplied by the later growth factors. Equation (8) substitutes that expression into . Both equations are included as milestones, stated along an arbitrary schedule by relabelling the jobs. The third milestone is the exact change in from swapping two adjacent jobs. These three statements are pathwise identities, so their mathematical content does not depend on a probability distribution.
The principal target is Proposition 2: if both sequences of job-indexed ratios are strictly increasing,
then, for every permutation ,
The first ratio compares an initial expected requirement with its growth rate. The second couples growth and the cost rate. The conclusion is global optimality over the paper's whole class of nonpreemptive, non-idling permutations. It does not assert that the identity order is the unique minimizer; strict input ratios do not by themselves justify a uniqueness claim.
The attack path records exactly the supporting statements printed in the paper: the closed completion-time formula (2), the weighted cost formula (8), and the unnumbered adjacent-interchange identity after (8). The milestone quotations preserve the paper's printed display, while the Lean statements use an arbitrary permutation where relabelling permits it. The interchange display has a multiplication dot before its second bracket; expansion for two jobs shows that the term is added. The formal statement records that correction, and the source quotation retains the printed symbol.
The proposition identifies a directly checkable pair of ordering conditions under which the natural job-label order solves a weighted stochastic scheduling problem. A condition involving only , enough for the paper's expected-makespan target, does not determine this weighted objective. The cost rates introduce another ordering requirement. The result gives a sufficient rule, not a characterization of every optimal schedule or of every parameter choice.
The mathematical result was published in 1990; this mission asks for its machine-checked formalization. A complete development will connect the processing-time recursion, the pathwise cost identities, and the expected optimality statement in Lean. The recursion and cost definitions can be reused for other finite single-machine problems in which a job's processing time depends on its start time. The milestone identities are also useful independently of the final sufficient condition, including for studying other choices of weights and ordering indices.
Sorting by expected initial requirement alone cannot settle the problem, because processing a job changes later start times and hence later processing times. Even sorting by the expected-makespan index leaves the cost rates unaccounted for. The value of an adjacent swap depends on the elapsed time before the pair and on the completion costs of jobs after the pair. It is not enough to compare the two jobs' own completion costs in isolation.
The source states the sufficient condition after its interchange display but does not present a full proof of the global claim. Closing the Lean goal requires connecting local comparisons to every schedule and handling the expected value of the recursively defined cost. The identities are finite, but their indices change between zero-based Lean positions and the paper's one-based display, especially at the first position and at an empty suffix.
Jobs are , and a policy is an equivalence permutation with equal to the job in position . Completion time is defined by the processing rule , not by the closed form (2). At positions beyond the jobs it stays constant, and theorems about the closed form restrict to . The total cost is defined from job-weighted completion times, not from equation (8). This keeps both identities substantive.
The proposition uses a probability space and the Bochner integral of the real-valued cost. Every is integrable, so its expectation and the finite linear combinations appearing in the cost are meaningful. Initial requirements are nonnegative at every outcome, reflecting the paper's standing positive-processing convention; strict positivity is unnecessary for the claim. Growth rates and cost rates are strictly positive. Those two assumptions make the printed ratios well-defined and support the ordering rule. The paper's common independence convention is not required for these expectations and is not assumed.
The two strict orderings are over the labels of jobs in , not positions of an arbitrary schedule. The conclusion compares with every permutation, not only with schedules obtained by one adjacent swap. The and cases are allowed: the order conditions have no pair to compare, and there is only one permutation. Solvers may contribute the finite-sum, interchange, and integrability facts needed to link the milestones to Proposition 2. The pathwise identities require no probability assumptions and can support later variants.
Fitting a statistical model usually means solving a convex problem of the form
where holds one training example per row and one feature per column, is the response, is a convex loss and a convex regularizer. Least squares, the lasso, logistic regression and the support vector machine are all of this form. When either dimension is very large, or the data are stored on many machines, the problem has to be solved by processors that each see only a block of .
Chapter 8 of Boyd, Parikh, Chu, Peleato and Eckstein's monograph on the alternating direction method of multipliers (ADMM) (Found. Trends Mach. Learn. 3(1), 2011) shows how ADMM does this in two ways: by splitting by rows (splitting across examples, §8.2), which turns the problem into a global consensus problem, and by splitting it by columns (splitting across features, §8.3), which turns it into a sharing problem. In both cases the method is only practical because the individual updates have closed forms or reduce to small standard problems. This mission formalizes those closed forms, culminating in the update for the group lasso.
Vectors are in with the Euclidean norm ; . Throughout, is the ADMM penalty parameter and a regularization weight.
Splitting across examples. Partition and by rows into blocks , . With scaled dual variables and averages , , the consensus ADMM iteration is
followed by . For the lasso, and .
Splitting across features. Partition with and with , so . Introducing gives a sharing problem; its ADMM -update minimizes . Writing and for the average of the , this reduces to a single problem in , all dual variables coincide, and each block update minimizes
for a vector assembled from the previous iterate. For the group lasso, (not squared).
Soft thresholding is for , for , for .
Let on and . Then
and then is the only minimizer; if , there is exactly one with , the point minimizes , and every minimizer is of this form.
The goal result says that a group-lasso block either switches off entirely, which is how group sparsity arises, or solves a ridge regression whose ridge parameter is the unique root of a scalar monotone equation; this is what makes the distributed group lasso implementable with one cached factorization per block and a bisection. The milestones are the remaining closed forms that turn the two distributed schemes of Chapter 8 into concrete algorithms, and the reduction of milestone 3 is the structural fact that lets feature splitting carry a single dual variable.
The book derives these facts in running text and states them without proof. None of them is formalized on Prove2Me, and the book's printed zero test for the lasso (p. 69) uses the wrong norm; a machine-checked collection of the correct updates removes that kind of error from the record and gives later ADMM missions a verified library of update formulas.
Each statement is a characterization of all minimizers of a nonsmooth convex function, not a check that a formula satisfies a stationarity equation. For the goal, the nonsmooth term has a kink at , need not be strictly convex when has a nontrivial kernel, and the existence and uniqueness of the parameter is part of the claim rather than an assumption: the obvious move of assuming a suitable and checking the formula proves nothing about the case split or about uniqueness, and the singular case of is exactly where naive arguments break. Milestone 3 must handle an arbitrary convex loss , with no closed form at all.
Vectors are EuclideanSpace ℝ (Fin n); matrices are Matrix (Fin m) (Fin n) ℝ acting through Matrix.toEuclideanLin; blocks are indexed by Fin N (0-based); the regularization weight is lam; the eigenvalue vector the book also calls (p. 70) is μ. " minimizes " is Mathlib's IsMinOn F Set.univ x. Iteration superscripts are dropped: each statement is about one update with the previous iterate given. Explicit choices:
A statement that only checks that satisfies the optimality equation, or that assumes the parameter exists, does not capture the goal; the goal asserts existence and uniqueness of and describes every minimizer of .
Contributions welcome: subgradient calculus for and in EuclideanSpace, first-order optimality for convex quadratics plus a convex nonsmooth term, and the monotonicity of for positive semidefinite ; these are reusable for every proximal and ADMM update.
Binary decisions arise when a variable records whether a project is selected, a facility is opened, or an action is taken. Linear constraints then describe the resources or conditions those choices must satisfy. Egon Balas's 1965 paper gives a direct algorithm for a finite linear program with zero-one variables: it begins with all variables at zero, adds variables with value one, and uses explicit tests to discard assignments that cannot improve the best feasible assignment found so far. The paper states that the procedure eventually produces an optimal feasible solution or a conclusion that none exists. Its numbered convergence theorem is the target of this mission. Balas (1965)
The result is historically distinct from algorithms that solve a continuous relaxation and then enforce integrality. Balas describes his method as a direct combinatorial search over binary assignments, with additions and subtractions used to update costs and slacks. The theorem concerns the correctness and finite termination of the particular steps printed in the paper, including their backward scan and cancellation rules. The local catalog contains work on branch and bound for a biconvex program, but no existing platform item about a zero-one programming algorithm with these steps; the biconvex result concerns a different model and algorithm. Balas (1965)
Let be a finite set of binary coordinates and a finite set of constraints. The data are a real matrix , a real vector , and nonnegative objective coefficients . A binary assignment is represented by the set of coordinates assigned one; all other coordinates are zero. Its slack and cost are
The assignment is feasible when for every . It is optimal when it is feasible and has no greater cost than any other feasible assignment. These are Balas's problem and solutions (1)–(8). The coefficients of and may have either sign; and may be empty. Balas (1965), pp. 519, 523
The algorithm generates assignments , starting at . Among the generated feasible assignments, their least cost is the ceiling ; if there are none, . Each generated assignment has an improving set formed when it first appears. Later steps cancel candidate indices and keep records of which values attached to an earlier assignment have been cancelled by the time is generated. The algorithm either processes the latest assignment, scans earlier strict subsets in descending order, or stops. Its value-based choice rule permits several choices when both value and cost tie. Balas (1965), pp. 523–528
The paper's two lemmas and Theorem 1 establish the cancellation claims used by its convergence theorem. Lemma 1 says a feasible completion below the current ceiling adds no index in ; Lemma 2 makes the corresponding assertion for an earlier assignment under its stated complete-cancellation hypothesis. Theorem 1 says that an abandoned assignment has no better feasible completion. The two numbered parts of the convergence proof assert that a single iteration cannot continue indefinitely and that no assignment is generated twice. A remark after (16) records that a feasible generated assignment has an empty improving set. Balas (1965), pp. 529–533
The mission's goal is Convergence Theorem 2:
The finite-step assertion includes progress: every reachable state before a stopping situation has a successor. At a stop, means no feasible binary assignment exists; if the ceiling is finite, a generated assignment attaining it exists and every generated assignment at that cost is optimal for . These clauses make the paper's two possible outcomes explicit. Balas (1965), Convergence Theorem 2 and step 5a
The theorem certifies the algorithm as a complete decision and optimization procedure for the stated finite binary program. The infeasibility outcome concerns every possible binary assignment, not only the assignments the algorithm happened to visit. The optimality outcome similarly compares the reported assignment against all feasible assignments. Without these global claims, reaching a stopping situation would only show that the current search path has no remaining candidates. Balas (1965), pp. 526, 533
The result was proved in the 1965 paper. The work here is to state its algorithm and correctness claims in Lean and provide a target for a machine-checked proof; the submitted theorem files are open statements. The finite binary-program model, cost and slack functions, ceiling with infinity, and state-transition vocabulary can also support formal analyses of other exact enumeration procedures. The particular cancellation and backward-scan rules belong to Balas's algorithm. Balas (1965)
It is immediate that there are finitely many binary assignments. That alone does not show finite termination: the paper's step 5 may revisit earlier generated assignments, and the rules must prevent repeated work within one iteration as well as repeated generated assignments across iterations. It also does not justify pruning. When an improving set becomes empty, the remaining challenge is to show that no feasible assignment omitted by the search improves the ceiling. These are the separate claims recorded in parts (a) and (b), Lemmas 1–2, and Theorem 1. Balas (1965), pp. 529–533
Lean uses Fin n and Fin m for the paper's one-based index sets. A binary assignment is a Finset (Fin n). A general finite zero-one linear program is its own definition; problem adds the paper's standing assumption . There is no positive-size assumption on either index set. The algorithm stores generated assignments, each improving set as formed, cancellation snapshots, current cancellations, and its program point. Slack and cost are recomputed from the assignment by (6) and (21). Reachability is the reflexive transitive closure of the printed steps, and all milestone claims about states are restricted to reachable ones. The strict symbol means proper inclusion as the paper's footnote specifies. Balas (1965), pp. 523–525
The ceiling is represented in WithTop ℝ, with for . The cost tests (14), (17), (24), and (29) are written additively so they retain the paper's meaning when no feasible assignment has yet been generated. The improving set remains fixed after generation; the step-5 scan uses with the stored snapshot , as in (18). Step 1a cancels the cost-bound indices for every earlier assignment, and steps 6a and 7b resume the scan below the index just checked. The final tie break permits any index still tied after minimizing its cost. “In a finite number of iterations” is encoded as no infinite run plus a next step at each reachable non-stopped state. “No feasible solution” quantifies over all binary assignments. “Abandoned” is the predicate specified before Theorem 1: is abandoned when the algorithm is instructed to stop, or to check some with , including the indices step 5 passes over because their remaining improving set is empty. Lemma 2 reads either as the cancellations accumulated so far during iteration or as the cancellation records at the transition that obtains . Balas (1965), pp. 525–533
The paper prints in Theorem 1, but its algorithm and proof use the ceiling at the abandonment iteration, ; the Lean theorem states that corrected version and retains the original wording in the milestone record. A transition system that is stuck before a declared stopping situation, a ceiling encoded as a finite real sentinel, or a verdict quantified only over generated assignments would make the goal weaker than the paper's claim. Contributions toward the milestone proofs, state invariants, and reusable finite-search lemmas are in scope. The preliminary reduction of a general binary program to , the efficiency remarks, numerical examples, and the modified algorithm of Remark II are outside this mission. Balas (1965), pp. 519, 528–533
Minimizing a smooth function over a closed convex set is the basic problem of constrained continuous optimization. When the constraint set is simple enough that the nearest point of the set to any given point can be computed (a ball, a box, an orthant, an affine subspace), the most direct method is the gradient projection method: take a gradient step and project back onto the set. The method is the ancestor of the projected gradient and proximal gradient algorithms used today in signal processing, machine learning, and optimal control, where the variable is often a function, so that the natural setting is an infinite-dimensional Hilbert space rather than .
A. A. Goldstein's 1964 note in the Bulletin of the AMS (Goldstein 1964) is one of the two founding papers of the method, alongside the independent work of Levitin and Polyak (1966). It states, in a Hilbert space and with an explicit step-size window, that the iterates stay in the initial level set, that the objective values converge, and that under convexity they converge to the optimal value, with weak and strong convergence of the iterates under further hypotheses. Goldstein motivates the method by applications to control theory (Balakrishnan 1963; Goldstein, Minimizing functionals on Hilbert space, 1964).
Timeline.
Let be a real Hilbert space with inner product and norm . Let be closed and convex, and let be the projection onto : is the point of closest to . In Lean, IsProjection C P says that and for all .
Let , , and let
be the level set (levelSet f C x0). Let be an open set containing the convex hull of . Write for the Fréchet derivative of at applied to , for the gradient (so ), and
for the directional second derivative in the sense of Gâteaux (d2 f x h). The curvature hypothesis is that for some , at every and for every , these derivatives exist and
Choose and step sizes . The method is
A point is stationary if for every .
Assume is bounded below and continuous on . There is such that
The goal is the whole theorem, because its five parts share one limit and one standing setting.
The projection inequality for ; the Lipschitz property of ; the characterization of stationarity for convex at a differentiability point; the one-step Taylor estimate; the step lemma (for the new point stays in and the decrease is at least ); parts (i) and (ii); the strong-convexity bound on ; the supporting-hyperplane inequality of the proof of (iii); parts (iii), (iv) and (v). A companion item states the last clause of (ii) under convexity of on .
The result. The theorem gives a step-size rule that needs only a curvature bound near the level set, not a global Lipschitz constant of the gradient, and it covers the infinite-dimensional case directly: (iii) gives convergence of the objective values to the optimal value without assuming that a minimizer exists, (iv) yields minimizers as weak cluster points when the level set is bounded, and (v) gives strong convergence of the iterates under strong convexity on the level set. These are the prototypes of the convergence statements now proved for projected and proximal gradient methods.
Formalizing it. The result is classical and proved on paper; it has no machine-checked proof. The note is two pages long and its proof is terse ("The proof of (ii) being straightforward"), and checking it in Lean exposes two places where the printed statement needs repair (see Formalization scope). A complete development also produces reusable infrastructure: the variational inequality and Lipschitz property of the metric projection in a Hilbert space, a one-dimensional Taylor estimate from a Gâteaux second derivative along a segment, and weak lower semicontinuity of convex continuous functions on closed convex sets used through cluster points in WeakSpace.
The obvious argument for (i) applies a quadratic upper bound for along the segment from to . That bound is only available where the curvature hypothesis holds, on , and nothing guarantees in advance that , or the segment, lies in . Ruling this out requires control of up to the boundary of the level set, which the printed hypotheses do not give; this is where the added continuity hypothesis enters. In (iii) the iterates may be unbounded and no minimizer need exist, so compactness arguments are unavailable. In (iv) the cluster points are weak, so norm-closedness arguments do not apply directly.
[NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]. The inner product is ⟪x, y⟫_ℝ, and is Mathlib's gradient f.IsProjection C P; there is no chosen projection and no junk value.SecondDerivBound) states both differentiabilities before the bound, so the bound is never on a junk zero.IsGLB (f '' C) L. Weak cluster points are cluster points in WeakSpace ℝ H.Contributions welcome: proofs of any milestone, in particular the projection inequality and Lipschitz property (independent of the rest), the Taylor estimate from the Gâteaux second derivative, and the weak-closedness argument of (iv).
Backward stochastic differential equations (BSDEs) prescribe a process by its terminal value rather than its initial value: the unknown must be adapted to the information flow, yet must reach a given random variable at the horizon . They arise in mathematical finance (pricing and hedging, where is a contingent claim), in stochastic control (adjoint equations of the stochastic maximum principle) and in economics, where the stochastic differential utility of Duffie and Epstein (1992) defines the utility of a consumption stream as the solution of a backward equation.
Timeline:
Let be a complete filtered probability space satisfying the usual hypotheses: the filtration is right-continuous and contains every -null set. Let be an adapted process with right-continuous paths of bounded variation, , whose total variation process satisfies for a constant . Integrals are pathwise Lebesgue–Stieltjes integrals over .
The Doléans–Dade measure of is the finite measure on with
and is the space of jointly measurable processes with .
The data are a driver , jointly measurable, and a terminal value , subject to hypotheses 1–4:
The backward equation is the fixed-point problem for
When this is the Duffie–Epstein equation .
Under hypotheses 1–4 there is a progressively measurable process with càdlàg paths such that
is a semimartingale through the decomposition
and any two solutions in agree -almost everywhere.
In the order of the paper's argument:
Milestones 3–7 live inside the proof, after its reduction to nondecreasing .
The result. Theorem 2.4 gives well-posedness of a backward equation with no square-integrability and no Brownian structure: the filtration is arbitrary (subject to the usual hypotheses), the integrator may jump, and only first moments are required. In the case it settles the case of the Duffie–Epstein conjecture, so stochastic differential utility is well defined for integrable consumption data. The same fixed-point scheme, with the Doléans measure of a dominating process, is the basis of the coupled backward–forward result of §3 of the paper (a separate mission of this series).
Formalizing it. The theorem is proved in the literature but, as far as is known, has no machine-checked proof; Mathlib has conditional expectations, filtrations, martingales and Stieltjes measures, but no càdlàg process theory, no optional projection and no Doléans measure. A complete development produces these pieces. Its milestones also make precise points the paper leaves implicit: G is defined only up to versions, and the iterate bound is printed with in place of .
The obvious approach is to show that itself is a contraction on . It is not in general: the one-step bound is , and nothing makes . The argument must instead control the -th iterate. This needs exchanging a conditional expectation with a Stieltjes integral against a random measure, which is the optional projection identity (2.6). It also needs iterated integrals against an integrator with jumps, where the continuous-case identity fails and only the inequality survives. A second difficulty is measure-theoretic: is defined only almost surely for each fixed , and the norm sees the whole path. A version must be chosen with càdlàg paths before the equation even makes sense in .
BVIntegrator carrying with its Jordan decomposition as data, tied to Mathlib's eVariationOn so that . are Stieltjes measures of the paths.Many estimation problems in statistics, machine learning and signal processing minimize a smooth loss plus a nonsmooth ℓ1-type regularizer: the lasso, basis pursuit, least absolute deviations, Huber fitting, the group lasso, and ℓ1-penalized maximum likelihood for Gaussian graphical models. Chapter 6 of Boyd, Parikh, Chu, Peleato and Eckstein, Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers (Found. Trends Mach. Learn. 3(1), 2011), shows that the alternating direction method of multipliers (ADMM) splits each of these problems into a step that touches only the loss and a step that touches only the regularizer, and that each step has a closed form. The practical value of ADMM on these problems rests entirely on those closed forms: an iteration is one cached linear solve, one projection, or one thresholding.
The capstone is sparse inverse covariance selection (§6.5), the ℓ1-penalized Gaussian maximum-likelihood problem of Banerjee, El Ghaoui and d'Aspremont (2008), also solved by the graphical lasso of Friedman, Hastie and Tibshirani (2008). Its ADMM X-update minimizes a log-determinant objective over positive definite matrices, and the book shows that it is solved exactly by one symmetric eigenvalue decomposition.
All vectors are real and is the Euclidean norm. For the soft thresholding operator is if , if , and if , applied componentwise to vectors and entrywise to matrices. The vector soft thresholding operator on is , with . The Huber penalty is for and for , summed over components for vectors.
In scaled-form ADMM for minimizing subject to , with penalty and scaled dual variable , the updates are
followed by . "The update is given by formula " means is the unique minimizer of the corresponding subproblem.
For sparse inverse covariance selection, is symmetric (the empirical covariance), is the regularization weight, , , and is the set of symmetric positive definite matrices, the domain of . ADMM alternates
and .
Let and be symmetric, , and with . Then
is positive definite and is the unique minimizer of over .
The closed forms are what make ADMM competitive on these problems. For the lasso the x-update is a ridge regression whose factorization is computed once; for basis pursuit it is a cached projection; the ℓ1 step is a componentwise threshold. For covariance selection the X-update costs one eigenvalue decomposition, and the book (p. 46) cites Scheinberg, Ma and Goldfarb (2010) as showing that ADMM outperforms state-of-the-art methods on this problem. The goal also yields that is always positive definite, so the iterates remain in the domain of without a line search.
All statements here are classical and their proofs are elementary convex analysis and linear algebra. A search of the platform found no machine-checked version of any of them. Formalizing them produces verified proximity operators (soft thresholding, vector soft thresholding, Huber, projection onto an affine set) and a verified matrix-function argument for that later missions on ADMM, proximal methods and Gaussian graphical models can import.
The vector updates reduce to separable one-dimensional problems or to a normal equation, and the difficulty there is bookkeeping: uniqueness, the case of vector soft thresholding, and the three regimes of the Huber prox.
The goal is harder. The book's argument says that satisfies the gradient equation "and thus minimizes the X-minimization objective". Checking the equation is algebra; the claim to be proved is minimality over the open cone , which needs the convexity (indeed strict convexity, for uniqueness) of on positive definite matrices and the identification of its gradient with along symmetric directions. Mathlib has determinants and positive definiteness; a usable convexity statement for on is not among the platform's published results. Showing that satisfies (6.5) alone does not establish the goal.
EuclideanSpace ℝ (Fin n), matrices Matrix (Fin m) (Fin n) ℝ acting by Matrix.toEuclideanLin. The Frobenius norm and the entrywise ℓ1 norm are written as explicit sums, not through Mathlib's matrix norm instances. The vector ℓ1 norm is the platform definition HighDimStat.SparseLinear.l1Norm.IsUniqueMinimizerOn). Iterates are not defined; the subproblem's data (, , ) are arbitrary.Matrix.PosDef only. Singular or indefinite matrices are never competitors, so Real.log of a nonpositive determinant plays no role.lam and μ.Real.log of nonpositive determinants, is not the book's claim; the goal states unique minimality over .Contributions welcome: convexity and strict convexity of on and its derivative; a general "prox of a separable function is componentwise" lemma; and the projection onto an affine set.
A discrete-event simulation of a queue, an inventory system or a communication network produces an output process , and the quantity of interest is usually its steady-state mean , the long-run average of . The natural estimator is the time average of a run of length . A confidence interval for needs the scale of the fluctuations of , the variance constant of the central limit theorem . For correlated simulation output, is a sum of autocovariances at all lags and is hard to estimate consistently.
The method of standardized time series (STS), introduced by Schruben (Schruben 1983), avoids estimating : it divides the centred time average by a functional of the whole observed path that scales like , so that cancels. Batch means, the standardized sum, and the standardized maximum are all of this form.
Glynn and Iglehart (Glynn & Iglehart 1990) put the method on a general footing. They require only a functional central limit theorem (FCLT) for , and they identify an abstract class of standardizing functionals for which the cancellation works. This mission formalizes their basic limit theorem, Theorem 2.4, and the four claims of its proof. Two companion results of §2, display (2.2) and the weak law , are included as further targets.
is the space of continuous real functions on with the uniform norm and its Borel -algebra; is the identity path . For , is the discontinuity set of , the set of at which is not continuous. A standard Brownian motion on a probability space is a random element of with Gaussian finite-dimensional laws, and .
The output is a real-valued measurable process. Its scaled partial-integral process and its centred, rescaled version are
Assumption (2.1) asks for finite constants and such that as , weak convergence of random elements of . It holds for -mixing, strongly mixing, associated and regenerative output processes, among others.
The class of (2.3) consists of the measurable with
The proof uses the auxiliary map for and otherwise.
For every , under Assumption (2.1),
and .
Theorem 2.4 is the limit theorem behind every STS confidence interval. The limit is free of and of the output process, so with chosen so that equals a prescribed level, the interval has asymptotically exact coverage for . Each choice of gives a method: batch means with a fixed number of batches, Schruben's standardized sum, the standardized maximum. The later sections of the paper compare the lengths of these intervals with those of consistent-estimation intervals, and those comparisons start from Theorem 2.4.
The theorem is classical and its proof is short on paper. What is missing is a machine-checked version. The formal proof needs a continuous mapping theorem for maps that are continuous only almost surely at the limit, on the non-locally-compact space ; Mathlib has the version for continuous maps only. A formal Theorem 2.4 also makes the class and the C[0,1]-valued FCLT available for the other results of the paper, the expected-length lower bound and its non-attainment, which are formalized in sibling missions.
The algebra (milestones 3 and 4) is elementary. The difficulty is the continuous-mapping step. The map is in general not continuous: it can be discontinuous wherever is and wherever vanishes, and itself may be discontinuous on a large set (the standardized maximum is). The continuous mapping theorem for continuous maps does not apply. One needs its almost-sure form: if and , then . The class controls only along the law of , and the hypothesis of the almost-sure theorem is about at the scaled limit , so the conditions (2.3iii) and (2.3iv) have to be transported from to and from to .
is C(unitInterval, ℝ) with its sup-norm topology; the Borel MeasurableSpace instance is declared in the mission's definition file, since Mathlib has none at this commit. Weak convergence is Mathlib's TendstoInDistribution, for the -valued FCLT and for the real-valued conclusions. The standard Brownian motion is a measurable -valued map whose coordinates agree, for every , with a process satisfying Mathlib's IsBrownianReal. is the set of points where ContinuousAt g fails, and is an outer measure, so no measurability of is assumed.
is a -valued parameter pinned pointwise by , so it is determined by . Assumption (2.1) carries joint measurability of and local integrability of each path; the second is implicit in the paper and makes defined. The index runs over , and milestone 4 assumes because (2.3i) is applied with . Real division by zero returns in Lean, which agrees with the paper's convention for ; it matters only on events of probability zero in the limit. Condition (2.3iii) is printed "" and is read as .
Condition (2.3iv) is stated with the discontinuity set, not as continuity of : requiring continuous everywhere would exclude the standardized maximum of Example 3.10 and would make the continuous-mapping step trivial. The goal assumes nothing about , or any mapping theorem; these appear only in the milestones.
Contributions welcome: the almost-sure continuous mapping theorem for TendstoInDistribution on a metric space (reusable well beyond this mission), the cone property of under positive homogeneity, and evaluation at a point as a continuous map on . Mathlib does not yet construct a Brownian motion with continuous paths as a -valued random element, so the hypotheses cannot be instantiated inside Lean; this is a hypothesis on , not a vacuity.
The cutting stock problem asks how to cut standard stock rolls of length into pieces of demanded lengths so that the demands are met at least cost. Gilmore and Gomory solved its linear programming relaxation by column generation (Part I, Opns. Res. 9 (1961)): every cutting pattern is a column, and the column to bring into the basis is found by solving an integer knapsack problem whose objective is given by the current dual prices. In Part II (Opns. Res. 11 (1963)) they replaced the dynamic-programming knapsack solver of Part I by a lexicographic enumeration with a bound test, the Knapsack Method, and reported it to be about five times as fast as dynamic programming on their problem set (p. 866). The method is an early enumeration-with-bounds (branch-and-bound type) procedure for the integer knapsack, and the same pricing problem remains the inner loop of column generation for cutting stock, bin packing and their many variants.
There are demanded lengths with linear programming prices , and standard stock lengths with costs . A column for is a vector of nonnegative integers with . The knapsack problem (1) for is
and the quantity to compute is : a column improves the linear program exactly when .
For a prefix write and . Step (1) sorts the data, and , and appends a slack item with , . The method then generates vectors in decreasing lexicographic order:
In Lean the method is a transition system Step on states (a, s, t, M, phase). Reachable means reachable from the start state of Step (2).
Under Step (1)'s ordering, with and :
and at the end every is or the price of a column for , with . With one stock length () this is the paper's correctness claim in full: the method solves the knapsack problem (1).
The goal certifies the pricing oracle of the Gilmore–Gomory column-generation method: the knapsack solver it calls returns the true optimum. The pricing step is exact only if that holds, and so is the conclusion "no improving column exists, the LP is solved". Milestones 1–4 are reusable on their own. They are the textbook ingredients of lexicographic and depth-first branch-and-bound for the integer knapsack: the greedy completion, the density-ordered LP bound, and the pruning rule.
The paper's argument is a short paragraph, "clear from the order in which the -vectors are generated". Writing it out shows that the claim is false for several stock lengths as the steps are printed. With , , and , the method tests . The test of Step (5) at then fails for only because , Step (6) stops, and the run ends with while the column has price 2. This mission therefore states what the printed algorithm does achieve. The result is the full claim for and for the longest stock length in general. A sorry-free Lean proof of the counterexample run accompanies the mission. No part of the method or its correctness has been formalized before, as far as a search of the platform shows.
The method skips large parts of the lexicographic order in three ways:
Each skip has to be justified by a bound that holds for every vector skipped, and the justifications interact. A skipped vector may fit a longer stock length but not , and the bound for must cover exactly those vectors. The invariant that survives all three moves is not the naive "every vector above the current one has been examined": the vectors are not examined, only bounded. Termination needs the lexicographic decrease together with finiteness of the fitting vectors, and progress needs the reachability invariants and that make Step (5) meaningful.
Items are Fin m from 0. The paper's level is a natural number, and the prefix is the coordinates with index < s. Stock lengths are Fin k, and is index 0. The slack item enters only through and at . The lexicographic order is Mathlib's Pi.Lex, and is Nat.floor.
is the predicate IsKnapsackMax, never a real supremum, which would be 0 on an empty set. The algorithm's output is never defined as the maximum. The goal includes termination and progress, so its correctness clause is not vacuous. Every invariant is stated for reachable states only.
The goal adds two disclosed hypotheses:
Step (1) is a hypothesis on the data, not a step.
The goal also makes these corrections:
Not formalized:
Contributions welcome: proofs of the milestones, and a corrected multi-length variant of the method with a proof that it computes every .
Many large optimization problems arising in statistics, machine learning, signal processing and resource allocation have an objective that is a sum of terms, each depending on data held by a different processor, or a coupling term that depends on the sum of the agents' decisions. Chapter 7 of Boyd, Parikh, Chu, Peleato and Eckstein's monograph on the alternating direction method of multipliers (ADMM) (Found. Trends Mach. Learn. 3(1), 2011) introduces two templates that turn such problems into distributed algorithms: consensus and sharing. Nearly every distributed application in the rest of the monograph (distributed lasso, distributed logistic regression, splitting across examples and across features in Chapter 8) is an instance of one of the two. Consensus problems in the context of ADMM go back to Bertsekas and Tsitsiklis (Parallel and Distributed Computation, 1989).
The value of the templates lies in a handful of exact algebraic facts about the ADMM subproblems: the global update is an average, the dual variables average to zero, and the sharing update, which looks like a problem in variables, is really a problem in variables. These facts are what this mission formalizes.
There are agents. Vectors live in with the Euclidean inner product, and an overline denotes an average over agents, . Each local cost and the shared cost are functions into . The penalty parameter is .
Global variable consensus (§7.1) is the problem
with local variables and a global variable . ADMM alternates a parallel -update, an averaging -update and a dual update of the multipliers . With a regularizer added (7.2), the -update (7.4) becomes a minimization involving .
General form consensus (§7.2) lets local variable copy only some entries of : entry of corresponds to entry , and is defined by . The number of local entries copying is .
Sharing (§7.3) is the problem
written for ADMM with copies of the (7.12). In scaled form, with , its -update is
followed by .
For every : solves the -variable -update iff solves
and
and along every run of sharing ADMM,
so all scaled dual variables agree after one step.
The reduction is what makes sharing ADMM scale: the central step needs only the averages , and one -dimensional proximal problem, regardless of the number of agents, and the dual state collapses to a single vector. The same reduction underlies exchange ADMM (§7.3.2) and the splitting-across-features algorithms of §8.3. The consensus facts explain why the fusion center only averages and why the dual variables can be dropped from its update.
All results of the chapter are proved, informally, in the monograph; they are elementary. To our knowledge none has a machine-checked proof. The mission produces checked statements of the update formulas that later chapters of the series and distributed-optimization developments can cite instead of re-deriving.
The statements are exact identities between minimizer sets of nonsmooth problems in which may be any extended-real-valued function: there is no first-order condition to use, so each step must be argued by comparing objective values, and the iff requires producing, for an arbitrary competitor, a competitor of the reduced problem with no larger value. The index bookkeeping is the other half: averages of sums of sequences indexed by agents and by iterations, the off-by-one in "after the first iteration", and in §7.2 sums over the fibres of an index map between local vectors of different dimensions.
EuclideanSpace ℝ (Fin n); agents are indexed by Fin N, so the book's is Lean's ; components are 0-based as well.lam), for every global index in §7.2, and the index ranges for and for (the starting is arbitrary).In two-stage optimization under uncertainty, a first-stage decision is taken before the data are known, and a second-stage decision is taken after a scenario is revealed. The fully adaptive formulation lets depend on and minimizes the worst-case cost. It is the natural model of recourse, but it optimizes over policies, one decision per scenario, and is computationally hard in general. The static robust formulation fixes one in advance that must be feasible in every scenario. It is a single deterministic mixed integer program and is the standard tractable surrogate (Ben-Tal, Goryashko, Guslitzer, Nemirovski 2004; Bertsimas & Sim 2004).
The question is how much is lost by the surrogate. Bertsimas and Goyal (2010) bound the gap by against the stochastic problem and by against the adaptive problem when the uncertainty set is symmetric. Their §5.3 identifies a case with no gap at all: when the uncertainty set is a hypercube (a box), the static robust optimum equals the adaptive optimum, and this holds even when the constraint matrices themselves are uncertain. Box uncertainty is the simplest and most common uncertainty model in practice (interval data on every coefficient), so the result says that for it, adaptivity buys nothing.
This mission formalizes that theorem, Theorem 5.4, together with Theorem 2.4, which shows that under right-hand-side uncertainty the robust problem is a single deterministic problem with the coordinatewise worst right-hand side.
Fix dimensions and sets of integer coordinates. The decision domains are
which is up to relabelling coordinates, .
A scenario set is given. In scenario the data are a constraint matrix , a recourse matrix , a right-hand side and a second-stage cost . The first-stage cost is fixed.
The uncertainty set is , a subset of with . Following Definition 1.1, is a hypercube if for some .
For Theorem 2.4, , and are fixed and only varies; (1.2) is the robust problem above, and is the deterministic problem with right-hand side .
If is a hypercube, then
The integer coordinates are arbitrary, and nothing is assumed about the signs of , , .
The result. Theorem 5.4 says that for interval uncertainty on every coefficient, the static robust program, whose size does not grow with the number of scenarios, solves the adaptive problem exactly. Combined with Theorem 2.4 for right-hand-side uncertainty, the adaptive problem collapses to one deterministic mixed integer program with worst-case data. It marks the boundary case of the paper's adaptability-gap bounds: the gap is at most for symmetric sets, and exactly for boxes.
Formalizing it. The result is proved in the paper; to our knowledge it has no machine-checked proof. The mission produces a Lean model of two-stage robust and adaptive mixed integer programs with uncertain constraint matrices, with values as extended-real infima, which other formalizations of adjustable robust optimization can build on.
The mathematics is elementary; the care is in the statement. The step that fails for a general uncertainty set is the existence of a single worst scenario that is simultaneously entrywise smallest in , and entrywise largest in , . For a set that is only contained in a box, the box's worst corner need not be realized. With two scenarios and , , , the adaptive value is and the robust value is . A formalization therefore has to state the hypercube hypothesis as an equality of sets. A second point is the arithmetic of extended reals: the paper argues from optimal solutions, which need not exist, so the inequalities must be transported through infima over feasible sets that may be empty and through suprema that may be infinite.
Fin n → ℝ; matrices are Matrix (Fin m) (Fin n) ℝ; constraints use Mathlib's componentwise order and mulVec.EReal infima over the feasible set, when infeasible; worst-case costs are EReal suprema over . No optimal solution is assumed.IsHypercube (uncertaintySet A B b d), i.e. the realized data are exactly a box. Assuming only that the data lie inside a box would make the statement false (example above); assuming fixed , would state Corollary 5.1 instead of Theorem 5.4.Contributions welcome: proofs of the milestones and of the goal, and lemmas on monotonicity of mulVec for nonnegative vectors and on EReal infima over feasible sets, which are reusable across the other missions of this series.
In just-in-time scheduling each job has a preferred time, and finishing it early is as undesirable as finishing it late. Garey, Tarjan and Wilfong (Math. Oper. Res. 13 (1988), 330–348) study the one-processor version in which task has a length and a preferred starting time , and the discrepancy of a task started at time is . The penalty is symmetric: earliness and tardiness cost the same. The paper shows that minimizing the total discrepancy is NP-complete, gives an algorithm for a fixed task order, and, in §3, gives an efficient algorithm for minimizing the maximum discrepancy : a linear-time test for a given bound after an sort, combined with a search over .
This mission formalizes the structural core of §3: the normal-form theorems (Theorem 4, Corollaries 1 and 2) on which the paper's algorithm for maximum discrepancy is built. The two companion missions of the series cover the NP-completeness result (THEOREM 1) and the fixed-order algorithm (THEOREMS 2 and 3).
Fix a bound . A schedule has maximum discrepancy at most exactly when every task starts no earlier than its release time and finishes no later than its deadline (p. 342). These release times and deadlines are in special form: with , for every task
From here on the data are arbitrary reals , , in special form for some .
A schedule is an execution order ( is the task in position ) with starting times , such that a task finishes no later than any later-positioned task starts: for . It is feasible if and for every . Its makespan is , and it is optimum if it is feasible and no feasible schedule has a smaller makespan.
Let be a task of largest deadline. A schedule has the release time property if every task executed after has release time strictly later than the starting time of . When the tasks are indexed with , a schedule is in standard form with split index , , if it begins with an optimum schedule of , followed by started at the maximum of and the completion time of that first part, followed by in this order without idle time.
Two companion items state the reformulation of the maximum-discrepancy bound as release times and deadlines, and the special form with .
Corollary 2 reduces the search for an optimum schedule of to candidates, one per split index, each assembled from an optimum schedule of a shorter prefix. This is the dynamic program of §3.2, which the paper implements in time after an sort; combined with a search over it minimizes the maximum discrepancy. Without the special form, deciding whether one processor can meet arbitrary release times and deadlines is NP-complete (reference [4] of the paper, Garey and Johnson 1979), so the normal form is what separates the tractable case from the general one.
The results are proved in the paper; no machine-checked proof of them is known on Prove2Me. A formal proof of Corollary 2 would certify the correctness of the split-index recursion and, together with the companions, of the reduction from maximum discrepancy to this release-time/deadline problem.
The obvious argument fails in Theorem 4. Exchanging a straggler (a task after released no later than starts) with shifts the tasks between them, and for general release times and deadlines those tasks can become infeasible. The paper's argument uses the special form at every step: a task released after starts has , hence exactly, and this equality is what bounds how far tasks may move. It also needs an extremal choice of the optimum schedule (fewest tasks after , then fewest tasks between and the first straggler), which requires showing that optimum schedules exist over the reals. The passage to standard form then combines this with an earliest-deadline exchange for the tasks after and the replacement of the first part by an optimum sub-schedule without losing feasibility of the later tasks.
Tasks are indexed by Fin N (0-based: the paper's are ; the paper's in Corollary 2 is the index ). All data are real. A schedule is a permutation σ : Fin N ≃ Fin N with starting times s : Fin N → ℝ; "executed before/after" refers to σ, not to a comparison of starting times, because zero-length tasks may share a starting time. Execution intervals meet at most at endpoints. The makespan is a supremum over Fin N; "optimum" quantifies over all feasible schedules, not only standard-form ones.
The standing hypotheses on every structural item are , , (from , the in , and nonnegative lengths); since , start times are nonnegative, as the paper assumes throughout. The special form is a hypothesis of every structural item and cannot be dropped. The paper's dummy task () is not a task; an empty first part completes at time . Corollary 1's "the set of all tasks with deadline or less" is read as excluding , the only reading under which it is true. The page's "(which can be assumed optimum)" is part of the standard form. The deadline-split and release-before-finish milestones are stated for every feasible schedule, as their arguments allow.
A trivializing formalization is excluded: the standard form pins 's start to and the later tasks to consecutive positions in index order, so the goal is not Corollary 1 restated with an unconstrained split.
Running times (, ) and the algorithm of §3.2 are out of scope. The development needs only finite permutations, finite suprema and the exchange arguments of §3.1; the existence of an optimum schedule (minimum makespan over finitely many orders, earliest-start schedules) is reusable for other single-machine problems with release times and deadlines. Proofs of any milestone, and a sorry-free proof of the existence of optimum schedules, are welcome.
The residual life time of a lifetime at age is the remaining life given survival past . Its distribution at great age is a basic object in reliability, insurance and the statistics of extremes: excess-of-loss reinsurance prices the part of a claim above a retention level, and peaks-over-threshold methods fit a model to the observations exceeding a high level. Balkema and de Haan (Residual Life Time at Great Age, Ann. Probab. 2 (1974), 792–804, doi:10.1214/aop/1176996548) determined every possible limit law of the suitably normed residual life time as and the domains of attraction of these laws; Pickands (1975) obtained the continuous part of the same picture, which is the probabilistic basis of the generalized Pareto approximation used in practice.
Limit theorems describe the behaviour only as . Section 4 of the paper gives approximation results for finite . In extreme-value theory, von Mises (1936) gave a sufficient condition for attraction to the Fréchet law : . Theorem 6 of the paper is a non-asymptotic, two-sided counterpart for the residual life time: two-sided bounds on the scaled hazard rate give two-sided bounds on the residual life distribution at every age past a threshold. This mission formalizes Theorem 6 (p. 801).
Let be a real random variable with law and distribution function . For an age with , the residual life distribution function is
which is for . For the residual life scaled by the age has distribution function .
For the Pareto-type law is
It is the law of when for . has a positive density for if is differentiable at every with derivative . The quantity is the hazard rate of at , and is the hazard rate scaled by the age.
Let have a positive density for , and let satisfy for . Then for all and all real ,
The smaller constant gives the lower bound: a smaller scaled hazard rate means a heavier tail and hence a larger chance that the remaining life is long. For a Pareto tail one may take , and both inequalities are equalities.
For and ,
The theorem turns a pointwise condition on the hazard rate, which can be checked on a density, into a bound on the whole conditional distribution of the residual life, valid at every age rather than only in the limit. If moreover , then can be taken arbitrarily close to for large , which recovers the convergence with an explicit error at finite ages. Such bounds are what a practitioner fitting a Pareto tail above a threshold needs to quantify the approximation.
The result is classical and its proof is short; it is not open. As far as is known, no machine-checked version exists, and Mathlib has no theory of residual life distributions or of the limit laws of Balkema and de Haan. A formal proof would provide reusable pieces: the identity between the integrated hazard rate and for a distribution function with a density, and the comparison of a residual life distribution with a Pareto law. The other missions of this series formalize the paper's limit theorems, for which this mission's objects (the residual life distribution and ) are shared.
The mathematics is elementary; the work lies in the regularity bookkeeping that the printed proof leaves implicit. The density is only assumed to exist pointwise, so the fundamental theorem of calculus must be applied to with a derivative that is not assumed continuous, and its integrability on has to come from the hazard bounds themselves. That stays positive, that , and that the case is trivial all have to be derived from the hypotheses rather than assumed. Finally, the conditional probability must be identified with , where , through the measure of intervals.
The law of is a probability measure on , and is Mathlib's ProbabilityTheory.cdf μ. The probability is residualLife μ t (x * t) . is a real function defined by cases, with Real.rpow for the power. The density is an explicit function with having derivative at every , the derivative taken within . This is a right derivative at and the ordinary derivative for . It is the weakest reading of "positive density for ", and it admits the exact Pareto law with , whose distribution function has no two-sided derivative at . The bounds are stated for with Lean's real division.
No hypothesis is added to the printed theorem, and no printed slip was found. The conditions and follow from the hypotheses: for the ratio is not , and a positive derivative on makes strictly increasing there. Lean's convention therefore never acts at the ages concerned. The conclusion is stated for all real , as printed; for all three quantities are . The milestone does not assume the hazard rate integrable: it is bounded and measurable on , and a non-integrable integrand would make the inequality false rather than trivially true. A formalization that dropped the density hypothesis, replaced by deriv without differentiability, or let the bounds hold only on a set not containing every would not be this theorem; all three are excluded by the statement.
A proof needs the fundamental theorem of calculus for derivatives within a half-line (in Mathlib), the identity , and the chain rule for . Proofs of the milestone and the goal are welcome, as are sorry-free lemmas showing that is a distribution function and that the Pareto law satisfies the hypotheses with .
PERT (Program Evaluation and Review Technique) and the critical path method model a project as a directed acyclic network whose arcs are jobs and whose nodes are events; the duration of the project is the length of a longest path from the origin to the terminal. When job durations are random, the quantity a planner wants is the expected duration. Computing it exactly requires solving one longest-path problem for every joint outcome of the job durations: with jobs each taking two values, deterministic problems. Classical PERT practice replaced every random duration by its mean and reported the longest path for the mean durations. That figure is known to be optimistically biased.
D. R. Fulkerson, Expected Critical Path Lengths in PERT Networks (RAND Memorandum RM-3075-PR, 1962; Operations Research 10(6):808–817, 1962, doi:10.1287/opre.10.6.808), proposed a second estimate, computed node by node with work exponential only in the size of a single node's bundle of incoming arcs, and proved that it lies between the classical mean-length figure and the true expectation.
A project network has events with , origin and terminal . Its arcs are ordered pairs with , at most one per pair, and every event lies on a directed path from the origin to the terminal. Fulkerson numbers his nodes ; his node is event here. The bundle of an event is the set of arcs entering , and the set of their tails; the origin's bundle is empty.
For arc lengths , let be the length of a longest (critical) path from the origin to ; equivalently and .
The lengths of the arcs of each bundle form a random vector with a finite distribution: a finite set of bundle vectors , where is the length of arc , with probabilities summing to . Arcs within a bundle may be correlated; distinct bundles are independent, so an assignment of one bundle vector per event has probability . Three numbers are attached to each event :
In the order of Fulkerson's induction (pp. 10–12):
The chain (4.4) says that the classical PERT estimate never overstates the expected project duration, and that the numbers are a lower bound at least as tight. The computation visits each node once and sums over the support of that node's bundle only, so its cost grows exponentially with bundle size rather than with network size, while the exact expectation requires the whole product space. The Fig. 4.2 example shows that the bundle-independence hypothesis cannot be dropped for the upper inequality, while the lower inequality survives arbitrary dependence.
The result has a complete published proof. This mission seeks a machine-checked proof of (4.4) for finite distributions, with the longest-path characterisation of the earliest-event-time recursion and the locality of critical path lengths as reusable lemmas, and machine-checkable versions of the paper's numerical examples, including the counterexample showing the role of independence.
The left inequality compares an average of maxima with a maximum of averages. The right inequality requires more: averages over the bundle entering , while averages over assignments to every bundle. Taking expectations in yields , which gives the weaker bound . Fig. 4.2 shows that can fail when the bundles are dependent. In Lean, is a sum over a dependent product of finite supports (Fintype.piFinset); its interaction with the local recurrence for is the central technical difficulty.
CriticalPath.Events.ProjectNetwork (Kelley–Walker 1959): events Fin (n + 1), arcs a Finset of ordered pairs with strictly increasing labels, origin preceding and terminal following every event. This requires . Fulkerson's numbering condition "" on p. 3 is read as the strict (arcs join distinct nodes of an acyclic network). There is one arc per ordered pair, Fulkerson's own convention in (3.13).CriticalPath.Events.earliest, a recursion with Finset.sup' over the nonempty set of incoming arcs. This is the paper's convention that terms of missing arcs are ignored. Nothing uses a default value of or .Finset and a weight function per bundle) plus a predicate IsProb (nonnegative weights on the support, summing to , for every event including the origin). Bundle vectors are functions on all events, and coordinates outside are never read.Infrastructure that a full development needs, and that is reusable elsewhere, includes the longest-path characterisation of the earliest-event-time recursion, the locality lemma, and the factorisation of sums over Fintype.piFinset along one coordinate. Proofs of any milestone or companion are welcome. Out of scope here: §5 (computational examples) and the general-network analogues of §6.
A task may have a preferred execution time because a material delivery, external event, or downstream operation is timed to it. Starting early can be as costly as starting late. Garey, Tarjan, and Wilfong study this situation on one processor, where tasks cannot overlap but idle time between tasks is permitted. Their total-discrepancy problem is hard when the execution order is free; fixing the order leaves a substantial timing problem because each start can still move and can force changes to earlier starts. The paper gives an explicit scheduling procedure for that case and proves that it minimizes the sum of deviations from preferred starts (Garey, Tarjan, and Wilfong, 1988, §§1–2).
This mission targets that procedure and its correctness theorem. It also records the paper's equal-length result: when task lengths are identical, a minimum-cost schedule exists in preferred-start order, so the fixed-order procedure applies after sorting. These are two precise claims about total discrepancy, distinct from the paper's separate maximum-discrepancy problem.
There are tasks, indexed . Task has a nonnegative length , a nonnegative preferred starting time , and an actual starting time . Once started, it occupies the one processor until . Each start must be nonnegative. For the fixed-order problem, task must finish before task starts, so . This permits idle time when the inequality is strict. The task's discrepancy is ; because its preferred completion is , this is also its absolute completion-time discrepancy. The total discrepancy is
A block is a maximal consecutive set of tasks with no idle time between neighboring tasks. Within a block, Decrease counts tasks whose actual starts are later than preferred, and Increase counts tasks whose actual starts are no later than preferred. These names describe the effect of moving the entire block earlier: the discrepancy of a Decrease task falls initially, whereas that of an Increase task rises. The algorithm's state is a schedule for the first tasks. It inserts the next task at its preferred start when the previous task has finished, and at that finish time otherwise. In the latter case it may move the final block earlier until one of the paper's stopping events occurs: the block reaches time zero, a late task reaches its preferred start, or the block meets its predecessor (§2.2, p. 337).
For the equal-length result, schedules may execute tasks in any order. Two distinct tasks are feasible together when one completes before the other starts; meeting at endpoints is allowed. The objective remains the same sum of absolute discrepancies.
The main target is the paper's Theorem 2. For all nonnegative task data and every , the actual schedule produced by the block-shifting algorithm is feasible and satisfies
This includes the empty schedule and schedules with idle time. The milestone list follows the paper's own assertions: a balanced final block can move earlier without changing cost; every block of has more Increase tasks than Decrease tasks or begins at zero (Lemma 7); and the two claims in Case 2 of the proof record the cost of adding a late task and the comparison with schedules that place it earlier (Theorem 2 and Lemma 7, p. 338).
The companion target is Theorem 3. If every task has a common length and the preferred starts are indexed so that , then among all feasible schedules, including those with another task order, at least one minimum-cost schedule starts the tasks in index order:
The paper uses this statement to connect free-order equal-length scheduling to its fixed-order procedure (Theorem 3, p. 340).
Theorem 2 certifies an explicit schedule, not just the existence of an optimum. It fixes the objective value for a prescribed execution order and gives a baseline against which any other legal timing of the same tasks can be compared. Theorem 3 supplies the ordering fact needed to use that result when all lengths agree. Together they explain why a problem that is difficult for unrestricted task lengths still has these structured solvable cases (Garey, Tarjan, and Wilfong, 1988, abstract and §2.5).
The paper proves both theorems on paper. The work here is to formalize its schedule construction, cost, block boundaries, and comparison classes in Lean, then obtain machine-checked proofs of the stated targets. The draft theorem declarations compile with proof placeholders; this proposal does not claim that they are already machine-checked results. A completed development would make the model and the algorithm available for later formal work on scheduling with idle time and symmetric earliness and tardiness penalties.
Moving a task closer to its preferred start can move neighboring tasks farther from theirs. A simple task-by-task choice therefore does not establish global optimality. Nor does a count of late and early tasks in one block, by itself, justify arbitrary earlier movements of individual tasks. The difficult comparison in the paper is between the algorithm's schedule and a competing feasible schedule whose new task starts earlier: the whole final block and its constrained relative movements matter. The proof also has to account for the boundary at time zero and for blocks that merge when shifted. These are the reasons the explicit procedure and its block invariant need careful statements (§§2.2–2.3, pp. 337–338).
The Lean development represents task data and starts as functions from natural-number indices to real numbers; only indices below count. Task in Lean is the paper's . Preferred times, lengths, and legal starting times are nonnegative. The start-time condition is a standing convention used by the paper's algorithm, especially its zero-boundary stopping rule. Fixed-order feasibility requires successive tasks to be separated by at least the earlier task's length; unrestricted feasibility uses pairwise nonoverlap. An empty schedule is legal and has cost zero. The representation allows zero-length tasks, as does the paper's model.
The algorithm is defined by its stated insertion and single-block-shift operations. Defining as a chosen minimizer would erase the content of Theorem 2; the goal also explicitly asserts feasibility so that an illegal low-cost function cannot qualify. Theorem 3 compares with every feasible unrestricted-order schedule, not just schedules already in preferred-start order. The core definitions, the block invariant, and the cost comparisons are useful beyond this particular proof. Formalizing the paper's running-time bounds and heap implementation is outside this mission.
3SUM asks whether three distinct positions in a list of integers contain values summing to zero. It is a central problem in fine-grained complexity.
This mission formalizes a deterministic algorithm for 3SUM on polynomially bounded integers, on a word RAM with -bit words. Alman and Vassilevska Williams's 2026 breakthrough gives a truly subquadratic bound, refuting the integer 3SUM hypothesis in this model.
The mission uses the accompanying Lean specification and shares the Exact Triangle milestone with Truly Subcubic APSP on a Word RAM.
Theorem_22_3SUM.Many network optimization algorithms spend most of their time in a heap (priority queue): a set of items with real keys that supports inserting an item, finding and deleting an item of minimum key, melding two heaps, decreasing the key of an item, and deleting an arbitrary item. Dijkstra's shortest-path algorithm performs at most one delete min per vertex and may perform a decrease key for each edge, so on a graph with vertices and edges its running time is governed by how cheap decrease key is. Binomial queues support the heap operations in worst-case time.
Fredman and Tarjan (J. ACM 34 (1987)) introduced Fibonacci heaps (F-heaps), in which delete min and delete take amortized time and every other operation, decrease key included, takes amortized time. This brings Dijkstra's algorithm to and improves the best bounds then known for all-pairs shortest paths, weighted bipartite matching (the assignment problem) and minimum spanning trees. F-heaps descend from the binomial queues of Vuillemin (1978) and use the potential technique of amortized analysis of Sleator and Tarjan. This mission formalizes the paper's §2 analysis, culminating in THEOREM 1 on p. 604.
An F-heap is a list of heap-ordered rooted trees: every child's key is at least its parent's key. Each node holds an item, the item's real key and a mark bit; the children of a node are kept in the order in which they were linked to it, earliest first. The rank of a node is its number of children. A collection is a list of heaps, named by position; a run starts with no heaps.
Linking two trees with roots and makes the last child of if the key of is smaller, and otherwise makes the last child of ; the root that becomes a child is unmarked. The operations act as follows:
The actual time of an operation is one unit, plus one per linking step, plus one per cut, plus for delete min the scan of the rank array (the largest rank involved). The potential of a collection is the number of trees plus twice the number of marked nonroot nodes, and the amortized time of an operation is its actual time plus the increase of .
There is an absolute constant such that for every sequence of operations started from no heaps, with the number of items in the heap that operation acts on, just before it acts,
The paper's wording is "the total time is at most the total amortized time, where the amortized time is for each delete min or delete operation and for each of the other operations"; the goal pins the to one constant and does not name the potential.
THEOREM 1 is the data-structure fact behind the paper's algorithmic results: Dijkstra's algorithm in , all-pairs shortest paths and the assignment problem in , and minimum spanning trees in .
The result has been proved since 1987. What the mission adds is a machine-checked version of the paper's own analysis on an operational model with arbitrary linking order, unmarking on link, marking or cascading on every cut, and the paper's unit costs. The proposal states the theorem and its supporting claims; their proofs remain to be formalized.
The obvious argument, that every tree is a binomial tree and so every rank is at most , fails as soon as cuts are allowed: decrease key and delete remove subtrees arbitrarily, and the trees of an F-heap need not be binomial. The rank bound has to come from an invariant of the whole history (LEMMA 1), which only holds because a node loses at most one child before it is cut itself; without cascading cuts a node of rank can be left with only descendants, and no logarithmic rank bound holds. A second difficulty is that the actual cost of one decrease key is unbounded, since a single operation may trigger arbitrarily many cascading cuts; a per-operation worst-case argument cannot give THEOREM 1, and the bound holds only for whole sequences started from no heaps.
All declarations sit in the namespace FibHeap.Amort. Trees are a nested inductive FTree with item ℕ, key ℝ, a mark bit and a list of children in linking order; a heap is List FTree (its roots) and a collection is List Heap. Operations are a step relation Step s op s' d whose data d records linking steps, cuts, cascading cuts and the scan, so that cost d = 1 + links + cuts + scan is determined by what the operation did. The linking loop allows every order of linking; a link tie makes the first root a child of the second, while delete min may choose any minimum-key root. Runs start from no heaps; reachable collections consist of heap-ordered trees with each item in at most one heap. LEMMA 1, COROLLARY 1 and the delete-min bound are stated for reachable collections only, as the paper's "a node in an F-heap" intends. The paper's standing assumption that an item is in only one heap at a time is enforced by the precondition of insert and is not a hypothesis. The minimum pointer and returned items are not stored in the step relation; find min is a state-preserving step charged one unit. A heap destroyed by meld remains as an empty heap at its index.
Logarithms in the goal are base 2 (footnote 1, p. 600), with a so that one-item heaps have positive budget. The paper's constant "" on p. 604 is a rounding slip (); milestones use the exact .
The goal is not trivialized: the cost counts every linking step and every cut as fixed by the step relation, is quantified before the run, and a companion theorem (step_exists) shows that every valid operation can be performed, so runs containing delete min, decrease key and cascading cuts exist. A further supporting statement gives an explicit form of the delete potential bound. A complete development needs facts about the nested inductive (sizes, subtree lists, marked counts under list edits), an invariant for LEMMA 1 recording when each child was linked, and the Fibonacci inequality; contributions of any of these as separate lemmas are welcome.
A postal route that must traverse every street and return to its starting point is a Chinese postman tour. In a street network, crossings are nodes, streets are edges, and the cost of a route is the sum of the lengths of the streets it traverses, counted with repetition. The practical question is which streets must be repeated, and how often. Edmonds and Johnson's 1973 paper separates that question from constructing the resulting tour: choose the repeated edges first, then find an Euler tour of the resulting multigraph. This mission concerns their reduction of the first question to a minimum-weight matching of the odd-degree nodes.
The reduction matters because it turns a route problem with arbitrary repeated edge traversals into a finite pairing problem. The graph of odd nodes is complete, with the weight of a pair given by its shortest-path distance in the original network. A matching chooses which odd nodes to pair, and paths realizing those pairs identify edges to repeat. The paper also explains why overlapping paths can be replaced so that no edge needs to be repeated by this construction more than once (§3, pp. 92–93).
A graph has finite node and edge sets. Each edge has two distinct endpoints. Different edges may join the same pair of nodes, so parallel streets remain distinct. The graph is connected when every pair of nodes is joined by an edge-labelled walk. A walk records both its node sequence and its edge sequence; a tour is a closed walk. An Euler tour uses each edge exactly once, while a postman tour uses each edge at least once. Edge lengths are real and nonnegative, as in §2, p. 89.
The degree of is the number of named edges meeting it. Let be the set of nodes of odd degree. For every edge , let be the number of additional traversals. The parity equations require a nonnegative integer at each node such that
Their objective is . These are the paper's (3.1)–(3.4), with natural-number values encoding integrality and nonnegativity (§3, pp. 90–91). The equations express the even-degree condition after adding copies of each original edge.
For nodes , write for the length of a shortest path in . This distance is backed by an attaining edge-simple path and is a lower bound on the length of every walk from to . Connectivity and nonnegative edge lengths make that specification meaningful. Let be the complete graph on , with edge of weight . A 1-matching pairs every node of with exactly one distinct node. Its length is , equivalently half the sum of over for the pairing involution (§3, p. 92).
The goal asserts the existence of a 1-matching of the odd nodes and both directions of the cost comparison:
The existence conclusion and these comparisons identify the two attained minimum values. The goal does not prescribe a particular matching algorithm. Its supporting targets are the paper's uncrossing of overlapping shortest paths, parity of their union, reduction of multiplicities to zero or one, and decomposition of a parity solution into paths between odd nodes (§3, pp. 92–93).
The companion target relates a tour's edge counts to the parity equations. A postman tour traverses edge exactly times, and its length is
Conversely, positive integer edge counts with even incidence at every node can be ordered into a postman tour of a connected graph. The supporting Euler theorem handles a connected even multigraph (§2, p. 89).
The matching result characterizes the optimal additional cost of an undirected postman route. It says that the parity correction can be chosen from paths pairing odd nodes, and that no feasible choice of repeated traversals can beat the best such pairing. The companion identifies how that correction becomes an actual tour. The distinction is useful when one wants to change the matching method while retaining the mathematical guarantee on route length.
A formal development would provide a reusable account of finite multigraph walks whose edge names distinguish parallel edges, of shortest-path distances with explicit attainment, and of parity subgraphs decomposed into odd-to-odd paths and even-degree residual tours. These pieces support later formal work on route inspection, -joins, and matching-based graph algorithms. The paper proves the mathematical result. The exact multigraph and cost statements drafted here are open formalization targets; the local prior-art search found related results for simple graphs and metric traveling-salesman models, but no published statement with this paper's objects and conclusion.
A direct shortest-path construction can assign the same original edge to two matching pairs. Simply setting for the union then loses the additivity of path lengths, and setting loses the promised zero-or-one form. The uncrossing claim must control both the matching cost and the number of times each original edge appears. In the converse direction, an arbitrary feasible may contain repeated edges and cycles; the argument must account for these without assuming that every supported edge belongs to a path between odd nodes (§3, pp. 92–93).
Lean uses the published EdmondsMatching65.Polyhedron.Graph for : finite node and edge types and an endpoint map into unordered node pairs. A proof field excludes loops; distinct edge names may have identical endpoints. Walks use lists of nodes and named edges with zero-based indices, and the one-node, zero-edge walk is allowed. Edge multiplicities and parity witnesses are natural numbers. Costs and shortest-path lengths are real. The distance relation requires both an attaining edge-simple path and a bound against all walks; no real infimum over a possibly empty family is used. The matching is a fixed-point-free involution on the odd nodes, extended by the identity elsewhere, and each pair contributes half of its two directed distance terms.
The goal assumes a connected graph and nonnegative edge lengths, exactly as the section does. The tour-only results require a nonempty node type because a list-based tour must have a starting node; without it an edgeless graph on no nodes would satisfy connectivity and even degree vacuously. The path-decomposition statement permits unused even-degree cycles. No independent set of “odd nodes” is accepted as input: it is computed from the degree of .
The development needs finite multigraph incidence, edge-labelled walks, shortest paths, finite matchings, parity arithmetic, path uncrossing, and Euler tours. Proofs or useful intermediate results for these objects are welcome, including results applicable to multigraphs beyond the postman setting.
The Chinese postman problem asks for a shortest closed walk in a graph that traverses every edge at least once. Edmonds and Johnson (Math. Programming 5 (1973) 88–124) reduce it to two subproblems: choosing, by matching, which edges to duplicate so that every node has even degree, and then actually finding an Euler tour of the resulting even graph, a closed walk using every edge exactly once. Euler's theorem guarantees such a tour exists in a connected even graph, but an algorithm has to produce one and represent it compactly.
Section 5 of the paper gives two such representations and two algorithms. This mission formalizes the next-node representation: for each node , a list of the nodes the tour goes to when leaving . Theorem 5.1, which the paper attributes to its reference [1] (van Aardenne-Ehrenfest and de Bruijn, 1951) and to Berge's textbook, characterises exactly which lists describe an Euler tour; Theorem 5.2 shows the paper's next-node algorithm produces such lists. The same correspondence between Euler tours and arborescences is the combinatorial core of the BEST theorem on counting Euler tours of directed graphs (van Aardenne-Ehrenfest and de Bruijn, 1951).
A graph is a finite set of nodes and a finite set of edges, each edge meeting two distinct nodes; several edges may meet the same pair of nodes. The degree counts the edges meeting , and counts the edges meeting both and . A tour is an alternating sequence in which meets and ; an Euler tour contains every edge exactly once. is connected when every two nodes are joined by such a sequence, and even when every degree is even.
Next-node lists assign to each node a list of nodes. Given a starting node , the lists specify a walk: start at ; the first time a node is reached (for , at the start), leave it to ; the second time, to ; and so on, so the lists are read from the last entry to the first. The walk stops at the first node whose list is used up. The lists describe an Euler tour when this walk uses every entry of every list and its node sequence is the node sequence of an Euler tour of . With parallel edges, the lists name nodes only, and the edge used at each step is chosen so that every edge is used once.
An arborescence with root is a tree whose edges are directed so that every node has exactly one edge directed away from it, and has none.
For any node of an even, connected graph , next-node lists describe an Euler tour from if and only if
The printed condition (iii) names the edges ; the paper's own proofs of Theorems 5.1 and 5.2 use , the last exit from , and the printed version is false on a five-edge example. The goal states .
The proof on pp. 112–113 splits into five claims, each a milestone:
The lists produced by any complete run of the next-node algorithm of §5.2 satisfy (i), (ii) and (iii); together with Theorem 5.1, they describe an Euler tour.
Theorem 5.1 replaces a global property, that a walk uses each edge exactly once, by three local checks: list lengths, pair counts, and a tree condition on one distinguished entry per node. That is what makes the next-node representation usable. An algorithm only has to build lists with (i)–(iii), and Theorem 5.2 shows the paper's algorithm does so for every nondeterministic choice it makes. The same arborescence condition counts Euler tours in the BEST theorem: each arborescence and each ordering of the remaining exits gives a distinct tour.
The results have been proved since 1951. What this mission proposes is a Lean formalization on multigraphs with parallel edges, which is the setting the Chinese postman reduction needs, since duplicated edges are parallel. A search of Mathlib and of the platform finds no formalization of Theorem 5.1, of next-node lists, or of arborescences in this form. Mathlib has Eulerian walks only for simple graphs, and the existing platform statements of Euler's theorem (for example SupplyChainTheory.euler_tour_iff) are about simple graphs and existence only.
The necessity of (i) and (ii) is counting. The substance is in two places.
First, necessity of (iii): the last exits must be shown to leave every set avoiding . The tempting choice of the first exits , which is what the theorem's printed text says, is wrong: on an Euler tour the first exits can form a cycle, so any argument that does not distinguish first from last exits cannot work.
Second, the converse: a walk that follows lists satisfying only (i) and (ii) can return to early and leave edges untraversed, so (iii) is indispensable, and the statement depends on exactly which list entries have been used when the walk stops. Making that bookkeeping precise for a walk defined by a counter per node, and turning the used entries into an actual edge sequence in a multigraph, is the main formal work. For Theorem 5.2 the difficulty is the invariant of a nondeterministic algorithm: every trail it starts closes at its starting node because the graph is even.
All declarations live in the namespace ChinesePostman.NextNode. A graph is a local ChinesePostman.NextNode.Graph V E structure on finite types: ends : E → Sym2 V and a proof that no edge is a loop, so parallel edges are distinct elements of E with the same ends. Walks are pairs of a node list and an edge list. A list is a Lean List V, so is the entry at index and is the length. The walk specified by the lists is computed by follow L r, a fuel-bounded iteration whose state is the current node and the number of departures made from each node. It returns the node sequence and the final counters. DescribesEulerTour G r L requires every counter to reach the list length and some edge list to make the node sequence an Euler tour. Condition (ii) is quantified over all pairs including , where it forbids a node in its own list. Condition (iii) requires every list of a node to be nonempty, its chosen exit to be an edge of , and requires the iterates of the parent map (with ) to reach from every node. The next-node algorithm is an inductive step relation on states, and "produced" means reachable termination from the Step 0 state.
Added hypotheses: Theorem 5.2 and its corollary assume an edge meeting , which Step 0 needs; a one-node graph without edges satisfies Theorem 5.1 trivially and is not excluded. Milestones drop the hypotheses their claims do not use (connectivity, evenness), which makes them stronger.
A trivializing formalization is ruled out explicitly: the lists are read backwards, from to , and must all be used up. Reading them forwards, dropping the "uses every entry" clause, or stating (iii) with an empty-list default for the parent would each make a different, and in some cases false, statement.
The development needs walks on multigraphs, counting arguments for closed walks (in-degree equals out-degree along the walk), and a finite pigeonhole/orbit argument for the arborescence. The arborescence lemma (milestone 3) is graph-free and reusable. Proofs of any milestone, and of the multigraph walk lemmas they need, are welcome.
A matroid abstracts the dependence structure of the columns of a matrix: which sets of columns are linearly independent, forgetting the numbers themselves. Graphs are the special case of incidence matrices over the integers mod 2, where a set of edges is independent exactly when it contains no cycle. A natural combinatorial question in this setting is the minimum partition (or covering) problem: how few independent sets are needed to cover all the elements? For a graph this is the least number of forests that cover its edges, its arboricity.
J. Edmonds answered this question for every finite matroid in Minimum partition of a matroid into independent subsets (J. Res. NBS 69B, 1965, doi:10.6028/jres.069b.004). The answer is a good characterization in Edmonds's sense: there is a short certificate both that a partition into independent sets exists (the partition itself) and that it does not (a single subset that is too large for its rank). The paper is also the source of the matroid partition algorithm, which together with matroid intersection became a basic tool of combinatorial optimization.
Timeline:
Let be a finite set of elements and call some subsets of independent. Edmonds's two axioms are:
A matroid is a system satisfying both. The rank of is the largest cardinality of an independent subset of ; in a matroid every maximal independent subset of has exactly elements.
A circuit is a minimal dependent set. A span (closed set) is a set such that no circuit has exactly one element outside , and the span of is the minimal span containing . A partition into independent sets is a family of mutually disjoint independent sets whose union is ; any number of the may be empty.
For every finite matroid and every integer , the elements of can be partitioned into independent sets if and only if there is no with
The condition ranges over all subsets of , as printed.
The milestones follow the paper's own lemmas and the claims of its main proof, in order.
A further item states the paper's COROLLARY (Nash-Williams): the edges of a loopless finite graph can be colored with colors so that no circuit is one color if and only if no nonempty node set has , where is the set of edges with both ends in .
THEOREM 1 is the base case of matroid union: the sets coverable by independent sets form a matroid whose rank is , and the paper's proof is the origin of the polynomial-time matroid partition algorithm and of Edmonds's later matroid intersection theory. Its graphic case gives the arboricity formula of Nash-Williams, used for sparse-graph decompositions and orientation problems. The criterion is a certificate: a single set with proves that no partition exists.
The theorem has been proved since 1965 and appears in every matroid textbook. As far as the platform and Mathlib record, it has no machine-checked proof: Mathlib has matroids, circuits, closure and strong circuit elimination for its own Matroid structure, but no matroid union or partition theorem. This mission produces a formal proof from Edmonds's own axioms (Axiom 2 as an equal-cardinality condition, not an exchange axiom), together with the equivalences between his axiom systems, which are themselves standard results.
The "only if" direction is a three-line count. The difficulty lies in the converse: a greedy procedure that fills the sets one after another fails even for matroids, so an element that fits in no current set must be accommodated by moving other elements between sets. Such a chain of exchanges must keep all sets independent and disjoint at every step and must terminate; stating it with sets whose contents change while their labels persist is the part that needs careful bookkeeping in a formal proof. A second, smaller difficulty is the translation between the paper's equal-cardinality Axiom 2 and the circuit and span language its proof uses (PROPOSITIONS 1–5).
Finset.univ, subsets are Finset α, and the independent sets are a predicate Indep : Finset α → Prop.IndepI1 and rankOfIndep (WhitneyMatroid.RankIndep.Postulates). The rank is integer-valued, and every inequality versus is compared in with .Matroid.Fin k → Finset α of pairwise disjoint independent sets covering , with empty parts allowed and included.ends : E → Sym2 V (parallel edges allowed, loops excluded), with independence as linear independence of incidence columns over . It quantifies over nonempty : as printed, makes the statement false.Contributions welcome: proofs of the axiom equivalences (reusable for any work with Edmonds-style or circuit-axiom matroids), the span lemmas, the augmentation step, and bridges to Mathlib's Matroid that would let its circuit and closure library be reused.
Truncated-Newton methods minimize a smooth function by taking, at each iterate , a search direction obtained by solving the Newton equation only approximately, with the linear conjugate gradient (CG) method. Here is the gradient and the Hessian of . The approach was analysed by Dembo and Steihaug (Math. Programming 26, 1983), building on the inexact Newton framework of Dembo, Eisenstat and Steihaug (SIAM J. Numer. Anal. 19, 1982), and Newton–CG with curvature tests remains a standard large-scale method (Nocedal and Wright, Numerical Optimization, Ch. 7).
Away from a minimizer the Hessian need not be positive definite, and CG on an indefinite system can produce directions along which curves downward. The Dembo–Steihaug method stops CG when it meets such a direction. A practical question follows: started at or near a stationary point that is not a local minimizer, will the method ever notice the nonpositive curvature? Theorem 2.4 of the paper answers it for exact CG: it does, except in a degenerate case described by the eigenspaces of .
Fix a symmetric linear operator on , with the Euclidean inner product and norm , and a vector . In the paper these are and at the current iterate.
The TNCG minor iteration (p. 194) runs CG on from . Its state at iteration is :
and, writing ,
At iteration the method first applies the curvature test (2.1), , and stops if it holds; otherwise it computes and applies the truncation test (2.2), , and stops if it holds. With , (2.1) reads and (2.2) reads . The method exits through (2.1) at when no test fired at any iteration and (2.1) holds at .
For the eigenspace is (A.21). The span of vectors is written ; the Krylov space of is .
Let . If is not positive definite, then either the minor iteration exits through (2.1) at some iteration , so that
or
The theorem is the theoretical justification, given in the paper on p. 197, for using the direction of negative curvature produced in case (ii) of the minor iteration: with exact arithmetic and no truncation, CG either produces a direction of nonpositive curvature or the gradient lies entirely in the span of eigenvectors with positive eigenvalues. The paper draws the consequence that if and the method terminates through (2.2), then, outside this rare case, is a strong local minimizer. Theorem A.5 is a self-contained statement about conjugate families in Krylov spaces, usable in any analysis of CG on indefinite systems.
The result is proved in the paper (Appendix, pp. 206–211), with the CG relations of Theorem A.1 cited from Hestenes and Stiefel. No machine-checked proof of these statements is known to this mission. Formalizing them produces a Lean development of CG on a symmetric, possibly indefinite operator, with its conjugacy and Krylov-span relations, which classical treatments state only for positive definite systems.
The CG relations of Theorem A.1 are usually proved for positive definite , where every denominator is positive. Here is indefinite, and the relations hold only as long as the curvature along the directions has stayed positive; the induction must carry that hypothesis and must also show the residuals do not vanish early. The passage from "CG ended with " to a statement about all eigenspaces is the second obstacle: the CG run sees only the Krylov space of , so one must relate that space to the eigenspaces that meets, using symmetry of and a count of distinct eigenvalues. A direct argument via "the directions span " fails, because when misses an eigenspace the Krylov space is a proper subspace.
is EuclideanSpace ℝ (Fin n); is a continuous linear map that is self-adjoint (IsSelfAdjoint H), as the paper's is a Hessian. Positive definiteness is for all . The CG recursion is total and carries no stopping test; division by zero returns in Lean, so states after a would-be stop are junk, and the statements read the iteration only through first-exit predicates. The test (2.2) is encoded in the product form .
Theorem 2.4 is stated for an arbitrary symmetric and vector rather than at an iterate of a run of the full algorithm. It uses nothing else about or the run, and every such pair occurs as the Hessian and gradient of an admissible objective. The paper's (A.5) prints as the last Krylov vector; the correct is used.
A trivializing formalization exists and is ruled out: the first alternative is not " for some " over the unstopped recursion, which holds automatically once a residual vanishes (the recursion then continues with ); it requires that iteration is reached with no earlier exit. The goal does not assume conjugacy, the Krylov span identity, or the hypotheses of Theorem A.5.
A complete development needs the spectral theorem for self-adjoint operators on finite-dimensional spaces (in Mathlib), finiteness of the set of eigenvalues, and the CG invariants. The CG lemmas are reusable for any Newton–CG or trust-region CG analysis. Proofs of the milestones, and of auxiliary CG invariants such as (A.3)–(A.4), are welcome.
A Markov decision process describes repeated choices whose costs and subsequent states depend on the current state. Such models are used when a decision affects both today's expense and the options available tomorrow. Papadimitriou and Tsitsiklis studied how the computational difficulty of finding an optimal policy changes between stochastic and deterministic transitions. Their general finite-state problems are P-complete, while their deterministic cases admit highly parallel algorithms Papadimitriou and Tsitsiklis, 1987. The contrast makes the deterministic case a useful setting in which to isolate the precise graph problem hidden inside long-run optimization.
This mission concerns their infinite-horizon average-cost case. When transitions are certain, every decision is an arc in a directed graph. The long-run cost of a policy can be related to the mean cost of a cycle reachable from the initial state. That relation is the mathematical claim supporting the algorithm in the paper's Theorem 3, whose headline says that the deterministic average-cost problem is in NC Papadimitriou and Tsitsiklis, p. 446.
Let be a finite set of states and the initial state. At each there is a finite, nonempty decision set . A decision has a real cost and moves the process with certainty to . All of these data are stationary: they do not change with time. A policy chooses a decision for each state and each time . It generates a trajectory by . The corresponding directed graph has a state for each node and a decision for each arc. It may contain loops and parallel arcs, since different decisions can lead to the same next state.
The paper prints the finite average with cost terms and denominator :
A time-dependent policy's averages may fail to converge. We use the upper limit and optimize over all policies, . A state is reachable if some finite walk of decision arcs goes from to . A simple cycle is a positive-length closed sequence of decision arcs with distinct states before it returns to its start; its mean cost is . A loop is a one-arc simple cycle.
For states , the min-plus adjacency entry is the least cost of a decision arc from to , or when no such arc exists. A min-plus product uses addition in place of multiplication and minimum in place of addition. Thus represents the least cost of a -arc walk from to , when such a walk exists Papadimitriou and Tsitsiklis, pp. 445–446.
The first target identifies the value of the original policy optimization problem:
It also states that a policy attains this value with convergent finite averages. The milestone for following a reachable cycle gives the attainable direction; the milestone saying that no policy can improve the least mean gives the reverse direction. The latter is formulated with , so it applies even when a policy's averages oscillate.
The second target identifies the finite graph calculation used in the paper:
The milestones establish what a min-plus power says about decision walks and why closed walks of lengths from through recover the least simple-cycle mean. The restriction to reachable is essential: a cheap cycle in a disconnected component cannot be used from .
The result reduces optimization over infinitely many decision times and all state-and-time policies to finitely many closed-walk calculations. It also guarantees that an optimal long-run value is realized by a trajectory with a genuine limiting average, despite the nonconvergence possible for other policies. The finite formula lets one determine the value by comparing graph quantities indexed by states and lengths; it is the correctness statement beneath the paper's parallel algorithm Papadimitriou and Tsitsiklis, p. 446.
Formalizing the identity creates a reusable bridge between deterministic decision processes, weighted directed walks and min-plus powers. Related proved tropical-algebra results on maximum cycle means use dense matrices and a max-plus convention, rather than the reachable, possibly missing-arc, minimum-cost process here; for example, the platform's TropicalLA.tpow_isGreatest concerns greatest walk weights. The present mission keeps the policy optimum and reachability explicit. The paper proves the result mathematically; these Lean statements are open proof targets in the proposal.
An arbitrary policy can keep changing its choices at repeated visits to the same state. Its averages can oscillate, so one cannot simply assume that its infinite trajectory becomes periodic or that its printed limit exists. The lower-bound claim must apply to every such trajectory. There is a second distinction between a closed walk and a simple cycle: a diagonal min-plus entry allows repeated states, whereas the cycle characterization is stated using simple cycles. Finally, an unrestricted matrix calculation would include cycles unreachable from the chosen initial state.
Lean represents the general finite stationary deterministic process in its own definition, then defines policies, finite walks, simple cycles, average costs and min-plus powers on top of it. Decisions are arcs, so parallel arcs remain distinguishable; takes their least cost and uses WithTop ℝ for a missing arc. Decision sets are explicitly nonempty because a policy has to make a choice at every state. The finite state set is automatically nonempty once is supplied. Policy time starts at zero. The printed terms divided by are retained; Lean's quotient is zero and has no effect on the limit. The optimum is the infimum over all policies , not a quantity defined by cycles or by stationary policies. Finite states and finite decision sets bound the one-step costs and hence the averages; this gives real limsup and infimum their intended values.
The paper's Theorem 3 asserts membership in NC. This mission formalizes the exact optimization identity that makes that algorithm correct. Its processor count and parallel-time bound are outside the scope, as are membership in P, log-space computability of reductions, PSPACE membership and the paper's Corollaries 1–2. Contributions to the finite-walk and min-plus lemmas, the lower bound for arbitrary policy paths, and the cycle-attainment statement are all needed; the graph definitions can be reused in other deterministic control problems.
All-pairs shortest paths (APSP) computes the shortest distance between every pair of vertices in a weighted graph. It is a fundamental problem in graph algorithms and a fundamental problem in fine-grained complexity.
This mission formalizes a deterministic algorithm for APSP on directed -vertex graphs with polynomially bounded integer edge weights and no negative cycles, on a word RAM with -bit words. This is a truly subcubic bound and refutes the integer-weight APSP hypothesis in this model.
Theorem_22_APSP.Minimum makespan scheduling on unrelated parallel machines, written , is one of the basic models of scheduling theory: jobs must each be run on one of machines, and the time a job takes depends arbitrarily on the machine. Lenstra, Shmoys and Tardos (CWI Report OS-R8714, 1987; journal version Math. Programming 46, 1990) gave a polynomial 2-approximation algorithm for this problem and, in the same paper, a matching limit from below: no polynomial algorithm can guarantee a factor smaller than unless (their Corollary 2).
The two bounds have stood for more than three decades. Closing the gap between and for is listed among the central open problems of approximation algorithms (Williamson and Shmoys, The Design of Approximation Algorithms, 2011, open problem on unrelated machines; Schuurman and Woeginger, Polynomial time approximation algorithms for machine scheduling: ten open problems, J. Scheduling 1999). The lower bound of is the subject of this mission.
Timeline:
3-dimensional matching. There are three disjoint sets , , and a family of triples, each with one element of , one of and one of . A matching is a subfamily with whose union is . In Lean an instance is a map , and HasMatching T says that a matching exists.
The scheduling model. Machines are , jobs are , and is the positive integer processing time of job on machine . A schedule assigns each job to one machine; the load of machine is and the makespan is the largest load. These are the published definitions MatousekLP.Scheduling.load and makespan.
The instance of Theorem 5. The triples containing are the triples of type ; let be their number. From the paper builds a scheduling instance with machines, machine corresponding to , and with
If , machine processes the element jobs of and in time , each dummy job of type in time , and every other job in time . In Lean the processing-time matrix is P T.
A -approximate schedule of an instance is a schedule with for every schedule of the same instance.
For every instance , every , and every -approximate schedule of the instance of Theorem 5 built from ,
This is the mathematical content of "for every there is no polynomial -approximation algorithm unless ": a -approximate answer on the reduced instance decides 3-dimensional matching.
For every instance ,
The result. Theorem 5 shows that is NP-hard already when every processing time lies in and the target makespan is . Corollary 2 turns this into the best known inapproximability bound for the problem, , which sits opposite the paper's own factor-2 algorithm. The same reduction pattern (machines as triples, dummy jobs that pin machines down) is reused in many later hardness proofs for scheduling and assignment problems.
Formalizing it. The result is proved on paper; no machine-checked version is known to exist. A formal proof requires the full combinatorial argument behind the reduction, including the counting of machines per type and the case where some element of lies in no triple, which the paper does not discuss. Together with mission 1 of this series (the factor-2 algorithm), it fixes both ends of the gap in one formal library.
The construction is short, but the converse direction carries the weight: from an arbitrary schedule with makespan at most one must recover a matching, although nothing in the schedule singles out the triples that form it. The obvious first idea, to read the matching off the machines that receive unit-time jobs, fails as it stands: a machine may receive one unit-time job or none, and the argument must exclude this for every schedule, including the degenerate instances in which some lies in no triple or triples repeat. For Corollary 2, the passage from the real-valued approximation guarantee to the threshold depends on the strict inequality ; at the statement is no longer implied by Theorem 5.
Fin m; 3DM elements are Fin n; a 3DM instance is T : Fin m → Fin n × Fin n × Fin n, so a triple may repeat. A matching is a set of triple indices covering every , , (the covering form of the paper's definition, which forces disjointness).MatousekLP.Scheduling.makespan applies. All statements quantify over every schedule, so the choice of bijection is irrelevant.Assortment optimization asks which products a retailer should offer when customers choose among the offered products according to a probabilistic choice model, so as to maximize expected revenue. Under the nested logit model the products are grouped into nests: a customer first picks a nest, then a product inside it. The model is the standard relaxation of the independence of irrelevant alternatives property of the multinomial logit, and it is used throughout revenue management and transportation demand modelling.
Davis, Gallego and Topaloglu (Oper. Res. 62(2), 2014) classify the complexity of the assortment problem under four variants of the nested logit model, according to whether the dissimilarity parameters are at most one and whether a customer who picks a nest always buys there. The problem is NP-hard as soon as some dissimilarity parameter exceeds one (their Theorem 5), and also when the nests have positive no-purchase weights (Theorem 8), so for the general variant approximation is the realistic aim. §6.2 of the paper gives an approximation scheme for the most general variant: for any it restricts each nest to a short list of candidate assortments indexed by the powers of , solves a small linear program, and loses at most a factor of the optimal revenue. This mission formalizes the guarantee behind that scheme, Theorem 12.
There are nests and products in each nest. Product of nest has revenue and preference weight ; the products are ordered so that . Nest has a no-purchase weight and a dissimilarity parameter , and is the weight of leaving without choosing a nest. Offering in nest gives
The optimal expected revenue is the optimal value of the linear program (3): minimize subject to and for every nest and every . Problem (4) keeps the second family of constraints only for a candidate collection of assortments in each nest.
Let , assumed throughout §6, and fix . Put , , and let , be the least integers with , . For each level , problem (15) maximizes over the assortments with ; its value is . An assortment is feasible for (15) and satisfies . The candidate collection of nest is .
If is an optimal solution of problem (4) over the candidate collections , then
Theorem 12 is the analytical half of the approximation scheme. Together with the paper's Theorem 1 it shows that a linear program with variables and at most constraints yields an assortment within a factor of the optimum, for the most general variant, which is NP-hard, and Proposition 15 makes the candidate assortments computable. Letting trades accuracy for running time, so the result is the paper's answer to how well the general problem can be approximated by this LP approach.
The result is proved in the paper; the work here is to formalize the known proof. To the best of a search of the Prove2Me library (local index and platform mirror, October 2026), no nested logit approximation result, and no knapsack lemma matching Proposition 15, has a machine-checked statement or proof. The definitions of the shared model (the instance, , , , the linear programs (3) and (4)) are common to the six missions of this series.
The obvious argument compares an arbitrary assortment with the candidate of its level and uses the candidate's constraint in (4). This fails as a direct comparison because the nest weight enters twice with different exponents, in front of the revenue and in front of , and within one level may vary by a factor . When and when the monotonicity of goes in opposite directions, so the losses must be tracked separately by and , and they are absorbed by the common factor only because . The other half, Proposition 15, concerns a knapsack with both a lower and an upper bound on the total weight, where a feasible solution must be produced as well as a good objective value.
Products are Fin n ( for ), nests a finite type, powers real powers, and , which gives . The shared model carries the standing assumptions of §1 with the disclosed pins , and (the page allows and zero-weight padding products, under which its convention and its proofs fail). Every statement of the mission also assumes (for ), is the greatest of the (so at least one nest exists) with , and . Integer powers are zpow, and , are written , , which equal the minima of the paper. An optimal solution of (4) is a feasible pair whose is minimal among feasible pairs. The companion guarantee adds , the pin of Theorem 1. In Proposition 15 the capacity row of (33) includes , correcting a printed slip, and the running-time claim is not stated.
The assortments enter Theorem 12 as an arbitrary family with the two properties of p. 28; the theorem is stated for every such family. A level at which (15) has no feasible assortment imposes nothing on , as on the page. Requiring to lie in its level unconditionally would make the hypothesis unsatisfiable for most instances and the goal vacuous; that encoding, and any goal that assumes displays (34)–(36) or the exponent bounds, is ruled out.
Contributions welcome: proofs of the real-power milestones (3)–(5), which are self-contained, of the two cases (6)–(7), and of Proposition 15, whose fractional knapsack lemma (the greedy solution of a continuous knapsack sorted by ratio is optimal) is reusable beyond this mission.