The OR Formalization Drive

Motivation

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 $O(n\log n)$ (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 $m$ 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 $\lceil m/2\rceil$ (Lemma 11). This mission formalizes that bound.

Setting

A flow shop has $m$ processors $P_1,\dots,P_m$ and $n$ jobs. Job $i$ consists of $m$ tasks; task $j$ runs on processor $P_j$ and needs processing time $t_{j,i}\ge 0$ (zero is allowed). A non-preemptive schedule gives every task a start time $s_{j,i}$, and the task occupies $P_j$ during $[s_{j,i},s_{j,i}+t_{j,i})$. It is feasible when all start times are nonnegative, when task $j+1$ of a job starts only after task $j$ of that job has completed ($s_{j,i}+t_{j,i}\le s_{j+1,i}$), and when no processor runs two tasks of positive length at the same time. Its finish time $\mathrm{FT}(s)$ is the latest completion time $s_{j,i}+t_{j,i}$ (and $0$ if there is no task). An optimal finish time (OFT) schedule $S^*$ is a feasible schedule of least finish time.

Heuristic H (p. 48) divides the processors into $\lceil m/2\rceil$ groups: group $g$ consists of $P_{2g-1}$ and $P_{2g}$, and when $m$ is odd the last group is $P_m$ alone. The flow shop $F_g$ on group $g$ has the same jobs, with task times $t_{2g-1,i},t_{2g,i}$ only. For each group an OFT schedule $R(g)$ of $F_g$ is computed (by Johnson's algorithm), with finish time $f(R(g))$. The schedule $S$ generated by H runs these schedules one after another: every task of group $g$ starts at its time in $R(g)$ plus the offset $\sum_{h<g}f(R(h))$.

Formalization targets

Goal: Lemma 11 (p. 49)

For every flow shop with $m$ processors and $n$ jobs, every choice of OFT schedules $R(g)$ of the group flow shops, the schedule $S$ generated by H, and every feasible non-preemptive schedule $\tau$ of the flow shop (in particular an OFT schedule $S^*$),

$$\mathrm{FT}(S)\le\Big\lceil\frac m2\Big\rceil\,\mathrm{FT}(\tau).$$

The paper writes this as $\mathrm{FT}(S)/\mathrm{FT}(S^*)\le\lceil m/2\rceil$.

Milestones

1. Every group flow shop $F_g$ has an OFT schedule (p. 48; the paper obtains it with Johnson's algorithm).
2. The concatenation of feasible group schedules is a feasible schedule of the $m$-processor flow shop (p. 48).
3. $\mathrm{FT}(S^*)\ge\max_g f(R(g))$ (proof of Lemma 11, p. 49).
4. $\mathrm{FT}(S)\le\sum_g f(R(g))\le\lceil m/2\rceil\max_g f(R(g))$ (proof of Lemma 11, p. 49).

Significance

The result gives a polynomial-time heuristic, running in time $O(mn\log n)$, whose finish time is within a factor $\lceil m/2\rceil$ of the optimum on every instance, half the factor $m$ that every busy schedule already achieves. The paper's Example 4 (p. 49) shows that for $m=3$ the factor $2=\lceil 3/2\rceil$ is approached, so the analysis cannot be improved in general.

Formalizing it produces a reusable, machine-checked model of the $m$-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 $m$, 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.

Difficulty

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 $R(g)$ to be optimal, makes the statement false; one that lets $S$ be any schedule with the right restrictions makes it witnessed by $S^*$ 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).

Formalization scope

• Representation. Processors are 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 $g$ (0-based, g : Fin ((m + 1) / 2)) contains the processors $2g$ and $2g+1$ that exist, min 2 (m - 2g) of them.
• Finish time. A fold of max with baseline $0$ over all tasks; it is $0$ for $m=0$ or $n=0$. The maximum of the group finish times is also a fold of max with baseline $0$. No supremum over an unbounded or empty set is taken.
• Zero task times. A zero-length task occupies no processor time (it is exempt from the non-overlap condition) but still respects the job's task order and counts in the finish time when it is placed late; optimal schedules are unaffected.
• The optimum. "OFT schedule $S^*$" is replaced by a universally quantified feasible schedule $\tau$, which is stronger and needs no existence assumption for $S^*$. Optimality of $R(g)$ is the predicate "feasible, and finish time at most that of every feasible schedule of the same group flow shop".
• Constants. $\lceil m/2\rceil$ is (m + 1) / 2 in $\mathbb N$, cast to $\mathbb R$; the two agree for every $m\ge 0$. The ratio is multiplied out, so a zero optimum does not divide by zero.
• Not formalized. Johnson's algorithm and the running times $O(n\log n)$ and $O(mn\log n)$. The goal quantifies over every family of optimal group schedules, which includes the one Johnson's algorithm computes; the paper's proof uses only optimality. The preemptive comparison on p. 50 and the tightness examples are outside the mission.
• Trivialization ruled out. The schedule $S$ is a function of the $R(g)$ with the fixed offsets $\sum_{h<g}f(R(h))$, and each $R(g)$ must be optimal for its group flow shop; neither the offsets nor $S$ are free.
• Infrastructure. Elementary facts about 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.

Selected references

• T. Gonzalez, S. Sahni, Flowshop and Jobshop Schedules: Complexity and Approximation, Operations Research 26(1), 36–52, 1978. https://doi.org/10.1287/opre.26.1.36
• 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, 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

Motivation

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.

Setting

Customers arrive in order at a single server; customer $r$ is served after all its predecessors. On a probability space $(\Omega, \mathcal F, P)$ let

• $t_r \ge 0$ be the interarrival time between customers $r$ and $r+1$,
• $s_r \ge 0$ be the service time of customer $r$.

Assumption 1: the $t_r$ are independent and identically distributed with finite mean $\mathscr{E}(t_r)$. Assumption 2: the $s_r$ are independent and identically distributed with finite mean $\mathscr{E}(s_r)$, and the families $\{s_r\}$ and $\{t_r\}$ are independent of each other.

Put $u_r = s_r - t_r$; the $u_r$ are i.i.d. and integrable, and $\mathscr{E}(u) = \mathscr{E}(s) - \mathscr{E}(t)$ denotes their common mean. The waiting time $w_r$ of customer $r$ (time from arrival to start of service) satisfies Lindley's recursion

$$w_1 = 0, \qquad w_{r+1} = \max(w_r + u_r,\ 0).$$

Write $F_r(x) = p(w_r \le x)$ for the waiting-time distribution function, $G$ for the law of $u_r$, and $U_n = u_1 + \dots + u_n$ for the associated random walk. Lindley shows that $F_r(x)$ converges for every $x$ to

$$F(x) = p(U_s \le x \text{ for all } s \ge 1) \quad (x \ge 0), \qquad F(x) = 0 \quad (x < 0).$$

Formalization targets

Goal: Lindley's theorem (§4, p. 281)

1. The waiting-time distribution $F_r$ converges to a proper (non-degenerate) limit distribution if and only if

$$\mathscr{E}(u) < 0 \quad \text{or} \quad u = 0 \text{ almost surely.}$$

2. If $\mathscr{E}(u) \ge 0$ and $u$ is not almost surely $0$, then $p(w_r \le x) \to 0$ for every $x$.

Milestones, in the order of the paper

• Eq. (2), the one-step convolution $F_{r+1}(x) = \int_{u \le x} F_r(x-u)\,dG(u)$ for $x \ge 0$ (an existing platform statement, referenced).
• Eq. (3), the duality with the random walk: $F_{r+1}(x) = p(U_s \le x \text{ for all } s \le r)$ for $x \ge 0$.
• The limit: $F_r(x) \to F(x)$ for every $x$.
• Eqs. (4)–(5), Lindley's integral equation $F(x) = \int_{u \le x} F(x-u)\,dG(u)$ for $x \ge 0$.
• Case (i): $\mathscr{E}(u) > 0 \Rightarrow F \equiv 0$. Case (ii): $\mathscr{E}(u) < 0 \Rightarrow F(x) \to 1$ as $x \to \infty$.
• Eq. (8), the theorem of Chung and Fuchs quoted by Lindley: a mean-zero, non-lattice random walk comes within $\epsilon$ of every point infinitely often.
• Case (iii): $\mathscr{E}(u) = 0$, $u \not\equiv 0 \Rightarrow F \equiv 0$.
• Companion: for $\mathscr{E}(u) < 0$, exactly one distribution on $[0,\infty)$ solves the integral equation.

Significance

The theorem is the stability criterion $\rho = \mathscr{E}(s)/\mathscr{E}(t) < 1$ 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 $\rho = 1$ 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.

Difficulty

Cases (i) and (ii) follow from the strong law of large numbers, which Mathlib provides. The obstacle is the critical case $\mathscr{E}(u) = 0$: the strong law only gives $U_n/n \to 0$, which says nothing about whether $\sup_n U_n$ 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.

Formalization scope

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 $\mathbb R^{\mathbb N}$, and nonnegativity. Theorems assume IsProbabilityMeasure P. Committed conventions:

• Indexing from 0: w 0 is the paper's $w_1$, F r is $F_{r+1}$, U n $= \sum_{i<n}$ u i is the paper's $U_n$.
• Non-degenerate means proper: the limit is a probability measure $\nu$ on $\mathbb R$, and convergence is $F_r(x) \to \nu((-\infty,x])$ at every $x$ with $\nu\{x\} = 0$. When $u = 0$ a.s. the limit is the point mass at $0$, and the theorem counts it as convergent.
• "Certainly" means almost surely, for $u_1$; all $u_r$ share its law.
• $\mathscr{E}(u)$ is the Bochner integral of the integrable u 0; $G$ is the push-forward law of u 0, and Stieltjes integrals $\int_{u \le x} \cdots dG(u)$ are integrals over Set.Iic x.
• $F(x)$ is defined with the case split $x \ge 0$ / $x < 0$; eqs. (3), (4) are stated for $x \ge 0$, as on the page.
• Eq. (8) is stated for an arbitrary i.i.d. integrable mean-zero sequence (only the non-lattice half).

Trivializing formalizations are ruled out: the goal is about the queue's $F_r$, 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 "$u = 0$" is almost-sure, not pointwise. A verification file builds an Input with $s_r = t_r = 1$, 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.

Selected references

• D. V. Lindley, The theory of queues with a single server, Mathematical Proceedings of the Cambridge Philosophical Society 48(2), 277–289, 1952. https://doi.org/10.1017/S0305004100027638
• K. L. Chung and W. H. J. Fuchs, On the distribution of values of sums of random variables, Memoirs of the American Mathematical Society 6, 1951. https://doi.org/10.1090/memo/0006
• R. M. Loynes, The stability of a queue with non-independent inter-arrival and service times, Mathematical Proceedings of the Cambridge Philosophical Society 58(3), 497–520, 1962. https://doi.org/10.1017/S0305004100036781
• S. Asmussen, Applied Probability and Queues, 2nd ed., Springer, 2003, Ch. III and X. https://doi.org/10.1007/b97236

Motivation

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.

Setting

There are $n\ge1$ jobs and three machines $A$, $B$, $C$. Job $i$ needs time $a_i$ on $A$, then $b_i$ on $B$, then $c_i$ on $C$. Following Johnson, only permutation schedules are considered: a full sequence is a permutation $\sigma$ of the jobs, processed in that order on all three machines, each operation starting as early as possible. Its makespan is the time machine $C$ finishes the last job.

A node $J_r$ is a partial sequence: an ordered list of $r$ distinct jobs. Its unscheduled set $\bar J_r$ is the set of the other $n-r$ jobs. The attributes $\mathrm{TIMEA}(J_r)$, $\mathrm{TIMEB}(J_r)$, $\mathrm{TIMEC}(J_r)$ are the times at which machines $A$, $B$, $C$ finish the jobs of $J_r$ processed in order. A full sequence begins with $J_r$ when its first $r$ positions are $J_r$. The lower bound of a node with $\bar J_r\neq\emptyset$ is

$$LB(J_r)=\max\Big[\mathrm{TIMEA}(J_r)+\sum_{\bar J_r}a_i+\min_{\bar J_r}(b_i+c_i),\ \mathrm{TIMEB}(J_r)+\sum_{\bar J_r}b_i+\min_{\bar J_r}c_i,\ \mathrm{TIMEC}(J_r)+\sum_{\bar J_r}c_i\Big].$$

The branch-and-bound procedure keeps a list of nodes ranked by $LB$, 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 $n-1$ jobs, so that its last job is forced.

Formalization targets

Goal: the stopping rule certifies an optimal sequence

$$\exists k:\ \text{the first node of } \mathrm{run}(k) \text{ is terminal},\qquad\text{and}\qquad \text{first node } P \text{ terminal} \ \Longrightarrow\ \mathrm{makespan}(\sigma_P)\le\mathrm{makespan}(\sigma)\ \ \forall\sigma ,$$

where $\sigma_P$ is $P$ 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.

Milestones

1. Validity of the bound (p. 401): $LB(J_r)\le\mathrm{makespan}(\sigma)$ for every $\sigma$ beginning with $J_r$, $r<n$.
2. Exactness at depth $n-1$ (general form of an observation on p. 403): for $r=n-1$, $LB(J_{n-1})$ equals the makespan of the completed sequence.
3. Node counts (p. 403): at least $\tfrac12n(n+1)$ nodes are created before stopping, at most $1+n+n(n-1)+\cdots+n!$ are ever created, and the list never holds more than $n!$ nodes.
4. Dominance (pp. 403–404): if $J_r$ and $I_r$ contain the same jobs, $\mathrm{TIMEA}(J_r)=\mathrm{TIMEA}(I_r)$; if also $\mathrm{TIMEB}(J_r)\le\mathrm{TIMEB}(I_r)$ and $\mathrm{TIMEC}(J_r)\le\mathrm{TIMEC}(I_r)$, replacing $I_r$ by $J_r$ at the beginning of any sequence does not increase its makespan, and $LB(J_r)\le LB(I_r)$ (p. 404).
5. The 4-job example (pp. 402–403): the run stops after 6 steps with node 231 first, whose bound 62 is the optimal makespan.
6. The refined bound (p. 409): the strengthened bound used in the paper's computations is still a lower bound.

Significance

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 $\tfrac12n(n+1)$ 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.

Difficulty

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.

Formalization scope

Jobs are Fin n (the paper's job $i$ is $i-1$), processing times are arbitrary reals with no sign condition, and full sequences are Equiv.Perm (Fin n). The makespan is the machine-$C$ 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 $\bar J_r$ are Finset.inf'; on an empty set the auxiliary minimum returns a placeholder $0$ that no statement evaluates.

Explicit readings of the paper's phrases:

• "is a lower bound … for any node that emanates from node $P$" is "$\le$ the makespan of every permutation whose first $r$ positions are $J_r$";
• "a node that has scheduled all $n$ jobs" is read as a node with $n-1$ jobs, whose sequence is completed by the forced last job. The example (stop at node 231 of a 4-job problem), the node counts and the formula for $LB$ all require this reading;
• "the problem is solved: that node's sequence is an optimal one" is termination together with optimality over all $n!$ permutations;
• "cannot be hurt by replacing $I_r$ with $J_r$" compares the completions of $J_r$ and $I_r$ by the same ordering of the remaining jobs;
• children are inserted one at a time in increasing job index, each before every node with an equal bound; this reproduces the paper's LIST table;
• dominance discarding is not part of the procedure in the goal.

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.

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
• 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
• 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

Motivation

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 $1\|\sum w_jU_j$. Everything in those applications rests on the claim checked in this mission: that the recursion computes the minimum loss it is said to compute.

Setting

There are $n$ jobs, performed one at a time in the fixed order $1, 2, \dots, n$. Job $j$ can be performed in one of two modes. In the first mode it takes $a_j$ time units, and a loss $\alpha_j(t)$ is incurred if it is completed at time $t$. In the other mode it takes $b_j$ time units, with loss $\beta_j(t)$. Times are nonnegative integers.

A mode assignment $m$ picks a mode for each job, which fixes its processing time $p_j \in \{a_j, b_j\}$. A feasible timing of the first $j$ jobs is a vector of completion times $c_1, \dots, c_j$ with

$$c_{i-1} + p_i \le c_i \qquad (i = 1, \dots, j), \qquad c_0 = 0,$$

so each job starts at time $0$ or later and after its predecessor has finished; idle time between jobs is allowed. The total loss $L_j(m, c)$ is the sum of $\alpha_i(c_i)$ over the jobs $i \le j$ in the first mode and of $\beta_i(c_i)$ over the others. The problem asks for the mode assignment and timing of all $n$ jobs that minimize $L_n(m, c)$.

The paper's recursion is defined for $j = 0, \dots, n$ and integer $t$, with values in $\mathbb R \cup \{+\infty\}$:

$$f(0, t) = 0 \ (t \ge 0), \qquad f(j, t) = +\infty \ (t < 0),$$ $$f(j, t) = \min\{f(j, t-1),\ \alpha_j(t) + f(j-1, t-a_j),\ \beta_j(t) + f(j-1, t-b_j)\} \quad (j \ge 1,\ t \ge 0). \tag{1}$$

Formalization targets

Milestone: Eq. (1) computes the constrained minimum

For $0 \le j \le n$ and every integer $t$, let $\mathcal L(j, t)$ be the set of total losses of the first $j$ jobs over all mode assignments and feasible timings with $c_j \le t$. Then

$$f(j, t) = \min \mathcal L(j, t),$$

meaning: $f(j, t) = +\infty$ exactly when $\mathcal L(j, t)$ is empty, and otherwise $f(j,t)$ is an element of $\mathcal L(j,t)$ and a lower bound for it. No assumption is made on the losses.

Goal: $f(n, T)$ solves the problem

If every $\alpha_j$ and $\beta_j$ is monotone nondecreasing and

$$T = \sum_{j=1}^n \max\{a_j, b_j\},$$

then $f(n, T)$ is finite and equals the minimum of $L_n(m, c)$ over all mode assignments and all feasible timings of the $n$ jobs, with no deadline. This is the paper's sentence "The problem is solved by the calculation of $f(n, T)$, where $T$ is a sufficiently large number. For example, if all of the $\alpha_j$'s and $\beta_j$'s are monotone nondecreasing, we may choose $T = \sum_{j=1}^n \max\{a_j, b_j\}$."

Significance

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 $b_j = 0$ 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.

Difficulty

The paper gives no argument beyond "the usual dynamic programming argumentation". The recursion is in two variables: $f(j, \cdot)$ refers to itself at $t-1$ as well as to $f(j-1, \cdot)$, so the correspondence with timings is not a plain stage-by-stage principle of optimality. The edge cases are where a careless reading fails: $t = 0$, where $f(j, -1) = +\infty$; zero processing times $a_j = 0$ or $b_j = 0$, where $f(j-1, t-a_j)$ is evaluated at the same $t$; and $j = 0$, where the deadline constraint degenerates to $0 \le t$. The goal is harder than the milestone: the problem's feasible set is unbounded, and the horizon $T$ is only sufficient under monotone losses. Without monotonicity the goal is false: one job with $a = b = 1$, $\alpha(1) = 5$, $\alpha(t) = 0$ for $t \ge 2$ and $\beta \equiv 5$ has optimum $0$, attained only at completion time $2 > T = 1$, while $f(1, 1) = 5$.

Formalization scope

• Jobs are Fin n and 0-based: Lean job i is the paper's job $i+1$. The recursion f takes the number $j \in \{0,\dots,n\}$ of jobs done; for $j > n$ its value is $+\infty$ and is never used.
• Modes are Bool, with true the first mode ($a_j$, $\alpha_j$). Processing times are natural numbers and may be $0$. Losses are real-valued functions of the natural-number completion time.
• Integer time is an explicit reading: the paper's recursion steps $t$ by one, so time is discrete.
• $+\infty$ is ⊤ : WithTop ℝ, so $x + (+\infty) = +\infty$ as in the paper.
• Idle time is allowed, and the first job starts at time $0$ or later.
• "Minimum total loss" is read as an attained least element of the set of total losses, with $+\infty$ exactly when that set is empty. "The problem is solved by $f(n, T)$" is read as: $f(n, T)$ is finite, at most every feasible total loss, and attained.
• "Monotone nondecreasing" is 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 $f$; statements in which the optimum is $f$ again, timings forced to have no idle time, an $\mathbb R$-valued $f$ with an arbitrary value for $t < 0$, 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.

Selected references

• E. L. Lawler, J. M. Moore, A Functional Equation and Its Application to Resource Allocation and Sequencing Problems, Management Science 16(1) (1969) 77–84. https://doi.org/10.1287/mnsc.16.1.77
• R. Bellman, Dynamic Programming, Princeton University Press, 1957. https://doi.org/10.1515/9781400835386
• J. M. Moore, An n Job, One Machine Sequencing Algorithm for Minimizing the Number of Late Jobs, Management Science 15(1) (1968) 102–109. https://doi.org/10.1287/mnsc.15.1.102

Motivation

A single machine must process $n$ jobs, each with a processing time and a deadline, and some jobs must be finished before others may start. The first question of any planner is whether the deadlines can be met at all. Without precedence constraints the answer is classical: Jackson's rule (J. R. Jackson, 1955, reported by W. E. Smith, 1956) says that all jobs can be completed on time if and only if they are completed on time when sequenced by earliest deadline first. Precedence constraints break this rule, because the earliest-deadline order may put a job before one of its required predecessors.

E. L. Lawler and J. M. Moore (Management Science 16 (1969) 77–84) repair the rule by replacing each deadline by a modified deadline that accounts for the deadlines of the job's successors. Their §2 Theorem says that a single sequence, the one in increasing order of modified deadlines, decides feasibility. They use it as the first step of their dynamic programming method for sequencing with deadlines and precedence constraints: because the sequence does not depend on processing times, the jobs to be scheduled on time can always be taken in this one fixed order.

Setting

There are $n$ jobs $1,\dots,n$. Job $j$ has a processing time $a_j \ge 0$ and a deadline $d_j \in \mathbb R$. A sequence $\sigma$ lists every job exactly once; the machine starts at time $0$ and processes the jobs in the order of $\sigma$, one after another, without idle time. The completion time $C_j(\sigma)$ of job $j$ is the sum of the processing times of $j$ and of all jobs before it in $\sigma$. Job $j$ is on time in $\sigma$ if $C_j(\sigma) \le d_j$.

Precedence constraints are a partial order $\rho$ on the jobs (reflexive, antisymmetric, transitive). If $i\rho j$ and $i \ne j$, job $i$ must precede job $j$; such a $j$ is a successor of $i$, and every job counts as one of its own successors. A sequence is consistent with $\rho$ if no job appears before a job that must precede it. The jobs are numbered so that $i\rho j$ implies $i \le j$.

For a number $\varepsilon$ the modified deadline of job $j$ is

$$\bar d_j = \min\{\, d_k \mid j\rho k \,\} + j\varepsilon ,$$

the earliest deadline among $j$ and its successors, plus a tie-breaking term. The paper takes $\varepsilon$ to be "a small number"; here that means $\varepsilon > 0$ and $n\varepsilon < d_l - d_k$ whenever $d_k < d_l$.

Formalization targets

Goal: the §2 Theorem (p. 78)

Let $\sigma^*$ be the sequence in which $\bar d_j$ increases. Then

$$\Big(\exists\,\sigma \text{ consistent with } \rho:\ C_j(\sigma) \le d_j\ \ \forall j\Big)\iff C_j(\sigma^*) \le d_j\ \ \forall j .$$

Milestones (from §2 and the proof of the Theorem, p. 78)

1. For distinct jobs, $i\rho j \Rightarrow \bar d_i < \bar d_j$.
2. The sequence $\sigma^*$ is consistent with $\rho$ (the "if" part of the Theorem).
3. If $\bar d_j < \bar d_i$, then $j$ or some successor $k$ of $j$ has $d_k \le d_i$.
4. In an on-time sequence consistent with $\rho$, two adjacent jobs $i, j$ (in this order) with $\bar d_i > \bar d_j$ can be interchanged, and the result is again on time and consistent with $\rho$.

Significance

The Theorem reduces a question over all $n!$ sequences consistent with $\rho$ to the evaluation of one sequence, and the sequence depends only on the deadlines and on $\rho$, not on the processing times. This independence is what the paper's later sections rely on: it lets a subset-selection dynamic program (Eq. (1) of the paper) process jobs in a fixed order. Without precedence constraints ($\rho$ the identity) the Theorem is Jackson's rule. The operational form, "always take next, from among the available jobs, a job which has a successor with the earliest possible deadline", is a list-scheduling rule of the same kind as the backward rule of Lawler (1973) for $1\mid prec\mid f_{\max}$.

The result has been proved on paper since 1969. As far as is known it has no machine-checked proof. This mission produces a formal proof of the Theorem and of the exchange step behind it, stated on the same sequence and completion-time model as the platform's existing single-machine scheduling missions.

Difficulty

The obvious argument is the exchange argument for Jackson's rule: swap an adjacent pair that is out of order and check that nothing becomes late. Two things fail without care. First, the swap must not violate precedence; this is why the deadline of a job is replaced by the minimum over its successors. Second, after the swap, job $i$ completes when job $j$ used to complete, but $d_i$ need not be at least $d_j$: one must find a successor of $j$ that is later in the sequence, on time, and due no later than $i$. That step uses the smallness of $\varepsilon$: with a large $\varepsilon$ the tie-breaking term outweighs a difference of deadlines, and the Theorem fails (three jobs without precedence, $a = (2,4,3)$, $d = (7,9,8)$, $\varepsilon = 3$). Finally, the exchange step must be turned into a terminating transformation of an arbitrary feasible sequence into $\sigma^*$, a bubble-sort argument over lists.

Formalization scope

• Jobs are Fin n, 0-based: the Lean job j is the paper's job $j+1$, and the tie-break is $((j:\mathbb N)+1)\varepsilon$. Processing times and deadlines are real.
• Sequences and completion times are the published platform definitions MooreLateJobs.Shared.IsSchedule and MooreLateJobs.Shared.completionTime (a duplicate-free list of all jobs; start at time $0$, no idle time). Idle time never helps meet a deadline, so this loses nothing. Consistency with $\rho$ is the published LawlerPrec.MinMax.IsFeasible.
• The modified deadline minimizes over insert j {k | ρ j k}, which is nonempty; for the reflexive $\rho$ of the paper this is $\{k \mid j\rho k\}$ ("considering a job to be one of its own successors").
• Explicit readings of the paper's phrases:
  • "$\varepsilon$ is a small number": $\varepsilon > 0$ and $n\varepsilon < d_l - d_k$ whenever $d_k < d_l$. A fixed $\varepsilon$ is quantified universally, not hidden under an existential.
  • "the sequence obtained by ordering jobs according to increasing values of $\bar d_j$": any duplicate-free list of all jobs along which $\bar d_j$ strictly increases. Under the hypotheses the $\bar d_j$ are distinct, so exactly one such list exists.
  • "iρj implies $\bar d_i < \bar d_j$": stated for $i \ne j$, since $\rho$ is reflexive.
  • The pair condition "a consecutive pair with $\bar d_i > \bar d_j$" of milestone 3 is dropped, since the claim does not use it.
• Added hypothesis: $a_j \ge 0$. The paper uses it tacitly ("$j$ will remain on time since it will be earlier in the sequence") and the Theorem is false without it.
• The milestones assume only what they use (for instance, milestone 1 needs transitivity, the numbering and $\varepsilon > 0$). The goal assumes the full partial order of the paper.
• Trivializing formalizations ruled out: $\varepsilon = 0$ or an unconstrained $\varepsilon$; a minimum over a possibly empty set, which Lean would assign a junk value; completion times not tied to the order of the list; and dropping "consistent with the precedence constraints" from the left-hand side, which turns the Theorem into a false variant of Jackson's rule.
• Not in scope: the "order of computational steps" remarks, §3 and the later sections (other missions of this series).

Related platform items: Jackson's rule for unrestricted jobs is already posed as MooreLateJobs.NumLate.jackson (Moore 1968) and is not re-posed here; Lawler's $1\mid prec\mid f_{\max}$ theorem is posed as LawlerPrec.MinMax.sequencing_theorem. Contributions welcome: general list-exchange lemmas (adjacent swaps, bubble-sort termination toward a sorted list) are reusable well beyond this mission.

Selected references

• E. L. Lawler, J. M. Moore, A Functional Equation and Its Application to Resource Allocation and Sequencing Problems, Management Science 16(1) (1969) 77–84. https://doi.org/10.1287/mnsc.16.1.77
• J. R. Jackson, Scheduling a Production Line to Minimize Maximum Tardiness, Research Report 43, Management Science Research Project, UCLA, 1955.
• W. E. Smith, Various Optimizers for Single-Stage Production, Naval Research Logistics Quarterly 3 (1956) 59–66. https://doi.org/10.1002/nav.3800030106
• E. L. Lawler, Optimal Sequencing of a Single Machine Subject to Precedence Constraints, Management Science 19(5) (1973) 544–546. https://doi.org/10.1287/mnsc.19.5.544

Motivation

Minimizing the weighted number of tardy jobs on a single machine, written $1\|\sum w_jU_j$ 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 $p_j = 1$ 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.

Setting

There are $n \ge 1$ jobs, processed by a single machine one immediately following the other from time $0$. Job $j$ has a nonnegative integer processing time $a'_j$, a nonnegative integer deadline $d_j$ and a penalty $p_j \ge 0$. A sequence $\sigma$ is an ordering of all jobs; job $j$ completes at time $C_j(\sigma)$, the total processing time of job $j$ and the jobs before it. Job $j$ is tardy in $\sigma$ if $C_j(\sigma) > d_j$, and the total loss of $\sigma$ is

$$W(\sigma) = \sum_{j \text{ tardy in } \sigma} p_j ,$$

the loss $c_j(t)$ being $0$ for $t \le d_j$ and $p_j$ for $t > d_j$.

The jobs are numbered by deadline, $d_1 \le d_2 \le \cdots \le d_n$. A 0–1 vector $x$ ($x_j = 1$: job $j$ on time; $x_j = 0$: tardy) is prefix-feasible if

$$a'_1x_1 + \cdots + a'_kx_k \le d_k \qquad (k = 1, \dots, n).$$

Equation (3) defines $f(j,t)$ for $j = 0, \dots, n$ and integer $t$:

$$f(j,t) = \begin{cases}\max\{f(j,t-1),\ f(j-1,t),\ p_j + f(j-1,t-a'_j)\}, & 0 \le t \le d_j,\\ f(j, d_j), & t > d_j,\end{cases}$$

with $f(0,t) = 0$ for $t \ge 0$ and $f(j,t) = -\infty$ for $t < 0$.

Formalization targets

Goal: the minimum weighted number of tardy jobs

With $d_1 \le \cdots \le d_n$ and $p_j \ge 0$, $f(n, d_n)$ is finite and

$$\min_{\sigma} W(\sigma) = \sum_{j=1}^n p_j - f(n, d_n).$$

This is the paper's claim that the problem "is solved by" its recursion, with the evaluation point made explicit.

Milestones (Section 5, Section 6, Eq. (3))

1. Section 5. For any sequence, the on-time jobs, sequenced in order of their deadlines and followed by the tardy jobs in arbitrary order, stay on time, and the total loss does not increase.
2. Section 6. Every sequence has a prefix-feasible $x$ with $\sum p_j - \sum p_jx_j \le W(\sigma)$, and every prefix-feasible $x$ has a sequence with $W(\sigma) \le \sum p_j - \sum p_jx_j$: the two problems have the same optimal value.
3. Eq. (3). For $0 \le j \le n$ and $t \ge 0$,

$$f(j,t) = \max\Bigl\{\textstyle\sum_{i \le j} p_ix_i : \sum_{i\le k} a'_ix_i \le d_k\ (k \le j),\ \sum_{i\le j} a'_ix_i \le t\Bigr\}.$$

The goal follows from milestones 2 and 3 at $j = n$, $t = d_n$.

Significance

The result is the exact algorithm for $1\|\sum w_jU_j$ with running time proportional to $n\,d_n$, 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.

Difficulty

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 $k$ that is tardy, the prefix constraint at $k$ is not a completion-time constraint of any job, and only the monotonicity $d_i \le d_k$ for the last on-time job $i \le k$ bounds it. Milestone 3 is a dynamic-programming correctness proof in which the cap $f(j,t) = f(j,d_j)$ for $t > d_j$ and the $-\infty$ base cases must be tracked through a well-founded recursion on $(j, t)$.

Formalization scope

Jobs are Fin n, 0-based: Lean job $j$ is the paper's job $j+1$, and the paper's $f(j,\cdot)$ uses Lean job ⟨j-1, _⟩. Sequences are lists in the published model MooreLateJobs.Shared (IsSchedule Finset.univ l, completionTime, no idle time, start at $0$), which replaces the paper's permutation $\pi$; tardy jobs are the published MooreLateJobs.NumLate.lateSet (strictly $d_j < C_j$). Processing times and deadlines are natural numbers, penalties real. Vectors $x$ are Fin n → Bool. $f$ takes values in WithBot ℝ, with $\bot = -\infty$ and $p + \bot = \bot$; $+\infty$ never occurs.

Explicit readings of the paper's loose phrases:

• Integer data: (3) steps $t$ by $1$ and subtracts $a'_j$, so $a'_j$ and $d_j$ are nonnegative integers.
• Penalties $p_j \ge 0$ ("a penalty $p_j$ is exacted"); the goal, milestone 1 and milestone 2 assume it, milestone 3 does not need it.
• Deadline numbering ("ordering the jobs by deadlines") is Monotone d on the job index; assumed in the goal and milestone 2 only.
• Base cases of (3) are those of Equation (1), with $-\infty$ for a maximum: $f(0,t) = 0$ ($t \ge 0$), $f(j,t) = -\infty$ ($t < 0$). The dominated term $f(j,t-1)$ is kept as printed.
• "Equivalent" is the pair of inequalities of milestone 2, i.e. equal optimal values.
• "Solved by" means $f(n,d_n)$ is finite and $\sum p_j - f(n,d_n)$ is the least weighted number of tardy jobs (IsLeast over all schedules); $n \ge 1$ only so that $d_n$ exists.
• "Arbitrary order" of the tardy jobs in milestone 1 is a universal quantifier over the remaining lists.

Section 5 literally applies Equation (1) with $a_j = a'_j$, $\alpha_j(t) = 0$, $b_j = 0$, $\beta_j(t) = p_j$; 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 $x$; the optimum is a minimum over sequences, not defined as $f$; (3) keeps its cap $f(j,t) = f(j,d_j)$; the goal assumes $p_j \ge 0$ 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.

Selected references

• E. L. Lawler, J. M. Moore, A Functional Equation and Its Application to Resource Allocation and Sequencing Problems, Management Science 16(1), 1969, 77–84. https://doi.org/10.1287/mnsc.16.1.77
• J. M. Moore, An n Job, One Machine Sequencing Algorithm for Minimizing the Number of Tardy Jobs, Management Science 15(1), 1968, 102–109. https://doi.org/10.1287/mnsc.15.1.102
• J. R. Jackson, Scheduling a Production Line to Minimize Maximum Tardiness, Research Report 43, Management Science Research Project, UCLA, 1955.
• J. K. Lenstra, A. H. G. Rinnooy Kan, P. Brucker, Complexity of Machine Scheduling Problems, Annals of Discrete Mathematics 1, 1977, 343–362. https://doi.org/10.1016/S0167-5060(08)70743-X

Motivation

A Nash equilibrium is a joint choice of strategies at which no player can improve their own expected payoff by changing their strategy alone. This gives a testable notion of stable behavior for a finite game, including games in which the players' aims differ. Nash's two-page 1950 note established the existence of such a point for finite games by organizing each player's best replies into a single correspondence and using a fixed-point theorem. The note identifies several properties of that correspondence and ends by comparing equilibrium payoffs in zero-sum and general games. Those claims, stated together in Nash's published note, are the subject of this mission.

The existence conclusion itself already has a proved formal statement, AGT.nash_existence, in the game vocabulary used here. The remaining claims explain what the fixed-point argument acts on: which profiles are related by countering, why countering sets are usable as values of a correspondence, and what their fixed points mean. Keeping those statements explicit makes the 1950 argument legible independently of the existence theorem's proof.

Setting

There is a finite set $I$ of players. Each player $i$ has a finite, nonempty set $S_i$ of pure strategies. A pure-strategy profile $s$ chooses one element of every $S_i$, and $u_i(s)\in\mathbb R$ is player $i$'s payoff. A mixed strategy $P_i$ assigns a nonnegative real weight to each element of $S_i$, with weights summing to one. The space $\Sigma$ of mixed profiles $P=(P_i)_{i\in I}$ is the product of these finite probability simplices.

Players randomize independently. Thus the probability of a pure profile $s$ under $P$ is $\prod_{j\in I}P_j(s_j)$, and player $i$'s expected payoff is

$$U_i(P)=\sum_{s\in\prod_j S_j}\left(\prod_{j\in I}P_j(s_j)\right)u_i(s).$$

For a strategy $\tau_i$ of player $i$, write $U_i(\tau_i,P_{-i})$ for the payoff obtained by replacing only coordinate $i$ of $P$. A profile $Q$ counters $P$ if $Q\in\Sigma$ and, for every player $i$, its coordinate $Q_i$ gives that player the highest expected payoff available against the other players' coordinates of $P$:

$$Q\in C(P)\quad\Longleftrightarrow\quad Q\in\Sigma\quad\text{and}\quad U_i(\tau_i,P_{-i})\le U_i(Q_i,P_{-i}) \quad\text{for every }i\in I\text{ and every mixed }\tau_i.$$

The countering correspondence $C$ assigns the set $C(P)$ to each $P\in\Sigma$. Its graph comprises the pairs $(P,Q)$ with $P\in\Sigma$ and $Q\in C(P)$. A fixed point is a profile $P$ belonging to $C(P)$; Nash calls it an equilibrium point.

Formalization targets

The goal states the three properties of $C$ that Nash uses, along with the identification of its fixed points:

$$\forall P\in\Sigma,\qquad \varnothing\ne C(P)\subseteq\Sigma, \qquad C(P)\text{ is convex};$$ $$P_k\to P,\ Q_k\to Q,\ Q_k\in C(P_k)\text{ for all }k \quad\Longrightarrow\quad Q\in C(P); \qquad P\in C(P)\ \Longleftrightarrow\ P\text{ is a Nash equilibrium}.$$

The milestone list follows the claims in the note: the payoff functions are polylinear and continuous; the correspondence maps mixed profiles to nonempty subsets of mixed profiles; its values are convex; its graph is closed in the sequential formulation Nash writes; and self-countering is equilibrium. A separate closed-set formulation records the graph property in the product topology.

The note also asserts a distinction about payoffs. In a two-person zero-sum game, where $u_0(s)+u_1(s)=0$ on every pure profile, any two equilibria have the same expected payoff for each player:

$$U_i(\sigma)=U_i(\sigma')\qquad(i=0,1).$$

For general games, this can fail. A companion target asks for a finite two-person game with two equilibria having different expected payoffs.

Significance

The correspondence theorem records the precise conditions on which Nash's application of Kakutani's fixed-point theorem rests. Nonempty convex values and a closed graph make the fixed-point route applicable to the mixed-strategy space; the fixed-point clause says why its output is an equilibrium of the game rather than only a topological point. The zero-sum companion separates the common value of a two-person zero-sum game from the possible range of equilibrium payoffs in a general game. These consequences and the comparison appear in Nash's note.

The equilibrium existence theorem is already proved as the referenced AGT.nash_existence. What remains here is to formalize the correspondence properties and the payoff comparison as their own auditable statements, using that theorem's published game definitions. The claims are known results from 1950; their appearance as goals means proofs of these particular statements are still to be supplied in this development.

Difficulty

The payoff of a player depends on every player's strategy, while countering compares only one changed coordinate at a time. The relevant set of maximizers is therefore indexed by the countered profile, and all players' choices must fit into one countering profile. Establishing closedness requires passing the payoff comparisons and the probability-vector conditions through limits of profiles. The zero-sum equality concerns arbitrary pairs of equilibria, which need not use the same strategies; an argument based only on the existence of an equilibrium cannot give it. For general games, a single equilibrium says nothing about whether another equilibrium has a different payoff.

Formalization scope

The Lean development uses a finite player type ι, finite pure-strategy types S i, real payoffs u, and the published definitions AGT.IsLottery, AGT.IsMixedProfile, AGT.expectedPayoff, and AGT.IsMixedNash. The goal and nonempty-value milestone require each S i to be nonempty. The note's probability distributions implicitly require this; the player type itself may be empty. A mixed profile is a tuple of finite real weight vectors, with no measure-theoretic integration or hidden normalization. In the two-person claim, players are 0, 1 : Fin 2.

Convergence is in the ordinary product topology of the real coordinate spaces. The sequence index is $k$ because the note also uses $n$ for the number of players. Counters u P Q requires $Q$ to be a mixed profile and compares $Q_i$ with every mixed deviation against $P_{-i}$; this rules out arbitrary weight vectors and comparisons against the wrong opponents. Neither continuity nor the existence of a best response is assumed in the goal: those properties are targets. The definition layer and the payoff continuity and polylinearity results can be reused by other finite-game formalizations.

Selected references

• J. F. Nash, Jr., Equilibrium Points in n-Person Games, Proceedings of the National Academy of Sciences 36(1), 48–49 (1950). DOI: 10.1073/pnas.36.1.48.
• S. Kakutani, A Generalization of Brouwer's Fixed Point Theorem, Duke Mathematical Journal 8, 457–459 (1941), cited in Nash's footnote 1. DOI: 10.1215/S0012-7094-41-00838-4.