Operations Research

Motivation

A single machine must process $n$ jobs that arrive over time. Job $j$ is released at time $r_j$, needs $p_j$ units of uninterrupted processing, and has weight $w_j > 0$; the goal is to minimize the total weighted completion time $\sum_j w_j C_j$. Offline, with all release dates equal to zero, Smith's rule (sequence by nondecreasing $p_j/w_j$) is optimal (Smith 1956); with arbitrary release dates the problem $1\,|\,r_j\,|\,\sum w_j C_j$ is strongly NP-hard (Lenstra, Rinnooy Kan and Brucker 1977).

In the online version the scheduler learns of job $j$ only at time $r_j$, and at each moment must either start a released job or keep the machine idle. Its quality is measured by its competitive ratio: the worst case, over all instances, of the ratio between the online schedule's cost and the offline optimum. Release-date scheduling is one of the basic test cases of online optimization.

Timeline:

• 1996. Hoogeveen and Vestjens show that no online algorithm has competitive ratio below 2, even with equal weights, and give the 2-competitive algorithm Delayed SPT for equal weights.
• 1997. Hall, Schulz, Shmoys and Wein give a $(3+\varepsilon)$-competitive algorithm for arbitrary weights, based on geometric intervals and linear programming.
• 1998. Phillips, Stein and Wein give another 2-competitive algorithm for equal weights, which does not extend to arbitrary weights.
• 2002. Goemans, Queyranne, Schulz, Skutella and Wang obtain a $(1+\sqrt2)$-competitive deterministic algorithm from an LP relaxation.
• 2004. Anderson and Potts show that Delayed SWPT has competitive ratio exactly 2 for arbitrary positive weights, matching the lower bound.

Setting

An instance has jobs $j \in J = \{1,\dots,n\}$ with integer release dates $r_j \ge 0$, integer processing times $p_j \ge 1$ and real weights $w_j > 0$. A schedule assigns each job an integer start time $S_j$. It is feasible if $S_j \ge r_j$ for every $j$ and no two intervals $[S_j, S_j + p_j)$ overlap; idle time is allowed. Its cost is $C(S) = \sum_j w_j (S_j + p_j)$.

Delayed SWPT runs over unit time slots $[t, t+1)$. When the machine is available at time $t$, it looks at the jobs released by $t$ and not yet started, and selects one with the smallest ratio $p_j/w_j$. Ties go to the smaller $p_j$, then to the smaller index. If $p_j \le t$, it starts $j$ at $t$ and the machine is busy until $t + p_j$. Otherwise the machine stays idle and the rule is applied again at $t+1$. The resulting schedule is written $\pi$, or dswpt I in Lean. In particular no job starts before time $p_j$.

The proof uses three auxiliary problems:

• the doubled problem (2P), with data $(2r_j, 2p_j, w_j)$;
• the extended problem (E), with release dates $r'_j = \max\{p_j, f(r_j)\}$, where $f(t)$ is the first time at or after $t$ at which $\pi$ leaves the machine free;
• one unit-length gap job $g_t$ for each slot $[t,t+1)$ in which Delayed SWPT idles although a job $j$ is available. The gap job has release date $f(r_j)$ and weight $w_j/p_j$.

The schedule $\pi_E$ of (E) runs the original jobs as in $\pi$ and each $g_t$ in $[t,t+1)$.

Formalization targets

Goal: Theorem 8

$$\min\Bigl\{\rho \;:\; \sum_j w_j C_j(\pi) \le \rho \sum_j w_j C_j(S)\ \text{for every instance and every feasible schedule } S\Bigr\} = 2.$$

Lean: IsLeast {ρ | ∀ n I S, IsFeasible I.r I.p S → cost I.w I.p (dswpt I) ≤ ρ * cost I.w I.p S} 2. Both halves are required: the upper bound $2$ and the fact that no smaller constant is valid for this algorithm.

Milestones

1. $\pi_j \ge p_j$ for every job (§2) and $r'_j \le \max\{2r_j, p_j\}$ (§3.2).
2. $\pi_E$ is feasible for (E) (§3.2).
3. Lemma 1. If $\pi^*$ and $\mu^*$ are optimal for (P) and (2P), then $C(\mu^*) = 2\,C(\pi^*)$.
4. Lemma 2. $\pi_E$ is optimal for (E).
5. Lemma 3. If $\mu^*$ is optimal for (2P) and a feasible $\sigma_E$ for (E) satisfies

$$\sum_{j\in J} w_j C_j(\sigma_E) + \sum_{g\in G} w_g C_g(\sigma_E) \le \sum_{j\in J} w_j C_j(\mu^*) + \sum_{g\in G} w_g C_g(\pi_E), \tag{1}$$

then $C(\pi) \le 2\,C(S)$ for every feasible $S$. 6. Inequality (1) holds for some feasible $\sigma_E$, for every optimal $\mu^*$ of (2P) (§§3.4–3.6).

Significance

The theorem shows that a deterministic online algorithm can match the lower bound of Hoogeveen and Vestjens for arbitrary positive weights. This settles the best competitive ratio for deterministic online algorithms for $1\,|\,r_j\,|\,\sum w_j C_j$. The algorithm needs no linear program. The analysis also does not compare the algorithm with a lower bound on the optimum. Instead it shows that the online schedule is optimal for a modified problem (E), and it converts an optimal schedule of (2P) into a schedule of (E).

The result was proved on paper in 2004. Neither Mathlib nor the Prove2Me catalog contains a machine-checked proof of it, or of any competitive ratio for online scheduling with release dates. This mission provides several reusable pieces:

• an executable, verified-terminating definition of an online scheduling rule;
• the doubling lemma for release-date problems;
• the optimality criterion behind Lemma 2;
• the block-by-block exchange argument of §§3.3–3.6.

Difficulty

The obvious argument fails at Lemma 2. Delayed SWPT is far from optimal for (P) itself, and its idle time is unbounded in relative terms. The proof therefore has to show that the inserted gap jobs make every idle slot "justified", so that a preemptive best-available argument becomes valid for (E). That argument rests on an optimality criterion of Belouadah, Posner and Potts (1992), which is not in Mathlib.

The second difficulty is inequality (1). Once $\mu^*$ is doubled and the gap jobs are inserted, nongap jobs must be shifted, and the gain of each gap-generating job must be charged against the delay of the gap jobs in its block. That accounting (Lemmas 4–7 of the paper) is an induction over blocks with signed differences of completion times.

The natural first idea, plain online SWPT (start the available job with the smallest $p_j/w_j$ whenever the machine is free), has no finite competitive ratio (Example 1 of the paper), so the delay $\pi_j \ge p_j$ is essential to the bound and must be tracked through the whole argument.

Formalization scope

Conventions committed to in Lean:

• Data. Jobs are Fin n (0-based, so "smallest index" is the order of Fin n). Times are natural numbers, the paper's standing integer-data assumption (p. 688), and weights are real. Every instance carries $p_j \ge 1$ and $w_j > 0$.
• Schedules and optimality. Schedules are integer start times. Feasibility, cost and optimality are defined for any finite job type, so (E), with job type Fin n ⊕ gapTimes I, uses the same notions. "Optimal" means optimal among all feasible nonpreemptive schedules with integer start times.
• The algorithm. Delayed SWPT is a def: a unit-time simulation that compares ratios by cross-multiplication and re-applies the rule at every slot. It runs to the horizon $\sum_j (r_j + 2p_j) + 1$. A sorry-free check (not uploaded) shows that every job has started by then, and that the simulation reproduces Examples 3 and 4 of the paper, including the gap times $0,2,3,4,5,6$ of Table 2.
• Completion times. In (2P) the completion time is $\mu^*_j + 2p_j$, and gap jobs have unit length.

The goal quantifies over every feasible schedule of every instance. It cannot be met by restricting the competitor to schedules without idle time or to list schedules, by dropping release-date feasibility, or by leaving jobs unscheduled.

Out of scope:

• The general lower bound "no online algorithm beats 2" (Example 2 of the paper, due to Hoogeveen and Vestjens) is not part of the mission. The lower half of the goal concerns Delayed SWPT only.
• The Belouadah–Posner–Potts optimality criterion is an external ingredient of Lemma 2. Solvers may formalize it as a supporting theorem.

Infrastructure that a complete development needs:

• simulation invariants for the algorithm;
• exchange and left-shift arguments for single-machine schedules;
• the job-splitting relaxation behind the best-available criterion.

The schedule vocabulary and the criterion are reusable for other release-date scheduling results. Contributions toward the block lemmas of §§3.3–3.6 (Lemmas 4–7, the bound (9)) are welcome as supporting theorems.

Selected references

• E. J. Anderson and C. N. Potts, Online Scheduling of a Single Machine to Minimize Total Weighted Completion Time, Mathematics of Operations Research 29(3), 686–697, 2004. https://doi.org/10.1287/moor.1040.0092
• J. A. Hoogeveen and A. P. A. Vestjens, Optimal On-Line Algorithms for Single-Machine Scheduling, IPCO 1996, LNCS 1084, 404–414. https://doi.org/10.1007/3-540-61310-2_30
• L. A. Hall, A. S. Schulz, D. B. Shmoys and J. Wein, Scheduling to Minimize Average Completion Time: Off-line and On-line Approximation Algorithms, Mathematics of Operations Research 22(3), 513–544, 1997. https://doi.org/10.1287/moor.22.3.513
• C. Phillips, C. Stein and J. Wein, Minimizing Average Completion Time in the Presence of Release Dates, Mathematical Programming 82, 199–223, 1998. https://doi.org/10.1007/BF01585872
• M. X. Goemans, M. Queyranne, A. S. Schulz, M. Skutella and Y. Wang, Single Machine Scheduling with Release Dates, SIAM Journal on Discrete Mathematics 15(2), 165–192, 2002. https://doi.org/10.1137/S089548019936223X
• H. Belouadah, M. E. Posner and C. N. Potts, Scheduling with Release Dates on a Single Machine to Minimize Total Weighted Completion Time, Discrete Applied Mathematics 36(3), 213–231, 1992. https://doi.org/10.1016/0166-218X(92)90255-9
• J. K. Lenstra, A. H. G. Rinnooy Kan and P. Brucker, Complexity of Machine Scheduling Problems, Annals of Discrete Mathematics 1, 343–362, 1977. https://doi.org/10.1016/S0167-5060(08)70743-X
• W. E. Smith, Various Optimizers for Single-Stage Production, Naval Research Logistics Quarterly 3, 59–66, 1956. https://doi.org/10.1002/nav.3800030106

Motivation

Electricity demand response asks consumers to lower their consumption during price events, when generation is expensive or scarce. Field trials such as the Low Carbon London experiment showed that consumers do react to price signals, but that the reaction is erratic: the average consumption falls while its variability stays high, and a producer that has to follow the load curve in real time pays for that variability. Aïd, Possamaï and Touzi (arXiv:1810.09063; Math. Oper. Res. 2022, doi:10.1287/moor.2021.1201) model this as a continuous-time principal–agent problem in which the consumer (the agent) controls both the level and the volatility of consumption, and the producer (the principal) designs a payment that rewards both.

The paper compares two benchmarks. In the second best, the producer observes only the consumption path and the consumer responds optimally to the contract; this is the subject of the companion mission of this series. In the first best, the producer dictates both the contract and the consumer's effort, subject only to the consumer's participation. The first best is the reference point against which the cost of moral hazard, the information rent, is measured. This mission formalizes the first-best value in closed form, Proposition 3.1 (i) of the paper.

The methodology follows the continuous-time principal–agent literature: Holmström and Milgrom (1987) for exponential utilities and linear contracts, Sannikov (2008) for the dynamic-programming view of the agent's continuation value, and Cvitanić, Possamaï and Touzi (2018) for contracts indexed on both the output and its quadratic variation.

Setting

Fix integers $N,d\ge0$ (usages for the mean effort and for the volatility effort), cost parameters $\mu\in(0,\infty)^N$, $\lambda\in(0,\infty)^d$, nominal volatilities $\sigma\in(0,\infty)^d$, effort bounds $A_{\max}>0$ and $0<\varepsilon\le1$, risk aversions $r,p>0$, a marginal volatility cost $h>0$, slopes $\kappa,\theta\in\mathbb R$, a horizon $T>0$, an initial consumption $X_0\in\mathbb R$ and a reservation utility $R_0<0$.

The consumer chooses a mean effort $\alpha$ with values in $A=\prod_i[0,\mu_iA_{\max}]$ and a responsiveness effort $\beta$ with values in $B=[\varepsilon,1]^d$, at cost

$$c(\alpha,\beta)=c_1(\alpha)+\tfrac12c_2(\beta),\qquad c_1(a)=\tfrac12\sum_i\frac{a_i^2}{\mu_i},\qquad c_2(b)=\sum_j\frac{\sigma_j^2}{\lambda_j}\big(b_j^{-1}-1\big).$$

The consumption $X$ follows $X_t=X_0-\int_0^t\alpha_s\cdot\mathbf 1\,ds+\int_0^t\sigma(\beta_s)\cdot dW_s$ with $\sigma(b)=(\sigma_1\sqrt{b_1},\dots,\sigma_d\sqrt{b_d})$, in the weak sense: $X$ is the canonical process on $C([0,T],\mathbb R)$, and an admissible pair $(\nu,\mathbb P)$ is a progressively measurable control $\nu=(\alpha,\beta)$ with a probability measure under which $X$ starts at $X_0$ and solves the associated martingale problem.

The consumer values consumption by $f(x)=\kappa x$ and the producer bears the generation cost $g(x)=\theta x$; write $\delta=\kappa-\theta$. For a payment $\xi$ made at time $T$, the consumer's and the producer's criteria are

$$J_A=\mathbb E^{\mathbb P}\Big[-e^{-r\left(\xi+\int_0^T(\kappa X_s-c(\nu_s))ds\right)}\Big],\qquad J_P=\mathbb E^{\mathbb P}\Big[-e^{-p\left(-\xi-\int_0^T\theta X_sds-\frac h2\langle X\rangle_T\right)}\Big].$$

A contract is an $\mathcal F_T$-measurable $\xi$ with uniform exponential moments (2.5). The first-best value is

$$V^{FB}=\sup\big\{J_P(\xi,\nu,\mathbb P):\ \xi\text{ a contract},\ (\nu,\mathbb P)\text{ admissible},\ J_A(\xi,\nu,\mathbb P)\ge R_0\big\}.$$

The consumer's Hamiltonians are $H_m(z)=-\inf_{a\in A}\{a\cdot\mathbf 1\,z+c_1(a)\}$ and $H_v(\gamma)=-\frac12\inf_{b\in B}\{c_2(b)-\gamma|\sigma(b)|^2\}$. Finally $\rho=\frac{rp}{r+p}$, $L_0=-\frac1r\log(-R_0)$, $U(x)=-e^{-px}$, $\bar\mu=\sum_i\mu_i$ and $x^-=\max(0,-x)$.

Formalization targets

Goal: Proposition 3.1 (i)

Assume $\delta^-T\le A_{\max}$. Then

$$V^{FB}=U\big(\bar v(0,X_0)-L_0\big),\quad \bar v(0,X_0)=\delta TX_0+\int_0^T\Big(\tfrac12\bar\mu(\delta^-)^2(T-t)^2+H_v\big(-h-\rho\delta^2(T-t)^2\big)\Big)dt.$$

Milestones

1. Proposition 2.1. The best responses $\hat a(z)$, $\hat b(\gamma)$ attain the infima defining $H_m$, $H_v$, and these Hamiltonians have explicit closed forms.
2. (A.5). The auxiliary value $\bar V=\sup_{(\nu,\mathbb P)}\mathbb E^{\mathbb P}\big[-e^{-\rho(\int_0^T(\delta X_t-c(\nu_t))dt-\frac h2\langle X\rangle_T)}\big]$ is finite and negative, and $V^{FB}=R_0(\bar V/R_0)^{1+p/r}$.
3. Proposition A.3 (i), with the explicit solution of p. 28.

$$\bar V=-e^{-\rho\left(\delta TX_0+\int_0^T\bar m(t)dt\right)},\qquad \bar m(t)=H_m(\delta(T-t))+H_v\big(-h-\rho\delta^2(T-t)^2\big).$$

Significance

The closed form shows how the first-best value depends on each parameter: on the energy value discrepancy $\delta$ through the mean-effort term, on the volatility cost $h$ and the effective risk aversion $\rho$ through the volatility Hamiltonian, and on the reservation utility only through the shift by $L_0$. It is one half of the paper's information rent (Proposition 3.4), the gap between the first- and second-best values, and it is the benchmark against which the calibrated contracts of the paper's Section 4 are judged.

The result is proved in the paper, partly by appeal to standard stochastic control arguments. To our knowledge it has no machine-checked proof. A formal proof requires a verification theorem for an exponential-utility control problem in the weak formulation, and a risk-sharing argument with a pathwise quadratic-variation term in the contract; both are reusable beyond this paper.

Difficulty

The deterministic parts, Proposition 2.1 and the algebra that turns (A.5) and the value of $\bar V$ into the goal, are calculus. The difficulty lies in the two stochastic steps. In (A.5), the producer's optimal payment for a given effort depends on $\langle X\rangle_T$; it must be realised as a measurable function of the path that is a contract in the sense of (2.5), uniformly over all admissible laws, and the participation constraint must be shown to bind. In Proposition A.3 (i), the upper bound on $\bar V$ must hold for every progressively measurable, path-dependent control, not only for Markov feedback controls; the paper invokes "standard stochastic control theory", which has to be made precise for controls of the volatility under a martingale-problem formulation, where no Brownian motion is given in advance.

Formalization scope

The canonical space is $C([0,T],\mathbb R)$ with the coordinate σ-algebra and the canonical filtration; processes are indexed by $[0,T]$. Admissible pairs are given by a martingale problem: $X_0=X_0$ almost surely, and both $X_t-X_0+\int_0^t\alpha_s\cdot\mathbf 1\,ds$ and its square minus $\int_0^t|\sigma(\beta_s)|^2ds$ are martingales. In the criteria, $\langle X\rangle_T$ is replaced by its almost-sure value $\int_0^T|\sigma(\beta_s)|^2ds$; a contract remains any $\mathcal F_T$-measurable function of the path. Expectations of utilities are negated lower Lebesgue integrals of exponentials in $[-\infty,0]$, and every value is an extended-real supremum with $\sup\emptyset=-\infty$. $B$ is read as $[\varepsilon,1]^d$, with indices in Fin N and Fin d.

The Hamiltonians are defined by their infima, never by their closed forms, so that Proposition 2.1 is not true by definition, and the first-best value is a supremum over the model's own objects, not a variable pinned by hypotheses. Three hypotheses are added to the page: $\varepsilon\le1$ (so $B\ne\emptyset$), $R_0<0$ (so $L_0$ is defined), and, for the goal only, $\delta^-T\le A_{\max}$, without which the printed $\frac12\bar\mu(\delta^-)^2(T-t)^2$ exceeds $H_m(\delta(T-t))$ and contradicts the paper's own proof. Misprints corrected and disclosed in the items: the closed form of $H_m$ in Proposition 2.1 is false for $z^->A_{\max}$ and is replaced by $\bar\mu(m z^--m^2/2)$ with $m=z^-\wedge A_{\max}$; the index range of $\hat b$ is $j=1,\dots,d$; on p. 28, $\int_0^t\bar m$ is $\int_t^T\bar m$ and "(A.11)" is (A.6).

The parts (ii)–(iii) of Proposition 3.1, the optimal efforts and the optimal contract, are not stated. Contributions welcome: a verification theorem for controlled martingale problems with bounded coefficients, exponential moment bounds uniform over admissible laws, and a pathwise quadratic variation on the canonical space.

Selected references

• R. Aïd, D. Possamaï, N. Touzi, Optimal electricity demand response contracting with responsiveness incentives, arXiv:1810.09063v3, 2019; Math. Oper. Res. 2022. https://arxiv.org/abs/1810.09063
• J. Cvitanić, D. Possamaï, N. Touzi, Dynamic programming approach to principal–agent problems, Finance Stoch. 22, 2018. https://arxiv.org/abs/1510.07111
• B. Holmström, P. Milgrom, Aggregation and linearity in the provision of intertemporal incentives, Econometrica 55, 1987. https://doi.org/10.2307/1913238
• Y. Sannikov, A continuous-time version of the principal–agent problem, Rev. Econ. Stud. 75, 2008. https://doi.org/10.1111/j.1467-937X.2007.00463.x
• I. Karatzas, S. Shreve, Brownian Motion and Stochastic Calculus, Springer, 1991, §5.4 (martingale problems and weak solutions). https://doi.org/10.1007/978-1-4612-0949-2

Motivation

Demand response asks electricity consumers to lower or smooth their consumption when generation is expensive, in exchange for payments. Field trials such as Low Carbon London showed two effects of such incentives: consumers reduce their average consumption, and the variability of their response depends on how much effort they put into it. A producer who cannot observe the consumer's individual usages, only the aggregate consumption path, faces a moral hazard problem: the payment can depend only on what is observed.

Aïd, Possamaï and Touzi (arXiv:1810.09063v3, 2019; Math. Oper. Res. 2022) cast this as a continuous-time principal–agent problem in which the consumer controls both the drift and the volatility of his consumption, and the producer pays for reductions in both. The volatility channel is what makes the problem new: the classical Holmström–Milgrom model (Econometrica 1987) controls only the drift. The paper uses the general reduction of Cvitanić, Possamaï and Touzi (Finance Stoch. 2018) to optimal contracts with volatility control, and obtains the producer's value in closed form up to a scalar minimisation. This mission formalizes that closed form.

Setting

Fix integers $N,d\ge0$, cost parameters $\mu\in(0,\infty)^N$ and $\lambda\in(0,\infty)^d$, nominal volatilities $\sigma\in(0,\infty)^d$, effort bounds $A_{\max}>0$ and $\varepsilon\in(0,1]$, risk aversions $r,p>0$, a marginal cost of volatility $h>0$, marginal energy value $\kappa$ and cost $\theta$ with $\delta:=\kappa-\theta$, a horizon $T>0$, an initial consumption $X_0$ and a reservation utility $R_0<0$. Write $\bar\mu:=\sum_i\mu_i$ and $x^-:=\max(0,-x)$.

Consumption. $X$ is the canonical process on $\Omega=C([0,T],\mathbb R)$ with its natural filtration $\mathbb F$. A control $\nu=(\alpha,\beta)$ is progressively measurable, with $\alpha_t\in A:=\prod_i[0,\mu_iA_{\max}]$ (effort to reduce consumption) and $\beta_t\in B:=[\varepsilon,1]^d$ (effort to reduce volatility). Under $\nu$ the consumption follows, in the weak sense,

$$X_t=X_0-\int_0^t\alpha_s\cdot\mathbf 1\,ds+\int_0^t\sigma(\beta_s)\cdot dW_s,\qquad |\sigma(b)|^2=\sum_j\sigma_j^2b_j .$$

Effort costs $c(\nu)=c_1(\alpha)+\frac12c_2(\beta)$ per unit time, with $c_1(a)=\frac12\sum_ia_i^2/\mu_i$ and $c_2(b)=\sum_j\frac{\sigma_j^2}{\lambda_j}(b_j^{-1}-1)$.

Criteria. For a payment $\xi$ at time $T$, the consumer's criterion is $J_A=\mathbb E[-e^{-r(\xi+\int_0^T(\kappa X_s-c(\nu_s))ds)}]$ and the producer's is $J_P=\mathbb E[U(-\xi-\int_0^T\theta X_sds-\frac h2\langle X\rangle_T)]$ with $U(x)=-e^{-px}$. Contracts $\mathcal C$ are the $\mathcal F_T$-measurable $\xi$ with exponential moments of order $m>1$ uniformly over the consumer's responses (2.5). The consumer's value is $V_A(\xi)=\sup J_A$, and $\mathcal P^\star(\xi)$ is the set of his optimal responses.

Second best. The producer offers $\xi$, the consumer responds optimally, ties are broken in the producer's favour, and participation requires $V_A(\xi)\ge R_0$:

$$V^{SB}:=\sup_{\xi\in\mathcal C,\ V_A(\xi)\ge R_0}\ \sup_{\mathcal P^\star(\xi)}J_P(\xi,\cdot),\qquad\sup\emptyset=-\infty .$$

Hamiltonians. $H_m(z)=-\inf_{a\in A}\{a\cdot\mathbf 1\,z+c_1(a)\}$ and $H_v(\gamma)=-\frac12\inf_{b\in B}\{c_2(b)-\gamma|\sigma(b)|^2\}$.

Formalization targets

Goal: Proposition 3.2 (i)

Assume $\delta^-T\le A_{\max}$. With $q_t(z)=h+rz^2+p(z-\delta(T-t))^2$, $L_0=-\frac1r\log(-R_0)$,

$$m_{SB}(t)=\frac12\bar\mu\delta^2(T-t)^2-\frac12\inf_{z\in\mathbb R}\Big\{\bar\mu\big(z^-+\delta(T-t)\big)^2-2H_v\big(-q_t(z)\big)\Big\},$$ $$V^{SB}=U\big(v(0,X_0)-L_0\big),\qquad v(0,X_0)=\delta TX_0+\int_0^Tm_{SB}(s)\,ds .$$

Milestones

1. Proposition 2.1. The consumer's best responses $\hat a_i(z)=\mu_i(z^-\wedge A_{\max})$ and $\hat b_j(\gamma)=(1\wedge(\lambda_j\gamma^-)^{-1/2})\vee\varepsilon$ attain the infima defining $H_m$ and $H_v$, and

$$H_m(z)=\bar\mu\big(m z^--\tfrac{m^2}2\big),\ m=z^-\wedge A_{\max};\qquad H_v(\gamma)=-\tfrac12\big(\hat c_2(\gamma)-\gamma|\hat\sigma(\gamma)|^2\big).$$

2. Lemma A.1. With $f_0(q,\gamma)=q|\hat\sigma(\gamma)|^2+\hat c_2(\gamma)$, $F_0(q):=\inf_{\gamma\le0}f_0(q,\gamma)=f_0(q,-q)=-2H_v(-q)$, and $F_0$ is non-decreasing.
3. Proposition A.4 (ii). A minimiser of $z\mapsto F_0(h-k+rz^2+p(z-y)^2)+\bar\mu(z^-+y)^2$ is $\frac p{r+p}y$ when $y\ge0$, and lies in $[y,\frac p{r+p}y]$ when $y\le0$.

A companion statement, Corollary 3.1 (i), gives the explicit off-peak payment rates $z_{SB}(t)=\frac p{r+p}\delta(T-t)$ and $\gamma_{SB}(t)=-h-\frac{rp}{r+p}\delta^2(T-t)^2$ when $\delta\ge0$.

Significance

The closed form reduces an infinite-dimensional contracting problem, a supremum over all path-dependent payments and all consumer responses, to a deterministic one-dimensional minimisation at each time. It is the basis of the paper's comparisons: with the first-best value it measures the cost of moral hazard, and its minimiser gives the price of energy and of responsiveness that the optimal contract charges, which the paper calibrates on Low Carbon London data.

The result is proved on paper. No part of it is machine-checked. A complete formalization would give a checked instance of a continuous-time principal–agent theorem with volatility control. It would also fix, in exact terms, the conventions the paper leaves implicit (weak solutions, the effort cap), and the printed misprints that this mission corrects.

Difficulty

The deterministic milestones are calculus on boxes. The goal is not. The upper bound $V^{SB}\le U(v(0,X_0)-L_0)$ must hold for every $\mathcal F_T$-measurable contract, not only for contracts of a convenient form. The step that fails in a direct attempt is the representation of an arbitrary contract: one needs that every $\xi\in\mathcal C$ inducing an optimal response can be written as $Y_T^{y_0,Z,\Gamma}$, an integral against $dX$ and $d\langle X\rangle$ driven by the consumer's continuation certainty equivalent. This is the main theorem of Cvitanić–Possamaï–Touzi (2018) and rests on second-order backward SDEs; it has no counterpart in Mathlib. Restricting the supremum to linear or representable contracts at the outset would assume exactly that theorem. The lower bound needs, for the candidate contract, existence of the consumer's optimal response as a weak solution and a verification argument for the producer's HJB equation.

Formalization scope

All objects live in the namespace DemandResponse.SecondBest, and all hypotheses are fields of a structure Params. Conventions:

• Weak formulation. An admissible pair $(\nu,\mathbb P)$ is a control and a probability measure on $C([0,T],\mathbb R)$ with $X_0=X_0$ a.s., under which $X_t-X_0+\int_0^t\alpha_s\cdot\mathbf 1\,ds$ and its square minus $\int_0^t|\sigma(\beta_s)|^2ds$ are $\mathbb F$-martingales. This is the martingale problem equivalent to weak solutions of (2.1); the paper deliberately leaves weak solutions informal (footnote 2). The pair, not the law alone, is the admissible object, because the cost depends on $\nu$.
• Quadratic variation. $\langle X\rangle_T$ in $J_P$ is its almost-sure value $\int_0^T|\sigma(\beta_s)|^2ds$.
• Values. Expected utilities are negated lower Lebesgue integrals, in $[-\infty,0]$; all suprema are in the extended reals, so the empty supremum is $-\infty$, as on p. 9.
• Hamiltonians are defined by their infima, not by the closed forms of Proposition 2.1.
• Indices are Fin N, Fin d; $N=0$, $d=0$ are allowed. $\hat b_j(\gamma)=1$ when $\lambda_j\gamma^-\le1$ (the paper's $0^{-1/2}=+\infty$).
• Added hypotheses. $\varepsilon\le1$ ($B\neq\emptyset$), $R_0<0$ ($\log(-R_0)$ defined), and for the goal $\delta^-T\le A_{\max}$. The paper's closed form is computed with the effort cap removed ("$\eta_A\to0$ as $A\nearrow\infty$", p. 30), and with the capped effort of the model it is correct exactly under this hypothesis.
• Corrected misprints. $-2H_m(-q(z))$ in $m_{SB}$ is read as $-2H_v(-q(z))$; with $H_m$ the infimum is $-\infty$. The printed $H_m(z)=\frac12\bar\mu(z^-\wedge A_{\max})^2$ is false for $z^->A_{\max}$ and is corrected. "$j=1,\dots,N$" for $\hat b$ means $j=1,\dots,d$. In Proposition A.4 (ii) the open interval becomes closed, and "for large $A$" is read as $\eta_A\equiv0$.

The goal is an equality of extended reals between $V^{SB}$, defined from the model, and an explicit real number. A formalization that defines $V^{SB}$ over a restricted class of contracts, or with a real-valued supremum that returns $0$ on unbounded sets, would trivialize or change it and is not the goal.

Needed infrastructure: continuous-time martingales on the canonical path space (Mathlib has Martingale and progressive measurability), existence of weak solutions with bounded coefficients, a representation theorem for contracts (Cvitanić–Possamaï–Touzi), and a verification theorem for the producer's HJB equation. The weak-formulation layer and the contract representation are reusable for any continuous-time principal–agent model with drift and volatility control. Contributions of any of these pieces, and proofs of the deterministic milestones, are welcome.

Selected references

• R. Aïd, D. Possamaï, N. Touzi, Optimal Electricity Demand Response Contracting with Responsiveness Incentives, arXiv:1810.09063v3, 2019; Mathematics of Operations Research 47 (2022). https://arxiv.org/abs/1810.09063v3
• J. Cvitanić, D. Possamaï, N. Touzi, Dynamic programming approach to principal–agent problems, Finance and Stochastics 22 (2018) 1–37. https://doi.org/10.1007/s00780-017-0344-4
• B. Holmström, P. Milgrom, Aggregation and Linearity in the Provision of Intertemporal Incentives, Econometrica 55 (1987) 303–328. https://doi.org/10.2307/1913238
• Y. Sannikov, A Continuous-Time Version of the Principal–Agent Problem, Review of Economic Studies 75 (2008) 957–984. https://doi.org/10.1111/j.1467-937X.2008.00486.x
• I. Karatzas, S. Shreve, Brownian Motion and Stochastic Calculus, 2nd ed., Springer 1991, §5.4 (martingale problem and weak solutions). https://doi.org/10.1007/978-1-4612-0949-2

Motivation

Thompson Sampling (TS) is the oldest heuristic for the stochastic multi-armed bandit problem: it was proposed by Thompson in 1933 (Biometrika 25) and is used in practice for online advertising and recommendation, where it often performs as well as or better than upper-confidence-bound methods (Chapelle and Li, NIPS 2011; Scott 2010). Until 2012 its theoretical guarantees for the frequentist regret were weak: earlier analyses gave only $o(T)$ regret in time $T$ (Granmo 2010; May, Korda, Lee and Leslie 2011).

Agrawal and Goyal, Analysis of Thompson Sampling for the Multi-armed Bandit Problem (arXiv:1111.1797v3, COLT 2012), gave the first logarithmic finite-time bound on the expected regret of TS. This mission formalizes their two-armed result, Theorem 1. A companion mission covers the $N$-armed bound, Theorem 2.

Timeline. Lai and Robbins (1985) proved that every consistent algorithm has regret at least $\big[\sum_i \Delta_i/D(\mu_i\|\mu^*)+o(1)\big]\ln T$. Auer, Cesa-Bianchi and Fischer (2002) gave UCB1 with an $O(\sum_i \ln T/\Delta_i)$ finite-time bound. Agrawal and Goyal (2012) proved $O(\ln T/\Delta+1/\Delta^3)$ for two-armed TS. Kaufmann, Korda and Munos (ALT 2012) and Agrawal and Goyal (AISTATS 2013) later proved asymptotically optimal bounds for Bernoulli TS.

Setting

There are two arms. Arm $i\in\{1,2\}$ has a fixed, unknown reward distribution $D_i$ supported in $[0,1]$, with mean $\mu_i$. Plays of an arm give i.i.d. rewards, independent of the other arm. Arm 1 is the unique optimal arm, $\mu_1>\mu_2$, and $\Delta=\mu_1-\mu_2$ is the gap.

Thompson Sampling for general stochastic bandits (Algorithm 2 of the paper) keeps, for each arm $i$, a success count $S_i$ and a failure count $F_i$, both starting at $0$. In each round $t=1,2,\dots$ it

1. samples, independently for each arm, $\theta_i(t)\sim\mathrm{Beta}(S_i+1,F_i+1)$;
2. plays $i(t)=\arg\max_i\theta_i(t)$ and observes a reward $\tilde r_t\sim D_{i(t)}$;
3. performs a Bernoulli trial with success probability $\tilde r_t$, with outcome $r_t\in\{0,1\}$;
4. increments $S_{i(t)}$ if $r_t=1$ and $F_{i(t)}$ otherwise.

$k_i(t)$ is the number of plays of arm $i$ before round $t$. The expected regret in time $T$ is

$$\mathbb E[\mathcal R(T)]=\mathbb E\Big[\sum_{t=1}^T(\mu_1-\mu_{i(t)})\Big],$$

the expectation being over the rewards and the algorithm's randomness.

The analysis uses the Beta cdf $F^{beta}_{\alpha,\beta}$, the binomial cdf $F^B_{n,p}$, and the random variable $X(j,s,y)$: the number of independent $\mathrm{Beta}(s+1,j-s+1)$ draws made before one exceeds $y$.

Formalization targets

Goal: Theorem 1 (p. 3)

There is an absolute constant $C>0$ such that for every two-armed instance with rewards in $[0,1]$ and $\mu_1>\mu_2$, and every $T\ge 2$,

$$\mathbb E[\mathcal R(T)]\le C\Big(\frac{\ln T}{\Delta}+\frac1{\Delta^3}\Big).$$

The constant is not fixed numerically: the paper states the theorem in $O(\cdot)$ form (footnote 1), and the explicit display it reports on p. 8, $40\ln T/\Delta+48/\Delta^3+18\Delta$, is not the formal claim.

Milestones

• Fact 1 (p. 12): $F^{beta}_{\alpha,\beta}(y)=1-F^B_{\alpha+\beta-1,y}(\alpha-1)$ for positive integers $\alpha,\beta$.
• Lemma 1 (p. 6): $\mathbb E[X(j,s,y)]=1/F^B_{j+1,y}(s)-1$.
• Lemma 6 (p. 13): Hoeffding-type bounds (10)–(11) on binomial cdfs.
• Fact 2 (p. 13): every median of $\mathrm{Binomial}(n,p)$ is $\lfloor np\rfloor$ or $\lceil np\rceil$.
• Lemma 2 (p. 7): $\Pr(E_2(t))\ge 1-2/T^2$, where $E_2(t)=\{\theta_2(t)\le\mu_2+\Delta/2\ \text{or}\ k_2(t)<24\ln T/\Delta^2\}$.
• Lemma 3 (p. 7): a three-case bound on $\mathbb E\big[\mathbb E[\min\{X(j,s(j),y),T\}\mid s(j)]\big]$ for $s(j)\sim\mathrm{Binomial}(j,\mu_1)$.
• Eq. (1) (p. 7): $\mathbb E[k_2(T)]\le C(\ln T/\Delta^2+1/\Delta^4)$.

Significance

The result. Theorem 1 shows that TS, a randomized Bayesian heuristic with no explicit confidence bonus, has regret logarithmic in $T$ on every two-armed instance, matching the order in $T$ of the Lai–Robbins lower bound. The proof introduced a way to control the optimal arm's waiting time between plays through the Beta–Binomial duality, and later analyses of TS reuse that device.

Formalizing it. The result is proved on paper and has no machine-checked proof that we know of. The platform's existing TS results concern Gaussian TS (Lattimore and Szepesvári, Ch. 36) and Bayesian regret, which are different algorithms or regret notions. A formalization adds a reusable Lean model of Algorithm 2 on $[0,1]$-valued rewards, Beta–Binomial facts (Fact 1, Lemma 1), a binomial-median theorem, and binomial Hoeffding bounds. It also produces a proof with a constant that has been checked, since the printed constants contain an arithmetic slip.

Difficulty

The standard UCB argument does not transfer to TS. For UCB, the optimal arm's index exceeds its mean with high probability however often the arm has been played, because the exploration bonus is deterministic; the analysis then only has to count plays of the suboptimal arm until its own index concentrates, after $\Theta(\ln T/\Delta^2)$ plays. Under TS the optimal arm's sample $\theta_1(t)$ is random and, if the arm has been played rarely or its early rewards were poor, it falls below $\mu_2$ with constant probability. The optimal arm may then wait a long, random time between plays, and the length of that wait depends on the arm's posterior, which in turn depends on how long it has waited. Counting plays of the suboptimal arm with a union bound over rounds, under the assumption that the optimal arm is already concentrated, therefore does not work; controlling these waiting times is the central difficulty and is where the $1/\Delta^3$ dependence enters.

Formalization scope

• Model. The instance is the platform's StochasticBandit 2 (a probability measure on $\mathbb R$ per arm, mean banditArmMean), with the hypothesis that each reward law gives mass $1$ to $[0,1]$. Lean arm 0 is the paper's arm 1 and Lean arm 1 the paper's arm 2. Lean rounds are indexed from $0$.
• Algorithm. Algorithm 2 is realized on one probability space with three independent i.i.d. tables: Beta draws $W(i,t,a,b)\sim\mathrm{Beta}(a+1,b+1)$, rewards $X(i,t)\sim D_i$, and uniforms $V(i,t)$. Round $t$ uses $\theta_i(t)=W(i,t,S_i(t),F_i(t))$, $\tilde r_t=X(i(t),t)$ and $r_t=\mathbf 1\{V(i(t),t)<\tilde r_t\}$. Ties in the arg max go to the smaller index (a null event).
• Values. Regret and expectations are lower Lebesgue integrals in $[0,\infty]$. $X(j,s,y)$ is $\mathbb N\cup\{\infty\}$-valued, so Lemma 1 at $y=1$ reads $\infty=\infty$, as in the paper.
• O(·). The paper's $O(\cdot)$ (footnote 1: $f\le cg$ for $n\ge n_0$) is stated with one universal constant $C>0$, quantified before the instance, the means and the horizon, for all $T\ge 2$. Eq. (1) is stated the same way, without its printed numerals.
• Not trivial. The goal is about Algorithm 2 itself, with fresh Beta samples, fresh rewards and the Bernoulli coin. A statement about "any policy satisfying Lemma 2's event bound", or one whose constant depends on $\Delta$, the reward laws or $T$, would not be Theorem 1.
• Edge cases. $\mu_1<1$ is assumed only in Lemma 3, where the paper's $R$ and $D$ require it. It is not a hypothesis of the goal.
• Infrastructure. A complete proof needs: inverse-transform or order-statistics facts for Beta laws (Fact 1); geometric expectations; Hoeffding's inequality for sums of Bernoulli variables (Mathlib has Hoeffding/Azuma); the binomial median theorem (Jogdeo–Samuels; Kaas–Buhrman); and the coupling from the reward tables to the per-arm i.i.d. output stacks the paper reasons with. Fact 1, Lemma 6 and Fact 2 are reusable beyond this mission. Contributions to any milestone are welcome, and so is a direct proof of the regret bound with an explicit constant.

Selected references

• S. Agrawal and N. Goyal, Analysis of Thompson Sampling for the Multi-armed Bandit Problem, COLT 2012; arXiv:1111.1797v3. https://arxiv.org/abs/1111.1797
• W. R. Thompson, On the likelihood that one unknown probability exceeds another in view of the evidence of two samples, Biometrika 25 (1933) 285–294. https://doi.org/10.2307/2332286
• T. L. Lai and H. Robbins, Asymptotically efficient adaptive allocation rules, Advances in Applied Mathematics 6 (1985) 4–22. https://doi.org/10.1016/0196-8858(85)90002-8
• P. Auer, N. Cesa-Bianchi and P. Fischer, Finite-time analysis of the multiarmed bandit problem, Machine Learning 47 (2002) 235–256. https://doi.org/10.1023/A:1013689704352
• K. Jogdeo and S. M. Samuels, Monotone convergence of binomial probabilities and a generalization of Ramanujan's equation, Annals of Mathematical Statistics 39 (1968) 1191–1195. https://doi.org/10.1214/aoms/1177698243
• R. Kaas and J. M. Buhrman, Mean, median and mode in binomial distributions, Statistica Neerlandica 34 (1980) 13–18. https://doi.org/10.1111/j.1467-9574.1980.tb00681.x
• O. Chapelle and L. Li, An empirical evaluation of Thompson Sampling, NIPS 2011. https://papers.nips.cc/paper/4321-an-empirical-evaluation-of-thompson-sampling

Motivation

Project scheduling with cumulative resources models production and logistics projects in which activities fill and empty storage: an activity withdraws material from an inventory when it starts and deposits its output when it completes, and every inventory must stay between a safety stock and a storage capacity. Neumann, Schwindt and Zimmermann treat this model in §2.12 of Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003, doi:10.1007/978-3-540-24800-2) and use it in their process-industry applications.

Before any optimization, a scheduler must know whether a feasible schedule exists at all. Theorem 2.12.1 of the book answers the complexity of this question: it is NP-complete, and it stays NP-complete when the project network has no cycles. The contrast with renewable resources (machines, workers) is the point of the theorem: with renewable resources, the feasibility problem is NP-complete as well (Theorem 2.3.13, after Bartusch, Möhring and Radermacher, 1988), but an acyclic network always admits a feasible schedule when every requirement is within capacity.

The mission also collects the two other reductions the book proves in full: Proposition 2.5.4 (recognizing whether an activity lies in some minimal delaying alternative, the branching object of the book's branch-and-bound procedures, is NP-complete) and Proposition 3.4.2 (maximizing weighted start-time deviations, a resource-levelling objective, is NP-hard without any resource constraints).

Setting

A project has activities $V=\{0,1,\dots,n+1\}$ with $n\ge1$; activity $0$ is the project beginning and $n+1$ the project completion. Activity $i$ has a duration $p_i\in\mathbb N$, with $p_0=p_{n+1}=0$. The project network $N$ has arc set $E$; an arc $\langle i,j\rangle$ with integer weight $\delta_{ij}$ imposes the temporal constraint $S_j-S_i\ge\delta_{ij}$ on the start times. A schedule is a real vector $S=(S_i)_{i\in V}$ with $S_0=0$ and $S_i\ge0$; it is time-feasible if it meets every temporal constraint.

Cumulative resources $k\in\mathcal R^\gamma$ carry integer demands $r_{ik}$: $r_{ik}<0$ depletes $-r_{ik}$ units at the start $S_i$, $r_{ik}>0$ replenishes $r_{ik}$ units at the completion $S_i+p_i$, and $r_{0k}$ is the initial stock. The inventory at time $t$ is

$$r_k(S,t)=\sum_{i:\ r_{ik}<0,\ S_i\le t} r_{ik}+\sum_{i:\ r_{ik}>0,\ S_i+p_i\le t} r_{ik}.$$

With safety stock $\underline R_k$ and storage capacity $\overline R_k$ (integers, $\underline R_k\le\sum_{i\in V}r_{ik}\le\overline R_k$ by (2.12.1)), $S$ is feasible if it is time-feasible and $\underline R_k\le r_k(S,t)\le\overline R_k$ for every $k$ and every $t\ge0$. The decision problem of $PSc|temp|C_{\max}$ asks whether a feasible schedule exists.

For renewable resources $k\in\mathcal R$ with capacities $R_k$ and requirements $r_{ik}\in\mathbb N$, a set $F\subseteq V$ is forbidden if $\sum_{i\in F}r_{ik}>R_k$ for some $k$. A delaying alternative for $F$ is a set $B\subseteq F$ such that $F\setminus B$ is not forbidden; it is minimal if no proper subset of $B$ is one.

In $PS\infty|temp,\bar d|f$ there are no resources, schedules must also satisfy $S_{n+1}\le\bar d$, and the objective here is $f(S)=-\sum_{i\in V}\sum_{j>i}w_{ij}|S_j-S_i|$ with weights $w_{ij}\ge0$.

NP and NP-completeness are taken in the sense of Cook's Turing-machine formulation, with instances written in binary.

Formalization targets

Goal: Theorem 2.12.1

Assuming PARTITION is NP-complete,

$$L=\{\text{codes of instances of }PSc|temp|C_{\max}\text{ with a feasible schedule}\}\ \text{ and }\ L_{\mathrm{acyc}}=L\cap\{N\text{ acyclic}\}$$

are both NP-complete.

Milestones

1. Membership (proof of Theorem 2.12.1): $L\in\mathrm{NP}$ and $L_{\mathrm{acyc}}\in\mathrm{NP}$.
2. Reduction correctness (proof of Theorem 2.12.1): for sizes $s(1),\dots,s(\nu)$ with even sum, the project with $r_0=r_{n+1}=-\sum s(i)/2$, $r_i=s(i)$, $\underline R=\overline R=0$, $d^{\min}_{0,n+1}=1$ has an acyclic network, and it has a feasible schedule iff the sizes split into two parts of equal sum.
3. Polynomial transformation: $\mathrm{PARTITION}\le_p L_{\mathrm{acyc}}$.
4. Proof of Proposition 2.5.4, one resource: for $j^*\in B\subseteq F$, $B$ is a minimal delaying alternative iff $R-\min_{j\in B}r_j<\sum_{i\in F\setminus B}r_i\le R$.
5. Proof of Proposition 2.5.4, with $r_{j^*}=1$: a minimal delaying alternative contains $j^*$ iff some $A\subseteq F\setminus\{j^*\}$ has $\sum_{i\in A}r_i=R$.
6. Proposition 2.5.4: assuming SUBSET SUM is NP-complete, deciding whether some minimal delaying alternative for a forbidden set $F$ contains $j^*\in F$ is NP-complete.
7. Proof of Proposition 3.4.2: a graph has a cut of at least $M$ edges iff the constructed instance has a schedule with $S_i\in\{0,1\}$ and $\sum_{i<j}w_{ij}|S_j-S_i|\ge M$.
8. Proposition 3.4.2: assuming SIMPLE MAX CUT is NP-complete, the decision version of $PS\infty|temp,\bar d|-\sum\sum w_{ij}|S_j-S_i|$ is NP-hard.

The goal follows from milestones 1 and 3 together with the transfer of NP-completeness along $\le_p$ (on the platform as CookPvsNP.npComplete_of_polyReducible).

Significance

The result. Theorem 2.12.1 explains why the book's methods for cumulative resources enumerate precedence relations between depleting and replenishing activities (minimal surplus and shortage sets, Theorem 2.12.4) instead of relying on a constructive feasibility test: unless P = NP, no polynomial algorithm decides feasibility, even for acyclic networks, where the renewable-resource case is trivial. Proposition 2.5.4 does the same for the branching scheme of §2.5, and Proposition 3.4.2 places the resource-levelling objectives of Chapter 3 among the hard ones.

Formalizing it. The three results are proved in the book, as short reductions whose delicate steps are left implicit: the polynomial size of a certificate for real-valued schedules, the handling of instances outside the construction (odd sums, empty index sets, oversized items), and the passage from an optimization problem to its decision version. None of the three reductions is machine-checked anywhere known. The mission states them against a single Turing-machine model and a single binary encoding, reusing the published definitions CookPvsNP_defs, so that the reductions compose with the Cook–Levin development already on the platform.

Difficulty

The mathematical content of the reductions is short; the difficulty is in the complexity-theoretic layer. Two steps resist the obvious argument.

First, NP membership. The book's certificate is a schedule, and a schedule is a real vector: it is not a string. A verifier needs a finite certificate of polynomial length, and it is not immediate that a feasible instance has a feasible schedule with small rational (or integer) start times, since the inventory constraints involve strict orderings between event times.

Second, polynomial-time computability in a concrete Turing-machine model. The transformation must compute, on a one-tape machine, binary codes of sums and halves of the input sizes, an arc list of quadratic length, and must map malformed strings to fixed no-instances. Informal "clearly polynomial" arguments have to become explicit machine constructions or a reusable library of closure properties.

Formalization scope

The Lean development fixes the following conventions.

• Activities are Fin (n + 2), with the completion Fin.last (n + 1); resources are Fin m. Start times are real.
• The inventory constraints hold for every $t\ge0$, not only for $0\le t\le\bar d$ as (2.12.2) is printed; the book's proofs use this reading.
• Real activities may have duration $0$ in $PSc|temp|C_{\max}$: the reduction of Theorem 2.12.1 uses only such activities.
• Instances are coded as lists of integers written in binary over the alphabet $\{0,1,-,\#\}$; arc weights are listed for every ordered pair of activities together with an arc indicator. Well-formedness (standing assumptions such as $n\ge1$, $p_0=p_{n+1}=0$, no loops, (2.12.1), $r_{ik}\le R_k$) is part of each language.
• "Acyclic" means the nodes admit a numbering increasing along every arc.
• The NP-completeness of PARTITION, SUBSET SUM and SIMPLE MAX CUT (Karp, 1972) enters as a hypothesis of the corresponding theorem; these are not results of the book.
• Proposition 3.4.2 is stated for the decision version of the optimization problem, with natural-number weights and threshold.

A trivializing formalization is ruled out: the languages contain only codes of well-formed instances, the encoding is injective, and the hypotheses on the source problems are true theorems, so the goal cannot hold vacuously or by a degenerate encoding.

A complete development needs closure properties of polynomial-time computable functions in Cook's model (composition, binary arithmetic, list manipulation), transitivity of $\le_p$, and a small-certificate lemma for systems of difference constraints with strict and non-strict inequalities. These are reusable for every NP-hardness proof stated in the same framework. Contributions to any of them, to the instance-level milestones 2, 4, 5 and 7, or to the NP-completeness of PARTITION, SUBSET SUM and SIMPLE MAX CUT in this model, are welcome.

Selected references

• K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003. doi:10.1007/978-3-540-24800-2
• M. Bartusch, R. H. Möhring, F. J. Radermacher, Scheduling project networks with resource constraints and time windows, Annals of Operations Research 16, 1988.
• M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979.
• R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972. doi:10.1007/978-1-4684-2001-2_9
• S. Cook, The P versus NP Problem, Clay Mathematics Institute problem description. claymath.org

Motivation

In make-to-order production, chemical process industries and other manufacturing settings modelled as projects, activities do not only occupy machines for a while: they also consume intermediate products at their start and deposit products into storage facilities at their completion. Storage is bounded above by a tank or warehouse capacity and below by a safety stock. Resources of this kind are called cumulative resources (or inventory resources, reservoirs in the constraint-programming literature). They were introduced into resource-constrained project scheduling by Neumann and Schwindt (2002), and Chapter 2 of Neumann, Schwindt and Zimmermann, Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003), develops their theory in §2.12.

A scheduler handling cumulative resources needs a finite combinatorial description of which schedules respect the inventory bounds at every instant, because the time axis is continuous and cannot be checked point by point in a search procedure. Theorem 2.12.4 of the book gives such a description, and it is the basis of the branch-and-bound procedure of Neumann and Schwindt for the problem $PSc|temp|C_{\max}$.

Setting

A project consists of activities $V=\{0,1,\dots,n+1\}$ with $n\ge 1$, where $0$ is the project beginning and $n+1$ the project completion. Activity $i$ has an integer duration $p_i\ge 0$, with $p_0=p_{n+1}=0$ and $p_i>0$ for the real activities.

For each cumulative resource $k$ in a set $\mathcal R^\gamma$, every activity $i$ has an integer demand $r_{ik}$. If $r_{ik}<0$, activity $i$ withdraws $-r_{ik}$ units of $k$ at its start; if $r_{ik}>0$, it deposits $r_{ik}$ units at its completion; $r_{ik}=0$ means $k$ is not used. The demand $r_{0k}$ of the project beginning is the initial stock. Write $V_k^-=\{i\mid r_{ik}<0\}$ and $V_k^+=\{i\mid r_{ik}>0\}$. Each resource has a safety stock $\underline R_k\in\mathbb Z$ and a storage capacity $\overline R_k\in\mathbb Z$.

A schedule is a vector $S=(S_i)_{i\in V}$ of real start times with $S_0=0$ and $S_i\ge 0$. The active set and the inventory of $k$ at time $t\ge 0$ are

$$\mathcal A_k(S,t)=\{i\in V_k^-\mid S_i\le t\}\cup\{i\in V_k^+\mid S_i+p_i\le t\},\qquad r_k(S,t)=\sum_{i\in\mathcal A_k(S,t)} r_{ik}.$$

The schedule is inventory-feasible if $\underline R_k\le r_k(S,t)\le\overline R_k$ for all $k$ and all $t\ge 0$.

Two standing assumptions of the section are used throughout: (2.12.1) $\underline R_k\le\sum_{i\in V}r_{ik}\le\overline R_k$, so the final inventory is admissible; and Remark 2.12.2, $\underline R_k\le 0\le\overline R_k$.

A nonempty $F\subseteq V$ is a $k$-surplus set if $\sum_{i\in F}r_{ik}>\overline R_k$, and a $k$-shortage set if $\sum_{i\in F}r_{ik}<\underline R_k$. A $k$-surplus set $F$ is minimal if no $k$-surplus set arises from $F$ by removing a nonempty set of replenishing activities, and none arises by adding a nonempty set of depleting activities. Minimal $k$-shortage sets are defined with the roles of replenishing and depleting activities exchanged. $\mathcal F_k^+$ and $\mathcal F_k^-$ denote the minimal $k$-surplus and $k$-shortage sets.

Formalization targets

Goal: Theorem 2.12.4

A schedule $S$ is inventory-feasible if and only if

$$\forall k,\ \forall F\in\mathcal F_k^+\ \exists j\in F,\ i\notin F:\ r_{jk}>0,\ r_{ik}<0,\ S_j+p_j\ge S_i,$$ $$\forall k,\ \forall F\in\mathcal F_k^-\ \exists j\in F,\ i\notin F:\ r_{jk}<0,\ r_{ik}>0,\ S_j\ge S_i+p_i.$$

Milestones

1. The invariance claim after Remark 2.12.2 (p. 131): adding the same integer $a_k$ to $r_{0k}$, $\underline R_k$ and $\overline R_k$ does not change the set of inventory-feasible schedules.
2. Lemma 2.12.3 (a): for every $k$-surplus set $F$ there is a minimal $k$-surplus set $F'$ with $\emptyset\ne F'\cap V_k^+\subseteq F\cap V_k^+$ and $F'\cap V_k^-\supseteq F\cap V_k^-$.
3. Lemma 2.12.3 (b): the shortage counterpart.
4. Theorem 2.12.4 (a) on its own: the upper constraints $r_k(S,t)\le\overline R_k$ hold for all $t\ge 0$ iff condition (a) holds.
5. Theorem 2.12.4 (b) on its own: the lower constraints hold for all $t\ge 0$ iff condition (b) holds.

Significance

The theorem turns a constraint over a continuum of time points into finitely many disjunctions, each a choice among precedence relations. An inventory excess caused by a minimal surplus set is removed by a start-to-completion relation $S_j+p_j\ge S_i$ (a replenishment is postponed until after a withdrawal starts, equivalently a maximum time lag), and a shortage by a completion-to-start relation $S_j\ge S_i+p_i$. Consequences stated in the book: the feasible region of $PSc|temp|C_{\max}$ is a finite union of polyhedra; branching on these relations, organized as pairs of strict orders and reflexive relations, is a complete search scheme; and minimal delaying alternatives for surplus and shortage sets can be enumerated. Because every problem with renewable resources can be rewritten as one with cumulative resources (p. 130), the book also concludes that this union of polyhedra is in general disconnected.

The result is proved in the book (and in Neumann and Schwindt, 2002). To our knowledge it has no machine-checked proof. This mission produces a Lean formalization of the model, of the one-sided minimality notion, and of the two-sided characterization with its supporting lemma.

Difficulty

The combinatorial core is simple to state but easy to state wrongly. The natural first idea, to use inclusion-minimal surplus sets as for renewable resources, gives a different family $\mathcal F_k^+$ and a false theorem: the book's minimality allows removing only replenishing activities and adding only depleting ones. The existence lemma needs Remark 2.12.2 to keep at least one replenishing activity in the minimal set, and the sufficiency direction needs (2.12.1) to guarantee a depleting activity outside the minimal set. Both membership conditions of the active set are closed at $t$, so activities that deplete or replenish exactly at the critical instant must be counted on the correct side; a half-open reading changes which schedules are feasible. The initial stock $r_{0k}$ is handled by the same active-set rule as any other demand, which matters for the invariance claim.

Formalization scope

• Activities are Fin (n + 2), activity $n+1$ is Fin.last (n + 1); resources are an arbitrary type K. Demands, safety stocks and capacities are integers (ℤ); start times are reals (ℝ); durations are natural numbers cast to ℝ.
• The inventory constraints are required for every $t\ge 0$. The book prints (2.12.2) for $0\le t\le\bar d$, but its proof of Theorem 2.12.4 works with an arbitrary $t\ge 0$ (the necessity half uses the last completion time of a replenishing activity, which need not be at most $\bar d$). The two readings coincide for schedules with $S_{n+1}\le\bar d$ whose activities all finish by $S_{n+1}$.
• A schedule satisfies $S_0=0$ and $S_i\ge 0$ and is not required to be time-feasible; time lags play no role in this section's results and are not part of the model.
• (2.12.1) and Remark 2.12.2 are explicit hypotheses (TotalDemandWithinBounds, BoundsStraddleZero) wherever the book's proofs use them. Surplus and shortage sets are nonempty by definition, and minimality uses proper inclusions.
• A formalization in which $\mathcal F_k^+$ is empty or trivial (for instance, minimality with non-strict inclusions, which no set satisfies) makes condition (a) vacuous; the definitions here follow p. 131 exactly, and a concrete instance with a nonempty $\mathcal F_k^+$ has been checked locally.

Reusable parts: the cumulative-resource model and inventory profile, which later missions on continuous cumulative resources (§2.12.2) or on the NP-completeness of $PSc|temp|C_{\max}$ (Theorem 2.12.1) can build on. Contributions welcome: proofs of the lemmas, of either half of the theorem, and finite-sum lemmas about Finset.filter that the proofs need.

Selected references

• K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003, §2.12.1, pp. 128–135. https://doi.org/10.1007/978-3-540-24800-2
• K. Neumann, C. Schwindt, Project scheduling with inventory constraints, Mathematical Methods of Operations Research 56 (2003) 513–533 (cited in the book as 2002). https://doi.org/10.1007/s001860200251