Operations Research

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

A discrete-event simulation of a queue, an inventory system or a communication network produces an output process $Y = \{Y(t) : t \ge 0\}$, and the quantity of interest is usually its steady-state mean $\mu$, the long-run average of $Y$. The natural estimator is the time average $\bar Y_n(1) = \frac1n\int_0^n Y(s)\,ds$ of a run of length $n$. A confidence interval for $\mu$ needs the scale of the fluctuations of $\bar Y_n(1)$, the variance constant $\sigma^2$ of the central limit theorem $n^{1/2}(\bar Y_n(1) - \mu) \Rightarrow \sigma N(0,1)$. For correlated simulation output, $\sigma^2$ is a sum of autocovariances at all lags and is hard to estimate consistently.

The method of standardized time series (STS), introduced by Schruben (Schruben 1983), avoids estimating $\sigma$: it divides the centred time average by a functional of the whole observed path that scales like $\sigma$, so that $\sigma$ cancels. Batch means, the standardized sum, and the standardized maximum are all of this form.

Glynn and Iglehart (Glynn & Iglehart 1990) put the method on a general footing. They require only a functional central limit theorem (FCLT) for $Y$, and they identify an abstract class $\mathcal M$ of standardizing functionals for which the cancellation works. This mission formalizes their basic limit theorem, Theorem 2.4, and the four claims of its proof. Two companion results of §2, display (2.2) and the weak law $\bar Y_n(1) \Rightarrow \mu$, are included as further targets.

Setting

$C[0,1]$ is the space of continuous real functions on $[0,1]$ with the uniform norm and its Borel $\sigma$-algebra; $k \in C[0,1]$ is the identity path $k(t) = t$. For $g : C[0,1] \to \mathbb R$, $D(g)$ is the discontinuity set of $g$, the set of $x$ at which $g$ is not continuous. A standard Brownian motion $B$ on a probability space $(\Omega, \mathcal F, P)$ is a random element of $C[0,1]$ with Gaussian finite-dimensional laws, $B(0) = 0$ and $\operatorname{Cov}(B(s), B(t)) = \min(s,t)$.

The output $Y$ is a real-valued measurable process. Its scaled partial-integral process and its centred, rescaled version are

$$\bar Y_n(t) = \frac1n\int_0^{nt} Y(s)\,ds, \qquad X_n(t) = n^{1/2}\bigl(\bar Y_n(t) - \mu t\bigr), \qquad 0 \le t \le 1 .$$

Assumption (2.1) asks for finite constants $\mu$ and $\sigma > 0$ such that $X_n \Rightarrow \sigma B$ as $n \to \infty$, weak convergence of random elements of $C[0,1]$. It holds for $\phi$-mixing, strongly mixing, associated and regenerative output processes, among others.

The class $\mathcal M$ of (2.3) consists of the measurable $g : C[0,1] \to \mathbb R$ with

1. $g(\alpha x) = \alpha g(x)$ for $\alpha > 0$ (positive homogeneity);
2. $g(x - \beta k) = g(x)$ for $\beta \in \mathbb R$ (invariance under subtracting a linear drift);
3. $P\{g(B) > 0\} = 1$;
4. $P\{B \in D(g)\} = 0$.

The proof uses the auxiliary map $h(x) = x(1)/g(x)$ for $g(x) \ne 0$ and $h(x) = 0$ otherwise.

Formalization targets

Goal: Theorem 2.4

For every $g \in \mathcal M$, under Assumption (2.1),

$$\frac{\bar Y_n(1) - \mu}{g(\bar Y_n)} \Rightarrow \frac{B(1)}{g(B)} \qquad (n \to \infty). \tag{2.5}$$

Milestones: the four claims of the proof (p. 3)

1. $P\{\sigma B \in D(h)\} = 0$.
2. $h(X_n) \Rightarrow h(\sigma B)$.
3. $h(\sigma B) = B(1)/g(B)$, by (2.3i).
4. $h(X_n) = (\bar Y_n(1) - \mu)/g(\bar Y_n)$ for $n \ge 1$, by (2.3i) and (2.3ii).

Companions

$$n^{1/2}\bigl(\bar Y_n(1) - \mu\bigr) \Rightarrow \sigma B(1) \tag{2.2}$$

and $\bar Y_n(1) \Rightarrow \mu$.

Significance

Theorem 2.4 is the limit theorem behind every STS confidence interval. The limit $B(1)/g(B)$ is free of $\sigma$ and of the output process, so with $z$ chosen so that $P\{-z \le B(1)/g(B) \le z\}$ equals a prescribed level, the interval $\bar Y_n(1) \pm z\,g(\bar Y_n)$ has asymptotically exact coverage for $\mu$. Each choice of $g \in \mathcal M$ gives a method: batch means with a fixed number of batches, Schruben's standardized sum, the standardized maximum. The later sections of the paper compare the lengths of these intervals with those of consistent-estimation intervals, and those comparisons start from Theorem 2.4.

The theorem is classical and its proof is short on paper. What is missing is a machine-checked version. The formal proof needs a continuous mapping theorem for maps that are continuous only almost surely at the limit, on the non-locally-compact space $C[0,1]$; Mathlib has the version for continuous maps only. A formal Theorem 2.4 also makes the class $\mathcal M$ and the C[0,1]-valued FCLT available for the other results of the paper, the expected-length lower bound and its non-attainment, which are formalized in sibling missions.

Difficulty

The algebra (milestones 3 and 4) is elementary. The difficulty is the continuous-mapping step. The map $h$ is in general not continuous: it can be discontinuous wherever $g$ is and wherever $g$ vanishes, and $g$ itself may be discontinuous on a large set (the standardized maximum is). The continuous mapping theorem for continuous maps does not apply. One needs its almost-sure form: if $X_n \Rightarrow X$ and $P\{X \in D(h)\} = 0$, then $h(X_n) \Rightarrow h(X)$. The class $\mathcal M$ controls $D(g)$ only along the law of $B$, and the hypothesis of the almost-sure theorem is about $D(h)$ at the scaled limit $\sigma B$, so the conditions (2.3iii) and (2.3iv) have to be transported from $B$ to $\sigma B$ and from $g$ to $h$.

Formalization scope

$C[0,1]$ is C(unitInterval, ℝ) with its sup-norm topology; the Borel MeasurableSpace instance is declared in the mission's definition file, since Mathlib has none at this commit. Weak convergence is Mathlib's TendstoInDistribution, for the $C[0,1]$-valued FCLT and for the real-valued conclusions. The standard Brownian motion is a measurable $C[0,1]$-valued map whose coordinates agree, for every $\omega$, with a process satisfying Mathlib's IsBrownianReal. $D(g)$ is the set of points where ContinuousAt g fails, and $P\{B \in D(g)\}$ is an outer measure, so no measurability of $D(g)$ is assumed.

$\bar Y_n$ is a $C[0,1]$-valued parameter pinned pointwise by $\bar Y_n(t) = \frac1n\int_0^{nt}Y(s)\,ds$, so it is determined by $Y$. Assumption (2.1) carries joint measurability of $Y$ and local integrability of each path; the second is implicit in the paper and makes $\bar Y_n$ defined. The index $n$ runs over $\mathbb N$, and milestone 4 assumes $n \ge 1$ because (2.3i) is applied with $\alpha = n^{1/2}$. Real division by zero returns $0$ in Lean, which agrees with the paper's convention for $h$; it matters only on events of probability zero in the limit. Condition (2.3iii) is printed "$P\{g(b) > 0\} = 1$" and is read as $P\{g(B) > 0\} = 1$.

Condition (2.3iv) is stated with the discontinuity set, not as continuity of $g$: requiring $g$ continuous everywhere would exclude the standardized maximum of Example 3.10 and would make the continuous-mapping step trivial. The goal assumes nothing about $h$, $D(h)$ or any mapping theorem; these appear only in the milestones.

Contributions welcome: the almost-sure continuous mapping theorem for TendstoInDistribution on a metric space (reusable well beyond this mission), the cone property of $D(g)$ under positive homogeneity, and evaluation at a point as a continuous map on $C[0,1]$. Mathlib does not yet construct a Brownian motion with continuous paths as a $C[0,1]$-valued random element, so the hypotheses cannot be instantiated inside Lean; this is a hypothesis on $B$, not a vacuity.

Selected references

• P. W. Glynn and D. L. Iglehart, Simulation output analysis using standardized time series, Mathematics of Operations Research 15(1):1–16, 1990. https://doi.org/10.1287/moor.15.1.1
• L. Schruben, Confidence interval estimation using standardized time series, Operations Research 31(6):1090–1108, 1983. https://doi.org/10.1287/opre.31.6.1090
• P. Billingsley, Convergence of Probability Measures, Wiley, 1968 (Theorem 5.1, the continuous mapping theorem).
• K. L. Chung, A Course in Probability Theory, 2nd ed., Academic Press, 1974 (p. 93, converging-together lemma).

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

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

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

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

Alternating-offer bargaining asks how an agreement is selected when two people can keep making proposals until one accepts. A prediction based only on behavior at the start may rely on threats that would no longer be sensible after a rejection. Ariel Rubinstein's 1982 paper studies strategies after every possible sequence of offers and gives a characterization of the partitions compatible with perfect equilibrium. Its setting has a unit pie, complete information, no fixed last round, and preferences that may describe more than a particular discount formula.

The question matters for sequential bargaining models in which the order of moves and the cost of delay affect the agreement. The paper distinguishes the set obtained when player 1 offers first from the set obtained when player 2 offers first. It also provides applications to fixed bargaining costs and fixed discount factors. This mission targets the paper's general characterization, from which those examples can be studied without building a new equilibrium concept for each preference family.

Setting

A partition is a number $s\in S=[0,1]$: player 1 receives $s$ of the unit pie and player 2 receives $1-s$. An outcome $(s,t)$ means that the offer $s$ is accepted in period $t$; $(0,\infty)$ denotes perpetual disagreement. Periods of actual play start at 1. The paper also uses $(s,0)$ when comparing acceptance of a current offer with a future outcome. Each player $i\in\{1,2\}$ has a complete, reflexive, transitive preference relation $\succcurlyeq_i$ on outcomes. Strict preference $\succ_i$ and indifference $\sim_i$ are derived from it.

The game alternates proposals and responses. One player offers a partition, the other accepts or rejects, and rejection makes the responder the next proposer. A strategy specifies what a player does after every possible history, including histories inconsistent with the player's earlier plans. A perfect equilibrium requires the relevant player's continuation to withstand every alternative continuation strategy at each rejected history and to make a planned acceptance or rejection consistent with the current offer. The empty history is included, so the opening proposer must also have no profitable deviation.

Write $A$ for the set of player-1 shares reached by perfect equilibria when player 1 opens, and $B$ for the corresponding set when player 2 opens. Perpetual disagreement contributes no share to either set. Define $\Delta\subseteq S\times S$ by a pair of one-period thresholds: for $(x,y)\in\Delta$, $y$ is the smallest share whose immediate acceptance player 1 weakly prefers to $(x,1)$, and $x$ is the largest share whose immediate acceptance player 2 weakly prefers to $(y,1)$. Let $\Delta_1$ and $\Delta_2$ be its coordinate projections. All four sets contain numbers interpreted as player-1 shares, even when player 2 moves first. These are the objects of Sections 2–5.

Formalization targets

Characterization

Under the paper's five preference assumptions (A-1)–(A-5), the goal is its THEOREM on p. 106:

$$A=\Delta_1\ne\varnothing,\qquad B=\Delta_2\ne\varnothing,$$

with $A$ and $B$ nonempty closed intervals and some $e\ge 0$ satisfying

$$B=\{a-e:a\in A\}.$$

The translation parameter is allowed to be zero, and either interval may be a single point. The goal fixes the paper's general shape without choosing a particular utility representation or assuming immediate agreement in every equilibrium.

Milestone statements

The attack path follows Lemmas 1–4 and Propositions 1–4 in their printed order. The lemmas constrain how a partition in one opening order relates to a feasible continuation in the other. Proposition 1 places each pair in $\Delta$ inside $A\times B$; Proposition 2 asserts existence; Proposition 3 describes $\Delta$ as a closed segment parallel to the diagonal; Proposition 4 gives the reverse containment of $A$ and $B$ in the threshold projections. Each numbered result is a separate theorem target.

Significance

The theorem identifies the full set of equilibrium partitions from preference comparisons one period apart. Nonemptiness says the model admits at least one equilibrium partition in either opening order. The interval conclusion describes cases with multiple equilibrium shares, while the translate relation states exactly how reversing the first mover changes the two sets. In the paper's discounting example, a single share is selected under the stated parameter conditions; in a fixed-cost boundary case, multiple shares can occur. These are applications in Section 6, not assumptions of the general target.

Rubinstein proved the result in 1982. Here the definitions and theorem statements are Lean drafts; the numbered targets and the main theorem still require machine-checked proofs. A local verification module establishes that one discounting instance satisfies the first three axioms and that the paper's Section 3 strategy example accepts its first offer in period 1. Completing the mission would give a reusable formal account of an infinite-horizon alternating-offer game and its subgame equilibrium conditions, alongside the paper's characterization.

Difficulty

A first-round equilibrium condition does not control what a strategy promises after an offer is rejected. The paper's equilibrium definition checks the entire continuation at every history, with the player's role changing after each rejection. As a result, showing that a proposed share is an equilibrium partition requires more than checking the opening offer: the answer and the next proposal must remain consistent throughout the game tree. The model also allows arbitrary complete preferences satisfying axioms, so a calculation with one discount function cannot establish the general theorem.

The boundary at a zero share requires care. Assumption (A-2) asserts strict preference for earlier positive shares; it says nothing directly about a player receiving zero. The printed proof of Lemma 1 invokes it for a comparison that can occur at that boundary. The local lemma drafts explicitly carry the paper's (A-4) closedness axiom to support that comparison. This added assumption, and its propagation to Lemmas 2–4, is disclosed in the audit notes rather than silently attributed to the Section 4 statement.

Formalization scope

Lean represents $S$ as the subtype of real numbers in $[0,1]$. Outcomes are an option type: an agreement contains a partition and a natural-number period, while none is perpetual disagreement. This prevents an endless play from acquiring a default last partition. Strategies are unrestricted functions of lists of past offers. The play uses the first accepted offer, with period number one greater than its zero-based sequence index. A subgame after a rejected history restarts the period count and swaps the opening role when the history has odd length. The perfect-equilibrium predicate includes the empty history; acceptance comparisons use period 0 for the offer already on the table.

The threshold correspondence uses actual least and greatest elements among partitions in $S$. No real infimum or supremum supplies a default for an empty candidate set. “Closed interval” in the goal means an explicit $[\ell,u]$ with $\ell\le u$. “$A-e$” is the image of $A$ under $a\mapsto a-e$. Proposition 3's “parallel line segment” is the full image of a nonempty interval under $x\mapsto(x,x-e)$. These readings exclude a vacuous equilibrium set, a disagreement-to-zero coercion, and a hard-coded discounting special case.

The common outcome and preference definitions, the history-based strategy and play, and the equilibrium predicate are reusable for other alternating-offer questions. Contributions toward their structural properties, the numbered milestones, and the full theorem are in scope. The two displayed claims inside proofs and the fixed-cost and discounting conclusions are deferred to keep this proposal on the theorem's numbered path. Existing platform entries on Nash's axiomatic bargaining solution and a sealed-offer double auction concern different objects; neither supplies this game's equilibrium definition.

Selected references

• Ariel Rubinstein, Perfect Equilibrium in a Bargaining Model, Econometrica 50(1), 97–109, 1982. DOI 10.2307/1912531.

Motivation

A Markov decision process is the standard model of sequential decision making under uncertainty: a controller observes the state of a finite system, chooses a decision, pays a cost, and the system moves to a random next state. In many applications (maintenance, inventory with unreliable records, robotics, medical treatment) the controller does not see the state itself, only partial information about it. This is the partially observed problem, and the usual way to solve it is to replace the state by the conditional distribution of the state given the observations (Åström 1965; Bertsekas). That reformulation has an infinite state space, and Smallwood and Sondik (1973) showed that the finite-horizon cost-to-go is nevertheless piecewise linear, but with a number of pieces that may grow exponentially with the horizon.

Papadimitriou and Tsitsiklis (Math. Oper. Res. 12(3), 1987) asked whether this blow-up is an artefact of the reformulation or intrinsic to the problem. Their Theorem 6 answers it: deciding whether a partially observed process can achieve a given expected cost is PSPACE-hard, already for stationary processes and horizons shorter than the number of states. This mission formalizes the reduction behind that theorem.

Setting

A partially observed stationary Markov decision process has a finite state set $S$, a partition $\Pi$ of $S$, and an initial state $s_0$. For a state $s$ write $z(s) \in \Pi$ for the set containing it. Each set $z$ carries a nonempty finite set $D_z$ of decisions; decision $i \in D_z$ costs $c(z, i)$ and moves a current state $s \in z$ to the next state $s'$ with probability $p(s, s', i)$. The controller sees only the sequence of sets visited, so a policy $\pi$ maps each observation sequence $z_0, \dots, z_t$ to a decision in $D_{z_t}$. For a horizon $T$, the expected cost of $\pi$ is

$$J_\pi(T) = \mathbb{E}_\pi\Bigl[\sum_{t=0}^{T} c\bigl(z(s_t), \pi(z(s_0), \dots, z(s_t))\bigr)\Bigr],$$

and the optimal cost is $\inf_\pi J_\pi(T)$.

A quantified Boolean formula is $Q_1 x_1 \cdots Q_n x_n\, F(x_1, \dots, x_n)$ with each $Q_j \in \{\exists, \forall\}$ and $F$ a conjunction of $m$ clauses $C_1, \dots, C_m$, each a set of literals $x_j$ or $\neg x_j$. It is true if there is a value of $x_1$ such that for all values of $x_2$, and so on, $F$ comes out true. Deciding truth (QSAT) is PSPACE-complete (Stockmeyer and Meyer 1973).

From a formula with $m \ge 1$ clauses the paper builds a process $M_\varphi$: an initial state, six states $A_{ij}, A'_{ij}, T_{ij}, T'_{ij}, F_{ij}, F'_{ij}$ per clause $i$ and variable $j$, end states $A_{i,n+1}, A'_{i,n+1}$, and one absorbing state, so $|S| = 6mn + 2m + 2$. The first transition chooses a clause uniformly; primed states record that the chosen clause is not yet satisfied; existential variables are set by decisions and universal ones by fair coins; the only nonzero cost, $1$, is paid at $A'_{i,n+1}$. The horizon is $T = 2n + 2$.

Formalization targets

Goal: the reduction is correct

For every formula $\varphi$ in the paper's QSAT class (an alternating prefix beginning with $\exists x_1$ and ending with $\forall x_n$, and three literals per clause), with $m \ge 1$ clauses and $T = 2n+2$,

$$T < |S|, \qquad \bigl(\exists \pi:\ J_\pi(T) = 0\bigr) \iff \varphi \text{ is true}, \qquad \inf_\pi J_\pi(T) \le 0 \iff \varphi \text{ is true}.$$

The goal states all three claims the paper makes: the horizon bound (p. 448), the existence of a zero-cost policy (p. 449), and the bound on the optimum (p. 448).

Milestones

1. The cost splits over the clause chosen at time 1: each clause is chosen with probability $1/m$, and a policy has zero expected cost iff it has zero cost for every choice of clause.
2. If a trajectory of positive probability ends in $A'_{i,n+1}$, the expected cost is at least $2^{-n}/m$.
3. A zero-cost policy makes the formula true.
4. A true formula yields a zero-cost policy.

Significance

Theorem 6 locates the partially observed finite-horizon problem in the complexity landscape: unless P = PSPACE there is no polynomial-time algorithm for it, even for stationary processes with short horizons. The paper's Corollary 1 strengthens this into evidence that no polynomial-size precomputed controller exists either. Together these results explain why exact algorithms for partially observed processes are exponential and motivated the later work on approximation and on restricted policy classes.

The formalization adds a machine-checked proof of the correctness of the reduction, the step on which the hardness claim rests, together with a reusable definition of a finite partially observed process with observation-history policies and of quantified Boolean formulas. The paper's argument is a short paragraph; a formal proof has to make precise how a policy that only sees observation sequences determines a strategy for the existential player. As far as we know, no machine-checked proof of this reduction exists.

Difficulty

The "if" direction is a direct translation of a winning strategy into a policy. The "only if" direction is where the work is. A zero-cost policy acts on observation sequences, and the paper argues that it never learns which clause was chosen. Under the paper's own partition this is not literally true: the sets $T_j$ and $T'_j$ differ, so the observations reveal whether the chosen clause was already satisfied. The existential strategy must therefore be extracted from the policy's behaviour on the observation histories in which the clause is still unsatisfied, and one must check that it is a single strategy, independent of the clause, that satisfies every clause against every choice of the universal variables. The bound of milestone 2 also requires tracking the probability of a single trajectory through the coin flips.

Formalization scope

The process is a Lean structure POMDP S Z with an observation map obs : S → Z encoding the partition, nonempty finite decision types D z, real costs c z i, and next-state laws given as Mathlib PMFs, so every transition row is a probability vector. A policy is a function List Z → (z : Z) → D z of the earlier observations and the current one. The expected cost is a finite sum over trajectories $x_0, \dots, x_T$ of their probability times $\sum_{t=0}^{T} c$, and the optimum is the infimum over all policies. Paper clause $C_i$ and variable $x_j$ are Lean indices $i - 1$ and $j - 1$.

Choices made explicit:

• Horizon. The paper prints $T = 2m + 2$ but says it is "just enough time for the process to reach one of $A_{i,n+1}$ or $A'_{i,n+1}$", which happens at time $2n+1$. With the printed value and $m < n$ the cost is never paid and every formula would map to a zero-cost process. We use $T = 2n+2$.
• The set $A_j$. The partition sentence puts all $A_{ij}$ and $A'_{ij}$ in one set $A_j$; the decision sentence mentions "the set $A'_j$". We follow the partition sentence.
• The new state reached from $A_{i,n+1}$ and $A'_{i,n+1}$ is unspecified; it gets its own set, one zero-cost decision and a self-loop.
• Formulas. The general QBF definition allows any quantifier prefix and clause width. Every theorem assumes IsPaperQSAT, which requires the paper's alternating prefix $\exists x_1 \forall x_2 \cdots \forall x_n$ with $n>0$ even and three literals per clause. Clauses are sets of literals; three witnesses allow repetitions. $m \ge 1$ is also a hypothesis.
• Decisions are nonempty; rows are probability vectors.

Policies see only observation sequences. A formalization in which the policy reads the state would make the "only if" direction false and the reduction meaningless; one in which it sees only the current observation would make the "if" direction false. Neither is admissible.

Not formalized: PSPACE-hardness itself (Mathlib has no PSPACE or polynomial-time reductions), the polynomial-time computability of the construction, the membership of the problem in PSPACE (sketched on p. 449), Corollary 1 (a $\Sigma_2^p$ collapse) and Corollary 2 (NP-completeness of the unobserved case, stated without proof).

The definitions of partially observed processes and quantified Boolean formulas are reusable. Contributions of lemmas on trajectory sums (marginalising later coordinates, the probability of a fixed prefix) are welcome; they also serve the other missions of this series.

Selected references

• C. H. Papadimitriou and J. N. Tsitsiklis, The Complexity of Markov Decision Processes, Mathematics of Operations Research 12(3), 1987, 441–450. https://doi.org/10.1287/moor.12.3.441
• L. J. Stockmeyer and A. R. Meyer, Word problems requiring exponential time, Proc. 5th ACM STOC, 1973, 1–9. https://doi.org/10.1145/800125.804029
• R. D. Smallwood and E. J. Sondik, The optimal control of partially observable Markov processes over a finite horizon, Operations Research 21(5), 1973, 1071–1088. https://doi.org/10.1287/opre.21.5.1071
• K. J. Åström, Optimal control of Markov processes with incomplete state information, Journal of Mathematical Analysis and Applications 10, 1965, 174–205. https://doi.org/10.1016/0022-247X(65)90154-X
• D. P. Bertsekas, Dynamic Programming: Deterministic and Stochastic Models, Prentice-Hall, 1987.