All missions

Why graph dimension matters

A finite graph has distances defined by the lengths of its shortest paths. Representing those distances inside a normed vector space lets geometric language describe a combinatorial object, but the number of coordinates required can depend sharply on the graph. The isometric dimension asks for the smallest dimension of any real normed space that preserves every graph distance exactly. Linial, London, and Rabinovich study this invariant alongside metric embeddings and algorithmic uses of graph geometry in their 1995 paper. The cube is a useful test case: its vertices already have an obvious coordinate description, while the theorem must show that no different norm compresses those exact distances into fewer coordinates.

The paper's Section 5.3 relates isometric dimension to the rank of a matrix recording vertex distances in a maximum norm. It then computes the dimension of an even cycle and uses an isometric cycle inside the cube. These are known results of the paper, not an open conjecture. The mission isolates the rank characterization, the cycle calculation, and the cube calculation as reusable formal targets.

Graphs, norms, and the cube

For a finite connected simple graph $G=(V,E)$, let $d_G(x,y)$ be the minimum number of edges in a path from $x$ to $y$. A norm $N$ on $\mathbb R^d$ is nonnegative, vanishes only at zero, satisfies $N(av)=|a|N(v)$, and obeys $N(u+v)\leq N(u)+N(v)$. An isometric embedding is a map $\varphi:V\to\mathbb R^d$ such that $N(\varphi(x)-\varphi(y))=d_G(x,y)$ for every pair of vertices. The number $\dim(G)$ is the least $d$ for which some norm and some such map exist. The paper states the more general metric-space definition in Definition 2.1 and adopts connected graphs as the standing convention in Section 5.1 (pp. 218–219, 229).

The $m$-cube has binary strings $x=(x_1,\ldots,x_m)$ as vertices. Two strings are adjacent when exactly one coordinate differs. Its graph distance is the Hamming distance, the number of differing coordinates. For $m\geq2$, the even cycle $C_{2m}$ has $2m$ vertices in cyclic order, each adjacent to its two neighbors. A graph $J$ is an isometric subgraph of $G$ when its distances between its own vertices agree with their distances in $G$.

An $|V|\times r$ real matrix $M$ implements $G$ when the maximum absolute coordinate difference between rows $i$ and $j$ is $d_G(i,j)$, for every pair. The number of columns $r$ is allowed to vary; the matrix rank is its ordinary linear-algebraic rank. This is the matrix object in Theorem 5.7, p. 232.

Formalization targets

The first main intermediate target is the rank characterization

$$\dim(G)=\min_{M\text{ implements }G}\operatorname{rank}(M).$$

The next is the even-cycle result, stated for $m\geq2$:

$$\dim(C_{2m})=m.$$

The goal is Corollary 5.12, p. 233, for every positive integer $m$:

$$\boxed{\dim(m\text{-Cube})=m.}$$

The milestone list also records the isometric-subgraph lower bound, the nonsingularity of the distance matrix of a path, an isometric embedding of the cube into $\ell_1^m$, and an isometric $C_{2m}$ inside the cube. The paper's proof of the corollary names the last two facts in consecutive sentences (p. 233).

What the result establishes

The upper bound says the familiar $m$ binary coordinates suffice: the cube embeds in $\ell_1^m$ with all distances preserved. The lower bound is stronger than a claim about that particular norm or embedding. It rules out every real normed space of dimension below $m$, regardless of its norm. The even cycle provides a separate exact dimension calculation, while Theorem 5.7 gives a matrix-rank way to study other finite graph metrics. These statements separate the graph invariant from whichever embedding happens to be easiest to draw (Section 5.3, pp. 232–233).

The paper proves these claims mathematically. The remaining formalization work is to build machine-checked proofs of their precise statements, including the finite-dimensional norm interface, graph-distance calculations, implementing matrices, and the rank lower bound. The definitions of normed realization and implementing matrix can be reused for other graphs; the path-distance determinant can be used independently of graph embedding questions. The mission's theorem files are open proof targets, not claims that these proofs have already been checked in Lean.

Where the difficulty lies

Placing binary cube vertices in $\ell_1^m$ gives an immediate candidate for an upper bound, but it cannot by itself exclude embeddings into lower-dimensional spaces with a different norm. The lower bound has to control all norms. Theorem 5.7 converts that unrestricted geometric question into a rank statement for every implementing matrix, and Proposition 5.10 supplies the exact cycle dimension needed by the cube argument (pp. 232–233).

The paper's printed proof of Proposition 5.10 first obtains only $\operatorname{rank}(A)\geq m-1$, then says a more careful analysis yields $m$ without spelling it out. That final rank step is a genuine proof obligation for solvers; the stated proposition and its use in Corollary 5.12 are retained exactly (p. 233). The path-distance matrix cited in that proof is nonsingular when its size is at least two; size one would be a zero matrix.

Formalization scope

Lean represents an arbitrary $d$-dimensional real normed space by a norm function on Fin d → ℝ. This includes every finite-dimensional real normed space up to a choice of coordinates. The isoDim definition takes the least natural-number dimension admitting an isometric embedding, with equality of distances for every vertex pair. The graph metric comes from SimpleGraph.dist; connectedness is explicit where the paper assumes it. The cube is the graph on Fin m → Bool with Hamming-distance-one adjacency, and $C_{2m}$ is Mathlib's cycleGraph (2 * m). The goal assumes $m\geq1$; its $m=1$ case is direct, while the cycle milestones use $m\geq2$. A zero-dimensional cube consists of one vertex and is covered by the auxiliary upper-bound statement, though the goal follows the paper's positive-dimensional convention.

An implementing matrix has arbitrary finite column count. Instead of taking a maximum over an empty index set, the formal definition requires all column differences to be bounded by the graph distance and a column to attain that distance for distinct rows. This agrees with the paper's maximum formula whenever columns are present and handles a one-vertex graph with zero columns. Matrix rank is taken over $\mathbb R$; the path-distance matrix has entries $|r-s|$ for indices $0,\ldots,m-1$. The infimum over achievable dimensions or ranks is a minimum, since these are nonempty subsets of $\mathbb N$ for finite connected graphs. No asymptotic $O(\cdot)$ or $\Omega(\cdot)$ bound occurs in these targets, so there is no hidden constant to instantiate.

The statements require genuine norm axioms and exact graph distances. Allowing a seminorm, assuming the desired dimension bound, or replacing the cube by a path would empty the main claim. Useful contributions include the cube-distance calculation, the path determinant, an exact even-cycle lower bound, and the general rank characterization. The paper makes no running-time claim for these particular results; no algorithmic complexity assertion is included.

Selected references

• N. Linial, E. London, Y. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica 15(2), 215–245, 1995. DOI: 10.1007/BF01200757.
• J. H. van Lint, R. M. Wilson, A Course in Combinatorics, Cambridge University Press, 1992, pp. 64–65, cited as [44] by Linial et al. for the path distance-matrix fact. Book record.

Motivation

In online prediction, a learner makes a forecast before seeing the next label. A collection of other forecasters may offer useful advice, but the learner need not know beforehand which forecaster will perform well. Littlestone and Warmuth's Weighted Majority Algorithm (WM) gives a deterministic way to combine such advice. Its guarantees hold for every finite sequence of instances and labels, including sequences chosen without any probability model. That worst-case setting is useful when the reliability of the forecasters can change or when no data-generating distribution has been justified. The paper develops WM and several variants; this mission isolates its basic mistake bound. Littlestone and Warmuth, 1994.

Setting

A finite pool has $n$ members, each of which predicts either $0$ or $1$ on every trial. The true label on trial $t$ is $\rho_t\in\{0,1\}$, and member $i$ predicts $x_{t,i}\in\{0,1\}$. The master prediction is $\lambda_t\in\{0,1\}$. Pool members may themselves be learning algorithms, so their predictions may reflect all earlier labels. The mission treats their prediction vectors and the labels as arbitrary finite sequences; no independence or stationarity is assumed.

Each member begins with a strictly positive real weight $w_{0,i}$. Before trial $t$, let $w_{t,i}$ be its current weight. For $b\in\{0,1\}$, let $q_{t,b}$ be the sum of weights of members predicting $b$. WM predicts the value with the larger backing total. When the two totals tie, either binary prediction is allowed. After the label is revealed, WM changes weights only if its own prediction was wrong. On such a trial, each member that predicted the wrong label has its weight multiplied by a fixed factor $\beta$ with $0\le\beta<1$; every other member retains its weight. If WM predicted correctly, every weight stays as it was. This is the version of the algorithm stated in §1 of the paper. A footnote there says the bounds also apply to the variant that updates on every trial. Littlestone and Warmuth, 1994, p. 215.

Write $W_t=\sum_i w_{t,i}$ for the total pool weight at a trial boundary. Thus $W_0=w_{\mathrm{init}}$ and $W_T=w_{\mathrm{fin}}$ after $T$ trials. Let $m$ count the trials with $\lambda_t\ne\rho_t$. The default initial weights in the paper are all one, but its Theorem 2.1 permits arbitrary positive initial weights. Littlestone and Warmuth, 1994, pp. 220–221.

Formalization targets

The two milestones state the weight facts used immediately before and within Theorem 2.1. First, on each trial where WM errs,

$$W_{t+1}\le \frac{1+\beta}{2}W_t.$$

Across the whole sequence, with $m$ master mistakes, the corresponding estimate is

$$W_T\le W_0\left(\frac{1+\beta}{2}\right)^m.$$

The goal is the paper's Theorem 2.1, retaining its explicit constant:

$$m\le \frac{\log(W_0/W_T)} {\log\!\left(2/(1+\beta)\right)} \qquad\text{when }W_T>0.$$

The logarithm base is immaterial because the same base occurs above and below the fraction. The paper explicitly uses this convention for ratios of logarithms. The positive-final-weight condition represents the paper's statement that the displayed logarithmic bound is vacuous when all weight has vanished, which can happen for $\beta=0$. The whole-sequence weight estimate remains meaningful in that case. Littlestone and Warmuth, 1994, pp. 220–221.

Significance

The result limits the mistakes of a master predictor without assigning probabilities to the predictions or labels. It relates a visible property of the run, the reduction of total weight, to the number of master errors. Later bounds in the paper use this starting point to compare WM with an individual pool member and to analyze related algorithms; this mission fixes the initial, exact-constant result on which those comparisons rest. The $\beta=0$ case includes the paper's Halving Algorithm interpretation when initial weights are equal. Littlestone and Warmuth, 1994, pp. 215, 221–222.

The mathematical theorem is proved in the 1994 paper. The remaining task here is to represent its algorithm and finite-sequence bound in Lean and supply machine-checked proofs. A complete development would give later formalizations a reusable finite-pool voting and weight-update model, along with a checked potential estimate. The local draft statements compile; their proofs remain open. A separate, sorry-free local check constructs a run for every finite prediction and label sequence with a nonempty pool and valid weights and parameter, so the quantified run relation has witnesses.

Difficulty

The master can be wrong even when some pool members are right, and members may change their predictions over time. Counting one member's errors therefore does not directly control the master's error count. The exact contraction constant also depends on which side of a weighted vote the master chose, including the permitted tie case. When $\beta=0$, a single mistake can erase all weight backing the wrong label, so the logarithmic expression must be interpreted with care if no positive weight remains. These are features of the stated algorithm, rather than assumptions about how the sequence was generated.

Formalization scope

The formalization indexes pool members by Fin n and trials by Fin T. Booleans represent binary predictions and labels; weights and $\beta$ are real. A WM run is a relation on the full sequence of weights and master predictions, admitting every choice at a tied vote. Its update rule changes weights only after a master mistake, scales exactly the members that disagreed with the label, and leaves all other weights unchanged. Theorems require $0\le\beta<1$ and strictly positive initial member weights. The goal additionally requires $W_T>0$, while the two weight inequalities permit $W_T=0$. Natural logarithms instantiate the paper's common-base logarithm convention. Finite sums and a finite mistake count match the paper's finite-sequence convention.

The statement ranges over arbitrary pool predictions and labels, so it cannot be satisfied merely by selecting an easy input sequence. The run relation allows both legal outcomes of a tie; selecting one favorable tie rule would weaken the target. The sorry-free run-existence check also rules out a vacuous theorem caused by an inconsistent update relation. The paper's update-on-every-trial variant, its member-specific corollaries, and its later algorithms are outside this mission's goal.

A completed formalization needs finite sums of real weights, cardinalities of finite sets of mistake trials, a finite induction over trial boundaries, and real logarithm inequalities. The run definition and the first two bounds can be reused in the later parts of this paper's formalization. Contributions that prove the exact stated milestones or supply supporting facts about legal runs and nonnegative weights are within scope.

Selected references

• Nick Littlestone and Manfred K. Warmuth, The Weighted Majority Algorithm, Information and Computation 108(2), 212–261, 1994. DOI: 10.1006/inco.1994.1009.

Motivation

Semiconductor burn-in tests hold several jobs in an oven at once. A production planner must decide which jobs share each oven run and in what order those runs take place. A job may become available only after earlier manufacturing steps, and a due date marks when its test should finish. The planning objective here is to minimize how many jobs finish after their due dates. Lee, Uzsoy, and Martin-Vega studied this batch scheduling problem and gave a dynamic program for the case of equal processing times and compatible release and due-date orders (Lee, Uzsoy, and Martin-Vega 1992, §4, pp. 770–771).

Setting

There are $n$ jobs and one batch processing machine with capacity $B\ge1$. Job $j$ has release time $r_j$, due date $d_j$, and processing time $p_j$. In the main problem every processing time equals a common value $p$. A batch is a nonempty set of at most $B$ jobs. Its processing time is the longest processing time among its members; it begins only after all its jobs have been released and the previous batch has finished. Processing is uninterrupted. A schedule is an ordered list of disjoint batches that covers every job. Each batch starts at the earliest time allowed by these conditions.

The completion time $C_j(S)$ of job $j$ in schedule $S$ is the completion time of its batch. A job is on time when $C_j(S)\le d_j$ and tardy when $d_j<C_j(S)$. Write $U(S)=\#\{j:d_j<C_j(S)\}$ and let $U^*$ be the minimum of $U(S)$ over all valid complete batch schedules. Tardy jobs still belong to a schedule and consume machine time. An on-time batch is one whose every member is on time.

For the structural lemmas, agreeable release times and due dates mean that $r_i<r_j$ implies $d_i\le d_j$. For the dynamic program, jobs are indexed so that both $r_j$ and $d_j$ are nondecreasing. A batch is in batch-EDD order relative to later batches when no job in it has a later due date than a job in a later batch. A batch of consecutive jobs contains exactly an index interval. These are the paper's Lemmas 4 and 5 and Definition 1 (pp. 767, 770).

Formalization targets

Structural optimal schedules

Lemma 4 asserts that some optimum has an initial list of wholly on-time batches in batch-EDD order, followed by batches containing only tardy jobs. Lemma 5 asserts that some optimum has every wholly on-time batch made of consecutive indexed jobs. These are existence statements about schedules of all jobs; neither restricts the feasible schedules over which $U^*$ is defined.

Correctness of Algorithm DP3

Let $f(i,j)$ be the table defined by Algorithm DP3 for the first $j$ jobs and a selected count $i$ of on-time jobs. Its boundary values are $f(0,j)=0$ and $f(i,j)=+\infty$ for $i>j$. For $1\le i\le j$, it takes the minimum of $f(i,j-1)$ and the eligible transitions that append a batch of $k$ jobs, $1\le k\le\min(B,i)$. A transition uses $\max\{f(i-k,j-k),r_j\}+p$ and is eligible when that completion time does not exceed $d_{j-k+1}$. The main target is

$$U^*=n-\max\{i\in\{0,\ldots,n\}:f(i,n)<+\infty\}.$$

The maximum includes zero, which is always feasible in the table. The printed range begins at one and has no value when every job is tardy. This is the corrected boundary reading of the displayed answer on p. 771 (source).

Unequal processing times

The paper also gives a variant for jobs available at time zero, with nondecreasing processing times and due dates. Its transition replaces the release-time maximum and common $p$ by $f(i-k,j-k)+p_j$. The corresponding correctness statement is a further milestone (p. 771).

Significance

The structural results connect the optimization over arbitrary complete batch schedules to the restricted arrangements represented by the table. DP3 correctness then identifies the number of tardy jobs from finite table entries, including instances with no on-time job. The variable-time extension covers the related case where each job has its own duration but all jobs are available together.

The paper proves these results informally; this mission leaves their Lean proofs open. A complete formalization would supply reusable definitions of batch schedules, release-limited completion times, tardy-job counts, and a finite dynamic program with an explicit infinite value. The machine-checked statements and the local instance check establish the interface for that work, while the structural and correctness theorems remain solver targets.

Difficulty

The objective ranges over every valid batching and every processing order. The table examines an indexed prefix and places the last on-time batch among consecutive jobs. Establishing that the table's choices preserve the full optimum requires the existence statements in Lemmas 4 and 5. Reordering jobs is delicate because delaying a batch can change release feasibility and can make an earlier on-time job late. Equal due dates also require care: a due-date order alone need not put the latest release of a proposed batch at its last index.

Formalization scope

Jobs use Fin n, with index zero representing the paper's job 1; the table's $j$ is a prefix length. Data and completion times are natural numbers, matching the paper's integer-data setting; $+\infty$ in the table is WithTop ℕ. The schedule model uses nonempty batches of cardinality at most $B$, pairwise disjointness, and complete coverage. A batch starts at the maximum of its latest release and the preceding completion time. This earliest-start convention is sufficient for minimizing the regular tardy-job objective. The empty job set is included: its empty schedule has zero tardy jobs.

The strict implication $r_i<r_j\Rightarrow d_i\le d_j$ makes the paper's loose “agreeable” condition precise without forcing equal due dates for tied release times. For the recurrence, both release times and due dates are nondecreasing in job index, including their ties. This ensures that $r_j$ is the last batch's latest release and $d_{j-k+1}$ its earliest due date. The variable-time version similarly indexes by nondecreasing processing times and due dates, so the last job gives the batch duration. The table uses a minimum over exactly the paper's range $1\le k\le\min(B,i)$, with an empty range giving $+\infty$. Zero is included in the final maximum. Tardy jobs are scheduled in the underlying optimum; defining the optimum as an on-time subset or defining the table as that optimum would erase the two structural claims.

This mission covers correctness only. The paper's $O(n^2B)$ running-time statement and the bisection procedure are outside the formalization because they would need a specified computational cost model. The paper's FBEDD remark for this objective is also excluded: a three-job instance contradicts it. Contributions to the open theorem proofs, schedule-existence facts, and reusable batch scheduling lemmas are welcome.

Selected references

• C.-Y. Lee, R. Uzsoy, and L. A. Martin-Vega, Efficient Algorithms for Scheduling Semiconductor Burn-In Operations, Operations Research 40(4), 1992, pp. 764–775. DOI: 10.1287/opre.40.4.764.

Motivation

In a two-machine flow shop, each of $n$ jobs is processed first on machine $A$ and then on machine $B$, and the order of the jobs is to be chosen. For the makespan (the finishing time of the last job), Johnson (1954) gave an exact sorting rule. For the sum (equivalently, the mean) of the completion times, no such rule is known: the problem is NP-hard in the strong sense (Garey, Johnson and Sethi, 1976), and exact methods search the $n!$ sequences implicitly.

Ignall and Schrage (1965) were among the first to apply branch and bound to sequencing. They view the $n!$ sequences as the leaves of a tree of partial sequences, keep a list of partial sequences ranked by a lower bound, and always extend the most promising one. For the two-machine mean-completion-time problem they introduced a lower bound, built from two relaxations (one where machine $A$ is the bottleneck, one where machine $B$ is), that became the template for many later flow-shop bounds.

Setting

There are $n\ge1$ jobs; job $i$ has processing time $a_i$ on machine $A$ and $b_i$ on machine $B$. A sequence is a permutation $\sigma$ of the jobs, processed in that order on both machines with every operation started as early as possible. The completion time $d_i(\sigma)$ of job $i$ is the time machine $B$ finishes it, and the objective is $\sum_{i=1}^n d_i(\sigma)$.

A node $J_r$ is a partial sequence of $r$ jobs; $\bar J_r$ is the set of the $n-r$ jobs not in it; $k$ is the last job of $J_r$ and $d_k$ its completion time; $d_i$ ($i\in J_r$) are the completion times of the jobs of $J_r$. For an ordering $(i_1,\dots,i_{n-r})$ of $\bar J_r$,

$$T_r=\sum_{p=1}^{n-r}\Big[\sum_{j\in J_r}a_j+(n-r-p+1)a_{i_p}+b_{i_p}\Big],$$

and for an ordering $(j_1,\dots,j_{n-r})$ of $\bar J_r$,

$$S_r=\sum_{p=1}^{n-r}\Big[\max\Big(d_k,\sum_{j\in J_r}a_j+\min_{i\in\bar J_r}a_i\Big)+(n-r-p+1)b_{j_p}\Big].$$

$\hat T_r$ and $\hat S_r$ are their minima over all orderings of $\bar J_r$, and the lower bound of the node is

$$LB(J_r)=\sum_{i\in J_r}d_i+\max(\hat T_r,\hat S_r).$$

The procedure starts with a list holding only the empty node. A step removes the first node, creates one child for every unscheduled job by appending it, and inserts the children into the list ranked by $LB$ (a new node goes before old nodes with equal bound). It stops the first time the first node of the list is terminal, i.e. has scheduled $n-1$ jobs, so that its last job is forced.

Formalization targets

Goal: the procedure finds a sequence of least mean completion time

For all real data, (i) the procedure reaches a list whose first node $P$ is terminal, and (ii) whenever that happens, the sequence $\sigma^\ast$ formed by $P$ and its one unscheduled job satisfies

$$\sum_{i=1}^n d_i(\sigma^\ast)\le\sum_{i=1}^n d_i(\sigma)\qquad\text{for every sequence }\sigma .$$

Milestones

1. For $1\le r\le n-1$ and every sequence $\sigma$ beginning with $J_r$: $T_r$ of the order in which $\sigma$ processes $\bar J_r$ is at most $\sum_{i\in\bar J_r}d_i(\sigma)$, hence so is $\hat T_r$ (pp. 405–406).
2. An ordering of $\bar J_r$ by increasing $a_i$ attains $\hat T_r$ (p. 406).
3. An ordering of $\bar J_r$ by increasing $b_j$ attains $\hat S_r$ (p. 406).
4. The analogue of 1 for $S_r$ and $\hat S_r$ (p. 406).
5. $LB(J_r)\le\sum_i d_i(\sigma)$ for every $\sigma$ beginning with $J_r$ (p. 406).
6. At depth $n-1$, $LB$ equals the value of the node's unique completion (labelled: what the stopping rule of p. 402 needs).
7. Without delays, job $i_p$ completes at $\sum_{J_r}a_j+a_{i_1}+\dots+a_{i_p}+b_{i_p}$ and $\sum_{\bar J_r}d_i=T_r$ (pp. 405–406).
8. The three-job example of p. 408: 1–2 is optimal for jobs 1, 2, while 3–2–1 is optimal for all three.

Significance

The goal is the correctness of the paper's algorithm for the two-machine problem: the sequence it returns is optimal, not merely good, and it returns one for every input. The lower-bound milestones are the paper's own justification of its bound, and the sorting milestones show that the bound is computable in $O(n\log n)$ per node rather than by a minimization over $(n-r)!$ orderings.

On the formal side, no item on the platform treats flow-shop lower bounds or branch and bound over sequences; the nearest is the branch-and-bound mission for jointly constrained biconvex programs (BiconvexProg.BranchBound, Al-Khayyal and Falk 1983), an unrelated algorithm over boxes. The paper's arguments are short and informal ("it should be evident"); the formalization makes explicit that the $S_r$ bound holds for every order and every input, which the paper derives only by analogy with $T_r$. The published definitions of Johnson's as-soon-as-possible schedule (from the Johnson 1954 missions) are reused for the completion times.

Difficulty

The two halves of the bound are relaxations of different kinds. $T_r$ ignores waiting on machine $B$; $S_r$ ignores idle time on machine $B$ after its first job of $\bar J_r$ and replaces that job's machine-$A$ time by the smallest one. The paper's description of $S_r$ as "the sum of the completion times" when $\min b\ge\max a$ is not an identity, since $\min a$ replaces $a_{j_1}$; only the inequality is true, and it has to be proved for the given order directly. The sorting claims are rearrangement inequalities, with the coefficient $n-r-p+1$ decreasing in the position.

The goal is a statement about all $n!$ sequences, while the procedure only ever looks at the nodes on its list, whose length changes at every step. The tempting one-line justification, that the first terminal node has the smallest bound, says nothing by itself about sequences that are not descendants of nodes still on the list, nor about whether the bound of a terminal node is the value of its sequence; and termination of the search has to be shown, not assumed.

Formalization scope

• Jobs are Fin n (the paper's $1,\dots,n$ shifted to $0,\dots,n-1$); processing times are arbitrary reals, with no sign condition; all statements are true without one.
• Completion times of a full sequence come from Johnson's asapC2 (referenced definition JohnsonFlowShop.TwoStage.asapStart2). The objective is the sum of the completion times; the paper's mean differs by the fixed factor $1/n$.
• A node is a list of jobs; "a sequence begins with $J_r$" means $J_r$ is a prefix of its list of jobs.
• $\hat T_r$ and $\hat S_r$ are defined as minima over all orderings of $\bar J_r$, not by a sorted order; that sorting attains them is milestones 2 and 3. Defining them by sorting would make those milestones true by definition.
• At the root ($r=0$) $d_k$ is read as $0$; the root is never ranked, and the lower-bound milestones are stated for $1\le r\le n-1$.
• Terminal nodes are at depth $n-1$. The paper says "a node that has scheduled all $n$ jobs"; its own example stops at a node with three of four jobs, and its node counts end at level $n-1$.
• Explicit readings: "is a lower bound" means $\le$ the objective of every sequence beginning with the node; "will exceed" means $\ge$; "the problem is solved: that node's sequence is an optimal one" means termination plus optimality over all $n!$ sequences.
• A trivializing formalization is ruled out: the bound is not taken over an unrestricted or empty set of orderings (the set of orderings of $\bar J_r$ is nonempty), optimality is over all permutations rather than over the nodes the run visits, and termination is part of the goal.
• Not formalized: the reduction to permutation schedules (the paper's footnote on p. 401 asserts it for mean completion time without proof, and no platform item proves it), dominance discarding (pp. 403–405), the jobset generator, Tables I–III and the 9-job examples.

Proofs of any milestone, and reusable lemmas on as-soon-as-possible two-machine schedules (completion times of a prefix, monotonicity in the start time), are welcome.

Selected references

• E. Ignall and L. Schrage, Application of the branch and bound technique to some flow-shop scheduling problems, Operations Research 13(3), 400–412, 1965. https://doi.org/10.1287/opre.13.3.400
• S. M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1(1), 61–68, 1954. https://doi.org/10.1002/nav.3800010110
• M. R. Garey, D. S. Johnson and R. Sethi, The complexity of flowshop and jobshop scheduling, Mathematics of Operations Research 1(2), 117–129, 1976. https://doi.org/10.1287/moor.1.2.117
• A. H. Land and A. G. Doig, An automatic method of solving discrete programming problems, Econometrica 28(3), 497–520, 1960. https://doi.org/10.2307/1910129

Motivation

Kelso and Crawford's 1982 Econometrica paper studies a labor market in which firms hire sets of heterogeneous workers at individually negotiated salaries. Their existence results for the core and for competitive equilibrium, and the convergence of their salary-adjustment process, all rest on one hypothesis about each firm's technology, the gross-substitutes condition (GS): raising some workers' salaries never makes a firm drop a worker whose salary did not change. The condition has since become central to matching with contracts, ascending auctions and the theory of discrete convexity (Hatfield and Milgrom 2005; Fujishige and Yang 2003). It is defined through the firm's demand correspondence rather than through the production function, so its economic content is not obvious.

Section 6 of the paper explains that content. Its first result, Theorem 6, says that when workers are alike in production, (GS) is exactly the familiar requirement of nonincreasing returns to workers. This mission formalizes Theorem 6, the two halves of its proof, and the companion claim that with two heterogeneous workers (GS) is equivalent to subadditivity.

Setting

Fix a finite set $W$ of $m$ workers and a single firm. Its production technology is a function $y : 2^W \to \mathbb{R}$; $y(C)$ is the gross product when the firm hires the set $C$. A salary vector $s \in \mathbb{R}^W$ assigns to each worker $i$ the salary $s_i$ the firm must pay to hire him or her. The firm's net profit is

$$\pi(C; s) = y(C) - \sum_{i \in C} s_i ,$$

and $C$ is demanded at $s$, written $C \in M(s)$, if it maximizes $\pi(\,\cdot\,; s)$ over all subsets of $W$ (problem (A) of the paper). The technology satisfies (GS) if for all salary vectors $s \le \tilde s$ and every $C \in M(s)$ there is $\tilde C \in M(\tilde s)$ with

$$T(C) = \{\, i \in C : \tilde s_i = s_i \,\} \subseteq \tilde C .$$

Workers are alike in production when the product depends only on how many are hired: $y(C) = \bar y(|C|)$ for some $\bar y : \mathbb{N} \to \mathbb{R}$. The workers remain distinct individuals, since their salaries can differ. The function $\bar y$ has nonincreasing returns to workers (DR) if

$$\bar y(w + 1) - \bar y(w) \le \bar y(w) - \bar y(w - 1) \qquad \text{for every integer } w,\ 1 \le w \le m - 1 .$$

A technology $y$ is subadditive if $y(C \cup D) \le y(C) + y(D)$ for disjoint $C, D \subseteq W$.

In the Lean development these are profit, IsDemanded, GrossSubstitutesOn y Set.univ, DR (Fintype.card W) ybar and Subadditive y, in the namespace KelsoCrawford.Returns.

Formalization targets

Goal: Theorem 6 (p. 1499)

For every $\bar y : \mathbb{N} \to \mathbb{R}$,

$$\text{(DR) for } \bar y \text{ on } \{0, \dots, m\} \iff C \mapsto \bar y(|C|) \text{ satisfies (GS) on } \mathbb{R}^W .$$

Milestones

1. (DR) implies (GS) (proof of Theorem 6, p. 1499).
2. If (DR) fails, (GS) fails (proof of Theorem 6, pp. 1499–1500): if for some $w$ with $1 \le w \le m - 1$

$$\bar y(w + 1) - \bar y(w) > \bar y(w) - \bar y(w - 1), \tag{19}$$

then $C \mapsto \bar y(|C|)$ violates (GS). 3. Two workers (p. 1500), off the goal's path: if $|W| = 2$ and $y(\emptyset) = 0$, then $y$ satisfies (GS) if and only if $y$ is subadditive, that is $v_1 + v_2 \ge v_{12}$.

Significance

The result itself. Theorem 6 gives a production-side reading of (GS): restricted to identical workers it is nonincreasing returns, so (GS) can be viewed as the generalization of that convexity condition to heterogeneous workers. The paper uses this reading to explain why something like (GS) is needed for existence: without it the core and the competitive equilibrium may fail to exist, as the example of Section 6 shows (mission 7 of this series). The two-worker claim locates the boundary further: with two workers (GS) is subadditivity, while with three or more subadditivity is no longer enough.

Formalizing it. Nothing of this paper was on Prove2Me before this series. Theorem 6 is a proved result in the paper. This draft provides compiling Lean statements of both directions, with (GS) in the paper's own form (real salary vectors and the set $T(C)$), and of the two-worker characterization; their proofs remain open. A completed mission would provide machine-checked proofs of those statements. The statements fix the boundary conventions exactly (which $w$ are constrained, what happens with zero or one worker), which the informal argument leaves implicit. The definitions of profit, demand and (GS) are the same as in the other missions of the series (1–5 and 7), so proofs here are reusable there.

Difficulty

For (DR) $\Rightarrow$ (GS), the natural argument sorts workers by salary and observes that a profit-maximizing firm hires the $w^*$ cheapest workers. With ties among salaries this description is not literally true (any $w^*$ cheapest workers will do), and after a salary increase the new optimal size and the new ranking change at once; showing that some new maximizer keeps every worker whose salary stayed fixed requires a careful exchange argument rather than a monotone comparison of indices. For the converse, a single failure of (DR) must be turned into an explicit pair of salary vectors; the construction must make one worker strictly demanded before the change and strictly undemanded after it, which requires controlling every competing set, not only the sets of the critical sizes $w$ and $w + 1$. The two-worker characterization requires a case analysis over the four candidate demands at every salary pair, including ties.

Formalization scope

Workers form an arbitrary finite type W with m = Fintype.card W; a technology is a function Finset W → ℝ, and "alike in production" is the technology fun C => ybar C.card with ybar : ℕ → ℝ. Salaries are arbitrary real vectors W → ℝ, and (GS) is required on all of $\mathbb{R}^W$ (Set.univ), the continuous version that Theorem 6 is about. A discrete market can satisfy (GS) on its salary grid while its continuous version does not, so the discrete version is a different statement and is not targeted here. (DR) is written for natural numbers with 1 ≤ w and w + 1 ≤ m, so that w - 1 never truncates. For $m \le 1$ it is vacuous, and no lower bound on $m$ is imposed. Neither (MP) nor (NFL), $\bar y(0) = 0$, is assumed in Theorem 6: the paper uses neither, and adding them would weaken the theorem. The two-worker claim keeps the paper's normalization $y(\emptyset) = 0$ and uses its general definition of subadditivity over disjoint pairs.

A trivializing formalization would restrict (GS) to a single salary vector, quantify demand over a subfamily of sets, or replace "some demanded set contains $T(C)$" by "the given set does", and is ruled out by the definitions above, which follow the paper's (A) and (GS) word for word. The read-out of the goal as two milestones is the paper's own split of its proof.

Infrastructure needed: finite sums over Finset, sorting of a finite salary vector, and elementary facts on concave sequences. Contributions that would be reusable beyond this mission include a general lemma that concave functions of cardinality yield gross-substitutes demand, and the link between (GS) and M$^\natural$-concavity of set functions (Murota's gross-substitutes axioms are on Prove2Me as Shuze Chen's DiscreteConvex_MConvexFunctionsC_MNatGS, a related but different object: one price per good and integer bundles). Proofs of either direction, of the two-worker claim, or of intermediate lemmas are welcome.

Selected references

• A. S. Kelso, Jr. and V. P. Crawford, Job matching, coalition formation, and gross substitutes, Econometrica 50(6) (1982), 1483–1504. https://doi.org/10.2307/1913392
• V. P. Crawford and E. M. Knoer, Job matching with heterogeneous firms and workers, Econometrica 49(2) (1981), 437–450. https://doi.org/10.2307/1913320
• S. Fujishige and Z. Yang, A note on Kelso and Crawford's gross substitutes condition, Mathematics of Operations Research 28(3) (2003), 463–469. https://doi.org/10.1287/moor.28.3.463.16393
• J. W. Hatfield and P. R. Milgrom, Matching with contracts, American Economic Review 95(4) (2005), 913–935. https://doi.org/10.1257/0002828054825466
• K. Murota, Discrete Convex Analysis, SIAM, 2003. https://doi.org/10.1137/1.9780898718508

Why monotone comparative statics matters

An optimization problem often changes when a parameter changes: a price rises, a constraint expands, or a strategic environment shifts. Comparative statics asks whether the optimal choice moves in a predictable direction. The usual numerical tools, such as derivatives, can be unavailable when choices form a discrete set or the objective is neither smooth nor concave. Milgrom and Shannon's Monotonicity Theorem gives a condition expressed entirely through order and preference comparisons. It applies to individual optimization problems and supplies the order argument used later in their paper for games with strategic complementarities.

Their 1994 paper moves beyond cardinal conditions such as supermodularity and increasing differences. Those conditions imply useful comparative statics, but they can change under a strictly increasing transformation of the objective even though every argmax set stays the same. Quasisupermodularity and single crossing describe the comparisons that actually govern the argmax. The theorem characterizes these conditions through the behavior of optimizers over all constraint sets, rather than giving only a sufficient test. The historical relationship and the claims in this paragraph are described in Milgrom and Shannon, Sections 1–2.

Ordered choices, constraints, and preferences

Let $X$ be a lattice: a partially ordered choice set in which every two choices $x,y$ have a meet $x\wedge y$ and a join $x\vee y$. Let $T$ be a partially ordered parameter set and $f:X\times T\to\mathbb R$ an objective. For any constraint set $S\subseteq X$, define the possibly empty maximizer set

$$M(t,S)=\operatorname{argmax}_{x\in S}f(x,t)=\{x\in S: f(y,t)\le f(x,t)\text{ for every }y\in S\}.$$

The strong set order, written $A\le_s B$, compares subsets of the lattice by requiring $a\wedge b\in A$ and $a\vee b\in B$ for every $a\in A$ and $b\in B$. It can compare feasible sets as well as sets of optimizers. On singleton sets it agrees with the order on $X$. It also holds vacuously if either set is empty; it is reflexive at $S$ exactly when $S$ is a sublattice. These are the paper's conventions on page 159.

A function $g:X\to\mathbb R$ is quasisupermodular if, for every $x,y\in X$, both

$$g(x\wedge y)\le g(x)\Rightarrow g(y)\le g(x\vee y),\qquad g(x\wedge y)<g(x)\Rightarrow g(y)<g(x\vee y)$$

hold. The single crossing property of $f$ in $(x;t)$ requires, whenever $x''<x'$ and $t''<t'$, that a weak or strict preference for $x'$ over $x''$ at $t''$ remains respectively weak or strict at $t'$. The strict version sends even a weak preference at $t''$ to a strict one at $t'$. These definitions are given on pages 160 and 162.

Formalization targets

Theorem 4: the monotonicity equivalence

The main target is Theorem 4 on page 162:

$$\bigl[\forall t\le t',\ S\le_s S': M(t,S)\le_s M(t',S')\bigr] \quad\Longleftrightarrow\quad \bigl[\forall t,\ f(\cdot,t)\text{ is quasisupermodular on }X\bigr] \land\bigl[f\text{ has single crossing in }(x;t)\bigr].$$

The milestone list records the two necessity claims and the sufficiency claim separately, using the three corresponding passages of the paper's proof. The goal keeps both directions together. It imposes no restriction on which subsets may be used as constraints.

Consequences and the stronger selection statement

Corollary 1 characterizes quasisupermodularity alone through monotonicity as the constraint set changes, with no varying parameter. Corollary 2 says that the maximizers over a sublattice themselves form a sublattice. The reflexivity remark identifies when $S\le_s S$ holds. Theorem 4′ uses the strict single crossing property and a nondecreasing feasible-set correspondence $S:T\to 2^X$ to conclude that every selection of maximizers is nondecreasing. These nearby results share the definition layer with the main theorem and give distinct targets for the formal development.

What the result supplies

The equivalence turns an order property of an entire family of optimization problems into two properties of the objective. In particular, its converse shows that if every feasible-set comparison produces monotone maximizers, then quasisupermodularity and single crossing are forced. This matters for problems where an analyst can reason about choice behavior more directly than about algebraic properties of $f$. The corollaries also separate the effects of constraints and parameters and describe the structure of the optimal-choice set. The paper develops these consequences on pages 162–163.

The theorem is proved in the paper. The remaining work here is a machine-checked Lean proof of the ordinal characterization, its two directions, and the adjacent consequences. Published Prove2Me definitions already encode the strong set order, and its Topkis series covers related cardinal hypotheses such as supermodularity and increasing differences. This mission adds the paper's quasisupermodularity and single crossing predicates and seeks formal proofs of the distinct ordinal results. The separate characterization and linear-perturbation results of the same paper are targets of the other missions in this series.

Where the proof is difficult

The obstacle is the interaction of two orders. An increase in $t$ changes preferences, while an increase in $S$ changes which choices can be compared. A pointwise claim that an optimizer rises does not follow from either order condition alone, particularly when maximizers tie or are incomparable. The main theorem concerns sets of maximizers under the strong set order, so both the meet and join of optimizers at two parameter–constraint pairs must land in the correct maximizing sets. Conversely, observing monotonicity for one fixed feasible set cannot establish quasisupermodularity; the equivalence relies on monotonicity across every constraint set. The weak and strict preference clauses have different roles, so replacing either by the other changes the target. These are the distinctions visible in Theorem 4 and its proof.

Formalization scope

Lean represents $X$ with Lattice, $T$ with PartialOrder, and $f:X\to T\to\mathbb R$ in curried form. No finiteness, total order, topology, measurability, or maximizer-attainment hypothesis is imposed. The paper's product order for product lattices is Lean's usual componentwise order. The imported Supermodularity.Lattices.InducedSetOrder is exactly the paper's strong set order, including its behavior on empty sets. The definition argmaxOn returns the set of points in $S$ whose objective value bounds every value attained in $S$; it may be empty.

Quasisupermodularity is encoded with a reusable set argument but applied to Set.univ in every theorem here, so the property concerns the whole lattice. Single crossing compares strictly ordered choices and strictly ordered parameters and preserves both weak and strict preferences. ArgmaxMonotone compares weakly ordered parameters and all constraint sets under the strong set order. Theorem 4′ encodes a selection on an arbitrary domain $D\subseteq T$ where maximizers actually exist; it makes no global existence assertion. For Corollary 2, an arbitrary parameter is fixed and its objective is written $g:X\to\mathbb R$.

These choices rule out easy specializations that would change the theorem: taking $X$ to be a chain, restricting quasisupermodularity to a selected feasible set, demanding nonempty argmax sets, or dropping strict preference clauses. The reusable development consists of the maximizer-set definition, the two ordinal predicates, and their relation to the published strong set order. Contributions proving the goal, its three proof-direction milestones, the corollaries, and the selection theorem all fit this scope.

Selected references

• Paul Milgrom and Chris Shannon, Monotone Comparative Statics, Econometrica 62(1), 1994, 157–180. DOI: 10.2307/2951479.

Why this question matters

In a strategic game, each player evaluates a change in their own strategy using that player's own payoff. These incentives need not point in a common direction. A potential game is a case in which one real-valued function records every player's payoff change under a unilateral deviation. This common function lets questions about incentives be expressed as questions about one object on the space of strategy profiles. Monderer and Shapley's 1996 paper introduced several kinds of potential and gave a local characterization of the exact kind. The characterization is the subject of this mission.

The local test matters because the defining condition appears to require finding an unknown potential on the entire profile space. Theorem 2.8 says that a condition on four-step cycles already determines whether such a function exists, even when individual strategy sets are infinite. The paper compares this characterization with the familiar idea that a conservative field has zero integral around closed curves; here the “integral” is a finite sum of payoff changes along unilateral deviations (Monderer and Shapley, pp. 130–131).

Games, deviations, and path sums

Let $N$ be a finite set of players. For each player $i\in N$, let $Y^i$ be a strategy set, and let $Y=\prod_{i\in N}Y^i$ be the set of pure strategy profiles. The payoff of player $i$ is a function $u^i:Y\to\mathbb R$. If $y\in Y$, the notation $(y^{-i},x)$ means the profile obtained by replacing only player $i$'s strategy with $x\in Y^i$. The strategy sets themselves are not required to be finite in this section of the paper (p. 127).

An exact potential is a function $P:Y\to\mathbb R$ such that, for every $i$, every opponents' profile $y^{-i}$, and every $x,z\in Y^i$,

$$u^i(y^{-i},x)-u^i(y^{-i},z) =P(y^{-i},x)-P(y^{-i},z).$$

A game admitting such a function is an exact potential game. The paper uses the shorter term “potential game” for this class when the adjective is clear (pp. 127–128, equation (2.2)).

A path $\gamma=(y_0,\ldots,y_L)$ is a sequence in which each step changes exactly one player's strategy to a different value. Write $i_k$ for the unique player who moves from $y_{k-1}$ to $y_k$. The path sum of the payoff vector $u$ is

$$I(\gamma,u)=\sum_{k=1}^{L} \bigl(u^{i_k}(y_k)-u^{i_k}(y_{k-1})\bigr).$$

The path is closed when $y_0=y_L$. It is simple closed when, in addition, the vertices $y_0,\ldots,y_{L-1}$ are pairwise distinct. Its length is $L$, the number of steps and the number of vertices before the final return. These definitions follow pp. 128, 130–131.

Formalization targets

Theorem 2.8: four equivalent conditions

For a game with finitely many players, Theorem 2.8 asserts the equivalence of all four claims:

$$\begin{aligned} &\Gamma\text{ has an exact potential};\\ &I(\gamma,u)=0\quad\text{for every finite closed path }\gamma;\\ &I(\gamma,u)=0\quad\text{for every finite simple closed path }\gamma;\\ &I(\gamma,u)=0\quad\text{for every simple closed path }\gamma\text{ of length }4. \end{aligned}$$

The last condition is a local criterion, but the goal keeps the full four-way equivalence of the published theorem, p. 131. The milestone list follows five claims in its Appendix A proof: vanishing path sums from a potential, path independence, construction of a potential from vanishing closed-path sums, the local exchange of two different players' moves, and the reduction from all closed paths to length-four simple cycles (pp. 138–139).

Related results in the same development

Corollary 2.9 expresses the length-four test directly as a zero sum of payoff changes around four corners obtained by varying two players' strategies. Lemma 2.7 says that two exact potentials for the same game differ by one additive constant. Both are included as supporting statements from the same definition layer, although they are not milestones in the attack path for Theorem 2.8 (pp. 130–131).

What the result provides

Theorem 2.8 turns existence of a global function into a test on local cycles. Corollary 2.9 makes those cycles visible in payoff tables: fixing all but two players, the alternating sum around each two-player rectangle must vanish. For finite strategy sets this gives a direct finite collection of conditions; for infinite strategy sets the theorem remains a mathematical characterization without claiming a finite algorithm (Monderer and Shapley, p. 131).

The original paper proves these statements. The formalization work is to represent games, paths, path sums, and the four-way equivalence in Lean, then supply machine-checked proofs. The present mission contains compiled statements with open proofs. Its definition modules are also reusable for the paper's other results about potentials, improvement paths, and congestion games.

Where the proof is difficult

The challenging direction is that zero sums on simple length-four cycles force zero sums on every closed path. A closed path may repeat vertices and may involve more than two players. A direct appeal to the local condition does not cover such a path. The Appendix A argument uses changes to a path's sequence of deviators, and its informal treatment of adjacent moves by the same player leaves a boundary case: the two moves can cancel, so replacing them by one move would create a null step, which the definition of a path excludes. A formal proof must account for this case while preserving the paper's exact statement (pp. 138–139).

Formalization scope

Lean represents the finite player set by a finite type $\iota$ and a profile by a dependent function $y:\prod_{i:\iota}Y^i$. Strategy sets $Y^i$ remain arbitrary types. The operation $(y^{-i},x)$ is a one-coordinate update. A finite path stores $L+1$ vertices and its deviator at each of the $L$ steps; the step condition determines that deviator uniquely. Closed paths of length zero are allowed and have sum zero. The paper prints $n$, the number of players, as the upper limit of the path sum on p. 130, although its summands are indexed by path steps. The Lean definition sums over all $L$ steps, as the surrounding definition and later equations require.

The four-cycle hypothesis quantifies only over simple closed paths of exactly four genuine steps. It is not replaced by all four-step walks or by cycles with null or simultaneous deviations. The goal retains all four clauses rather than only its shortest equivalence. Corollary 2.9 explicitly requires the two varying players to be distinct; this is implicit in the paper's four-corner construction. No finite-strategy assumption is imposed on Theorem 2.8, Corollary 2.9, or Lemma 2.7.

The development needs ordinary finite sums, dependent functions, coordinate updates, and finite-indexed paths. Its path and potential definitions are intended as an interface for later work. Contributions proving any of the five source-backed milestones, the goal, or the two related statements are within scope.

Selected references

• Dov Monderer and Lloyd S. Shapley, Potential Games, Games and Economic Behavior 14 (1996), 124–143. DOI: 10.1006/game.1996.0044.

Motivation

How likely is a sum of independent random variables to exceed a large level $x$? If the summands have exponential moments, the classical answer is a Bernstein- or Hoeffding-type bound, exponentially small in $x$. Many quantities met in statistics, queueing, insurance mathematics and the analysis of algorithms have only finitely many moments, and then no exponential bound can hold: the tail of the sum is at least as heavy as the tail of the largest summand. The Fuk–Nagaev inequality is the standard answer for this situation. It bounds $P(S_n\ge x)$ by a polynomial term, which accounts for one summand being large, plus a Gaussian term, which accounts for the bulk of the sum.

The inequality was proved by D. Kh. Fuk and S. V. Nagaev in 1971 (Fuk–Nagaev 1971). S. V. Nagaev's survey of 1979 in the Annals of Probability states it as Theorem 1.3 and gives a complete proof, together with its corollaries (1.23) and (1.24). The form (1.24), $P(S_n\ge x)\le c_t^{(1)}A_t^+x^{-t}+\exp\{-c_t^{(2)}x^2/B_n^2\}$, is the version quoted in the later literature on heavy-tailed sums, empirical processes and high-dimensional statistics, where it is the usual replacement for Bernstein's inequality under polynomial moments.

Setting

Let $X_1,\dots,X_n$ be independent real random variables on a probability space, with distribution functions $F_i(u)=P(X_i<u)$, and let $S_n=X_1+\dots+X_n$. Fix a level $x>0$, truncation levels $Y=\{y_1,\dots,y_n\}$ (positive numbers), and a number $y\ge\max_iy_i$.

The truncated summands are $\tilde X_i=X_i$ if $X_i\le y_i$ and $\tilde X_i=0$ if $X_i>y_i$, with sum $\tilde S_n=\sum_i\tilde X_i$. The paper writes $\mu(\cdot,\cdot)$, $B^2(\cdot,\cdot)$ and $A(t;\cdot,\cdot)$ for sums of truncated means, second moments and absolute moments of order $t$, the arguments being the truncation levels. The three used here are

$$\mu(-\infty,Y)=\sum_{i=1}^n\int_{u\le y_i}u\,dF_i(u),\qquad B^2(-\infty,Y)=\sum_{i=1}^n\int_{u\le y_i}u^2\,dF_i(u),\qquad A(t;0,Y)=\sum_{i=1}^n\int_{0\le u\le y_i}|u|^t\,dF_i(u).$$

For $t\ge2$, $0<\alpha<1$ and $\beta=1-\alpha$, write $L=\log\big(\beta xy^{t-1}/A(t;0,Y)+1\big)$ and define

$$P_4=\exp\Big\{\beta\frac xy-\Big(\big(1-\tfrac\alpha2\big)\frac xy-\frac{\mu(-\infty,Y)}y\Big)L\Big\},\qquad P_5=\exp\Big\{\Big(\beta-\frac{t\alpha}2\Big)\frac xy-\Big(\beta\frac xy-\frac{\mu(-\infty,Y)}y\Big)L\Big\},$$ $$P_6=\exp\Big\{-\frac{\alpha x\,(\alpha x/2-\mu(-\infty,Y))}{e^tB^2(-\infty,Y)}\Big\}.$$

Finally $A_t^+=\sum_i\int_{u\ge0}u^t\,dF_i(u)$ and $B_n^2=\sum_i\operatorname{Var}X_i$.

In Lean these are the definitions S, Xt, St, muY, B2Y, AY, Atplus, Bn2, P4, P5, P6 of NagaevLD.FukNagaev.Setting.

Formalization targets

Goal: Theorem 1.3 (p. 749)

Suppose $t\ge2$, $0<\alpha<1$, $\beta=1-\alpha$ and $B^2(-\infty,Y)<\infty$. Write (1.4) for $\max[t,L]\ge\alpha xy/(e^tB^2(-\infty,Y))$ and (1.6) for $\max[t,L]<\alpha xy/(e^tB^2(-\infty,Y))$. Then

$$\text{(1.4)}\implies P(S_n\ge x)\le\sum_{i=1}^nP(X_i>y_i)+P_6,\qquad \text{(1.6)}\implies P(S_n\ge x)<\sum_{i=1}^nP(X_i>y_i)+P_4,$$

and if (1.6) holds together with $\beta\ge t\alpha/2$ or $\beta x\ge\mu(-\infty,Y)$, then $P(S_n\ge x)<\sum_iP(X_i>y_i)+P_5$. The page prints the last case as "if, instead of (1.6), …"; the proof on p. 752 proves it "if, in addition", and this is what is stated.

Milestones

The milestones follow the proof: the truncation inequality (1.8); the exponential Chebyshev bound with factorisation (1.9); Lemma 1.4, the cumulant bounds (1.10) and (1.11) for a variable bounded above, with the intermediate estimates (1.13) and (1.16); the bounds (1.17) and (1.18) for $P(\tilde S_n\ge x)$; the equivalence of (1.4) with $h_1\le\max[t/y,h_2]$; (1.19), $P(\tilde S_n\ge x)\le P_6$ under (1.4); $P(\tilde S_n\ge x)<P_4$ under (1.6); and (1.20), $P(\tilde S_n\ge x)<P_5$.

Corollaries

Corollary 1.7 (1.23): for $\mathbb EX_i=0$, $\beta=t/(t+2)$, $\alpha=1-\beta$,

$$P(S_n\ge x)\le\sum_{i=1}^nP(X_i>y_i)+\exp\Big\{-\frac{\alpha^2x^2}{2e^tB^2(-\infty,Y)}\Big\}+\Big(\frac{A(t;0,Y)}{\beta xy^{t-1}}\Big)^{\beta x/y}.$$

Corollary 1.8 (1.24): for $\mathbb EX_i=0$, $A_t^+<\infty$, $t\ge2$,

$$P(S_n\ge x)\le\Big(1+\frac2t\Big)^tA_t^+x^{-t}+\exp\Big\{-\frac{2e^{-t}x^2}{(t+2)^2B_n^2}\Big\}.$$

Significance

Theorem 1.3 makes no assumption on the summands beyond independence and finiteness of the truncated moments; no centring, no identical distribution, no bound on the summands. The free parameters $y_i$, $y$, $\alpha$ let a user trade the polynomial term against the Gaussian term. Corollary 1.8 is the form used for moment bounds of sums ($t$-th moment inequalities of Rosenthal type follow by integrating it in $x$), for maximal inequalities, and for concentration of empirical processes indexed by heavy-tailed classes.

The result has been proved since 1971 and is not open. As far as a search of the Prove2Me catalog and of Mathlib shows, it has not been formalized: Mathlib has the exponential Chebyshev bound and the moment generating function of independent sums, but no tail inequality for sums of heavy-tailed summands. This mission produces a checked proof of the theorem in the paper's exact form, of the cumulant bound of Lemma 1.4, and of both corollaries with their explicit constants $(1+2/t)^t$ and $2(t+2)^{-2}e^{-t}$.

Difficulty

The obvious argument, Chernoff's bound applied to $S_n$, fails at once: without exponential moments $\mathbb Ee^{hS_n}$ is infinite for every $h>0$. Truncating the summands repairs this, but the bound then depends on the choice of the exponent $h$, and no single choice works for all parameters. The proof splits into cases according to the relative position of three numbers, $t/y$ and the minimisers $h_1$, $h_2$ of two convex functions, and every case needs its own estimate of the cumulant of a variable bounded above. The bookkeeping of strict and non-strict inequalities across these cases is exactly what (1.7) and (1.7a) assert, and the printed text has a misprint at that point.

The corollaries need a separate step: Corollary 1.7 requires $\mu(-\infty,Y)\le0$, which follows from centring only because truncation removes positive mass, and Corollary 1.8 requires combining the Chebyshev bound for $P(X_i>\beta x)$ with the truncated moment $A(t;0,Y)$ so that the two polynomial terms add to exactly $A_t^+/(\beta x)^t$.

Formalization scope

• The summands are X : Fin n → Ω → ℝ on a probability space, measurable and mutually independent (iIndepFun); index $i$ stands for the paper's $i+1$. $x>0$, $y_i>0$, $y\ge y_i$ and $y>0$ are hypotheses ($y>0$ follows from the others when $n\ge1$).
• Every integral $\int_E\varphi(u)\,dF_i(u)$ is the expectation of $\varphi(X_i)$ over the event $\{X_i\in E\}$, with the endpoints of $E$ copied from the page. Powers with exponent $t$ are real powers; $A(t;0,Y)$ uses $|u|^t$.
• Added hypotheses. Finiteness of $B^2(-\infty,Y)$ is assumed as integrability of $X_i^2$ on $\{X_i\le y_i\}$ for each $i$; Lemma 1.4 assumes $X\in L^2$ (its $\beta=\mathbb EX^2$ is a number); Corollary 1.8 assumes each $X_i\in L^2$, since Mathlib's variance is $0$ outside $L^2$. On the page an infinite second moment makes each bound trivial; in Lean it would be replaced by $0$ and the statements would become false.
• Degenerate values. On the page $A(t;0,Y)=0$ makes $L=+\infty$, so (1.4) holds. Lean's division by $0$ would make $L=0$; condition (1.4) is therefore the definition cond_1_4, which includes the case $A(t;0,Y)=0$, and (1.6) is cond_1_6, which requires $A(t;0,Y)>0$. For $A\ge0$ the two are exact complements. If $B^2(-\infty,Y)=0$, $P_6$ and the exponential term of (1.23) take the page's limiting value $0$, and so does the exponential term of (1.24) when $B_n^2=0$; Lean's $x/0=0$ would otherwise make them $1$.
• Ruled out. Stating the goal for the truncated sum $\tilde S_n$ instead of $S_n$, or only the moment-generating-function bound, would replace the theorem by a step of its proof; the goal is about $P(S_n\ge x)$, with the strict inequalities of (1.7) and (1.7a) kept strict.
• Lemma 1.4 uses $\beta$ for $\mathbb EX^2$; it is unrelated to $\beta=1-\alpha$ of Theorem 1.3.
• Reusable beyond this mission: Lemma 1.4 (a cumulant bound for variables bounded above) and the truncation inequality (1.8). Contributions welcome on any milestone, and on the corollaries independently of the goal.

Selected references

• S. V. Nagaev, Large deviations of sums of independent random variables, Ann. Probab. 7(5):745–789, 1979. https://doi.org/10.1214/aop/1176994938
• D. Kh. Fuk and S. V. Nagaev, Probability inequalities for sums of independent random variables, Theory Probab. Appl. 16(4):643–660, 1971. https://doi.org/10.1137/1116071

Motivation

Semiconductor wafer fabrication lines are reentrant: a wafer returns to the same photolithography or etching station many times along its route, so the parts competing for a machine are at different stages of completion. In such a line, a local dispatching rule decides at every machine which waiting part goes next, and the question is whether a given rule keeps the line stable whenever there is enough capacity. Lu and Kumar (IEEE TAC 36(12), 1991) showed that the answer depends on the rule. Some natural buffer priority rules make the line unstable even when every machine has spare capacity (their Example 1; see also Kumar and Seidman 1990). Two rules are proved stable for every route: first buffer first serve (FBFS) and last buffer first serve (LBFS).

LBFS serves at each machine the waiting part that is closest to completion. It is the "pull" rule of the two, and the one closer to practice: it minimizes work in progress in many settings and coincides with earliest due date when parts arrive in due-date order. This mission formalizes the paper's LBFS results, §V. The sibling mission (FBFS, §IV) treats the other policy on the same model.

Timeline:

• 1990: Kumar and Seidman exhibit instability of clearing policies on a reentrant line with spare capacity.
• 1991: Lu and Kumar prove stability of FBFS (Theorem 1) and of LBFS (Theorems 2–3) under deterministic bursty arrivals. They also prove it for least slack and earliest due date (Theorem 4, Corollary 1), and show that a buffer priority policy can be unstable (Example 1).
• 1996: Dai and Weiss prove stability of the fluid models of FBFS and LBFS on reentrant lines (Math. Oper. Res. 21(1)), which by Dai's fluid limit theorem gives positive Harris recurrence for the stochastic versions.

Setting

A nonacyclic flow line has $S$ service centers; center $\sigma$ has $m_\sigma \ge 1$ identical machines, each processing one part at a time. Every part follows the same route through buffers $b_1, \dots, b_l$: in buffer $b_i$ it waits at center $\sigma_i$, then needs $\tau_i > 0$ units of uninterrupted processing on one machine of that center. A center may serve several buffers.

Parts are released into $b_1$; part $\pi$ is released at time $\alpha(\pi)$ and exits at time $e(\pi)$, when its service at $b_l$ ends. Finitely many parts may be present at time $0$, in any buffer, some already in service. With $u(t)$ the number of releases in $[0,t]$, the arrivals are bursty with rate $\lambda$ and burst $\gamma$ if

$$u(t)-u(s)\le \lambda(t-s)+\gamma\qquad(0\le s\le t).\tag{1}$$

The work per machine that one part brings to center $\sigma$ is $w_\sigma=\sum_{i:\sigma_i=\sigma}\tau_i/m_\sigma$, and the load is $\rho=\lambda\overline w$ with $\overline w=\max_\sigma w_\sigma$. The capacity condition is $\rho<1$ (3). Also $\overline\tau=\max_j\tau_j$, and $w^{(k)}$ is the maximum per-machine work brought to a center by a part in $b_k$, counting only buffers $b_k,\dots,b_l$ (6).

Scheduling is nonidling (a machine idles only if every buffer of its center is empty) and nonpreemptive, and a machine takes the part at the head of a buffer. Under LBFS, a machine takes a part from $b_i$ only if every buffer $b_j$ of its center with $j>i$ is empty. The number of parts in the system at time $t$ is $x(t)$.

Formalization targets

Goal: Theorem 3, Stability of LBFS

Under (1) and (3), for every $\varepsilon>0$ with $1-\rho-\lambda\varepsilon>0$,

$$x(t)\le\max\Big\{(1+\rho+\lambda\varepsilon)x(0)+\lambda c(\varepsilon)+\gamma,\ \frac{2(\lambda c(\varepsilon)+\gamma)}{1-\rho-\lambda\varepsilon}\Big\}\quad(t\ge0),$$ $$\limsup_{t\to\infty}x(t)\le\frac{\lambda c(\varepsilon)+\gamma}{1-\rho-\lambda\varepsilon}.$$

Here $c(\varepsilon)$ is the explicit constant of the delay estimate. The paper prints the second bound as $\lambda c(\varepsilon)+\gamma/(1-\rho-\lambda\varepsilon)$; its proof establishes the form above, which is the one posed.

Milestones

The delay estimate behind the goal, in the order of its proof:

• the base case (8) for the last buffer;
• the one-step comparison (11) with the part just ahead;
• the induction claim (10) for every truncated line $B^{(k)}=\{b_k,\dots,b_l\}$: a part in $B^{(k)}$ with $x$ parts ahead exits within $c^{(k)}(\varepsilon)+(w^{(k)}+\varepsilon)x$;
• Theorem 2, the contractive estimate

$$e(\pi)-\alpha(\pi)\le c(\varepsilon)+(\overline w+\varepsilon)x\qquad(\varepsilon>0),$$

for a part that finds $x$ parts in the system on release.

Then the Pipeline Property $e(\pi)-\alpha(\pi)\le\overline wx+o(x)$, order preservation (parts exit in the order they enter), and the recursion (14) for the number in system along successive exit times. A further item states that LBFS is stable in the sense of §II: every delay $e(\pi)-\alpha(\pi)$ is bounded.

Significance

Theorem 2 says the delay of a part under LBFS grows with the number of parts ahead at rate $\overline w+\varepsilon$: the line behaves like a pipeline whose speed is set by its bottleneck center, although parts revisit centers. Theorem 3 converts this into a bound on work in progress that holds for all time, with an asymptotic bound that does not depend on the initial state. Together they give stability of LBFS for every route and every burst size, with explicit constants. This is a deterministic, sample-path result: no distributional assumption on arrivals is needed. Its constants are explicit, so they can be evaluated for a given line.

The results are proved in the paper; none is formalized. The mission produces a machine-checked model of a multi-server reentrant line with nonidling, nonpreemptive, head-of-buffer buffer-priority dispatch, together with Theorems 2 and 3 on it. The model carries over to the other policies of the paper (FBFS, least slack, earliest due date).

Difficulty

The obvious argument fails because under LBFS parts released later do interfere with a part $\pi$: they occupy machines nonpreemptively at the low-priority buffers $\pi$ must still pass. So the delay of $\pi$ cannot be bounded by the work ahead of it alone. The paper's estimate is an induction from the end of the line backwards over the truncated systems $B^{(k)}$, nested with an induction on the position of $\pi$ in its buffer. The constant $c^{(k)}(\varepsilon)$ is recomputed at every level from $c^{(k+1)}(\varepsilon/2)$, so $\varepsilon$ is halved at each level. A formal proof must also handle what the paper treats informally:

• the order in which parts leave buffers when several arrive at the same instant;
• parts already in service at time $0$;
• an empty system between busy periods.

Formalization scope

All declarations are in the namespace ReentrantScheduling.LBFS.

• Buffers are 0-based in Lean: the paper's $b_i$ is index $i-1$.
• A run lists its parts in a fixed line order: parts present at time $0$ first (deeper buffers first, then earlier service start), then released parts by release time. This order breaks ties between simultaneous arrivals, and "parts ahead of $\pi$" means the parts in the system that precede $\pi$ in it.
• Service start times are in WithTop ℝ, with ⊤ meaning never, so a run need not serve every part, and the theorems assert that parts are served. A formalization with real-valued start times would assume every part is served, which is half of what stability asserts.
• All counts (capacity, nonidling, (1), $x(t)$) are Set.encard, never Set.ncard, which would count an infinite set as $0$ and make the capacity rule vacuous.
• The constants $c^{(k)}(\varepsilon)$ of (8)–(9) are explicit definitions that depend only on the line and $\varepsilon$. A constant chosen after the run would let it depend on the arrivals or the initial state.
• Theorem 3's bounds are inequalities in $[0,\infty]$; the lim sup is taken there, so it cannot be a junk value of an unbounded real function.
• The standing assumptions of §II are hypotheses or part of the run predicate: nonidling, nonpreemptive, head-of-buffer service, $m_\sigma\ge1$, $l\ge1$. The positivity $\tau_i>0$ is pinned: the paper leaves it implicit.
• Every theorem quantifies over all admissible LBFS runs. The empty run and nontrivial runs satisfy the hypotheses.

The model is reusable for other dispatch rules on reentrant lines. Proofs of any milestone are welcome, as are lemmas on admissible runs (FIFO within buffers, finiteness of $x(t)$).

Not posed here:

• Example 1, which is already on the platform as QueueingStability.LuKumar.theorem31;
• Theorem 4 and Corollary 1 (least slack, earliest due date), whose proof modifications the paper leaves to the reader;
• Theorem 5 (several flow lines), whose proof is a sketch.

Selected references

• S. H. Lu and P. R. Kumar, Distributed Scheduling Based on Due Dates and Buffer Priorities, IEEE Transactions on Automatic Control 36(12), 1406–1416, 1991. https://doi.org/10.1109/9.106156
• P. R. Kumar and T. I. Seidman, Dynamic Instabilities and Stabilization Methods in Distributed Real-Time Scheduling of Manufacturing Systems, IEEE Transactions on Automatic Control 35(3), 289–298, 1990. https://doi.org/10.1109/9.50339
• J. G. Dai and G. Weiss, Stability and Instability of Fluid Models for Reentrant Lines, Mathematics of Operations Research 21(1), 115–134, 1996. https://doi.org/10.1287/moor.21.1.115