Operations Research

Motivation

Many scheduling situations involve more than one decision maker sharing a resource. Two departments of a firm may share a machine shop, two clients may share a contractor, or two users may share a processor, and each cares only about how its own jobs are served. Agnetis, Mirchandani, Pacciarelli and Pacifici (Oper. Res. 52(2), 2004) introduced a systematic study of such two-agent scheduling problems. Their framework has two questions. The constrained problem asks for the best schedule for one agent among those that keep the other agent's cost below a bound. The Pareto problem asks for the schedules whose cost pair cannot be improved for one agent without hurting the other. The paper settles the complexity of these questions for the standard scheduling objectives and gave rise to a large literature on multi-agent scheduling (see the survey by Perez-Gonzalez and Framinan, EJOR 235, 2014).

This mission covers §5.2 of the paper: agent $A$ minimizes the total completion time of its jobs, and agent $B$ requires that the maximum of its jobs' regular costs stay below a bound $Q$.

Setting

Agent $A$ owns jobs $J^A_1,\dots,J^A_{n_A}$ and agent $B$ owns jobs $J^B_1,\dots,J^B_{n_B}$. Job $J_j$ has a processing time $p_j>0$. All jobs are available at time $0$ and are processed one at a time, without interruption, on a single machine. Because every objective here is nondecreasing in the completion times, the machine is never left idle, and a schedule $\sigma$ is simply a sequence of all $n_A+n_B$ jobs; the completion time $C_j(\sigma)$ of a job is the total processing time of that job and the jobs before it. Write $P_A$ and $P_B$ for the total processing times of the two agents.

Agent $A$'s objective is the total completion time $\sum_h C^A_h(\sigma)$. Each $B$-job has a nondecreasing cost function $f^B_k$, and agent $B$'s objective is the maximum cost

$$f^B_{\max}(\sigma)=\max_k f^B_k\bigl(C^B_k(\sigma)\bigr).$$

Given a bound $Q$, a schedule is feasible for the problem $1\|\sum C^A_i : f^B_{\max}\le Q$ if $f^B_k(C^B_k)\le Q$ for every $B$-job, and optimal if it is feasible and minimizes $\sum C^A_h$ among feasible schedules. The instance is feasible if a feasible schedule exists. A schedule is nondominated if no schedule is at least as good for both agents and strictly better for one.

The paper solves the problem with a backward rule (Figure 1). Fill the sequence from the end. With $\tau$ the total length of the jobs not yet placed, place last any unplaced $B$-job with $f^B_k(\tau)\le Q$. If there is none, place last a longest unplaced $A$-job. If neither exists, the instance is infeasible. The least-cost variant of §5.2.1 chooses, among the $B$-jobs, one minimizing $f^B_k(\tau)$ over all unplaced $B$-jobs. A B-block of a schedule is a maximal run of consecutive $B$-jobs.

Formalization targets

Goal: Theorem 5.7

On a feasible instance with $n_B\ge1$, every schedule $\tilde\sigma$ produced by the least-cost variant, under any tie-breaking, satisfies

$$\tilde\sigma \text{ is optimal for } 1\|\textstyle\sum C^A_i : f^B_{\max}\le Q \quad\text{and}\quad \tilde\sigma \text{ is nondominated for } \bigl(\textstyle\sum C^A_i,\ f^B_{\max}\bigr).$$

The nondominance is the printed theorem; the optimality is how the paper introduces $\tilde\sigma$, and rests on Theorem 5.5.

Milestones

• Lemma 5.3: if some $B$-job $J^B_{\bar k}$ has $f^B_{\bar k}(P_A+P_B)\le Q$, some optimal schedule ends with $J^B_{\bar k}$ and no optimal schedule ends with an $A$-job.
• Lemma 5.4: if every $B$-job has $f^B_k(P_A+P_B)>Q$, every optimal schedule ends with a longest $A$-job.
• Theorem 5.5 (correctness): on a feasible instance every schedule of Figure 1 is optimal, and Figure 1 runs to completion exactly on feasible instances.
• Lemma 5.6: all optimal schedules have the same partition of the $B$-jobs into B-blocks, and each B-block occupies the same time interval in all of them.

Significance

Theorem 5.5 shows that the constrained problem with total completion time against a maximum cost is solvable by sorting, in contrast to its weighted version, which the same section shows NP-hard. Lemma 5.6 describes all optimal schedules: they agree on the completion times of the $A$-jobs (up to permuting identical jobs) and on the B-blocks, and differ only inside each block. Theorem 5.7 turns this into a nondominated schedule. It is the building block for the Pareto problem $1\|\sum C^A_i\circ f^B_{\max}$ of §11.2, where solving the constrained problem for a sequence of bounds enumerates the nondominated pairs.

The results are proved in the paper; none of them has a machine-checked proof that we know of. The mission formalizes the statements and asks for their proofs. The proof of Theorem 5.7 invokes "the very same proof of Lawler's algorithm (Lawler 1973) restricted to $1\|f_{\max}$", applied inside each B-block. Lawler's rule is a separate statement on the platform, LawlerPrec.MinMax.lawler_rule_optimal, currently open. A solver may prove it and adapt it, but the goal does not need it in that exact form.

Difficulty

The interchange arguments of Lemmas 5.3 and 5.4 are short. The obstacle is Lemma 5.6. Two optimal schedules can differ in which $B$-job is placed at each step, and in the order of $A$-jobs of equal length. The paper's argument compares the completion time of each $A$-job across two optimal schedules and shows it cannot move earlier. That needs the fact that a $B$-job finishing before an $A$-job could not have been placed at that $A$-job's completion time, which comes from applying Lemma 5.3 to a prefix of the schedule. Formalizing it requires restricting optimality to prefixes and sub-instances, which the bare sequence model does not provide. The tempting shortcut of proving Theorem 5.7 from Lawler's rule on the whole schedule fails, since the bound $Q$ and agent $A$'s objective change which jobs may be placed where; the reduction is only to one Lawler instance per block.

Formalization scope

Jobs are Fin nA ⊕ Fin nB (0-based). A schedule is a duplicate-free list of all jobs, with completion times from the published sequence model MooreLateJobs.Shared.completionTime (Moore 1968 series), which this mission reuses. Processing times are real and strictly positive. Without positivity the second claim of Lemma 5.3 fails, because a zero-length $B$-job can sit anywhere. Cost functions are real-valued and nondecreasing, and $Q$ is real (the paper's integer $Q$ is a special case). Feasibility is stated job by job; $f^B_{\max}$ is a finite maximum and requires $n_B\ge1$, which the goal assumes. Lemma 5.4 assumes $n_A\ge1$, since "a longest $A$-job" presupposes one.

The paper's loose phrases are read as follows:

• "the algorithm" is a property of a finished sequence. At position $m$, with the jobs at positions $0,\dots,m$ unplaced and $\tau$ their total length, the job at $m$ must be a choice the rule allows.
• "Ties are broken arbitrarily" means that every sequence satisfying the rule is covered.
• "no solution exists, STOP" leaves no allowed choice. Running to completion therefore means that some sequence satisfies the rule.
• "the optimal schedule generated in this way" puts optimality into the goal as a conclusion, not a hypothesis.
• "a longest A-job" is an $A$-job of maximal length; when several are tied, no statement fixes which one.
• Nondominance quantifies over all schedules, not only those feasible for $Q$.
• A B-block's interval runs from the earliest start to the latest completion of its jobs.

The running times of Theorems 5.5 and 5.8 ($O(n_A\log n_A+n_B\log n_B)$ and $O(n_A\log n_A+n_B^2)$) are not formalized. Nor is the claim (3) inside the proof of Lemma 5.6.

A trivializing formalization is ruled out: feasibility of the instance is a hypothesis and not built into the rule, the rule constrains every position, and the goal asserts nondominance against all schedules.

Useful infrastructure includes interchange lemmas for the sequence model (moving one job to the end, swapping two jobs), restriction of a schedule to a prefix, and Lawler's rule for $1\|f_{\max}$ on a fixed time window. The interchange lemmas and the prefix restriction are reusable across the whole two-agent series.

Selected references

• A. Agnetis, P. B. Mirchandani, D. Pacciarelli, A. Pacifici, Scheduling Problems with Two Competing Agents, Operations Research 52(2), 229–242, 2004. https://doi.org/10.1287/opre.1030.0092
• E. L. Lawler, Optimal Sequencing of a Single Machine Subject to Precedence Constraints, Management Science 19(5), 544–546, 1973. https://doi.org/10.1287/mnsc.19.5.544
• J. M. Moore, An n Job, One Machine Sequencing Algorithm for Minimizing the Number of Late Jobs, Management Science 15(1), 102–109, 1968. https://doi.org/10.1287/mnsc.15.1.102
• R. L. Graham, E. L. Lawler, J. K. Lenstra, A. H. G. Rinnooy Kan, Optimization and Approximation in Deterministic Sequencing and Scheduling: A Survey, Annals of Discrete Mathematics 5, 287–326, 1979. https://doi.org/10.1016/S0167-5060(08)70356-X
• P. Perez-Gonzalez, J. M. Framinan, A common framework and taxonomy for multicriteria scheduling problems with interfering and competing jobs: Multi-agent scheduling problems, European Journal of Operational Research 235(1), 1–16, 2014. https://doi.org/10.1016/j.ejor.2013.09.017

Second-order worst-case complexity of cubic regularisation

Unconstrained minimization of a smooth nonconvex function $f:\mathbb R^n\to\mathbb R$ is the core subproblem of most nonlinear optimization software. Methods that only drive the gradient to zero may stall at saddle points, so a second-order guarantee (approximately nonnegative curvature) is the natural target for nonconvex problems. Worst-case evaluation complexity, meaning the number of function and derivative evaluations needed to reach a prescribed accuracy, is the standard way to compare such methods.

Timeline:

• 1981. Griewank, in an unpublished report, proposed globally minimizing a cubic regularisation of the second-order Taylor model to obtain an affine-invariant Newton method converging to second-order critical points.
• 2006. Nesterov and Polyak (Math. Program. 108) proved that, when the Hessian is globally Lipschitz and the step is the exact global minimizer of the cubic model with the exact Hessian, their method reaches approximate first-order criticality in $O(\epsilon^{-3/2})$ iterations and approximate second-order criticality in $O(\epsilon^{-3})$.
• 2009–2011. Cartis, Gould and Toint introduced the Adaptive Regularisation with Cubics (ARC) framework (Part I, Math. Program. 127). It uses an adaptive weight, an approximate Hessian and inexact subspace minimization. In Part II (Math. Program. 130) they proved that its second-order variant ARC(S) matches the Nesterov–Polyak orders under these weaker requirements.

This mission formalizes the second-order bound of Part II, Corollary 5.4.

Setting

Write $g(x)=\nabla f(x)$ and $H(x)=\nabla^2 f(x)$, and let $\|\cdot\|$ be the Euclidean norm. At iterate $x_k$, given a symmetric operator $B_k$ (an approximation of $H(x_k)$) and a weight $\sigma_k>0$, the cubic model is

$$m_k(s)=f(x_k)+s^\top g_k+\tfrac12 s^\top B_ks+\tfrac13\sigma_k\|s\|^3 .$$

Algorithm ARC computes a step $s_k$ that decreases $m_k$ at least as much as the best step along $-g_k$ (the Cauchy condition). It then forms the ratio $\rho_k=(f(x_k)-f(x_k+s_k))/(f(x_k)-m_k(s_k))$. If $\rho_k\ge\eta_1$ it accepts the step, $x_{k+1}=x_k+s_k$, and the iteration is successful; otherwise $x_{k+1}=x_k$. Finally it updates $\sigma_{k+1}$: it may shrink after a very successful step ($\rho_k>\eta_2$) and grows by a factor in $[\gamma_1,\gamma_2]$ after an unsuccessful one. The parameters satisfy $\gamma_2\ge\gamma_1>1$, $1>\eta_2\ge\eta_1>0$ and $\sigma_0>0$.

ARC(S) further requires

$$g_k^\top s_k+s_k^\top B_ks_k+\sigma_k\|s_k\|^3=0,\qquad s_k^\top B_ks_k+\sigma_k\|s_k\|^3\ge0,$$

and the inner termination rule TC.s, $\|\nabla_s m_k(s_k)\|\le\kappa_\theta\min(1,\|s_k\|)\|g_k\|$ with $\kappa_\theta\in(0,1)$. In Corollary 5.4 each step is moreover a global minimizer of $m_k$ over a subspace $\mathcal L_k$ spanned by the orthonormal columns of a matrix $Q_k$. The curvature measure is the leftmost eigenvalue

$$\lambda_k=\lambda_{\min}(Q_k^\top B_kQ_k)=\min\{v^\top B_kv: v\in\mathcal L_k,\ \|v\|=1\}.$$

The assumptions are:

• AF.3: $f\in C^2$;
• AF.4: $g$ is $\kappa_H$-Lipschitz on an open convex set containing the iterates;
• AF.6: $H$ is $L$-Lipschitz on $\mathbb R^n$;
• AM.4: $\|(H(x_k)-B_k)s_k\|\le C\|s_k\|^2$;
• $f(x_k)\ge f_{\rm low}$ for all $k$;
• $\sigma_k\ge\sigma_{\min}>0$ for all $k$;
• the standing assumption $m_k(s_k)<f(x_k)$ for every $k$ (the paper's (2.6)).

Formalization targets

Goal: Corollary 5.4

Let

$$L_0=\max\big(\sigma_0,\tfrac32\gamma_2(C+L)\big),\quad \alpha_{\rm curv}=\frac{\sigma_{\min}}{6L_0^3},\quad \kappa_{\rm curv}=\frac{f(x_0)-f_{\rm low}}{\eta_1\alpha_{\rm curv}},$$ $$\kappa^u_S=\frac{\log(L_0/\sigma_{\min})}{\log\gamma_1},\qquad \kappa^t_{\rm curv}=(1+\kappa^u_S)\kappa_{\rm curv}+\kappa^u_S .$$

For every $\epsilon>0$, the successful iterations with $-\lambda_k>\epsilon$ number at most

$$L^s_2=\lceil\kappa_{\rm curv}\epsilon^{-3}\rceil .$$

Some iterate $l$ has $-\lambda_l\le\epsilon$, and if $-\lambda_k>\epsilon$ for all $k\le j$, then at most $L^s_2$ of the iterations $0,\dots,j$ are successful. When $\epsilon\le1$, every such $j$ satisfies

$$j\le\lceil\kappa^t_{\rm curv}\epsilon^{-3}\rceil .$$

The constants are those printed in the paper.

Milestones

The milestones follow the paper's proof:

• Theorems 2.1 and 2.2 (generic counting bounds for ARC);
• Lemma 4.1 (properties of a subspace minimizer);
• Lemma 4.2 (model decrease $\tfrac16\sigma_k\|s_k\|^3$);
• Lemma 5.1 ($\sigma_k\le L_0$);
• the displays (5.28), (5.29), (5.30) and (5.32) from the proof of the corollary.

Significance

The corollary gives an explicit, dimension-free bound of order $\epsilon^{-3}$ on the number of iterations, and function evaluations, that a practical second-order method needs to reach approximate nonnegative curvature in its subspaces of minimization. The order is the one Nesterov and Polyak proved under much stronger requirements: exact Hessians and exact global minimization over $\mathbb R^n$. Taking $\mathcal L_k=\mathbb R^n$ and $B_k=H(x_k)$ recovers their second-order guarantee. Corollary 5.5 of the paper combines this bound with the first-order bound of Corollary 5.3 into a joint first- and second-order complexity bound.

All results here are proved in the paper (some by citation of Part I). None has a machine-checked proof. A formal development would supply:

• the counting arguments of §2;
• the characterization of global minimizers of a cubic model over a subspace (Lemma 4.1, whose proof is in Part I);
• the Taylor-type estimate that bounds $\sigma_k$ (Lemma 5.1).

The neighbouring missions of this series formalize the first-order bounds (Corollaries 3.4 and 5.3).

Difficulty

The counting arguments are elementary once the per-iteration estimates are available. The substantial step is Lemma 4.1. Global minimality over a subspace must be turned into the identity (4.1), the inequality (4.2) and positive semidefiniteness of $Q_k^\top B_kQ_k+\sigma_k\|s_k\|I$. First-order stationarity of the reduced model gives only (4.1); the semidefiniteness needs the global characterization of minimizers of a nonconvex cubic, which a local second-order condition does not provide. Lemma 5.1 needs a third-order Taylor remainder bound under a Lipschitz Hessian. A second point of care is the bookkeeping between $\sigma_k$ and $\sigma_{k+1}$ in Theorem 2.1, where the printed hypothesis is one index short (see below).

Formalization scope

• The space is $\mathbb R^n$ as EuclideanSpace ℝ (Fin n). The gradient is Mathlib's gradient, the Hessian is fderiv ℝ (gradient f), and $B_k$ are self-adjoint continuous linear operators with the operator norm.
• The algorithm is a predicate on sequences $(x_k,s_k,\sigma_k,B_k)$, not a function, because the step and the new weight are choices. The Cauchy condition is stated as $m_k(s_k)\le m_k(-\alpha g_k)$ for all $\alpha\ge0$. Successful means $\rho_k\ge\eta_1$, and the counts are cardinalities of filtered ranges.
• $\lambda_{\min}(Q_k^\top B_kQ_k)$ is the Rayleigh-quotient infimum of $B_k$ over unit vectors of $\mathcal L_k$, never the eigenvalue of $B_k$ on all of $\mathbb R^n$; for $\mathcal L_k=\{0\}$ Lean's empty infimum is $0$. The subspace minimizer condition is $s_k\in\mathcal L_k$ with $m_k(s_k)\le m_k(t)$ for all $t\in\mathcal L_k$, and it is stated in addition to the ARC(S) conditions.
• (2.6) is a hypothesis for every $k$; the paper assumes it "unless the algorithm terminates". Lean's $x/0=0$ would otherwise classify a zero predicted decrease as unsuccessful.
• "Takes at most $N$ iterations to reach $-\lambda_{l_2+1}\le\epsilon$" is stated as: every $j$ with $-\lambda_k>\epsilon$ for all $k\le j$ satisfies the bound; the existence of a first iterate with $-\lambda_{l_2+1}\le\epsilon$, which the corollary asserts, is stated separately. The total count is stated as finiteness of the set together with a bound on its cardinality.
• Correction. Theorem 2.1 is stated with $\sigma_k\le\bar\sigma$ for $k\le j+1$ instead of the printed $k\le j$. The printed version fails for $j=0$ when iteration $0$ is unsuccessful and $\bar\sigma=\sigma_0$.
• A formalization in which the subspace measure is replaced by $\lambda_{\min}(B_k)$, the subspace minimizer condition is dropped, or (2.6) is weakened to a vacuous hypothesis does not count as this result; nor does one in which the constants are replaced by an existential.
• Contributions are welcome on any milestone. Lemmas 4.1, 4.2 and 5.1 are reusable for every cubic-regularisation development.

Selected references

• C. Cartis, N. I. M. Gould, Ph. L. Toint, Adaptive cubic regularisation methods for unconstrained optimization. Part II: worst-case function- and derivative-evaluation complexity, Math. Program. 130(2):295–319, 2011 (preprint rev. 15 Sep 2009). https://doi.org/10.1007/s10107-009-0337-y
• C. Cartis, N. I. M. Gould, Ph. L. Toint, Adaptive cubic regularisation methods for unconstrained optimization. Part I: motivation, convergence and numerical results, Math. Program. 127(2):245–295, 2011. https://doi.org/10.1007/s10107-009-0286-5
• Yu. Nesterov, B. T. Polyak, Cubic regularization of Newton method and its global performance, Math. Program. 108(1):177–205, 2006. https://doi.org/10.1007/s10107-006-0706-8
• A. Griewank, The modification of Newton's method for unconstrained optimization by bounding cubic terms, Technical Report NA/12, DAMTP, University of Cambridge, 1981.

Motivation

Second-order methods for smooth nonconvex minimization are used in practice because they converge in far fewer iterations than gradient descent, yet for a long time their worst-case guarantee from an arbitrary starting point was no better than that of steepest descent. Nesterov and Polyak (Math. Program. 108, 2006) showed that adding a cubic term to Newton's quadratic model and minimizing that model globally at each step reaches a point with $\|\nabla f\|\le\epsilon$ in $O(\epsilon^{-3/2})$ iterations when the Hessian is Lipschitz, against $O(\epsilon^{-2})$ for steepest descent. Their analysis needs the exact Hessian and an exact global minimizer of a nonconvex model, both of which are too expensive in large-scale computation.

Cartis, Gould and Toint built the Adaptive Regularisation with Cubics (ARC) framework for that setting: the Hessian may be replaced by an approximation $B_k$, the regularisation weight is adapted without knowledge of a Lipschitz constant, and the step only approximately minimizes the model over a subspace (in practice a Krylov subspace generated by the Lanczos method). Part I (Math. Program. 127, 2011) proved convergence and fast local rates. Part II (Math. Program. 130, 2011), the source of this mission, proved that the practical variant ARC(S) keeps the $O(\epsilon^{-3/2})$ worst-case bound. Later work showed that this order is sharp for the method (Cartis, Gould & Toint, SIAM J. Optim. 2010) and cannot be improved by any method using derivatives up to second order (Carmon, Duchi, Hinder & Sidford, Math. Program. 2020).

Setting

Let $f:\mathbb R^n\to\mathbb R$ be twice continuously differentiable, with gradient $g=\nabla f$, Hessian $H=\nabla^2 f$, and Euclidean norm $\|\cdot\|$. At iterate $x_k$, with $g_k=g(x_k)$, a symmetric operator $B_k$ and a weight $\sigma_k>0$, the cubic model is

$$m_k(s)=f(x_k)+s^\top g_k+\tfrac12 s^\top B_k s+\tfrac13\sigma_k\|s\|^3 .$$

ARC (Algorithm 2.1) has parameters $\gamma_2\ge\gamma_1>1$, $1>\eta_2\ge\eta_1>0$ and $\sigma_0>0$. At each iteration it:

1. chooses a step $s_k$ with $m_k(s_k)\le m_k(-\alpha g_k)$ for every $\alpha\ge0$ (the Cauchy condition);
2. computes $\rho_k=\dfrac{f(x_k)-f(x_k+s_k)}{f(x_k)-m_k(s_k)}$;
3. accepts the step ($x_{k+1}=x_k+s_k$) if $\rho_k\ge\eta_1$, and otherwise sets $x_{k+1}=x_k$;
4. picks $\sigma_{k+1}$ in $(0,\sigma_k]$, $[\sigma_k,\gamma_1\sigma_k]$ or $[\gamma_1\sigma_k,\gamma_2\sigma_k]$ according as $\rho_k>\eta_2$, $\eta_1\le\rho_k\le\eta_2$ or $\rho_k<\eta_1$.

Iterations with $\rho_k\ge\eta_1$ are successful. $\mathcal S_j$ and $\mathcal U_j$ are the successful and unsuccessful iterations $k\le j$.

ARC(S) (Algorithm 4.1) additionally requires each step to satisfy

• $g_k^\top s_k+s_k^\top B_ks_k+\sigma_k\|s_k\|^3=0$ (4.1);
• $s_k^\top B_ks_k+\sigma_k\|s_k\|^3\ge0$ (4.2);
• the termination rule TC.s: $\|g_k+B_ks_k+\sigma_k\|s_k\|s_k\|\le\kappa_\theta\min(1,\|s_k\|)\,\|g_k\|$, with $\kappa_\theta\in(0,1)$.

The assumptions are:

• AF.4: $g$ is $\kappa_H$-Lipschitz on an open convex set containing the iterates, $\kappa_H\ge1$;
• AF.6: $H$ is $L$-Lipschitz on $\mathbb R^n$, $L>0$;
• AM.4: $\|(H(x_k)-B_k)s_k\|\le C\|s_k\|^2$, $C>0$;
• (2.11): $\sigma_k\ge\sigma_{\min}>0$;
• (2.6): $m_k(s_k)<f(x_k)$ for every $k$;
• $f(x_k)\ge f_{\rm low}$ for every $k$.

Formalization targets

Goal: Corollary 5.3

With $L_0=\max(\sigma_0,\tfrac32\gamma_2(C+L))$, $\kappa_g=\sqrt{(1-\kappa_\theta)/(\tfrac12L+C+L_0+\kappa_\theta\kappa_H)}$, $\alpha_S=\sigma_{\min}\kappa_g^3/6$, $\kappa^s_S=(f(x_0)-f_{\rm low})/(\eta_1\alpha_S)$, $\kappa^u_S=\log(L_0/\sigma_{\min})/\log\gamma_1$ and $\kappa_S=(1+\kappa^u_S)(2+\kappa^s_S)$, the corollary has three parts:

1. at most $\lceil\kappa^s_S\epsilon^{-3/2}\rceil$ successful iterations have $\min(\|g_k\|,\|g_{k+1}\|)>\epsilon$;
2. if $\|g_0\|,\|g_1\|>\epsilon$, at most $\lceil\kappa^s_S\epsilon^{-3/2}\rceil+1$ successful iterations precede the first $l_1$ with $\|g_{l_1+1}\|\le\epsilon$;
3. if moreover $\epsilon\le1$, then

$$l_1\le\left\lceil\kappa_S\,\epsilon^{-3/2}\right\rceil .$$

Milestones

The milestones follow the proof:

• Theorem 2.1, (2.13) and (2.14): unsuccessful iterations bounded by successful ones;
• Theorem 2.2: a uniform model decrease bounds the number of successful iterations;
• Lemma 4.2: $f(x_k)-m_k(s_k)\ge\tfrac16\sigma_k\|s_k\|^3$;
• Lemma 5.1: $\sigma_k\le L_0$;
• Lemma 5.2: $\|s_k\|\ge\kappa_g\sqrt{\|g_{k+1}\|}$ on successful iterations;
• the displayed steps (5.20), (5.22) and (5.23) of the corollary's proof.

Significance

The corollary shows that inexact subspace minimization and approximate Hessians cost nothing in worst-case order. The bound is the same $O(\epsilon^{-3/2})$ count of iterations, function evaluations and gradient evaluations as for the exact cubic-regularised Newton method. It is the founding result of the evaluation-complexity theory of adaptive regularisation methods, and later results build on it: higher-order regularisation, constrained and stochastic variants, and the lower bounds showing that $\epsilon^{-3/2}$ is optimal for second-order methods.

The result is proved on paper; to the knowledge of this mission it has no machine-checked proof. Formalizing it fixes the exact hypotheses: the standing assumption (2.6), the Lipschitz set in AF.4, and the off-by-one in Theorem 2.1. It also yields reusable Lean statements of the counting arguments (Theorems 2.1 and 2.2) shared by every trust-region and adaptive-regularisation complexity proof.

Difficulty

The first idea is to bound the model decrease by $\epsilon^{3/2}$ directly from $\|g_k\|>\epsilon$. That fails: TC.s and the Taylor estimates bound the step length by the gradient at the next iterate, $\|g_{k+1}\|$, not by $\|g_k\|$. The count must therefore use $\min(\|g_k\|,\|g_{k+1}\|)$, and turning it into a bound on the first $l_1$ with $\|g_{l_1+1}\|\le\epsilon$ needs care at the last iteration. The constant $\kappa_g$ combines four sources of error: the Hessian approximation, the Lipschitz Hessian, the bound on $\sigma_k$, and the inexact model gradient. The bound on $\sigma_k$ itself (Lemma 5.1) needs a second-order Taylor estimate of $f$ along the step. Unsuccessful iterations do not decrease $f$ and are counted separately through the growth of $\sigma_k$.

Formalization scope

The Lean development uses the following conventions:

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n), $g$ is gradient f and $H$ is fderiv ℝ (gradient f);
• $B_k$ is a continuous linear operator with IsSelfAdjoint, and operator norms are Mathlib's;
• runs of ARC and ARC(S) are predicates on the sequences $x,s,\sigma,B$, because the step and the new weight are choices;
• the Cauchy condition is stated as $m_k(s_k)\le m_k(-\alpha g_k)$ for all $\alpha\ge0$;
• TC.s uses the explicit model gradient $g_k+B_ks_k+\sigma_k\|s_k\|s_k$;
• powers $\epsilon^{\pm3/2}$ are real powers and ceilings are integer ceilings.

Hypotheses and quantifiers:

• (2.6) is a hypothesis for every $k$, the paper's standing assumption for ARC(S) (p. 12). It also rules out the junk value $\rho_k=0$ that Lean's division by zero would give.
• "At most $N$ iterations before $\|g_{l_1+1}\|\le\epsilon$" is stated as: every $j$ with $\|g_k\|>\epsilon$ for all $k\le j$ satisfies $j\le N$. This also asserts that $l_1$ exists.
• Theorem 2.1 is posed with $\sigma_k\le\bar\sigma$ for $k\le j+1$: the printed range $k\le j$ makes it false at $j=0$.

The constants are written out exactly as printed; replacing them with "there is a constant" would trivialize the goal and is excluded. Contributions are welcome:

• Taylor estimates under a Lipschitz Hessian on EuclideanSpace;
• a general counting lemma behind Theorems 2.1–2.2.

Both are reusable well beyond this mission.

Selected references

• C. Cartis, N. I. M. Gould, Ph. L. Toint, Adaptive cubic regularisation methods for unconstrained optimization. Part II: worst-case function- and derivative-evaluation complexity, Math. Program. 130(2):295–319, 2011 (preprint rev. 15 Sep 2009). https://doi.org/10.1007/s10107-009-0337-y
• C. Cartis, N. I. M. Gould, Ph. L. Toint, Adaptive cubic regularisation methods for unconstrained optimization. Part I: motivation, convergence and numerical results, Math. Program. 127(2):245–295, 2011. https://doi.org/10.1007/s10107-009-0286-5
• C. Cartis, N. I. M. Gould, Ph. L. Toint, On the complexity of steepest descent, Newton's and regularized Newton's methods for nonconvex unconstrained optimization problems, SIAM J. Optim. 20(6):2833–2852, 2010. https://doi.org/10.1137/090774100
• Y. Carmon, J. C. Duchi, O. Hinder, A. Sidford, Lower bounds for finding stationary points I, Math. Program. 184:71–120, 2020. https://doi.org/10.1007/s10107-019-01406-y
• Yu. Nesterov, B. T. Polyak, Cubic regularization of Newton method and its global performance, Math. Program. 108(1):177–205, 2006. https://doi.org/10.1007/s10107-006-0706-8

Motivation

Many stochastic dynamic programs in operations research, such as inventory control with partially observed demand or the pricing of American options, are too large to solve exactly. A heuristic policy gives a lower bound on the optimal expected reward; to judge whether it is good enough one needs an upper bound. Brown, Smith and Sun (Oper. Res. 2010) build such bounds by information relaxation: let the decision maker see more than she would in reality, and charge a penalty for using the extra information. The construction generalizes the martingale duality for optimal stopping of Haugh and Kogan (Oper. Res. 2004), Rogers (Math. Finance 2002) and Andersen and Broadie (Manage. Sci. 2004).

In applications, the analyst chooses both the relaxation and the penalty, trading the quality of the bound against the cost of computing it. Proposition 2.3 of the paper collects four properties that govern this choice. The first is the subject of this mission.

Setting

Uncertainty is a probability space $(\Omega,\mathcal F,\mathbb P)$, and decisions are made in periods $t=0,\dots,T$. The natural filtration $\mathbb F=(\mathcal F_0,\dots,\mathcal F_T)$ records what is known in each period, with $\mathcal F_0=\{\emptyset,\Omega\}$. An action sequence is $a=(a_0,\dots,a_T)$, chosen from feasible sets $A_t(a_0,\dots,a_{t-1})$. Period rewards $r_t(a_0,\dots,a_t)$ are $\mathcal F_t$-measurable random variables and the total reward is $r(a)=\sum_t r_t(a)$.

A policy is a map $\alpha:\Omega\to A$ from outcomes to feasible action sequences. It is adapted to a filtration $\mathbb G$ if the period-$t$ action is $\mathcal G_t$-measurable; $\mathcal A_{\mathbb G}$ denotes these policies. A filtration $\mathbb G$ with $\mathcal F_t\subseteq\mathcal G_t\subseteq\mathcal F$ for all $t$ is a relaxation of $\mathbb F$, written $\mathbb F\subseteq\mathbb G$. A penalty is a function $z(a,\omega)$; it is dual feasible if $\mathbb E[z(\alpha_F)]\le0$ for every $\alpha_F\in\mathcal A_{\mathbb F}$. For any relaxation $\mathbb G$ and dual feasible $z$, the dual bound

$$\sup_{\alpha_G\in\mathcal A_{\mathbb G}}\mathbb E\big[r(\alpha_G)-z(\alpha_G)\big]$$

is at least the optimal value $\sup_{\alpha_F\in\mathcal A_{\mathbb F}}\mathbb E[r(\alpha_F)]$ (weak duality, Lemma 2.1).

The paper's main source of penalties is Proposition 2.2. Given generating functions $w_t(a)$ depending only on $a_0,\dots,a_t$, set

$$z_t(a)=\mathbb E[w_t(a)\mid\mathcal G_t]-\mathbb E[w_t(a)\mid\mathcal F_t],\qquad z(a)=\sum_{t=0}^T z_t(a).$$

Such a penalty has zero mean along every nonanticipative policy, and its dual bound is computed by the backward recursion (10), the Bellman recursion with rewards $r_t-z_t$ and conditional expectations given $\mathcal G_t$.

Formalization targets

Goal: Proposition 2.3(i)

For filtrations $\mathbb F\subseteq\mathbb G^1\subseteq\mathbb G^2$ and one common sequence of generating functions $(w_0,\dots,w_T)$, let $z^i$ be the Proposition 2.2 penalty of $(\mathbb G^i,w)$. Then

$$\sup_{\alpha_G\in\mathcal A_{\mathbb G^1}}\mathbb E\big[r(\alpha_G)-z^1(\alpha_G)\big]\le\sup_{\alpha_G\in\mathcal A_{\mathbb G^2}}\mathbb E\big[r(\alpha_G)-z^2(\alpha_G)\big].\qquad(12)$$

With a common generating function, a looser relaxation gives a weaker bound.

Milestones

1. Equation (10). For a Proposition 2.2 penalty under a relaxation $\mathbb G$, the expectation of the initial dual value function $V^{\mathbb G}_0$ equals the dual bound.
2. Proposition 2.3(ii). For dual feasible $z^1,z^2$ and one relaxation $\mathbb G$, the difference of the two dual bounds lies between $\inf_{\alpha_G}\mathbb E[z^2(\alpha_G)-z^1(\alpha_G)]$ and $\sup_{\alpha_G}\mathbb E[z^2(\alpha_G)-z^1(\alpha_G)]$, eq. (13).
3. Proposition 2.3(iii). For $\mathbb F\subseteq\mathbb F'\subseteq\mathbb G$, the penalty $z_t(a)=\mathbb E[w_t(a)\mid\mathcal G_t]-\mathbb E[w_t(a)\mid\mathcal F'_t]$ still satisfies the conclusions of Proposition 2.2.
4. Proposition 2.3(iv). If $\hat z_t(a)$ are unbiased estimates of the terms $z_t(a)$ of a dual feasible penalty, $\mathbb E[\hat z_t(a)\mid\mathcal G_t]=z_t(a)$, and the relaxation $\widehat{\mathbb G}$ additionally reveals the estimates, then the dual bound of $(\mathbb G,z)$ is at most that of $(\widehat{\mathbb G},\hat z)$, eq. (14).

Milestone 1 is on the goal's path; milestones 2–4 are the remaining parts of the same proposition.

Significance

Proposition 2.3(i) tells the analyst how to read a weak bound. If a cheap generating function (for instance $w_t=0$, the zero penalty) gives a satisfactory bound under some relaxation, it will give a bound at least as tight under any less informative relaxation that still contains $\mathbb F$; conversely, moving to a looser relaxation without improving the generating function can only weaken the bound. Part (ii) is a continuity statement: penalties close to the ideal penalty give bounds close to the optimal value. Part (iii) permits the subtracted conditional expectation to be computed under an intermediate filtration, which the paper uses when volatility is unobserved in its option-pricing example. Part (iv) is the justification for estimating penalties by nested simulation, as in the methods of Haugh–Kogan and Andersen–Broadie: unbiased estimates yield valid, if weaker, upper bounds.

The results are proved in the paper's electronic companion. To our knowledge none of them, nor the information-relaxation duality framework itself, has a machine-checked proof. Formalizing them requires a usable theory of policies adapted to a filtration, penalties evaluated along random action sequences, and backward recursions with conditional expectations, all of which are reusable for other duality results in stochastic dynamic programming.

Difficulty

The obvious argument for (12) compares the two suprema policy by policy: $\mathcal A_{\mathbb G^1}\subseteq\mathcal A_{\mathbb G^2}$. This fails, because the two bounds use different penalties: for a fixed $\mathbb G^1$-adapted policy, $\mathbb E[z^1(\alpha)]$ and $\mathbb E[z^2(\alpha)]$ need not agree, so the larger policy set alone does not order the bounds. The penalty changes with the relaxation exactly so as to remove part of the value of the extra information, and the statement asserts that it never removes more than that information is worth. Even the representation (10) of a dual bound by a backward recursion is nontrivial: it requires near-optimal actions to be selected measurably in every period.

In Lean, the further difficulty is the composition of an action-indexed family of conditional expectations with a random action: $\omega\mapsto z_t(\alpha(\omega))(\omega)$, where each $z_t(a)$ is only defined almost surely. Countability of the action set is what makes this composite well defined up to null sets.

Formalization scope

Periods are Fin (T + 1); an action sequence is a function Fin (T + 1) → X for one countable action type X with the discrete σ-algebra (the disjoint union of the per-period action sets). Filtrations are Mathlib Filtrations of the ambient σ-algebra; a relaxation is 𝔽 ≤ 𝔾. Policies are maps Ω → (Fin (T + 1) → X) with values in the feasible set, adapted when each action is measurable for the corresponding σ-algebra. Conditional expectations are Mathlib's μ[f | m], so identities between them hold almost surely. Dual bounds are suprema in EReal over the adapted policy sets, so an infinite bound is represented and no junk value $0$ arises from an unbounded supremum.

Pinned regularity, beyond the paper's text: period rewards and generating functions are uniformly bounded (almost surely for the latter) and measurable, so that every expectation exists; in part (iv), the estimates are measurable and uniformly bounded. In part (ii), the difference of two dual bounds is taken in EReal, and the case where both bounds are $+\infty$ (where the page's difference is undefined) is excluded.

The penalties $z^1,z^2$ of the goal are computed from $w$ by the formula of Proposition 2.2; stating the goal for arbitrary penalties with Proposition 2.2's properties would be a different and false claim. Likewise $\widehat{\mathbb G}$ in part (iv) is constructed from $\mathbb G$ and the estimates.

The definitions duplicate those of mission 1 of this series (the framework, the recursive model, the penalty construction); they are expected to be merged. Contributions of reusable lemmas about adapted policies over countable action sets and about backward recursions with conditional expectations are welcome.

Selected references

• D. B. Brown, J. E. Smith, P. Sun, Information Relaxations and Duality in Stochastic Dynamic Programs, Operations Research, Articles in Advance, 2010. https://doi.org/10.1287/opre.1090.0796
• M. B. Haugh, L. Kogan, Pricing American Options: A Duality Approach, Operations Research 52(2), 2004. https://doi.org/10.1287/opre.1030.0070
• L. Andersen, M. Broadie, Primal-Dual Simulation Algorithm for Pricing Multidimensional American Options, Management Science 50(9), 2004. https://doi.org/10.1287/mnsc.1040.0258
• L. C. G. Rogers, Monte Carlo Valuation of American Options, Mathematical Finance 12(3), 2002. https://doi.org/10.1111/1467-9965.02010

Motivation

Bounded-confidence models describe a population of agents who repeatedly average their opinions with those of agents whose opinions are close to their own. They are used to study consensus and polarization in opinion formation, and in control as a primitive for decentralized rendezvous of mobile agents. Simulations of these models show a robust phenomenon: opinions converge to clusters, and the distances between clusters are typically close to twice the confidence radius rather than just above it. For finitely many agents this regularity has resisted proof.

V. D. Blondel, J. M. Hendrickx and J. N. Tsitsiklis (SIAM J. Control Optim. 48 (2010) 5214–5240) study a continuous-time version of the model in two forms: with $n$ discrete agents, and with a continuum of agents indexed by $[0,1]$. For the continuum they prove that regular initial opinions converge to clusters whose separation obeys a lower bound depending on the cluster weights. To transfer such conclusions to finitely many agents one needs to know that the $n$-agent model is close to the continuum model when $n$ is large. Section 4 of the paper proves this on every finite time horizon. This mission formalizes that result.

Setting

Discrete agents. There are $n\ge1$ agents with real opinions $\xi_i(t)$, $t\ge0$. Agents $i$ and $j$ interact when $|\xi_i-\xi_j|<1$. A solution of (2.1) is a continuous $\xi:[0,\infty)\to\mathbb R^n$ with

$$\xi_i(t)=\xi_i(0)+\int_0^t\sum_{j:\,|\xi_i(\tau)-\xi_j(\tau)|<1}\bigl(\xi_j(\tau)-\xi_i(\tau)\bigr)\,d\tau$$

for all $t\ge0$ and all $i$. The right-hand side is discontinuous when the interaction graph changes, so the integral form is used. A solution is proper if it is the unique solution from its initial value, its non-differentiability times have no accumulation point, and two agents that meet stay together.

Continuum agents. Agents are indexed by $\alpha\in I=[0,1]$ with Lebesgue measure. $Y$ is the set of bounded measurable functions $I\to\mathbb R$. For $m,M>0$, $X_m^M$ is the set of nondecreasing $\tilde x$ with $m\le\frac{\tilde x(\beta)-\tilde x(\alpha)}{\beta-\alpha}\le M$ for $\beta\ne\alpha$; such $\tilde x$ are regular. The interaction operator is

$$\mathcal L(\tilde x)(\alpha)=\int_I \mathbf 1\bigl[|\tilde x(\alpha)-\tilde x(\gamma)|<1\bigr]\,\bigl(\tilde x(\gamma)-\tilde x(\alpha)\bigr)\,d\gamma ,$$

and a solution of (3.2) from $\tilde x_0$ is a measurable $x:(\alpha,t)\mapsto x_t(\alpha)$ with every $x_t\in Y$ and $x_t(\alpha)=\tilde x_0(\alpha)+\int_0^t\mathcal L(x_\tau)(\alpha)\,d\tau$ for all $t\ge0$ and all $\alpha\in I$.

The embedding. For $\xi\in\mathbb R^n$, $G(\xi)$ is the step function with $G(\xi)(\alpha)=\xi_i$ on $[\frac{i-1}n,\frac in)$ and $G(\xi)(1)=\xi_n$. It distributes the $n$ agents over $n$ blocks of $I$ of length $1/n$.

Formalization targets

Goal: Theorem 7 (finite-horizon approximation)

Let $\tilde x_0\in X_m^M$, $x$ the solution of (3.2) from $\tilde x_0$, and for each $n\ge1$ let $\xi^{\langle n\rangle}$ be a proper solution of (2.1) with nondecreasing $\xi^{\langle n\rangle}(0)$ and $\|G(\xi^{\langle n\rangle}(0))-\tilde x_0\|_\infty\to0$. Then for every $T$ and $\varepsilon>0$ there is $n'$ with

$$\bigl\|G\bigl(\xi^{\langle n\rangle}(t/n)\bigr)-x_t\bigr\|_\infty\le\varepsilon\qquad(t\in[0,T],\ n\ge n').$$

The statement fixes no rate in $n$ and no dependence of $n'$ on $T$; it asserts only uniform convergence on bounded time intervals.

Milestones

1. Lemma 1: for $\tilde x\in X_m$ and $\tilde y\in Y$, $\|\mathcal L(\tilde x)-\mathcal L(\tilde y)\|_\infty\le(2+8/m)\|\tilde x-\tilde y\|_\infty$.
2. Theorem 4, left inequality of (3.7): a solution from $\tilde x_0\in X_m^M$ satisfies $x_t(\beta)-x_t(\alpha)\ge m e^{-t}(\beta-\alpha)$ for all $t\ge0$, $\alpha<\beta$.
3. Proposition 4: for every $\varepsilon,T>0$ there is $\delta>0$ such that every solution $y$ of (3.2) with $\|y_0-\tilde x_0\|_\infty\le\delta$ satisfies $\|y_t-x_t\|_\infty\le\varepsilon$ on $[0,T]$.
4. Embedding (Section 4): if $\xi$ solves (2.1), then $(\alpha,t)\mapsto G(\xi(t/n))(\alpha)$ solves (3.2) from $G(\xi(0))$.

Significance

The theorem says that the continuum model is the large-population limit of the $n$-agent model over any fixed time window. Combined with the paper's continuum convergence result (Theorem 6), it supports the paper's Conjecture 1 on intercluster distances for finitely many agents, and it is the first step of the paper's Proposition 5, which derives Conjecture 1 for random initial opinions from a stability conjecture for the continuum. It is a mean-field limit for a model whose interaction kernel is discontinuous, where standard Lipschitz mean-field arguments do not apply directly.

All four results and the goal are proved in the paper (with the time-scale correction described below). None of them has a machine-checked proof that this mission is aware of. The formalization contributes a checked continuous-dependence estimate for a discontinuous integral equation, a checked statement that the finite-agent dynamics embed in the continuum dynamics, and a precise record of the time normalization under which the two models agree.

Difficulty

The operator $\mathcal L$ is not Lipschitz on $Y$: moving one opinion across the confidence threshold changes the interaction set discontinuously. The obvious Gronwall argument for continuous dependence therefore fails for two arbitrary solutions. It works only around a trajectory that stays in some $X_{m'}$, where few agents sit near the threshold, which is why the lower slope bound must hold at every time and not only at time $0$. The perturbed trajectory, coming from $n$ agents, is a step function and is never regular, so the estimate must be one-sided in this sense.

A literal reading of the page also fails. The page writes $G(\xi^{\langle n\rangle}(t))$, but for $\alpha$ in block $i$ the continuum interaction $\mathcal L(G(\xi))(\alpha)$ equals $\frac1n$ times the discrete right-hand side of (2.1). With $\tilde x_0(\alpha)=\alpha/2$ and $\xi^{\langle n\rangle}_i(0)=\tilde x_0(i/n)$, both models are linear; at $t=1$ the sup distance between $G(\xi^{\langle n\rangle}(1))$ and $x_1$ tends to $e^{-1}/4$. The discrete time must be rescaled by $1/n$.

Formalization scope

Namespace BHTOpinion.Approx. Agents of the discrete model are Fin n (0-based); the continuum index set is Set.Icc (0:ℝ) 1 with Lebesgue measure. Opinion functions are ℝ → ℝ, of which only the values on $I$ matter; trajectories are written x t α, time first, with time in ℝ and explicit $t\ge0$ guards. In 0-based form, $G(\xi)(\alpha)=\xi_{\min(\lfloor n\alpha\rfloor,n-1)}$ on $I$; for $n=0$ the definition returns $0$, and every statement assumes $n\ge1$.

Explicit readings of the paper's phrases:

• Sup norms are written pointwise over $I$, including $\alpha=1$: a bound at every $\alpha\in I$, never a real supremum.
• "$\lim_{n\to\infty}\|G(\xi^{\langle n\rangle}(0))-\tilde x_0\|_\infty=0$" is: for every $\delta>0$ there is $N$ such that the pointwise bound $\delta$ holds for all $n\ge N$.
• "There exists $n'$" is an explicit $\exists\,n'$ with the bound for all $n\ge n'$, $t\in[0,T]$, $\alpha\in I$.
• "The solution $x$" of (3.2) is any solution from $\tilde x_0$; the theorem holds for each.
• "Proper initial condition, admitting a unique solution" is kept as printed: uniqueness from $\xi^{\langle n\rangle}(0)$, finitely many non-differentiability times on every bounded interval, agents that meet stay together.
• Solutions of (2.1) and (3.2) require the time integrand to be integrable; Lean's integral of a non-integrable function is $0$.
• The labelled correction: the discrete trajectory enters as $\xi^{\langle n\rangle}(t/n)$ in the embedding claim and in Theorem 7. Equivalently, the page's statement holds for the weighted model (2.4) with weights $1/n$; only the rescaled form is stated.
• Only the left inequality of (3.7) is a milestone. The right inequality $Me^{4t/m}$ is not used by Section 4.

A trivializing formalization is ruled out: the hypotheses are satisfied by $\tilde x_0(\alpha)=\alpha\in X_1^1$, the conclusion is not vacuous because $G$ is evaluated at $n\ge1$ only, and the perturbed initial values $y_0$ in Proposition 4 range over all of $Y$, not over regular functions.

Infrastructure needed: Gronwall's inequality for a sup-norm difference, measure-theoretic bookkeeping for $\mathcal L$ on step functions, and a change of variables $\tau\mapsto\tau/n$ in interval integrals. The Lipschitz estimate on $X_m$ and the slope bound are reusable for any continuum bounded-confidence model. Contributions to any milestone are welcome; the embedding milestone is independent of the other three.

Selected references

• V. D. Blondel, J. M. Hendrickx, J. N. Tsitsiklis, Continuous-time average-preserving opinion dynamics with opinion-dependent communications, SIAM J. Control Optim. 48(8), 2010, 5214–5240. https://doi.org/10.1137/090766188

Motivation

In many production and service settings a single resource is shared by several parties, each judging the outcome only by how its own work is treated. Multi-agent scheduling studies this situation. Agnetis, Mirchandani, Pacciarelli and Pacifici (Oper. Res. 52(2), 2004) introduced the two-agent single-machine model in which two agents, A and B, each own a set of jobs and each minimize their own objective. Their paper treats two questions: the constrained problem, minimizing A's objective subject to a bound on B's, and the Pareto problem, describing every schedule that cannot be improved for one agent without hurting the other.

For the Pareto problem the first quantity of interest is the number of distinct trade-offs, because the natural way to compute the whole front is to solve the constrained problem repeatedly with a decreasing bound (the paper's scheme PP, Figure 4, p. 239). Enumeration of this kind is polynomial exactly when the number of nondominated pairs is polynomially bounded. This mission formalizes the paper's bound for the case where both agents minimize a maximum of regular cost functions (§11.1, pp. 239–240).

Setting

Agent A owns the jobs $J^A_1,\dots,J^A_{n_A}$ and agent B owns $J^B_1,\dots,J^B_{n_B}$, with $n_A,n_B\ge1$. Every job $j$ has a processing time $p_j\ge0$. All jobs are available at time $0$. A schedule $\sigma$ is an ordering of all $n_A+n_B$ jobs; the machine processes them in that order from time $0$ without idle time, so the completion time $C_j(\sigma)$ of a job is the sum of the processing times of the jobs up to and including it.

Each A-job carries a cost function $f^A_h:\mathbb R\to\mathbb R$ and each B-job a cost function $f^B_k$, all nondecreasing (regular). The agents' objectives are the maximum costs

$$f^A_{\max}(\sigma)=\max_{h} f^A_h\big(C^A_h(\sigma)\big),\qquad f^B_{\max}(\sigma)=\max_{k} f^B_k\big(C^B_k(\sigma)\big).$$

This covers the makespan and maximum lateness of each agent as special cases.

A schedule $\sigma$ is nondominated if no schedule $\bar\sigma$ satisfies $f^A_{\max}(\bar\sigma)\le f^A_{\max}(\sigma)$ and $f^B_{\max}(\bar\sigma)\le f^B_{\max}(\sigma)$ with at least one inequality strict. The pair $(y^A,y^B)=(f^A_{\max}(\sigma),f^B_{\max}(\sigma))$ of a nondominated schedule is a nondominated pair, and the schedule corresponds to that pair. Write $\mathcal N$ for the set of nondominated pairs. Different nondominated schedules can share a pair; the problem $1\|f^A_{\max}\circ f^B_{\max}$ asks for $\mathcal N$, with one schedule per pair. Job $a$ precedes job $b$ in $\sigma$ if $a$ comes before $b$ in the ordering.

Formalization targets

Goal: Theorem 11.3, corrected (p. 240)

$$|\mathcal N|\le n_A\,n_B+1 .$$

The paper prints the bound $n_An_B$. It is off by one: with $n_A=n_B=1$, unit processing times and $f^A(t)=f^B(t)=t$, the schedules AB and BA give the two nondominated pairs $(1,2)$ and $(2,1)$. The goal states $n_An_B+1$, the bound the printed argument supports once the first schedule is counted.

Milestones

1. Lemma 11.1 (p. 239). For nondominated pairs $(y^A,y^B)$, $(\tilde y^A,\tilde y^B)$ with $y^A<\tilde y^A$ and $y^B>\tilde y^B$ and for a fixed A-job $J^A_h$ and B-job $J^B_k$, there are corresponding nondominated schedules $\sigma,\tilde\sigma$ such that if $J^B_k$ precedes $J^A_h$ in $\sigma$, it does so in $\tilde\sigma$.
2. Lemma 11.2 (p. 240). The same, with one pair $\sigma,\tilde\sigma$ serving every A-job and every B-job at once.
3. The exchange claim (proof of Theorem 11.3, p. 240). Two nondominated schedules $\sigma,\tilde\sigma$ with $f^A_{\max}(\sigma)<f^A_{\max}(\tilde\sigma)$ and $f^B_{\max}(\tilde\sigma)<f^B_{\max}(\sigma)$ differ in the relative order of at least one A-job and one B-job: some $J^A_h$ precedes some $J^B_k$ in $\sigma$, and $J^B_k$ precedes $J^A_h$ in $\tilde\sigma$.

Significance

The bound places $1\|f^A_{\max}\circ f^B_{\max}$ among the two-agent problems whose Pareto front has polynomially many points. Combined with the polynomial algorithm for the constrained problem $1\|f^A_{\max}:f^B_{\max}\le Q$ (Theorem 4.1 of the same paper), it means the full front can be listed with polynomially many constrained solves. The structural content is an order statement: as the bound on agent B tightens along the front, B-jobs overtake A-jobs and never fall back, so each of the $n_An_B$ (A-job, B-job) pairs changes order at most once. The same question for other pairs of objectives is the subject of later work on multi-agent scheduling, collected in the monograph of Agnetis, Billaut, Gawiejnowicz, Pacciarelli and Soukhal (Springer 2014).

The result is published but, to our knowledge, has no machine-checked proof. Formalizing it also fixes the printed off-by-one error in the statement. The overtaking lemmas are of independent use for other pairs of regular min-max objectives.

Difficulty

The obvious argument walks along the front and charges each step to one (A-job, B-job) pair that changes order. Two things must be secured. First, the charged pair must change order in a consistent direction; schedules corresponding to a pair are not unique, and nothing forces two arbitrary representatives of different pairs to agree on the order of the jobs they do not charge. Lemma 11.2 asserts that representatives can be chosen so that no B-job falls back behind an A-job, and establishing it requires control over every job pair simultaneously, not one at a time as in Lemma 11.1. Second, a step must change at least one order. The tempting proof looks at a B-job attaining $y^B$ and argues that the jobs it overtakes include an A-job; this fails for an arbitrary choice of that B-job, since another B-job with a flatter cost function can be the one that moves. Finally, the count of reversals bounds the number of steps, not the number of pairs; the first pair has to be added.

Formalization scope

Jobs are Fin nA ⊕ Fin nB (Sum.inl h is $J^A_{h+1}$, Sum.inr k is $J^B_{k+1}$, 0-based). A schedule is a duplicate-free list containing every job, and completion times are prefix sums of processing times; this is the published sequence model MooreLateJobs.Shared.completionTime (Moore 1968), reused as a reference item. Processing times are real and nonnegative; costs are real-valued and Monotone; $n_A,n_B\ge1$ so that both maxima exist. Nondominance compares against all schedules of all jobs. Precedence compares first positions in the list.

The count is over pairs, $\mathcal N\subseteq\mathbb R^2$, measured with Set.encard, so finiteness is part of the goal. Counting nondominated schedules instead would be a different and false statement: permuting jobs inside a block often leaves both maxima unchanged. The printed bound $n_An_B$ is replaced by $n_An_B+1$ and the reason is given in the goal's statement; stating a larger bound "to be safe" or the printed one would make the mission either weaker than the paper's argument or false. The scheme PP and the choice of $\epsilon$ in it are not formalized; they are the paper's computation device, not part of the theorem. In the exchange claim the paper's σ and σ̃ are schedules of consecutive pairs; the milestone states it for any two nondominated schedules with the two strict inequalities, which includes that case. Running times are not formalized.

A complete development needs elementary facts about completion times when one job is moved within a sequence, the simultaneous statement of Lemma 11.2, and a counting argument along the front. Contributions of reusable lemmas about job moves in the sequence model are welcome.

Selected references

• A. Agnetis, P. B. Mirchandani, D. Pacciarelli, A. Pacifici, Scheduling Problems with Two Competing Agents, Operations Research 52(2) (2004) 229–242. https://doi.org/10.1287/opre.1030.0092
• J. M. Moore, An n Job, One Machine Sequencing Algorithm for Minimizing the Number of Late Jobs, Management Science 15(1) (1968) 102–109. https://doi.org/10.1287/mnsc.15.1.102
• A. Agnetis, J.-C. Billaut, S. Gawiejnowicz, D. Pacciarelli, A. Soukhal, Multiagent Scheduling: Models and Algorithms, Springer, 2014. https://doi.org/10.1007/978-3-642-41880-8