Optimization

Why certify nonconvex scenario solutions

The scenario approach replaces an optimization problem with uncertain constraints $\theta\in\Theta_\delta$, $\delta\in\Delta$, by the program that enforces only $N$ constraints $\Theta_{\delta_1},\dots,\Theta_{\delta_N}$ drawn at random from the distribution $\mathbb P$ of the uncertainty. Its solution $\theta^*$ is then judged by its violation, the probability that a new instance $\delta$ is not satisfied. For convex programs in $\mathbb R^d$ the violation is controlled by the dimension $d$ alone (Calafiore and Campi 2006; Campi and Garatti 2008), because a convex program has at most $d$ support constraints. Many problems where the scenario approach is used in practice are not convex: control with quantized inputs, mixed-integer design, classification with nonconvex losses, and decisions over infinite-dimensional or unstructured sets. For those programs no a priori bound on the number of constraints that determine the solution exists.

Timeline, as recorded in Chapter 8 of Campi and Garatti's textbook:

• 2006–2008: the violation of convex scenario solutions is bounded, and then characterized exactly, in terms of $d$.
• 2018: the wait-and-judge theory (Campi and Garatti, Math. Programming 2018) evaluates the violation from the number of support constraints counted after solving the program; it extends to nonconvex programs but requires a nondegeneracy assumption.
• 2018: Campi, Garatti and Ramponi (IEEE TAC 2018) prove a bound in terms of the size of any support set, with no convexity and no nondegeneracy assumption. This is the result formalized here, stated in the book as Eq. (8.15).

Setting

Let $\Theta$ be a generic set; it may be an infinite-dimensional space or a set with no algebraic structure. Let $f:\Theta\to\mathbb R$ be a cost and $\Theta_\delta\subseteq\Theta$ constraint sets indexed by $\delta\in\Delta$, where $\Delta$ carries a probability $\mathbb P$. Neither $f$ nor the $\Theta_\delta$ is required to be convex. With a sample $\delta_1,\dots,\delta_N$ drawn independently from $\mathbb P$, the scenario program is

$$\min_{\theta\in\Theta} f(\theta)\quad\text{subject to}\quad \theta\in\bigcap_{i=1,\dots,N}\Theta_{\delta_i},\tag{8.12}$$

and $\theta^*$ denotes its solution, assumed to exist and be unique for every sample.

The violation of a decision is $V(\theta)=\mathbb P\{\delta\in\Delta:\theta\notin\Theta_\delta\}$ (Definition 3.1).

A support set (Definition 8.8) is a subset $\{\Theta_{\delta_{i_1}},\dots,\Theta_{\delta_{i_k}}\}$ of the constraints such that the program with only these constraints in place has the same solution $\theta^*$ as the program with all constraints. The full set of constraints is always a support set; a support set need not be minimal (of smallest cardinality) or irreducible (with no removable element). Let $\sigma^*$ be the cardinality of the support set returned, for every sample, by some fixed algorithm.

Formalization targets

Goal: the support-set bound, Eq. (8.15)

For every function $\epsilon:\{0,1,\dots,N\}\to[0,1]$ with $\epsilon(N)=1$,

$$\mathbb P^N\{V(\theta^*)>\epsilon(\sigma^*)\}\le\sum_{k=0}^{N-1}\binom Nk\,(1-\epsilon(k))^{N-k}.$$

The level function $\epsilon$ is free: the statement is one inequality per admissible $\epsilon$, and it holds for any algorithm producing support sets. This is the weakest form that carries the whole result.

Milestone: the level function for a confidence $\beta$, Eq. (8.16)

For $\beta\in[0,1]$ let

$$\epsilon(k)=\begin{cases}1 & k=N,\\ 1-\sqrt[N-k]{\dfrac{\beta}{N\binom Nk}} & \text{otherwise.}\end{cases}$$

The arithmetic half states that $\epsilon$ maps $\{0,\dots,N\}$ into $[0,1]$, $\epsilon(N)=1$, and the right-hand side of (8.15) equals $\beta$ (for $N\ge1$). The probabilistic half states $\mathbb P^N\{V(\theta^*)>\epsilon(\sigma^*)\}\le\beta$.

Significance

The result turns the size of a support set, a quantity observed after the program is solved, into a certificate on the violation of the solution, for any optimization or decision problem whose solution is determined by a subset of the data. With the choice (8.16), a user who finds a support set of size $\sigma^*$ can assert $V(\theta^*)\le\epsilon(\sigma^*)$ with confidence $1-\beta$. The book's Figure 8.12 shows that $\epsilon(k)$ for $\beta=10^{-6}$ remains well below $1$ for $k$ up to a sizeable fraction of $N$. Because the algorithm that finds the support set is arbitrary, cheap heuristics that return non-minimal support sets still give valid, if weaker, guarantees. The result does not recover the tight convex bound (3.4); for convex programs the Chapter 3 theory remains sharper.

The statement is proved in [31] and is the probabilistic core of the sample-compression arguments of learning theory (Floyd and Warmuth 1995) in the form used by the scenario approach. To the best of available knowledge it has no machine-checked proof. The platform's UnderstandingML.compression_bound proves a sample-compression bound for a fixed compression size with a different constant; it does not cover a data-dependent size $\sigma^*$ or an arbitrary level function. A formal proof here provides a reusable bound for data-dependent support sets over arbitrary decision sets.

Difficulty

The natural first step is: condition on the support set being a particular index set $I$ with $|I|=k$, and argue that the solution is then a function of the $k$ sampled constraints in $I$ alone, while the other $N-k$ samples are independent of it and must all be satisfied. The difficulty is that the event "the algorithm returns $I$" depends on all $N$ samples, and the solution of the reduced program on $I$ is defined only where that program has a unique solution; the decomposition of the probability therefore has to be carried out on sections of the product space, with a measurability argument for each piece. A second point is that $\sigma^*$ is random and data-dependent: a bound for each fixed $k$ does not directly give a bound at the random level $\epsilon(\sigma^*)$, and the role of the condition $\epsilon(N)=1$ must be accounted for at $k=N$.

Formalization scope

Lean representation and committed conventions:

• $\Theta$ and $\Delta$ are arbitrary types with measurable structures; $\mathbb P$ is a probability measure on $\Delta$; a sample is ω : Fin N → Δ with law Measure.pi (fun _ : Fin N => P); indices run over $0,\dots,N-1$.
• A subset of constraints is a Finset (Fin N); the reduced program with index set $I$ has feasible set $\bigcap_{i\in I}\Theta_{\delta_i}$ (all of $\Theta$ for $I=\emptyset$).
• The solution map $\theta^*$ is a parameter with the hypothesis that $\theta^*(\omega)$ is the unique solution of the full program for every sample.
• "Has the same solution" in Definition 8.8 means: the reduced program has a unique solution and it equals the unique solution of the full program. Existence of solutions is not assumed for reduced programs in general, only for those that are support sets.
• The algorithm is an arbitrary map alg : (Fin N → Δ) → Finset (Fin N) returning a support set for every sample; $\sigma^*$ is the cardinality of its output. The goal is universal over such maps.
• $\epsilon$ is a real function on $\mathbb N$ with $\epsilon(k)\in[0,1]$ for $k\le N$ and $\epsilon(N)=1$.
• The violation is real-valued in $[0,1]$; the probability of the event is compared in $[0,\infty]$ with ENNReal.ofReal of the real right-hand side.

Implicit hypotheses of the page, made explicit (the book states on p. 33 that measurability issues are glossed over): the constraint relation $\{(\theta,\delta):\theta\in\Theta_\delta\}$ is measurable in $\Theta\times\Delta$; the solution map is measurable; each event $\{\omega:\text{the algorithm returns }J\}$ is measurable; $\theta^*$ exists and is unique for every sample; $N\ge1$ in the arithmetic half of (8.16).

A trivializing formalization is ruled out: the algorithm is not existentially quantified and is not the minimal support set, the reduced programs are not all assumed solvable (which would be unsatisfiable when $f$ has no unconstrained minimizer), and the support-set property requires uniqueness of the reduced solution, without which the bound is false.

Needed infrastructure: product measures on Fin N → Δ, splitting of such products along a subset of coordinates, and Fubini/Tonelli for sections. These pieces are reusable for other compression-type bounds. Contributions welcome: proofs of the two milestones and of the goal, and lemmas on splitting Measure.pi over a Finset of coordinates.

Selected references

• M. C. Campi, S. Garatti, Introduction to the Scenario Approach, MOS-SIAM Series on Optimization 26, SIAM/MOS, 2018, §8.6, pp. 101–105. https://doi.org/10.1137/1.9781611975444
• M. C. Campi, S. Garatti, F. A. Ramponi, A general scenario theory for nonconvex optimization and decision making, IEEE Transactions on Automatic Control, 2018. https://doi.org/10.1109/TAC.2018.2808446
• M. C. Campi, S. Garatti, Wait-and-judge scenario optimization, Mathematical Programming, 2018. https://doi.org/10.1007/s10107-016-1056-9
• G. C. Calafiore, M. C. Campi, The scenario approach to robust control design, IEEE Transactions on Automatic Control, 2006. https://doi.org/10.1109/TAC.2006.875041
• M. C. Campi, S. Garatti, The exact feasibility of randomized solutions of uncertain convex programs, SIAM Journal on Optimization, 2008. https://doi.org/10.1137/07069821X
• S. Floyd, M. Warmuth, Sample compression, learnability, and the Vapnik–Chervonenkis dimension, Machine Learning, 1995. https://doi.org/10.1007/BF00993593

Motivation

Traffic information systems (TIS) such as navigation apps send drivers noisy signals about the state of a road network: incidents, weather, closures. When several such systems coexist, each with its own subscriber base and its own information, a natural question for operators and regulators is whether subscribing to one system rather than another actually lowers a driver's expected travel cost in equilibrium, and how this advantage depends on how many drivers use each system. More information for one population also changes the congestion everybody else faces, so the answer is not simply "more information is better".

Wu, Amin and Ozdaglar (Operations Research 69(1), 2021) answer this question for nonatomic routing games with heterogeneous, possibly correlated information. Their model builds on the weighted potential game framework of Sandholm (2001) and on sensitivity analysis of convex programs. This mission formalizes their Section 5 result: for any two populations the sign of the relative value of information is determined by which of three explicitly computable size regimes the population sizes lie in, and the relative value decreases as one population grows at the expense of the other.

Setting

A Bayesian routing game has a finite set of populations $\mathcal I$, one per TIS, a finite set of network states $\mathcal S$, and for each population $i$ a finite nonempty type space $\mathcal T^i$ of signals. A common prior $\pi$ is a probability distribution on $\mathcal S\times\mathcal T$, $\mathcal T=\prod_i\mathcal T^i$. A network with a single origin–destination pair has edges $\mathcal E$ and a finite nonempty set of routes $\mathcal R$; each edge has a state-dependent cost $c^s_e$ that is positive, strictly increasing and differentiable. The total demand is $D>0$, and population $i$ carries the fraction $\lambda^i$ of it, with $\lambda^i\ge0$ and $\sum_i\lambda^i=1$.

A strategy profile $q$ assigns to each population $i$ and type $t^i$ a split $q^i_r(t^i)\ge0$ of its demand $\lambda^iD$ over routes. It induces the route flow $f_r(t)=\sum_iq^i_r(t^i)$ and the edge load $w_e(t)=\sum_{r\ni e}f_r(t)$. With the belief $\beta^i(s,t^{-i}\mid t^i)=\pi(s,t^i,t^{-i})/\Pr(t^i)$, type $t^i$ evaluates route $r$ by its expected cost $\mathbb E[c_r(q)\mid t^i]$. A Bayesian Wardrop equilibrium (BWE) is a feasible $q$ in which every type uses only routes of minimal expected cost. The equilibrium population cost is $C^{i*}(\lambda)=\sum_{t^i}\Pr(t^i)\min_r\mathbb E[c_r(q)\mid t^i]$ at a BWE $q$.

The game has a weighted potential $\Phi(q)=\sum_{s,e,t}\pi(s,t)\int_0^{w_e(t)}c^s_e(z)\,dz$; its minimum over feasible profiles is the equilibrium potential value $\Psi(\lambda)$. For two populations $i\ne j$, the direction $z^{ij}$ moves demand share from $j$ to $i$, and $|\lambda^{-ij}|$ is the total share of the other populations. The impact of information $\widehat J^i(f)$ measures how much of population $i$'s demand is moved by its signal. Two thresholds $\underline\lambda^i\le\overline\lambda^i$ are computed from the optimal set $\mathcal F^{ij,\dagger}$ of an auxiliary convex program over route flows in which the separate information constraints of $i$ and $j$ are merged. They define three regimes: $\Lambda^{ij}_1$ ($\lambda^i<\underline\lambda^i$), $\Lambda^{ij}_2$ ($\underline\lambda^i\le\lambda^i\le\overline\lambda^i$) and $\Lambda^{ij}_3$ ($\lambda^i>\overline\lambda^i$). The relative value of information is $V^{ij*}(\lambda)=C^{j*}(\lambda)-C^{i*}(\lambda)$.

Formalization targets

Goal: Theorem 3

For $i\ne j$ and admissible $\lambda$ (in the simplex with $\lambda^i,\lambda^j>0$), and every BWE of $\Gamma(\lambda)$,

$$V^{ij*}(\lambda)>0 \text{ on } \Lambda^{ij}_1,\qquad V^{ij*}(\lambda)=0 \text{ on } \Lambda^{ij}_2,\qquad V^{ij*}(\lambda)<0 \text{ on } \Lambda^{ij}_3,$$

and $V^{ij*}$ is nonincreasing along $z^{ij}$: $V^{ij*}(\lambda+\varepsilon z^{ij})\le V^{ij*}(\lambda)$ for $\varepsilon>0$ with both endpoints admissible.

Milestones

The route to the goal follows the paper: Lemma 1 (weighted potential), Lemma 2 (strict convexity of the edge-load potential), Theorem 1 (equilibria are the minimizers of $\Phi$; unique edge load), Lemma 3 (unique Lagrange multipliers), Proposition 1 (the feasible route flows form a polytope $\mathcal F(\lambda)$), Proposition 2 (equilibrium route flows minimize $\widehat\Phi$ over $\mathcal F(\lambda)$), Lemma 4 ($0\le\underline\lambda^i\le\overline\lambda^i\le1-|\lambda^{-ij}|$), Theorem 2 (equilibrium flows in each regime), Proposition 3 ($\Psi$ decreases, stays constant, increases along $z^{ij}$ in the three regimes) and Lemma 5 ($\Psi$ is convex and directionally differentiable, and $V^{ij*}(\lambda)=-\frac1D\nabla_{z^{ij}}\Psi(\lambda)$).

Significance

Theorem 3 says that a population has an advantage over another exactly when it is the minor population of the pair, relative to thresholds that depend only on the other populations' sizes. Both populations face the same equilibrium cost in the middle regime. It gives a procedure for comparing two information systems without computing equilibria for each size vector: solve one convex program, read off two thresholds, and locate $\lambda^i$. The paper's Section 6 uses the same machinery, through Lemma 5, to characterize the equilibrium adoption rates of information systems.

The paper proves these results with the main proofs in the article and the sensitivity-analysis lemmas (Lemmas EC.1–EC.4) in its e-companion. None of them has a machine-checked proof. The formalization requires a Lean account of Bayesian Wardrop equilibria, of the equivalence between equilibria and a convex program, and of directional derivatives of the optimal value of a parametric convex program. Parts of this are reusable for any nonatomic routing or congestion game.

Difficulty

The equilibrium strategy profile is not unique and changes discontinuously with $\lambda$. Differentiating equilibrium costs in $\lambda$ directly therefore fails. The paper instead works with the optimal value $\Psi(\lambda)$, whose one-sided directional derivative is expressed through Lagrange multipliers. That requires a sensitivity theorem for convex programs whose constraints depend affinely on the parameter, together with uniqueness of multipliers, which fails for populations of size zero. The regime analysis also needs a characterization of the route flows that are induced by feasible strategy profiles. That set is described by the nonlinear-looking constraint $\widehat J^i(f)\le\lambda^iD$, a minimum over types inside a sum over routes. Strict monotonicity of $\Psi$ in the side regimes needs the tightness of an information constraint at every equilibrium, not only at one.

Formalization scope

The model is a Lean structure BayesRouting.VOI.Game over finite types of populations, type spaces, states, edges and routes. Routes are given by their edge sets, and the directed-graph structure is not used. Type spaces and the route set are nonempty. The prior is a probability distribution, $D>0$, and costs are positive on nonnegative loads, strictly increasing and differentiable on $\mathbb R$. One assumption is added: every type profile has positive probability. It makes beliefs well defined and the equilibrium edge load unique, and it excludes perfectly correlated signals.

Conventions: $C^{i*}$ is the last form of eq. (7), which does not divide by $\lambda^iD$. $\widehat J^i$ is the maximum of eq. (16) over the reference profile, so that $\widehat J^i(f)\le\lambda^iD$ is exactly (14d). $\Psi$ and the thresholds are sInf/sSup over sets that are nonempty and compact for size vectors in the simplex, and every statement keeps size vectors there. Statements about "the" equilibrium are stated for every BWE, and existence of a BWE is a separate item, so they are not vacuous. The thresholds are defined from the optimal set of the auxiliary program, not assumed as parameters. Taking them as parameters constrained only by Lemma 4 would give a different theorem.

Disclosed deviations: Lemma 2's $C^2$ clause assumes $C^1$ costs; Lemma 3 is stated for populations of positive size; Lemma 5 assumes $\lambda^j>0$; Proposition 3 is stated with strict monotonicity in the side regimes, as used in the proof of Theorem 3. Contributions of reusable infrastructure are welcome: interval-integral potentials of monotone costs, KKT theory for polyhedral constraints, and directional derivatives of parametric optimal values.

Selected references

• M. Wu, S. Amin, A. Ozdaglar, Value of Information in Bayesian Routing Games, Operations Research 69(1):148–163, 2021. https://doi.org/10.1287/opre.2020.1999
• W. H. Sandholm, Potential Games with Continuous Player Sets, Journal of Economic Theory 97(1):81–108, 2001. https://doi.org/10.1006/jeth.2000.2696
• R. T. Rockafellar, Directional Differentiability of the Optimal Value Function in a Nonlinear Programming Problem, in Sensitivity, Stability and Parametric Analysis (Mathematical Programming Studies 21), Springer, 1984, pp. 213–226.
• A. V. Fiacco, J. Kyparisis, Convexity and Concavity Properties of the Optimal Value Function in Parametric Nonlinear Programming, Journal of Optimization Theory and Applications 48(1):95–126, 1986.

Motivation

Scheduling tasks on machines owned by self-interested parties is the running example of Nisan and Ronen's Algorithmic Mechanism Design (Games and Economic Behavior 35, 2001), the paper that introduced the study of mechanisms whose allocation rule is an algorithm with a computational objective. Each machine (agent) privately knows how long it needs for each task; the designer wants to minimize the make-span, the completion time of the last machine, and can only influence the agents through payments.

Without further information the designer is in a weak position: the paper shows that no mechanism approximates the optimal make-span within a factor below 2 (Theorem 4.6), and that the natural truthful mechanism, MinWork, only achieves a factor $n$. Section 5 of the paper observes that in many applications the designer learns more than the agents' reports: it can pay after the work is done and observe how long each task actually took. It introduces mechanisms with verification and shows that, with this extra information, the make-span can be minimized exactly by a strongly truthful mechanism. This mission formalizes that result, Theorem 5.1, together with the steps of its proof and the participation variant, Theorem 5.4.

Setting

There are $k$ tasks and $n$ agents. The type of agent $i$ is the vector $t^i = (t^i_1,\dots,t^i_k)$ of positive numbers, $t^i_j$ being the least time in which agent $i$ can perform task $j$. An allocation $x$ gives each task to one agent; $x^i$ is the set of tasks of agent $i$. For a type vector $t$ and for a vector $\tilde t$ of actual execution times the make-spans are

$$g(x,t) = \max_i \sum_{j\in x^i} t^i_j, \qquad g(x,\tilde t) = \max_i \sum_{j\in x^i} \tilde t_j .$$

A mechanism with verification is a pair $(x, p)$. The allocation $x(d)$ is computed from the agents' declarations $d = (d^1,\dots,d^n)$ only. Each agent then performs its tasks, in any times $\tilde t_j \ge t^i_j$ it chooses, and the mechanism pays agent $i$ the amount $p^i(d, \tilde t)$, which may depend on the declarations and on the observed actual times. Agent $i$'s utility is $p^i(d,\tilde t) - \sum_{j \in x^i} \tilde t_j$. A strategy of agent $i$ therefore has two parts: a declaration $d^i$ and an execution plan $e^i$ that says, for every allocation, how long the agent takes on each of its tasks.

A strategy is dominant if it maximizes the agent's utility against all declarations and all execution plans of the other agents. The mechanism is truthful if, for every agent and type, declaring the true type (with a suitable execution plan) is dominant, and strongly truthful if the only dominant strategy is to declare the true type and to execute every task in minimal time.

The Compensation-and-Bonus mechanism uses an optimal allocation algorithm $x(\cdot)$ and pays

$$p^i(d,\tilde t) = \underbrace{\sum_{j \in x^i(d)} \tilde t_j}_{\text{compensation } c^i} \;\underbrace{-\, g\big(x(d), \mathrm{corr}^i(x(d), d, \tilde t)\big)}_{\text{bonus } b^i},$$

where the corrected time vector $\mathrm{corr}^i$ lists agent $i$'s own tasks at their actual times and every other task at the time declared by the agent it was given to.

Formalization targets

Goal: Theorem 5.1

For $n \ge 2$ agents and every optimal allocation algorithm (ties broken arbitrarily), the Compensation-and-Bonus mechanism is a strongly truthful implementation of task scheduling:

$$\text{strongly truthful} \quad\text{and}\quad g\big(x(D), \tilde t\big) \le \min_y g(y, t) \text{ whenever every agent plays a dominant strategy for its true type.}$$

Milestones (proof of Claim 5.2)

1. The utility of every agent equals its bonus.
2. For every allocation, the bonus of agent $i$ is maximized by executing its tasks in minimal time.
3. With $t = (d^{-i}, t^i)$, for every declaration $t'^i$,

$$-g\big(x(t), \mathrm{corr}^*(x(t), t)\big) \ge -g\big(x(t'^i, d^{-i}), \mathrm{corr}^*(x(t'^i, d^{-i}), t)\big).$$

4. Declaring the true type and executing in minimal time is dominant.
5. Claim 5.2: the mechanism is strongly truthful.

Further target: Theorem 5.4

For $n \ge 2$ there is a strongly truthful mechanism with an optimal allocation algorithm that satisfies participation constraints: an agent that performs its tasks in its declared times never ends with negative utility.

Significance

The result. Theorem 5.1 shows that the lower bound of 2 for task scheduling (Theorem 4.6) is an artefact of the information structure, not of incentives as such: once execution times are observable, the exact optimum is achievable in dominant strategies, and the agents have a unique rational behaviour. The construction also isolates a general principle, used again in §5.6 of the paper: an agent paid by the global objective value, computed with the others' declarations, has the designer's incentives. Theorem 5.4 shows that the bonus can be shifted to make participation individually rational, which the plain mechanism violates (its bonus is negative).

Formalizing it. The theorem is proved in the paper, in a few lines, and has no machine-checked version. A formalization has to settle what the paper leaves informal: what a strategy with an execution part is, over which strategies of the others dominance is quantified, what "the only dominant strategy" demands of the execution plan on allocations that seem never to arise, and which hypotheses on the number of agents the uniqueness needs. The model built here is also the base of two companion missions of the same series (Compensation-and-Bonus with a non-optimal allocation algorithm, and the rounding mechanism with verification).

Difficulty

Truthfulness (milestones 1–4) is short once the model is right. The difficulty is uniqueness. For a misreport or a slow execution to be excluded, one must exhibit, for every alternative strategy, declarations of the other agents under which that strategy is strictly worse. The declarations must be positive, the optimal allocation algorithm breaks ties arbitrarily, and agent $i$'s slower execution only hurts it when agent $i$ is the bottleneck. The paper's proof dismisses this step with "clearly, … there are circumstances"; the naive reading ("the others declare $+\infty$ elsewhere") is not available in a model with finite positive times, and the uniqueness clause must also cover the execution plan on every allocation, not only on the allocation produced by truthful play.

Formalization scope

• Agents are Fin n, tasks Fin k, allocations functions Fin k → Fin n; both make-spans are Finset.sup' over the nonempty set of agents ([NeZero n]).
• Types and declarations are positive real vectors; declarations range over this type space (Definition 18's "unrestricted" declaration is any element of it).
• An execution plan is a function from allocations to actual times; feasibility for type $t^i$ requires $\tilde t_j \ge t^i_j$ on the agent's own tasks only. In the dominance quantifier the other agents' plans are arbitrary.
• Payments are amounts handed to the agent; utility is quasi-linear.
• The optimal allocation algorithm is a parameter with the hypothesis that it minimizes $g(\cdot, d)$ on every positive $d$; every theorem holds for every such algorithm.
• Strong truthfulness constrains both parts of the strategy: the declaration equals the type, and the plan executes every task in minimal time under every allocation.
• Thresholds made explicit: $n \ge 2$ in Claim 5.2, Theorem 5.1 and Theorem 5.4 (not printed; with one agent every declaration is dominant, and the construction of Theorem 5.4 needs a second agent).
• Printed slips: the displayed inequality prints >=; Theorem 5.4 prints "strongly truthfulmechanism"; Definition 28 writes $\tilde t_j = t_j$ for $\tilde t_j = t^i_j$.
• Running time is out of scope.
• A formalization in which dominance is checked only against truthful other agents, in which the mechanism ignores executions, in which strong truthfulness constrains only the declaration, or in which the implementation clause is stated only at the truthful profile, is not the theorem and is ruled out by the statements.

Welcome contributions: proofs of the milestones, the uniqueness witnesses as reusable lemmas, and the contribution-based mechanism behind Theorem 5.4. Theorem 5.3 (generalized Compensation-and-Bonus) is not stated in this mission.

Selected references

• N. Nisan, A. Ronen, Algorithmic Mechanism Design, Games and Economic Behavior 35 (2001) 166–196. https://doi.org/10.1006/game.1999.0790
• T. Groves, Incentives in Teams, Econometrica 41 (1973) 617–631. https://doi.org/10.2307/1914085
• A. Mas-Colell, M. D. Whinston, J. R. Green, Microeconomic Theory, Oxford University Press, 1995.

Motivation

Algorithmic mechanism design, introduced by Nisan and Ronen (Games Econ. Behav. 35, 2001), studies optimization problems whose input is held by self-interested agents. Each agent reports its private data to a protocol, and the protocol must choose an output and payments so that reporting the truth is in every agent's interest while the chosen output is close to optimal.

The paper's test case is task scheduling on unrelated machines: $k$ tasks must be assigned to $n$ agents, agent $i$ needs time $t^i_j$ for task $j$, and the goal is to minimize the make-span. For deterministic mechanisms the paper shows that truthfulness is costly: the MinWork mechanism achieves ratio $n$, and no mechanism achieves a ratio below $2$ (Theorem 4.6). Section 4.4 asks whether randomization helps and answers yes for two agents: a randomized mechanism, truthful for every outcome of its coins, achieves expected ratio $7/4 < 2$.

Timeline.

• 1979: Roberts characterizes weighted (affine) maximizers; the weighted Vickrey–Groves–Clarke (VGC) mechanisms are truthful.
• 1999: Lehmann supplies the case analysis that improves the authors' original bound of $1.823$ to $7/4$ (acknowledged on p. 182).
• 2001: Nisan and Ronen publish the randomly biased min work mechanism and Theorem 4.16.

Setting

There are two agents, $1$ and $2$, and $k$ tasks. A type vector $t = (t^1, t^2)$ gives, for each agent $i$ and task $j$, the positive time $t^i_j$ agent $i$ needs for task $j$. An allocation $x$ assigns each task to one agent; $x^i$ is the set of tasks of agent $i$. The make-span of $x$ is

$$g(x, t) = \max_{i \in \{1,2\}} \sum_{j \in x^i} t^i_j .$$

A direct mechanism receives declared types $d$ and returns an allocation $x(d)$ and payments $p^i(d)$ handed to the agents. Agent $i$ with true type $t^i$ gets utility $p^i(d) - \sum_{j \in x^i(d)} t^i_j$. The mechanism is truthful if declaring the true type maximizes an agent's utility whatever the other agent declares, and strongly truthful if in addition every false declaration is strictly worse for some declaration of the other agent.

A randomized mechanism is a probability distribution over deterministic mechanisms; its objective is the expected make-span. It is universally truthful if every mechanism in its support is truthful, and universally strongly truthful if moreover truth-telling is the only strategy dominant in every mechanism of the support.

The biased min work mechanism with parameters $\beta \ge 1$ and $s \in \{1,2\}^k$ treats each task $j$ separately. With $i = s_j$ the favoured agent and $i' = 3 - i$ the other: if $t^i_j \le \beta \cdot t^{i'}_j$, task $j$ goes to $i$, who is paid $\beta \cdot t^{i'}_j$; otherwise it goes to $i'$, who is paid $\beta^{-1} \cdot t^i_j$. The randomly biased min work mechanism draws $s$ uniformly from $\{1,2\}^k$ and uses $\beta = 4/3$. Its expected make-span is

$$\mathbb{E}_s\, g(x_s(t), t) = \frac{1}{2^k} \sum_{s \in \{1,2\}^k} g(x_s(t), t).$$

Formalization targets

Goal: Theorem 4.16

For every $k$: the randomly biased min work mechanism is universally strongly truthful, and for every positive type vector $t$ and every allocation $y$,

$$\frac{1}{2^k} \sum_{s \in \{1,2\}^k} g(x_s(t), t) \le \frac74\, g(y, t).$$

Milestones

• Theorem 3.2 (Roberts): for positive weights $\beta^i$, a mechanism whose output maximizes $\sum_i \beta^i v^i(t^i, o)$ and whose payments are $p^i = \frac{1}{\beta^i}\sum_{j \ne i}\beta^j v^j(t^j, o) + h^i(t^{-i})$ is truthful.
• Lemma 4.15: for every $\beta \ge 1$ and every $s$, the biased min work mechanism is strongly truthful.
• Lemma 4.17: the randomly biased min work mechanism is universally strongly truthful.
• Claim 4.19, part 5: allocating two tasks independently at random gives an expected make-span no larger than allocating their merge at random.
• Reduced case (Fig. 2, Cases 1–3): for $a, b, c, d \ge 0$ with $a + c = \frac43 b + d$,

$$\tfrac14\Big(\max(a+b+c+\tfrac43 d, 0) + \max(a+b+c, d) + \max(a+b+\tfrac43 d, \tfrac43 c) + \max(a+b, \tfrac43 c + d)\Big) \le \tfrac74 (a+c).$$

• Lemma 4.18: the $7/4$ bound on the expected make-span.

Significance

The result. Theorem 4.16 separates randomized from deterministic truthful mechanisms for scheduling two unrelated machines: $7/4$ against the deterministic lower bound of $2$. The notion of truthfulness it uses is the strong one, dominance for every coin outcome, so the separation does not rest on agents being risk-neutral or knowing the distribution. Later work on truthful randomized scheduling, and on the gap between deterministic and randomized truthful mechanisms, starts from this construction.

Formalizing it. The theorem is proved in the paper; no machine-checked proof of it is known. A formalization produces a checked definition of universal truthfulness for randomized mechanisms, a checked weighted VGC theorem usable for any affine-maximizer mechanism, and a checked version of the reduction argument (Claim 4.19), which the paper states in five informal instance transformations, one of them a limiting argument.

Difficulty

Truthfulness reduces to one task at a time, where the mechanism is a weighted VGC mechanism; the difficulty lies in the approximation bound. A naive task-by-task comparison with the optimum fails: the bound is on a maximum of two loads averaged over $2^k$ coin vectors, and the maximum does not decompose over tasks. The paper reduces an arbitrary instance to four tasks through transformations that each move the ratio in one direction, and the reduced instance still needs a three-way case analysis. Making the reduction rigorous is the main work: part 1 of Claim 4.19 replaces a ratio "arbitrarily close to $\beta$" by $\beta$, and under the mechanism's tie rule a task with ratio exactly $\beta$ is allocated by the coin rather than to the efficient agent.

Formalization scope

• Agents are Fin 2 (agent $1$ is 0, agent $2$ is 1); the other agent is other i = 1 - i. Tasks are Fin k; allocations are functions Fin k → Fin 2. The statements hold for every $k$, including $k = 0$.
• Types are positive: every truthfulness quantifier ranges over positive declarations, true types and misreports, and the approximation bound is stated on positive type vectors. The reduced-case and merging milestones are pure real inequalities with nonnegative times, since the paper represents missing tasks by zero times.
• Payments are handed to the agent; utility is quasi-linear.
• The make-span is a finite maximum (Finset.sup') over the two agents. The expected make-span is the average over all $2^k$ vectors $s$, which is exactly the expectation of Definition 15 for the uniform distribution; no measure theory is used.
• Universal (strong) truthfulness quantifies over all $s \in \{1,2\}^k$, the support of the uniform distribution. Truthfulness in expectation over $s$ is weaker and is not the notion stated.
• The tie rule of Fig. 1 ($\le$: ties go to the favoured agent) is kept.
• The goal fixes $\beta = 4/3$; only Lemma 4.15 is stated for every $\beta \ge 1$. The ratio is compared with every allocation $y$, not with one fixed allocation, and the average is over all $s$, not the best $s$.
• Roberts' theorem is stated for arbitrary output sets, type sets and valuations, with positive weights.
• "Polynomial time computable" in Theorem 4.16 is not formalized; running time is out of scope.
• Claim 4.19 (the reduction to the four-task case) is not a separate item beyond its part 5, because its parts are instance transformations with a limiting step, not a single statement; a solver may formalize the reduction in any form that proves Lemma 4.18.

Contributions welcome: proofs of the milestones, and reusable lemmas on averages of maxima over product coin spaces.

Selected references

• N. Nisan, A. Ronen, Algorithmic Mechanism Design, Games and Economic Behavior 35 (2001) 166–196. https://doi.org/10.1006/game.1999.0790
• K. Roberts, The characterization of implementable choice rules, in J.-J. Laffont (ed.), Aggregation and Revelation of Preferences, North-Holland, 1979, pp. 321–349.
• T. Groves, Incentives in teams, Econometrica 41 (1973) 617–631. https://doi.org/10.2307/1914085

Motivation

Nisan and Ronen's Algorithmic Mechanism Design (Games and Economic Behavior 35, 2001) asks how well a computational task can be carried out when its inputs are held by self-interested agents who may lie about them. Their test case is scheduling on unrelated machines: tasks must be assigned to agents (machines), each agent privately knows how long it needs for each task, and the planner wants to minimize the time at which the last agent finishes. The paper shows that the mechanism MinWork, which gives each task to the fastest agent and pays it the second-fastest time, is truthful and loses a factor of at most $n$ against the optimum, and that no truthful mechanism can do better than a factor $2$. It then conjectures (Conjecture 4.9) that the factor $n$ cannot be improved by any truthful mechanism.

That conjecture became the Nisan–Ronen conjecture, one of the central questions of algorithmic mechanism design. A sequence of papers raised the general lower bound from $2$ to $1 + \sqrt 2$ (Christodoulou, Koutsoupias and Vidali), to $1 + \varphi \approx 2.618$ (Koutsoupias and Vidali) and to larger constants, and Christodoulou, Koutsoupias and Kovács (STOC 2023) finally proved the conjecture for all deterministic truthful mechanisms. In the original paper, Nisan and Ronen confirm the conjecture for two restricted classes of mechanisms, with short direct arguments. This mission concerns the second class, local mechanisms (Theorem 4.12).

Setting

There are $k$ tasks $j \in \{1, \dots, k\}$ and $n$ agents $i \in \{1, \dots, n\}$. A type vector $t$ records, for every agent $i$ and task $j$, the positive time $t^i_j$ agent $i$ needs for task $j$. An allocation $x$ assigns every task to one agent; $x^i$ is the set of tasks of agent $i$. For a set $X$ of tasks write $t^i(X) = \sum_{j \in X} t^i_j$. The make-span of $x$ is $g(x, t) = \max_i t^i(x^i)$.

A direct mechanism $(x, p)$ asks every agent for its type, computes an allocation $x(t)$ from the declarations, and hands agent $i$ the payment $p^i(t)$. Agent $i$'s utility is $p^i(t) - t^i(x^i(t))$ measured with its true times. The mechanism is truthful if declaring the true type maximizes each agent's utility whatever the other agents declare. The allocation rule is a $c$-approximation if $g(x(t), t) \le c \cdot g(y, t)$ for every type vector $t$ and every allocation $y$.

For a truthful mechanism the payment to agent $i$ depends only on the set it receives and on the declarations $t^{-i}$ of the others (Proposition 4.4). This gives the price offered to agent $i$ for a set $X$ (Definition 12):

$$p^i(X, t^{-i}) = \begin{cases} p^i(t'^i, t^{-i}) & \text{if some } t'^i \text{ gives } x^i(t'^i, t^{-i}) = X, \\ 0 & \text{otherwise.} \end{cases}$$

A mechanism is local (Definition 14) if $p^i(X, t^{-i})$ depends only on the other agents' times $\{t^l_j : l \ne i, j \in X\}$ on the tasks of $X$. MinWork is local: its price for $X$ is $\sum_{j \in X} \min_{l \ne i} t^l_j$.

Formalization targets

Goal: Theorem 4.12

For every $n \ge 1$, every $k \ge n^2$ and every real $c < n$, no truthful local mechanism is a $c$-approximation:

$$\forall (x, p) \text{ truthful and local},\ \forall c < n:\quad \exists\, t,\ y \quad g(x(t), t) > c \cdot g(y, t).$$

The bound holds for every $c < n$, so together with MinWork it shows that $n$ is the exact best ratio for local truthful mechanisms.

Milestones

1. Proposition 4.4 (Independence). Payments depend only on the allocated set and on $t^{-i}$.
2. Proposition 4.5 (Maximization). $x^i(t)$ maximizes $p^i(X, t^{-i}) - t^i(X)$ over the sets $X$ that agent $i$ can obtain.
3. Lemma 4.13. Every type vector has type vectors arbitrarily close to it at which each agent's maximizing set is unique.
4. Claim 4.14, first step. If $x^i(t)$ is the unique maximizer, lowering agent $i$'s times on $x^i(t)$ keeps $x^i(t)$.
5. Ratio step. An allocation that gives one agent $n$ tasks of time about $1$, while every other agent's own tasks are nearly free, has make-span about $n$, while splitting those $n$ tasks gives make-span about $1$.

Significance

The result. Theorem 4.12 settles the Nisan–Ronen conjecture for a natural class of mechanisms. Locality captures the mechanisms in which the price for a bundle of tasks is set only by the competition for those tasks. It includes MinWork and, more generally, every mechanism that prices tasks separately using the other agents' bids on them. The theorem says that for this class the trivial per-task auction is already optimal, so any improvement over the ratio $n$ must use prices that depend on the other agents' times on tasks outside the bundle.

Formalizing it. The statement is not open: it follows from the 2023 proof of the Nisan–Ronen conjecture, and Nisan and Ronen's own argument is much shorter. That argument is a sketch, though. Lemma 4.13 rests on an informal measure-theoretic appeal, and the core claim relies on a maximization property stated over all sets of tasks. A machine-checked proof pins down exactly which properties of truthful mechanisms the short argument needs. None of these results is known to have been formalized. The definitions (type vectors, truthful mechanisms, prices, locality) are shared with the other missions of this series.

Difficulty

An argument that looks at one agent at a time does not go through. Changing one agent's declaration changes the prices offered to every other agent, so an allocation that is stable for one agent can shift for another. The argument needs a type vector at which every agent's choice is strict, and only then can it lower times agent by agent and follow the allocation. Producing such a type vector is Lemma 4.13. The printed argument for it applies a "for almost every type vector" statement to sets defined by the price functions of an arbitrary mechanism, which need not be measurable. A proof must therefore work without any regularity of the mechanism. A second difficulty is Definition 12's convention that a set the agent cannot obtain has price $0$. Locality constrains these zero prices too, and the argument has to account for sets that are obtainable at one type vector and not at a nearby one.

Formalization scope

Agents are Fin n, tasks Fin k. An allocation is a function Fin k → Fin n, a type vector is Fin n → Fin k → ℝ, and a mechanism is a pair of functions alloc (declarations to allocation) and pay (declarations to the payment handed to each agent). Utilities are quasi-linear. All types, declarations and misreports are positive, and every truthfulness, locality and approximation quantifier ranges over positive type vectors. The make-span is a Finset.sup' over the nonempty set of agents ([NeZero n]).

Conventions and explicit thresholds:

• $k \ge n^2$. The theorem is printed without a bound on the number of tasks, and its proof begins "Let $k \ge n^2$". The goal carries $k \ge n^2$ as a hypothesis.
• Truthfulness is assumed. §4.3 assumes throughout that the mechanism is truthful (by the revelation principle this is no loss). The goal quantifies over all truthful local mechanisms.
• Prices use Definition 12 literally, including the value $0$ for sets the agent cannot obtain, and locality is Definition 14 applied to that price function over all sets $X$, not only single tasks. When several declarations give the same set, the price uses one chosen witness; by Proposition 4.4 the choice does not matter for truthful mechanisms.
• Proposition 4.5 is stated over the sets the agent can obtain. As printed, over all subsets, it is false for a truthful mechanism that never leaves an agent idle and pays it negative amounts. Uniqueness of maximizers (Lemma 4.13, Claim 4.14) refers to the same family.
• Lemma 4.13 uses Mathlib's norm on Fin n → Fin k → ℝ, the sup norm. No measurability of the mechanism is assumed.
• Claim 4.14 is printed at $t^i_j = 1$ with $0 < \varepsilon < 1$. The first step is stated at any type vector, with $0 < \varepsilon \le t^i_j$ on the lowered tasks.
• Running time and computability are out of scope.

Ruled-out trivializations: locality is not restricted to single tasks; the goal does not assume that maximizers are unique at every type vector (that is Lemma 4.13's conclusion at one point, not a hypothesis); and the bound holds for every $c < n$, not for some.

Needed infrastructure: finite sums over allocation fibres, sup norms on function spaces, and a genericity argument for finitely many affine functions (Lemma 4.13). The model file and the price and locality definitions are reusable in the other missions of the series. Proofs of individual milestones are welcome independently.

Selected references

• N. Nisan, A. Ronen, Algorithmic Mechanism Design, Games and Economic Behavior 35 (2001) 166–196. https://doi.org/10.1006/game.1999.0790
• A. Mas-Colell, M. D. Whinston, J. R. Green, Microeconomic Theory, Oxford University Press, 1995 (pp. 876–880, basic properties of truthful mechanisms).
• G. Christodoulou, E. Koutsoupias, A. Vidali, A lower bound for scheduling mechanisms, Algorithmica 55 (2009).
• E. Koutsoupias, A. Vidali, A lower bound of 1+φ for truthful scheduling mechanisms, Algorithmica 66 (2013).
• G. Christodoulou, E. Koutsoupias, A. Kovács, A proof of the Nisan–Ronen conjecture, STOC 2023.

Motivation

Algorithms deployed on the Internet often take their inputs from parties who own them and who may lie when lying pays. Nisan and Ronen's Algorithmic Mechanism Design (Games and Economic Behavior 35, 2001) proposed studying optimization problems in this setting: the algorithm designer may hand out payments, and must guarantee that the intended output is produced when every participant acts in its own interest. The paper's central test case is scheduling on unrelated machines, a standard problem of combinatorial optimization, in which the machines are the selfish participants and only they know how long each job takes them.

For this problem the paper shows that incentives cost a factor of two at least: with two or more machines, no mechanism can guarantee a make-span below twice the optimum. This was the first lower bound separating what incentive-compatible mechanisms can achieve from what ordinary approximation algorithms can achieve, and it started a line of work on the "Nisan–Ronen conjecture" (that the right factor for $n$ machines is $n$), with improved lower bounds by Christodoulou, Koutsoupias and Vidali (Algorithmica, 2009) and by Koutsoupias and Vidali (Algorithmica, 2013), and a resolution announced by Christodoulou, Koutsoupias and Kovács (STOC 2023).

Setting

There are $n$ agents (machines) $i = 1,\dots,n$ and $k$ tasks $j = 1,\dots,k$. Agent $i$'s private type is the vector $t^i = (t^i_1,\dots,t^i_k)$ of positive real numbers, $t^i_j$ being the time agent $i$ needs for task $j$; a type vector is $t = (t^1,\dots,t^n)$. An allocation $x$ assigns every task to one agent; $x^i$ is the set of tasks given to agent $i$. For a set $X$ of tasks write $t^i(X) = \sum_{j\in X} t^i_j$. The objective is the make-span

$$g(x,t) = \max_{i} t^i(x^i),$$

and an allocation rule is a $c$-approximation if its make-span is at most $c$ times that of every allocation, on every type vector.

A mechanism $m = (o,p)$ gives each agent $i$ a set $A^i$ of strategies. On a strategy profile $a = (a^1,\dots,a^n)$ it outputs an allocation $o(a)$ and hands agent $i$ a payment $p^i(a)$. An agent of type $t^i$ has utility $p^i(a) - t^i(o^i(a))$. A strategy is dominant if it maximizes the agent's utility whatever the others play. The mechanism implements a $c$-approximation if every agent of every type has a dominant strategy and every profile of dominant strategies yields a $c$-approximate allocation.

A direct mechanism $(x,p)$ has $A^i$ equal to the set of types, and is truthful if reporting the true type is dominant. For a truthful mechanism, the price $p^i(X,t^{-i})$ is the payment agent $i$ receives when, against the others' reports $t^{-i}$, some report of its own makes it receive exactly $X$ (and $0$ if none does); the price difference is $\Delta^i(A,B) = p^i(A\cup B,t^{-i}) - p^i(A,t^{-i})$.

Formalization targets

Goal: Theorem 4.6

For every $n\ge 2$, $k\ge3$ and $c<2$, no mechanism with any strategy sets implements a $c$-approximation:

$$\forall\, (A, o, p):\quad \neg\ \mathrm{Implements}(o,p,c).$$

Milestones

1. Proposition 2.1 (revelation principle): a mechanism implementing a $c$-approximation yields a truthful direct mechanism whose allocation rule is a $c$-approximation.
2. Theorem 4.6 for truthful mechanisms (§4.3): no truthful direct mechanism has a $c$-approximate allocation rule for $c<2$. With milestone 1 it gives the goal.
3. Proposition 4.4 (independence): for a truthful mechanism, $t_1^{-i}=t_2^{-i}$ and $x^i(t_1)=x^i(t_2)$ imply $p^i(t_1)=p^i(t_2)$.
4. Proposition 4.5 (maximization): $x^i(t)$ maximizes $p^i(X,t^{-i}) - t^i(X)$ over attainable $X$.
5. Lemma 4.7: the price-difference inequalities satisfied by $x^i(t)$, and the uniqueness statement for sets satisfying them strictly.
6. Claim 4.8: for two agents, all-ones types and $0<\varepsilon<1$, moving agent 1's times to $\varepsilon$ on its own bundle and $1+\varepsilon$ elsewhere leaves the allocation unchanged.
7. The even case of the ratio: at that perturbed instance the mechanism's make-span is $|x^2(t)|$ while some allocation achieves $\tfrac12|x^2(t)| + k\varepsilon$.

Significance

The result. Theorem 4.6 shows that the requirement of dominant-strategy incentive compatibility, by itself, rules out approximation ratios below $2$ for scheduling on unrelated machines, a problem for which polynomial-time $2$-approximation algorithms that ignore incentives exist (Lenstra, Shmoys, Tardos 1990) and for which the exact optimum is computable in exponential time. Combined with the MinWork mechanism of the same paper (an $n$-approximation), it determines the optimal ratio for two machines. It is the base case of the Nisan–Ronen conjecture and the prototype of the "characterize truthful mechanisms by prices" technique used throughout later work on the conjecture.

Formalizing it. The theorem has been proved since 1999, but no machine-checked version is known to exist. The mission produces a formal account of general mechanisms with arbitrary strategy sets, dominant-strategy implementation, the revelation principle in that generality, and the price characterization of truthful mechanisms (independence and maximization). These are reusable for every other lower bound in this paper and for the later literature on the conjecture.

Difficulty

The statement quantifies over all mechanisms, with arbitrary strategy sets and arbitrary payment functions, so no finite search settles it. The revelation principle reduces to truthful direct mechanisms, but even these are an infinite-dimensional family: the allocation rule may break ties in any way, and prices may be any functions of the other agents' reports.

The printed argument also has two places that need care. Proposition 4.5 and Lemma 4.7, as printed, range over all sets of tasks, while Definition 12 gives unattainable sets price $0$; the statements hold only over attainable sets, and are formalized that way. And the case where agent 2's bundle has odd size is dispatched in one sentence ("which still yields the same allocation"), which the preceding lemma does not justify when agent 2's best bundle at the perturbed prices is not unique. A complete formal proof of the goal must supply an argument for that case.

Formalization scope

• Agents are Fin n, tasks Fin k; an allocation is a function Fin k → Fin n; bundles may be empty. The make-span is a finite maximum and assumes $n\ge1$ (NeZero n).
• Types, declarations and misreports are strictly positive reals throughout (Definition 10). Utility is quasi-linear; payments are handed to the agent and may have either sign.
• A general mechanism has strategy sets A : Fin n → Type u (any universe), output $o$ and payments $p$ on dependent strategy profiles. Implements requires both that every agent of every positive type has a dominant strategy and that every profile of dominant strategies yields a $c$-approximate allocation. Dominance is against every profile of the others, not only dominant ones. Without the existence clause, a mechanism with no dominant strategies would implement vacuously; the definition excludes that.
• Thresholds made explicit: $n\ge2$ and $k\ge3$, both taken from the proof ("We prove the theorem for the case of two agents"; "Let $k\ge3$"). The goal holds for each fixed $n$ and $k$ and every $c<2$, for every mechanism, with no restriction on tie-breaking and no requirement of strong truthfulness. At $n=1$ the claim is false.
• Proposition 2.1 is stated for task scheduling with the $c$-approximation specification; "truthful implementation" is read as truth-telling dominant and the truthful output $c$-approximate.
• Printed slips: Proposition 4.5 and Lemma 4.7 are stated over attainable sets; the "Moreover" of Lemma 4.7 requires $Y$ attainable. The odd case of the ratio step is not a milestone.
• The reduction from $n>2$ to two agents ("having the other agents be much slower") is not a separate milestone; the goal covers every $n\ge2$.
• Running time ("polynomial-time computable") is out of scope and not modelled.

Contributions of any of the milestones are welcome, as are alternative proofs of the goal that avoid the terse odd case.

Selected references

• N. Nisan, A. Ronen, Algorithmic Mechanism Design, Games and Economic Behavior 35 (2001) 166–196. https://doi.org/10.1006/game.1999.0790
• A. Mas-Colell, M. D. Whinston, J. R. Green, Microeconomic Theory, Oxford University Press, 1995 (revelation principle, p. 871).
• J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, Mathematical Programming 46 (1990) 259–271. https://doi.org/10.1007/BF01585745
• G. Christodoulou, E. Koutsoupias, A. Vidali, A lower bound for scheduling mechanisms, Algorithmica 55 (2009).
• E. Koutsoupias, A. Vidali, A lower bound of 1+φ for truthful scheduling mechanisms, Algorithmica 66 (2013).
• G. Christodoulou, E. Koutsoupias, A. Kovács, A proof of the Nisan–Ronen conjecture, STOC 2023.

Motivation

Every physical or engineering model built from linear relations mixes two kinds of numbers. Some coefficients are exact — the $\pm 1$ entries recording Kirchhoff's current and voltage laws in an electrical network, or the incidence structure of a mechanical linkage — because they come from a topological or combinatorial fact, not a measurement. Others are physical parameters: resistances, masses, spring constants, reaction rates. These are known only approximately, and different parameters are, for modeling purposes, independent of one another. Classical linear algebra treats every entry of a coefficient matrix alike, so it cannot express this distinction, and a numerical computation on a matrix with noisy parameter entries can accidentally hit a non-generic coincidence — a determinant that would vanish only for a measure-zero set of parameter values, but that plain Gaussian elimination has no way to certify is not actually structurally forced to vanish. Murota and collaborators (see the bibliographical notes to chapter 12; the underlying theory is developed at length in Murota's Matrices and Matroids for Systems Analysis, 2000) formalized this distinction through mixed matrices, and showed that their key structural questions — is the matrix nonsingular, and what is its rank — reduce to a combinatorial optimization problem solvable by the discrete convex analysis this book develops. This mission formalizes that reduction and its capstone consequence, a generalization of the classical König–Egerváry theorem.

Setting

Fix two fields $K \subseteq F$: typically $K = \mathbb{Q}$ and $F$ a field large enough to hold every number in the problem. A family $t_1, \dots, t_m \in F$ is algebraically independent over $K$ if no nonzero polynomial with coefficients in $K$ vanishes at $(t_1, \dots, t_m)$ — informally, the $t_i$ behave as free, unconstrained parameters relative to $K$. Fix finite row and column index sets $R$ and $C$. A matrix $A = (A_{ij})_{i \in R, j \in C}$ over $F$ is a mixed matrix with respect to $(K, F)$ if it decomposes as

$$A = Q + T$$

where $Q = (Q_{ij})$ has every entry in $K$, and $T = (T_{ij})$ has entries in $F$ whose nonzero values, taken together as one family, are algebraically independent over $K$. $Q$ models the exact, structural part of the system; $T$ models the independent physical parameters. For $I \subseteq R$ and $J \subseteq C$, write $A[I,J]$ for the submatrix with rows $I$ and columns $J$. The rank of $A$ is its rank over $F$ — equivalently, the size of the largest nonvanishing-determinant square submatrix. Write $\rho(I,J) = \operatorname{rank} Q[I,J]$, $\tau(I,J) = \operatorname{rank} T[I,J]$, and $\gamma(I,J)$ for the number of rows of $I$ that contain a nonzero entry of $T$ in some column of $J$. A mixed polynomial matrix $A(s) = Q(s) + T(s)$ is the same decomposition applied entrywise to matrices whose entries are polynomials in an indeterminate $s$ (used to model the Laplace- or $z$-transform variable of a linear time-invariant system): $Q(s)$ has every coefficient of every entry in $K$, and the coefficients of $T(s)$'s entries, taken together, are algebraically independent over $K$.

Formalization targets

$$\textbf{Theorem 12.9 (goal).}\quad \text{For a mixed matrix } A=Q+T,\ \exists\, I \subseteq R,\ J \subseteq C:\quad |I|+|J|-\operatorname{rank} Q[I,J] = |R|+|C|-\operatorname{rank} A \ \ \text{and}\ \ \operatorname{rank} T[I,J] = 0.$$

This is the König–Egerváry theorem for mixed matrices: a combinatorial certificate of $A$'s rank deficiency, generalizing the classical theorem relating the maximum matching size of a bipartite graph (equivalently, the rank of a 0-1 matrix) to a minimum vertex cover. It is reached via three supporting results, each a genuine theorem in its own right: Proposition 12.6 (nonsingularity of $A$ reduces to nonsingularity of a $Q$-part and a $T$-part on complementary index splits), Theorem 12.7 (the resulting rank max-formula), and Theorem 12.8 (the three dual min-formulas Theorem 12.9 is extracted from). Theorem 12.13 extends the max-formula to the degree of the determinant of a mixed polynomial matrix.

Significance

The result itself. Theorem 12.9 gives a certificate, not just a number: a pair $(I,J)$ that simultaneously proves the exact numeric rank contribution of $Q$ and exhibits a submatrix of $T$ that vanishes identically. Because $\rho$ (via Gaussian elimination on $Q$) and $\gamma$, $\tau$ (via maximum bipartite matching on $T$'s nonzero pattern) are each individually cheap to evaluate, and the min-max structure of Theorem 12.8 is exactly the kind of problem Edmonds's matroid intersection theorem (a special case of this book's Theorem 4.18) and this book's discrete convexity machinery solve efficiently, the whole rank computation for a mixed matrix — and hence the generic solvability test for a physical system modeled by one — is polynomial-time, despite Theorem 12.7's formula naively ranging over exponentially many index-set pairs.

Formalizing it. All five results in this mission are proved in the source text (this is textbook, not open, mathematics). What formalization adds is a machine-checked confirmation that the genericity hypothesis — "the nonzero entries of $T$ are algebraically independent" — is precisely what the printed proofs use, expressed through Mathlib's own AlgebraicIndependent rather than an informal paraphrase such as "generic" or "random" values, which would be either meaningless or a different (probabilistic) condition.

Difficulty

The naive approach to testing whether $A = Q+T$ is nonsingular is to expand $\det A$ directly and check whether the resulting expression, as a polynomial in $T$'s free parameters, is the zero polynomial. This is exactly what genericity is supposed to let you avoid: Proposition 12.6's proof observes that the Laplace-type expansion $\det A = \sum_{|I|=|J|} \pm \det Q[I,J] \cdot \det T[R\setminus I, C\setminus J]$ has no cancellation between distinct terms, precisely because the nonzero entries of $T$ are algebraically independent — a coincidental cancellation would be a nontrivial polynomial relation among free parameters, which cannot happen. This turns a determinant computation with symbolic entries into a purely combinatorial search over row/column splits, each of whose two pieces is checked in the "easy" arithmetic appropriate to it (numeric determinant for $Q$, a nonzero-pattern-only matching argument for $T$). Missing this point — e.g. by treating $T$'s entries as merely "distinct" or "typically nonzero" rather than algebraically independent — reintroduces exactly the cancellation risk the theorem is built to rule out.

Formalization scope

Row and column index sets $R$, $C$ are general finite types (Fintype, with DecidableEq where needed for Finset operations), not fixed to $\mathrm{Fin}\ n$. No constant appears in any statement in this mission — every quantity (ranks, cardinalities, $\gamma$) is instance-dependent, so rule 7's explicit-constant obligation does not apply here. "Nonsingular" for a (possibly rectangular, cross-type-indexed) submatrix $M[I,J]$ is formalized as I.card = J.card together with rank M[I,J] = I.card (full rank) rather than via Matrix.det, because Mathlib's determinant requires both index sets to be the same Lean type, which I : Finset R and J : Finset C are not in general even when equinumerous; this coincides with ordinary nonsingularity whenever the ambient matrix is genuinely square. The degree of the determinant of a submatrix in Theorem 12.13 is computed the same way, via an arbitrary reindexing bijection between the row- and column-index subtypes — a choice that changes the determinant by at most a sign and hence never changes its degree. A formalization that replaced the genericity hypothesis on $T$ with mere distinctness of its nonzero entries would admit spurious cancellations in the determinant expansion and would not prove Proposition 12.6 or any of its consequences; AlgebraicIndependent K is the precise, non-trivializing condition the book's proofs use. This chapter is self-contained: no definitions from any other mission in this series are imported. Reusable beyond this mission: MatrixSubRank, IsNonsingularSub, and SubDegDet apply to any pair of matrices over any field, not only to mixed-matrix decompositions.

Selected references

• Murota, K. Discrete Convex Analysis. SIAM, 2003. DOI: 10.1137/1.9780898718508. (Chapter 12.)
• Murota, K. Matrices and Matroids for Systems Analysis. Springer, 2000.
• Murota, K. "Systems Analysis by Graphs and Matroids: Structural Solvability and Controllability." Springer, 1987.
• König, D. "Gráfok és mátrixok" (Graphs and matrices). Matematikai és Fizikai Lapok 38, 1931, 116–119.
• Egerváry, J. "Matrixok kombinatorius tulajdonságairól" (On combinatorial properties of matrices). Matematikai és Fizikai Lapok 38, 1931, 16–28.

Motivation

This mission continues chapter 10's algorithmic account across its remaining two sections: finishing the Iwata-Fleischer-Fujishige fixing algorithm for submodular minimization (§10.2.3's tail), the steepest descent algorithm for L-convex function minimization (§10.3), and — the capstone of chapter 10's account of the M-convex submodular flow problem (§10.4) — conjugate scaling, the operation that finally makes the primal-dual algorithm run in polynomial time. As in mission 34-ch10b-algorithms, most of this block's numbered results are asymptotic complexity bounds; this mission places the results that are ordinary mathematical propositions.

Setting

The IFF fixing algorithm (mission 34-ch10b-algorithms) builds an acyclic graph D=(U,F) and partition Z,H,Γ certifying the maximal minimizer of a submodular ρ once η≤0 (Eq. (10.26)); this mission places the case-independent inequality its own legitimacy rests on, and restates its correctness conclusion. The steepest descent algorithm for an L-convex function g repeatedly minimizes the submodular set function ρ_p(X)=g(p+χ_X)-g(p) and moves to p+χ_X for its minimal minimizer X (the tie-breaking rule (10.33)); this mission places the resulting monotonicity fact and a domain-size bound for the L$^\natural$-convex adaptation. Conjugate scaling replaces a dual-integral M-convex function's conjugate g with g_α(p)=g(αp)/α, defining f⟨α⟩ via the resulting sup-formula (Eq. (10.77)) — a scaling operation compatible with M-convexity where the naive ⌈f(·)/α⌉ is not.

Formalization targets

Goal: Conjugate scaling preserves M-convexity (Proposition 10.41)

For a dual-integral polyhedral M-convex function f (represented as the mixed real-primal/ integer-dual conjugate of an L$^\natural$-convex g), the conjugate scaling f⟨α⟩ is again dual-integral M-convex, witnessed by g_α itself being L$^\natural$-convex, provided f⟨α⟩>-∞. Chosen as goal: this is the fact the whole conjugate scaling algorithm — chapter 10's final and most refined algorithm for the M-convex submodular flow problem — depends on, and the book's own text singles it out as the "compatible scaling operation" that makes M-convex cost scaling work where a naive approach provably does not.

Supporting structural targets

Proposition 10.26 (the case-independent inequality underlying the IFF fixing algorithm's own legitimacy) and Proposition 10.28 (that algorithm's correctness conclusion) close out mission 34-ch10b-algorithms's coverage of §10.2.3. Proposition 10.30 gives the steepest descent algorithm's monotonicity property under its tie-breaking rule; Proposition 10.32 (found by direct reading) bounds the L$^\natural$-convex adaptation's domain-size parameter in terms of the original function's.

Significance

Conjugate scaling is chapter 10's demonstration that M-convexity, while a combinatorial rather than a numeric-magnitude notion, still admits a genuine scaling technique compatible with its own structure — completing the book's account of the M-convex submodular flow problem with an algorithm whose polynomial running time depends on exactly this compatibility. Propositions 10.26/10.28 complete the correctness/legitimacy argument for the strongly polynomial submodular- minimization algorithm mission 34-ch10b-algorithms began placing, and Propositions 10.30/10.32 are the analogous structural facts for L-convex function minimization, chapter 10's third major algorithmic thread.

None of these results are open — they are Murota's own account of submodular-function- minimization (§10.2 continued), L-convex minimization (§10.3), and conjugate scaling (§10.4.5). What this mission contributes is a faithful, machine-checked formal statement of each, including one result (Proposition 10.32) the platform's own automated extractor missed; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

As in mission 34-ch10b-algorithms, several numbered results in this block are excluded as hard for being pure algorithmic-complexity bounds (Propositions 10.25, 10.27, 10.31); see HARD.md. A further three (Propositions 10.37-10.39, on the primal-dual algorithm's maximum submodular flow subproblem) are excluded for a distinct reason: the source text's own OCR extraction demonstrably cannot distinguish the two visually different capacity-bound symbols (c* overlined vs. underlined) central to their shared defining formula, confirmed directly against the raw extracted bytes, making faithful reconstruction of that formula impossible from the available text; see HARD.md.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq. All apparatus needed for Propositions 10.26/10.28 (Submodular, GammaSet, RhoTilde, ReachSet, Eta, IsMaximalMinimizer) is redeclared fresh from mission 34-ch10b-algorithms, genericized over an arbitrary ground type where the original was V-specific, since this draft cannot import that sibling. Proposition 10.26 is placed as the case-independent core inequality its own proof establishes, rather than by replicating the three-case verification against Proposition 10.24's own internal proof objects (Cases (i)-(iii)); see HARD.md. Proposition 10.30 omits its own trailing iteration-count corollary (a pure complexity bound); see HARD.md. Six numbered results (Propositions 10.25, 10.27, 10.31, 10.37, 10.38, 10.39) are hard. Contributions completing any of the five sorrys are welcome; the goal carries the most independent proof content (via the conjugacy theorem and Theorem 7.10(2), both established elsewhere in this series).

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• S. Iwata, "A faster scaling algorithm for minimizing submodular functions," SIAM Journal on Computing, 32 (2003), pp. 833-840 [99] (conjugate scaling's origin).
• A. Frank, "A weighted matroid intersection algorithm," Journal of Algorithms, 2 (1981), pp. 328-336 [55] (the primal-dual framework this mission's Proposition 10.28 continues, via mission 34-ch10b-algorithms's own Proposition 10.24).

Motivation

In the capacitated vehicle routing problem (CVRP) a fleet of $m$ vehicles of capacity $Q$ leaves a depot and serves $n$ customers; every customer is visited once, and the load of each route must not exceed $Q$. In practice customer demands are uncertain at planning time. The chance-constrained CVRP asks that each route respect the capacity with probability at least $1-\epsilon$, but this presupposes a known demand distribution, which is rarely available. Ghosal and Wiesemann (Oper. Res. 68(3), 2020) require the chance constraints to hold for every distribution in an ambiguity set $\mathcal P$ built from the information that can actually be estimated: support, means and dispersion bounds.

Their branch-and-cut method separates rounded capacity inequalities whose right-hand side is the worst-case value-at-risk of the total demand of a customer set $S$. This quantity is evaluated thousands of times during the search, so it matters whether it has a closed form or a small convex reformulation. This mission concerns the paper's covariance ambiguity sets (§5.2), which bound the whole covariance matrix of the demands and can therefore express that demands of nearby customers are correlated, as happens with geographically clustered demand. The covariance bound can be derived from data, for example analytically through McDiarmid's inequality (Delage and Ye, 2010) or by bootstrapping.

Setting

Customers are indexed by $i\in\{1,\dots,n\}$ and their random demand vector is $\tilde{\boldsymbol q}\in\mathbb R^n$. Fix a box $\mathcal Q=[\underline{\boldsymbol q},\overline{\boldsymbol q}]$ with $\underline{\boldsymbol q}\ge\mathbf 0$, a mean vector $\boldsymbol\mu$ in the interior of $\mathcal Q$, and a symmetric positive definite matrix $\Sigma\succ0$. The covariance ambiguity set is

$$\mathcal P=\Big\{\mathbb P\in\mathcal P_0(\mathbb R^n):\ \mathbb P[\tilde{\boldsymbol q}\in\mathcal Q]=1,\ \mathbb E_{\mathbb P}[\tilde{\boldsymbol q}]=\boldsymbol\mu,\ \mathbb E_{\mathbb P}\big[(\tilde{\boldsymbol q}-\boldsymbol\mu)(\tilde{\boldsymbol q}-\boldsymbol\mu)^\top\big]\preceq\Sigma\Big\},\tag{16}$$

where $\mathcal P_0(\mathbb R^n)$ is the set of all probability distributions on $\mathbb R^n$ and $A\preceq\Sigma$ means that $\Sigma-A$ is positive semidefinite.

For a distribution $\mathbb P$ and a real random variable $\tilde X$, the value-at-risk at level $1-\epsilon$, $\epsilon\in(0,1)$, is $\mathbb P\text{-VaR}_{1-\epsilon}[\tilde X]=\inf\{x\in\mathbb R:\mathbb P[\tilde X\le x]\ge1-\epsilon\}$. For a customer set $S$, the worst-case value-at-risk is $\sup_{\mathbb P\in\mathcal P}\mathbb P\text{-VaR}_{1-\epsilon}[\sum_{i\in S}\tilde q_i]$. A route serving $S$ satisfies the chance constraint for every $\mathbb P\in\mathcal P$ exactly when this number is at most $Q$.

Two componentwise bounds appear in the answer:

$$\boldsymbol q^\ell=\max\Big\{-\tfrac{1-\epsilon}{\epsilon}(\overline{\boldsymbol q}-\boldsymbol\mu),\ \underline{\boldsymbol q}-\boldsymbol\mu\Big\},\qquad\boldsymbol q^u=\min\Big\{\tfrac{1-\epsilon}{\epsilon}(\boldsymbol\mu-\underline{\boldsymbol q}),\ \overline{\boldsymbol q}-\boldsymbol\mu\Big\}.$$

A route set is an ordered partition of the customers into $m$ nonempty ordered routes. It is feasible in the distributionally robust problem RVRP($\mathcal P$) if every route satisfies the chance constraint for every $\mathbb P\in\mathcal P$, and feasible in a deterministic instance with capacity $Q'$ and demands $\boldsymbol q$ if every route's total demand is at most $Q'$.

Formalization targets

Goal: Theorem 7

For every customer set $S$,

$$\sup_{\mathbb P\in\mathcal P}\mathbb P\text{-VaR}_{1-\epsilon}\Big[\sum_{i\in S}\tilde q_i\Big]=\max\Big\{\mathbf 1_S^\top\boldsymbol\mu+\mathbf 1_S^\top\boldsymbol q:\ \boldsymbol q^\top\Sigma^{-1}\boldsymbol q\le\tfrac{1-\epsilon}{\epsilon},\ \boldsymbol q\in[\boldsymbol q^\ell,\boldsymbol q^u]\Big\}.\tag{17}$$

The right-hand side maximizes an affine function over the intersection of an ellipsoid and a box.

Milestone: Corollary 4 (corrected)

For a diagonal bound $\Sigma=\operatorname{diag}(\sigma_1^2,\dots,\sigma_n^2)$, program (17) collapses to a search over one parameter $\theta\ge0$ with $S(\theta)=\{i\in S:\sigma_i^2>\theta q^u_i\}$:

$$\sup_{\theta}\ \mathbf 1_S^\top\boldsymbol\mu+\sum_{i\in S(\theta)}q^u_i+\sqrt{\Big[\tfrac{1-\epsilon}{\epsilon}-\sum_{i\in S(\theta)}\big(\tfrac{q^u_i}{\sigma_i}\big)^2\Big]\Big[\sum_{i\in S\setminus S(\theta)}\sigma_i^2\Big]},\tag{18}$$

over the $\theta$ for which the first bracket is nonnegative and the point of (17) that $\theta$ induces respects $\boldsymbol q^u$ (see Formalization scope).

Milestone: Theorem 6

For some instance with the ambiguity set (16), no deterministic CVRP instance on the same customers and fleet has the same set of feasible route sets.

Significance

Theorem 7 makes the worst-case value-at-risk over (16) computable in polynomial time as a convex quadratically constrained program. With it, the rounded capacity inequalities of the two-index vehicle flow formulation can be separated for covariance information. Theorem 2 of the same paper shows that the resulting demand estimator is subadditive, so this formulation is exact. Corollary 4 gives a closed form for the diagonal case, which the paper uses to evaluate the estimator in time linear in $|S|$ after sorting. Theorem 6 explains why the paper needs this machinery: the robust feasible region cannot be reproduced by any deterministic demand vector and capacity.

The results are proved in the paper's online supplement. No part of them is formalized anywhere to our knowledge; the platform has no worst-case value-at-risk and no moment-based ambiguity set. A complete development would give machine-checked worst-case VaR bounds over moment sets with second-order information. These are used well beyond routing, in distributionally robust portfolio and inventory models.

Difficulty

The supremum ranges over an infinite-dimensional set of distributions, while (17) ranges over vectors. The inequality "$\ge$" requires, for every feasible $\boldsymbol q$ of (17), a sequence of distributions in (16) whose value-at-risk approaches $\mathbf 1_S^\top(\boldsymbol\mu+\boldsymbol q)$. The value-at-risk is a lower quantile, so a distribution placing mass exactly $\epsilon$ on a high point does not attain the value: the construction has to be a limit. The inequality "$\le$" is harder. It must rule out every distribution, not only two-point ones, and a bound through the one-dimensional Chebyshev–Cantelli inequality for $\sum_{i\in S}\tilde q_i$ alone ignores the box: it yields $\sqrt{\frac{1-\epsilon}{\epsilon}\mathbf 1_S^\top\Sigma\mathbf 1_S}$, which is too large whenever the support bounds bind. The interaction between the Loewner constraint and the componentwise support bounds, which produces the unusual bound $\boldsymbol q^\ell$, is where the work lies. For Theorem 6 the difficulty is to exhibit the instance and to evaluate enough chance constraints exactly.

Formalization scope

Customers are Fin n (0-based) and demand vectors are Fin n → ℝ. Distributions are measures on Fin n → ℝ. The set (16) is covarianceSet qlo qhi μ Sig: a probability measure with P (Set.Icc qlo qhi) = 1, coordinate means μ, and Sig - M positive semidefinite, where M is the matrix of integrals $\int(q_i-\mu_i)(q_j-\mu_j)\,d\mathbb P$. The covariance bound is called Sig because Σ is Lean syntax. The side conditions $\underline{\boldsymbol q}\ge\mathbf 0$, $\boldsymbol\mu\in\operatorname{int}\mathcal Q$, $\Sigma\succ0$ (Sig.PosDef) and $0<\epsilon<1$ are hypotheses of every theorem. The value-at-risk is the published MultistageStochastic.valueAtRisk P Y (1 - ε). The worst-case value-at-risk is a real sSup over the image of the set. That image is nonempty (the Dirac measure at $\boldsymbol\mu$ lies in (16)) and bounded (the box), so the supremum is genuine. "The optimal objective value" of a maximization is stated as a supremum; attainment is not part of any claim. $\Sigma^{-1}$ is Mathlib's matrix inverse.

The paper states Theorem 7 and Corollary 4 with "$\mathbb P$-VaR" without a level; the level $1-\epsilon$, used in the sentence introducing Theorem 7 and everywhere else, is read in. Corollary 4 as printed is false. It maximizes over every $\theta\ge0$ with a nonnegative bracket. For $n=1$, every large $\theta$ then gives the value $\mu_1+\sigma_1\sqrt{(1-\epsilon)/\epsilon}$, which can exceed $\overline q_1$ and hence every value-at-risk. The formal statement adds the condition that makes each $\theta$ a feasible point of (17): $\sigma_i^2\sqrt{s(\theta)}\le q^u_i\sqrt{\sum_{k\in S\setminus S(\theta)}\sigma_k^2}$ for $i\in S\setminus S(\theta)$, where $s(\theta)$ is the first bracket. With this condition the statement is the diagonal case of Theorem 7.

A theorem about the Lean set is trivial if the set is empty or the supremum is a junk value. Neither happens here, and replacing the Loewner constraint by a scalar variance bound on $\sum_{i\in S}\tilde q_i$ would state a different theorem. The dual second-order cone program printed after Theorem 7 is not a target: as printed it has the all-ones vector where Lagrangian duality gives $\mathbf 1_S$, and it has no multiplier for $\boldsymbol q\ge\boldsymbol q^\ell$.

Needed infrastructure: quantiles of pushforward measures, the Loewner order on moment matrices, and finite-support (two-point) distributions. The value-at-risk lemmas and the moment-matrix lemmas are reusable beyond this mission, and contributions of either kind are welcome. Theorem 6 needs only the route-set layer defined here and one explicit instance.

Selected references

• S. Ghosal and W. Wiesemann, The Distributionally Robust Chance-Constrained Vehicle Routing Problem, Operations Research 68(3):716–732, 2020. https://doi.org/10.1287/opre.2019.1924
• E. Delage and Y. Ye, Distributionally Robust Optimization Under Moment Uncertainty with Application to Data-Driven Problems, Operations Research 58(3):595–612, 2010. https://doi.org/10.1287/opre.1090.0741
• S. Boyd and L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004. https://doi.org/10.1017/CBO9780511804441
• G. Laporte, Y. Nobert and M. Desrochers, Optimal Routing under Capacity and Distance Restrictions, Operations Research 33(5):1050–1073, 1985. https://doi.org/10.1287/opre.33.5.1050