Graph Theory

Motivation

Many questions in operations research and combinatorics ask whether a system of linear inequalities on a network has a solution: can the demands at a set of warehouses be met from the supplies at a set of factories through roads of limited capacity; is there a nonnegative matrix with bounded entries whose row and column sums lie between given limits; can a periodic schedule be met when every activity has a minimum and a maximum rate. Chapter II of L. R. Ford, Jr. and D. R. Fulkerson's Flows in Networks (RAND Report R-375-PR, 1962; Princeton University Press, 1962, doi:10.1515/9781400875184) answers these questions by feasibility theorems: a system of flow constraints has a solution exactly when a family of inequalities, one for each set of nodes, holds.

The history in the chapter's first three sections is short. D. Gale proved the supply-demand theorem in 1957 (A theorem on flows in networks, Pacific J. Math. 7 (1957) 1073–1082). A. J. Hoffman proved the circulation theorem, with lower and upper bounds on every arc, in 1960 (Some recent applications of the theory of linear inequalities to extremal combinatorial analysis, Proc. Sympos. Appl. Math. 10, AMS, 1960), originally through the separation theorem for convex sets. Ford and Fulkerson derive all of these, and the two-sided variants, from the max flow min cut theorem of their Chapter I.

Setting

A network $[N; \mathcal A]$ is a finite set $N$ of nodes together with a set $\mathcal A$ of ordered pairs $(x, y)$ of distinct nodes, the arcs; there is at most one arc from $x$ to $y$, but both $(x, y)$ and $(y, x)$ may be arcs. Each arc carries a real capacity $c(x, y) \ge 0$. For a real function $g$ on the arcs and node sets $X, Y \subseteq N$,

so $f(x, N)$ is the total of $f$ on arcs leaving $x$ and $f(N, x)$ the total on arcs entering $x$. For a node set $X$, $\bar X = N - X$; for a node function $a$, $a(X) = \sum_{x \in X} a(x)$.

In §§1–2 the nodes are partitioned into sources $S$, intermediate nodes $R$ and sinks $T$ (any of them may be empty). Sources carry a supply $a(x) \ge 0$, sinks a demand $b(x) \ge 0$. A function $f$ on the arcs is a feasible flow for the supply-demand problem when the net outflow $f(x, N) - f(N, x)$ is at most $a(x)$ at every source, zero at every intermediate node, the net inflow $f(N, x) - f(x, N)$ is at least $b(x)$ at every sink, and $0 \le f \le c$ on every arc.

In §3 there are no distinguished nodes. A lower bound function $\ell$ with $0 \le \ell \le c$ is given on the arcs, and a feasible circulation is a function $f$ on the arcs with

Formalization targets

Goal: Hoffman's circulation theorem (Chapter II, Theorem 3.1, p. 26)

For a network with capacities $c$ and lower bounds $0 \le \ell \le c$, a feasible circulation exists if and only if

Milestones

1. Theorem 1.1 (p. 4), Gale's supply-demand theorem. The supply-demand constraints are feasible if and only if $b(T \cap \bar X) - a(S \cap \bar X) \le c(X, \bar X)$ for every $X \subseteq N$.
2. Corollary 1.2 (p. 7). They are feasible if and only if for every $T' \subseteq T$ some flow respecting the supplies, conservation and capacities delivers $f_{T'}(N, T') - f_{T'}(T', N) \ge b(T')$.
3. Theorem 2.1 (p. 21). With two-sided bounds $0 \le a \le a'$ on the net outflow at sources and $0 \le b \le b'$ on the net inflow at sinks, feasibility holds if and only if, for all $X \subseteq N$,

4. Corollary 2.2 (p. 22). The two-sided system is feasible if and only if each of the two one-sided systems (lower bound at sources with upper bound at sinks; upper bound at sources with lower bound at sinks) is feasible.
5. Corollary 2.3 (p. 23). For $0 \le a_i \le a'_i$, $0 \le b_j \le b'_j$, $c_{ij} \ge 0$: if one $m \times n$ matrix meets $a_i \le \sum_j f_{ij}$, $\sum_i f_{ij} \le b'_j$ and another meets $\sum_j f_{ij} \le a'_i$, $b_j \le \sum_i f_{ij}$, both with $0 \le f_{ij} \le c_{ij}$, then a single matrix meets all four row and column limits with $0 \le f_{ij} \le c_{ij}$.
6. Theorem 3.2 (p. 28). With node bounds $a \le a'$ (no sign condition) on the net inflow $f(N, x) - f(x, N)$ at every node and arc bounds $0 \le \ell \le c$, feasibility holds if and only if

With $a = a' = 0$ this is the goal.

Significance

The circulation theorem is the most general of the chapter's feasibility criteria for directed networks: the supply-demand theorem, the existence of $s$–$t$ flows between lower and upper arc bounds (Chapter I, §9), and the transportation-matrix criterion of Corollary 2.3 all follow from it or from its extension, Theorem 3.2, by adjoining arcs, and the rest of Chapter II applies them to systems of distinct representatives and (0, 1)-matrices.

All results of the mission have been proved for more than sixty years. None of them, in this form, is formalized on Prove2Me: the platform has decomposition results for circulations and max flow min cut statements in other conventions, but no Gale or Hoffman feasibility criterion. The mission produces machine-checked versions of the six numbered results and the goal over one shared notion of network, in the book's notation.

Difficulty

Necessity is the routine half of every theorem. Sufficiency asks for a flow built from a family of $2^{|N|}$ inequalities, one per node set, and constructing a flow arc by arc or node by node with local repairs gives no argument that the repairs stop or that all constraints hold at once. The statements also differ in ways that are easy to get wrong: §§1–2 bound the net outflow at sources but the net inflow at sinks, §3 bounds the net inflow everywhere, the node bounds of Theorem 3.2 carry no sign condition and may be negative, and Theorem 2.1 needs two inequalities per node set rather than one. Real-valued data rule out any argument by induction on integer flow values without a separate limiting step.

Formalization scope

Nodes form a Fintype with decidable equality; arcs are a Finset (N × N) with no loops; capacities and flows are real functions $N \to N \to \mathbb R$. A flow is required to vanish off $\mathcal A$, and every sum $g(X, Y)$ runs over arcs only, so the values of $c$ and $\ell$ off $\mathcal A$ never matter. Supplies, demands and node bounds are real functions on all of $N$ whose values enter only through sums over the sets the book names ($S \cap \bar X$, $T \cap X$, …). The partition $S, R, T$ is three pairwise disjoint Finsets covering $N$. $X$ ranges over all subsets of $N$, including $\emptyset$ and $N$. Each section's sign convention is copied: §§1–2 bound the net outflow at sources and the net inflow at sinks, §3 bounds the net inflow. Corollary 2.3 is stated for real matrices indexed by Fin m × Fin n. All data are finite reals; no integrality is assumed.

Feasibility is always stated as the existence of a function on the arcs satisfying the book's displayed constraints. Defining feasibility through the cut condition itself, or through a linear-programming solver predicate, would make every theorem definitional and is ruled out.

Beyond the paper. One variant is posed beside the faithful goal: [Strengthened] Theorem 3.1, the circulation theorem for any real lower bound $\ell \le c$ without $\ell \ge 0$ (capacities stay nonnegative). The substitution $g = f - \ell$ reduces it to a supply-demand problem with nonnegative capacities $c - \ell$, whose Gale condition is $c(X, \bar X) \ge \ell(\bar X, X)$ regardless of the sign of $\ell$; it implies the faithful statement.

A complete development needs Chapter I's max flow min cut theorem in some form (or the linear-programming duality theorem, or Farkas' lemma), the manipulation of arc sums over node sets, and the auxiliary-network constructions. The definitions of networks, arc sums and partitions are reusable by the later Chapter II missions. Proofs of any milestone, of the variant, and alternative proofs through LP duality are welcome.

Selected references

• L. R. Ford, Jr. and D. R. Fulkerson, Flows in Networks, The RAND Corporation, Report R-375-PR, 1962; Princeton University Press, 1962. doi:10.1515/9781400875184
• D. Gale, A theorem on flows in networks, Pacific Journal of Mathematics 7 (1957), 1073–1082. doi:10.2140/pjm.1957.7.1073
• A. J. Hoffman, Some recent applications of the theory of linear inequalities to extremal combinatorial analysis, Proceedings of Symposia in Applied Mathematics 10, American Mathematical Society, 1960, 113–127.
• L. R. Ford, Jr. and D. R. Fulkerson, Maximal flow through a network, Canadian Journal of Mathematics 8 (1956), 399–404. doi:10.4153/CJM-1956-045-5

Motivation

Many combinatorial and nonconvex problems can be written as the maximization or minimization of a quadratic form under quadratic constraints. Such problems are NP-hard in general, but each has a semidefinite relaxation: a convex problem over positive semidefinite matrices, solvable to any accuracy in polynomial time, whose optimal value bounds the original one. The relaxation is useful exactly to the extent that this bound is tight, and the quality of the bound is measured by an explicit approximation ratio.

Lecture 4 of Ben-Tal and Nemirovski, Lectures on Modern Convex Optimization (SIAM, 2001), develops this theory from first principles and proves the two classical ratios. The history it follows:

• N. Z. Shor (1987) introduced the semidefinite relaxation scheme for quadratically constrained problems that §4.3.1 describes.
• M. X. Goemans and D. P. Williamson (J. ACM 42, 1995, doi:10.1145/227683.227684) proved that for MAXCUT with nonnegative weights the semidefinite relaxation is within a factor $0.87856\ldots$ of the maximum cut.
• Yu. Nesterov (1998, doi:10.1080/10556789808805690) proved that for the maximization of any positive semidefinite quadratic form over the vertices of the cube $\{-1,1\}^n$ the relaxation is within a factor $2/\pi$.
• Nesterov and Y. Ye, and A. Nemirovski, C. Roos and T. Terlaky (doi:10.1007/s101070050100), extended such bounds to systems of quadratic inequalities, with factors $\pi/2$ (commuting constraints) and $2\ln(2\sum_i \operatorname{Rank} B_i)$ (general convex constraints).

This mission formalizes the book's statements of these results.

Setting

Let $A$ be a real symmetric $n\times n$ matrix and let $S_n$ be the set of vectors $x \in \mathbb R^n$ with every coordinate equal to $+1$ or $-1$. The quadratic sign problem (4.3.17) is

and its semidefinite relaxation (4.3.18) is

where $X \succeq 0$ means that $X$ is symmetric positive semidefinite. Every $x \in S_n$ gives the feasible matrix $X = xx^T$, which is why $\mathrm{SDP} \ge \mathrm{OPT}$. For a matrix $X$, $\operatorname{asin}[X]$ denotes the matrix with entries $\operatorname{asin}(X_{ij})$.

The MAXCUT problem (4.3.14) with weights $a_{ij} = a_{ji} \ge 0$ is $\max\{\tfrac14\sum_{i,j}a_{ij}(1 - x_ix_j) : x_i^2 = 1\}$, with relaxation (4.3.15) $\max\{\tfrac14\sum_{i,j}a_{ij}(1 - X_{ij}) : X = X^T \succeq 0,\ X_{ii} = 1\}$. The constant $\alpha = 0.87856\ldots$ is the largest $\alpha$ with $\operatorname{acos}(x)/\pi \ge \alpha\cdot\tfrac12(1 - x)$ for all $x \in [-1, 1]$.

The general quadratically constrained problem (4.3.5) minimizes $f_0(x) = x^TA_0x + 2b_0^Tx + c_0$ subject to $f_i(x) = x^TA_ix + 2b_i^Tx + c_i = 0$, $i = 1, \dots, m$. Its Lagrangian lower bound (4.3.9) and Shor's relaxation (4.3.11) are semidefinite programs built from the bordered matrices $\bar A_i = \begin{pmatrix} c_i & b_i^T\\ b_i & A_i\end{pmatrix}$.

Finally, the setting (SL.??) of the exercises takes a system $x^TB_ix \le d_i$, $i = 1,\dots,m$, with $d_i \ge 0$, the value $f^* = \max\{x^TAx : x^TB_ix \le d_i\}$, the relaxation value $F^* = \max\{\operatorname{Tr}(AX) : \operatorname{Tr}(B_iX) \le d_i,\ X \succeq 0\}$, and the dual (SDD) $\min\{\sum_i\lambda_id_i : \sum_i\lambda_iB_i \succeq A,\ \lambda \ge 0\}$.

Formalization targets

Goal: Nesterov's theorem (Theorem 4.3.2, p. 173)

For every positive semidefinite $A$,

The constant $2/\pi$ is the book's, stated exactly.

Milestones

1. Simple lemma (p. 163): $x^TAx + 2b^Tx + c \ge 0$ for all $x$ if and only if $\begin{pmatrix} c & b^T\\ b & A\end{pmatrix} \succeq 0$.
2. Proposition 4.3.1 (p. 163): the optimal value of (4.3.9) is at most that of (4.3.5).
3. Proposition 4.3.2 (p. 164): the optimal value of Shor's relaxation (4.3.11) is at most that of (4.3.5).
4. Theorem 4.3.1 (p. 171, Goemans–Williamson): $\mathrm{OPT} \le \mathrm{SDP}$ and $\alpha\cdot\mathrm{SDP} \le \mathrm{OPT}$ for MAXCUT, $\alpha = 0.87856\ldots$.
5. Lemma 4.3.1 (p. 174): for every feasible $X$ of (4.3.18), $\mathrm{OPT} \ge \frac2\pi\sum_{i,j}a_{ij}\operatorname{asin}(X_{ij})$, and consequently $\mathrm{OPT} \ge \frac2\pi\max\{\operatorname{Tr}(A\operatorname{asin}[X]) \mid X \succeq 0,\ X_{ii} = 1\}$ (4.3.19).
6. Nesterov's observation (p. 174): $\operatorname{asin}[X] \succeq X$ for every positive semidefinite $X$ with $|X_{ij}| \le 1$.
7. Proposition 4.10.5 (pp. 314–315, Nesterov–Ye): if the $B_i$ commute, the system is strictly feasible, some nonnegative combination of the $B_i$ is positive definite and $A \succeq 0$, then $f^* \ge 0$, (SDD) is solvable with optimal value $F^*$, and $F^* \le \frac\pi2 f^*$.
8. Proposition 4.10.6 (p. 315, Nemirovski–Roos–Terlaky): if $B_i \succeq 0$, $d_i > 0$ and $\sum_iB_i \succ 0$, then $f^* \ge 0$, (SDD) is solvable with optimal value $F^*$, and $F^* \le 2\ln\big(2\sum_{i=1}^m\operatorname{Rank}(B_i)\big)f^*$.

Significance

Nesterov's theorem was the first constant-factor guarantee for semidefinite relaxation of a quadratic program whose objective is not a cut function, and it holds for every positive semidefinite form, including those arising in graph partitioning and in robust optimization. Together with the Goemans–Williamson theorem it underlies the matrix cube theorem and the approximate S-lemma later in the book, and the general logarithmic bound of Proposition 4.10.6 is the template for many approximation results in robust and chance-constrained optimization.

All statements of this mission are proved in the literature. On Prove2Me, a Goemans–Williamson statement exists in another form (the expected value of Gaussian rounding against the integer optimum, with constant $0.878$), and a constant-factor bound for the same objects as the goal exists with a much weaker constant ($2K$ with $K \le 288$, via Grothendieck's inequality). Neither the factor $2/\pi$ nor the exact constant $0.87856\ldots$ nor the bounds of Propositions 4.10.5–4.10.6 has a machine-checked statement or proof. Formalizing them also yields reusable infrastructure: optimal values of semidefinite programs as explicit predicates, the elliptope $\{X \succeq 0, X_{ii} = 1\}$, and entrywise matrix functions.

Difficulty

The upper bounds ($\mathrm{SDP} \ge \mathrm{OPT}$, Propositions 4.3.1–4.3.2) are the routine part. The lower bounds compare a continuous relaxation with a discrete optimum, and the book's constants ($2/\pi$, $0.87856\ldots$, $\pi/2$, $2\ln(2\sum_i\operatorname{Rank}B_i)$) leave no slack: an argument that loses any constant factor proves a different theorem. No feasible matrix of the relaxation is in general close to a rank-one matrix $xx^T$ with $x \in S_n$, so the obvious idea of reading a sign vector off an optimal $X$ directly gives no factor at all. The objects involved also go beyond what Mathlib packages: optimal values of semidefinite programs, entrywise transcendental functions of matrices, and, for Propositions 4.10.5–4.10.6, duality between (SDP) and (SDD).

Formalization scope

Vectors are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, and $X \succeq 0$ is Mathlib's Matrix.PosSemidef, which includes symmetry. The $(n+1)\times(n+1)$ matrices of §4.3.1 are indexed by Unit ⊕ Fin n. Optimal values are never a bare sSup: a maximization's optimal value enters as the hypothesis that a real number is the least upper bound of the objective over the feasible set, and these sets are nonempty and bounded, so the hypotheses are satisfiable for every instance. The optimal values of §4.3.1, which can be $\pm\infty$, are infima and suprema in EReal. The constant $0.87856\ldots$ is defined as the exact infimum $\inf_{-1\le x<1} 2\operatorname{acos}(x)/(\pi(1-x))$, never a decimal. The ratio $1 \ge \mathrm{OPT}/\mathrm{SDP} \ge 0.87856\ldots$ of (4.3.16) is stated in product form, $\mathrm{OPT} \le \mathrm{SDP}$ and $\alpha\cdot\mathrm{SDP} \le \mathrm{OPT}$: with Lean's convention $x/0 = 0$, a ratio would make the all-zero-weight instance meaningless, and the product form rules out that trivialization. The book's standing conditions (symmetric data; $d_i \ge 0$ in (SL.??)) are explicit hypotheses.

Contributions welcome: compactness of the elliptope $\{X \succeq 0,\ X_{ii} = 1\}$ and attainment of SDP values, rotation-invariant measures on spheres in Fin n → ℝ, entrywise functions of positive semidefinite matrices (Mathlib has the Schur product theorem, Matrix.PosSemidef.hadamard), and conic duality for (SDP)/(SDD). These are reusable well beyond this chapter.

Beyond the paper. One sharpness probe accompanies the goal: Nesterov's theorem with "$A \succeq 0$" weakened to "$A$ symmetric". It is false (finding F3: for $n = 1$, $A = (-1)$, $\mathrm{OPT} = \mathrm{SDP} = -1$ and $-\tfrac2\pi \le -1$ fails); its disproof is the sought outcome.

Selected references

• A. Ben-Tal, A. Nemirovski, Lectures on Modern Convex Optimization: Analysis, Algorithms, and Engineering Applications, SIAM/MPS, 2001, §4.3 and §4.10. doi:10.1137/1.9780898718829
• M. X. Goemans, D. P. Williamson, Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming, J. ACM 42 (1995), 1115–1145. doi:10.1145/227683.227684
• Yu. Nesterov, Semidefinite relaxation and nonconvex quadratic optimization, Optimization Methods and Software 9 (1998), 141–160. doi:10.1080/10556789808805690
• A. Nemirovski, C. Roos, T. Terlaky, On maximization of quadratic form over intersection of ellipsoids with common center, Mathematical Programming 86 (1999), 463–473. doi:10.1007/s101070050100

Motivation

Supply-chain traceability depends on firms adopting a technology together. A firm may benefit only after enough other firms in a shared supply chain have adopted; a supply chain may in turn become traceable only when a threshold number of its firms participate. Selecting firms to seed therefore couples many local adoption decisions. Blaettchen, Calmon, and Hall model this coupling as a network diffusion problem and ask for a least-cost seed set that eventually activates every firm Blaettchen, Calmon, and Hall, 2024. Their model permits overlapping supply chains and firm-specific benefits and costs, so it describes more than a single threshold rule on an ordinary graph.

The paper establishes an exact linear programming reformulation whose size depends exponentially on treewidth but only linearly on the numbers of firms and supply chains, up to parameter factors Theorem 2. This mission records that mathematical claim as a cost-independent extended formulation, together with source propositions describing the diffusion correspondence and the first binary formulation.

Setting

Let $N_F$ contain $n$ firms and let $N_{SC}$ contain $m$ supply chains. Supply chain $j$ comprises the hyperedge $e_j\subseteq N_F$. Firm $i$ has an adoption cost $c_i>0$ and receives a nonnegative integral benefit $r_{ji}$ from an incident supply chain $j$ once enough of that chain's firms are active. The chain's threshold satisfies $2\le\theta_j\le|e_j|$. The paper assumes that each firm's total incident benefit can cover its adoption cost. A seed set $S_0$ is active at time zero; every later set $S_t$ retains the already active firms and adds a firm $i$ when

A seed set fully activates the network if $S_t=N_F$ at some finite time. Given real seeding costs $w_i$, the optimization value is

The auxiliary graph $G'$ has a firm vertex for each $i$ and a supply-chain vertex for each $j$, joined when $i\in e_j$. Its directed weighted version sends weight $1$ from a firm to a supply-chain vertex and weight $r_{ji}$ in the reverse direction. Firm thresholds are $c_i$; supply-chain thresholds are $\theta_j-1$. A weighted linear-threshold update activates vertices whose total incoming weight from active vertices reaches their threshold. Proposition 1 identifies the firms active after $t$ original steps with those active after $2t$ auxiliary-graph steps Proposition 1, p. 10.

A tree decomposition is a tree of vertex bags that covers every vertex, places each graph edge or hyperedge in a bag, and keeps the bags containing one vertex connected along the tree. Its width is the largest bag size minus one. Write $\omega$ for an upper bound on the treewidth of the original hypergraph and $\vartheta_{\max}=\max(\max_i c_i,\max_j(\theta_j-1))$ Definition 2, p. 13; Proposition 9, p. 18.

Formalization targets

Exact LP reformulation

The target is one finite linear system $Az\ge b$, where $z=(x,y)$ has visible seed coordinates $x\in\mathbb R^n$ and auxiliary coordinates $y$. The system is chosen from the adoption instance and is independent of $w$. Its projection onto $x$ is exactly the convex hull of fully activating seed indicators:

Consequently, minimizing $\sum_iw_ix_i$ over the same LP yields $\operatorname{OPT}(w)$ for every real $w$. One absolute constant $C>0$, placed before all instances and treewidth parameters, bounds the total number of variables and constraints by

This is the $2^{O(\omega^2)}\vartheta_{\max}^{O(\omega)}O(n+m)$ form stated immediately after Theorem 2 p. 18. The source's more detailed displayed bracket is not used as the target because its fixed exponents do not match the asymptotic bound obtained from the propositions cited in the proof.

Supporting results

The milestones follow the proof of Theorem 2 on p. 41. Proposition 1 and Corollary 1 identify the adoption process with a weighted threshold process on $G'$. Proposition 5 gives a binary program (4) whose feasible seed vectors are exactly the fully activating seed sets. Proposition 7 replaces its global acyclicity constraints by constraints inside the bags of a tree decomposition of $G'$, formulation (5). Proposition 8 splits the long covering constraints of (5) into partial sums along a rooted binary decomposition, formulation (10). Proposition 9 bounds the treewidth of the intersection graph of (10) by $O(\omega'^2+\omega'\log_2\vartheta_{\max})$, where $\omega'$ is the width of the decomposition of $G'$. Proposition 3 gives $\operatorname{tw}(G')\le\operatorname{tw}(G)+1$, and Proposition 4 is the bounded-treewidth LP theorem for binary programs pp. 10–18.

Significance

An exact LP gives the same optimum for every seeding-cost vector while keeping the constraints fixed. The size guarantee explains why a structurally sparse supply-chain network can admit a formulation far smaller than a generic enumeration of seed sets. It also separates the economics of choosing $w$ from the combinatorics of diffusion: once the network formulation is built, different cost scenarios use the same feasible region Theorem 2 and §5.3.

The paper proves the theorem, citing Proposition 4 from Laurent (2009) and Bienstock and Muñoz (2018). Neither Theorem 2 nor Proposition 4 has a machine-checked proof on Prove2Me. The remaining work is to formalize the paper's chain of reformulations and the cited LP theorem. The tree decomposition definitions are already published as reusable Prove2Me objects from Robertson and Seymour. The diffusion model, the binary formulation, and their relationship to an LP extended formulation are the new formal objects here.

Difficulty

The first binary program represents the activation order but connects variables across many firm–supply-chain pairs. Its intersection graph has treewidth at least $nm-1$, even when the underlying supply-chain graph is sparse Proposition 6, p. 16. Applying a bounded-treewidth LP theorem directly to that program therefore loses the desired parameter bound. The source introduces a more local formulation tied to a tree decomposition, and controlling the intersection graph of that formulation is the central difficulty. Formulation (10) as printed is not exactly right: the bit count (6) is one bit short, so that an instance with $c_1=2$ loses its optimal seed set, and the root inequalities (10c), (10g) use an undeclared variable. The targets use the bit ranges of the integer program (11) in the proof of Proposition 8 and the partial sum $u$ at each subtree root.

Formalization scope

The Lean instance uses Fin n for firms, Fin m for supply chains, and natural numbers for benefits, adoption costs, and thresholds. The auxiliary graph is a simple graph on the disjoint union of these two finite types; the diffusion update retains active vertices and uses the paper's weak inequality at the threshold. Hypergraph treewidth requires every entire hyperedge in some bag and uses the published Robertson–Seymour tree decomposition predicate for the primal graph. Graph treewidth for $G'$ uses the corresponding published bound predicate.

The paper treats connectedness as without loss of generality. Here it means that the incidence graph $G'$ is connected and is included with the other standing assumptions. The gcd normalization discussed in §3.1 is a preprocessing convention, not a hypothesis. The finite family of successful seed sets always contains the all-firm set, so OPT is a genuine finite minimum. The formulation counts both auxiliary variables and inequalities. The additive shifts in the size bound handle small values of $n$, $m$, $\omega$, and $\vartheta_{\max}$; they do not change the asymptotic claim. The LP is quantified before $w$, and its projection is specified, excluding a trivial LP selected separately for each cost vector.

Formulations (4), (5) and (10) are binary feasibility predicates over natural-number variables bounded by one; the adoption inequality $c_i(1-s_i)\le\cdots$ is written as $c_i\le\cdots+c_is_i$. Constraints (5c), (5d), (10i), (10j) range over distinct vertices of a bag (with $i=j$ the printed (5c) would be infeasible). A rooted binary tree decomposition is a published tree decomposition together with a root, a parent map and at most two children per node; the subtree root $z_0^p$ is the node of the subtree nearest the root. The partitions $J^i_z$, $I^j_z$ are arbitrary data with the properties stated on p. 17, which are all the proofs use. Proposition 7 is stated for every tree decomposition of $G'$; binarity is not needed there.

The generic finite linear-system and intersection-graph definitions can be reused beyond this paper. Contributions are welcome at every milestone; Proposition 4 is a general result on binary programs and is the most widely reusable.

Selected references

• Paul Blaettchen, André P. Calmon, and George Hall, Traceability Technology Adoption in Supply Chain Networks, Management Science, 2024; preprint arXiv:2104.14818v4 (2023). arXiv
• Neil Robertson and Paul D. Seymour, Graph Minors. V. Excluding a Planar Graph, Journal of Combinatorial Theory, Series B 41, 1986. DOI
• Monique Laurent, Sums of Squares, Moment Matrices and Optimization over Polynomials, in Emerging Applications of Algebraic Geometry, IMA Vol. 149, Springer, 2009. DOI
• Daniel Bienstock and Gonzalo Muñoz, LP Formulations for Polynomial Optimization Problems, SIAM Journal on Optimization 28(2), 2018. DOI

Motivation

In atomic dynamic routing, indivisible agents (vehicles, packets, travellers) enter a network over time and travel along fixed routes. Each road admits a limited number of agents per unit of time, so agents queue at its entrance. A basic question for traffic models, packet-switching networks and dynamic routing games is how long an agent can stay in the network, its residence time. Upper bounds on residence times are what make it possible to bound queue lengths and the price of anarchy in dynamic routing games.

Greedy packet scheduling, where an edge never idles while packets wait for it, was studied by Cidon, Kutten, Mansour and Peleg (SIAM J. Comput. 1995), who showed that cycles can make delays large, and by Mansour and Patt-Shamir (J. Algorithms 1993), who bounded delivery times when every route is a shortest path. Cao, Chen, Chen and Wang (MOR 2022) prove a bound for arbitrary routes on acyclic networks. It holds under any rule that decides which waiting agent may leave next, and agents may keep entering forever. Their Theorem 1 is the goal of this mission. The paper then uses it to show that equilibria of three dynamic routing games on series-parallel networks have bounded queues (§6).

Setting

A network $G=(V,E)$ is a finite directed multigraph (parallel edges allowed) that is acyclic. Every edge has unit length and unit capacity. A path is a sequence of edges, each starting where the previous one ends. $L_{vw}$ is the number of edges of a longest $v$-$w$ path.

Time is discrete, $0,1,2,\dots$. Agents form a set $\Delta$, possibly infinite. At each time finitely many agents enter. Agent $i$ enters at time $r_i$ at his origin $o_i$ and follows a fixed route, a nonempty $o_i$-$d_i$ path. The tail of each edge holds a buffer. Two rules govern the dynamics:

• (A1) an agent reaching a vertex that is not his destination enters the buffer of his next edge at once;
• (A2) at every integer time, whenever a buffer is nonempty, exactly one agent leaves it and reaches the head of the edge one time unit later; the others wait.

No rule says which agent leaves. Every choice consistent with (A2) is an admissible run. An agent exits $G$ on reaching his destination. His residence time is his exit time minus his entry time (Definition 1).

Fix a focal agent $\zeta$ with entry time $r$. $G_\zeta$ is the subnetwork formed by all $o_\zeta$-$d_\zeta$ paths. For an integer time $r_0$:

• $A_{\zeta,p}$ is the set of agents who enter after time $r$ and use an edge of $G_\zeta$;
• $B_{\zeta,p}(r_0)$ is the set of agents $i\neq\zeta$ who entered by time $r$, are still inside $G$ at time $r_0$, and use an edge of $G_\zeta$.

An agent exits $G_\zeta$ when he reaches the head of the last edge of his route lying in $G_\zeta$.

Formalization targets

Goal: Theorem 1 (p. 7)

For every admissible run and every integer $r_0\ge r$: if no agent of $A_{\zeta,p}$ exits $G_\zeta$ before $\zeta$ exits $G$, then

where $t_\zeta$ is the exit time of $\zeta$.

Milestones (§3.2, p. 9)

When $\zeta$ is still inside $G$ at $r_0$, the proof follows tokens: imaginary markers that $\zeta$ produces from time $r_0$ on, and that travel with the agents leaving buffers ((s1), (s2), p. 8). The milestones are the paper's statements about them, with $L=L_{o_\zeta d_\zeta}$:

1. (p1) each agent holds at most one token, and a buffer never contains more tokens than agents;
2. (p2) the agent leaving $\zeta$'s buffer always holds exactly one token;
3. (p3) after $r_0$, $\zeta$ produces a new token only while he waits;
4. Claim 1 the induction step of Lemma 1 at the vertices where token $k$ departs right after a smaller token;
5. Lemma 1 token $k$ departs every vertex $v$ of its trail inside $G_\zeta$ by time $r_0+(L-L_{vd_\zeta}+k-1)$;
6. token exit token $k$ exits $G_\zeta$ by time $r_0+(L+k-1)$.

Significance

The result. The bound does not depend on the rule that selects the leaving agent, so it covers every queueing discipline at once: FIFO, global agent priorities, and the edge-priority rules of earlier dynamic routing games. With $r_0=r$ and no later entrants on $G_\zeta$, it gives Corollary 1: the residence time of $\zeta$ is at most $L_{o_\zeta d_\zeta}+|B_{\zeta,p}(r)|$. Example 1 (p. 8) shows that the bound can be attained. The freedom in $r_0$ is what §6 uses to show that queue lengths stay bounded at equilibria of dynamic routing games on series-parallel networks.

Formalizing it. The theorem is proved on paper. No machine-checked version is known to exist, and the platform has no rule-free model of atomic dynamic routing. The mission adds that model: a run is a set of leave times constrained by (A1)–(A2), not a fixed simulation. It also adds the multi-token process and the paper's chain of statements leading to Theorem 1.

Difficulty

The obvious argument is wrong. One might reason that $\zeta$ travels at most $L_{o_\zeta d_\zeta}$ edges and each earlier agent delays him at most once, giving the bound at once. The paper notes (p. 7) that this intuition fails even with two agents: a single agent can delay $\zeta$ more than $|\Delta|$ times, because delays propagate through other buffers. Bounding the total therefore means tracking chains of delays across the network rather than charging each delay to one agent.

Formally, the hard parts are:

• the run is only constrained, not determined;
• the token process is defined by recursion over time, using the unique leaver of each buffer;
• (p1)–(p3) are invariants proved by induction on time;
• Lemma 1 combines induction on the token index with longest-path inequalities in an acyclic graph.

Formalization scope

• Model. Network V E (tail and head maps) with finite V, E and a hypothesis Acyclic: no nonempty closed walk. Paths are edge lists. longest v w is the supremum of path lengths in $\mathbb N$; it is a maximum wherever it is used.

• Runs. RunData holds entry times, routes, origins and destinations, and leave times leave i j in $\mathbb N\cup\{\infty\}$ for the $j$-th edge of $i$'s route, numbered from $0$. IsADR states that:

  • routes are nonempty origin–destination paths;
  • finitely many agents enter per time;
  • nobody leaves a buffer before entering it;
  • (A2) holds, as unique existence of the leaver of each nonempty buffer at each time.

  Agents form an arbitrary type and may be infinitely many. An agent may never be served (leave time $\infty$), as in the paper, so the theorem also asserts that $\zeta$ exits.

• Derived objects. Exit times, $G_\zeta$, $A_{\zeta,p}$, $B_{\zeta,p}(r_0)$ and the exit time from $G_\zeta$ are definitions computed from the run, never free parameters. $|B_{\zeta,p}(r_0)|$ is Set.ncard of a set that is finite under IsADR.

• Tokens. The token milestones assume that $\zeta$ is inside $G$ at $r_0$, as §3.1 requires when starting the construction. Tokens are indexed from $1$. A new token gets index one plus the number produced so far. Bounds with subtraction are written additively over $\mathbb N$, e.g. $s+L_{vd_\zeta}+1\le r_0+L+k$, which is the same inequality over the integers.

• Ruled out. None of these is used, since each proves a different statement: a fixed tie-breaking rule (FIFO or priorities), exit times as free parameters, finitely many agents, or dropping acyclicity, which Remark 2 shows is necessary.

Contributions welcome: proofs of the token invariants, of Lemma 1, and of the goal. The network and run definitions can be reused for the paper's other results (Theorem 2 on uniform capacities, the routing games of §5–6).

Selected references

• Z. Cao, B. Chen, X. Chen, C. Wang, Bounding residence times for atomic dynamic routings, Mathematics of Operations Research, 2022 (accepted manuscript: WRAP 160244). https://doi.org/10.1287/moor.2021.1242 , https://wrap.warwick.ac.uk/160244
• Y. Mansour, B. Patt-Shamir, Greedy packet scheduling on shortest paths, Journal of Algorithms 14(3):449–465, 1993.
• I. Cidon, S. Kutten, Y. Mansour, D. Peleg, Greedy packet scheduling, SIAM Journal on Computing 24(1):148–157, 1995.
• T. Harks, B. Peis, D. Schmand, B. Tauer, L. Vargas Koch, Competitive packet routing with priority lists, ACM Transactions on Economics and Computation 6(1):4:1–4:26, 2018.

Motivation

Community detection asks for a hidden partition of the nodes of a graph from its edges. Its simplest probabilistic benchmark is the two-community stochastic block model (SBM), in which the minimum bisection problem is the maximum a posteriori estimator. That problem is NP-hard, so convex relaxations are used in its place, and the question is when a relaxation still returns the hidden partition exactly. For semidefinite relaxations this question has sharp answers (Abbe, Bandeira, Hall 2016; Bandeira 2018). Del Pia, Khajavirad and Kunisky (arXiv:2006.03213v2) ask the same question for the most common linear programming relaxation of minimum bisection, the metric relaxation. They show that it recovers the planted bisection in very dense graphs when $p-q>1/2$ (their Theorem 6). This mission is their converse in the very dense and dense regimes, Theorem 7: above explicit thresholds the LP fails with high probability.

Setting

The node set is $V=\{1,\dots,n\}$, $n$ even. A bisection is a partition $V=V_1\sqcup V_2$ with $|V_1|=|V_2|=n/2$. The cut vector $\bar x\in\{0,1\}^{\binom n2}$ of $V_1,V_2$ has $\bar x_{ij}=1$ exactly when $i$ and $j$ lie on different sides. For a graph $G$ with adjacency indicators $a_{ij}$, the metric relaxation is

over $x\in\mathbb R^{\binom n2}$, with the first family over distinct $i,j,k$ with $i<j$ and the second over $i<j<k$. The LP recovers the planted bisection if $\bar x$ is its unique optimal solution.

In the SBM $\mathcal G_{n,p,q}$ a bisection $V_1,V_2$ is first drawn uniformly at random; then each pair on the same side is an edge with probability $p$ and each pair across with probability $q$, independently, with $p>q$. The Erdős–Rényi graph $\mathcal G_{n,p}$ has every pair an edge with probability $p$. The dense scaling (20) is $p=\alpha n^{-\omega}$, $q=\beta n^{-\omega}$ with $\alpha>\beta>0$, $0\le\omega<1$; $\omega=0$ is the very dense regime. An event holds with high probability (w.h.p.) if its probability tends to $1$ as $n\to\infty$.

For a graph $G$, $\rho_G(i,j)$ is the shortest-path distance ($+\infty$ across components), $\rho_{\max}(G)=\max_{i,j}\rho_G(i,j)$ is the diameter, and $\rho_{\mathrm{avg}}(G)=\frac2{n^2}\sum_{i<j}\rho_G(i,j)$ is the average distance. $E$ is the edge set of $G$, $E_0$ the set of edges across the planted bisection.

Formalization targets

Goal: Theorem 7 (pp. 15–16)

Let $p=\alpha n^{-\omega}$, $q=\beta n^{-\omega}$ with $\alpha>\beta>0$, $\omega\in[0,1)$, and $\alpha,\beta<1$ if $\omega=0$. If one of

1. $\omega=0$ and $\beta>\max\big\{\tfrac{3-\alpha-\sqrt{(3-\alpha)^2-4\alpha}}2,\ 2\alpha-1\big\}$ (22),
2. $\omega\in(0,1)$, $\tfrac1{1-\omega}\notin\mathbb N$ and $\beta>\alpha/(2\lceil\tfrac1{1-\omega}\rceil-1)$ (23),
3. $\omega=\tfrac12$ and $\beta>\max\big\{\tfrac{1-2e^{-\alpha^2}}{2-e^{-\alpha^2}},\tfrac1{3+2e^{-\alpha^2}}\big\}\alpha$ (24),
4. $\omega\in(0,1)$, $\tfrac1{1-\omega}\in\mathbb N\setminus\{2\}$ and $\beta>\alpha/\big(\tfrac2{1-\omega}-1+2e^{-\alpha^{1/(1-\omega)}}\big)$ (25)

holds, then

Milestones

1. (26), p. 16: for $p,q=\Omega(\log n/n)$ with $\lim q/p\in(0,1]$, the ratio $|E_0|/|E|$ lies in $(1\pm\epsilon)\,q/(p+q)$ w.h.p.
2. Proposition 11, p. 28: a coupling of $\mathcal G_{n,q}$, $\mathcal G_{n,q,p}$ and $\mathcal G_{n,p}$ in which the three graphs are nested.
3. Proposition 12, p. 28: w.h.p. $\rho_{\max}(\mathcal G_{n,\alpha n^{-\omega}})=1+\lfloor\frac1{1-\omega}\rfloor$.
4. Proposition 14, p. 29 (Shimizu): w.h.p. $\rho_{\mathrm{avg}}(\mathcal G_{n,\alpha n^{-\omega}})\in((1-\epsilon)\mu,(1+\epsilon)\mu)$, where $\mu=\lceil\frac1{1-\omega}\rceil+\mathbf 1\{\frac1{1-\omega}\in\mathbb N\}e^{-\alpha^{1/(1-\omega)}}$.
5. Propositions 16, 17, 18, pp. 29–30: the diameter of the very dense and dense SBM, and lower bounds on its average distance, in the three cases $\omega=0$, $\frac1{1-\omega}\notin\mathbb N$ and $\frac1{1-\omega}\in\mathbb N$.

Significance

Theorem 6 and Theorem 7 together bracket the success region of the metric relaxation in the very dense regime: recovery for $p-q>1/2$, failure above the curve (22). In the dense regime, Theorem 7 gives explicit linear thresholds $\beta>c(\omega,\alpha)\,\alpha$ above which the LP fails. The proof reduces failure to a deterministic distance criterion (Theorem 5, posed in mission 4 of this series) and turns asymptotic distance distributions of random graphs into statements about an LP.

The results are proved in the paper, partly by citing Bollobás's diameter theorems and Shimizu's average-distance theorem; none of them has a machine-checked proof. Formalizing the mission yields, besides Theorem 7, the diameter and average distance of dense Erdős–Rényi graphs (Propositions 12 and 14) and the monotone coupling between Erdős–Rényi graphs and the SBM (Proposition 11), each of which is usable beyond this paper. The coupling and (26) are also the inputs of the logarithmic-degree result (Theorem 8, mission 7).

Difficulty

The deterministic half is short: once $|E_0|/|E|$, $\rho_{\max}$ and $\rho_{\mathrm{avg}}$ are pinned down, the case computations (28)–(29) reduce to inequalities between explicit expressions in $\alpha$, $\beta$ and $\omega$. The difficulty is the random-graph input. The diameter of $\mathcal G_{n,p}$ for $p=\alpha n^{-\omega}$ needs the second-moment analysis of the number of pairs at distance greater than $d$ (Bollobás, Corollaries 10.11–10.12), and the average distance needs the finer limit law for path counts at the critical exponent $\frac1{1-\omega}\in\mathbb N$, where the constant $e^{-\alpha^{1/(1-\omega)}}$ appears. A first-moment argument gives only one side of each estimate. Concentration of $|E|$ and $|E_0|$ (26) is a Hoeffding bound, but it must hold uniformly over the random planted bisection.

Formalization scope

Nodes are Fin n and graphs SimpleGraph (Fin n). A bisection is its side $V_1$ with $2|V_1|=n$. The LP variable is a symmetric, zero-diagonal array Fin n → Fin n → ℝ, with no box constraints, so uniqueness is uniqueness over $\mathbb R^{\binom n2}$. Probabilities are finite sums over all graphs (and all bisections for the SBM). Edge probabilities are clamped into $[0,1]$, which affects only finitely many $n$. SBM limits run over even $n=2m$. Distances are in ℕ∞ and $\rho_{\mathrm{avg}}$ in $[0,\infty]$, so disconnected samples have infinite diameter and average distance; no real truncation is used.

Disclosed choices:

• Theorem 7 adds $\alpha>\beta$, the SBM's standing assumption $p>q$ (§4, p. 13), also assumed by Proposition 18 and (26).
• (26) is posed for $p=\alpha s(n)$, $q=\beta s(n)$ with $s(n)\ge c\log n/n$ and $\alpha s(n)\le1$ eventually. Then $q/p=\beta/\alpha$, which avoids the printed "$\lim p/q\in(0,1]$", a slip for $q/p$.
• Proposition 11 is posed as printed, with middle law $\mathcal G_{n,q,p}$ (within $q$, across $p$).

Two encodings would make the statements trivial, and both are excluded. Unnormalized LP variables would make uniqueness false. Reading $\rho$ in $\mathbb R$ via toReal would make the upper bounds hold for disconnected graphs.