All missions

Motivation

Many procedures in high-dimensional statistics reduce to computing the probability that a normalized sum of independent random vectors falls into a set: simultaneous confidence intervals for many means, max-type tests, multiple testing with family-wise error control, and inference after model selection. When the dimension $p$ is comparable to or much larger than the sample size $n$, these probabilities are approximated by those of a Gaussian vector with the same covariance, the high-dimensional central limit theorem. That Gaussian law is not available in practice, because its covariance matrix is unknown. The Gaussian multiplier bootstrap replaces it by a Gaussian vector built from the data, whose covariance is the sample covariance, and simulates from it.

Chernozhukov, Chetverikov and Kato, Central limit theorems and bootstrap in high dimensions (Ann. Probab. 45 (2017)), prove that this bootstrap is valid uniformly over hyperrectangles and over simple convex sets (sets sandwiched between a polytope with polynomially many facets and its small enlargement), with error depending on $p$ only through $\log p$. This mission formalizes their abstract multiplier bootstrap theorem, Theorem 4.1.

Timeline:

• 2013: the same authors prove Gaussian approximation and multiplier bootstrap validity for maxima of sums of high-dimensional vectors (Ann. Statist. 41 (2013)).
• 2015: comparison and anti-concentration bounds for maxima of Gaussian vectors (Probab. Theory Related Fields 162 (2015)), reference [20] of the paper; its Theorem 1 is the Gaussian-to-Gaussian comparison used here.
• 2017: the present paper extends both the CLT and the bootstrap from maxima to hyperrectangles and simple convex sets.

Setting

Let $n\ge4$ and $p\ge3$. Let $X_1,\dots,X_n$ be independent random vectors in $\mathbb R^p$ with coordinates $X_{ij}$, centred ($\mathrm E[X_{ij}]=0$) with $\mathrm E[X_{ij}^2]<\infty$. Let $Y_1,\dots,Y_n$ be independent Gaussian vectors with $Y_i\sim N(0,\mathrm E[X_iX_i'])$ and set

$$S_n^Y=\frac1{\sqrt n}\sum_{i=1}^nY_i .$$

The multiplier bootstrap: let $e_1,\dots,e_n$ be i.i.d. $N(0,1)$, independent of the data $X_1^n=\{X_1,\dots,X_n\}$, let $\bar X=n^{-1}\sum_iX_i$, and

$$S_n^{eX}=\frac1{\sqrt n}\sum_{i=1}^ne_i(X_i-\bar X).$$

Given the data, $S_n^{eX}$ is Gaussian with covariance $\widehat\Sigma=n^{-1}\sum_i(X_i-\bar X)(X_i-\bar X)'$, while $S_n^Y$ has covariance $\Sigma=n^{-1}\sum_i\mathrm E[X_iX_i']$.

A hyperrectangle is a set $\{w:a_j\le w_j\le b_j\ \forall j\}$ with $-\infty\le a_j\le b_j\le\infty$. For a finite set $\mathcal V$ of unit vectors and thresholds $s(v)$, the polyhedron $A^m=\bigcap_{v\in\mathcal V}\{w:w'v\le s(v)\}$ has the enlargement $A^{m,\epsilon}=\bigcap_{v\in\mathcal V}\{w:w'v\le s(v)+\epsilon\}$. For constants $a,d>0$, a Borel set $A$ satisfies condition (C) if $A^m\subseteq A\subseteq A^{m,a/n}$ for some such polyhedron with $m\le(pn)^d$ facets; $A^m(A)$ denotes this polyhedron and $\mathcal V(A^m)$ its normals. Condition (M.1′) with constant $b>0$ asks $n^{-1}\sum_i\mathrm E[(v'X_i)^2]\ge b$ for every $v\in\mathcal V(A^m)$. Finally,

$$\Delta_n(\mathcal A)=\sup_{A\in\mathcal A}\max_{v_1,v_2\in\mathcal V(A^m(A))}\big|v_1'(\widehat\Sigma-\Sigma)v_2\big|,\qquad \Delta_{n,r}=\max_{j,k}|\widehat\Sigma_{jk}-\Sigma_{jk}| .$$

Formalization targets

Goal: Theorem 4.1

Let $\mathcal A$ be a class of sets satisfying (C) and (M.1′). There is $C$ depending only on $a,b,d$ such that for every $\bar\Delta_n>0$, on the event $\Delta_n(\mathcal A)\le\bar\Delta_n$,

$$\rho_n^{MB}(\mathcal A)=\sup_{A\in\mathcal A}\big|P(S_n^{eX}\in A\mid X_1^n)-P(S_n^Y\in A)\big|\le C\big\{\bar\Delta_n^{1/3}\log^{2/3}(pn)+n^{-1}\log^{1/2}(pn)\big\}.$$

The theorem is deterministic in the data: it holds at every realization on the event, and turning it into a rate requires only a bound on $\Delta_n(\mathcal A)$.

Milestones

In the order of the proof (App. E.2, p. 2342):

1. Conditional Gaussianity: given $X_1^n$, $S_n^{eX}\sim N(0,\widehat\Sigma)$.
2. Display (21): $0\le F_\beta(w)-\max_j(w_j-y_j)\le\beta^{-1}\log p$ for the smooth max $F_\beta(w)=\beta^{-1}\log\sum_je^{\beta(w_j-y_j)}$.
3. The comparison display $|\mathrm E[g(F_\beta(S^{eX}_n))\mid X_1^n]-\mathrm E[g(F_\beta(S^Y_n))]|\le(\|g''\|_\infty/2+\beta\|g'\|_\infty)\Delta_{n,r}$.
4. Lemma A.1 (Nazarov's inequality): $P(Y\le y+a)-P(Y\le y)\le Ca\sqrt{\log p}$ for a centred Gaussian $Y$ with variances at least $b$.
5. The smoothed step: $|P(S^{eX}_n\le y-\phi^{-1}\mid X_1^n)-P(S^Y_n\le y-\phi^{-1})|\le C\{\phi^{-1}\log^{1/2}p+(\phi^2+\beta\phi)\Delta_{n,r}\}$ with $\beta=\phi\log p$.
6. Display (39): $\sup_y|P(S^{eX}_n\le y\mid X_1^n)-P(S^Y_n\le y)|\le C\Delta_{n,r}^{1/3}\log^{2/3}p$ under (M.1): $n^{-1}\sum_i\mathrm E[X_{ij}^2]\ge b$.
7. Remark 4.1 = (38): $\rho_n^{MB}(\mathcal A^{re})\le C\bar\Delta_n^{1/3}\log^{2/3}p$ on $\Delta_{n,r}\le\bar\Delta_n$, $C$ depending only on $b$.
8. The reduction display: for one simple convex set, the error at $A$ is at most $C\epsilon\log^{1/2}(pn)+\bar\rho$, where $\bar\rho$ is the larger error at $A^m$ and $A^{m,\epsilon}$.

Significance

Theorem 4.1 is the abstract step behind the paper's explicit multiplier bootstrap rates: Proposition 4.1 combines it with maximal inequalities that bound $\Delta_n(\mathcal A)$ with high probability, and obtains, with probability at least $1-\alpha$, the rate $(B_n^2\log^5(pn)\log^2(1/\alpha)/n)^{1/6}$ for simple convex sets with sparse facet normals. In applications it justifies bootstrap critical values for max-type statistics and simultaneous confidence regions when $p\gg n$. Remark 4.1, the hyperrectangle case, is the version most used in practice.

The results are proved on paper; none is formalized on the platform. A formal development produces machine-checked versions of the smooth-max sandwich, a Gaussian anti-concentration bound (Nazarov's inequality), a quantitative Gaussian comparison inequality and the bootstrap theorem itself. The comparison display and Lemma A.1 are proved in the paper only by citation ([20] and Klivans–O'Donnell–Servedio, Thm. 20), so formal proofs of them are new work rather than transcriptions.

Difficulty

The obvious route compares $S^{eX}_n$ and $S^Y_n$ through the Kolmogorov distance of their laws or through a total-variation bound between two Gaussians. Both depend polynomially on $p$ and fail when $p\gg n$. The proof instead compares smooth functionals of the coordinatewise maximum, where the error depends on $p$ only through $\beta\sim\log p$, and then converts back to probabilities of orthants with an anti-concentration inequality whose constant grows like $\sqrt{\log p}$. Both conversions must hold uniformly in the threshold $y$, and the final bound for simple convex sets requires passing to the $m$-dimensional vectors $(v'X_i)_{v\in\mathcal V}$ with $m\le(pn)^d$, which is why $\log(pn)$ appears. The comparison inequality for $g\circ F_\beta$ is the step with the least existing infrastructure: it is a Slepian–Stein interpolation between two Gaussian laws with explicit control of second derivatives of $F_\beta$.

Formalization scope

• Vectors live in EuclideanSpace ℝ (Fin p); $N(0,\Sigma)$ is Mathlib's multivariateGaussian 0 Σ. Independence is iIndepFun; $Y_i$'s law is fixed by P.map (Y i) = multivariateGaussian 0 (covMat P (X i)), and square integrability of each $X_{ij}$ makes covMat positive semidefinite, so this is the genuine Gaussian law.
• $n\ge4$ and $p\ge3$ (the paper's standing assumption) are hypotheses of every theorem.
• $P(\cdot\mid X_1^n)$ is read per realization: the bootstrap law mbLaw x is the push-forward of $N(0,1)^{\otimes n}$ under $e\mapsto n^{-1/2}\sum_ie_i(x_i-\bar x)$, and the bound is asserted at every $\omega$ on the event, for the data $X(\omega)$. Since $e$ is independent of the data, this is a version of the conditional law; no conditional expectation appears.
• Suprema over the class, over $v_1,v_2$ and over hyperrectangles are encoded as bounds for every member.
• The class $\mathcal A$ is an indexed family of measurable sets, each with its approximating polyhedron given by a finite set of unit vectors and real thresholds. The page uses facet normals and support values; allowing any finite family of unit vectors is a mild generalization that implies the page's theorem.
• Constants: $C$ is quantified after $a,b,d$ (after $b$ alone for (38), (39), Lemma A.1 and the smoothed step) and before $n$, $p$, the probability space, the data, the class, $\bar\Delta_n$ and the realization. A constant chosen after $n$ or $p$ would trivialize the goal.
• Moments enter only through lower bounds ((M.1), (M.1′)) on integrals of square-integrable functions, so no integral takes a default value; the comparison display integrates continuous functions of linear growth against Gaussian laws. The goal does not mention $F_\beta$, $g$, $\varrho_n^{MB}$, (38) or (39).

Infrastructure needed: multivariate Gaussian laws and their linear images, Gaussian integration by parts or Slepian interpolation, Nazarov's inequality, and properties of log-sum-exp. Lemma A.1, display (21) and the comparison display are reusable beyond this mission, for the high-dimensional CLT of the companion mission and for any max-type Gaussian approximation. Proofs of any milestone are welcome, as are proofs of the conditional Gaussianity identity from Mathlib's Gaussian API.

Selected references

• V. Chernozhukov, D. Chetverikov, K. Kato, Central limit theorems and bootstrap in high dimensions, Ann. Probab. 45(4):2309–2352, 2017. https://doi.org/10.1214/16-AOP1113
• V. Chernozhukov, D. Chetverikov, K. Kato, Comparison and anti-concentration bounds for maxima of Gaussian random vectors, Probab. Theory Related Fields 162:47–70, 2015. https://doi.org/10.1007/s00440-014-0565-9
• V. Chernozhukov, D. Chetverikov, K. Kato, Gaussian approximations and multiplier bootstrap for maxima of sums of high-dimensional random vectors, Ann. Statist. 41(6):2786–2819, 2013. https://doi.org/10.1214/13-AOS1161
• A. Klivans, R. O'Donnell, R. Servedio, Learning geometric concepts via Gaussian surface area, FOCS 2008. https://doi.org/10.1109/FOCS.2008.64
• F. Nazarov, On the maximal perimeter of a convex set in ℝⁿ with respect to a Gaussian measure, Geometric Aspects of Functional Analysis, Lecture Notes in Math. 1807, 169–187, 2003. https://doi.org/10.1007/978-3-540-36428-3_14

Motivation

Many statistical procedures look at a large number of averages at once: simultaneous confidence intervals for $p$ means, multiple testing of $p$ hypotheses, the maximum of $p$ $t$-statistics. Their calibration needs the joint law of a $p$-dimensional normalized sum, and in modern applications $p$ is comparable to, or much larger than, the sample size $n$. Classical multivariate central limit theorems with explicit error, such as Bentkus's bound over convex sets (Bentkus 2003), require $p$ to grow slowly with $n$ (roughly $\sqrt p = o(n^{1/7})$), which rules out these applications.

Chernozhukov, Chetverikov and Kato showed that when the class of sets is restricted to hyperrectangles, the Gaussian approximation error depends on the dimension only through $\log p$ (Ann. Probab. 45 (2017)).

Timeline. In 2013 the same authors proved a Gaussian approximation for the maximum of a sum (sets of the form $\{w : w_j \le a \ \forall j\}$) with rate $n^{-1/8}$ (Ann. Statist. 41 (2013)). The 2017 paper extends this to all hyperrectangles, improves the rate to $n^{-1/6}$, and adds bootstrap results.

Setting

Let $n \ge 4$ and $p \ge 3$. Let $X_1, \dots, X_n$ be independent random vectors in $\mathbb R^p$ with coordinates $X_{ij}$, each centred ($\mathrm E[X_{ij}] = 0$) with $\mathrm E[X_{ij}^2] < \infty$. Let $Y_1, \dots, Y_n$ be independent centred Gaussian vectors with $Y_i \sim N(0, \mathrm E[X_iX_i'])$, the same covariance as $X_i$. The normalized sums are

$$S^X_n := \frac{1}{\sqrt n}\sum_{i=1}^n X_i, \qquad S^Y_n := \frac{1}{\sqrt n}\sum_{i=1}^n Y_i.$$

A hyperrectangle is a set $A = \{w \in \mathbb R^p : a_j \le w_j \le b_j \text{ for all } j\}$ with $-\infty \le a_j \le b_j \le \infty$; $\mathcal A^{\mathrm{re}}$ is the class of all of them. The quantity to bound is

$$\rho_n(\mathcal A^{\mathrm{re}}) := \sup_{A \in \mathcal A^{\mathrm{re}}}\big|\mathrm P(S^X_n \in A) - \mathrm P(S^Y_n \in A)\big|.$$

The error is measured through the third-moment parameter $L_n := \max_j n^{-1}\sum_i \mathrm E|X_{ij}|^3$ and the truncated maximal moments

$$M_{n,X}(\phi) := \frac1n\sum_{i=1}^n \mathrm E\Big[\max_j|X_{ij}|^3\,1\Big\{\max_j|X_{ij}| > \frac{\sqrt n}{4\phi\log p}\Big\}\Big],$$

$M_{n,Y}(\phi)$ the same with $Y$, and $M_n(\phi) := M_{n,X}(\phi) + M_{n,Y}(\phi)$. Here $\log$ is the natural logarithm.

Formalization targets

Goal: Theorem 2.1

If $n^{-1}\sum_i \mathrm E[X_{ij}^2] \ge b > 0$ for all $j$, there are constants $K_1, K_2 > 0$ depending only on $b$ such that for every $\bar L_n \ge L_n$,

$$\rho_n(\mathcal A^{\mathrm{re}}) \le K_1\left[\left(\frac{\bar L_n^2\log^7 p}{n}\right)^{1/6} + \frac{M_n(\phi_n)}{\bar L_n}\right], \qquad \phi_n := K_2\left(\frac{\bar L_n^2\log^4 p}{n}\right)^{-1/6}.$$

The constants are left existential, as on the page: the goal asserts the shape of the bound, not particular values.

Milestones

1. Display (21): the smooth maximum $F_\beta(w) = \beta^{-1}\log\sum_j e^{\beta(w_j - y_j)}$ is within $\beta^{-1}\log p$ of $\max_j(w_j - y_j)$.
2. Lemma B.1: association inequalities for nondecreasing nonnegative functions, including (20) without independence.
3. Lemma A.1 (Nazarov's inequality): $\mathrm P(Y \le y + a) - \mathrm P(Y \le y) \le Ca\sqrt{\log p}$ for a centred Gaussian $Y$ with $\mathrm E[Y_j^2] \ge b$.
4. Lemma 5.1, the key lemma: a recursive bound on $\varrho_n := \sup_{y, v\in[0,1]}|\mathrm P(\sqrt v S^X_n + \sqrt{1-v}S^Y_n \le y) - \mathrm P(S^Y_n \le y)|$.
5. Corollary 5.1: the same bound for $\varrho_n'$, the supremum over hyperrectangles.
6. Lemma C.1: an exponential tail bound gives $\mathrm E[\xi^3 1\{\xi > t\}] \le 6A(t+B)^3e^{-t/B}$.

Companion: Proposition 2.1

Under the moment conditions (M.1)–(M.2) and either an exponential (E.1) or a polynomial (E.2) moment bound with parameter $B_n \ge 1$,

$$\rho_n(\mathcal A^{\mathrm{re}}) \le C\Big(\frac{B_n^2\log^7(pn)}{n}\Big)^{1/6} \quad\text{or}\quad \rho_n(\mathcal A^{\mathrm{re}}) \le C\Big\{\Big(\frac{B_n^2\log^7(pn)}{n}\Big)^{1/6} + \Big(\frac{B_n^2\log^3(pn)}{n^{1-2/q}}\Big)^{1/3}\Big\}.$$

Significance

The result. Under the exponential moment condition (E.1), Proposition 2.1 makes the Gaussian approximation error tend to zero when $B_n^2\log^7(pn) = o(n)$, allowing $p$ much larger than $n$. Under the polynomial moment condition (E.2), its second error term must also tend to zero. Theorem 2.1 is the probabilistic basis of the paper's multiplier and empirical bootstrap results for simultaneous inference (Chernozhukov, Chetverikov and Kato 2017).

Formalizing it. The result is proved on paper; no machine-checked version of this theorem was found in the platform catalog during this mission's prior-art search. A formal proof needs interpolation between $S^X_n$ and $S^Y_n$, Gaussian anti-concentration (Nazarov's inequality), and third-order Taylor estimates of smooth approximations of indicator functions. Nazarov's inequality is used in the paper by citation, so its formal proof is a separate milestone.

Difficulty

The obvious route, a Lindeberg replacement of each $X_i$ by $Y_i$ after smoothing the indicator of a hyperrectangle coordinate by coordinate, loses a polynomial factor in $p$: the derivatives of a product of $p$ smoothed one-dimensional indicators add up over coordinates, so the error grows like a power of $p$ rather than of $\log p$. Any smoothing must also be paid for by the probability that the Gaussian vector falls in a thin neighbourhood of the boundary of a hyperrectangle, and a dimension-free bound on that probability is not available for general hyperrectangles; the $\sqrt{\log p}$ anti-concentration bound is the best one can use. Finally, a direct comparison yields an inequality in which the quantity to be bounded appears on both sides, and the rate $n^{-1/6}$ is obtained only after that inequality is solved; a one-shot estimate gives a worse power of $n$. The truncation in $M_n(\phi)$ handles coordinates too large for a third-order Taylor expansion, since no moment condition beyond third moments is assumed.

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin p) and the coordinate $X_{ij}$ is X i ω j. The Gaussian comparison vectors satisfy P.map (Y i) = multivariateGaussian 0 (covMat P (X i)) with covMat P Z = (E[Z_j Z_k])_{j,k}, which is positive semidefinite, so this is the genuine $N(0, \mathrm E[X_iX_i'])$; the $Y_i$ are independent. Hyperrectangle endpoints are extended reals used only in comparisons. Every theorem carries the standing assumptions $n \ge 4$, $p \ge 3$, independence, centring and finite second moments. Items that involve $L_n$ or $M_n$ add $\mathrm E|X_{ij}|^3 < \infty$; when a third moment is infinite the paper's bounds are vacuous, so this loses nothing. $M_n(\phi)$ is defined by its formula for every real $\phi$, because Theorem 2.1 evaluates it at $\phi_n$, which may be below $1$. Lemma 5.1 and Corollary 5.1 assume the $Y$'s independent of the $X$'s, as the definition of $\varrho_n$ does; Theorem 2.1 and Proposition 2.1 do not. A bound on a supremum is stated set by set.

Constants that the paper says depend only on $b$ (or on $b$ and $q$) are quantified after $b$ and before $n$, $p$, the probability space and every random vector; a constant chosen after $n$, $p$ or the law would trivialize every statement. Upper bounds on expectations in hypotheses ((M.2), (E.1), (E.2)) and in Lemma C.1's conclusion are lower Lebesgue integrals, so a non-integrable function cannot make a hypothesis hold with a junk value of $0$. Dropping the independence of the $Y_i$ or using a wrong covariance would make the goal false.

A complete development needs: a multivariate Stein or Slepian interpolation, third-order Taylor expansion with remainder for functions on $\mathbb R^p$, Gaussian integration by parts, and Nazarov's inequality. The anti-concentration and smooth-max lemmas are reusable for any max-type Gaussian approximation, including the bootstrap results of the second mission of this series. Proofs of individual milestones, of Nazarov's inequality in particular, are welcome on their own.

Selected references

• V. Chernozhukov, D. Chetverikov, K. Kato, Central limit theorems and bootstrap in high dimensions, Ann. Probab. 45(4):2309–2352, 2017. https://doi.org/10.1214/16-AOP1113
• V. Chernozhukov, D. Chetverikov, K. Kato, Gaussian approximations and multiplier bootstrap for maxima of sums of high-dimensional random vectors, Ann. Statist. 41(6):2786–2819, 2013. https://doi.org/10.1214/13-AOS1161
• V. Bentkus, On the dependence of the Berry–Esseen bound on dimension, J. Statist. Plann. Inference 113:385–402, 2003. MR1965117, https://mathscinet.ams.org/mathscinet-getitem?mr=1965117
• F. Nazarov, On the maximal perimeter of a convex set in ℝⁿ with respect to a Gaussian measure, Geometric Aspects of Functional Analysis, Lecture Notes in Math. 1807, 169–187, Springer, 2003. MR2083397, https://mathscinet.ams.org/mathscinet-getitem?mr=2083397

Motivation

Many scheduling decisions are not owned by a single decision maker. A machine shared by two departments, a production line serving two customers, or a computing resource shared by two users must process the jobs of two agents, each of which judges a schedule by its own criterion. Agnetis, Mirchandani, Pacciarelli and Pacifici introduced this model in Scheduling Problems with Two Competing Agents (Operations Research, 2004, doi:10.1287/opre.1030.0092), and it became the starting point of the literature on multi-agent scheduling (surveyed in Agnetis, Billaut, Gawiejnowicz, Pacciarelli and Soukhal, Multiagent Scheduling, Springer, 2014, doi:10.1007/978-3-642-41880-8).

When neither agent can impose its criterion on the other, the natural object to compute is the set of compromises that cannot be improved for one agent without hurting the other: the Pareto frontier. Section 11 of the paper asks how large that frontier can be for each pair of criteria it studies, because the size of the frontier decides whether it can be listed in polynomial time. This mission formalizes the answer for one agent minimizing its total completion time against the other agent's maximum cost.

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}$, with $n_B\ge 1$. Every job $J_j$ has a positive processing time $p_j$, is available at time $0$, and is processed without interruption on a single machine that handles one job at a time. Since both criteria below are nondecreasing in completion times, a schedule $\sigma$ is a sequence of all $n_A+n_B$ jobs processed in that order from time $0$ without idle time, and $C_j(\sigma)$ denotes the completion time of $J_j$.

• Agent $A$ wants to minimize its total completion time $\sum_{h=1}^{n_A} C^A_h(\sigma)$.
• Each $B$-job has a nondecreasing cost function $f^B_k$ of its completion time, and agent $B$ wants to minimize its maximum cost $f^B_{\max}(\sigma)=\max_k f^B_k(C^B_k(\sigma))$.

A schedule $\sigma$ is nondominated if no schedule $\bar\sigma$ has $\sum C^A_h(\bar\sigma)\le\sum C^A_h(\sigma)$ and $f^B_{\max}(\bar\sigma)\le f^B_{\max}(\sigma)$ with at least one inequality strict. Its nondominated pair is $\bigl(\sum C^A_h(\sigma),f^B_{\max}(\sigma)\bigr)$. The constrained problem $1\|\sum C^A_i : f^B_{\max}\le Q$ asks for a schedule with $f^B_k(C^B_k)\le Q$ for every $B$-job that minimizes $\sum C^A_h$ among such schedules; such a schedule is optimal for the bound $Q$.

The $A$-jobs of a schedule follow the SPT order when they appear by nondecreasing processing time, equal lengths in index order. A $B$-job overtakes an $A$-job when it moves from after it to before it.

Formalization targets

Goal: Theorem 11.6, corrected

$$\bigl|\{(\textstyle\sum C^A_h(\sigma),\,f^B_{\max}(\sigma)) : \sigma\ \text{nondominated}\}\bigr|\ \le\ n_A\,n_B+1.$$

The paper prints the bound $n_An_B$. That bound is false: with one job per agent, unit processing times and $f^B(t)=t$, the schedules $AB$ and $BA$ give the two nondominated pairs $(1,2)$ and $(2,1)$. The corrected bound $n_An_B+1$ is the one the printed argument supports.

Milestones

1. Lemma 5.4 (p. 234): if no $B$-job can complete last within the bound, every optimal schedule ends with a longest $A$-job. This is the reason the $A$-jobs of optimal schedules are in SPT order.
2. Lemma 11.4 (p. 240): for $Q'<Q$ and optimal schedules $\sigma,\sigma'$ for $Q$ and $Q'$ whose $A$-jobs follow the SPT order, $C_j(\sigma')\ge C_j(\sigma)$ for every $A$-job $j$.
3. Lemma 11.5 (p. 240): under the same hypotheses, if a $B$-job precedes an $A$-job in $\sigma$, it precedes it also in $\sigma'$.

Significance

A frontier of size at most $n_An_B+1$ means that the scheme the paper calls PP, which solves the constrained problem for a decreasing sequence of bounds, lists every nondominated pair with polynomially many calls to a polynomial algorithm (Theorem 5.5 of the paper). The contrast with the other criteria of §11 is the point: for two total-completion-time agents the paper exhibits an exponential frontier (Example 11.7). The bound therefore separates criteria whose compromises can be negotiated over an explicit list from those where they cannot.

Formalizing it adds three things. First, the printed statements need corrections: the bound is off by one, and Lemmas 11.4 and 11.5 are false when identical $A$-jobs may be ordered differently in the two schedules. A machine-checked version fixes the exact hypotheses. Second, the monotonicity of overtakes (Lemma 11.5) is a reusable structural fact about parametric scheduling under a tightening constraint. Third, no part of this paper or of two-agent scheduling has been machine-checked before, to our knowledge; the published sequence model the mission builds on comes from the formalization of Moore's 1968 algorithm.

Difficulty

The obvious argument counts overtakes: as the bound decreases, each $B$-job overtakes each $A$-job at most once, so consecutive frontier points differ by at least one new overtake. The step that does not go through as printed is "at most once". Optimal schedules for a given bound are not unique, and two optimal schedules can disagree on the order of identical $A$-jobs and on the position of a $B$-job between them. Then an "overtake" can be undone between two bounds without any change in the objectives. The counting is valid only for a consistently chosen family of schedules, and turning the comparison of optimal schedules for two different bounds into a strict improvement needs an exchange argument with careful bookkeeping of which jobs shift. A second, smaller gap is the base case: the first schedule of the chain carries no overtake and must be counted separately.

Formalization scope

Jobs are Fin nA ⊕ Fin nB, 0-based, and a schedule is a duplicate-free list of all jobs; completion times come from the published definition MooreLateJobs.Shared.completionTime (Moore 1968 series), referenced rather than redefined. Processing times are real and strictly positive, the paper's standing convention, which the exchange arguments use. The bound $Q$ is real; the paper's integer $Q$ is a special case. Feasibility for the bound is stated job by job. The maximum cost $f^B_{\max}$ is a finite maximum and requires $n_B\ge 1$.

Explicit readings of the paper's phrases:

• "Nondominated schedules" in Theorem 11.6 is read as nondominated pairs, one schedule per pair, as §11 defines the set it enumerates. Counting schedules would count swaps of identical jobs separately.
• The count is Set.encard of a set of real pairs, so the goal asserts finiteness as well as the bound; it is not a Set.ncard, which would be $0$ on an infinite set.
• "The $A$-jobs are always SPT ordered" (p. 240) is read as the SPT order with ties broken by index, imposed as a hypothesis on both schedules in Lemmas 11.4 and 11.5. Without a fixed tie-break both lemmas are false.
• Lemma 5.4 is restated with $n_A\ge 1$, since an empty schedule has no last job. It is also a milestone of mission 3 of this series and is restated here identically because draft items cannot import each other.

Nothing in the statements is trivial by construction. The goal is about every instance with positive data, its hypotheses are satisfiable, and the counterexample to the printed bound is checked in Lean. The milestones' SPT hypotheses are met by some optimal schedule of every feasible instance, so they are not vacuous. Running times, including the polynomiality of PP and the choice of the decrement $\epsilon$ in Figure 4, are not formalized.

A complete development needs exchange lemmas for single-machine sequences (moving a job, swapping two adjacent jobs, and their effect on completion times), the existence of SPT-ordered optimal schedules, and a chain-counting argument for nested sets of overtakes. The exchange lemmas are reusable for any single-machine sequencing mission. Contributions of any of these, and of a proof of the corrected bound that avoids the scheme PP, are welcome.

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
• 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
• 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

Why composition matters

Optimization models often build an objective from several intermediate quantities: constraints, penalties, and transformed measurements are evaluated first, then combined by an outer function. These intermediate and outer functions can be Lipschitz without being differentiable at the point of interest. Ordinary differentiation supplies no chain rule there. The generalized-gradient framework gives a set of possible first-order slopes, while semismoothness provides stronger directional behavior along sequences approaching the point. Mifflin's IIASA report asks whether this behavior survives such compositions and how the generalized gradient of the result relates to those of its ingredients.

The report first establishes basic properties of the generalized gradient in §2, including almost-everywhere differentiability and a nonsmooth mean value theorem. Section 4 then states a chain-rule inclusion as Theorem 4 and the semismooth composition result as Theorem 5. The report is dated December 1976; a journal version appeared in 1977. The mission cites theorem numbers and pages from the report version throughout. No claim about differences between the report and journal texts is needed here.

Setting and definitions

Work in finite-dimensional Euclidean spaces. Let $f_i:\mathbb R^n\to\mathbb R$, for $i=1,\ldots,m$, be component functions, and let $E:\mathbb R^m\to\mathbb R$ be an outer function. Define the component map $Y$ and the composite $F$ by

$$Y(x)=(f_1(x),\ldots,f_m(x)),\qquad F(x)=E(Y(x)).$$

The functions are locally Lipschitz in the report's precise sense: on each bounded subset of their Euclidean domain they have a finite Lipschitz constant. For a scalar function $H$, a point $x$, and a direction $d$, the generalized directional derivative $H^0(x;d)$ is the joint upper limit of $[H(x+h+td)-H(x+h)]/t$ as $h\to0$ and $t\downarrow0$. Its associated generalized gradient is the support set

$$\partial H(x)=\{g:\langle g,d\rangle\le H^0(x;d)\text{ for every direction }d\}.$$

This is the definition used in Mifflin's report, not an identification assumed in advance with a hull of ordinary gradient limits. Proposition 1(c) supplies that identification under the paper's Lipschitz assumption. The ordinary one-sided directional derivative $H'(x;d)$ is the limit of $[H(x+td)-H(x)]/t$ for $t\downarrow0$, when that limit exists.

Mifflin calls $H$ semismooth at $x$ if it is Lipschitz on a ball about $x$ and the scalar sequence $\langle g_k,d\rangle$ has exactly one accumulation point whenever $t_k>0$ tends to zero, $\theta_k/t_k\to0$, and $g_k\in\partial H(x+t_kd+\theta_k)$. The quantification is over every direction and every such sequence. This pointwise condition is Definition 1 of the report, and its link to one-sided directional derivatives is Lemma 2.

To state the chain rule, form the set

$$G(x)=\operatorname{conv}\left\{\sum_{i=1}^{m}w_i g^i:g^i\in\partial f_i(x)\text{ for every }i,\quad w\in\partial E(Y(x))\right\}.$$

The same $w$ is used across all components. The sum is the action of the report's matrix $[g^1\cdots g^m]$ on $w$.

Formalization targets

Generalized-gradient chain rule

Theorem 4 asserts that $F$ is locally Lipschitz and that, at every point,

$$\partial F(x)\subseteq G(x).$$

This is an inclusion, not a general equality. The report gives an example immediately after Theorem 4 in which the inclusion is strict: two identical absolute-value components cancel under an outer difference, while $G(0)$ remains larger than $\partial F(0)$.

Semismooth composition

The goal, Theorem 5, assumes the setting of Theorem 4. If each $f_i$ is semismooth at a selected $x$ and $E$ is semismooth at $Y(x)$, then

$$E\circ Y\text{ is semismooth at }x.$$

The conclusion is pointwise. It does not assert semismoothness throughout $\mathbb R^n$ from hypotheses at one point. The milestone list contains the chain rule and the source's stated support results: Proposition 2, Lemma 1, Proposition 1(c) and (d), Lemma 2, and the claims (4.2) and (4.11)–(4.12) from the proofs.

What the results provide

Theorem 5 permits composite nonsmooth objectives to be treated within the same semismooth class as their components. Theorem 4 gives a concrete set built from component generalized gradients that contains the composite's generalized gradient. Together, they let later statements about a composite use first-order information from its stated ingredients, subject to the inclusion's possible strictness. These are results proved in Mifflin's report, not open mathematical conjectures.

This mission drafts machine-checkable statements of those known results and their definition layer. The local Lean modules compile with proof placeholders; this staging does not supply machine-checked proofs of the theorems. A complete development would formalize the known arguments or another proof of the same statements. The reusable output would include the support-set generalized gradient, sequence-based semismoothness, the nonsmooth mean value result, and the chain-rule inclusion, all with their source assumptions exposed.

Main difficulty

At a point where $F$ is differentiable, the component functions $f_i$ need not be differentiable, and the outer function $E$ need not be differentiable at $Y(x)$. The ordinary smooth chain rule therefore cannot simply multiply ordinary gradients. The candidate $G(x)$ is a convex set of combinations of generalized gradients; a single chosen combination does not in general describe all nearby limiting slopes. The report's strict-inclusion example also shows why replacing Theorem 4 by equality would be false. For semismoothness, the condition concerns every admissible sequence of generalized gradients near the point, so checking just one path or one gradient selection does not establish Theorem 5.

Formalization scope

The Lean domain is EuclideanSpace ℝ (Fin n) and the outer domain is EuclideanSpace ℝ (Fin m). The report's norm is the Euclidean norm and its pairing is the real inner product. An index of type Fin m represents the $m$ components; $m=0$ is admitted, in which case the component space is a point and the composite is constant. A finite sum represents the column-matrix product. The generalized gradient is defined by all directional support inequalities, so Proposition 1(c) remains a theorem rather than becoming true by definition.

The generalized directional derivative is imported from the published definition matching the report's joint limit. Lean's real limsup has a default value for an unbounded quotient; Lipschitz hypotheses are carried wherever that operation is used. “Locally Lipschitz” is imported as Lipschitzness on every bounded subset, and the explicit constants of §2 use nonnegative reals, equivalent to the report's positive constants by enlarging them. The directional derivative is a relation asserting a limit, so no value is assigned when the limit fails. “Exactly one accumulation point” remains an existence-and-uniqueness assertion about cluster points. The report's $t_k\downarrow0$ means positive convergence to zero, as its proof of Lemma 2 says explicitly. These choices exclude a vacuous formulation that only asks about one convenient sequence or gives a default directional value.

The scope includes the two local definition files and the cited theorem statements, including both conclusions of Theorem 4 and Lemma 2. Proof contributions would need finite-dimensional Lipschitz and differentiability infrastructure, limiting-gradient compactness, convex hull and separation facts, and sequence convergence facts. Results about the alternative Qi–Sun vector-valued semismoothness notion are outside this mission's definition layer.

Selected references

• R. Mifflin, Semismooth and Semiconvex Functions in Constrained Optimization, IIASA Research Report RR-76-21, December 1976. Report PDF.
• R. Mifflin, “Semismooth and Semiconvex Functions in Constrained Optimization,” SIAM Journal on Control and Optimization 15(6), 1977. DOI. This mission's page and theorem references are to the IIASA report.

Motivation

A graph is 3-colorable if its vertices can be colored with three colors so that adjacent vertices get different colors. Deciding 3-colorability is NP-complete in general, and one of the standard ways to map the boundary between easy and hard cases is to forbid an induced subgraph. For the path $P_t$ on $t$ vertices, 3-colorability of $P_6$-free graphs was known to be polynomial (Randerath and Schiermeyer, 2004, reference [21] of the paper), and Randerath, Schiermeyer and Tewes asked in 2002 whether the same holds for $t = 7$.

Bonomo, Chudnovsky, Maceli, Schaudt, Stein and Zhong (Combinatorica, 2017) answered this question. Their Theorem 1 states that the list version, in which every vertex $v$ may only receive a color from a prescribed list $L(v) \subseteq \{1,2,3\}$, can be decided for $P_7$-free graphs in time $O(|V(G)|^{21}(|V(G)|+|E(G)|))$. The algorithm first reduces the instance to a polynomial number of configurations described by a seed, and then calls Lemma 11 (p. 14) on each configuration. Lemma 11 rests on one structural fact about $P_7$-free graphs, Claim 13 (p. 16), which is the goal of this mission.

Timeline:

• 2002: Randerath, Schiermeyer and Tewes ask whether 3-colorability of $P_7$-free graphs is polynomial.
• 2004: Randerath and Schiermeyer give a polynomial algorithm for $P_6$-free graphs.
• 2017: Bonomo et al. give a polynomial algorithm for list 3-coloring of $P_7$-free graphs; Claims 12 and 13 are its structural core.
• As of the paper, no $t$ is known for which 3-coloring $P_t$-free graphs is NP-complete (p. 2); the case $t = 8$ is open.

Setting

All graphs are finite and simple. For a set $S$ of vertices of a graph $G$, $N(S)$ is the set of vertices outside $S$ with a neighbor in $S$, and $\overline{S} = S \cup N(S)$. A graph is $P_t$-free if it has no induced subgraph isomorphic to $P_t$.

A palette $L$ assigns each vertex a list $L(v) \subseteq \{1,2,3\}$. A seed of $(G,L)$ is a nonempty set $S$ that induces a connected subgraph, is 2-dominating (every vertex is at distance at most $2$ from $S$), and satisfies $|L(v)| = 1$ for $v \in S$ and $|L(v)| = 2$ for $v \in N(S)$.

The Lemma 11 setting consists of a graph $G$, a palette $L$ and a seed $S$ such that

1. $G$ is connected and $P_7$-free;
2. adjacent $v \in S$ and $w \in N(S)$ have disjoint lists;
3. the set $X$ of vertices with $|L(v)| = 3$ is stable and anticomplete to $V(G) \setminus (\overline{S} \cup X)$;
4. no vertex of $X$ has a connected neighborhood.

For $i \in \{1,2,3\}$, $D_i$ is the set of $v \in N(S)$ with $L(v) = \{1,2,3\} \setminus \{i\}$, and $N_i(x) = N(x) \cap D_i$. For $\{i,j,k\} = \{1,2,3\}$, $X_i$ is the set of $x \in X$ for which $N_j(x)$ is not complete to $N_k(x)$, and for $x \in X_i$ the paper fixes non-adjacent $n_j(x) \in N_j(x)$, $n_k(x) \in N_k(x)$.

Formalization targets

Goal: Claim 13 (p. 16)

In the Lemma 11 setting, let $\{i,j,k\} = \{1,2,3\}$, $x, y \in X_i$, and let $n_j \in N_j(x)$, $n_k \in N_k(x)$ be non-adjacent. Then

$$\exists\, a \in \{x, n_j, n_k\},\ \exists\, b \in \{y, n_j(y), n_k(y)\}:\quad ab \in E(G).$$

Milestones

1. Display (1), p. 6. For a seed $S$ and two non-adjacent $v, w \in N(S)$ there is an induced $v$–$w$ path on at least $3$ vertices whose inner vertices lie in $S$.
2. p. 15. For $d \in D_i$ and $s \in S \cap N(d)$, $L(s) = \{i\}$.
3. p. 15. No vertex of $X$ has a neighbor in $S$.
4. Claim 12, p. 15. For $i \ne j$, $u_i, v_i \in D_i$, $u_j, v_j \in D_j$ with $\{u_i, v_i, u_j, v_j\}$ stable, there is an induced path $P$ with ends $a, b$ among them such that $\{a,b\} \ne \{u_i,u_j\}$, $\{a,b\} \ne \{v_i,v_j\}$, the interior $P^*$ lies in $S$, and $P^*$ is anticomplete to the other two vertices.

Significance

Claim 13 says that the neighbor triples $\{x, n_j(x), n_k(x)\}$ of the vertices of $X_i$ pairwise touch. This is what allows the proof of Lemma 11 (Claims 14 to 17) to refine the palette of all of $X_i$ simultaneously with only polynomially many guesses: without it, the vertices of $X_i$ could interact independently and the number of cases would be exponential. Claim 12 and display (1) are the general tools for building long induced paths through a seed, used throughout §3.1.

The paper's result is proved and published. None of it is formalized in a proof assistant as far as the platform's index shows. This mission produces a machine-checked version of the structural core of Lemma 11, and the definitions it needs (seeds, the Lemma 11 setting, the sets $D_i$ and $N_i(x)$) are reusable for the rest of the paper's argument.

Difficulty

The proof of Claim 13 is short on paper, but it assembles an induced $P_7$ from three pieces: the path through $S$ given by Claim 12 and the two short paths $n_j - x - n_k$ and $n_j(y) - y - n_k(y)$. Showing that the union is induced requires every non-adjacency between the pieces, and these come from different hypotheses: the stability of $X$, the fact that $X$ has no neighbor in $S$, the list structure of the vertices of $S$ next to $D_i$, and part (c) of Claim 12. Claim 12 itself is an extremal argument (choose the neighbor closest to an end of a path), which in a formal setting requires explicit manipulation of paths as sequences of vertices: splitting, reversing and concatenating them while keeping them induced. The obvious approach of taking any shortest path through $S$ between two of the four vertices fails, because such a path can have interior vertices adjacent to the other two.

Formalization scope

Graphs are SimpleGraph V on a finite type V with decidable equality; vertex sets are Finset V. The colors $1,2,3$ are 0,1,2 in Fin 3, and a palette is V → Finset (Fin 3). $P_7$-freeness is the negation of Mathlib's induced containment IsIndContained of pathGraph 7; ordinary subgraph containment would be a different, much stronger condition. Connectedness uses Mathlib's Connected, which includes nonemptiness. An induced path is the published platform definition StrongPerfectGraph.Main.IsInducedPath (a nonempty list of distinct vertices in which two vertices are adjacent exactly when consecutive); its ends are the first and last list entries and its interior $P^*$ is the list with both ends removed.

The Lemma 11 setting is a structure Lemma11Hyp G L S bundling its hypotheses. Lemma 11's own conclusion, a decision procedure with running time $O(|V(G)|^9(|V(G)|+|E(G)|))$, and the running time of Theorem 1 are not formalized, since there is no machine model. The paper's arbitrary choice of $n_j(y), n_k(y)$ is replaced by quantification over every non-adjacent pair $m_j \in N_j(y)$, $m_k \in N_k(y)$, which is Claim 13 for every possible choice. The case $x = y$ is allowed.

One hypothesis is added to Claim 12: the four vertices $u_i, v_i, u_j, v_j$ are pairwise distinct, and the ends $a, b$ of the path are required to be distinct. The paper's proof and its use in Claim 13 take the four vertices distinct; without the assumption the claim can fail, and without $a \ne b$ a one-vertex path would satisfy it vacuously.

The following trivializing readings are excluded: dropping the overline in "anticomplete to $V(G) \setminus (\overline{S} \cup X)$" (which, together with milestone 3, would force $X$ to be isolated); a one-vertex path or repeated vertices in Claim 12; and subgraph instead of induced-subgraph containment for $P_7$-freeness. The setting is satisfiable with $X \neq \emptyset$: the 5-cycle $y - a - s - t - b - y$ with $S = \{s,t\}$, $L(s) = \{2\}$, $L(t) = \{3\}$, $L(a) = \{1,3\}$, $L(b) = \{1,2\}$, $L(y) = \{1,2,3\}$ satisfies every hypothesis, with $y \in X_1$.

Proofs of the milestones and the goal are welcome, as are general lemmas about induced paths as lists (subpaths, concatenation through a connected set) that would serve other graph-theory missions.

Selected references

• F. Bonomo, M. Chudnovsky, P. Maceli, O. Schaudt, M. Stein and M. Zhong, Three-coloring and list three-coloring of graphs without induced paths on seven vertices, Combinatorica 38 (2018) 779–801 (OnlineFirst 2017). https://doi.org/10.1007/s00493-017-3553-8
• B. Randerath and I. Schiermeyer, 3-Colorability ∈ P for P₆-free graphs, Discrete Applied Mathematics 136 (2004) 299–313 (reference [21] of the paper).
• B. Randerath, I. Schiermeyer and M. Tewes, Three-colorability and forbidden subgraphs. II: polynomial algorithms, Discrete Mathematics 251 (2002) 137–153 (reference [22] of the paper).
• E. Camby and O. Schaudt, A new characterization of $P_k$-free graphs, Algorithmica (reference [2] of the paper; the source of Theorem 4, which the other missions of this series use).

Why interpretations

Twin-width is a graph parameter introduced by Bonnet, Kim, Thomassé and Watrigant in Twin-width I: Tractable FO Model Checking (J. ACM 69(1), Article 3, 2021; arXiv:2004.14789). Its main algorithmic consequence is that first-order model checking is fixed-parameter tractable on graphs given with a contraction sequence of bounded width. A parameter of this kind is useful only if the classes it bounds are closed under the constructions that arise in practice. Many such constructions are first-order definable: the complement of a graph, its square (join vertices at distance at most two), the map graph of a planar map. Section 8 of the paper shows that twin-width is stable under every such construction: a first-order interpretation of a class of bounded twin-width has bounded twin-width. Bounded VC-dimension, by contrast, is not preserved (interval graphs have VC-dimension at most two but interpret every graph, p. 3:41).

The result has since become the basis of the "model-theoretic" view of twin-width: bounded twin-width classes are closed under first-order transductions (Theorem 8.1 of the paper), and later work identifies them, among ordered structures, with the monadically dependent classes (Twin-width IV, Bonnet, Giocanti, Ossona de Mendez, Simon, Thomassé and Toruńczyk).

Setting

Let $G$ be a finite simple graph on a vertex set $V$.

Two vertex sets $X,Y$ are homogeneous if all pairs in $X\times Y$ are edges or none is. For a partition $\mathcal P$ of $V$, the red graph $G_{\mathcal P}$ has the parts as vertices, two distinct parts being adjacent when they are not homogeneous. $\mathcal P$ is a $d$-partition if $G_{\mathcal P}$ has maximum degree at most $d$. The graph $G$ has twin-width at most $d$, $\operatorname{tww}(G)\le d$, if there is a sequence of $d$-partitions from the partition into singletons to a partition with at most one part, each obtained from the previous one by merging two parts (p. 3:32).

A prenex formula of depth $\ell$ with two free variables is

$$\varphi(x,y)=Q_1x_1\,Q_2x_2\cdots Q_\ell x_\ell\ \varphi^*,\qquad Q_i\in\{\forall,\exists\},$$

with $\varphi^*$ a Boolean combination of atoms $u=v$ and $E(u,v)$, $u,v\in\{x_1,\dots,x_\ell,x,y\}$. The interpretation $\varphi(G)$ is the graph on $V$ in which distinct $u,v$ are adjacent iff $G\models\varphi(u,v)\wedge\varphi(v,u)$. For a class $\mathcal G$, $\varphi(\mathcal G)$ is the class of all induced subgraphs of the graphs $\varphi(G)$, $G\in\mathcal G$.

The proof works with morphism-trees. The complete tree $MT_k(V)$ has as nodes all tuples $(v_1,\dots,v_i)$ of vertices with $i\le k$, the parent of a tuple being its prefix. Two sibling nodes are equivalent in $(G,\mathcal P)$ if an automorphism of the tree swaps them, preserving equalities and adjacencies among the entries of every tuple and the part of $\mathcal P$ of every entry. A reduction deletes one of two equivalent siblings with its subtree, repeatedly; a reduct admits no further reduction. Two vertices $u,u'$ are adjacent in $E_{\ell+2}(G,\mathcal P)$ when $(u)$ and $(u')$ are equivalent in some reduction of $MT_{\ell+2}(V)$, and $I_{\ell+2}(G,\mathcal P)$ is the partition into the connected components of $E_{\ell+2}(G,\mathcal P)$.

Formalization targets

Goal: Theorem 8.3 (graphs)

For every prenex formula $\varphi(x,y)$ and every $d$ there is $D$ such that

$$\operatorname{tww}(G)\le d\ \Longrightarrow\ \operatorname{tww}\bigl(\varphi(G)[S]\bigr)\le D\quad\text{for every graph } G \text{ and every } S\subseteq V(G).$$

The bound $D$ depends on $\varphi$ and $d$ only. No explicit function is asserted: the paper gives none (the proof goes through a tower-type bound on reducts).

Milestones

1. Lemma 5.2 in graph form (p. 3:18, applied on p. 3:43): $r$-refining $h$-partitions from the finest to the coarsest partition give $\operatorname{tww}(G)\le r(h+1)$.
2. Lemma 7.3 (p. 3:32): reducts of $MT_\ell(G)$ have size bounded by a function of $\ell$.
3. Lemmas 7.11–7.14 (pp. 3:35–3:38): restriction to connected tuples rooted at a part and the pruned shuffle commute with reductions; the pruned shuffle of all $MT_\ell(G,\mathcal P,X)$ is $MT_\ell(G,\mathcal P)$, and that of reducts is a reduction of it.
4. Lemma 8.4 (p. 3:41) and its extension to reductions (p. 3:42): equivalent nodes $(u,v),(u,v')$ of $MT_{\ell+2}$ satisfy the same prenex formulas of depth $\ell$.
5. $I_{\ell+2}$ refines $\mathcal P$ and is monotone under coarsening (p. 3:42).
6. Lemma 8.5 (p. 3:42): a part of a $d$-partition meets boundedly many components of $E_{\ell+2}(G,\mathcal P)$.
7. Lemma 8.6 (p. 3:43): parts of $I_{\ell+2}(G,\mathcal P)$ inside parts at distance at least $3^{\ell+2}$ in $G_{\mathcal P}$ are homogeneous in $\varphi(G)$.

Significance

Theorem 8.3 turns every first-order definable graph construction into a source of bounded-twin-width classes: squares and fixed powers of planar graphs, complements, map graphs (as transductions, via Theorem 8.1), $k$-planar graphs and bounded-degree string graphs. Combined with the model-checking algorithm it gives FPT first-order model checking on all these classes, provided a contraction sequence is available. The theorem is also the first step of the model-theoretic characterisations of bounded twin-width in the later papers of the series.

The result is proved in the paper; no machine-checked proof of it, or of any twin-width bound, exists to our knowledge, and Mathlib has no notion of twin-width or of first-order interpretations of graphs. The mission asks for a formal proof of the graph case. The morphism-tree milestones are also the combinatorial core of the paper's linear-time model-checking algorithm (Theorems 7.5, 7.15), whose running-time statements are not part of this mission.

Difficulty

The obvious approach refines the $d$-partitions $\mathcal P_i$ of $G$ by the "type" of each vertex with respect to $\varphi$. The number of such types is not bounded: a vertex's behaviour depends on the whole graph through the quantifiers. The paper replaces types by the components of $E_{\ell+2}(G,\mathcal P_i)$, defined through reductions of morphism-trees that respect $\mathcal P_i$. Two facts must then be shown, and neither is local in an obvious way. First, the number of components inside a part is bounded (Lemma 8.5); this needs the pruned shuffle, which assembles a reduction of the whole tree $MT_{\ell+2}(G,\mathcal P)$ from reductions of the local trees $MT_{\ell+2}(G,\mathcal P,X)$, and the fact that it commutes with reductions (Lemma 7.12), where an automorphism of one local tree must be extended to the shuffle without breaking adjacency between non-homogeneous parts. Second, far-apart components are homogeneous in $\varphi(G)$ (Lemma 8.6), which needs the evaluation argument of Lemma 8.4 inside a reduction of the partitioned tree.

Formalization scope

• Graphs are SimpleGraph V on a Fintype with decidable equality. Twin-width is the predicate TwinWidthLE G d in the paper's partition form (pp. 3:12, 3:32); trigraphs are not formalized, and twin-width is never an infimum, so no junk value of sInf can make a bound vacuous. Merge steps merge exactly two distinct parts, so a sequence cannot jump to one part.
• Formulas are Mathlib's FirstOrder.Language.graph.Formula (Fin 2), evaluated in G.structure; variable 0 is $x$, variable 1 is $y$. Prenex is Mathlib's IsPrenex; quantifier depth qdepth is defined in the mission ($\exists=\neg\forall\neg$ counts once).
• The interpretation requires $u\neq v$ for an edge (a simple graph has no loops). The goal is the graph case of Theorem 8.3, which the page states for augmented binary structures; Section 8 itself says it works with undirected graphs (p. 3:40).
• In the goal the bound $D$ is chosen after $\varphi$ and $d$ and before the graph: a bound chosen after the graph would make the statement trivial. The hereditary closure (induced subgraphs on every $S$) is part of the statement.
• Morphism-trees are sets of tuples (Set (List V)), the paper's identification of a node with its current path (p. 3:30), which is exact for reductions of complete trees. Equivalent siblings are distinct. Distances in $G_{\mathcal P}$ are in $\mathbb N\cup\{\infty\}$, so disconnected parts are far apart. The sequence graph uses 0-based indices, hence the exponent $3^{\ell-(k+1)}$. The pruned shuffle is defined by its characterisation (each component of the sequence graph of a tuple lies in the tree of its local root). Lemmas of §7.3 carry its standing assumption $\ell>0$.
• Lemma 5.2 is posed for graphs with the bound $r(h+1)$ (the matrix lemma's $rt$ with $t=h+1$).
• Not in the mission: Theorem 8.1 (transductions), Lemma 8.2 and Lemma 5.1 (augmented binary structures), and all running-time statements (Theorems 1.1, 7.1, 7.5, 7.15, Corollaries 7.16–7.17).

Reusable beyond this mission: the partition form of twin-width, quantifier depth of first-order formulas, and the morphism-tree machinery (reductions, pruned shuffles), which formalizes the algorithmic core of first-order model checking on bounded twin-width. Contributions welcome: proofs of the §7 lemmas, of Lemma 8.4 by induction on the quantifier prefix, and the closure of twin-width under induced subgraphs.

Selected references

• É. Bonnet, E. J. Kim, S. Thomassé, R. Watrigant, Twin-width I: Tractable FO Model Checking, J. ACM 69(1), Article 3, 2021. https://doi.org/10.1145/3486655 (arXiv:2004.14789, https://arxiv.org/abs/2004.14789)
• É. Bonnet, U. Giocanti, P. Ossona de Mendez, P. Simon, S. Thomassé, S. Toruńczyk, Twin-width IV: Ordered Graphs and Matrices, J. ACM, 2024. https://arxiv.org/abs/2102.03117

Motivation

Join-the-shortest-queue (JSQ) is the load-balancing rule in which each arriving job is sent to a server with the fewest jobs. It is a baseline in the design of server farms and data centers, and in the many-server Halfin–Whitt regime, where the load per server approaches one at rate $1/\sqrt n$, it combines near-full utilization with vanishing waiting. Eschenfeldt and Gamarnik (arXiv:1502.00999, 2015) proved that the suitably scaled JSQ process converges, over bounded time intervals, to a two-dimensional reflected diffusion; Mukherjee, Borst, van Leeuwaarden and Whiting (J. Appl. Probab. 53, 2016) gave the form of the result that Braverman quotes as Theorem 1. Process-level convergence over bounded time intervals says nothing about the stationary distribution. To conclude that the stationary distributions converge as well, one needs tightness of the scaled stationary distributions, uniformly in the number of servers $n$.

Braverman (arXiv:1801.05121, Math. Oper. Res. 45(3), 2020) supplied this, together with positive recurrence of the diffusion limit. This mission formalizes the first of the two main results, Theorem 2, and the chain of lemmas the paper uses to prove it.

Setting

There are $n$ identical servers, each with its own infinite buffer. Jobs arrive as a Poisson process of rate $n\lambda$ and service times are i.i.d. exponential with mean one. An arriving job joins a server with the fewest jobs, ties broken arbitrarily. The Halfin–Whitt regime is

$$\lambda = 1 - \beta/\sqrt n,\qquad \beta > 0 \text{ fixed}.$$

For $i \ge 1$, $Q_i$ is the number of servers with at least $i$ jobs. The process $Q = (Q_1, Q_2, \dots)$ is a continuous-time Markov chain on

$$S = \Big\{ q \in \{0,1,\dots,n\}^\infty \ \Big|\ q_i \ge q_{i+1},\ \textstyle\sum_i q_i < \infty \Big\}.$$

Its generator $G_Q$ sends $q$ to $q + e^{(i)}$ at rate $n\lambda$ when $q_1 = \dots = q_{i-1} = n > q_i$, and to $q - e^{(i)}$ at rate $q_i - q_{i+1}$. The fluid-scaled coordinates are $X_1 = (Q_1 - n)/n \le 0$, the negative of the fraction of idle servers, and $X_i = Q_i/n$ for $i \ge 2$. The diffusion-scaled coordinates are $\sqrt n X_i$. Expectations $\mathbb E$ are taken under a stationary distribution $\pi$ of the chain.

The proof works with functions on $\Omega = (-\infty, 0] \times [0, \infty)$ and with the first-order operator

$$Lf(x) = (-x_1 + x_2 - \beta/\sqrt n) f_1(x) - x_2 f_2(x),$$

where $f_i$ is the partial derivative in $x_i$, taken one-sided on $\partial\Omega$.

Formalization targets

Goal: Theorem 2

For each $\beta > 0$ there is a constant $C(\beta)$ such that for all $n \ge 1$ with $\beta < \sqrt n$ and every stationary distribution,

$$\mathbb E\big|\sqrt n X_i\big| \le C(\beta),\ \ i = 1, 2,\qquad \mathbb E\big|n X_i\big| \le C(\beta),\ \ i \ge 3.$$

The constant depends on $\beta$ only, not on $n$, the stationary distribution, or $i$.

Milestones, in the order the proof uses them

1. Lemma 1: $\mathbb E\,G_Q f(Q) = 0$ whenever $\mathbb E|f(Q)| < \infty$.
2. Lemma 2: $\mathbb E Q_1 = n\lambda$ and $\mathbb E Q_i = n\lambda\,\mathbb P(Q_1 = \dots = Q_{i-1} = n)$.
3. Lemma 3: the generator, applied to $f(x_1, x_2)$, equals $Lf(x) + (f_2 - f_1)(x)\lambda 1(x_1 = 0) + \varepsilon(x)$ with an explicit remainder $\varepsilon$ built from second weak derivatives.
4. Lemmas 5 and 6: the curve $\Gamma^{(\kappa)}$ and the hitting time $\tau(x)$ of the fluid model; existence and uniqueness, finiteness, derivative formulas and monotonicity in $\kappa$.
5. Lemma 7 and Lemma 4: for $\kappa > \beta$, the explicit function $f^*$ of (4.14) solves

$$Lf(x) = -\big((x_2 - \kappa/\sqrt n)\vee 0\big)\ \text{on } \Omega,\qquad f_1(0, x_2) = f_2(0, x_2),$$

with $f^*_{11}, f^*_{12}, f^*_{22} \ge 0$, vanishing second derivatives for $x_2 \le \kappa/\sqrt n$, and explicit upper bounds of order $\sqrt n/\beta$ above that level. 6. (3.18): $\mathbb E\big((X_2 - \kappa/\sqrt n)\vee 0\big) \le \frac{1}{\beta\sqrt n}\big(12 + \frac{6\kappa}{\kappa - \beta}\big)\mathbb P(X_2 \ge \kappa/\sqrt n - 1/n)$. 7. Theorem 2, (2.2): the $i = 1, 2$ half of the goal.

Significance

Theorem 2 shows that in steady state the number of idle servers and the number of servers holding two or more jobs are $O(\sqrt n)$ on average, and the number of servers holding $i \ge 3$ jobs is $O(1)$ on average, uniformly in $n$. Combined with the process-level limit and the positive recurrence of the limiting diffusion (Theorem 3, the companion mission), it yields Proposition 1: the diffusion-scaled stationary distribution converges to the stationary distribution of the diffusion. This justifies the diffusion as a steady-state approximation for JSQ.

The method is the generator-comparison or Stein's-method approach: a Lyapunov function solving a first-order PDE for the fluid model, with explicit bounds on its derivatives. It applies to other many-server systems, and the paper is an example of that approach on an infinite-dimensional chain whose diffusion limit is two-dimensional.

The result is proved in the paper; no machine-checked proof is known to exist. The work remaining is to formalize the known proof: the adjoint relation for a countable-state chain with bounded rates, the Taylor expansion of the generator, and the explicit analysis of $f^*$ through the fluid curves.

Difficulty

The obvious route is to bound $\mathbb P(Q_1 = \dots = Q_{i-1} = n)$ in Lemma 2 directly. The paper notes that no good handle on these probabilities exists. The PDE route needs a solution whose second derivatives are bounded by $O(\sqrt n)$. General results that give such bounds require a continuous fluid vector field, and the JSQ fluid model is discontinuous because of the reflection at $x_1 = 0$. So $f^*$ is constructed explicitly from the fluid paths, and its derivatives must be bounded by hand through the implicitly defined $\tau(x)$ and $\nu^*(x_1)$.

A second difficulty is dimensional: the chain is infinite-dimensional while the PDE is two-dimensional, so the remainder of Lemma 3 contains a term with $q_3$ that is controlled only by combining Lemma 2 with the monotonicity of $f^*_2$.

Formalization scope

• Model. States are functions ℕ → ℕ with 0-based indices: Lean q.1 i is the paper's $q_{i+1}$, so the goal's "$i \ge 3$" is Lean index $\ge 2$. Each state is bounded by $n$, nonincreasing and eventually zero. The generator genQ is the displayed formula on p. 6.
• Stationarity. No process is constructed. A stationary distribution is a probability $\pi$ on $S$ satisfying global balance $\pi G_Q = 0$, which characterizes stationarity for this chain with bounded rates. Such a $\pi$ exists, since the chain is positive recurrent for $\lambda < 1$ (Bramson 2011), so statements quantifying over it are not vacuous. Expectations are sums against $\pi$. Lemma 1 keeps its integrability hypothesis, and all other expectations are of bounded functions.
• Parameters. $\lambda = 1 - \beta/\sqrt n$ with $0 < \beta < \sqrt n$, so that $\lambda > 0$; $\lambda$ is free in Lemmas 1–2. Constants are quantified as $\exists C$ after $\beta$ and before $n$.
• Misprint. The printed Theorem 2 omits $\mathbb E$. Read as an almost-sure bound it is false, so the expectation version, which the paper proves, is the target.
• Derivatives. Points of $\Omega$ are pairs in ℝ × ℝ. Partial derivatives are named functions asserted to be one-sided derivatives along coordinate lines (HasDerivWithinAt on Set.Iic 0 or Set.Ici 0). Weak second derivatives are a.e. derivatives of absolutely continuous functions, in integral form on compact intervals. A "solution" of the PDE whose derivatives are the junk values of a derivative operator is thereby excluded. The PDE needs genuine derivatives, and Lemma 7 is about the explicit $f^*$ of (4.14), not about an arbitrary function.
• Fluid objects. $\nu^*, \eta^*$ are the components of the unique solution of (4.8). $\tau$ is valued in WithTop ℝ, with $\infty$ as ⊤, so a missing solution is never read as $0$. $f^*$ is an if cascade, and Lemma 7 states the agreement of its branches. $f^*$ is defined by the closed form (4.14), not through the fluid model (4.1).
• Not included. Lemma 9 (via the Lambert W function, which Mathlib lacks), the bootstrapping argument of App. A.4 (not a numbered result), Theorems 1 and 3, and Proposition 1.

Contributions of reusable infrastructure are welcome: the adjoint relation for countable-state chains with bounded rates, and FTC/Taylor lemmas for absolutely continuous first derivatives.

Selected references

• A. Braverman, Steady-State Analysis of the Join-the-Shortest-Queue Model in the Halfin–Whitt Regime, Math. Oper. Res. 45(3), 2020; arXiv:1801.05121v2. https://arxiv.org/abs/1801.05121
• P. Eschenfeldt, D. Gamarnik, Join the Shortest Queue with Many Servers. The Heavy Traffic Asymptotics, arXiv preprint, 2015. https://arxiv.org/abs/1502.00999
• D. Mukherjee, S. C. Borst, J. S. H. van Leeuwaarden, P. A. Whiting, Universality of Load Balancing Schemes on the Diffusion Scale, J. Appl. Probab. 53, 1111–1124, 2016. https://projecteuclid.org/euclid.jap/1481132840
• M. Bramson, Stability of Join the Shortest Queue Networks, Ann. Appl. Probab. 21, 1568–1625, 2011. https://doi.org/10.1214/10-AAP726
• S. Halfin, W. Whitt, Heavy-Traffic Limits for Queues with Many Exponential Servers, Oper. Res. 29(3), 1981. https://doi.org/10.1287/opre.29.3.567