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?
All-pairs shortest paths (APSP) asks for the exact distance between every ordered pair of vertices in an -vertex weighted directed graph. Floyd–Warshall solves it in time, and for decades no algorithm beat for any constant on graphs with polynomially bounded integer weights. The APSP conjecture of fine-grained complexity asserted that none exists. In 2026, Alman and Vassilevska Williams (arXiv:2610.06783) refuted it with a deterministic algorithm. That bound is the campaign's first entry, and it is formally proved on the platform.
This entry records the deterministic exponent , obtained by tightening the accounting in the same algorithm.
The model is the campaign's fixed deterministic word RAM (foundation mission: Truly Subcubic APSP on a Word RAM). A finite program uses add, subtract and multiply modulo , indirect load and store, a sign branch, and accept or reject, on words of width . Inputs have integer weights of absolute value at most for a fixed , and there are no negative cycles. The machine has no source of randomness, so randomized (Las Vegas) algorithms do not count.
The goal is the campaign template with the value :
which says there is a deterministic word-RAM program that solves APSP in steps.
The core of the published algorithm is a data structure for thin min-plus-type products with inner dimension . It has preprocessing and queries , with parameters (recursion ratio) and (switch threshold). Four changes improve the saving from to about :
The explicit parameters , and satisfy the thinness condition () and give . Since , the slack absorbs all polylogarithmic factors.
The randomized version of the same argument reaches about by repeating random-prime hashing. That bound is out of reach in this deterministic model. Closing the gap between deterministic and randomized collision handling is a natural next target for the campaign.
The 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. The question is how large a comparison constant is needed to make this inequality hold.
This mission asks whether the best possible constant for complex diagonal matrices, already proved in Lean for every real , also holds for every real . This is an open problem: no proof is known. The constant is the one from the foundation mission: the largest comparison constant required by the cyclic family of three diagonal matrices. Because the cutoff-85 mission already covers every , the new work is the range from 80 to 85.
The cutoff came down from 90 to 85 in two days, through moona3k's proofs at 89, 88, 87 and 85. The step to 89 sharpened the estimates of the cutoff-90 argument. The step to 85 added a new idea, a weighted pair-curvature and confinement estimate. How far that idea reaches is not known; 80 asks for five more units. The goal theorem below gives the exact statement.
This is an entry in the sharp diagonal Hlawka campaign, which asks for the smallest cutoff at which the same formula holds. Any proof for a cutoff of 80 or lower also settles this mission.
The broader question of optimal constants for Schatten norms appears in Audenaert and Kittaneh’s Problem 7. Extending the sharp diagonal constant to general matrices is a separate challenge.
79aa498bfcf7b22bd91d771fb32ec278e2d4704b. Source libraryThis entry lowers the sufficient exponent cutoff for the sharp diagonal Hlawka formula from85 to84. For every real p≥84, the foundation's unchanged cyclic constant is the least constant comparing the triple deficit with the pair-deficit sum for every complex coordinate triple in every finite dimension.
The statement includes unequal and zero input vectors and dimension zero. It concerns complex diagonal matrices through their coordinate norms; it does not settle the conjectured cutoff2 or the full noncommutative matrix problem.
Both exact proof submissions have been ACCEPTED by Prove2Me, and both theorem records are Proved. Their accepted sources match the submitted files and exact target statements in the pinned environment. This proposal references those existing verified results; the remaining steps are human submission and campaign moderation.
The construction is by Ezzeri Esa (GitHub savarin), with the accepted cutoff90 formalization by BrunoDCDO. Claude Opus5.5 produced moona3k's accepted89,88,87 work. Codex's accepted85 continuation and new84 extension reuse their verified generic calculus and transfer arguments.
On[84,85], an exact rational matrix sum-of-squares certificate proves a coupled radial energy estimate throughout a larger localization box. Residual estimates give nonnegative actual deficit Hessians and box convexity. Tight logarithm/Taylor bounds and exact positive Bernstein certificates localize every normalized failure. Orbit averaging and circle transfer prove the real and complex bounds, and the cyclic obstruction establishes leastness. The accepted85 development supplies the remaining tail.
The campaign began with cutoff256, followed by90,89,87,85. This entry instantiates its exact template with84 over the same foundation definitions.
Scheduling unrelated parallel machines to minimize the makespan, written , is one of the basic NP-hard problems of scheduling theory. A set of jobs must each be run on one of several machines, and the time a job takes depends arbitrarily on the machine; the goal is to finish all jobs as early as possible. Before the work formalized here, the best polynomial algorithm known guaranteed only a schedule within times the optimum (Davis and Jaffe, 1981), a factor that grows with the number of machines .
Lenstra, Shmoys and Tardos (FOCS 1987; CWI Report OS-R8714, 1987; Math. Programming 46, 1990) gave a polynomial algorithm with guarantee , independent of . Their tool is a rounding theorem: a vertex of a natural linear-programming relaxation can be rounded to an integral schedule that exceeds each machine's budget by at most one job. The rounding theorem and the binary-search framework around it became standard material in approximation algorithms.
There are jobs and machines. If job is scheduled on machine , it takes time units, a positive integer. A schedule assigns every job to one machine . The load of machine is , the makespan of is the largest load, and is the minimum makespan over all schedules.
For deadlines and a threshold , let and . The linear program (LP) has variables for and constraints
The integer program (IP) replaces by and requires . A vertex of (LP) is an extreme point of its feasible polytope. The support graph of a point is the bipartite graph on machines and jobs with an edge whenever .
A -relaxed decision procedure answers, for a deadline , either 'no' or a schedule, such that (1) every schedule it returns has makespan at most , and (2) if it answers 'no', no schedule has makespan at most . The binary search of Lemma 1 starts from the greedy schedule (each job on a machine where it runs fastest), whose makespan is an upper bound , with lower bound , queries the procedure at , moves to on a schedule and to on 'no', and outputs the best schedule found once .
The LP rounding procedure answers, on deadline , by solving (LP) with : 'no' if it is infeasible, and otherwise a 0-1 solution of (IP) obtained by rounding a vertex chosen by the LP solver, supported on .
For every LP solver (every rule choosing a vertex of (LP) when it is feasible), an LP rounding procedure exists, and for every such the output of the binary search satisfies
Theorem 2 gives a constant-factor approximation for that does not depend on . The same rounding theorem drives the paper's second algorithm, a -approximation for a fixed number of machines using polynomial space, and the paper's lower bound shows that no polynomial algorithm achieves a factor below unless . The Rounding Theorem, in its later form for generalized assignment by Shmoys and Tardos (1993), is a standard tool for LP-based scheduling and assignment.
The result is proved; it has, to our knowledge, no machine-checked proof. The platform contains Matoušek and Gärtner's textbook version (MatousekLP.Scheduling.lst_two_approximation, Theorem 8.3.4 of Understanding and Using Linear Programming), which uses a different relaxation: one bound minimized parametrically over , optimal solutions with linearly independent columns, and no per-machine deadlines. This mission formalizes the report's own route: deadlines , arbitrary vertices, binary search over a relaxed decision procedure. A formal proof would also yield reusable statements about extreme points of transportation-type polytopes and matchings in pseudoforests.
The obvious rounding, putting each job on a machine where is largest, can overload a machine by many jobs at once: nothing in feasibility alone prevents many jobs from each placing a small fraction on the same machine. The bound requires that each machine receive at most one job that the vertex treats fractionally, and this fails for general feasible points; it holds only because is a vertex. The step that carries the weight is therefore a statement about the combinatorial structure of the support of an extreme point, which must be derived from the linear independence of the tight constraints, followed by a matching argument on the resulting graph. Neither step is available in Mathlib in the form needed.
On the algorithmic side, the binary search must be shown to return a schedule within although the decision procedure is only approximately correct; the invariants (the lower bound stays below , the stored schedule stays within times the upper bound) have to be tracked through a recursion.
Fin m, jobs Fin n, processing times a matrix P : Matrix (Fin m) (Fin n) ℕ with all entries positive in Lemma 1 and Theorem 2 (the paper's model, p. 2). Loads, makespans and optimal schedules are the published MatousekLP.Scheduling.Schedule definitions applied to the real matrix ; is the makespan of a schedule σopt with IsOptimalSchedule.Set.extremePoints) correspond exactly. Theorem 1 and its steps are stated for real deadlines and real , more general than the paper's integers; the paper's proof does not use integrality, and mission 2 of this series needs non-integral .The assignment problem asks how to assign men to jobs, one man per job, so that the total cost (or, equivalently, the total rating) is optimal. It is the simplest combinatorial optimization problem with a nontrivial polynomial-time algorithm, and it appears as a subroutine across operations research: in transportation and network-flow methods, in tracking and data association, in scheduling, and as the relaxation behind branch-and-bound methods for the travelling salesman problem.
The algorithm studied here is the one now usually called the Hungarian method or Kuhn–Munkres algorithm.
The mission formalizes Munkres' correctness proof for §1 of that paper.
Let be a real matrix, being the cost of assigning man (row ) to job (column ). A set of entries is independent if no two of them lie in the same line (row or column). An assignment is a permutation , with the man doing job . Its cost is , and is an optimal assignment if this cost is at most that of every permutation . Choosing independent entries of minimum sum is the same as choosing an optimal assignment.
The algorithm. A state of the algorithm holds the current matrix, a set of starred zeros , a set of primed zeros , a set of covered rows and a set of covered columns. An entry is non-covered, once-covered or twice-covered according as it lies in zero, one or two covered lines.
The quantity , the maximal number of independent zeros of the matrix , measures progress.
For every real matrix :
The four clauses are needed together: optimality at final states alone holds for an algorithm that never stops.
Correctness of the Hungarian method is the basis of a standard algorithm for the assignment problem and, through it, of methods for transportation problems, minimum-cost bipartite matching and weighted bipartite matching. Its refinements remain in practical use. The invariants of the proof are the primal–dual structure of the problem: the row and column constants subtracted along the way form a dual solution, and the starred zeros at the end are a primal solution satisfying complementary slackness.
The result has been proved since 1957 and is in every textbook on combinatorial optimization. A machine-checked version of Munkres' specific procedure, as a transition system with all its free choices, with finiteness for real (not only integer) matrices, is not available on this platform; Mathlib has no assignment algorithm. The mission produces a verified specification of the algorithm, reusable invariants about covers and independent zeros, and a termination argument that does not rely on integrality.
Optimality at termination is short once the invariants are known. The work lies in two places.
First, the invariants hold only along runs. "Each is covered by precisely one line", "no column contains more than one " and "no row contains more than one " fail for arbitrary marked matrices, so they must be carried as an inductive invariant through every move, including the Step 3 transformation, which keeps the primes.
Second, termination. The obvious measure, the sum of the entries, decreases by at each Step 3, but for real entries can be arbitrarily small, so the decreasing sum gives no bound on the number of steps. The page replaces this argument by the stronger result of p. 35 (milestone 8), which holds for real entries. Turning it into a proof that every run of the nondeterministic move relation is finite, including the moves inside Step 1 and Step 2, is the core of the formalization.
Fin n × Fin n (row, column).HeldWolfeCrowder_Assignment_Setting: σ r is the row assigned to column r, the starred positions are , and optimality is IsOptimalAssignment A σ with respect to the original input matrix.Step. The order in which the Preliminaries consider the zeros, and the non-covered zero primed in Step 1, are free choices. Every claim holds for every run.Acc) of each start state for the reversed move relation.Not formalized: the operation count of pp. 35–36, whose cost model is informal; the argument that returning to the standard input after Step 3 is unnecessary (pp. 34–35); König's theorem (Remark (1), cited); and §2 on the transportation problem, which is stated without proof.
Welcome contributions: proofs of the milestones, a general library of lines and independent zeros in matrices (reusable for König–Egerváry), and an executable refinement of the move relation.
A firm that sells a product line of different qualities cannot see how much each customer values quality. It can only post a price for every quality and let customers choose. Mussa and Rosen's 1978 paper solves the monopolist's problem in this setting and compares the result with the competitive outcome. Their model is, together with Mirrlees' optimal income tax and Maskin and Riley's later treatment of nonlinear pricing, one of the founding examples of screening: the seller designs a menu so that customers sort themselves. The model's main qualitative prediction, that a monopolist degrades the quality sold to every customer except the one who values quality most, is the origin of the phrase "no distortion at the top". Textbooks on contract theory and mechanism design still teach it in this form.
Timeline. Mussa and Rosen (1978) give the first-order analysis, including "bunching" of customers at a common quality when marginal revenue is not monotone. Maskin and Riley (1984) treat the same problem for nonlinear quantity pricing. Myerson (1981) introduced the "ironing" procedure for non-monotone virtual valuations in auction design, which later became the standard way of describing the bunching conditions of this paper.
Consumer types are numbers with , distributed with a density that is positive and differentiable on the whole interval; . A consumer of type buys at most one unit, and from quality at price gets utility . Producing one unit of quality costs , where , is twice differentiable, and , for .
Under competition, price equals unit cost and type buys the quality with , or nothing when .
The monopolist chooses an assignment , the quality bought by type . It must be nondecreasing, nonnegative and piecewise differentiable on ; such assignments are called admissible. Incentive compatibility and participation fix the consumer surplus at , so the monopolist maximizes
An assignment is optimal if it is admissible and maximizes among admissible assignments. The marginal revenue of quality sold to type is
The paper's analysis runs through the marginal profit of a uniform quality increase for all types ,
For every optimal assignment :
and, if , the limit exists and satisfies (if , then ). In words: for every type below the top that buys under competition, types that do not buy under competition do not buy from the monopolist, and .
The paper's own chain of claims, in order: except at (p. 308); the first-order condition (9), for every admissible deformation; the identity (10) = (12), ; condition (13), ; condition (15), where ; at a jump; the absence of jumps; (17), where ; the bunching conditions (18)–(19); and the absence of a bunch at the top. Companion items state the two-type case of footnote 4, the uniform–quadratic example of §5, and the loss of consumer surplus (§6, "Second").
The result. The goal says how the monopolist differs from competition: it lowers every quality except the top one, and it never serves a type that competition leaves out. The distortion comes from the gap , which closes only at . The same comparison underlies results on second-degree price discrimination, regulation of product lines, and versioning of information goods. The bunching conditions (18)–(19) are an early statement of what is now called ironing.
Formalizing it. The result has been proved since 1978 in the economic literature, under the paper's smoothness assumptions and by a variational argument. As far as is known, it has not been machine-checked: no formal library contains the monopoly quality problem, its first-order conditions or the bunching conditions. The mission produces a checked version with the hypotheses made explicit, including the conventions at the endpoints that the paper leaves implicit. The uniform–quadratic example gives a concrete optimum that certifies the hypotheses are satisfiable.
The obvious argument sets pointwise and compares with . This fails when is not increasing: the pointwise solution is then decreasing somewhere and not admissible. The optimal assignment is constant on some intervals, and on such a bunch pointwise. The comparison with there needs the boundary conditions (18)–(19) and the fact that no bunch reaches . All of these come from one-sided deformations that respect monotonicity, so the first-order conditions are inequalities and need a separate argument for equality. The paper also asserts without a separate step that optimal assignments have no jumps, and later steps use continuity.
Types and assignments are real functions on ; only their values on matter. The type distribution and are the published MechanismDesign.Screening.TypeDistribution and virtualValuation. The standing assumptions are hypotheses of every main statement: is differentiable on (positivity and total mass 1 are part of the distribution), , and are differentiable on , and , on . is an added normalization: quality 0 means not buying. "Piecewise differentiable" means differentiable on outside a finite set. The competitive assignment is never formed; every comparison with is written through . Admissible deformations in (9) are required to keep .
The value does not affect , so a statement about itself would be false; the top-type claim is stated as a left limit. Optimality ranges over admissible assignments only. Any reading under which no optimal assignment exists makes the goal vacuous; the §5 companion rules this out, since its optimal assignment has a kink and uses the same notion of optimality.
Needed infrastructure: interval integrals of monotone functions, first variations under monotonicity constraints, and fundamental-theorem-of-calculus arguments for . The incentive-compatibility reduction (monotonicity and the envelope formula) is not posed here, because it is posed on the platform in Börgers' screening chapter. Related platform item: Börgers' Proposition 2.6 (MechanismDesign.Screening.nonlinear_pricing_optimal) treats a linear-cost, concave-valuation model under regularity, which is a different statement. Contributions to any milestone, and reusable lemmas about monotone deformations, are welcome.
Semiconductor burn-in ovens can process several jobs at once. A group placed in one oven must remain together until the longest job has finished, so increasing batch size saves oven starts but can delay short jobs. When several ovens are available, a scheduler also has to decide which oven receives each batch. Lee, Uzsoy, and Martin-Vega studied this setting and gave guarantees for a simple rule that first groups an arbitrary job list into batches and then sends those batches to the next available oven (Lee, Uzsoy & Martin-Vega 1992, §§2 and 5). Their bounds give a way to assess this easily specified rule against the best possible schedule, even when finding that schedule is difficult.
The paper treats both makespan, the time when all jobs have finished, and maximum lateness, the largest difference between a job's completion time and its due date. These objectives respond differently to batching. The makespan ignores which particular job finishes late; maximum lateness depends on each job's due date. Proposition 4 relates the lateness guarantee to the makespan guarantee of Proposition 1, making the two results a natural formalization unit (Lee, Uzsoy & Martin-Vega 1992, pp. 772–773).
There are jobs, indexed by , with processing times and due dates . All jobs are available at time zero. There are identical batch machines, each able to process at most jobs at once. A batch cannot be interrupted or enlarged after it begins, and its processing time is the largest among its members. A schedule partitions the jobs into nonempty batches, chooses a machine for each batch, and orders the batches on each machine. Batches assigned to a machine run one after another from time zero. Every job in a batch finishes when that batch finishes (Lee, Uzsoy & Martin-Vega 1992, p. 766).
For a set of jobs , write for the least makespan over all valid batchings and machine assignments. Write for the least possible value of , where is job 's completion time. For the full job set, abbreviate these by and . The maximum due date over all jobs is .
Batch list scheduling (BLS) begins with any ordering of the jobs. It divides successive entries into full batches of jobs, apart from a possibly smaller final batch. It then assigns each next batch to a machine that becomes available first. Denote the resulting makespan by and its maximum lateness by . The guarantee applies to every initial list; it does not require an earliest-due-date or longest-processing-time order (Lee, Uzsoy & Martin-Vega 1992, p. 771, Algorithm BLS).
Proposition 1 asserts, for every BLS list,
The milestone list includes the paper's processing-volume lower bound, , and Proposition 1 itself. The latter is stated for arbitrary job subsets as well as the full instance, because the paper applies it to a prefix sub-instance in the proof of Proposition 4 (Lee, Uzsoy & Martin-Vega 1992, p. 772).
The mission's goal is the printed ratio of Proposition 4:
The denominator is positive under the stated conditions, even if the optimal maximum lateness is negative. The remaining milestones record the paper's lower bound for a nonempty sub-instance and its reduction from the full instance to the BLS prefix containing a maximum-lateness job (Lee, Uzsoy & Martin-Vega 1992, p. 773).
The makespan result controls the cost of using an arbitrary initial list and simple next-available-machine assignments instead of optimizing both the batching and machine allocation. At , its factor becomes , the ordinary list-scheduling factor noted by the authors. Proposition 4 gives a corresponding bound for maximum lateness, normalized in a way that remains meaningful when (Lee, Uzsoy & Martin-Vega 1992, pp. 772–773).
These are proved results in the 1992 paper. The formalization work is to give their batch model, sub-instance optima, and the printed inequalities machine-checked statements and eventually proofs. The imported library already has definitions of least-loaded list scheduling and optimal assignment makespan for ordinary items on identical machines. This mission adds the batch layer, its lateness objective, and the comparison between the batch algorithm and unrestricted batch schedules. The Lean declarations here compile as open theorem targets; this proposal does not claim completed machine-checked proofs.
The processing time of a batch is a maximum, while its contribution to the volume of jobs is a sum. Treating each batch as an ordinary job gives a list-scheduling instance, but it does not by itself compare that instance's optimum with the optimum over all ways to form batches. That gap is central to the makespan bound. The lateness goal has a second obstacle: the job that determines the BLS maximum lateness may sit in a batch that is not the last to finish, and due dates prevent a direct substitution of a makespan bound for a lateness bound. Moreover, may be negative, so dividing by it would not give a valid relative error. The stated normalization and its positivity require explicit attention (Lee, Uzsoy & Martin-Vega 1992, proof of Proposition 4).
Jobs are Fin n and machines are Fin m; the paper's first job is Lean index zero. Processing times and due dates are real numbers. The paper's integer-data convention is sufficient for these inequalities but is not needed for their statements. Processing times are positive, all jobs are available at time zero, and the lateness goal requires nonnegative due dates. This last condition makes explicit what the paper's final inequality uses: allowing negative due dates makes Proposition 4 false. The full job set is nonempty. Prefix jobs are the first batches of the given arbitrary list, and the optimal values for a prefix range over every valid batching and assignment of those jobs.
The BLS implementation chunks the list into full batches and a final remainder. A batch is sent to a least-loaded machine, which is the first machine to become free when no idle time is inserted. The published list-scheduling definitions of NumStochOpt.ListScheduling supply this rule and the ordinary assignment optimum. They select the lowest machine index on a tie; identical-machine labels do not affect the resulting completion times. Machine schedules are represented by an ordered batch list and an assignment, with each machine processing its own batches back to back. No bound is obtained by defining the optimum over BLS-shaped consecutive batches, and no theorem fixes a favorable job list.
The mission covers correctness inequalities, not the paper's running-time claims or its later BLPT rule. Useful contributions include proofs of the four milestones, finite-schedule facts showing the optima are attained, and reusable links between batch completion times and least-loaded list scheduling. The parallel batch model can also support other objectives and scheduling rules.
Burn-in is the final testing stage of semiconductor manufacturing: finished integrated circuits are loaded on boards and held in an oven at high temperature for a prescribed minimum time, so that weak devices fail before shipment. An oven holds many boards at once, a load cannot be interrupted, and a board may stay in the oven longer than its specified time but never shorter. Because burn-in times are long compared to the other test operations, the ovens are frequently the bottleneck of the test facility, and the order in which lots enter them determines whether customer due dates are met.
Lee, Uzsoy and Martin-Vega (Operations Research 40(4), 1992) modelled an oven as a batch processing machine and gave polynomial algorithms for several due-date objectives. This mission covers the first of them: one machine, jobs with release times and a common processing time, and the question whether every job can be completed by its due date. Ikura and Gimple (Operations Research Letters 5(2), 1986) had already given an algorithm for this feasibility question when release times and due dates are agreeable; the paper replaces it by a simpler dynamic program, DP1, and uses DP1 with a bisection search to minimize the maximum tardiness.
There are jobs, indexed . Job has a release time (it cannot be processed earlier), a due date , and the common processing time ; all data are natural numbers. One machine processes up to jobs simultaneously.
A batch schedule of a set of jobs is a sequence of batches : nonempty, pairwise disjoint sets of at most jobs whose union is , processed in this order. A batch cannot be interrupted, and no job joins it once it has started. It starts as soon as the previous batch is finished and all its jobs are released, and it takes time :
Job completes at for the batch ; the makespan is . A schedule is feasible (has ) if for every job, and its maximum tardiness is .
Release times and due dates are agreeable if implies . A schedule is in batch-EDD order if no job of an earlier batch has a larger due date than a job of a later batch.
Algorithm DP1. With the jobs indexed in nondecreasing order of due dates, let and, for ,
For an index order nondecreasing in both and , and every ,
The minimum ranges over all batch schedules of the prefix: every batching and every batch order. The case is the paper's statement that DP1 "will find a feasible schedule with minimum makespan if a feasible schedule exists" (p. 768).
DP1 decides feasibility of and, when the instance is feasible, returns the minimum makespan of an on-time schedule. Applied to due dates augmented by a trial value , it decides whether is achievable, which together with the bound of Lemma 2 gives the paper's polynomial procedure for minimizing . The consecutive-partition structure behind it recurs in the paper's later dynamic programs (DP2 for agreeable processing times and due dates, DP3 for the number of tardy jobs), and in much of the later literature on batch scheduling with release dates.
The results are proved in the paper; none of them has a machine-checked proof. The mission formalizes the known proofs. Its formal statements also make explicit two assumptions that the printed text leaves loose: the tie-break of the index order, without which DP1 returns a wrong value, and the hypothesis of Lemma 2, without which the lemma is false.
The obvious argument for the goal is "by Lemma 1 the batches are consecutive, and DP1 enumerates consecutive partitions". Lemma 1 orders the batches by due dates, but it does not make the batches intervals of the index order: jobs with equal due dates may still be split across batches in an order that is not the index order, and when equal due dates are indexed against the release order DP1's value underestimates the start of the batch . The step from batch-EDD order to consecutive batches, and the fact that the exchange never increases the makespan, are the content of the justification milestone. The goal also asserts two directions at once: that the DP value is attained by some feasible schedule, and that no feasible schedule, consecutive or not, finishes earlier.
Jobs are Fin n, 0-based (the paper's job is i - 1); a prefix "jobs " is a prefix length . Data are natural numbers, as the paper assumes ("all data to be integers", p. 769). A batch schedule is a List (Finset (Fin n)); schedules are semi-active, starting every batch as early as possible, which loses nothing for the regular objectives here. DP1 is a def written as printed, with values in ℕ∞ and ; the minimum in the goal is an infimum in ℕ∞ over all valid feasible schedules, so its value on an infeasible prefix is .
Explicit readings of loose phrases:
Not formalized: the running time of DP1, Algorithm 1 (bisection over ) and Corollary 1, whose content is a running time. A formalization that restricts the minimum in the goal to consecutive or batch-EDD schedules would assume the milestones and is excluded; so is a DP value defined as the optimum itself.
The development needs list-based schedule recursions and ℕ∞ arithmetic only; the exchange lemmas for batch schedules (moving a job between batches without delaying later batches) are reusable for the paper's other dynamic programs. Proofs of any milestone, and of auxiliary lemmas on finish, jobCompletion and permutations of batch lists, are welcome.
The classical central limit theorem concerns sums of independent summands. Most sums that arise in statistics and applied probability are not independent: estimating equations of time-series models, stochastic approximation iterates, additive functionals of Markov chains, sequential test statistics. The standard route to asymptotic normality for such sums is to approximate them by sums of martingale differences, for which a central limit theorem holds under conditions close to Lindeberg's. McLeish's 1974 paper gives one of the shortest and most widely used proofs of such a theorem, and its conditions remain the reference form in textbooks (Hall and Heyde 1980, Chapter 3).
Timeline.
Let be a probability space. For each let be a row of real random variables, and let be sub-σ-fields belonging to row . Nothing relates the σ-fields of different rows, and the row lengths are arbitrary. Write .
The array is a martingale difference array (m.d.a.) if each is -measurable and integrable, and almost surely. Put
For real , the complex random variable is the product of Salem and Zygmund. Convergence in probability is written , convergence in is , and convergence in distribution is .
If is a martingale difference array such that (a) , (b) , and (c) , then
The proof of (2.3) goes through an abstract criterion, Theorem (2.1): for an arbitrary array, if for every real
then . The milestones are the claims of the paper's proofs of (2.1) and (2.3), in order:
The mission also states the corollaries of §2: Corollary (2.6) for near-martingales, Corollary (2.7) without moments, Corollary (2.8) under the variance normalisation , Lemma (2.11) (a Scheffé-type lemma), Lemma (2.15), and Corollary (2.13) under the Lindeberg condition and a fourth-moment condition (2.14).
Theorem (2.3) and its corollaries give asymptotic normality of martingale sums under conditions that are checked directly on the summands: the sum of squares rather than the conditional variances, and the maximum rather than a full Lindeberg condition. Through martingale approximation they yield central limit theorems for stationary ergodic sequences, Markov chain averages, stochastic approximation and the asymptotic normality of maximum-likelihood and M-estimators under dependence. Corollary (2.13) shows that under variance normalisation no conditional condition is needed at all.
The theorem is classical and proved. What this mission adds is a machine-checked version in the generality of the paper: an independent filtration per row and arbitrary row lengths. The platform already has formalized statements of martingale central limit theorems for one filtration shared by all rows, rows of length , and bounded or -negligible increments; none of these covers McLeish's array, and the truncation step, the identity for unbounded summands, and the second-moment bound of milestone 7 are not on the platform in this form.
Characteristic functions of cannot be factorised, because the summands are dependent. The natural first idea, conditioning step by step on and expanding , needs conditional second moments that are not assumed. McLeish's product avoids conditioning on characteristic functions, but itself is not bounded: can be large, and its expectation is only when the products are integrable. Any argument must therefore control the size of the products without conditional variances and without finite moments of the individual summands beyond condition (a), and must keep the martingale property intact while doing so. The passage from convergence in probability plus uniform integrability to convergence of complex-valued products, and from convergence of characteristic functions to convergence in distribution, needs measure-theoretic infrastructure that is only partly available in Mathlib.
X : ℕ → ℕ → Ω → ℝ with row lengths k : ℕ → ℕ. The column index is 0-based: the paper's is X n (i-1); only j < k n is ever constrained.Filtration ℕ m0, ℱ n; the paper's is ℱ n i, so is P[X n j | ℱ n j] and X n j is ℱ n (j+1)-measurable.UniformIntegrable … 1 P, which includes measurability and a uniform bound.TendstoInDistribution towards the law of the identity under gaussianReal 0 1.A formalization with one filtration for all rows, rows of length , or an m.d.a. predicate without integrability would state a special case or a vacuous variant of the theorem; the statements here avoid all three.
A complete development needs: products of complex random variables and their integrability, the pull-out property of conditional expectation for bounded factors, uniform integrability and Vitali's theorem for complex-valued families, and Lévy's continuity theorem. These are reusable well beyond this mission. Contributions of proofs of any milestone, of the corollaries, and of general lemmas feeding them are welcome.
In semiconductor manufacturing, finished chips go through burn-in: they are loaded on boards and held in an oven at high temperature to expose early failures. An oven holds a bounded number of boards, a load cannot be interrupted once started, and a chip may stay in the oven longer than its specified burn-in time but not shorter. Lee, Uzsoy and Martin-Vega (Oper. Res. 40(4), 1992) model the oven as a batch processing machine and give polynomial algorithms for several due-date objectives. The model has since become a standard one in scheduling theory; the survey of Potts and Kovalyov (2000) traces the batching literature that grew from it.
This mission formalizes the part of the paper's §3 on minimizing maximum tardiness when all jobs are available at time and processing times and due dates are agreeable. That is the problem the paper writes . The paper's own route is a feasibility test by dynamic programming, Algorithm DP2, which a bisection over due-date shifts turns into a minimizer.
There are jobs . Job has a processing time and a due date , both natural numbers. The machine has capacity . A batch is a nonempty set of at most jobs processed together. It occupies the machine for the processing time of its longest job,
A batch schedule of a job set is a sequence of pairwise disjoint batches covering , processed in this order and back to back from time . Batch and all of its jobs complete at . The makespan is , and the maximum tardiness is
A schedule is feasible when , that is, when every job meets its due date.
A sequence is in batch-EDD order (Definition 1) if no job in an earlier batch has a strictly later due date than a job in a later batch. Processing times and due dates are agreeable if implies . A schedule is consecutive when every batch is a block of indices and the blocks appear in increasing order.
Algorithm DP2 computes values :
Index the jobs so that and . Then for every ,
with . The minimum ranges over all schedules: any batching, any order. This is the paper's reading of as "the minimum completion time of jobs if they can be scheduled feasibly, and infinity otherwise".
DP2 is the paper's feasibility test for with agreeable data. With a bisection over the common shift of the due dates, it yields a polynomial algorithm for minimizing . A correct statement of what DP2 computes is therefore the core of that result. The same consecutive-partition structure underlies the paper's DP1 (release times, equal processing times) and DP3 (number of tardy jobs), which are separate missions of this series.
No machine-checked proof of any of these statements is known. The dynamic program's correctness is argued in the paper only by reference ("the justification of this algorithm is similar to that of algorithm DP1"), and the index order it needs is left implicit. A formal proof pins down exactly which ordering of the jobs makes the recursion correct.
The recursion charges for the last batch and checks only . Both shortcuts rely on the jobs being sorted by due date and by processing time at the same time. Lemma 3's exchange argument sorts a feasible schedule by due date, but it does not by itself produce consecutive blocks of a fixed index order. With ties in due dates the indexing also has to be compatible with processing times. Without that, the recursion is wrong: for , , it gives , while every schedule takes at least . The goal compares the DP with the optimum over all schedules, so the exchange arguments have to bridge arbitrary batchings and the consecutive ones the recursion enumerates. That bridge is the main step left to prove.
Fin n (job of the paper is index ); jobs are jobsUpTo n j. Data are natural numbers; the paper assumes integral data (p. 769).List (Finset (Fin n)); validity requires nonempty batches of size at most inside the job set, pairwise disjoint, covering the set. Batches start as early as possible. Batch time is the maximum processing time in the batch.⊤ : ℕ∞, and the goal's minimum is the infimum in ℕ∞, which is ⊤ exactly when no feasible schedule exists. DP2 is defined by the printed recursion, not as an optimum.Monotone d ∧ Monotone p for DP2 and its justification, and Monotone d for FBEDD;Minimizing the weighted number of tardy jobs on a single machine, written in later scheduling notation, is one of the basic due-date objectives: each job either meets its deadline or pays a fixed penalty, and the question is which jobs to sacrifice. Moore (Management Sci. 15, 1968) solved the unweighted case with a greedy procedure. Lawler and Moore (Management Sci. 16, 1969) handled arbitrary weights by recasting the problem as a knapsack problem with nested prefix constraints and solving it by a recursion, their Equation (3). This is the classical pseudo-polynomial algorithm for the weighted problem; Lenstra, Rinnooy Kan and Brucker (Ann. Discrete Math. 1, 1977) showed that the weighted problem is NP-hard, so a pseudo-polynomial method is the expected kind of exact algorithm.
The paper's Sections 5 and 6 state the reduction in a few sentences: on-time jobs can be taken in deadline order, the problem is "equivalent" to the prefix-constrained knapsack, and (3) solves the latter. This mission turns those sentences into precise statements.
There are jobs, processed by a single machine one immediately following the other from time . Job has a nonnegative integer processing time , a nonnegative integer deadline and a penalty . A sequence is an ordering of all jobs; job completes at time , the total processing time of job and the jobs before it. Job is tardy in if , and the total loss of is
the loss being for and for .
The jobs are numbered by deadline, . A 0–1 vector (: job on time; : tardy) is prefix-feasible if
Equation (3) defines for and integer :
with for and for .
With and , is finite and
This is the paper's claim that the problem "is solved by" its recursion, with the evaluation point made explicit.
The goal follows from milestones 2 and 3 at , .
The result is the exact algorithm for with running time proportional to , and the reduction behind it (on-time jobs in earliest-deadline order, then a knapsack over the on-time set) is the template reused by later work on due-date objectives, including the two-agent and batching variants. The prefix-constrained knapsack itself reappears whenever a set of jobs must be feasible under nested capacity limits.
On formalization: the paper's argument is three sentences long and leaves several points implicit: the base cases of (3), the role of the deadline numbering, the sign of the penalties, and what "equivalent" means. A machine-checked development fixes each of them and yields a verified pseudo-polynomial algorithm for an NP-hard scheduling problem. To our knowledge none of these statements has a machine-checked proof; the platform's SchedComplexity.OneMachine.* items (Lenstra, Rinnooy Kan and Brucker) state the NP-hardness of the same problem in another model, MooreLateJobs.NumLate.* covers Moore's unweighted case, and TwoAgentSched.LateLate.lemma_7_1 is a two-agent analogue of milestone 1.
The obvious argument works with the set of on-time jobs and asserts that this set can be sequenced on time iff its earliest-deadline order is. That step is Jackson's rule, an exchange argument on lists that is not in Mathlib; it is where both milestone 1 and the first half of milestone 2 sit. The second half of milestone 2 needs the deadline numbering: for a job that is tardy, the prefix constraint at is not a completion-time constraint of any job, and only the monotonicity for the last on-time job bounds it. Milestone 3 is a dynamic-programming correctness proof in which the cap for and the base cases must be tracked through a well-founded recursion on .
Jobs are Fin n, 0-based: Lean job is the paper's job , and the paper's uses Lean job ⟨j-1, _⟩. Sequences are lists in the published model MooreLateJobs.Shared (IsSchedule Finset.univ l, completionTime, no idle time, start at ), which replaces the paper's permutation ; tardy jobs are the published MooreLateJobs.NumLate.lateSet (strictly ). Processing times and deadlines are natural numbers, penalties real. Vectors are Fin n → Bool. takes values in WithBot ℝ, with and ; never occurs.
Explicit readings of the paper's loose phrases:
Monotone d on the job index; assumed in the goal and milestone 2 only.IsLeast over all schedules); only so that exists.Section 5 literally applies Equation (1) with , , , ; read literally, that leaves the deadlines unenforced, so the mission formalizes the paper's own corrected form (3) instead. Trivializing formalizations are ruled out: the weighted number of tardy jobs is defined from completion times, not through ; the optimum is a minimum over sequences, not defined as ; (3) keeps its cap ; the goal assumes and sorted deadlines, without which it is false.
Infrastructure: an exchange lemma for earliest-deadline order on lists (Jackson's rule, posed on the platform as MooreLateJobs.NumLate.jackson) and well-founded-recursion lemmas for WithBot ℝ maxima are reusable beyond this mission. Proofs of any milestone, and of Jackson's rule, are welcome.
Many single-machine scheduling problems have a structure that is easy to describe: the jobs must be processed in an order that is already known, and the only decisions are how and when to process each one. Lawler and Moore, in A Functional Equation and Its Application to Resource Allocation and Sequencing Problems (Management Science 16(1), 1969, 77–84), isolate this situation in its simplest form: each job has two processing modes, and each mode has its own processing time and loss as a function of the completion time. They solve it with a single functional equation, Eq. (1), closely related to the recursion for the knapsack problem.
The point of the paper is that Eq. (1) solves more than this fixed-order problem. Later sections apply it to resource allocation in critical-path scheduling and to several sequencing problems with deadlines, including minimization of the weighted number of tardy jobs, often written . Everything in those applications rests on the claim checked in this mission: that the recursion computes the minimum loss it is said to compute.
There are jobs, performed one at a time in the fixed order . Job can be performed in one of two modes. In the first mode it takes time units, and a loss is incurred if it is completed at time . In the other mode it takes time units, with loss . Times are nonnegative integers.
A mode assignment picks a mode for each job, which fixes its processing time . A feasible timing of the first jobs is a vector of completion times with
so each job starts at time or later and after its predecessor has finished; idle time between jobs is allowed. The total loss is the sum of over the jobs in the first mode and of over the others. The problem asks for the mode assignment and timing of all jobs that minimize .
The paper's recursion is defined for and integer , with values in :
For and every integer , let be the set of total losses of the first jobs over all mode assignments and feasible timings with . Then
meaning: exactly when is empty, and otherwise is an element of and a lower bound for it. No assumption is made on the losses.
If every and is monotone nondecreasing and
then is finite and equals the minimum of over all mode assignments and all feasible timings of the jobs, with no deadline. This is the paper's sentence "The problem is solved by the calculation of , where is a sufficiently large number. For example, if all of the 's and 's are monotone nondecreasing, we may choose ."
The milestone is the correctness of a dynamic program: the value table computed by (1) coincides with the optimum of a combinatorial problem whose feasible set is infinite (timings are unbounded because of idle time). The goal turns that into a finite certificate for the unconstrained problem, with an explicit horizon. Downstream, the same equation with and suitable losses is the paper's algorithm for the weighted number of tardy jobs (§5–6), and the other sequencing applications are specializations of (1) as well; a formal version of this mission is the base on which those reductions can be stated.
The result is classical and its proof is short on paper. It has not been formalized: no item on Prove2Me states a two-mode fixed-order recursion. The work this mission asks for is a machine-checked proof of the two statements above, from the paper's own definitions.
The paper gives no argument beyond "the usual dynamic programming argumentation". The recursion is in two variables: refers to itself at as well as to , so the correspondence with timings is not a plain stage-by-stage principle of optimality. The edge cases are where a careless reading fails: , where ; zero processing times or , where is evaluated at the same ; and , where the deadline constraint degenerates to . The goal is harder than the milestone: the problem's feasible set is unbounded, and the horizon is only sufficient under monotone losses. Without monotonicity the goal is false: one job with , , for and has optimum , attained only at completion time , while .
Fin n and 0-based: Lean job i is the paper's job . The recursion f takes the number of jobs done; for its value is and is never used.Bool, with true the first mode (, ). Processing times are natural numbers and may be . Losses are real-valued functions of the natural-number completion time.⊤ : WithTop ℝ, so as in the paper.Monotone on the completion time; it is a hypothesis of the goal only.The optimum is defined from the scheduling problem itself (lossesBy, IsFeasible, totalLoss), never as ; statements in which the optimum is again, timings forced to have no idle time, an -valued with an arbitrary value for , or monotone losses assumed in the milestone are all ruled out by this choice of definitions.
Related platform items: GilmoreGomory61.CuttingStock.knapsack_dp_recursion (an unbounded-knapsack recursion) and the CriticalPath.CostCurve items (Kelley's continuous time–cost model) treat neighbouring recursions and models; neither states this problem. Proofs of the milestone and the goal, and reusable lemmas about the value function, are welcome.
Exponential bounds for the tails of the binomial distribution are among the most frequently used tools in probability, statistics and the analysis of algorithms: they control the number of successes in independent trials, the deviation of an empirical frequency from its mean, and, through counting arguments, the empirical distribution function itself. The two classical bounds are Hoeffding's inequality, which ignores the variance, and Bernstein's inequality, which uses the variance but loses accuracy for large deviations. Both are recorded in Shorack and Wellner, Empirical Processes with Applications to Statistics (1986), p. 440.
In his 1990 paper establishing the tight constant in the Dvoretzky–Kiefer–Wolfowitz inequality, P. Massart obtained, as a by-product of the proof, a binomial tail bound that implies both classical inequalities and, in his words, "does not seem to be known" (Massart 1990, p. 1271). Its ingredient, a lower bound for the Cramér transform of the Bernoulli law (Lemma 1), is also used in the proof of the main DKW result. This mission formalizes that by-product: Theorem 2, Lemma 1 and the Cramér–Chernoff bound (Comment 3) through which they are combined.
Fix an integer and a success probability , and write . A random variable has the binomial distribution if it counts the successes in independent trials, each succeeding with probability : for . Its mean is . The quantity of interest is the upper tail for a deviation with (for the event is empty).
Two auxiliary functions appear in Lemma 1. For (so that ),
which is the Cramér transform of the Bernoulli law with parameter at the point , i.e. the relative entropy between the Bernoulli laws with parameters and . For ,
In the Lean development these are MassartDKW.Binom.h and MassartDKW.Binom.phi.
If has the binomial distribution and , then for every with ,
The result. Theorem 2 has the shape of Bernstein's inequality with the variance proxy replaced by the smaller ; the second factor shrinks as approaches , so the bound is sharper in the large-deviation range, and it implies both Bernstein's and Hoeffding's inequalities for binomial tails. Lemma 1(ii) is a quantitative lower bound on the Bernoulli relative entropy, with an explicit nonnegative correction term , which is reusable wherever Chernoff bounds for Bernoulli sums are converted into closed-form exponents. In the paper, the same lemma is a step of the proof of the tight Dvoretzky–Kiefer–Wolfowitz inequality.
Formalizing it. The result is proved on the page, by a short calculus argument for Lemma 1 and the classical Cramér–Chernoff computation for Comment 3. To our knowledge none of the three statements has a machine-checked proof. The work this mission asks for is formalizing that known proof: the analysis of (signs of derivatives, the limit at infinity), the inequality between and the explicit quadratic term, the exponential-moment computation for the binomial law in Mathlib's measure-theoretic setting, and the bookkeeping of the boundary cases , and .
The obvious route to Theorem 2 is to bound the binomial moment generating function and optimize; this reproduces Comment 3, and the exponent it gives is the transcendental function , not the rational expression in the theorem. The step that needs care is the comparison of with uniformly in : a second-order Taylor expansion of in gives only the local behaviour near , and a bound proved by Taylor expansion alone does not survive up to , where the second logarithm of degenerates and blows up. The endpoint therefore has to be treated as a limit.
The binomial law is Mathlib's ProbabilityTheory.binomial n p : Measure ℕ with p : unitInterval; is an -valued map on a probability space with HasLaw S (binomial n p) P. Probabilities are values of the measure in , compared with real bounds through ENNReal.ofReal. The event is the strict upper tail . The goal assumes only , as on the page: and are allowed, and the denominator is positive on the whole range.
Conventions and added hypotheses ( is written out as throughout):
A formalization that states the goal with the exponent , or assumes Lemma 1 or Comment 3 as hypotheses, or restricts to , is not this theorem: the goal carries the explicit constants and the full range .
Needed infrastructure: elementary real analysis of (derivatives, monotonicity from derivative sign, limits at infinity), the moment generating function of the binomial law (or of a sum of independent Bernoulli variables) and Markov's inequality. The bound on the Bernoulli relative entropy and the binomial Chernoff bound are reusable beyond this mission. Contributions welcome: proofs of the three milestones, and helper lemmas computing for Mathlib's binomial.
Many problems in statistics, engineering and operations research ask for the input level at which an unknown response function is largest, when the response can only be measured with noise: the dose that maximizes a yield, the setting that maximizes throughput in a simulation, the parameter that maximizes an expected reward. Robbins and Monro (1951) had shown how to find, by sequential noisy measurements, the root of an unknown increasing function. Kiefer and Wolfowitz (1952) adapted the idea to maximization: at each step, measure the response at two points placed symmetrically about the current estimate, and move the estimate in the direction of the observed difference. Their scheme is the origin of finite-difference stochastic approximation, the gradient-free ancestor of simultaneous-perturbation and zeroth-order methods in simulation optimization and machine learning.
Timeline. 1951: Robbins and Monro, root finding, convergence in mean square. 1952: Wolfowitz, convergence in probability for Robbins–Monro under weaker conditions; Kiefer and Wolfowitz, the present paper, convergence in probability of the maximization scheme. 1954: Blum proved almost-sure convergence of both schemes under related conditions (doi:10.1214/aoms/1177728794). Later work (Spall 1992, among many) extended the finite-difference idea to many dimensions.
For each level , an observation taken at is a random number with distribution ; the family depends measurably on . The regression function is the mean observation,
and the observations have uniformly bounded variance: for all . The function is unimodal about an unknown point : strictly increasing for and strictly decreasing for .
Two sequences of positive numbers (step sizes) and (probe widths) satisfy
for example , . Starting from an arbitrary number , the Kiefer–Wolfowitz process is
where, given everything observed so far, and are independent with laws and .
The paper imposes three regularity conditions on :
In the Lean development these objects are regFun H (), SecondMomentBound H S, Unimodal, Cond1, Cond2, Cond3, StepSizes a c and the structure IsKWProcess, all in the namespace KieferWolfowitz.Convergence.
This is the theorem of the paper (stated on p. 462, proved in §3 in the form (3.22)). It fixes no rate and no constants, so it is the stable form of the result.
The result shows that the maximizer of a function observable only through noise can be located consistently using function evaluations alone, without gradients and without a parametric model of . The conditions are qualitative: no differentiability, no specific noise distribution, and the noise may change shape with . This is the template for gradient-free stochastic optimization: simulation optimization with finite-difference gradient estimates, simultaneous-perturbation methods, and zeroth-order methods in learning are all analysed by refining the same bias–variance balance between the probe width and the step .
The theorem has been proved since 1952 and is not open. To our knowledge no machine-checked proof of it exists. A formalization produces a checked proof of a founding result of stochastic approximation and, along the way, the probabilistic infrastructure such proofs share: processes defined through conditional laws given a filtration, recursions for second moments, conditional Chebyshev arguments, and the passage from subsequence convergence to full convergence by a restart bound. Alternative proofs (via supermartingale convergence, which would give almost-sure convergence under stronger hypotheses) are welcome as separate developments but are not the goal.
The obvious approach is to show that decreases. It does not: the drift term is negative only on average and only once the probes straddle correctly, while the noise term is always positive and the finite-difference estimate of the slope has a bias of order . A one-step contraction is therefore unavailable, and summability arguments alone give smallness only along a subsequence; turning that into convergence of the whole sequence is where the difficulty lies, and it is also where Condition 3, which forbids flat stretches of away from , cannot be dispensed with. The argument needs integrability of quantities the paper treats as finite without comment, and the conditional statements require the conditional law of the observation pair, not just its unconditional moments.
Kernel ℝ ℝ. Every has , so and the variance in (2.2) are genuine integrals.z 0 is , a n, c n are , .TendstoInMeasure; "" for a nonnegative sequence is "below every infinitely often".BanditAlgorithm.kiefer_wolfowitz_equivalence; the two results share authors and nothing else.Useful infrastructure, reusable beyond this mission: conditional expectations of functions of a pair with a given conditional law, tail-sum bounds, and the passage from a restart bound plus subsequence convergence in probability to full convergence. Contributions of any milestone, of intermediate lemmas such as (3.7), (3.9), (3.13) and (3.29), and of the final assembly are welcome.
In a flow shop every job passes through the same machines in the same order. Choosing the order in which jobs enter the shop so that the last job finishes as early as possible (minimizing the makespan) is one of the oldest problems of scheduling theory. For two machines Johnson (1954) gave an exact sorting rule; for three machines his rule is exact only in special cases, and the general problem was later shown to be NP-hard (Garey, Johnson and Sethi, 1976). Exact methods for three or more machines therefore enumerate sequences, and the question is how to enumerate as few of them as possible.
Ignall and Schrage (1965), at the same time as Lomnicki (Operational Research Quarterly, 1965), introduced branch and bound for the three-machine permutation flow shop. Their lower bound, which adds to the time each machine becomes free the work that remains on it and the least work that must follow on later machines, became the template for the machine-based bounds used in flow-shop branch and bound ever since.
Timeline. 1954: Johnson proves the two-machine rule and shows that for three machines a common job order on all machines loses nothing for the makespan. 1960: Land and Doig introduce branch and bound for integer programs. 1965: Ignall–Schrage and Lomnicki apply it to the three-machine flow shop. 1976: Garey, Johnson and Sethi prove the three-machine makespan problem NP-hard, so exact enumeration with good bounds remains the method for exact solutions.
There are jobs and three machines , , . Job needs time on , then on , then on . Following Johnson, only permutation schedules are considered: a full sequence is a permutation of the jobs, processed in that order on all three machines, each operation starting as early as possible. Its makespan is the time machine finishes the last job.
A node is a partial sequence: an ordered list of distinct jobs. Its unscheduled set is the set of the other jobs. The attributes , , are the times at which machines , , finish the jobs of processed in order. A full sequence begins with when its first positions are . The lower bound of a node with is
The branch-and-bound procedure keeps a list of nodes ranked by , starting from the root (no job scheduled). At each step it removes the first node, creates one child per unscheduled job by appending that job, and inserts the children ranked into the list, a new node going before old nodes of equal bound. It stops when the first node of the list is terminal, i.e. has scheduled jobs, so that its last job is forced.
where is followed by its one unscheduled job. This is the paper's "the problem is solved: that node's sequence is an optimal one" (p. 402), for any real processing times.
The goal is the correctness theorem of the Ignall–Schrage algorithm: best-first search over partial sequences, with a machine-based bound, returns an optimal permutation. Milestone 1 is the bound's validity, which every later machine-based flow-shop bound generalizes; milestone 4 is the dominance rule that justifies discarding nodes; milestone 3 brackets the effort of the search between the best case and full enumeration.
The paper's arguments are short and informal: validity of the bound is asserted with a one-line reason, and optimality at stopping is argued on the example. None of these results has a machine-checked proof. The formalization makes the procedure itself a precise object (list, insertion rule, stopping rule) and turns the paper's claims into statements about it, so that the correctness of the search is proved rather than illustrated.
Each inequality is elementary, but the goal is a statement about an iterated list-manipulating procedure. The obvious argument "the first node has the smallest bound and the bound is valid" needs an invariant that the paper does not state: at every step, every full sequence begins with some node on the list, and the list is sorted. Both must be proved to survive one step of removal and ranked insertion. Termination is likewise not stated: it needs a measure that strictly decreases, for instance the set of nodes that remain to be created, which requires showing that no node is created twice. A tempting shortcut, proving optimality only among the sequences whose nodes were created, is not the theorem.
Jobs are Fin n (the paper's job is ), processing times are arbitrary reals with no sign condition, and full sequences are Equiv.Perm (Fin n). The makespan is the machine- completion time of Johnson's as-soon-as-possible schedule, taken from the published definition JohnsonFlowShop.ThreeStage.asapSchedule. Nodes are lists of jobs, and the node attributes are the same recursion folded over the list. Minima over are Finset.inf'; on an empty set the auxiliary minimum returns a placeholder that no statement evaluates.
Explicit readings of the paper's phrases:
A formalization in which the optimality claim ranges only over sequences the run created, or one that asserts optimality without termination, would be trivial or vacuous and is ruled out by the goal's statement.
Not formalized: the reduction from general schedules to permutation schedules (Johnson's Lemma 3, proved on the platform as JohnsonFlowShop.ThreeStage.same_ordering_dominant), the dominance bookkeeping and its percentages, the two-machine mean-completion problem (a separate mission of this series), the computational tables, and the TIMEB/TIMEC columns of the example's LIST table. No platform item treats flow-shop lower bounds or branch and bound over sequences; the nearest branch-and-bound mission, BiconvexProg.BranchBound (Al-Khayyal and Falk), concerns biconvex programs and is unrelated.
The lemmas a solver will want (the invariant of the list, monotonicity of the completion recursion in its start times, validity of the bound) are reusable for the two-machine mission and for any other machine-based bound. Proofs of the milestones, and of the goal from them, are welcome in any order.
The single-server queue with general independent interarrival and service times (the GI/G/1 queue) is the basic model of congestion in operations research: customers arrive at a service facility, wait if the server is busy, are served in order of arrival, and leave. The first question about any such system is whether it settles down. If customers keep arriving faster than they can be served, waiting times grow without bound; otherwise one expects an equilibrium distribution of waiting time that capacity planning, staffing and performance analysis can be based on.
D. V. Lindley's 1952 paper Lindley 1952 answered this question for the GI/G/1 queue in complete generality. It introduced the recursion for successive waiting times that now carries his name, connected the queue with a random walk, and proved that an equilibrium exists exactly when the mean service time is smaller than the mean interarrival time, with the degenerate deterministic case as the only exception. The paper is the starting point of the random-walk approach to queueing theory and of the later work of Kiefer and Wolfowitz, Spitzer, Loynes and Kingman.
Customers arrive in order at a single server; customer is served after all its predecessors. On a probability space let
Assumption 1: the are independent and identically distributed with finite mean . Assumption 2: the are independent and identically distributed with finite mean , and the families and are independent of each other.
Put ; the are i.i.d. and integrable, and denotes their common mean. The waiting time of customer (time from arrival to start of service) satisfies Lindley's recursion
Write for the waiting-time distribution function, for the law of , and for the associated random walk. Lindley shows that converges for every to
The theorem is the stability criterion for the GI/G/1 queue, and its proof identifies the equilibrium waiting time with the supremum of a random walk with negative drift. Every later result on the equilibrium waiting time (Pollaczek–Khinchine for M/G/1, Kingman's bounds, the Wiener–Hopf factorization, heavy-traffic limits) presupposes this existence statement. The critical case is the part that goes beyond the law of large numbers: there is no equilibrium even though the queue has no drift.
The result has been proved since 1952 and appears in every queueing textbook. No machine-checked proof of it is known to exist. The platform already has related open statements in other frameworks: a law-level one-step identity and the stationary-delay equation from Gross et al. (QueueingFundamentals.GG1), and Loynes' theorem in a stationary ergodic Palm framework (PalmQueueing.Loynes.loynes_stability). None of them states convergence of the customer-indexed waiting-time distributions, and none treats the critical case. This mission produces the customer-indexed model, the random-walk duality, and the complete iff, including the Chung–Fuchs recurrence theorem for one-dimensional random walks, which is of independent use.
Cases (i) and (ii) follow from the strong law of large numbers, which Mathlib provides. The obstacle is the critical case : the strong law only gives , which says nothing about whether is finite. One needs the recurrence of mean-zero random walks (Chung–Fuchs), which is not in Mathlib. A second, smaller difficulty is eq. (3): it is an identity of probabilities, not of events, since the waiting time is built from sums taken in the reverse order of the walk's partial sums. Finally, the iff needs a careful passage from pointwise limits of distribution functions to convergence to a probability measure.
All objects live in one definitions file, LindleyQueue.Stability.Model. The input is a structure Input Ω P holding measurable sequences s t : ℕ → Ω → ℝ with iIndepFun for each family, identical distribution, integrability, independence of the two families as random elements of , and nonnegativity. Theorems assume IsProbabilityMeasure P. Committed conventions:
w 0 is the paper's , F r is , U n u i is the paper's .u 0; is the push-forward law of u 0, and Stieltjes integrals are integrals over Set.Iic x.Trivializing formalizations are ruled out: the goal is about the queue's , not the random walk's absorption probabilities; the limit must be a probability distribution, since "converges to some function" is already the limit milestone; and "" is almost-sure, not pointwise. A verification file builds an Input with , so the hypotheses are satisfiable.
Needed infrastructure: exchangeability of finite i.i.d. vectors, continuity of measure along decreasing events, the strong law (in Mathlib), recurrence of one-dimensional random walks, and convergence of distribution functions. The Chung–Fuchs theorem and the random-walk duality are reusable well beyond queueing; contributions of either are welcome.
Factoring a polynomial with rational coefficients into irreducible factors is one of the basic tasks of computer algebra. Before 1982 the standard method (Berlekamp's algorithm modulo a small prime, Hensel lifting, then recombination of the -adic factors, as in Zassenhaus's approach) could take exponential time, because the number of ways to recombine modular factors grows exponentially with the number of factors. A. K. Lenstra, H. W. Lenstra, Jr. and L. Lovász gave the first deterministic polynomial-time algorithm for factoring primitive polynomials in (Math. Ann. 261, 1982). Its key idea is to replace recombination by a search for a short vector in a lattice, and the lattice basis reduction algorithm introduced for that purpose (the LLL algorithm) has since become a standard tool in number theory, cryptanalysis and integer programming.
Section 2 of the paper, Factors and Lattices, is the bridge between the two halves: it shows that an irreducible factor of can be read off from a reduced basis of a lattice built from a -adic factor of . This mission formalizes that section.
Timeline. Mignotte (1974) bounded the coefficients of a factor of an integer polynomial in terms of the polynomial itself. A. K. Lenstra (Mathematisch Centrum report IW 190/81, 1981, Theorem 2) proved the weaker statement that, under the same conditions, a short lattice vector has a nontrivial gcd with . LLL (1982) proved the sharper Propositions (2.7), (2.13) and (2.16) used here, which pin down the irreducible factor itself.
For with real coefficients, the length of is . For a positive integer , is the polynomial over obtained by reducing every coefficient modulo .
Throughout, is a prime number, a positive integer, and a polynomial of degree . A polynomial is fixed with
Write , so . Proposition (2.5) shows that has an irreducible factor with , unique up to sign; this is the factor the section recovers.
Fix an integer . The lattice is the set of polynomials of degree at most such that divides . Identifying with , is a lattice of rank with basis and determinant .
A basis of is reduced if its Gram–Schmidt data , satisfy for and for .
Assume
that is a reduced basis of , and that some satisfies
If is the largest such , then
and (2.17) holds for all .
Companion items: the basis of and (2.6), and the remark that for the vector is itself an irreducible factor of .
Proposition (2.16) is what makes the factoring algorithm of Sect. 3 correct: running the reduction for increasing , the first for which (2.15) holds produces by one gcd computation, and repeating on factors completely. Together with the polynomial running time of basis reduction (missions I and II of this series), it yields the polynomial-time factoring theorem (3.6). Proposition (2.7) on its own is a general principle, often reused: a polynomial that is divisible by modulo and has small norm relative to must share the factor with .
All results here are proved in the paper and standard in textbooks (e.g. von zur Gathen and Gerhard, Modern Computer Algebra). To our knowledge there is no machine-checked proof of (2.7), (2.13) or (2.16) in Lean or Mathlib. Mathlib has Hensel-type lemmas and the Mahler measure, including a coefficient-wise Mignotte bound and Landau's inequality, but not the form of Mignotte's bound used here, nor any of the lattice statements. A Lean development of this section would be the algebraic core of a verified LLL factoring theorem.
The obvious argument for (2.7) is to bound the resultant of and : it is divisible by when they share a factor modulo , and bounded by by Hadamard. That argument gives only , the weaker version of [8], not that divides . The paper's sharper statement needs a lattice of combinations , the projection to its top coefficients, and the congruence argument (2.11) that forces the low-degree elements of into ; formalizing it requires determinant and Hadamard bounds for a lattice of rank inside a space of polynomials.
Mignotte's bound needs the Mahler measure and the inequality , which is not the coefficient-wise form available in Mathlib. The step (2.19) needs Proposition (1.12) on reduced bases, which is the goal of mission I. The final part of (2.16) needs the primitivity of the basis vectors, which depends on being exactly the set of multiples of modulo of degree at most .
Polynomials are Polynomial ℤ; is g.map (Int.castRingHom (ZMod q)); is the square root of the sum of the squares of the coefficients over the support. Degrees are natDegree, except in (2.11), where degree with values in WithBot ℕ keeps as on the page. A polynomial of degree at most is identified with its coefficient vector in EuclideanSpace ℝ (Fin (m + 1)). Linear independence of is over on coefficient vectors; "basis for " means in , independent, and spanning over . Gram–Schmidt vectors are Mathlib's unnormalised InnerProductSpace.gramSchmidt.
Indices are 0-based: the paper's is b 0. The index of (2.16) is kept as the paper's 1-based value, , so appears unchanged. The powers , , and are real powers with real exponents.
The standing assumptions are hypotheses of every item that involves , or : prime, , , (2.1)–(2.4), . Mignotte's bound (which assumes only ) and (2.18) (pure linear algebra on polynomials of degree at most ) do not need them. The factor is any irreducible with and . A gcd is stated by its universal property (divides each, and every common divisor divides it), which determines it up to sign. Two milestones are stated slightly more generally than the page: Mignotte's bound for every divisor of degree at most , and (2.18) for every nonzero common divisor .
The goal does not assume (2.7), (2.13), Mignotte's bound, (2.18) or (2.19); these are milestones. A trivial formalization in which is an arbitrary divisor of , or in which "reduced basis" is asserted of a family that need not be a basis of , is ruled out by the definitions.
Needed infrastructure: Hensel-type arguments over , Gauss's lemma, the Mahler measure, Hadamard's inequality, and Proposition (1.12) on reduced bases. The lattice determinant results and the Mignotte bound are reusable beyond this mission. Proofs of any milestone are welcome, as are proofs of the missing Mathlib infrastructure.
A flow shop is the simplest model of a production line: every job passes through the same sequence of machines in the same order. Minimizing the time at which the last job leaves the last machine (the finish time, or makespan) is easy for two machines, where Johnson's rule gives an optimal schedule in time (Johnson 1954), and NP-hard from three machines on (Garey, Johnson, Sethi 1976; Gonzalez, Sahni 1978, §1, for preemptive schedules). For three or more machines the practical question is therefore how far a fast heuristic can be from the optimum in the worst case.
Gonzalez and Sahni (1978, §2) first show that any busy schedule, one that never leaves a processor idle while a task is available for it, has finish time at most times the optimum (their Lemma 10), and that the natural "longest job first" order does no better. They then give a heuristic, H, that uses Johnson's two-machine algorithm as a subroutine and has the better worst-case ratio (Lemma 11). This mission formalizes that bound.
A flow shop has processors and jobs. Job consists of tasks; task runs on processor and needs processing time (zero is allowed). A non-preemptive schedule gives every task a start time , and the task occupies during . It is feasible when all start times are nonnegative, when task of a job starts only after task of that job has completed (), and when no processor runs two tasks of positive length at the same time. Its finish time is the latest completion time (and if there is no task). An optimal finish time (OFT) schedule is a feasible schedule of least finish time.
Heuristic H (p. 48) divides the processors into groups: group consists of and , and when is odd the last group is alone. The flow shop on group has the same jobs, with task times only. For each group an OFT schedule of is computed (by Johnson's algorithm), with finish time . The schedule generated by H runs these schedules one after another: every task of group starts at its time in plus the offset .
For every flow shop with processors and jobs, every choice of OFT schedules of the group flow shops, the schedule generated by H, and every feasible non-preemptive schedule of the flow shop (in particular an OFT schedule ),
The paper writes this as .
The result gives a polynomial-time heuristic, running in time , whose finish time is within a factor of the optimum on every instance, half the factor that every busy schedule already achieves. The paper's Example 4 (p. 49) shows that for the factor is approached, so the analysis cannot be improved in general.
Formalizing it produces a reusable, machine-checked model of the -processor flow shop with non-preemptive schedules, its restriction to blocks of consecutive processors, and the concatenation of schedules of disjoint blocks. Lemma 11 has a short paper proof; to our knowledge it has no machine-checked proof. The model's careful treatment of zero task times, of odd , and of the restriction of a schedule to a processor group is itself part of the value: these are the points at which an informal argument is silent.
The arithmetic of the bound is short; the content lies in two structural facts about a precise model: that the concatenated object is a feasible schedule of the whole flow shop, including across the boundary between consecutive groups and for a final group of a single processor, and that the optimum of the whole flow shop is at least the optimum of each group flow shop, whose first processor has no predecessor. Informal arguments are silent on exactly these points. A naive formalization that leaves the offsets free, or that does not require the to be optimal, makes the statement false; one that lets be any schedule with the right restrictions makes it witnessed by itself.
The existence of OFT schedules for the group flow shops (milestone 1) is a separate matter: the paper takes it from Johnson's algorithm, and proving it requires an optimality argument for two-machine flow shops (or a compactness argument over finitely many processing orders).
Fin m and jobs Fin n, both 0-based; times are real numbers. A flow shop is a matrix t : Fin m → Fin n → ℝ with t ≥ 0. A schedule is a matrix of start times. Group (0-based, g : Fin ((m + 1) / 2)) contains the processors and that exist, min 2 (m - 2g) of them.max with baseline over all tasks; it is for or . The maximum of the group finish times is also a fold of max with baseline . No supremum over an unbounded or empty set is taken.(m + 1) / 2 in , cast to ; the two agree for every . The ratio is multiplied out, so a zero optimum does not divide by zero.Finset.fold max and sums over Fin; nothing beyond Mathlib. Contributions proving milestone 1 by formalizing Johnson's rule for this model are welcome and reusable.Ulam asked, in the early 1960s, how long the longest increasing subsequence of a random permutation typically is. The question is a test case for a whole class of problems in combinatorial probability: a quantity defined by an optimisation over exponentially many configurations (here, all subsequences) whose typical size has to be found without enumerating them. The same structure appears in last-passage percolation, in the patience-sorting card game, in sequence comparison, and in scheduling problems where the longest chain of a random partial order determines a makespan.
J. F. C. Kingman's IMS Special Invited Paper Subadditive ergodic theory (Ann. Probab. 1 (1973), 883–899) presents Ulam's problem in §2.4 as an application of the subadditive ergodic theorem, following J. M. Hammersley, and then proves explicit bounds on the limiting constant. This mission formalizes those bounds.
Timeline.
Let be the group of permutations of . For , a sequence of positions is ascending if . The length of the longest ascending sequence, , is the largest such .
The uniform distribution on gives each of the permutations probability , so an event has probability . Let denote a permutation drawn from this distribution. The sequence converges in probability to a real number if, for every ,
For integers , denotes the number of ascending sequences of length in . For write
the exponent appearing in Kingman's condition (2.4.8). (The paper calls the second variable ; in Lean it is , because also names the constant below.)
Let be the limit in probability of . Let be the unique positive root of , and . Then
and hence
Numerically and . The goal states (2.4.4) and (2.4.5) as printed, together with the existence and uniqueness of .
The result. Theorem 8 was, at the time, the sharpest rigorous information about Ulam's constant. Its upper bound comes from a first-moment computation that applies to any random structure in which long increasing chains can be counted; the same calculation bounds the longest chain in random partial orders and the height of random -dimensional orders. The lower bound shows that a greedy path through a Poisson process already achieves a positive fraction of the optimum, an argument reused for last-passage percolation models.
Formalizing it. All results here are proved in the literature; none is open. To the best of our knowledge none of them has been machine-checked. A complete development produces: an exact non-asymptotic tail bound on the longest increasing subsequence ((2.4.7)), useful on its own; a Stirling-type asymptotic for products of binomial coefficients at scale ; and, through Theorem 7, a formal existence proof of the Ulam constant. Theorem 7 is the substantial piece: the paper's proof is a sketch through a continuous-parameter subadditive ergodic theorem and a planar Poisson process.
The upper bound needs care with asymptotics: (2.4.7) holds for each , but the passage to (2.4.8) uses Stirling's formula with and integers tending to infinity at rate , and the infimum in milestone 7 is not attained (the admissible set is open), so the argument must produce, for every , a suitable .
The lower bound is where the obvious approach fails. A first-moment or counting argument gives only upper bounds on ; a lower bound requires exhibiting long ascending sequences. The paper's argument does this with a greedy path in a planar Poisson process, which is not a statement about uniform permutations and needs the Poissonization of Theorem 7 to transfer back. Proving directly from the counting definition of is not available. Both bounds also need the existence of , which is Theorem 7.
Equiv.Perm (Fin n); the permutation is named in Lean because is Real.pi.Needed infrastructure: counting arguments on Finset.powersetCard; Stirling's formula (Mathlib has Stirling.tendsto_stirlingSeq_sqrt_pi); elementary calculus for the root ; Gaussian-type integrals on the quadrant. Theorem 7 additionally needs Poisson point processes in the plane, which Mathlib lacks, or another route to the existence of the limit. Contributions of that infrastructure are welcome and reusable well beyond this mission. The counting bounds (milestones 3–5) are independent of Theorem 7 and are a natural first target.
Many random growth models attach a cost, distance, or accumulated quantity to each time interval. If the quantity over a long interval is at most the sum over two adjacent intervals, it is subadditive. A stable rate over long intervals is useful even when the underlying random system does not have a simple independent-increment description. Kingman's 1973 account places percolation and products of random matrices among the applications of this framework. Its basic theorem treats integer time; the present mission concerns the change to every nonnegative real time. Kingman, §1.1 and §1.4.
The change matters because observing a process at integer times can miss arbitrarily large behavior between observations. Kingman gives a smooth stationary-increment example in Theorem 3 where no prescribed increasing bound eventually controls the values at all real times. Theorem 4 gives a condition that does control this local behavior. These two results together explain why the continuous-time statement needs more than a formal change of index type. Kingman, Theorems 3–4.
Work on a probability space . A continuous-parameter subadditive process is a family of real random variables indexed by . It satisfies whenever . Its stationarity says that, for every real shift , the complete shifted family has the same joint distribution as . Finally, the mean exists as a finite real number for each and obeys for one constant . These are the continuous-time versions of Kingman's conditions S₁, S₂, and S₃. Equality of the law of each individual coordinate would be too weak for S₂. Kingman, pp. 883–884, 887.
For an interval , the oscillation is . A process has the local oscillation condition when for one nondegenerate interval . In §1.4 the paper states that this condition then holds on every bounded interval. The quantity is the mean growth rate. Kingman, (1.4.1), (1.4.6)–(1.4.7).
The paper also requires separability. Here this means that, outside one probability-zero set, the value at every admissible pair of times can be approached along a sequence from a fixed countable dense set of pairs. It is a condition on how the uncountable family is observed, and it permits discontinuous sample paths. Kingman cites the standard separability convention without defining it in §1.4; the mission makes the convention explicit. Kingman, Theorem 4 and following discussion.
For a separable process satisfying S₁–S₃ and the local oscillation condition, the target is an integrable real random variable such that
The time variable ranges over all real values tending to infinity. The integer-time assertion (1.4.8) is a separate milestone, not the goal. Other milestones identify the deterministic mean rate, extend the oscillation condition to bounded intervals, record the bounds at times between consecutive integers, and state the vanishing of normalized unit-interval oscillation. Each comes from a sentence or display in §1.4. Kingman, Theorem 4 and proof.
Theorem 4 gives a long-run rate for a broad stationary subadditive family without assuming that its trajectories are continuous or differentiable. Its mean statement identifies the expectation of the random limit with a deterministic infimum of normalized expectations. The paper notes that the usual continuous-time ergodic theorem for additive integral processes is a corollary, because such processes satisfy its oscillation condition. The condition is therefore compatible with familiar additive models while also covering discontinuous subadditive ones. Kingman, p. 890.
The theorem and its argument are known from the paper; this mission asks for a machine-checked development of the stated result. A completed development would provide reusable formal interfaces for joint-law stationarity of an uncountable family, separability, extended-valued oscillations, and almost-sure plus limits. The proposed theorem statements compile as open goals; compiling them does not prove them. Kingman, §1.4.
An integer-time subadditive theorem controls only on its discrete skeleton. It cannot by itself rule out large values of for times between consecutive integers; Theorem 3 shows that such behavior can occur even with smooth stationary sample paths and finite expectations. A continuous-time result must control local variation as the observation window moves to large times. The uncountable supremum in also needs a genuine extended value and a measurability convention. Kingman, Theorems 3–4.
The paper's displayed assertion (1.4.1), that converges as real under S₁–S₃ alone, needs qualification: a discontinuous additive function can make a deterministic subadditive mean with no such limit. The corresponding milestone includes the finite-oscillation condition assumed by Theorem 4. This correction is disclosed in the theorem's formalization note. Kingman, (1.4.1), (1.4.7).
Lean indexes the family by and uses only ; values at other pairs carry no meaning. Each valid coordinate is measurable. S₁ is pointwise in the sample point, while S₂ is equality of the probability laws of the complete path before and after every nonnegative real shift. S₃ states integrability of for every and one linear lower bound on its mean. The sample-space type is called so that denotes oscillation without ambiguity.
Oscillation is valued in the extended nonnegative reals. Thus an unbounded supremum is infinite, and the expected-oscillation condition cannot hold because of a default real-supremum value. Separability is the countable graph-approximation condition outside one measurable null set. The premise is finiteness on one closed interval with ; the propagation milestone covers bounded intervals with either choice of endpoints. The limit in Theorem 4 uses the filter at infinity on real time. Its almost-sure convergence and convergence in mean are separate clauses, and is integrable. No continuity of paths, ergodicity, or independence is assumed.
A complete proof may build on Mathlib's measure theory, filters, Borel–Cantelli lemmas, and real analysis. The process and oscillation definitions, along with the finite-oscillation and skeleton statements, are reusable beyond this particular theorem. Contributions that establish these interfaces and the named intermediate statements are within scope. A statement limited to integer times, a marginal-only version of stationarity, or a real supremum that returns a default value on an unbounded set would not express this target.
Kingman's subadditive ergodic theorem (Theorem 1 of Kingman 1973, first proved in Kingman 1968) says that for a discrete-parameter subadditive process the ratio converges with probability one and in mean. Applications in first-passage percolation, products of random matrices and longest increasing subsequences often come with a continuous time parameter, so it is natural to ask whether the theorem holds with ranging over .
Section 1.4 of the 1973 paper answers this question. Under separability alone, a continuous-parameter version would contain, as its additive special case, the claim that every separable process with stationary increments and finite expectations has a finite limit with probability one. Kingman remarks that no such theorem appears in the literature, "for the excellent reason that the conclusion is false, and in a very strong sense" (p. 888). Theorem 3 makes that sentence precise. It is the reason the continuous-parameter theorem of the paper (Theorem 4) carries an extra integrability hypothesis on the oscillation .
A real-time process is a family of real random variables on a probability space . Its joint law is the law of the path on with the product -algebra, that is, the collection of all finite-dimensional distributions.
A growth bound is a function that is increasing (non-decreasing). The event " for all sufficiently large " is the set of for which some exists with for every real .
In the Lean development these notions are IsStationary, HasStationaryIncrements, Integrable (y t) P and ContDiffOn ℝ ∞ (fun t => y t ω) (Set.Ici 0), all in the namespace KingmanSubadditive.StationaryIncrements.
For every positive non-decreasing on there are a probability space and a process with stationary increments, finite expectations and sample functions such that
The quantifiers are "for every there exists ". Because may grow arbitrarily fast, no normalization with a deterministic can converge to a finite limit almost surely.
The milestones are the four steps of Kingman's proof, stated for the explicit process of (1.4.5) built from a bump function , a uniform and independent integer-valued with a law that depends on :
The result. Theorem 3 rules out any continuous-parameter subadditive ergodic theorem whose only hypotheses are separability, stationarity of the increments and finite means, and in fact any such theorem whose hypotheses are met by smooth stationary processes with finite means. The obstruction does not come from irregular paths: the counterexample is as regular as a path can be short of analyticity. Any continuous-time ergodic theorem therefore needs a hypothesis that controls the behaviour of the process inside unit intervals, such as in Theorem 4, or the integrability of in the classical continuous-parameter ergodic theorem. The result also separates two kinds of time. Along the integers, a stationary-increment process with finite mean is an additive discrete process, so converges almost surely; Theorem 3 shows that the real-time path can still escape any envelope between the integers.
Formalizing it. The theorem is classical and its proof is complete in the paper. To our knowledge it has no machine-checked proof. A formalization requires the existence of a probability space carrying a uniform variable and an independent i.i.d. sequence with a prescribed law on the integers, the joint-law notion of stationarity for real-time processes, a stationarity argument for a randomly shifted process, an expectation computation with a change of variables, and the second Borel–Cantelli lemma. The definitions of stationarity and stationary increments for real-time processes on are reusable beyond this mission.
The natural first attempt is a process with linear or polynomial growth, such as with a heavy-tailed integrable . Every such attempt fails against a that grows faster, so the process must depend on . A process that is large on a whole interval of length one cannot have finite mean when grows fast. The difficulty is to have excursions that are taller than any prescribed envelope infinitely often, and still keep finite expectation, stationarity in real time and smoothness. In the formal proof, the stationarity step is where most of the work sits: the shifted path must be identified in law with the original one for every real shift , not only for integer shifts.
y : ℝ → Ω → ℝ, with values at ignored; lives in Type. Every with is measurable, and both stationarity definitions include almost-everywhere measurability, so Measure.map never takes its junk value.Set.Ici (0:ℝ) → ℝ with the product -algebra. Stationary increments compare the laws of and for every real .MonotoneOn Γ (Set.Ioi 0)), which gives the stronger theorem. is a total function on ; its values at are irrelevant.ContDiffOn ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) on for every . This is , not the analytic order.Contributions welcome: proofs of the milestones, a general lemma that a uniformly shifted process built from an i.i.d. sequence of unit blocks is stationary in real time, and a proof of the goal.
Flow shops and job shops are the basic models of multi-stage production: every job passes through several machines, and each machine handles one task at a time. Gonzalez and Sahni (Operations Research 26(1), 1978) showed that minimizing the finish time of such shops is NP-complete even with preemption, and then asked how well simple heuristics do. One of the two objectives they study is the mean flow time, the average completion time of the jobs, which measures how long a job spends in the shop on average.
Their Lemma 9 analyses the most natural rule for that objective, shortest processing time first (SPT): process the jobs in order of nondecreasing total work. For a single machine SPT is optimal (Smith 1956; Conway, Maxwell and Miller, Theory of Scheduling, 1967, p. 76, which the paper cites). Lemma 9 shows that with processors the same rule loses at most a factor , and the paper's Example 2 shows that the factor is attained in the limit.
A job shop has processors and jobs. Job is a finite sequence of tasks; each task names the processor that must process it and a processing time . The tasks of a job are processed in their order: a task may start only after the job's previous task has completed. A flow shop is the special case in which every job has tasks and its -th task runs on .
A non-preemptive schedule gives every task a start time ; the task then occupies its processor during , and two distinct tasks on one processor never overlap. The finish time of job in schedule is the time at which all tasks of job have been completed, and the mean flow time is
An OMFT schedule is a feasible schedule of least mean flow time.
Let be the sum of the task times of job . An SPT order is a listing of the jobs with , ties broken arbitrarily. The SPT schedule processes the jobs in that order: each job in turn, each positive-time task starting at the later of the completion of the job's previous task and the latest completion of a task already placed on its processor. A zero-time task completes when its preceding task completes and leaves the processor available.
For every job shop, every SPT order with SPT schedule , and every feasible non-preemptive schedule ,
so that for an OMFT schedule . A separate item states the same bound for flow shops.
The milestones follow the paper's proof of Lemma 9 on p. 47:
Lemma 9 is one of the earliest performance guarantees for a shop-scheduling heuristic under a sum objective. It shows that a rule computable by one sort, plus a linear pass, is within a factor equal to the number of machines, independently of the number of jobs. This is better than the factor that Lemma 8 of the same paper gives for an arbitrary busy schedule, whenever . Example 2 of the paper shows that the factor cannot be improved for SPT. Lower bounds of the work-per-machine type used here recur in later approximation results for total completion time in shops and on parallel machines.
The result has been proved since 1978. As far as a search of the Prove2Me catalogue shows, it has not been machine-checked. This mission adds a machine-checked statement of the SPT schedule as an algorithm, not as an arbitrary schedule with a property. It also adds the guarantee for job shops with arbitrary task sequences, of which flow shops are a special case.
The arithmetic of the proof is short. The work is in two places. The SPT schedule is a concrete construction, a fold over jobs and tasks that updates processor availability, so the bound on its finish times has to be carried through an invariant of that construction. The lower bound on every feasible schedule needs a packing argument: tasks on one processor that complete by a given time have total length at most that time. That argument is not available in Mathlib in a form that applies here. The tempting shortcut of comparing the two schedules job by job fails: the optimal schedule need not finish jobs in SPT order, so the comparison must go through sums of sorted prefixes.
JobShopLTAS.Core.Instance (jobs Fin n, processors Fin m, tasks Fin (μ j), real processing times ). The local IsPaperFeasibleSchedule requires nonnegative starts, in-job order, and no overlap of positive-time tasks on the same processor. Zero-time tasks occupy no processor interval. The paper assumes , and the scheduling theorems carry that hypothesis.In a job shop, each job has an ordered list of tasks, and each task must use a specified machine. A production planner may be able to interrupt a task and resume it later, yet still be unable to find a short schedule efficiently. Gonzalez and Sahni studied how the ability to preempt changes the difficulty of minimizing the time at which all jobs are complete. Their 1978 paper establishes complexity results for flow shops and job shops and then examines approximation schedules when exact optimization is difficult (Gonzalez and Sahni, 1978).
This mission concerns the paper's two-machine construction from 3-PARTITION. It is the reduction used for their claim that finding an optimal preemptive or non-preemptive finish-time schedule remains NP-complete when input size is measured by the sum of task lengths. The formal target isolates the decision equivalence proved for the constructed instance. It gives solvers a precise schedule statement to establish without conflating the scheduling theorem with the separate complexity-class argument.
A 3-PARTITION input comprises an integer , a positive integer target , and positive integer sizes . A valid input satisfies
It has a 3-partition when the indices can be assigned to disjoint groups, each containing exactly three indices and having total size . The strict bounds rule out groups of other cardinalities at that sum and are part of the source problem, not a convenience added for formalization. When , the input has no sizes or groups and the empty grouping is a solution.
The paper builds a job shop with machines and jobs. For , job has a task of length on , followed by a task of length on . The last job, , has tasks, each of length . Its tasks alternate between the machines, starting on . This last order matters: reversing it would produce a different construction. The source gives the decision threshold (Lemma 7, p. 44).
A non-preemptive schedule gives each task one continuous processing interval. A preemptive schedule may divide an operation into finitely many positive-length intervals. In either case, jobs obey their task order, distinct pieces on the same machine do not overlap, and processing starts at or after time zero. Write for the time at which all tasks of schedule have finished. The paper allows the same job to revisit a machine, as the final job does here.
For every valid , the main goal states both the paper's preemptive equivalence and the non-preemptive form established by its two directions:
The milestones follow the source's proof text: the schedule supplied by a solution in Lemma 7(a), the timing forced on the final job, the exclusion of short preemptive schedules in Lemma 7(b), and the preemptive equivalence stated in the proof. The final-job milestone describes the occupied time slots of the paper's Figure 4, independently of how many adjacent pieces a formal schedule uses.
The equivalence transfers the distinction between solvable and unsolvable 3-PARTITION inputs to an exact finish-time threshold in a job shop with only two machines. It also establishes the non-preemptive decision equivalence for this construction, because a solution yields a non-preemptive schedule while an unsolvable input rules out even the more permissive preemptive schedules. These facts supply the scheduling part of the paper's strong NP-completeness claim; membership in NP is handled separately by Lemma 6 (pp. 44–45).
The result is proved in the source paper. The work proposed here is a machine-checked development of its explicit reduction equivalence and the finite-piece scheduling model needed to state it. The milestone theorems expose statements that can be reused when formalizing other preemptive scheduling reductions. The shared job-shop instance and 3-PARTITION input are already published definitions; the particular reduction instance and preemptive schedule predicate are new local definitions.
Preemption makes a task's processing time distributable across intervals. Merely checking that each machine has enough total capacity does not characterize feasible schedules: every job's operations must still occur in order, and pieces of different jobs must avoid one another on each machine. The converse direction must constrain every preemptive schedule that meets the threshold, not only a schedule having the visual pattern in Figure 4. A schedule can also represent one uninterrupted interval as several adjacent pieces, so piece count alone cannot express the source's timing claim.
Machines are Fin 2, with numbered and numbered . Jobs are Fin (3t+1); the final job is index . Its zero-based operation uses machine for even and machine for odd . The definition uses the published JobShopLTAS.Core.Instance for ordered operations, machines, real processing times, and non-preemptive feasibility. It uses the published ResourceScheduling.Chain.ThreePartition for , validity, and solutions. Those objects have the same conventions as the paper here. The local preemptive model uses finitely many positive-length pieces per task, whose durations sum exactly to that task's processing time. The threshold is the explicit real cast of ; no real infimum or division by a possibly zero optimum appears.
The goal is specific to the instance the paper constructs from each valid input. A free job-shop instance, a freely chosen schedule, or an extra hypothesis that the input has a solution would erase the reduction's content. Validity carries , total , and both strict bounds on each . The case remains in scope: the constructed job has no tasks and its finish-time threshold is zero. All existing tasks have positive length whenever the input is valid, so the published non-preemptive predicate's treatment of zero-length tasks does not affect this mission.
The paper states “3-Partition preemptive JOFT with ” and connects it to NP-completeness for preemptive and non-preemptive scheduling when complexity is measured by the sum of task lengths. The Lean theorem states the proof's two decision equivalences with constant and machine count . It does not formalize as a polynomial-time many-one reduction, the unary task-length measure, NP-completeness, or Lemma 6's NP-membership argument. Contributions that establish the reduction statements, the schedule construction, or general finite-piece scheduling facts are within scope.
Shop scheduling asks how to process a set of jobs, each a sequence of tasks on prescribed machines, so that all work is completed as early as possible. The flow shop, in which every job visits the machines in the same order, is the most studied of these models in operations research. For two machines, Johnson's rule (1954) computes a schedule of minimum finish time in time, and for two machines allowing interruptions (preemption) does not help. Garey, Johnson and Sethi (Math. Oper. Res. 1976) and Brucker, Lenstra and Rinnooy Kan (Mathematisch Centrum report BW 43/75, 1975; Ann. Discrete Math. 1977) showed that the non-preemptive problem becomes NP-complete with three machines.
Gonzalez and Sahni (Operations Research, 1978) extended this picture to preemptive schedules. Their Theorem 1 shows that minimizing the finish time of a three-machine flow shop is NP-complete with or without preemption, even when every job has at most two tasks of nonzero length. When every job has only one task the problem is trivial, so this is the simplest NP-complete case of the flow-shop finish-time problem. The result explains why no exact polynomial algorithm is expected and motivates the approximation results in the second half of the same paper.
Timeline:
A flow shop has processors and a finite set of jobs. Task of job must be processed on for time units, and it can start only after task of the same job is completed. Task times may be zero. The schedule starts at time .
A preemptive schedule gives every task a finite set of pieces with : the task is processed on its processor during . Pieces on the same processor do not overlap, the pieces of a task have total length , and every piece of a task starts after every piece of the earlier tasks of the same job has ended. A non-preemptive schedule processes every task in at most one piece. For a schedule , is the time at which job is completed and the finish time is .
PARTITION. A multiset of nonnegative integers has a partition if some set of indices satisfies .
The instance FS. With , the flow shop has processors and jobs:
and the threshold is . Every job has at most two nonzero tasks.
For every and every :
The result. The equivalence shows that a polynomial-time algorithm deciding whether a three-machine flow shop (with two nonzero tasks per job) has a schedule of finish time at most , preemptive or not, would decide PARTITION in polynomial time. With membership in NP (the paper's Lemma 2) it gives NP-completeness of both versions. It also marks the boundary with the polynomial cases: (Johnson's rule), and jobs with a single task.
Formalizing it. The result is proved in the paper; nothing here is open. To our knowledge no machine-checked proof of this reduction exists, and the platform has no formal model of preemptive shop schedules. The mission produces one: a piece-based preemptive schedule with zero task times, which subsumes the non-preemptive case, together with the first formal NP-hardness reduction for preemptive flow shops on the platform.
Direction (a) asks for one explicit schedule. Direction (b) must rule out every preemptive schedule of FS, and preemption is exactly what makes this delicate: a task may be split into any finite number of pieces placed anywhere on its processor, so the naive intuition that a failed partition leaves "unusable gaps" is no longer evident, since pieces of different jobs can be interleaved to fill gaps. A correct argument must therefore be an accounting of processor time over the pieces, valid for any number and position of pieces, and it must treat zero-length tasks, which occupy no processor time but still delay the next task of their job. Finally, the non-preemptive equivalence is not a formal consequence of the preemptive one alone: it uses that (a) produces a non-preemptive schedule and that (b) holds for all preemptive schedules, which include the non-preemptive ones.
Fin 3 ( = 0, 1, 2), jobs of FS are Fin n ⊕ Fin 2 (Sum.inr 0 is job , Sum.inr 1 is job ). Task times are real numbers; the PARTITION data are a : Fin n → ℕ, and "has a partition" is in .Finset of pieces per task with the four conditions of the Setting. Non-preemptive means at most one piece per task. Zero tasks have no pieces and occupy no processor time. and are maxima with baseline .A finite Markov decision system asks how to choose actions while a changing state controls which actions are available. The choice can affect both the reward now and the distribution of future states. In a total-reward problem, the process can continue indefinitely; if transitions are substochastic, it can also terminate. Kallenberg's treatment of positive dynamic programming connects this control problem to a finite linear program and uses an optimal flow to identify a policy that is optimal from every initial state Kallenberg, Chapter 3.
The connection matters when an optimizer is easier to compute as state-action frequencies than as an infinite sequence of decisions. A policy may depend on the entire observed history and may randomize at every decision. The theorem under study says that, when the dual linear program has an extreme optimal solution, its positive coordinates identify a pure stationary policy as good as every such general policy. This assertion includes models in which the selected policy is not transient Kallenberg, Theorem 3.5.2 and Example 3.5.1.
Let be a nonempty finite state space. At state , one chooses an action from the nonempty finite set . Action earns a real reward and moves to state with probability . The sum is at most one; any missing probability represents termination. Positive dynamic programming imposes for every admissible state-action pair Kallenberg, Section 2.2 and Assumption 3.5.1.
A policy assigns an action distribution after each finite history. The history records the initial state and all states and actions observed so far. Write for this full policy class. A pure stationary policy always chooses one fixed admissible action whenever it visits .
Starting from state , let be the expected total reward of , and let . Because the rewards are nonnegative, the finite-horizon expected totals increase to ; both policy and optimal values may be . A real vector is TMD superharmonic if for each and Kallenberg, Definition 3.3.1.
For given weights , equation (3.5.2) is a linear program over nonnegative state-action flows . It maximizes subject to
The set records the states with positive flow Kallenberg, Notation 3.1.1 and equation (3.5.2).
Theorem 3.5.1 identifies as the smallest nonnegative TMD-superharmonic vector. The original superharmonic definition ranges over real vectors; the value must also be allowed to take . The formal statement gives both the extended superharmonic inequalities for and its componentwise bound by every nonnegative real superharmonic vector:
This is the numbered milestone of the mission Kallenberg, Theorem 3.5.1.
The main goal is Theorem 3.5.2. Suppose is an extreme point of the feasible region of (3.5.2) and has objective at least as large as every feasible flow. Then every pure stationary rule choosing on , with arbitrary admissible actions outside , is total optimal:
The goal records the finite-optimum case by requiring an actual optimal solution ; it makes no extra assumption that every policy is transient Kallenberg, Theorem 3.5.2.
The theorem converts an extreme optimal state-action flow into one decision rule that is optimal simultaneously for all starting states. Since includes policies that change with time, use full histories or randomize, it establishes that those freedoms cannot improve the total-reward value when the stated dual optimizer exists. The positive model also reveals when extended values matter: outside the finite-optimum case, the dual objective may be unbounded and an optimal total reward may be infinite Kallenberg, pp. 78–83.
A formal development of this result must keep the policy class and the linear program in the same model. It provides reusable definitions of a finite substochastic control system, finite-history probabilities, extended total rewards, state-action flows and superharmonic vectors. The result is proved in the book; the mission asks for a machine-checked proof of its statement, not for a new optimization theorem. The draft statements are open goals until such proofs are supplied.
A finite linear program has finitely many variables, while the value compares a flow-derived rule with every infinite, history dependent policy. A comparison restricted to stationary or transient policies would miss the main assertion. The proof also has to treat zero-flow states: the dual solution does not prescribe an action there, yet the theorem permits every admissible choice. Finally, the superharmonic milestone permits an infinite value, while the linear program itself uses real coordinates. A development must connect those representations without turning an infinite reward into an arbitrary default real value.
Lean represents states as Fin N with , and each as a nonempty finite subset of a finite action type. The transition rows sum to at most one. Histories carry past states and actions, and the first action has internal index zero, corresponding to the book's time one. Policy probabilities are nonnegative, vanish outside and sum to one. The expected reward of a finite horizon is a finite sum over histories; nonnegative total reward is its supremum in EReal. The value takes the supremum over the full policy type, not over a restricted policy subclass.
Dual flow coordinates exist only for admissible state-action pairs. Extreme points are taken in the feasible set of (3.5.2) in those coordinates, and its balance constraints retain the source's direction. The goal quantifies over every admissible pure rule satisfying the positive-flow condition. These choices exclude the vacuous shortcut of defining the value using only pure stationary policies or assuming optimality as a hypothesis.
The mathematical infrastructure includes finite policy histories, state-action occupancy probabilities, extended nonnegative reward limits, the real flow polyhedron and its extreme points. The history and flow definitions can support later work on other finite decision models. Contributions to those foundational results and to the full comparison with history dependent policies are within the mission's scope. The negative-reward regime of Section 3.6, whose claims involve average optimality and recurrent classes in an extended stochastic model, requires its own representation and is outside this positive-reward target.