The OR Formalization Drive

Motivation

Commuters choose not only a route but also a departure time, trading travel delay against the penalty of arriving early or late. Static traffic assignment, in the tradition of Wardrop's user-equilibrium principle, ignores the time dimension; dynamic traffic assignment adds it, and its central modelling question is what "equilibrium" means when flows, delays and costs all vary over a time horizon. Friesz, Bernstein, Smith, Tobin and Wie (Oper. Res. 41(1), 1993) proposed the simultaneous route-departure (SRD) equilibrium of a path-based dynamic model and showed that it is equivalent to an infinite-dimensional variational inequality. That equivalence is the starting point of a large literature on dynamic user equilibrium: existence theory, solution algorithms and differential-variational formulations all take the variational inequality as their definition of the problem.

Timeline, as far as this mission is concerned:

• 1952: Wardrop states the static user-equilibrium criterion (equal and minimal travel times on used routes).
• 1979–1980: Smith and Dafermos formulate static user equilibrium as a finite-dimensional variational inequality.
• 1989: Friesz, Luque, Tobin and Wie treat dynamic route choice with a fixed departure schedule as an optimal-control problem.
• 1993: Friesz et al. (this paper) formulate simultaneous route and departure-time equilibrium and prove its equivalence with a variational inequality on $(L^2[0,T])^{|P|}$ (Theorem 2, p. 187).

Setting

A traffic network has a finite set $P$ of paths. Each path $p$ connects exactly one origin–destination (OD) pair $kl$; $P_{kl}$ denotes the paths of pair $kl$. Travellers depart during the horizon $[0,T]$, $T>0$, which carries Lebesgue measure $\nu$; "$\forall_\nu(t)$" means "for $\nu$-almost every $t\in[0,T]$".

A vector of departure-time densities $h=(h_p)_{p\in P}$ assigns to each path a square-integrable, almost everywhere nonnegative function $h_p$ on $[0,T]$: $h_p(t)$ is the rate at which travellers depart at time $t$ on path $p$. The set of such vectors is $H_+$. Each OD pair has a fixed travel demand $Q_{kl}$, and the feasible set is

$$\Lambda=\Big\{h\in H_+ : \sum_{p\in P_{kl}}\int_0^T h_p(t)\,d\nu(t)=Q_{kl}\ \text{for every OD pair } kl\Big\}.\qquad(38)$$

A cost operator gives the effective delay $C_p(t,h)\ge 0$ of departing at time $t$ on path $p$ when the densities are $h$: travel time plus a penalty for early or late arrival (13). Because densities are defined only up to null sets, the relevant lowest achievable cost on a path is an essential infimum,

$$\mu_p(h)=\operatorname{ess\,inf}\{C_p(t,h):t\in[0,T]\}=\sup\{x\in\mathbb R:\ \nu\{t: C_p(t,h)<x\}=0\},$$

and the lowest achievable cost for pair $kl$ is $\mu_{kl}(h)=\min_{p\in P_{kl}}\mu_p(h)$.

Definition 3. For $h\in\Lambda$ and a nonnegative vector $\mu=(\mu_{kl})$, the pair $(h,\mu)$ is an SRD equilibrium if for every OD pair $kl$ and every $p\in P_{kl}$:

$$h_p(t)>0\ \Rightarrow\ C_p(t,h)=\mu_{kl}\quad\forall_\nu(t),\qquad C_p(t,h)\ge\mu_{kl}\quad\forall_\nu(t).$$

No positive-measure set of travellers can lower its cost by switching route or departure time.

Formalization targets

Goal: Theorem 2 (PIE VIP)

For $h^*$ with nonnegative, square-integrable costs $C_p(\cdot,h^*)$:

$$\big(\exists\,\mu^*:\ (h^*,\mu^*)\ \text{SRD equilibrium}\big)\ \Longrightarrow\ h^*\in\Lambda\ \text{and}\ \sum_{p\in P}\int_0^T C_p(t,h^*)\,[h_p(t)-h^*_p(t)]\,d\nu(t)\ge 0\ \ \forall h\in\Lambda,\qquad(39)$$

and conversely, if $h^*\in\Lambda$ solves (39), then $(h^*,\mu(h^*))$ with $\mu^*_{kl}=\mu_{kl}(h^*)$ is an SRD equilibrium. The formal goal states the two directions as two conjuncts; the second names the equilibrium cost vector explicitly, which is stronger than an equivalence with an existential $\mu^*$.

Milestones

1. Lemma 2: a measurable function positive on a set of positive measure exceeds some $\varepsilon_0>0$ on a set of positive measure.
2. The pointwise inequality (42) at an equilibrium, and the necessity half of Theorem 2.
3. Condition (17) holds by construction for $\mu^*=\mu(h^*)$.
4. The positive-measure sets (44)–(46) and (47) produced by a failure of (16).
5. Feasibility (50) of the mass-shifted vector (48)–(49), the value bound (54), and the sufficiency half of Theorem 2.

Significance

The result. Theorem 2 converts an equilibrium defined by almost-everywhere complementarity conditions into a single variational inequality over a convex subset of a Hilbert space. This is what makes dynamic user equilibrium accessible to the general theory of variational inequalities: existence via monotonicity or compactness arguments, and projection-type algorithms in function space or after time discretization. The sufficiency half also identifies the equilibrium cost levels: they are the essential infima $\mu_{kl}(h^*)$, so the multiplier $\mu^*$ need not be found separately.

Formalizing it. The theorem is proved in the paper; no machine-checked version is known. A formal proof requires essential infima, the shifting of mass between paths on sets of prescribed measure (the paper cites Halmos, Proposition 41.2, for the nonatomicity of Lebesgue measure), and careful integrability bookkeeping. The development is a self-contained template for "complementarity conditions a.e. ⇔ variational inequality in $L^2$" arguments, which recur in continuous-time equilibrium models.

Difficulty

Necessity is routine once integrability is in place, though the paper's text asserts the per-path identity $\int_0^T[h_p-h^*_p]\,d\nu=0$, which is false; only the sum over $P_{kl}$ vanishes, and that suffices. Sufficiency is the substantive half. The obvious approach, testing (39) against a perturbation that moves flow from an expensive to a cheap route, has to be carried out with sets rather than points: the costs are only defined almost everywhere, the minimal cost is an essential infimum that need not be attained at any time, and the perturbation must keep the demand constraints exact. This forces the choice of sets of exactly equal positive measure inside the positive-measure sets $S_p(\varepsilon,\delta)$ and $T_q(\varepsilon)$, a nonatomicity argument that a pointwise proof would miss.

Formalization scope

Densities are plain functions $\mathbb R\to\mathbb R$ with a square-integrability condition with respect to $\nu=$ Lebesgue measure restricted to $[0,T]$, not $L^2$ equivalence classes; every pointwise condition is $\nu$-almost everywhere, and values outside $[0,T]$ are unconstrained. Paths and OD pairs are finite types, with a map sending each path to its OD pair. The essential infimum is the literal formula (12), a real supremum; it is not the pointwise infimum, which changes when $C$ is altered on a null set and makes sufficiency false. $\mu_{kl}$ is a real infimum over $P_{kl}$; for a pair with no paths it is an unused default value.

The cost operator C is abstract, with the paper's measurability assumption strengthened to square-integrability so that every integral in (39) is a genuine Lebesgue integral. The network dynamics (3)–(11) that produce C in the paper are not formalized. Nonnegativity (the codomain $\mathbb R_+$ of (13)) and square-integrability are assumed only at $h^*$, which makes the formal statements stronger than the paper's. Without integrability, Lean's integral of a non-integrable function is $0$, so (39) could hold vacuously; the added hypothesis excludes that trivialization. The goal quantifies over every cost operator satisfying these hypotheses and never fixes one. In the milestones, the reduction from $p=q$ to $p\ne q$ (p. 188) is taken as the hypothesis $p\ne q$.

A complete development needs: properties of the real essential infimum (12) on a finite measure space; Lemma 2 (continuity of measure from below); the existence of measurable subsets of prescribed measure in Lebesgue measure (nonatomicity, available in Mathlib in some form); and integral bookkeeping for products of $L^2$ functions on a finite measure. The essential-infimum and mass-shift lemmas are reusable for other continuous-time equilibrium models. Proofs of any milestone, and cleaner restatements of the essential-infimum API, are welcome.

Selected references

• T. L. Friesz, D. Bernstein, T. E. Smith, R. L. Tobin and B. W. Wie, A variational inequality formulation of the dynamic network user equilibrium problem, Operations Research 41(1):179–191, 1993. https://doi.org/10.1287/opre.41.1.179
• J. G. Wardrop, Some theoretical aspects of road traffic research, Proceedings of the Institution of Civil Engineers 1(3):325–362, 1952. https://doi.org/10.1680/ipeds.1952.11259
• M. J. Smith, The existence, uniqueness and stability of traffic equilibria, Transportation Research B 13(4):295–304, 1979. https://doi.org/10.1016/0191-2615(79)90022-5
• S. Dafermos, Traffic equilibrium and variational inequalities, Transportation Science 14(1):42–54, 1980. https://doi.org/10.1287/trsc.14.1.42
• T. L. Friesz, J. Luque, R. L. Tobin and B. W. Wie, Dynamic network traffic assignment considered as a continuous time optimal control problem, Operations Research 37(6):893–901, 1989. https://doi.org/10.1287/opre.37.6.893
• P. R. Halmos, Measure Theory, Van Nostrand, 1950 (Proposition 41.2, nonatomicity of Lebesgue measure).

Motivation

Dynamic traffic assignment models how commuters choose routes and departure times when travel times change over the day. In the model of Friesz, Bernstein, Smith, Tobin and Wie (Oper. Res. 41 (1993)), the time to traverse a path is built recursively from arc exit-time functions: a vehicle that enters an arc at time $t$ leaves it at time $\tau(t)$. The equilibrium conditions of that model refer to the inverses of these functions, so the model is only well defined when every arc exit-time function is invertible.

Invertibility has a direct traffic meaning. A strictly increasing exit time is the first-in-first-out (FIFO) property: a vehicle that enters later cannot leave earlier, so no overtaking occurs on the arc. Whether a given delay model respects FIFO was an active question in the early 1990s, because several delay functions used in practice violate it for some inflow patterns.

Timeline:

• 1969. Vickrey's bottleneck model introduces deterministic queueing at a single bottleneck (Vickrey 1969).
• 1986. Ben-Akiva and De Palma show (Trans. Sci. 20 (1986)), for uniform entry rates and deterministic queueing delays, that it is not possible to "arrive earlier by departing later".
• 1993. Friesz et al. prove (Theorem 1, p. 185) that for every linear arc delay $D = \alpha x + \beta$ the exit time is strictly increasing, extending the 1986 result to all continuous entry-rate patterns (remark, p. 186).

Setting

Consider one arc. Vehicles enter it at the entry rate $u(t) \ge 0$, a continuous function of time $t \ge 0$; the first vehicle enters at time $0$. For an exit-time function $\tau$, the arc volume at time $t \ge 0$ is the inflow mass of the vehicles that entered during $[0,t]$ and have not left by time $t$:

$$x(t) = \int_{\{s \in [0,t]\,:\,\tau(s) > t\}} u(s)\,ds .$$

The linear delay function (18) of the paper is

$$D(t) = \alpha\, x(t) + \beta, \qquad \alpha, \beta > 0,$$

a fixed free-flow travel time $\beta$ plus a queueing time determined by the service rate $1/\alpha$. The exit time is entry time plus delay, so $\tau$ is pinned by the exit-time equation

$$\tau(t) = t + \alpha\, x(t) + \beta \qquad (t \ge 0).$$

The equation is implicit: $\tau$ appears on the right through the volume. The proof partitions time at $t_0 = 0$, $t_{n+1} = \tau(t_n)$; in particular $t_1 = \tau(0) = \beta$ is the exit time of the first vehicle. In Lean these objects are linearDelay, arcVolume, IsLinearExitTime and tSeq in FrieszDUE.FIFO.

Formalization targets

Goal: Theorem 1 (p. 185)

For $\alpha, \beta > 0$ and a nonnegative continuous entry rate $u$, every $\tau$ satisfying the exit-time equation is strictly increasing on $[0, \infty)$:

$$0 \le s < t \implies \tau(s) < \tau(t),$$

and hence injective there, so $\tau^{-1}$ exists.

Milestones

1. Lemma 1 (19): for a differentiable invertible $f$, $[f^{-1}]'(z) = 1/f'[f^{-1}(z)]$.
2. First interval (21)–(24): $t_1 = \beta$; on $[0, t_1]$, $x(t) = \int_0^t u$, $\tau(t) = t + \alpha\int_0^t u + \beta$, and $\tau' = 1 + \alpha u > 0$.
3. Second interval (25)–(28): on $[t_1, t_2]$, $\tau(t) = t + \alpha\int_{\tau^{-1}(t)}^t u + \beta$ and $\tau'(t) = \alpha u(t) + 1/(1 + \alpha u[\tau^{-1}(t)]) > \alpha u(t)$.
4. Induction (29)–(34): the same representation and $\tau'(t) > \alpha u(t)$ on every $[t_{n+1}, t_{n+2}]$, with $\tau$ strictly increasing there.
5. Covering: $t_{n+1} - t_n \ge \beta$ and $\mathbb R_+ = \bigcup_{n \ge 0}[t_n, t_{n+1}]$.

A supporting, non-milestone item states that the exit-time equation has a solution for every admissible $u$.

Significance

The result makes the path exit-time functions of the dynamic network model invertible whenever the arc delays are linear in volume. That invertibility is what allows the path costs, and through them the variational inequality of Theorem 2 of the same paper, to be written down. In traffic terms it certifies that linear volume-based delays never let a later entrant overtake an earlier one, whatever the continuous inflow profile.

The theorem is proved in the paper. As far as is known it has no machine-checked proof. The mission produces one, together with a formal model of a single arc whose exit time is defined implicitly through the volume, which is reusable for other delay functions and for FIFO questions in dynamic traffic assignment.

Difficulty

The obvious argument differentiates $\tau(t) = t + \alpha x(t) + \beta$ and bounds the outflow rate. But the volume can only be written as $\int_{\tau^{-1}(t)}^t u$ once $\tau$ is known to be invertible, which is the conclusion. The paper breaks the circularity by working forward in time: on $[t_n, t_{n+1}]$ the volume depends only on $\tau$ restricted to the earlier interval, whose invertibility is already established. A formal proof must make this forward dependence rigorous for an exit time given only by the implicit equation, handle one-sided derivatives at the junctions $t_n$, where $\tau$ is generally not differentiable, and show that the junctions do not accumulate.

Formalization scope

Time is real; the entry rate is a function $u : \mathbb R \to \mathbb R$ with $u(t) \ge 0$ and $u$ continuous on $[0, \infty)$. Both are added hypotheses: Theorem 1 names none, nonnegativity is implicit in "entry rate", and the remark after the proof covers "all continuous entry rate patterns". Integrals are Lebesgue integrals. Monotonicity is claimed on $[0,\infty)$ only, the entry times that the equation constrains. Derivative claims in the milestones are taken within the closed interval $[t_n, t_{n+1}]$. The paper's separate pieces $\tau_k$ are one global function here, so the junction identities (27), (30), (33) are automatic. Lemma 1 adds the hypothesis $f'[f^{-1}(z)] \ne 0$, without which it is false.

The exit time τ is pinned by the implicit equation τ(t) = t + αx(t) + β, where x(t) is the inflow mass of vehicles that entered by time t and have not exited by time t; no monotonicity or invertibility of τ is assumed. A formalization that defined the volume through $\tau^{-1}$ or assumed $\tau$ monotone would assume the conclusion and is ruled out.

The development needs one-sided derivatives of parametric integrals, the inverse-function derivative on an interval, and a forward induction over the partition. Contributions of proofs for any milestone, of the existence item, and of a uniqueness result for the exit-time equation are welcome.

Selected references

• T. L. Friesz, D. Bernstein, T. E. Smith, R. L. Tobin and B. W. Wie, A variational inequality formulation of the dynamic network user equilibrium problem, Operations Research 41(1):179–191, 1993. https://doi.org/10.1287/opre.41.1.179
• M. Ben-Akiva and A. de Palma, Some circumstances in which vehicles will reach their destinations earlier by starting later: revisited, Transportation Science 20(1):52–55, 1986. https://doi.org/10.1287/trsc.20.1.52
• M. Ben-Akiva, A. de Palma and P. Kanaroglou, Dynamic model of peak period traffic congestion with elastic arrival rates, Transportation Science 20(3):164–181, 1986. https://doi.org/10.1287/trsc.20.3.164
• W. S. Vickrey, Congestion theory and transport investment, American Economic Review 59(2):251–261, 1969. https://www.jstor.org/stable/1823678

Motivation

A task may have a preferred execution time because a material delivery, external event, or downstream operation is timed to it. Starting early can be as costly as starting late. Garey, Tarjan, and Wilfong study this situation on one processor, where tasks cannot overlap but idle time between tasks is permitted. Their total-discrepancy problem is hard when the execution order is free; fixing the order leaves a substantial timing problem because each start can still move and can force changes to earlier starts. The paper gives an explicit scheduling procedure for that case and proves that it minimizes the sum of deviations from preferred starts (Garey, Tarjan, and Wilfong, 1988, §§1–2).

This mission targets that procedure and its correctness theorem. It also records the paper's equal-length result: when task lengths are identical, a minimum-cost schedule exists in preferred-start order, so the fixed-order procedure applies after sorting. These are two precise claims about total discrepancy, distinct from the paper's separate maximum-discrepancy problem.

Setting

There are $n$ tasks, indexed $i=0,\ldots,n-1$. Task $i$ has a nonnegative length $l_i$, a nonnegative preferred starting time $a_i$, and an actual starting time $s_i$. Once started, it occupies the one processor until $s_i+l_i$. Each start must be nonnegative. For the fixed-order problem, task $i$ must finish before task $i+1$ starts, so $s_i+l_i\le s_{i+1}$. This permits idle time when the inequality is strict. The task's discrepancy is $|s_i-a_i|$; because its preferred completion is $a_i+l_i$, this is also its absolute completion-time discrepancy. The total discrepancy is

$$\operatorname{cost}_n(s)=\sum_{i=0}^{n-1}|s_i-a_i|.$$

A block is a maximal consecutive set of tasks with no idle time between neighboring tasks. Within a block, Decrease counts tasks whose actual starts are later than preferred, and Increase counts tasks whose actual starts are no later than preferred. These names describe the effect of moving the entire block earlier: the discrepancy of a Decrease task falls initially, whereas that of an Increase task rises. The algorithm's state is a schedule $S_n$ for the first $n$ tasks. It inserts the next task at its preferred start when the previous task has finished, and at that finish time otherwise. In the latter case it may move the final block earlier until one of the paper's stopping events occurs: the block reaches time zero, a late task reaches its preferred start, or the block meets its predecessor (§2.2, p. 337).

For the equal-length result, schedules may execute tasks in any order. Two distinct tasks are feasible together when one completes before the other starts; meeting at endpoints is allowed. The objective remains the same sum of absolute discrepancies.

Formalization targets

Fixed-order optimality

The main target is the paper's Theorem 2. For all nonnegative task data and every $n$, the actual schedule $S_n$ produced by the block-shifting algorithm is feasible and satisfies

$$\operatorname{cost}_n(S_n)\le\operatorname{cost}_n(s) \qquad\text{for every feasible fixed-order schedule }s.$$

This includes the empty schedule and schedules with idle time. The milestone list follows the paper's own assertions: a balanced final block can move earlier without changing cost; every block of $S_n$ has more Increase tasks than Decrease tasks or begins at zero (Lemma 7); and the two claims in Case 2 of the proof record the cost of adding a late task and the comparison with schedules that place it earlier (Theorem 2 and Lemma 7, p. 338).

Equal-length schedules

The companion target is Theorem 3. If every task has a common length $L\ge0$ and the preferred starts are indexed so that $a_i\le a_{i+1}$, then among all feasible schedules, including those with another task order, at least one minimum-cost schedule starts the tasks in index order:

$$\exists s\;\bigl[ \operatorname{cost}_n(s)\le\operatorname{cost}_n(t) \text{ for every feasible }t \bigr] \quad\text{with }s_i\le s_{i+1}\text{ whenever }i+1<n.$$

The paper uses this statement to connect free-order equal-length scheduling to its fixed-order procedure (Theorem 3, p. 340).

Significance

Theorem 2 certifies an explicit schedule, not just the existence of an optimum. It fixes the objective value for a prescribed execution order and gives a baseline against which any other legal timing of the same tasks can be compared. Theorem 3 supplies the ordering fact needed to use that result when all lengths agree. Together they explain why a problem that is difficult for unrestricted task lengths still has these structured solvable cases (Garey, Tarjan, and Wilfong, 1988, abstract and §2.5).

The paper proves both theorems on paper. The work here is to formalize its schedule construction, cost, block boundaries, and comparison classes in Lean, then obtain machine-checked proofs of the stated targets. The draft theorem declarations compile with proof placeholders; this proposal does not claim that they are already machine-checked results. A completed development would make the model and the algorithm available for later formal work on scheduling with idle time and symmetric earliness and tardiness penalties.

Difficulty

Moving a task closer to its preferred start can move neighboring tasks farther from theirs. A simple task-by-task choice therefore does not establish global optimality. Nor does a count of late and early tasks in one block, by itself, justify arbitrary earlier movements of individual tasks. The difficult comparison in the paper is between the algorithm's schedule and a competing feasible schedule whose new task starts earlier: the whole final block and its constrained relative movements matter. The proof also has to account for the boundary at time zero and for blocks that merge when shifted. These are the reasons the explicit procedure and its block invariant need careful statements (§§2.2–2.3, pp. 337–338).

Formalization scope

The Lean development represents task data and starts as functions from natural-number indices to real numbers; only indices below $n$ count. Task $i$ in Lean is the paper's $T_{i+1}$. Preferred times, lengths, and legal starting times are nonnegative. The start-time condition is a standing convention used by the paper's algorithm, especially its zero-boundary stopping rule. Fixed-order feasibility requires successive tasks to be separated by at least the earlier task's length; unrestricted feasibility uses pairwise nonoverlap. An empty schedule is legal and has cost zero. The representation allows zero-length tasks, as does the paper's $l_i\ge0$ model.

The algorithm is defined by its stated insertion and single-block-shift operations. Defining $S_n$ as a chosen minimizer would erase the content of Theorem 2; the goal also explicitly asserts feasibility so that an illegal low-cost function cannot qualify. Theorem 3 compares with every feasible unrestricted-order schedule, not just schedules already in preferred-start order. The core definitions, the block invariant, and the cost comparisons are useful beyond this particular proof. Formalizing the paper's running-time bounds and heap implementation is outside this mission.

Selected references

• Michael R. Garey, Robert E. Tarjan, and Gordon T. Wilfong, One-Processor Scheduling with Symmetric Earliness and Tardiness Penalties, Mathematics of Operations Research 13(2), 330–348, 1988. DOI: 10.1287/moor.13.2.330.

Motivation

PERT (Program Evaluation and Review Technique) and the critical path method model a project as a directed acyclic network whose arcs are jobs and whose nodes are events; the duration of the project is the length of a longest path from the origin to the terminal. When job durations are random, the quantity a planner wants is the expected duration. Computing it exactly requires solving one longest-path problem for every joint outcome of the job durations: with $m$ jobs each taking two values, $2^m$ deterministic problems. Classical PERT practice replaced every random duration by its mean and reported the longest path for the mean durations. That figure is known to be optimistically biased.

D. R. Fulkerson, Expected Critical Path Lengths in PERT Networks (RAND Memorandum RM-3075-PR, 1962; Operations Research 10(6):808–817, 1962, doi:10.1287/opre.10.6.808), proposed a second estimate, computed node by node with work exponential only in the size of a single node's bundle of incoming arcs, and proved that it lies between the classical mean-length figure and the true expectation.

Setting

A project network has events $0,1,\dots,n$ with $n\ge1$, origin $0$ and terminal $n$. Its arcs are ordered pairs $(i,j)$ with $i<j$, at most one per pair, and every event lies on a directed path from the origin to the terminal. Fulkerson numbers his nodes $1,\dots,n$; his node $i$ is event $i-1$ here. The bundle $B_j$ of an event $j$ is the set of arcs entering $j$, and $\operatorname{pred}(j)$ the set of their tails; the origin's bundle is empty.

For arc lengths $t$, let $\ell_i(t)$ be the length of a longest (critical) path from the origin to $i$; equivalently $\ell_0=0$ and $\ell_j=\max_{i\in\operatorname{pred}(j)}(\ell_i+t_{ij})$.

The lengths of the arcs of each bundle $B_j$ form a random vector with a finite distribution: a finite set $S_j$ of bundle vectors $v$, where $v_i$ is the length of arc $(i,j)$, with probabilities $p_j(v)\ge 0$ summing to $1$. Arcs within a bundle may be correlated; distinct bundles are independent, so an assignment $\omega=(\omega_j)_j$ of one bundle vector per event has probability $p(\omega)=\prod_j p_j(\omega_j)$. Three numbers are attached to each event $i$:

1. the expected critical path length $e_i=\sum_\omega p(\omega)\,\ell_i(t(\omega))$;
2. the mean-length estimate $g_i=\ell_i(\bar t)$, where $\bar t_{ij}=\sum_{v\in S_j}p_j(v)\,v_i$ is the expected length of arc $(i,j)$;
3. Fulkerson's numbers $f_0=0$ and, for $j\neq0$,

$$f_j=\sum_{v\in S_j}p_j(v)\,\max_{i\in\operatorname{pred}(j)}\bigl(f_i+v_i\bigr).$$

Formalization targets

Goal: (4.4)

$$g_i\;\le\;f_i\;\le\;e_i\qquad\text{for every event } i .$$

Milestones

In the order of Fulkerson's induction (pp. 10–12):

1. the recursion for $\ell$ computes the greatest path length (§3, (3.6), and the display on p. 11);
2. $\ell_i(t)$ depends only on the arcs of the bundles $B_0,\dots,B_i$ (p. 6);
3. (4.8): $\max_{i\in\operatorname{pred}(j)}(f_i+\bar t_{ij})\le f_j$;
4. (4.5)/(4.9): if $g_k\le f_k$ for all $k<j$, then $g_j\le f_j$;
5. (4.13): $\sum_{v\in S_j}p_j(v)\max_{i\in\operatorname{pred}(j)}(e_i+v_i)\le e_j$;
6. (4.10)/(4.14): if $f_k\le e_k$ for all $k<j$, then $f_j\le e_j$.

Companion statements

• $g_i\le e_i$ under an arbitrary joint distribution of all arc lengths (remark, p. 12).
• Fig. 4.2: with correlated bundles, $e_3=g_3=1$ but $f_3=5/4$, so (4.4) fails without bundle independence.
• (4.17): an independent example with $g_3=f_3=1<e_3=5/4$.
• Fig. 4.1: explicit values $g_4=3/2$, $f_2=1/2$, $f_3=9/8$, $f_4=55/32$, and $f_i=e_i$.

Significance

The chain (4.4) says that the classical PERT estimate $g$ never overstates the expected project duration, and that the numbers $f$ are a lower bound at least as tight. The $f$ computation visits each node once and sums over the support of that node's bundle only, so its cost grows exponentially with bundle size rather than with network size, while the exact expectation $e$ requires the whole product space. The Fig. 4.2 example shows that the bundle-independence hypothesis cannot be dropped for the upper inequality, while the lower inequality $g\le e$ survives arbitrary dependence.

The result has a complete published proof. This mission seeks a machine-checked proof of (4.4) for finite distributions, with the longest-path characterisation of the earliest-event-time recursion and the locality of critical path lengths as reusable lemmas, and machine-checkable versions of the paper's numerical examples, including the counterexample showing the role of independence.

Difficulty

The left inequality compares an average of maxima with a maximum of averages. The right inequality requires more: $f_j$ averages over the bundle entering $j$, while $e_j$ averages over assignments to every bundle. Taking expectations in $\ell_j=\max_i(\ell_i+t_{ij})$ yields $e_j\ge\max_i(e_i+\bar t_{ij})$, which gives the weaker bound $g\le e$. Fig. 4.2 shows that $f\le e$ can fail when the bundles are dependent. In Lean, $e$ is a sum over a dependent product of finite supports (Fintype.piFinset); its interaction with the local recurrence for $f$ is the central technical difficulty.

Formalization scope

• Network: the published CriticalPath.Events.ProjectNetwork (Kelley–Walker 1959): events Fin (n + 1), arcs a Finset of ordered pairs with strictly increasing labels, origin preceding and terminal following every event. This requires $n\ge1$. Fulkerson's numbering condition "$i\le j$" on p. 3 is read as the strict $i<j$ (arcs join distinct nodes of an acyclic network). There is one arc per ordered pair, Fulkerson's own convention in (3.13).
• Critical path length: the published CriticalPath.Events.earliest, a recursion with Finset.sup' over the nonempty set of incoming arcs. This is the paper's convention that terms of missing arcs are ignored. Nothing uses a default value of $0$ or $-\infty$.
• Distributions: finite, given as data (a support Finset and a weight function per bundle) plus a predicate IsProb (nonnegative weights on the support, summing to $1$, for every event including the origin). Bundle vectors are functions on all events, and coordinates outside $\operatorname{pred}(j)$ are never read.
• Arc lengths are arbitrary reals. §3 assumes nonnegative lengths, but its footnote on p. 4 states that nonnegativity "is not essential in this or the following section"; the statements are given in this more general form.
• No trivialization: $e_i$ is the sum over every assignment of bundle vectors, weighted by the product probability (3.5). It is not defined by a recursion, and the goal assumes none of the milestones. $f$ at node $j$ uses only the distribution of the bundle of $j$.

Infrastructure that a full development needs, and that is reusable elsewhere, includes the longest-path characterisation of the earliest-event-time recursion, the locality lemma, and the factorisation of sums over Fintype.piFinset along one coordinate. Proofs of any milestone or companion are welcome. Out of scope here: §5 (computational examples) and the general-network analogues of §6.

Selected references

• D. R. Fulkerson, Expected Critical Path Lengths in PERT Networks, RAND Memorandum RM-3075-PR, March 1962; published in Operations Research 10(6):808–817, 1962. doi:10.1287/opre.10.6.808
• J. E. Kelley Jr. and M. R. Walker, Critical-Path Planning and Scheduling, Proceedings of the Eastern Joint Computer Conference, 1959, pp. 160–173. doi:10.1145/1460299.1460318
• D. G. Malcolm, J. H. Roseboom, C. E. Clark and W. Fazar, Application of a Technique for Research and Development Program Evaluation, Operations Research 7(5):646–669, 1959. doi:10.1287/opre.7.5.646

Motivation

The maximal multi-commodity flow problem asks how much total flow several commodities, each travelling from its own sources to its own sinks, can send through a network whose arcs have shared capacities. It arises in communication and transportation planning: Kalaba and Juncosa's 1956 study of communication networks (Management Science 3(1)) leads to linear programs of this form. For a single commodity the problem has a clean combinatorial theory: the max-flow min-cut theorem of Ford and Fulkerson (1956, doi:10.4153/CJM-1956-045-5) and the labeling algorithm. With several commodities both fail: the min-cut equality is false, and simplex bases are no longer triangular.

In a short note received in October 1957 and published in Management Science in 1958, L. R. Ford Jr. and D. R. Fulkerson proposed a way to solve the multi-commodity problem with the simplex method anyway (doi:10.1287/mnsc.1040.0269, reprinted 2004). They use the arc-chain formulation, which has one variable per chain from a source to a sink of a commodity. That formulation has far too many variables to write down. The note's point is that the simplex method never needs them explicitly. The "pricing" step (finding a variable to enter the basis, or recognizing that none exists) can be carried out by one shortest-chain computation per commodity, with the simplex multipliers as arc lengths.

Timeline. Ford (1956, RAND P-923) gave the label-correcting shortest-chain procedure the note uses. Ford and Fulkerson (1958) applied it to price the columns of the arc-chain program. Dantzig and Wolfe (1960) generalized the idea into the decomposition principle. Gilmore and Gomory (1961) applied the same pattern to the cutting-stock problem, and it is now called column generation.

Setting

A network has finitely many nodes $P_1,\dots,P_N$ and arcs $A_1,\dots,A_m$. Each arc $A_r$ joins two nodes, has a capacity $b_r$, and is either directed (traversable one way only) or undirected (traversable both ways). There are finitely many commodities; commodity $k$ has a set of sources $S_k$ and a set of sinks $T_k$.

A chain from $u$ to $w$ is the arc set of a path $u = v_0, v_1, \dots, v_p = w$ with distinct nodes, each arc traversable from $v_{i-1}$ to $v_i$. A commodity chain of $k$ is a chain from a node of $S_k$ to a node of $T_k$. List the commodity chains, for all commodities, as $C_1,\dots,C_n$, and let $A = (a_{rs})$ be the incidence matrix: $a_{rs} = 1$ if $C_s$ contains $A_r$ and $0$ otherwise. With $x_s$ the flow along $C_s$ and $x_{n+r}$ the slack of arc $A_r$, the problem is the linear program

$$\text{maximize } \sum_{s=1}^{n} x_s \quad\text{subject to}\quad \sum_{s=1}^{n} a_{rs}x_s + x_{n+r} = b_r,\qquad x_1,\dots,x_{n+m} \ge 0. \tag{2–3}$$

A basis is a set of $m$ columns of $[A \mid I]$ forming an invertible matrix $B = (b_{rj})$. Its simplex multipliers $\alpha_1,\dots,\alpha_m$ satisfy, for every basic column $j$,

$$\sum_{r=1}^{m} \alpha_r b_{rj} = \begin{cases} 1 & j \le n,\\ 0 & j > n.\end{cases} \tag{4}$$

Read as arc lengths, the $\alpha_r$ give each chain $C_s$ the length $\sum_r \alpha_r a_{rs}$. The labeling process for a source set $S$ starts with labels $\pi_i = 0$ on $S$ and $\pi_i = \infty$ elsewhere. It repeatedly finds an arc traversable from $P_i$ to $P_j$ with $\pi_i + l_{ij} < \pi_j$ and replaces $\pi_j$ by $\pi_i + l_{ij}$. In Lean the labels are lab : V → WithTop ℝ, the multipliers are α : E → ℝ, and all objects live in the namespace FordFulkerson58.ArcChain.

Formalization targets

Goal: the shortest-chain pricing test (§3, pp. 1779–1780)

Let $B$ be a basis with basic feasible solution $z$ and multipliers $\alpha \ge 0$. Then:

$$\begin{aligned} &\text{(a) for every commodity, every run of the labeling process with lengths } \alpha \text{ is finite;}\\ &\text{(b) if all final sink labels are } \ge 1, \text{ then } \textstyle\sum_s x_s \le \sum_s z_s \text{ for every feasible } x;\\ &\text{(c) if a final sink label } \pi_t < 1, \text{ some non-basic chain column to } t \text{ has length } \pi_t \text{ and } 1 - \textstyle\sum_r \alpha_r a_{rs} > 0. \end{aligned}$$

Milestones (§3, the labeling process and the test)

1. Termination of the labeling process for non-negative lengths (p. 1780).
2. Final labels are shortest-chain lengths from $S$; the smallest label on $T$ is the $S$-to-$T$ distance (p. 1780).
3. The trace-back: a chain of tight arcs from $S$ to every labeled node, of length its label (p. 1780).
4. If $\alpha \ge 0$ and every commodity chain has length $\ge 1$, the basis is optimal (p. 1779).

Further items state the remarks of §3–§4: a negative multiplier lets a slack enter; the slack basis is a feasible start; dominated chains can be ignored; limited supplies reduce to the same problem by adding new directed source arcs; Figure 2 is the incidence matrix of Figure 1; with negative lengths the labeling process may not terminate.

Significance

The result. The test turns a linear program with exponentially many columns into one whose pricing step costs one shortest-path computation per commodity. Only the $m \times m$ basis is ever stored. This is the first instance of column generation, which now underlies solvers for multi-commodity flow, cutting stock, vehicle routing, crew scheduling and many other set-partitioning models, typically inside branch-and-price. Part (a) together with milestones 2–3 also gives the correctness of Ford's label-correcting algorithm with non-negative lengths, started from a source set and with any order of arc scans.

Formalizing it. The results are classical and proved in the paper's informal style. None of them is formalized: the platform has no arc-chain LP, no column pricing, and no formal statement of Ford's label-correcting process. The general LP facts are on the platform (the simplex optimality criterion and weak duality, both proved) and are included as references. This mission adds the network-specific layer: chains as arc sets of simple paths, the labeling process as a relation on labelings, and the link from final labels to reduced costs. One sentence of the paper is corrected. The trace-back "eventually" reaches $S$ only along some backward path, because zero-length cycles can trap a naive backward search, and milestone 3 states the true version.

Difficulty

The obvious argument for termination says each step lowers a label and there are finitely many chains. It fails: labels are lengths of walks, not chains, and with zero-length arcs (multipliers are often $0$) there are infinitely many walks. Termination needs the finiteness of the set of walk lengths below a bound, not positivity. The correctness of the final labels needs both properties of the labeling: it is produced by the process (so every label is the length of a walk from $S$), and it is terminal. A terminal labeling alone, such as all labels $0$, is not a distance labeling. Finally, the optimality claim is an LP statement about the full, never-enumerated column set. It must be derived from (4), $\alpha \ge 0$ and the shortest-chain lengths, with the chain columns indexed abstractly.

Formalization scope

Nodes, arcs and commodities are finite types V, E, ι. Each arc has tail, head, a per-arc directed flag and a capacity b : E → ℝ; commodities have src snk : ι → Finset V. Parallel arcs and mixed directed/undirected networks are allowed. No sign of the capacities and no disjointness of sources and sinks is assumed, except 0 ≤ b in the zero-flow item, where it is disclosed. Chains are arc sets of simple paths. The null chain at a source is a chain, so sources have distance $0$. Columns are pairs (commodity, chain), so one arc set used by two commodities gives two columns. The columns of $[A \mid I]$ are indexed by Col N ⊕ E. A basis is β : E → Col N ⊕ E with IsUnit (basisMatrix N β).det; its basic feasible solution and multipliers (4) are hypotheses about this β. Labels are in WithTop ℝ with ⊤ for $\infty$. Shortest-chain lengths are finite infima (Finset.inf), equal to ⊤ when there is no chain. The process scans arcs, not node pairs, which handles parallel arcs and the undirected case $l_{ij} = l_{ji}$.

The standing assumption of §3 ("a stage has been reached in the computation where all $\alpha_r$ are non-negative", p. 1779) is a hypothesis of the goal and of milestones 1–4. Milestones 1–3 are stated for any non-negative length function. The paper has no numbered theorems; every milestone is an unnumbered sentence of §3, cited by page and position.

A trivializing formalization is ruled out: the goal does not assume shortest-chain lengths, the trace-back, or any reduced-cost fact beyond (4). Statements about final labels require labelings that are both reachable from the initial labels and terminal, and part (a) shows such labelings exist.

Reusable beyond this mission: the chain and labeling layer (a label-correcting shortest-path algorithm from a source set over mixed networks) and the arc-chain LP. Contributions to the LP layer, which can import the referenced Matoušek–Gärtner results after reindexing, are particularly welcome.

Selected references

• L. R. Ford Jr., D. R. Fulkerson, A suggested computation for maximal multi-commodity network flows, Management Science 5(1):97–101, 1958; reprinted Management Science 50(12S):1778–1780, 2004. https://doi.org/10.1287/mnsc.1040.0269
• L. R. Ford Jr., D. R. Fulkerson, Maximal flow through a network, Canadian Journal of Mathematics 8:399–404, 1956. https://doi.org/10.4153/CJM-1956-045-5
• L. R. Ford Jr., Network Flow Theory, RAND Corporation Paper P-923, 1956. https://www.rand.org/pubs/papers/P923.html
• G. B. Dantzig, P. Wolfe, Decomposition principle for linear programs, Operations Research 8(1):101–111, 1960. https://doi.org/10.1287/opre.8.1.101
• P. C. Gilmore, R. E. Gomory, A linear programming approach to the cutting-stock problem, Operations Research 9(6):849–859, 1961. https://doi.org/10.1287/opre.9.6.849
• J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer, 2007. https://doi.org/10.1007/978-3-540-30717-4

Motivation

Scheduling with earliness and tardiness penalties asks for schedules in which a job finishing early is as undesirable as a job finishing late. The model fits production planned for just-in-time delivery, where finished goods held before their due date cost money, and sequences of experiments tied to fixed external events. It departs from classical scheduling, in which finishing early is never penalized.

Garey, Tarjan and Wilfong (Math. Oper. Res. 13 (1988) 330–348) study the symmetric version on one processor: each task has a preferred starting time, and the penalty is the absolute deviation from it. Their §2.1 settles the complexity of the most natural objective, the sum of these deviations, by proving it NP-complete. The result explains why the rest of their paper, and much of the later literature, turns to special cases that can be solved efficiently: a fixed task order, equal task lengths, or the maximum deviation instead of the sum.

A short history of the model:

• Kanet (1981) minimized total absolute deviation from a common due date that is large enough not to constrain the schedule, by a sorting rule. The special case in the middle of §2.1 is the midtime version of this problem.
• Garey, Tarjan and Wilfong (1988) proved the problem with arbitrary preferred times NP-complete (THEOREM 1, this mission), and gave an $O(N\log N)$ algorithm for a fixed task order.
• Hall, Kubiak and Sethi (1991) proved that the common-due-date problem becomes NP-hard when the due date is restrictive. The reduction of THEOREM 1 already uses a common preferred midtime that is not large, together with one extra task that pins the right end.

Setting

There are $N$ tasks $T_1,\dots,T_N$. Task $T_i$ has a length $l_i$ and a preferred midtime $M_i$. A schedule $S$ assigns every task a starting time $s_i\ge0$ such that no two tasks overlap on the single processor: for $i\ne j$, either $s_i+l_i\le s_j$ or $s_j+l_j\le s_i$. Idle time is allowed. The actual midtime of $T_i$ is $m_i(S)=s_i+l_i/2$, and the total discrepancy of $S$ is

$$\mathrm{cost}(S)=\sum_{i=1}^N |m_i(S)-M_i| .$$

The paper works with midtimes because the special case below is then symmetric. Preferred midtimes and preferred starting times $a_i$ are interchangeable through $a_i=M_i-l_i/2$.

Total discrepancy (the decision problem). Given $N,k\in\mathbb Z^+$ and $M_i,l_i\in\mathbb Z^+$, is there a schedule with $\mathrm{cost}(S)\le k$?

Even-odd partition. Given positive integers $x_1<x_2<\dots<x_{2n}$, can they be split into two sets of equal sum so that each set contains exactly one of $x_{2i-1},x_{2i}$ for every $i$?

The special case. For tasks $T_0,\dots,T_{2n}$ with $0<l_0<l_1<\dots<l_{2n}$ and one common preferred midtime $M>\sum_i l_i$, write $A(S)=\{T_i: m_i(S)<M\}$ and $B(S)=\{T_i:m_i(S)>M\}$. A schedule is ordered if, on each side of $M$, shorter tasks lie nearer to $M$. The bracket $[A_n,\dots,A_1,T_0@M,B_1,\dots,B_n]$ is the schedule that puts $T_0$ at midtime $M$ and packs the listed tasks against it in the listed order.

Formalization targets

Goal: THEOREM 1

$$\text{Partition is NP-complete}\ \Longrightarrow\ \text{Total discrepancy is NP-complete.}$$

The hypothesis is the one result the paper imports (Garey and Johnson, 1979). The conclusion includes membership in NP and polynomial-time many-one reductions from every NP language, with Turing machines as the model of computation.

Milestones, in attack order

1. Even-odd partition is in NP; the instance $x_1=1$, $x_{2i}=x_{2i-1}+y_i$, $x_{2i+1}=x_{2i}+1$ built from a Partition instance $Y$ is a yes-instance if and only if $Y$ is; and LEMMA 1, even-odd partition is NP-complete.
2. The special case: a minimum cost schedule has no gaps and is ordered; LEMMA 2 (some $m_i(S)=M$), LEMMA 3 ($|A(S)|=|B(S)|$), LEMMA 4 ($m_0(S)=M$), LEMMA 5 (swapping $A_i$ and $B_i$ in a bracket keeps the cost), LEMMA 6 ($\{A_i,B_i\}=\{T_{2i},T_{2i-1}\}$ in a minimum cost bracket), and the minimum cost

$$k=\sum_{i=1}^n(l_{2i}+l_{2i-1})\left(n-i+\tfrac12\right)+l_0\,n .$$

3. At the midtime $M=\frac12\sum_{i=0}^{2n}l_i$ used in the reduction, every schedule of $T_0,\dots,T_{2n}$ costs at least $k$; equality forces the ordered, gap-free form in item 2.
4. The reduction: the instance D with $l_0=x_1-1$, $l_i=x_i$, $l_{2n+1}=2$, $M_j=M=\sum_{i\le 2n}l_i/2$, $M_{2n+1}=2M+1$ has a schedule of cost at most $k$ if and only if $X$ has an even-odd partition. Total discrepancy is in NP.

Significance

THEOREM 1 is the hardness boundary for one-processor scheduling with symmetric earliness–tardiness penalties and arbitrary preferred times. It is the reason exact algorithms for this objective are enumerative, and the reason polynomial results are sought under extra structure, such as the fixed-order algorithm of the same paper. The special-case lemmas characterize every optimal schedule for a common, unrestrictive midtime, not just one of them: shortest task centered at $M$, the $i$-th pair of lengths in the $i$-th positions on either side, either member on either side. This characterization holds independently of the reduction.

The result has been proved since 1988, and no machine-checked version of it is known to us. A formalization adds three things. First, the parts the paper calls "straightforward" or "a simple exercise", membership of both problems in NP. Second, the two places where the published argument is imprecise. The instance D has half-integer midtimes and threshold although the decision problem asks for integers, so a correct reduction must rescale. And the special-case lemmas are proved for a large midtime but applied with $M=\sum_i l_i/2$, so they must be restated for every $M$. Third, a reusable formal treatment of absolute-deviation scheduling objectives and of reductions between number problems written in binary.

Difficulty

The obvious argument fails at the step from the special case to the instance D. The lemmas on pp. 333–336 assume the common midtime is large, so that the constraint $s_i\ge0$ never binds. In D the midtime is $M=\sum_{i=0}^{2n}l_i/2$, exactly half the total length, and the reduction works because the constraint binds. The tasks before $M$ must fit in $[0,M-l_0/2]$, and the extra task $T_{2n+1}$ must sit at $[2M,2M+2]$. Together these force the two sides to have equal total length. A proof that only cites the large-$M$ lemmas proves nothing about D. Conversely, dropping $s_i\ge 0$ makes the reduction false: put the shorter element of every pair after $M$.

The other obstacle is the complexity bookkeeping. NP-completeness here means Turing machines, binary codes, and polynomial bounds, and a full proof must compute D from the code of $X$, double the times to clear the half-integers, and certify membership in NP for a problem whose schedules have real starting times. The certificate cannot be the real starting times themselves.

Formalization scope

• Everything is real-valued except the instance codes. Schedules have real starting times $s_i\ge0$, and integer data are cast to $\mathbb R$. Restricting to integer starting times would be a different problem and is not what is stated.
• Nonnegative starting times are a standing assumption. The paper uses them ("scheduled between 0 and $M-l_0/2$", p. 336) without writing them into the model. Nonoverlap is "one task finishes before the other starts", the reading of "intersect only at their endpoints".
• Tasks are indexed by Fin N from $0$. In the special case $T_i$ is index $i$, and the paper's $T_{2i-1},T_{2i}$ ($1\le i\le n$) are the indices $2k+1,2k+2$ for $k=i-1$.
• Languages use the published CookPvsNP_defs (Cook's one-tape Turing machines, NP, NPComplete) and the published ProjSchedTW.Complexity.Encoding (four-letter alphabet and binary codes). This mission defines positivePartitionLang by restricting the imported equal-sum predicate to nonempty lists of positive integers, as on p. 333. Only codes of well-formed instances belong to the even-odd and total discrepancy languages.
• The goal is not the combinatorial equivalence of milestone 4. It states NP-completeness, so it contains the polynomial-time computation of the reduction and membership in NP. Taking NPComplete evenOddLang as the hypothesis instead would drop LEMMA 1 and is not what is asked.
• Running times of the algorithms of §2.2–§2.4 are out of scope for this mission, as are all results after §2.1.

Contributions welcome: proofs of any milestone, and reusable lemmas on Turing-machine computability of arithmetic on binary codes, which the two membership results and both reductions need.

Selected references

• M. R. Garey, R. E. Tarjan, G. T. Wilfong, One-Processor Scheduling with Symmetric Earliness and Tardiness Penalties, Mathematics of Operations Research 13(2):330–348, 1988. https://doi.org/10.1287/moor.13.2.330
• M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979.
• J. J. Kanet, Minimizing the average deviation of job completion times about a common due date, Naval Research Logistics Quarterly 28(4):643–651, 1981. https://doi.org/10.1002/nav.3800280411
• N. G. Hall, W. Kubiak, S. P. Sethi, Earliness–tardiness scheduling problems, II: Deviation of completion times about a restrictive common due date, Operations Research 39(5):847–856, 1991. https://doi.org/10.1287/opre.39.5.847
• S. Cook, The P versus NP problem, Clay Mathematics Institute Millennium Problems, 2000. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf

Motivation

A game without side payments (an NTU game) describes cooperation in which utility cannot be transferred between players: each coalition $A$ of players is assigned the set $V(A)$ of payoff vectors it can secure on its own. The core is the set of payoffs to the grand coalition that no coalition can improve upon. Whether the core is nonempty is the basic stability question of cooperative game theory. For games with side payments the answer is the Bondareva–Shapley theorem. For NTU games it is Scarf's theorem (Scarf 1967): a balanced game has a nonempty core. Billera (1970) gave a convex version, in which the payoff sets are convex and balancedness is stated with weighted Minkowski sums.

Aubin's paper (Aubin 1981) obtains Billera's version of the theorem by a different route. Players may join coalitions at fractional rates of participation, and the paper first proves a core existence theorem for these fuzzy games. The game on ordinary coalitions is then embedded into a fuzzy game whose core lies inside the core of the original game.

Setting

The players are $N = \{1,\dots,n\}$. A coalition $A \subseteq N$ is identified with its characteristic vector $\tau^A \in \{0,1\}^n$, and $\tau^N = (1,\dots,1)$. A fuzzy coalition is a vector $\tau \in [0,1]^n$ of participation rates with support $A_\tau = \{i : \tau_i > 0\}$. Write $(\tau\cdot c)_i = \tau_i c_i$, $\mathbb{R}^\tau = \tau\cdot\mathbb{R}^n$ for the vectors vanishing off $A_\tau$, $\mathbb{R}^\tau_+$ for its nonnegative part, and $\mathring{\mathbb{R}}^\tau_+$ for the vectors strictly positive on $A_\tau$.

A fuzzy game without side payments assigns to each $\tau \ge 0$ a nonempty, closed, convex set $V(\tau)\subseteq\mathbb{R}^\tau$. Each $V(\tau)$ is comprehensive, meaning $V(\tau) = V(\tau)-\mathbb{R}^\tau_+$, and bounded above, meaning $V(\tau)\subseteq C-\mathbb{R}^\tau_+$ for some $C$. The map is positively homogeneous: $V(t\tau) = tV(\tau)$ for every $t>0$. Its core is the set of $c\in V(\tau^N)$ such that $\tau\cdot c\notin V(\tau)-\mathring{\mathbb{R}}^\tau_+$ for every fuzzy coalition $\tau\neq 0$. With the support function $v(\tau,\lambda)=\sup_{c\in V(\tau)}\sum_i\lambda_i c_i$ and the simplex $M^n$, a weak (resp. strong) canonical cooperative equilibrium is a $c\in V(\tau^N)$ together with a $\bar\lambda\in M^n$ (resp. $\bar\lambda$ with all coordinates positive) satisfying $\sum_i\bar\lambda^i\tau_ic_i\ge v(\tau,\bar\lambda)$ for every $\tau\in[0,1]^n$.

A usual NTU game lives on a family $\mathcal{C}$ of coalitions that contains $N$ and every singleton. For each $A\in\mathcal{C}$, the set $V(A)\subseteq\mathbb{R}^A$ is nonempty, closed, convex, comprehensive and bounded above. A balance of $\tau$ is a vector of weights $m\ge 0$ on $\mathcal{C}$ with $\sum_{A\ni i}m(A)=\tau_i$ for every $i$, and $\mathcal{C}(\tau)$ is the set of balances of $\tau$. The fuzzy extension of the game is

$$\pi V(\tau)=\bigcup_{m\in\mathcal{C}(\tau)}\ \sum_{A\in\mathcal{C}} m(A)\,V(A),$$

and the game is balanced if $V(N)=\pi V(\tau^N)$.

Formalization targets

Goal: Theorem 7.1

For a balanced game without side payments,

$$\emptyset\neq\operatorname{core}(\pi V)\subseteq\operatorname{core}(V),\qquad \mathrm{CCE}_{\rm strong}(V)\subseteq\operatorname{core}(\pi V)\subseteq\mathrm{CCE}_{\rm weak}(V),$$

and in particular $\operatorname{core}(V)\neq\emptyset$.

Milestones

• Proposition 3.1: $c\in V(\tau^N)$ is in the core iff the maximum complaint $\alpha(c)=\sup_{\tau\neq0}\inf_{\lambda\in M^\tau}[v(\tau,\lambda)-\sum_i\lambda^i\tau_ic_i]$ is $\le 0$.
• Proof of Theorem 3.1(b): if $V$ is superadditive, $V(\tau)+V(\sigma)\subseteq V(\tau+\sigma)$, then $\tau\mapsto v(\tau,\lambda)$ is concave on $\mathbb{R}^n_+$.
• Theorem 3.1: strong equilibria lie in the core, and for a superadditive game the core lies in the set of weak equilibria.
• Theorem 5.1: a superadditive fuzzy game has a nonempty core.
• §7, (6), (7), (11): $\pi V$ is a superadditive fuzzy game that extends $V$, and its support function is $\pi v(\tau,\lambda)=\sup_{m\in\mathcal{C}(\tau)}\sum_A m(A)v(A,\lambda)$.
• §7 and the proof of Theorem 7.1: under balancedness, $\operatorname{core}(\pi V)\subseteq\operatorname{core}(V)$, and the equilibria of $V$ coincide with those of $\pi V$.

Significance

Theorem 7.1 gives the core existence result for convex NTU games under Billera's balancedness condition. Its proof goes through a statement about fuzzy coalitions, Theorem 5.1, which uses no combinatorial pivoting. That theorem also has independent uses. Its fuzzy core is the solution concept that §4 of the paper identifies with Walras equilibria of exchange economies. The canonical cooperative equilibria give a price-like certificate, a common rate of transfer $\bar\lambda$, that sandwiches the core.

The results are classical and proved. Prove2Me holds no statement of Scarf's or Billera's theorem, of NTU cores, or of balancedness for games without side payments, and Mathlib has none of these notions. The mission produces faithful statements of the paper's chain of results, and their proofs once solvers close them. It also builds reusable infrastructure: support functions of comprehensive sets, Minkowski combinations indexed by balances, and positively homogeneous set-valued maps.

Difficulty

Most of §7 is bookkeeping with Minkowski sums. The hard part is Theorem 5.1, the existence of a point in the fuzzy core. The core is defined by infinitely many exclusion conditions, one for each $\tau\in[0,1]^n$, so a finite intersection argument does not apply directly. The paper's route works with prices: it uses the superdifferential of the concave map $\tau\mapsto v(\tau,\lambda)$ at $\tau^N$, Ky Fan's inequality on a truncated simplex where all $\lambda_i\ge\varepsilon$, and a limit as $\varepsilon\to0$. That limit requires compactness of the approximating payoffs, and at the boundary of the simplex the superdifferential map is not upper semicontinuous. Theorem 3.1(b) needs a minisup theorem for a function that is concave in $\tau$ and convex and lower semicontinuous in $\lambda$. Mathlib has neither Ky Fan's inequality nor this minimax theorem in that form.

Formalization scope

All statements import one definitions file, FuzzyGames.NTUCore.Basic. The formalization commits to the following conventions.

• Players are Fin n, and payoffs, fuzzy coalitions and rates of transfer are Fin n → ℝ, ordered coordinatewise. $\mathbb{R}^\tau$ is encoded as "vanishes where $\tau_i=0$", which equals $\tau\cdot\mathbb{R}^n$ for $\tau\ge0$.
• Fuzzy games are defined directly on the orthant $\tau\ge0$, the paper's extension of $V$ from $[0,1]^n$ by homogeneity. Homogeneity holds for every $t>0$, and superadditivity holds on $\mathbb{R}^n_+$.
• Support functions, $\alpha$ and $\pi v$ take values in EReal, so an unbounded supremum is $+\infty$ and never a junk $0$.
• The supremum defining $\alpha(c)$ ranges over $\tau\neq0$. Since $M^0=\emptyset$, including $\tau=0$ would make $\alpha\equiv+\infty$ and Proposition 3.1 false. Blocking coalitions are likewise $\tau\neq0$, as in §3 (4).
• $\mathcal{C}$ is a finite family of nonempty coalitions that contains $N$ and every singleton. "$\forall A\neq\emptyset$" in §7 ranges over $\mathcal{C}$.
• The paper leaves $n\ge1$ implicit. Theorem 3.1(b) and Theorem 5.1 carry $0<n$: for $n=0$ the simplex is empty while the core is not.
• In §7 (11), $\pi v(\tau,\lambda)$, which the paper uses without defining it, is taken to be the extension §6 (2) applied to $A\mapsto v(A,\lambda)$, for $\lambda\ge0$.
• The §7 sentence after (5) is stated with two extra conclusions: $\pi V(\tau)$ is nonempty and contained in $\mathbb{R}^\tau$. These are the remaining requirements of §3 (3) that are needed to apply Theorem 5.1.
• Sums and scalings of sets are Mathlib's pointwise operations.

The fuzzy-game axioms are a Prop-valued structure and are hypotheses of every theorem. The core and the equilibria are defined for an arbitrary set-valued map, so the theorems about $\pi V$ do not presuppose that it is a fuzzy game. That fact is the content of the §7 milestones and is not assumed. Non-vacuity has been checked locally on a concrete instance: $V(\tau)=\{c\in\mathbb{R}^\tau: c\le\tau\}$ is a superadditive fuzzy game, and $V(A)=\{c\in\mathbb{R}^A:c\le\tau^A\}$ is a balanced game on every admissible $\mathcal{C}$, with $(1,\dots,1)$ in both cores.

Contributions are welcome at every level: the §7 Minkowski-sum lemmas, the support-function identities, and a minisup or Ky Fan theorem in the form the proofs need. Reusable pieces include support functions of comprehensive sets and Sion-type minimax.

Selected references

• J.-P. Aubin, Cooperative Fuzzy Games, Mathematics of Operations Research 6(1) (1981) 1–13. https://doi.org/10.1287/moor.6.1.1
• H. E. Scarf, The Core of an N Person Game, Econometrica 35(1) (1967) 50–69. https://doi.org/10.2307/1909888
• L. J. Billera, Some Theorems on the Core of an n-Person Game without Side-Payments, SIAM Journal on Applied Mathematics 18(3) (1970) 567–579. https://doi.org/10.1137/0118053
• K. Fan, A Minimax Inequality and Applications, in O. Shisha (ed.), Inequalities III, Academic Press (1972) 103–113.

Motivation

In just-in-time scheduling each job has a preferred time, and finishing it early is as undesirable as finishing it late. Garey, Tarjan and Wilfong (Math. Oper. Res. 13 (1988), 330–348) study the one-processor version in which task $T_i$ has a length $l_i \ge 0$ and a preferred starting time $a_i \ge 0$, and the discrepancy of a task started at time $s_i$ is $|s_i - a_i|$. The penalty is symmetric: earliness and tardiness cost the same. The paper shows that minimizing the total discrepancy is NP-complete, gives an $O(N \log N)$ algorithm for a fixed task order, and, in §3, gives an efficient algorithm for minimizing the maximum discrepancy $\max_i |s_i - a_i|$: a linear-time test for a given bound $\gamma$ after an $O(N \log N)$ sort, combined with a search over $\gamma$.

This mission formalizes the structural core of §3: the normal-form theorems (Theorem 4, Corollaries 1 and 2) on which the paper's algorithm for maximum discrepancy is built. The two companion missions of the series cover the NP-completeness result (THEOREM 1) and the fixed-order algorithm (THEOREMS 2 and 3).

Setting

Fix a bound $\gamma \ge 0$. A schedule has maximum discrepancy at most $\gamma$ exactly when every task starts no earlier than its release time $r_i = \max\{0, a_i - \gamma\}$ and finishes no later than its deadline $d_i = a_i + l_i + \gamma$ (p. 342). These release times and deadlines are in special form: with $\alpha = 2\gamma$, for every task

$$d_i - r_i = l_i + \alpha \quad\text{or}\quad \big(r_i = 0 \text{ and } d_i < l_i + \alpha\big).$$

From here on the data are arbitrary reals $l_i \ge 0$, $r_i \ge 0$, $d_i$ in special form for some $\alpha \ge 0$.

A schedule is an execution order $\sigma$ ($\sigma(p)$ is the task in position $p$) with starting times $s_i$, such that a task finishes no later than any later-positioned task starts: $s_{\sigma(p)} + l_{\sigma(p)} \le s_{\sigma(q)}$ for $p < q$. It is feasible if $r_i \le s_i$ and $s_i + l_i \le d_i$ for every $i$. Its makespan is $\max_i (s_i + l_i)$, and it is optimum if it is feasible and no feasible schedule has a smaller makespan.

Let $T_N$ be a task of largest deadline. A schedule has the release time property if every task executed after $T_N$ has release time strictly later than the starting time of $T_N$. When the tasks are indexed with $d_1 \le \dots \le d_N$, a schedule is in standard form with split index $j$, $0 \le j \le N-1$, if it begins with an optimum schedule of $T_1, \dots, T_j$, followed by $T_N$ started at the maximum of $r_N$ and the completion time of that first part, followed by $T_{j+1}, \dots, T_{N-1}$ in this order without idle time.

Formalization targets

Goal: Corollary 2 (p. 344)

$$\exists\ \text{a feasible schedule} \;\Longrightarrow\; \exists\ \text{an optimum schedule that is in standard form and has the release time property.}$$

Milestones

1. Theorem 4 (pp. 342–343): if a feasible schedule exists, some optimum schedule has the release time property with respect to any task of largest deadline.
2. The deadline split (proof of Corollary 1, p. 344): in every feasible schedule with the release time property, a task $T_i \neq T_N$ precedes $T_N$ if and only if $d_i \le s_N + \alpha$.
3. Corollary 1 (p. 344): some optimum schedule executes before $T_N$ exactly the tasks of deadline at most $\beta$, for some $\beta \ge 0$.
4. Release before finish (p. 344): every task executed after $T_N$ has $r_i \le s_N + l_N$.
5. Normalization after $T_N$ (p. 344): an optimum schedule with the release time property can be changed, without moving $T_N$ later and without touching the tasks before it, so that there is no idle time from the start of $T_N$ on and the later tasks run in deadline order.

Two companion items state the reformulation of the maximum-discrepancy bound as release times and deadlines, and the special form with $\alpha = 2\gamma$.

Significance

Corollary 2 reduces the search for an optimum schedule of $T_1, \dots, T_n$ to $n$ candidates, one per split index, each assembled from an optimum schedule of a shorter prefix. This is the dynamic program of §3.2, which the paper implements in $O(N)$ time after an $O(N \log N)$ sort; combined with a search over $\gamma$ it minimizes the maximum discrepancy. Without the special form, deciding whether one processor can meet arbitrary release times and deadlines is NP-complete (reference [4] of the paper, Garey and Johnson 1979), so the normal form is what separates the tractable case from the general one.

The results are proved in the paper; no machine-checked proof of them is known on Prove2Me. A formal proof of Corollary 2 would certify the correctness of the split-index recursion and, together with the companions, of the reduction from maximum discrepancy to this release-time/deadline problem.

Difficulty

The obvious argument fails in Theorem 4. Exchanging a straggler (a task after $T_N$ released no later than $T_N$ starts) with $T_N$ shifts the tasks between them, and for general release times and deadlines those tasks can become infeasible. The paper's argument uses the special form at every step: a task released after $T_N$ starts has $r_i > 0$, hence $d_i - r_i = l_i + \alpha$ exactly, and this equality is what bounds how far tasks may move. It also needs an extremal choice of the optimum schedule (fewest tasks after $T_N$, then fewest tasks between $T_N$ and the first straggler), which requires showing that optimum schedules exist over the reals. The passage to standard form then combines this with an earliest-deadline exchange for the tasks after $T_N$ and the replacement of the first part by an optimum sub-schedule without losing feasibility of the later tasks.

Formalization scope

Tasks are indexed by Fin N (0-based: the paper's $T_1, \dots, T_N$ are $0, \dots, N-1$; the paper's $T_N$ in Corollary 2 is the index $N-1$). All data are real. A schedule is a permutation σ : Fin N ≃ Fin N with starting times s : Fin N → ℝ; "executed before/after" refers to σ, not to a comparison of starting times, because zero-length tasks may share a starting time. Execution intervals meet at most at endpoints. The makespan is a supremum over Fin N; "optimum" quantifies over all feasible schedules, not only standard-form ones.

The standing hypotheses on every structural item are $\alpha \ge 0$, $r_i \ge 0$, $l_i \ge 0$ (from $\gamma \ge 0$, the $\max\{0, \cdot\}$ in $r_i$, and nonnegative lengths); since $s_i \ge r_i$, start times are nonnegative, as the paper assumes throughout. The special form is a hypothesis of every structural item and cannot be dropped. The paper's dummy task $T_0$ ($r_0 = d_0 = l_0 = 0$) is not a task; an empty first part completes at time $0$. Corollary 1's "the set of all tasks with deadline $\beta$ or less" is read as excluding $T_N$, the only reading under which it is true. The page's "(which can be assumed optimum)" is part of the standard form. The deadline-split and release-before-finish milestones are stated for every feasible schedule, as their arguments allow.

A trivializing formalization is excluded: the standard form pins $T_N$'s start to $\max(r_N, C)$ and the later tasks to consecutive positions in index order, so the goal is not Corollary 1 restated with an unconstrained split.

Running times ($O(N \log N)$, $O(N)$) and the algorithm of §3.2 are out of scope. The development needs only finite permutations, finite suprema and the exchange arguments of §3.1; the existence of an optimum schedule (minimum makespan over finitely many orders, earliest-start schedules) is reusable for other single-machine problems with release times and deadlines. Proofs of any milestone, and a sorry-free proof of the existence of optimum schedules, are welcome.

Selected references

• M. R. Garey, R. E. Tarjan, G. T. Wilfong, One-Processor Scheduling with Symmetric Earliness and Tardiness Penalties, Mathematics of Operations Research 13(2):330–348, 1988. https://doi.org/10.1287/moor.13.2.330
• M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979 (reference [4] of the paper, cited on p. 342 for the NP-completeness of one-processor scheduling with release times and deadlines). ISBN 0-7167-1045-5