The OR Formalization Drive

Motivation

Network revenue management is the problem of selling several limited, perishable resources (seats on flight legs, hotel room-nights, machine hours) to customers who arrive over time and each want a fixed bundle of them. A seller who accepts every request early may run out of the resources that the most valuable later customers need, and a seller who is too cautious leaves capacity unsold at the end of the horizon. Airlines, hotels and car-rental firms solve instances of this problem daily (Talluri and van Ryzin, 2004).

The exact optimal policy is a dynamic program over the vector of remaining capacities, which is intractable for realistic networks. The standard remedy replaces the random demand by its mean, which gives a linear program, the deterministic LP (DLP), and turns its solution into an admission rule. Its value is an upper bound on what any policy can earn (Gallego and van Ryzin, 1997). Solving the LP once, at time zero, loses $O(\sqrt{T})$ against that bound over a horizon of length $T$. A natural improvement is to re-solve the LP as capacity is consumed.

Timeline of the re-solving question, as the source surveys it (Sec. 1, pp. 3–4):

• 1997: Gallego and van Ryzin: static policies built from the DLP lose $\Theta(\sqrt{T})$.
• 2002: Cooper gives an example in which re-solving the DLP makes booking-limit control worse.
• 2008: Reiman and Wang re-solve exactly once, at an endogenous random time, with probabilistic allocation, and obtain $o(\sqrt{T})$ loss.
• 2012: Jasin and Kumar prove that re-solving after every unit of time with probabilistic allocation (the policy FR below) loses $O(1)$, provided the DLP solution is nondegenerate. Wu et al. (2015) obtain $O(1)$ for one resource, with a constant that blows up as the solution approaches degeneracy.
• 2018: Bumpensanti and Wang (arXiv:1802.06192) show that FR can lose $\Omega(\sqrt{T})$ against the hindsight optimum on a degenerate instance, propose a modified policy with $O(1)$ loss in all cases, and prove that FR never loses more than $O(\sqrt{T})$ against the DLP. This mission formalizes the last of these results.

Setting

There are $n$ customer classes $j \in [n]$ and $m$ resources $l \in [m]$. Over the horizon $[0, T]$, class-$j$ customers arrive according to independent Poisson processes with rates $\lambda_j > 0$. Accepting a class-$j$ customer earns $r_j \ge 0$ and consumes $a_{lj} \ge 0$ units of each resource $l$; $A = (a_{lj})$ is the bill-of-materials matrix and $A_j$ its $j$-th column. The initial capacity vector is $C \ge 0$. A customer can be accepted only if $A_j \le C'$ componentwise, where $C'$ is the capacity remaining at its arrival.

For a capacity-per-unit-time vector $b \ge 0$, let

$$v(b) = \max\Big\{ \sum_{j=1}^n r_j x_j \ :\ \sum_{j=1}^n A_j x_j \le b,\ 0 \le x_j \le \lambda_j \Big\}.$$

The DLP value is $v^{\mathrm{DLP}}(T, C) = T\, v(C/T)$.

The Frequent Re-solving policy (FR) divides the horizon into $T$ unit periods $[t, t+1)$. At the start of period $t$, with remaining capacity $C(t)$, it sets $b(t) = C(t)/(T - t)$, computes an optimal solution $x(t)$ of the LP with right-hand side $b(t)$, and during the period accepts each class-$j$ arrival with probability $x_j(t)/\lambda_j$, subject to the capacity check. Its expected revenue is $v^{\mathrm{FR}}(T, C)$. The LP may have several optimal solutions; the results hold for every rule choosing among them.

Formalization targets

Goal: Proposition 3

There is a constant $M$, depending only on $\lambda$, $r$ and $A$, such that for every integer $T \ge 1$, every capacity $C \ge 0$ and every choice of optimal LP solutions,

$$v^{\mathrm{DLP}}(T, C) - v^{\mathrm{FR}}(T, C) \le M \sqrt{T}.$$

The content is the uniformity: $M$ does not depend on $C$, so the bound holds whether capacity is scarce, abundant, or degenerate for the LP.

Milestones, in the order the proof uses them

1. Eq. (32), p. 35. The capacity check costs FR at most $\sum_j r_j(\log T + 1) + \sum_j r_j \lambda_j$ relative to the LP revenue it targets:

$$v^{\mathrm{FR}} \ge \mathbb{E}\Big[\sum_{t=0}^{T-1} \sum_{j=1}^n r_j x_j(t)\Big] - \sum_{j=1}^n r_j (\log T + 1) - \sum_{j=1}^n r_j \lambda_j .$$

2. Eq. (33), p. 35. LP sensitivity in the right-hand side: $v(b) - v(b') \le \sum_l r^l_{\max} (b_l - b'_l)^+$ with $r^l_{\max} = \max_j r_j \mathbb{I}(a_{lj} > 0)/a_{lj}$.
3. Lemma 8, p. 43 (corrected). $\mathbb{E}[(b_l - b_l(t))^+] \le K_l \sqrt{\sum_{i=0}^{t-1} (T-i-1)^{-2}}$ with $K_l = \sqrt{\sum_j a_{lj}^2 \lambda_j}$.
4. p. 36. $\sum_{t=0}^{T-1} \sqrt{\sum_{i=0}^{t-1} (T-i-1)^{-2}} \le 2\sqrt{T} + \sqrt{2}$.
5. p. 36, explicit bound.

$$v^{\mathrm{DLP}} - v^{\mathrm{FR}} \le \sum_{l=1}^m r^l_{\max} K_l (2\sqrt{T} + \sqrt{2}) + n\, r_{\max} (\log T + 1) + n\, r_{\max} \lambda_{\max} .$$

Significance

The result. Because $v^{\mathrm{DLP}}$ bounds the expected revenue of every admissible policy, Proposition 3 says that FR loses at most $O(\sqrt{T})$ against the optimal policy in every instance, degenerate or not. Re-solving therefore never does worse, in order, than solving once. Together with the $\Omega(\sqrt{T})$ lower bound on a degenerate instance (Proposition 2 of the same paper), it shows that the order $\sqrt{T}$ is exact for FR. The nondegeneracy assumption of the earlier $O(1)$ analysis cannot be dropped. The explicit form (milestone 5) bounds the loss by constants computable from $(\lambda, r, A)$.

Formalizing it. The result is proved in the source; no part of it is machine-checked. A formalization adds three things. It gives a precise model of an adaptive, randomized admission policy in a Poisson network, which other results on re-solving and bid-price policies can reuse. It gives a checked LP sensitivity bound. And it checks the paper's constants: the printed constant of Lemma 8 is wrong (see Formalization scope), and the mission states the corrected one.

Difficulty

The obvious argument compares FR with the DLP period by period: the LP that FR solves at time $t$ differs from the original only in its right-hand side, so the loss should be controlled by how far $b(t)$ drifts below $b = C/T$. Two things break a naive version of this. First, $b(t)$ is a ratio whose denominator $T - t$ shrinks to $1$, so fluctuations late in the horizon are amplified; a crude bound on the drift at each $t$ sums to more than $\sqrt{T}$. Second, FR's realized consumption is not the LP's target: the capacity check rejects customers, and the LP solutions $x(i)$ depend on the whole past, so the consumption in different periods is not independent.

Uniformity in $C$ is the whole point. Arguments that rely on a margin between $C/T$ and the degenerate points of the LP, as in the nondegenerate analysis, give constants that blow up as that margin vanishes.

Formalization scope

The source is arXiv:1802.06192v3, whose printed page numbers equal the PDF page numbers. Everything lives in the namespace ResolvingNRM.FRUpper.

• LP value. $v(b)$ is the published piValue A r b lam of RLPBidPrice.Unbiased.Model (a real supremum, equal to the LP maximum for $b \ge 0$).
• Optimal solutions. The "$\arg\max$" of Algorithm 2 is an arbitrary optimal-solution selector sel; every theorem quantifies over all selectors, with constants chosen before the selector.
• Randomness. Within a period the acceptance probabilities are fixed, so the period's arrivals are represented exactly as a Poisson number of customers in arrival order, with i.i.d. classes of law $\lambda_j / \sum_i \lambda_i$ and independent Bernoulli acceptance coins. Expectations are series over this law (windowExp). FR's value is a backward recursion over periods (frTail), and expectations of functions of $C(t)$ are a forward recursion (frStateExp).
• Horizon. $T$ is a positive integer; capacities are real vectors.
• Standing assumptions of p. 7, left implicit there and hypotheses here: $\lambda_j > 0$, $r_j \ge 0$, $a_{lj} \ge 0$, $C \ge 0$.
• $O(\cdot)$. "$= O(\sqrt{T})$" is $\exists M,\ \forall\, \mathrm{sel}, T \ge 1, C \ge 0$. The paper's threshold $T_1$ is dropped, which is equivalent because $0 \le v^{\mathrm{FR}}$ and $v^{\mathrm{DLP}} \le T\sum_j r_j\lambda_j$.
• Corrected slip, Lemma 8. The printed $K_l = \sqrt{\sum_j a_{lj}^2 \lambda_j^2}$ is false: the proof replaces the conditional variance $x_j(i) \le \lambda_j$ of a Poisson increment by $\lambda_j^2$. With one class, one resource, $a = 1$, $\lambda = 0.01$, $C = \lambda T$, $T = 1000$ and $t = 2$, an exact computation gives $\mathbb{E}[(b - b(2))^+] \approx 1.96 \cdot 10^{-5}$, above the printed bound $1.42 \cdot 10^{-5}$. The mission uses $K_l = \sqrt{\sum_j a_{lj}^2 \lambda_j}$ in Lemma 8 and in the explicit bound.
• Index slip. The paper's sums $\sum_{l=1}^L$ run over its $m$ resources and are read as $l \in [m]$.

A trivializing formalization is ruled out. The constant $M$ is chosen before $C$. FR is defined with every optimal LP solution, not only nondegenerate or vertex ones. The capacity check is kept arrival by arrival; without it, FR's expected revenue would equal the LP revenue it targets and the gap would be trivially small.

Contributions welcome on every milestone. The LP sensitivity bound (33) is a statement about linear programs alone and milestone 4 about real numbers alone; both are reusable outside this mission, as is the window model of a randomized admission policy.

Selected references

• Y. Bumpensanti, H. Wang, A Re-solving Heuristic with Uniformly Bounded Loss for Network Revenue Management, arXiv:1802.06192v3, 2018 (the source of this mission; later in Management Science 66(7), 2020). https://arxiv.org/abs/1802.06192
• G. Gallego, G. van Ryzin, A Multiproduct Dynamic Pricing Problem and Its Applications to Network Yield Management, Operations Research 45(1), 24–41, 1997.
• W. L. Cooper, Asymptotic Behavior of an Allocation Policy for Revenue Management, Operations Research 50(4), 720–727, 2002.
• M. I. Reiman, Q. Wang, An Asymptotically Optimal Policy for a Quantity-Based Network Revenue Management Problem, Mathematics of Operations Research 33(2), 257–282, 2008.
• S. Jasin, S. Kumar, A Re-Solving Heuristic with Bounded Revenue Loss for Network Revenue Management with Customer Choice, Mathematics of Operations Research 37(2), 313–345, 2012.
• K. T. Talluri, G. J. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2004.

Bibliographic details of the non-arXiv entries are those of the source's reference list (pp. 24–25).

Motivation

Value iteration computes the optimal value function of a Markov decision process by applying the dynamic programming backup to every state until the values stop changing. When the state space is too large for a lookup table, practitioners replace the table by a function approximator: after each backup, the new values are computed only at a sample of states and an approximator (a neural net, a spline, a nearest-neighbour rule) is fitted to them. This approximate value iteration is the basis of much of reinforcement learning, and in the early 1990s it was known to work well in some experiments and to diverge in others, with no theory separating the two. Boyan and Moore (NIPS 7, 1995) exhibited divergence with linear regression and neural nets, and Tsitsiklis and Van Roy (1996) later studied the same question for feature-based architectures.

Gordon's technical report (CMU-CS-95-103, 1995; a shorter, differently numbered version appeared at ICML 1995) isolated a property of the approximator that guarantees convergence: the approximator must not exaggerate differences between target value functions in max norm. It identified a broad class with this property, the averagers (k-nearest-neighbour, kernel averaging, linear and bilinear interpolation on a mesh), and proved that in a discounted problem approximate value iteration through an averager always converges, with an explicit error bound. This mission formalizes that discounted theory: the report's §2–§3 and its error bound of §6.1.

Setting

A finite Markov decision process $M$ has states $1,\dots,n$, a finite nonempty set $U(i)$ of actions at each state $i$, an expected one-step cost $c_{ia}$ for action $a$ at state $i$, and transition probabilities $p_{aij}\ge0$ with $\sum_j p_{aij}=1$. It is discounted with factor $0\le\gamma<1$. A value function is a vector $V\in\mathbb R^n$, measured in the max norm $\|V\|=\max_i|V(i)|$.

The parallel value backup operator $T_M$ updates every state at once:

$$(T_MV)(i)=\min_{a\in U(i)}\Big(c_{ia}+\gamma\sum_{j=1}^n p_{aij}V(j)\Big).$$

Its fixed point $V^*$ is the optimal value function, the minimal expected discounted cost from each state.

A function approximator is studied through its mapping $M_F$: the function sending a vector of target values to the vector of fitted values. Two operators $M_F$ and $T$ are compatible if the iterates $(M_F\circ T)^k(x_0)$ converge from every initial guess $x_0$.

An averager $A$ is given by constants $k_i$ and nonnegative weights $\beta_i,\beta_{ij}$ with $\beta_i+\sum_j\beta_{ij}=1$ for every $i$; its mapping is

$$M_A(Y)_i=\beta_ik_i+\sum_{j=1}^n\beta_{ij}Y_j .$$

The weights are fixed in advance and do not depend on the targets $Y$.

Formalization targets

Goal: Theorem 6.2 (p. 12)

Let $V^A$ be any fixed point of $M_A$ and $\varepsilon=\|V^A-V^*\|$. Then there is $V_0$ such that $(T_M\circ M_A)^k(V)\to V_0$ from every initial guess $V$, and

$$\|V_0-V^*\|\le\frac{2\gamma\varepsilon}{1-\gamma}.$$

The goal has two parts: convergence from every start to a common limit $V_0$, and the error bound on that limit.

Milestones

1. Theorem 2.2, first clause (p. 4). $\|T_MV-T_MW\|\le\gamma\|V-W\|$.
2. Theorem 3.2 (p. 7). $M_A$ is a max-norm nonexpansion, $\|M_A(Y)-M_A(Z)\|\le\|Y-Z\|$, and is compatible with $T_M$ for every discounted MDP.
3. Theorem 3.1 (p. 5). If $M_F$ is any max-norm nonexpansion, then $M_F$ is compatible with $T_M$ and $\|M_F(T_MV)-M_F(T_MW)\|\le\gamma\|V-W\|$.
4. Corollary 3.1 (p. 6). There is $V_\infty$ with $\|(M_F\circ T_M)^k(V)-V_\infty\|\le\gamma^k\|V-V_\infty\|$ for all $V$ and $k$.

A further item, not a milestone, is the display after the proof of Theorem 6.2 (p. 13), the bound on the fitted output: $\|V^*-M_A(V_0)\|\le2\varepsilon+2\gamma\varepsilon/(1-\gamma)$.

Significance

Theorem 6.2 gives a guarantee that depends only on how well the approximator can represent $V^*$, not on how the iteration is started: if some fixed point of the averager lies within $\varepsilon$ of $V^*$, approximate value iteration finds a function within $2\gamma\varepsilon/(1-\gamma)$ of $V^*$. Theorems 3.1 and 3.2 explain why: an averager is a max-norm nonexpansion, and composing a nonexpansion with a $\gamma$-contraction leaves a $\gamma$-contraction. Together they separate the approximators that are safe to use with value iteration from those that are not (linear regression is not a nonexpansion: the report's Figure 2 shows it can expand max-norm distances).

All results of this mission are proved in the report; none is open. The contraction of the discounted Bellman operator and the identification of its fixed point with the optimal value function are proved on Prove2Me (BertsekasDP.discounted_main_theorem, used here as a reference item). No machine-checked proof of Gordon's averager results or of the $2\gamma\varepsilon/(1-\gamma)$ bound is known to exist; this mission produces one, on top of the published finite MDP model.

Difficulty

Each step is short on paper; the difficulty is in the bookkeeping that a formal proof cannot skip. The nonexpansion of an averager rests on nonnegative weights summing to at most one, which must be extracted from the row constraint $\beta_i+\sum_j\beta_{ij}=1$ in the max norm on $\mathbb R^n$. The goal's convergence clause asks for one limit $V_0$ shared by all initial guesses, which needs completeness of $\mathbb R^n$ and the contraction-mapping theorem applied to $T_M\circ M_A$, not to $T_M$. The error bound compares three different fixed points ($V^*$ of $T_M$, $V^A$ of $M_A$, $V_0$ of $T_M\circ M_A$) in a chain of triangle inequalities. The order of composition matters throughout: the compatibility results iterate $M_F\circ T_M$ (fit after the backup), while the goal iterates $T_M\circ M_A$ (back up after the fit), and the two may not be interchanged.

Formalization scope

• The MDP is the published BertsekasSSPModel (Fin n states, a finite action type, nonempty admissible action sets $U(i)$, costs g, transition probabilities p), and $T_M$ is its BertsekasDiscountedBellmanOp M γ. That model allows substochastic rows; every statement adds the hypothesis $\sum_j p_{aij}=1$ for admissible $a$, which makes it the report's MDP. Action sets may depend on the state, a harmless generalization of the report's single action set. The initial-state distribution $S_0$ never enters a statement and is omitted.
• The discount satisfies $0\le\gamma<1$ in every item. Theorem 6.2's page says only "with discount factor $\gamma$"; it belongs to the report's discounted discussion and its proof uses that $T_M$ is a $\gamma$-contraction.
• $\|\cdot\|$ on Fin n → ℝ is Mathlib's sup norm, i.e. the max norm.
• $V^*$ is a hypothesis: a fixed point of $T_M$. Theorem 2.2's last clause, proved on the platform as BertsekasDP.discounted_main_theorem, identifies it with the optimal value function.
• The averager acts on whole value functions $\mathbb R^n\to\mathbb R^n$, indexed by the states. The report's approximator fits a sample $X_0$ of states; ignoring the value at a state $j$ outside the sample is the special case $\beta_{ij}=0$.
• Theorem 3.1 is printed with "$X=S\times A$" and $M_F\in\mathbb R^{|X|}\mapsto\mathbb R^{|X|}$; since $T_M$ acts on value functions of the state, $M_F$ is stated on $\mathbb R^n$.
• "Converges at the rate $\gamma$" (Corollary 3.1) is the geometric rate of the contraction-mapping theorem, $\gamma^k$ times the initial distance to the limit.
• Theorem 6.2 keeps $\varepsilon=\|V^A-V^*\|$ as an equality, as printed, and its conclusion keeps the convergence clause. A statement asserting only the existence of some $V_0$ with $\|V_0-V^*\|\le2\gamma\varepsilon/(1-\gamma)$ would be trivial ($V_0=V^*$) and is not the theorem.
• Lemma 2.1 and the Contraction Mapping theorem (Theorem 2.1) are in Mathlib (LipschitzWith.comp, ContractingWith) and are not posed.

Proofs of any item are welcome, as are reusable lemmas on max-norm nonexpansions of row-stochastic linear maps, which also serve the nondiscounted companion mission (Stable Function Approximation in Dynamic Programming II).

Selected references

• G. J. Gordon, Stable Function Approximation in Dynamic Programming, Technical Report CMU-CS-95-103, Carnegie Mellon University, 1995; shorter version in Machine Learning Proceedings 1995 (ICML), 1995. https://doi.org/10.1016/B978-1-55860-377-6.50040-2
• D. P. Bertsekas and J. N. Tsitsiklis, Parallel and Distributed Computation: Numerical Methods, Prentice Hall, 1989 (the report's [BT89]; no DOI).
• J. A. Boyan and A. W. Moore, Generalization in Reinforcement Learning: Safely Approximating the Value Function, Advances in Neural Information Processing Systems 7, MIT Press, 1995 (the report's [BM95]).
• J. N. Tsitsiklis and B. Van Roy, Feature-Based Methods for Large Scale Dynamic Programming, Machine Learning 22, 1996, pp. 59–94. https://doi.org/10.1007/BF00114724

Motivation

Queueing results often relate an average accumulated over customers to an average accumulated over time. In the familiar relation $L=\lambda W$, the long-run average number in a system equals the arrival rate times the average time spent there. Glynn and Whitt study a broader relation, $H=\lambda G$, that can represent queue lengths and waiting times but also costs, work, and other cumulative inputs. Their framework is deterministic: a stochastic model may supply a sample path, yet the central comparison is a statement about functions on that path. This lets the same theorem apply to different queueing models without choosing a probability law for each one. Glynn and Whitt (1989)

The paper asks for more than the usual forward implication from a customer average to a time average. Its main theorem identifies conditions under which either average has a finite limit exactly when the other does. It also compares lim inf and lim sup when ordinary limits fail to exist. Both questions matter when sample paths fluctuate: convergence of one average cannot simply be inferred from a visual similarity between the two ways of indexing the input. Glynn and Whitt (1989), §§1–2

Setting

A cumulative input is a real-valued function $F(s,t)$ on $[0,\infty)\times[0,\infty)$, nondecreasing separately in the customer coordinate $s$ and the time coordinate $t$. Its marginal limits $F(s,\infty)$ and $F(\infty,t)$ are finite for every fixed argument. The first counts all eventual input associated with customers through index $s$; the second counts all input accumulated through time $t$. The marginal averages are

$$G(s)=\frac{F(s,\infty)}{s},\qquad H(t)=\frac{F(\infty,t)}{t}.$$

The paper permits cumulative inputs that are not distribution functions of measures on rectangles. In particular, it does not require a rectangle-increment inequality or nonnegative values of $F$. The finite marginal limits and monotonicity are the actual assumptions of its general framework. Glynn and Whitt (1989), p. 635, (1)

A time change $T_i(s)$, for $i=1,2$, is finite, nonnegative, nondecreasing, and right-continuous, and tends to infinity with $s$. Its right-continuous inverse is $S_i(t)=\inf\{s\geq0:T_i(s)>t\}$. The two time changes may differ. Both have the same asymptotic rate $T_i(s)/s\to\lambda^{-1}$ for a positive finite $\lambda$. The paper's two approximation conditions are

$$\frac{F(s,T_1(s-))-F(\infty,T_1(s-))}{s}\longrightarrow0 \quad(14), \qquad \frac{F(s,\infty)-F(s,T_2(s))}{s}\longrightarrow0 \quad(15),$$

as $s\to\infty$, where $T_1(s-)$ is the left limit. Condition (14) concerns input already present by a left-limit time; condition (15) concerns input not yet present by a right-limit time. Glynn and Whitt (1989), p. 638, (3), (14)–(15)

Formalization targets

One-sided asymptotic bounds

With only (14) and the rate for $T_1$, the corrected upper bounds are

$$\liminf H\leq\liminf \lambda G,\qquad \limsup H\leq\limsup \lambda G.$$

With only (15) and the rate for $T_2$, the corrected lower bounds reverse both inequalities. The two bounds remain useful separately when only one approximation condition holds. Their lim inf and lim sup may be infinite. Glynn and Whitt (1989), p. 639, Theorem 1(a)–(b) and Remark 2

Equality of asymptotic bounds and finite limits

Under both conditions, Theorem 1(c) asserts equality of the respective lim inf and lim sup. The mission goal is Theorem 1(f): for finite real limits,

$$H(t)\to h\quad\Longleftrightarrow\quad G(s)\to g, \qquad\text{and whenever these limits exist, }h=\lambda g.$$

Here the equivalence means existence of finite limits, with the second clause identifying their values. The lim inf and lim sup statement is retained as a milestone because it also covers nonconvergent paths. Glynn and Whitt (1989), p. 639, Theorem 1(c), (f)

Significance

The goal gives a two-way transfer between customer-indexed and time-indexed long-run averages. If an application establishes one finite average, the theorem supplies the other and fixes its value. The one-sided milestones give meaningful bounds when only one approximation condition is available; the lim inf and lim sup milestone retains information when neither average converges. These outcomes are stated for a general cumulative input, so applications can supply their own $F$, $T_1$, and $T_2$ without changing the theorem. Glynn and Whitt (1989), §§2–4

The paper proves these results on paper. The formalization target is a machine-checked interface for the paper's deterministic framework, its inversion lemmas, its asymptotic inequalities, and the two-way limit theorem. At this drafting stage the Lean theorem statements compile with proof placeholders; no machine-checked proofs of these new statements are claimed. The definitions and inverse-rate lemma can be reused in other sample-path results.

Difficulty

The two marginal averages examine different slices of $F$, and a time change may jump or have flat intervals. A direct substitution of $t=T_i(s)$ does not give an equality between $F(s,\infty)$ and $F(\infty,t)$ under the paper's assumptions. The left limit in (14) and the value in (15) also behave differently at jumps. The inverse $S_i$ connects the coordinates, but its boundary behavior and rate must be handled before comparing the averages. These issues are present even without stochastic randomness. Glynn and Whitt (1989), pp. 638–639

Formalization scope

Lean represents $s,t$ by nonnegative real numbers and $F$ by a real-valued function with separate monotonicity and bounded marginal ranges. Real suprema represent $F(s,\infty)$ and $F(\infty,t)$; the boundedness fields ensure those suprema are the paper's finite limits. The inverse is an infimum of a nonempty set because $T_i\to\infty$. The left limit is the supremum over earlier nonnegative arguments, with $T(0-)=0$. Ratios at zero use Lean's total division convention, but every ratio assertion is asymptotic at infinity.

Lim inf and lim sup are taken in the extended reals so an unbounded average retains an infinite limit. Multiplication by $\lambda$ happens in the reals before conversion. Ordinary limits in Theorem 1(f) are finite real limits. The two time changes are independent and share only the positive rate $\lambda$. The goal assumes only (14), (15), and the stated time-change rates; it does not assume its own inverse-rate or asymptotic conclusions. No nonnegativity or rectangle inequality is imposed on $F$.

Theorem 1(a) and (b) have their hypothesis pairing reversed in print. The formalized one-sided bounds use the corrected pairing, and the milestone text preserves the printed source for audit. The intermediate expressions involving $G(S_i(t))$ are excluded from the corrected statements because the framework does not assume customer-coordinate right continuity. Theorem 1(c) and (f) use both conditions and are true as printed. The scope includes the definitions, Lemmas 1–2, corrected parts (a)–(b), and parts (c) and (f). Contributions toward their proofs and reusable time-change lemmas are welcome. Glynn and Whitt (1989), p. 639, Theorem 1

Selected references

• P. W. Glynn and W. Whitt, Extensions of the Queueing Relations L = λW and H = λG, Operations Research 37(4):634–644, 1989. DOI: 10.1287/opre.37.4.634

Motivation

Shop scheduling asks how to sequence jobs that each need processing on several machines. In an open shop, a job's operations may be executed in any order, as in testing stations, repair bays, or classroom and examination timetables, where the order in which a candidate visits the stations is irrelevant. The objective studied here is the makespan $C_{\max}$, the time at which the last operation finishes.

The survey of Graham, Lawler, Lenstra and Rinnooy Kan (Ann. Discrete Math. 5, 1979) introduced the three-field notation $\alpha|\beta|\gamma$ that the scheduling literature still uses, and classified the complexity of the problems it names. For the open shop, its §5.2.1 presents a simplified exposition of the result of Gonzalez and Sahni (J. ACM 23, 1976): with two machines and no preemption, the obvious lower bound on the makespan is always achieved. The same page records that the three-machine case $O3\|C_{\max}$ is binary NP-hard, so two machines is exactly where the problem is easy.

Timeline. Gonzalez and Sahni (1976) gave the linear-time algorithm for $O2\|C_{\max}$, proved NP-hardness for $O3\|C_{\max}$, and gave a polynomial algorithm for the preemptive problem $O|pmtn|C_{\max}$. Graham et al. (1979, §5.2.1) gave the shorter construction formalized here, and observed (§5.2.2) that it implies preemption brings no advantage for $m = 2$. Lenstra (cited as forthcoming in the survey) showed $O2|r_j|C_{\max}$, $O2|tree|C_{\max}$ and $O\|C_{\max}$ unary NP-hard.

Setting

There are $n$ jobs $J_1, \dots, J_n$ and two machines $M_1$, $M_2$. Job $J_j$ has an operation on $M_1$ of length $a_j \ge 0$ and an operation on $M_2$ of length $b_j \ge 0$. There is no preemption, and every job is available at time $0$. A schedule assigns start times $s_1(j)$ and $s_2(j)$ to the two operations of $J_j$, which then occupy $[s_1(j), s_1(j)+a_j)$ on $M_1$ and $[s_2(j), s_2(j)+b_j)$ on $M_2$.

A schedule is feasible if

1. all start times are nonnegative;
2. each machine processes at most one job at a time: the intervals of distinct jobs on the same machine do not overlap;
3. each job is processed on at most one machine at a time: the two intervals of the same job do not overlap, in either order.

Write $T_1 = \sum_j a_j$ and $T_2 = \sum_j b_j$ for the two machine loads. The survey's construction uses the sets

$$A = \{J_j \mid a_j \ge b_j\}, \qquad B = \{J_j \mid a_j < b_j\},$$

two distinct jobs $J_r$, $J_l$ with $a_r \ge \max_{J_j \in A} b_j$ and $b_l \ge \max_{J_j \in B} a_j$, and $A' = A - \{J_r, J_l\}$, $B' = B - \{J_r, J_l\}$.

Formalization targets

Goal: the optimal makespan

$$C^*_{\max} = \max\Big\{T_1,\ T_2,\ \max_j\,(a_j + b_j)\Big\},$$

and the optimum is attained. Formally, for every $T \ge 0$: a feasible schedule completing every operation by $T$ exists if and only if $T_1 \le T$, $T_2 \le T$ and $a_j + b_j \le T$ for all $j$. The goal mentions neither $A$, $B$, $J_r$, $J_l$ nor the case analysis; those are the milestones.

Milestones (in the order of the argument)

1. Two distinct jobs $J_r$, $J_l$ with the required bounds exist when $n \ge 2$.
2. Fig. 5.1: the blocks $B' \cup \{J_l\}$ and $A' \cup \{J_r\}$, with $A'$ and $B'$ in arbitrary order, have feasible staircase schedules without idle time.
3. Fig. 5.2: if $T_1 - a_l \ge T_2 - b_r$, the blocks combine into a feasible schedule of all jobs ending by $T_1 + b_r$.
4. Case (1): if moreover $a_r \le T_2 - b_r$, some feasible schedule has length at most $\max\{T_1, T_2\}$.
5. Case (2): if moreover $a_r > T_2 - b_r$, some feasible schedule has length at most $\max\{T_1, a_r + b_r\}$.
6. The symmetric case $T_1 - a_l < T_2 - b_r$: some feasible schedule has length at most $\max\{T_1, T_2, a_l + b_l\}$.
7. The lower bound: every feasible schedule has $C_{\max} \ge \max\{T_1, T_2, \max_j(a_j + b_j)\}$.

Significance

The result. The theorem gives a closed form for the optimal makespan of a two-machine open shop, together with a linear-time construction of an optimal schedule. The survey uses it immediately: since the bound is also a lower bound for preemptive schedules, $O2|pmtn|C_{\max}$ is solved by the same schedules, so preemption gives no advantage on two machines (§5.2.2). It is the standard example of a shop problem whose trivial lower bound is tight, and the contrast with the binary NP-hard $O3\|C_{\max}$ marks the complexity boundary for nonpreemptive open shops.

Formalizing it. The result is classical and proved on paper; no machine-checked proof is known to exist on this platform. The mission produces a reusable model of nonpreemptive two-machine open-shop schedules with real processing times, a verified lower bound, and a verified constructive argument. Unlike many existence-of-schedule results, the survey's construction is explicit (orders and start times), so it can be formalized directly rather than through an abstract existence argument.

Difficulty

The lower bound is the easy half. The difficulty is the construction: a schedule must meet the bound simultaneously on both machines and for every job. The natural first idea, running every job on $M_1$ then $M_2$ in some order (a flow-shop schedule), fails: Johnson's rule then gives a makespan that can exceed $\max\{T_1, T_2, \max_j(a_j+b_j)\}$, because the open shop needs some job to visit $M_2$ first. The survey's construction moves exactly one job, $J_r$, to the front of $M_2$, and its correctness depends on the choice of $J_r$ and $J_l$ and on the case split on $T_1 - a_l$ versus $T_2 - b_r$. Figures 5.3 and 5.4 are drawn for $T_1 \ge T_2$; in the other subcases the start times shown in the figures need adjustment, and the formal statements of the cases assert lengths rather than the figures' exact start times.

Formalization scope

All declarations live in the namespace SchedSurvey.O2. Jobs are Fin n, 0-based ($J_j$ is index $j-1$). Processing times and start times are real numbers with $a_j, b_j \ge 0$; the survey's integer data are a special case, and every claim of §5.2.1 holds over the reals. A schedule is a pair of start-time functions s₁ s₂ : Fin n → ℝ. Interval non-overlap is s + p ≤ s' ∨ s' + p' ≤ s, so touching intervals are allowed and a zero-length operation occupies nothing. Feasibility (IsFeasible) contains both disjointness constraints of §2.1, the machine constraint and the job constraint, with the two operations of a job in either order. The job constraint is essential: without it the optimum would be $\max\{T_1, T_2\}$ and the goal false.

"Length at most $L$" is CompletesBy a b S L: every operation ends by $L$. Optimality is stated in threshold form, which avoids taking a supremum or infimum over a possibly empty set and is equivalent to "$C^*_{\max}$ equals the maximum and is attained". A maximum over $A$ or $B$ appears as a bound on every member, which is also correct for empty $A$ or $B$. The orders of $A'$ and $B'$ are duplicate-free lists whose members are exactly those sets; back-to-back start times are given by contigStart.

The milestone on the choice of $J_r$, $J_l$ assumes $n \ge 2$, which the page presupposes; the goal does not, and covers $n \le 1$ as well. The lower bound assumes $T \ge 0$, which matters only for $n = 0$.

A trivializing formalization is ruled out: feasibility includes both disjointness constraints and nonnegative start times, the threshold is quantified over all $T \ge 0$, and no constant is fixed.

Contributions welcome: proofs of the lower bound (a sum of disjoint intervals inside $[0, T]$), of the list-based block lemmas, of the case lemmas, and of the goal from them. The interval and back-to-back-schedule lemmas are reusable for other shop problems.

Selected references

• R.L. Graham, E.L. Lawler, J.K. Lenstra, A.H.G. Rinnooy Kan, Optimization and approximation in deterministic sequencing and scheduling: a survey, Annals of Discrete Mathematics 5 (1979) 287–326. https://doi.org/10.1016/S0167-5060(08)70356-X
• T. Gonzalez, S. Sahni, Open shop scheduling to minimize finish time, Journal of the ACM 23(4) (1976) 665–679. https://doi.org/10.1145/321978.321985
• S.M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1 (1954) 61–68. https://doi.org/10.1002/nav.3800010110

Motivation

A chance constraint limits the probability of violating a requirement rather than requiring that requirement to hold for every realization of uncertain data. Charnes and Cooper developed deterministic optimization problems for several ways of judging decisions under such constraints. Their P model gives a satisficing objective: increase the probability of reaching a specified aspiration level while meeting prescribed reliability levels for the resource constraints. The paper's concrete decision rule makes the decision vector depend linearly on the random right-hand side, and its P-model section moves from a fractional deterministic program to a convex one. The result explains how a risk-adjusted ratio can be optimized without retaining a fractional objective. The source is Charnes and Cooper, 1963, pp. 30–33, especially equations (35) and (38)–(39b).

The related linear-fractional change of variables was already being used for linear programs Charnes and Cooper, 1962; the present section applies it to constraints built from second moments rather than linear equations. That distinction matters because the normalized feasible set contains a boundary at zero scale, and because second-moment inequalities require their own convexity claim. The paper cites fractional programming results for its local-to-global assertion about (38); the mission focuses on its explicit transformed program (39). Charnes and Cooper, 1963, p. 32.

Setting

Let $m,n$ be positive integers and $(\Omega,P)$ a probability space. A fixed real $m\times n$ matrix $A$ has rows $a_i'$. Random vectors $b:\Omega\to\mathbb R^m$ and $c:\Omega\to\mathbb R^n$ give the right-hand side and objective coefficients. The paper restricts decisions to the linear decision rule $x=Db$, where the real $n\times m$ matrix $D$ is chosen before $b$ is realized. Write $\mu_b=E[b]$ and $\mu_c=E[c]$. A number $z_0$ is the given aspiration value. For each row $i$, its reliability level $\alpha_i$ is strictly between $1/2$ and $1$, and $K_i=\Phi^{-1}(\alpha_i)>0$ is the corresponding standard-normal quantile. These are the objects of equations (5), (19b), (21), and (27) in Charnes and Cooper, 1963.

The residual $a_i'Db-b_i$ has raw second moment $\sigma_i^2(D)=E[(a_i'Db-b_i)^2]$ and negative mean $\mu_i(D)=\mu_{b_i}-a_i'D\mu_b$. The aspiration error has raw second moment $V(D)=E[(c'Db-z_0)^2]$. These definitions come from equations (30) and (34). The expected linear objective appearing in the deterministic programs is $\mu_c'D\mu_b$; the model records the paper's assumption that the components of $b$ and $c$ are uncorrelated. Charnes and Cooper, 1963, pp. 26, 28, 30.

Program (38) chooses $(D,v,v_0,w_0)$ and maximizes $v_0/w_0$. Its inequalities bound the mean objective below by $z_0+v_0$, bound $w_0$ below by the root-mean-square aspiration error, and bound each nonnegative $v_i$ between the row's risk term and $\mu_i(D)$. The denominator satisfies $w_0>0$. Program (39) introduces a nonnegative scale $t$ and barred variables. It fixes $\bar w_0=1$ and maximizes the linear objective $\bar v_0$. The barred moments are calculated from $\bar D$ and $t$ by equation (39b), rather than declared to be scaled copies of the unbarred moments. Charnes and Cooper, 1963, pp. 32–33.

Formalization targets

Convex transformed program

Let $F_{39}$ contain every point satisfying all of (39), including $t=0$. The paper's convex-programming claim becomes

$$F_{39}\text{ is convex}.$$

The source states the claim after displaying the barred moments, in the paragraph following (39b). Charnes and Cooper, 1963, p. 33.

Equal optimal values

Let $F_{38}$ be the feasible set of (38). Provided $F_{38}$ is nonempty, the mission goal states that the normalized substitution sends each point of $F_{38}$ to a point of $F_{39}$ with the same objective, and that

$$\sup_{(D,v,v_0,w_0)\in F_{38}}\frac{v_0}{w_0} =\sup_{(\bar D,\bar v,\bar v_0,\bar w_0,t)\in F_{39}}\bar v_0.$$

The suprema may be infinite. The equality concerns the complete program (39), including $t=0$. Positive-scale points have an inverse substitution; zero-scale points are retained in the comparison. This is the precise optimal-value reading of the paper's statement that (38) can be replaced by one convex program. Charnes and Cooper, 1963, pp. 32–33.

Significance

The result places the P model alongside the paper's E and V models as an optimization problem with convex feasible constraints and a nonfractional objective. A solver of (39) can compare aspiration and resource reliability within the same matrix decision rule. Equality of suprema says the transformed model has the same best attainable value even when the best value is only approached, and even when points at $t=0$ occur in the transformed feasible set. The forward and inverse substitution statements identify how positive-scale solutions correspond. Charnes and Cooper, 1963, pp. 30–33.

The paper result is a published mathematical claim. The present formalization states its definitions and assertions in Lean; its theorem proofs are still open. The standard Gaussian CDF and its inverse are available as a separately published Prove2Me definition, while the model-specific second moments and feasible sets must be formalized for this mission. The previously published Derman linear-fractional lemma concerns a polyhedral linear program and does not assert this P-model result. Completing the mission would add reusable formal machinery for expected-square constraints, a normalized perspective program, and equality of optimal values at a scale boundary.

Difficulty

The pointwise substitution $t=1/w_0$ only reaches points of (39) with $t>0$, while (39) explicitly permits $t=0$. Therefore a bijection of feasible points at positive scale alone does not establish equality of the displayed suprema. The proof also has to reconcile the squared form of the row constraints with convexity: $\bar\sigma_i^2$ is a raw second moment and $\bar\mu_i^2$ is the square of its mean, so their difference is the variance term relevant to the risk bound. Taking the fourth inequality as a generic difference of quadratics would obscure that claim. The paper prints a conflicting square and sign in (38), which must be resolved against its earlier (29) and later (39). Charnes and Cooper, 1963, pp. 28, 32–33.

Formalization scope

Lean uses finite index types Fin m and Fin n, real matrices and scalars, a probability measure $P$, and Bochner integrals for the moments. Square integrability is stated for every component of $b$ and $c$ and every product $c_jb_k$; this keeps the expected squares meaningful. The paper assumes $b$ and $c$ are uncorrelated, so the same componentwise equalities are recorded. It also assumes that each row residual has a Gaussian law under a decision matrix; the Lean theorem retains this standing assumption even though the substitution from (38) to (39) is algebraic. The quantile $K_i$ is imported from the published Cohen2019.Robust.PhiInvReal, with $1/2<\alpha_i<1$ excluding its junk endpoint values. The theorem concerns (38) onward; it does not assert the paper's analogous reduction from the original probability model (35), because the text does not establish a distributional theorem for its random objective. Charnes and Cooper, 1963, pp. 26–27, 31–33.

The source phrase “replace ... by one convex programming problem” is made explicit as convexity of the (39) feasible set, feasibility and value preservation of the forward scaling, and equality of extended-real suprema. The normalization $\bar w_0=1$, strict $w_0>0$, and weak $t\ge0$ are separate conditions. The $t=0$ slice is included, and the main theorem assumes $F_{38}$ nonempty. The barred functions are genuine expectations of the homogenized expressions of (39b). The square-and-sign discrepancy in printed (38) is resolved in favor of the form printed in (29) and (39), consistent with the nearby statement that the row constraints are the same as before. These choices exclude a vacuous denominator, an artificially smaller transformed set, and a trivially defined scaling identity. Reusable contributions include moment lemmas, convexity results for expected-square constraints, and supremum comparison for normalized programs.

Selected references

• A. Charnes and W. W. Cooper, Deterministic Equivalents for Optimizing and Satisficing under Chance Constraints, Operations Research 11(1), 1963, pp. 18–39. DOI.
• A. Charnes and W. W. Cooper, Programming with Linear Fractional Functionals, Naval Research Logistics Quarterly 9(3–4), 1962, pp. 181–186. DOI.
• C. Derman, On Sequential Decisions and Markov Chains, Management Science 9(1), 1962, pp. 16–24. DOI.
• J. Cohen, E. Rosenfeld, and Z. Kolter, Certified Adversarial Robustness via Randomized Smoothing, ICML, 2019. arXiv.

Motivation

Open shops model production and service systems in which every job must visit every machine, but the order of the visits is free: a car that needs an inspection, a wash and a tyre change, a patient who needs several tests, a student who sits several exams. The survey of Graham, Lawler, Lenstra and Rinnooy Kan (Ann. Discrete Math. 5, 1979) fixed the three-field notation $\alpha|\beta|\gamma$ that the scheduling literature still uses, and classified the complexity of the problems it can express. Among the polynomially solvable cases, the preemptive open shop with makespan objective, $O|pmtn|C_{\max}$, is one of the few multi-machine problems whose optimal value has a closed form for any number of machines and jobs.

Timeline.

• 1976: Gonzalez and Sahni (J. ACM 23) prove that the optimal preemptive open-shop makespan is the largest machine load or job length, and give a polynomial algorithm. In the same paper they solve $O2\|C_{\max}$ in linear time and show $O3\|C_{\max}$ NP-hard.
• 1978: Lawler and Labetoulle (J. ACM 25) give a linear-programming treatment of preemptive scheduling on unrelated machines and reformulate the open-shop construction in terms of decrementing sets, found by an assignment problem through the Birkhoff–von Neumann theorem.
• 1979: the survey (§5.2.2, p. 313) presents this construction as the standard argument and records the $O(r+\min\{m^4,n^4,r^2\})$ bound of Gonzalez (1976), where $r$ is the number of nonzero processing times.

Setting

There are $m$ machines $M_1,\dots,M_m$ and $n$ jobs $J_1,\dots,J_n$. Job $J_j$ consists of operations $O_{1j},\dots,O_{mj}$; operation $O_{ij}$ must be processed on machine $M_i$ for $p_{ij}\ge 0$ time units. The processing-time matrix is $P=(p_{ij})$: its rows are machines and its columns are jobs. Every job is available at time $0$.

Preemption is allowed: an operation may be interrupted and resumed later. A schedule is a finite list of pieces $(i,j,s,e)$, each meaning that $M_i$ processes $J_j$ during $[s,e)$. A schedule is feasible if

1. every piece satisfies $0\le s\le e$;
2. each machine processes at most one job at a time, and each job is processed on at most one machine at a time: two pieces that share a machine or a job do not overlap;
3. for every pair $(i,j)$ the pieces of $O_{ij}$ have total length exactly $p_{ij}$.

The makespan $C_{\max}$ is the time at which the last piece ends, and $C^*_{\max}$ is its minimum over feasible schedules. The load of machine $M_i$ is the row sum $\sum_j p_{ij}$, the length of job $J_j$ is the column sum $\sum_i p_{ij}$, and

$$C=\max\Big\{\max_j \sum_i p_{ij},\ \max_i \sum_j p_{ij}\Big\}.$$

A row or column is tight if its sum equals $C$ and slack otherwise. A decrementing set is a set $S$ of strictly positive entries of $P$ with exactly one element in each tight row and each tight column and at most one in each slack row and each slack column.

Formalization targets

Goal: $C^*_{\max}=C$

For every $T\ge 0$,

$$\big(\exists \text{ feasible schedule with } C_{\max}\le T\big)\iff \Big(\sum_j p_{ij}\le T\ \forall i\ \text{ and }\ \sum_i p_{ij}\le T\ \forall j\Big).$$

This says that the optimal makespan is exactly the largest machine load or job length, and that it is attained.

Milestones (all from §5.2.2, p. 313)

1. Lower bound $C^*_{\max}\ge C$.
2. Existence of a decrementing set for every nonzero nonnegative $P$.
3. Positive step: for a decrementing set, the largest $\delta$ satisfying the constraints (1)–(3) of the survey exists and is positive.
4. Step property: after replacing each $p_{ij}\in S$ by $\max\{0,p_{ij}-\delta\}$, the largest line sum is exactly $C-\delta$.
5. Partial schedule: for each $p_{ij}\in S$, $M_i$ processes $J_j$ for $\min\{p_{ij},\delta\}$ time units, with no machine or job used twice.
6. Termination: every run of the procedure reaches $P'=(0)$ within a bounded number of stages.
7. Joining: the concatenated partial schedules form a feasible schedule with $C_{\max}\le C$.

Significance

The result. The theorem turns an optimization over continuous-time schedules into the computation of $m+n$ sums. It certifies optimality by a counting argument, it is the base case for preemptive open shops with release dates and due dates, and it is used elsewhere in the survey (§4.4.6) to reduce problems on unrelated machines with preemption to open-shop instances. Because a nonnegative matrix whose row and column sums are all equal is a multiple of a doubly stochastic matrix, the theorem is a scheduling form of the Birkhoff–von Neumann decomposition. It also underlies timetabling and edge-colouring results for bipartite multigraphs.

Formalizing it. The theorem has been proved since 1976 and is textbook material. No machine-checked proof is known to exist: Mathlib has the Birkhoff–von Neumann theorem for doubly stochastic matrices but no model of open-shop schedules. A formalization adds a reusable model of preemptive multi-machine schedules with both disjointness requirements, a checked proof of the decrementing-set construction, and a termination argument the survey asserts without proof.

Difficulty

The lower bound is a one-line counting argument. The difficulty is the construction of a schedule of length exactly $C$. Scheduling each machine's operations back to back gives length $\max_i\sum_j p_{ij}$, but may run one job on two machines at once. Scheduling job by job has the symmetric defect. A greedy list schedule that only respects both constraints can leave machines idle and overshoot $C$. The construction must keep every tight line busy at every moment while never letting a slack line fall behind. The existence of the decrementing set at each stage is the combinatorial core: it is a Hall-type matching condition, not a local choice. Termination is also not automatic, because a careless choice of step length can produce infinitely many shrinking steps.

Formalization scope

All objects live in the namespace SchedSurvey.OPmtn. Machines and jobs are Fin m and Fin n, both 0-based, and processing times and piece endpoints are real numbers; integer data are a special case. A schedule is a List of pieces. Feasibility requires nonnegative start times, disjointness for pieces sharing a machine or a job (touching intervals allowed), and exactly $p_{ij}$ units of processing for every pair $(i,j)$. Every theorem assumes $p_{ij}\ge 0$.

"$C$ is the maximum" is the predicate IsMaxLoad P C: all line sums are at most $C$ and one equals $C$. The goal is stated in threshold form and mentions no maximum at all. The display defining $C$ on p. 313 prints $\max_i\{\sum_i p_{ij}\}$ for the second term; the following sentence shows it means the row sums $\sum_j p_{ij}$, and the formalization uses those. The hypothesis $T\ge 0$ matters only for $P=0$, where the empty schedule finishes by every $T$.

A trivializing formalization is ruled out: the goal mentions neither decrementing sets nor $\delta$. Its "if" direction asserts that a schedule exists. Feasibility counts work per pair (machine, job), not per job, and forbids a job from running on two machines at once. Without either requirement the statement would be a different and easier theorem.

A complete development needs: list sums of interval lengths over disjoint intervals, the existence of decrementing sets (via Birkhoff–von Neumann, König's theorem or Hall's theorem on the bipartite graph of positive entries), the step and termination lemmas, and concatenation of schedules. The schedule model and the decrementing-set lemma are reusable for other preemptive shop problems. Contributions of alternative proofs of any milestone, for example a direct Hall-theorem proof of the existence of decrementing sets, are welcome.

Selected references

• R. L. Graham, E. L. Lawler, J. K. Lenstra, A. H. G. Rinnooy Kan, Optimization and approximation in deterministic sequencing and scheduling: a survey, Annals of Discrete Mathematics 5 (1979) 287–326. https://doi.org/10.1016/S0167-5060(08)70356-X
• T. Gonzalez, S. Sahni, Open shop scheduling to minimize finish time, Journal of the ACM 23 (1976) 665–679. https://doi.org/10.1145/321978.321985
• E. L. Lawler, J. Labetoulle, On preemptive scheduling of unrelated parallel processors by linear programming, Journal of the ACM 25 (1978) 612–619. https://doi.org/10.1145/322077.322090