Linear Optimization

Why process flexibility matters

A factory can respond to uncertain demand by allowing a plant to make more than one product. Those extra capabilities cost money, so the design question is where to place a limited number of plant–product links. The usual measure of a flexible production system is the number of units sold. When products have different contribution margins, however, two designs with the same sales may earn different profits: capacity used for a low-margin product cannot then serve a high-margin one. Wang, Wang and Zhang study this distinction through worst-case demand and show that a particular arrangement of two product classes is optimal within the family of long chains (Wang, Wang and Zhang 2020, §§1 and 4).

The result addresses a concrete design choice. A long chain gives every plant two product capabilities and connects the system in a cycle. If half the products have high margins and half low margins, should the two classes be grouped on that cycle or spread out? The paper's answer is that alternating high- and low-margin products gives at least as good a worst-case score as every other long-chain arrangement, for a broad class of scores.

Production and uncertain demand

A flexibility design $A$ is a set of arcs $(j,i)$ from plant $j$ to product $i$. Plant $j$ has capacity $C_j$, product $i$ has demand $d_i$ and margin $p_i$, and $x_{ij}$ units of product $i$ are made by plant $j$. The maximum profit $g(A,d)$ is the optimum of the finite linear program

$$g(A,d)=\max_{x\ge0}\sum_{(j,i)\in A}p_i x_{ij},\qquad \sum_jx_{ij}\le d_i,\quad \sum_i x_{ij}\le C_j.$$

Products fall into $T$ categories with margins $P_1<\cdots<P_T$. Write $S_t$ for the products with margin $P_t$ and $D_t(d)=\sum_{i\in S_t}d_i$ for their total demand. A deterministic score in the paper's class has the form $f(A,d)=h(g(A,d),(D_t(d))_t)$, with $h$ strictly increasing in its profit argument when category totals are fixed. Its robust score is $R^f(A,U)=\min_{d\in U}f(A,d)$ for an uncertainty set $U$ of nonnegative demand vectors. This includes maximum profit and scores that subtract a demand-based benchmark from profit (Wang, Wang and Zhang 2020, §2.2).

A set is part-wise independently symmetric when it is a Cartesian product of its category projections and remains unchanged if products are permuted within any category. The perturbation version applies that property to $E=\{d-\mu:d\in U\}$ for a fixed centre $\mu$. Such sets preserve the high/low distinction while treating products within each class interchangeably (Wang, Wang and Zhang 2020, Definitions 2.1–2.2).

Formalization targets

Alternate-chain optimality

In the target system there are $2k$ plants and $2k$ products, $k\ge1$, with unit plant capacities and exactly $k$ products in each of two margin classes $0<P_L<P_H$. A long chain places the fixed products in any cyclic order and connects each plant to two consecutive products. An alternate long chain places high- and low-margin products alternately. The goal, Theorem 3, says that for every such pair of chains, every part-wise independently symmetric $U$, and every robust score in the class above,

$$R^f(\mathrm{AL},U)\ge R^f(L_{HL},U).$$

This is the paper's worst-case comparison, rather than a claim about a single demand instance or a single performance measure (Wang, Wang and Zhang 2020, Theorem 3, p. 21).

Margin-group comparisons

The paper defines a dual margin group index $\delta^K_\mu(A)$ by an integer program that assigns product dual values from the finite menu $\beta_{tr}=P_t-P_r$, where $P_0=0$. The parameter $K$ counts how many products in each category receive each nonzero menu value. Its feasible set is $Q$. Theorem 1 expresses every robust score in terms of these indices and residual demand vectors; Theorem 2(a) says that index dominance for every $K\in Q$ implies robust-score dominance. Lemma 2 evaluates the index of an alternate chain in three cases, and Proposition 1 compares it with every long chain (Wang, Wang and Zhang 2020, pp. 17–22). These are the mission's milestones, alongside the profit LP's duality and two cyclic-window statements used in the comparison.

What the result provides

Within balanced, unit-capacity, two-margin long chains, the theorem resolves placement of the high-margin products without choosing one demand distribution or one profit-based robustness score. The dominance holds across the paper's whole class of category-symmetric uncertainty sets and scores. It gives a design rule within that family; it does not claim that an alternate chain beats every possible two-capability graph. The paper separately studies limits of that broader comparison (Wang, Wang and Zhang 2020, §4.3).

The paper proves these results on paper. This mission asks for machine-checked proofs of the stated Lean targets. Its reusable output includes the finite bipartite profit LP, its dual, category-wise demand symmetry, and the DMGI representation. None of the mission's theorems is presented here as already machine-checked.

Where the formal proof is difficult

The LP optimum must be related to a dual optimum whose product variables belong to a small, margin-dependent set. That is stronger than merely invoking an objective-value duality statement. The robust representation then has to account for both a discrete assignment of dual values and the permissible permutations of demand residuals within each product class. The last comparison is combinatorial: a general long chain can have runs of high-margin products, and its relevant cyclic windows must be compared with the alternating chain across every feasible count vector $K$ (Wang, Wang and Zhang 2020, Appendix A).

Formalization scope

The Lean development represents plants and products by finite index types, real capacities, demands and margins, and a design by a finite set of plant–product pairs. A separate general profit-LP definition is instantiated by the paper's margin-category system. Lean indices start at zero: category $t$ is the paper's category $t+1$, and the added margin level $P_0$ is zero. The production variable is written x j i in Lean for the paper's $x_{ij}$. Category residuals are enumerated by increasing product index; part-wise symmetry makes that choice immaterial. A long chain uses a permutation of fixed products around a cycle, so the uncertainty set stays attached to the same high- and low-margin categories.

The system requires positive numbers of plants, products and occupied margin categories, nonnegative capacities, and positive strictly increasing margins. The paper treats margins as positive profits but does not state that inequality explicitly. The model also supplies $z_j\ge0$ to the DMGI program, matching the dual program and the use of dual feasibility in the paper's proof; equations (4) and (5) omit this line. For the robust minimum, $U$ is nonempty, compact and contained in nonnegative demand, and the deterministic score is continuous there. Nonemptiness and compactness are explicit mathematical additions needed for the paper's minimum and minimizer. Every DMGI theorem restricts $K$ to $Q$. These conditions prevent empty or unbounded real infima from supplying Lean's default zero. The $k=1$ case is included.

Contributions may establish the LP duality, dual extreme-point structure, robust representations, exact alternate-chain index, or cyclic-window comparison. The definitions use finite sums and real suprema and infima; establishing attainment is part of the theorem work.

Selected references

• S. Wang, X. Wang and J. Zhang, Robust Optimization Approach to Process Flexibility Designs with Contribution Margin Differentials, Manufacturing & Service Operations Management, 2020. SSRN author version 3233721, 22 May 2020; DOI.

Motivation

Two-stage stochastic linear optimization is the standard model for decisions taken before uncertainty is revealed and corrected after it: capacity before demand, inventory before transport capacities, generation commitments before load. In practice the probability distribution of the uncertainty is unknown and only historical samples are available, so the stochastic problem has to be replaced by a data-driven one. The sample average approximation (SAA) is consistent but can overfit badly on small samples; distributionally robust formulations hedge against this, but for two-stage problems they are typically intractable.

Bertsimas, Shtern and Sturt (arXiv:1907.07142v4, published as a Technical Note in Operations Research, 2022) study sample robust optimization (SRO): each sample is perturbed adversarially within a small ball intersected with a known support polyhedron. SRO is equivalent to two-stage distributionally robust optimization over a type-∞ Wasserstein ball (Bertsimas, Shtern, Sturt 2018, Proposition 3, as cited on p. 7), and evaluating its objective is NP-hard even for one sample. The paper proposes a tractable multi-policy approximation (MP), with one linear decision rule per sample, and proves that it recovers the optimal value and the optimal decisions of the underlying stochastic problem as the data grow, without assuming relatively complete recourse.

Setting

The data are $c\in\mathbb R^n$, $q\in\mathbb R^r$, $T\in\mathbb R^{m\times n}$, $W\in\mathbb R^{m\times r}$ and an affine right-hand side $h(\zeta)=h^0+H\zeta$. The second-stage cost of a first-stage decision $x$ under the realization $\zeta\in\mathbb R^d$ is

$$Q(x,\zeta)=\inf_{y\in\mathbb R^r}\{q^\top y:\ Tx+Wy\ge h(\zeta)\},$$

equal to $+\infty$ when no recourse $y$ is feasible. With $\xi$ a random vector of law $\mu$, the stochastic problem is

$$v^*=\inf_{x\in\mathbb R^n}V^*(x),\qquad V^*(x)=c^\top x+\mathbb E[Q(x,\xi)].\tag{OPT}$$

The support of $\xi$ lies in a known polyhedron $\Xi=\{\zeta: G\zeta\ge g^0\}$. Given i.i.d. samples $\xi^1,\dots,\xi^N$, a radius $\epsilon_N\ge0$ and an $\ell_p$-norm, the uncertainty sets are $U^i_N=\{\zeta\in\Xi:\|\zeta-\xi^i\|\le\epsilon_N\}$ and

$$\hat v^{SRO}_N=\inf_x\Big\{c^\top x+\frac1N\sum_{i=1}^N\sup_{\zeta\in U^i_N}Q(x,\zeta)\Big\}.$$

A linear decision rule is a policy $y(\zeta)=y^0+Y\zeta$; the set of them is $\mathcal L$. The multi-policy approximation chooses, besides $x$, one rule $y^i\in\mathcal L$ per sample, feasible on its own set:

$$\hat v^{MP}_N=\inf_{x,\ y^1,\dots,y^N\in\mathcal L}\Big\{c^\top x+\frac1N\sum_{i=1}^N\sup_{\zeta\in U^i_N}q^\top y^i(\zeta)\ :\ Tx+Wy^i(\zeta)\ge h(\zeta)\ \forall\zeta\in U^i_N,\ i\in[N]\Big\}.$$

The single-policy approximation (SP) uses one shared rule for all $i$.

Formalization targets

Goal: Theorem 2 (p. 12)

Assume [A1] $\epsilon_N\to0$; [A2] $v^*$ is finite and $\mathbb E\|\xi\|<\infty$; [A3] the optimal set of (OPT) is nonempty and bounded; [A4] there are $x$ and $\epsilon>0$ such that around every $\hat\zeta\in\Xi$ some linear decision rule is feasible on $B(\hat\zeta,\epsilon)\cap\Xi$. Then

$$\lim_{N\to\infty}\hat v^{SRO}_N=\lim_{N\to\infty}\hat v^{MP}_N=v^*\quad\text{a.s.},$$

and almost surely every accumulation point of optimal first-stage decisions of (SRO) or (MP) is optimal for (OPT).

Milestones

1. SAA value consistency, cited in the proof of Theorem 2 (p. 20): $\hat v^{SAA}_N\to v^*$ a.s. under [A2]–[A3].
2. Theorem 1 (p. 10): $\hat v^{SRO}_N\le\hat v^{MP}_N\le\hat v^{SP}_N$, pointwise in $x$ as well, for any policy class.
3. Lemma 5 (p. 34) and Lemma 9 (p. 40): below the radius $\Delta_\Xi$ of a point, $B(\hat\zeta,\epsilon)\cap\Xi$ scales about $\hat\zeta$ and translates along the relative interior of a face.
4. Lemma 1 (p. 14): [A4] is equivalent to a condition on minimal faces ([A5]) and to feasibility with finitely many recourse matrices ([A6]).
5. Display (3) (p. 16) and Lemma 2 (p. 16): feasibility of rules with matrices in a set $\mathcal C$ moves to decisions $\lambda x^*+(1-\lambda)x$ near $x^*$, with a uniform smaller radius.
6. Lemma 3 (p. 17): $Q^{\mathcal C}_\epsilon(x,\zeta)\le Q(x^*,\zeta)+\epsilon\eta^{\mathcal C}+L\|x-x^*\|_*$ on the set $\Xi^*$ of realizations feasible for $x^*$.
7. SAA argmin consistency, cited on p. 22: accumulation points of near-optimal SAA solutions are a.s. optimal.

Significance

Theorem 2 says that a linear or second-order cone program with $O(N)$ variables and constraints (Proposition 1) is a consistent estimator of the optimal value and decisions of a two-stage stochastic linear program, under assumptions comparable to those for SAA, for unbounded $\Xi$ and without relatively complete recourse. Theorem 1 adds that (MP) is always a valid upper approximation of (SRO), so the same limit holds for the intractable SRO problem.

The result is proved in the paper; nothing here is open. No part of it has been machine-checked. A complete development would give a verified model of two-stage linear programs with extended-valued recourse, a verified sample-robust and multi-policy layer, and the polyhedral lemmas on balls intersected with polyhedra (Lemmas 5, 9 and display (3)), which are reusable for other robust and distributionally robust convergence results. The two cited consistency statements (milestones 1 and 7) would be the first formal consistency results for SAA with extended-valued convex integrands.

Difficulty

The upper bound $\limsup\hat v^{MP}_N\le v^*$ cannot be obtained by plugging an optimal $x^*$ into (MP): $x^*$ need not admit any linear decision rule feasible on a neighbourhood of a sample, and without relatively complete recourse a sample near the boundary of the feasible region may admit none at all. The proof perturbs $x^*$ towards the point given by [A4], which requires the uniform radius of display (3), obtained from an induction over the faces of $\Xi^*$ in Appendix C. Lemma 1's direction [A4] $\Rightarrow$ [A6] is a second induction over face dimension (Appendix B).

The lower bound reduces to SAA, but the SAA consistency it needs is for an extended-valued, merely lower semicontinuous convex integrand (King and Wets 1991), for which Mathlib has no epi-convergence theory and no law of large numbers for random lower semicontinuous functions. A uniform law of large numbers on a compact set does not apply: the feasible region need not be bounded and $Q$ is $+\infty$ off a polyhedron.

Formalization scope

Vectors are Fin k → ℝ; the $\ell_p$-norm is that of PiLp p for an arbitrary p : ℝ≥0∞ with 1 ≤ p, the dual norm is $\sup\{u^\top v:\|u\|\le1\}$, and the same p is used on $\mathbb R^n$ in Lemma 3. Every optimal value ($Q$, $V^*$, $v^*$, the SAA, SRO, SP and MP values, $Q^{\mathcal C}_\epsilon$, $\eta^{\mathcal C}$, $\Delta_\Xi$) is an infimum or supremum in EReal: "min" and "max" are read as inf and sup, attainment is never assumed, infeasibility gives $+\infty$, and the factor $1/N$ is the real $N^{-1}$. The expectation is the platform definition DupacovaWets.Consistency.expect ($+\infty$ when $\int Q^+=\infty$, else $\int Q^+-\int Q^-$), which agrees with the usual expectation whenever $v^*$ is finite. Samples are ξ 0, ξ 1, …, independent with law $\mu$ and $\mu(\Xi^c)=0$; the paper's $\xi^1,\dots,\xi^N$ are the first $N$. The radii $\epsilon_N\ge0$ are deterministic. (MP) is stated as printed with $N$ policies. Faces of $\Xi$ are nonempty sets $\{\zeta\in\Xi: G_I\zeta=g^0_I\}$, and the relative interior is intrinsicInterior.

Trivializing encodings are ruled out: $Q$ is not real-valued with a junk value for infeasibility, the expectation is not a Bochner integral of a real truncation, optimal values are not real sInfs, [A4] is the printed local condition and not the global single-rule condition of Proposition 2, and the accumulation-point clauses quantify over sequences that are optimal for all large $N$ (requiring optimality at $N=0$ would make them vacuous).

Disclosed readings: the accumulation-point clauses of Theorem 2 hold on one almost-sure event for every eventually-optimal sequence; Lemmas 2 and 3 and display (3) carry §4.2's standing [A2]–[A3], the support condition, and optimality of $x^*$; Lemmas 5 and 9 assume the appendix's normalization $\|g_i\|_*=1$ but not minimality of the representation; display (3)'s set-builder, which omits its bound variable, is read as in Theorem 3; Lemma 2 is stated as printed with $\lambda x^*+(1-\lambda)x$, although its proof derives the equivalent form with $\lambda$ and $1-\lambda$ swapped.

Contributions welcome: proofs of any milestone, in particular LP strong duality in this inequality form for Lemma 3, the polyhedral Lemmas 5 and 9, and the SAA consistency results, which are reusable beyond this mission.

Selected references

• D. Bertsimas, S. Shtern, B. Sturt, Two-Stage Sample Robust Optimization, arXiv:1907.07142v4, 3 Nov 2020 (the version formalized; later a Technical Note in Operations Research, 2022). https://arxiv.org/abs/1907.07142v4
• D. Bertsimas, S. Shtern, B. Sturt, A data-driven approach to multi-stage stochastic linear optimization, preprint, 2018. http://www.optimization-online.org/DB_HTML/2018/11/6907.html
• A. J. King, R. J.-B. Wets, Epi-consistency of convex stochastic programs, Stochastics and Stochastic Reports 34(1–2):83–92, 1991.
• S. M. Robinson, Analysis of sample-path optimization, Mathematics of Operations Research 21(3):513–528, 1996. https://doi.org/10.1287/moor.21.3.513
• M. Conforti, G. Cornuéjols, G. Zambelli, Integer Programming, Springer, 2014. https://doi.org/10.1007/978-3-319-11008-0

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

$$\text{(LP-P)}\qquad \min_x \sum_{i<j}a_{ij}x_{ij}\quad\text{s.t.}\quad x_{ij}\le x_{ik}+x_{jk},\quad x_{ij}+x_{ik}+x_{jk}\le2,\quad \sum_{i<j}x_{ij}=\frac{n^2}{4},$$

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

$$\lim_{n\to\infty}\mathbb P_{(V_1,G)\sim\mathcal G_{n,p,q}}\big[\text{(LP-P) does not recover }V_1,V_2\big]=1.$$

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.

The deterministic distance criterion (Theorem 5) is posed in mission 4 and is not restated. Contributions are welcome on the coupling, Hoeffding-type concentration of edge counts, and the Erdős–Rényi distance asymptotics. These are reusable for any finite random-graph development.

Selected references

• A. Del Pia, A. Khajavirad, D. Kunisky, Linear Programming and Community Detection, Mathematics of Operations Research, 2023; arXiv:2006.03213v2. https://arxiv.org/abs/2006.03213
• E. Abbe, A. S. Bandeira, G. Hall, Exact recovery in the stochastic block model, IEEE Trans. Inf. Theory 62 (2016) 471–487. https://arxiv.org/abs/1405.3267
• A. S. Bandeira, Random Laplacian matrices and convex relaxations, Found. Comput. Math. 18 (2018) 345–379. https://arxiv.org/abs/1504.03987
• B. Bollobás, Random Graphs, 2nd ed., Cambridge Studies in Advanced Mathematics 73, Cambridge University Press, 2001. https://doi.org/10.1017/CBO9780511814068
• N. Shimizu, The average distance of dense homogeneous random graphs, Mathematical Engineering Technical Report, Department of Mathematical Informatics, The University of Tokyo, November 2017 (Theorem 1; reference [38] of the paper). https://www.keisu.t.u-tokyo.ac.jp/research/techrep/

Motivation

The stochastic block model (SBM) is the standard benchmark for community detection: a random graph whose vertices are split into hidden communities, with denser connections inside a community than across. For two equal communities, the best possible estimator of the hidden partition is the minimum bisection problem, which is NP-hard in the worst case. Its tractable relaxations are therefore compared by asking for which edge densities they still recover the hidden partition exactly.

For semidefinite programming the answer is complete in the logarithmic-degree regime: Abbe, Bandeira and Hall (arXiv:1405.3267) located the information-theoretic threshold $\sqrt\alpha-\sqrt\beta=\sqrt2$, and the SDP relaxation was shown to reach it by Hajek, Wu and Xu (arXiv:1412.6156) and by Bandeira (arXiv:1504.03987). Linear programming relaxations are cheaper and widely used in combinatorial optimization, but their behaviour on the SBM was not known. Del Pia, Khajavirad and Kunisky (arXiv:2006.03213, Mathematics of Operations Research, 2023) study the most common one, the metric relaxation. This mission formalizes their result for the logarithmic-degree regime (Theorem 8): there the LP relaxation fails to recover the hidden partition with high probability, at every choice of the parameters.

Setting

Let $V=\{1,\dots,n\}$ with $n$ even. A bisection is a partition $V=V_1\sqcup V_2$ with $|V_1|=|V_2|=n/2$; its cost in a graph $G$ is the number of edges between $V_1$ and $V_2$. Given a fixed planted bisection $V_1,V_2$, an optimization problem recovers it if its unique optimal solution corresponds to $V_1,V_2$.

The cut vector $\bar x\in\{0,1\}^{\binom n2}$ of $V_1,V_2$ has $\bar x_{ij}=1$ exactly when $i,j$ lie on different sides. With $a_{ij}=1$ for edges and $0$ otherwise, the metric relaxation is

$$\text{(LP-P)}\quad \min_x \sum_{i<j}a_{ij}x_{ij}\ \ \text{s.t.}\ \ x_{ij}\le x_{ik}+x_{jk},\ \ x_{ij}+x_{ik}+x_{jk}\le2,\ \ \sum_{i<j}x_{ij}=\frac{n^2}{4},$$

the first family over distinct $i,j,k$ and the second over $i<j<k$, with $x_{ji}:=x_{ij}$. Every bisection's cut vector is feasible.

The distance $\rho_G(i,j)$ is the length of a shortest $i$–$j$ path ($+\infty$ across components). The diameter is $\rho_{\max}(G)=\max_{i,j}\rho_G(i,j)$ and the average distance is $\rho_{\mathrm{avg}}(G)=\frac{2}{n^2}\sum_{i<j}\rho_G(i,j)$.

The Erdős–Rényi model $\mathcal G_{n,p}$ draws each edge independently with probability $p$. The SBM $\mathcal G_{n,p,q}$ chooses a bisection $V_1,V_2$ uniformly at random, then draws each pair inside a side with probability $p$ and each pair across with probability $q$, independently, where $p>q$. The logarithmic-degree regime (21) is

$$p=\alpha\frac{\log n}{n},\qquad q=\beta\frac{\log n}{n},\qquad \alpha>\beta>0 .$$

An event $A_n$ holds with high probability if $\mathbb P[A_n]\to1$ as $n\to\infty$.

Formalization targets

Goal: Theorem 8 (p. 18)

$$\alpha>\beta>0\ \Longrightarrow\ \lim_{n\to\infty}\mathbb P_{\mathcal G_{n,p,q}}\big[\text{(LP-P) does not recover }V_1,V_2\big]=1 .$$

Milestones

1. The threshold of [2] (p. 14, strict cases): if $\sqrt\alpha-\sqrt\beta>\sqrt2$, the minimum bisection problem recovers $V_1,V_2$ with high probability; if $\sqrt\alpha-\sqrt\beta<\sqrt2$, it does not.
2. Proposition 13 (p. 29): for $\alpha>1$ and $G\sim\mathcal G_{n,\alpha\log n/n}$, $\rho_{\max}(G)\in\big((1-\epsilon)\frac{\log n}{\log\log n},(1+\epsilon)\frac{\log n}{\log\log n}\big)$ with high probability.
3. Proposition 15 (p. 29, Theorem 1 of Chung–Lu): for $\alpha>1$, $\rho_{\mathrm{avg}}(G)\in\big((1-\epsilon)\frac{\log n}{\log pn},(1+\epsilon)\frac{\log n}{\log pn}\big)$ with high probability.
4. Proposition 19 (p. 30): for $\alpha>\beta>0$ with $\frac{\alpha+\beta}{2}>1$ and $G\sim\mathcal G_{n,p,q}$,

$$(1-\epsilon)\frac{\log n}{\log\log n}\le\rho_{\mathrm{avg}}(G)\le\rho_{\max}(G)\le(1+\epsilon)\frac{\log n}{\log\log n}$$

with high probability.

Two results the proof of Theorem 8 uses are posed in sibling missions of this series and are not restated here: Theorem 5 (a distance-based non-recovery criterion for (LP-P), mission 4) and the coupling Proposition 11 together with the crossing-edge count (26) (mission 6).

Significance

The result. Theorem 8 separates linear from semidefinite programming on a natural statistical problem. In the logarithmic regime the SDP relaxation recovers the planted bisection whenever any method can, while the metric LP fails with high probability for all $\alpha>\beta>0$, including parameters far above the information-theoretic threshold. The paper's Theorem 6 shows that in the very dense regime (constant $p,q$) the LP does succeed when $p-q>1/2$; Theorem 8 shows that at logarithmic degree no such window exists.

Formalizing it. The theorem is proved in the paper, modulo results cited from the random-graph literature. Nothing in this mission is machine-checked yet. Formalization adds a precise account of what the cited distance asymptotics assert; Proposition 19's upper bound is justified in the paper only by reference to "a standard result on the diameter of the SBM" obtained by adapting an argument of Abbe's survey, so a complete proof of it is new work. Propositions 13 and 15 are classical facts about Erdős–Rényi graphs that have no formal proof in any library known to the curators, and are reusable well beyond community detection.

Difficulty

The LP side of the argument is deterministic and finite. The difficulty is probabilistic. The distance results require tight control of breadth-first neighbourhood growth in sparse random graphs near the connectivity threshold, where the average degree is only logarithmic, with error terms small enough to pin the diameter to a $(1\pm\epsilon)$ window. A first-moment estimate of path counts gives only one side of each bound. In the SBM the two edge probabilities make neighbourhood growth inhomogeneous, so the Erdős–Rényi results do not transfer verbatim. The threshold of [2] is a separate sharp large-deviation statement, at the level of individual vertices' in- and out-degrees.

Formalization scope

Vertices are Fin n (0-based); graphs are SimpleGraph (Fin n). A bisection is recorded by its side $V_1$ with $2|V_1|=n$. The LP variable is a symmetric, zero-diagonal array $x:V\times V\to\mathbb R$, which is a point of $\mathbb R^{\binom n2}$; no box constraints are added. LP recovery means that the planted cut vector is the unique optimal solution; minimum-bisection recovery means that every bisection of cost at most the planted one is the planted unordered partition. Distances are in $\mathbb N\cup\{\infty\}$ and the average distance in $[0,\infty]$, so a disconnected sample has infinite diameter. The random-graph laws are finite sums over all graphs; the SBM averages over all bisections. Edge probabilities are clamped into $[0,1]$, which matters only for the finitely many $n$ with $\alpha\log n/n>1$. "With high probability" is a limit of probabilities equal to $1$; for the SBM the limit runs along $n=2m$. Logarithms are natural.

Disclosed choices relative to the printed statements: Theorem 8 prints only $\alpha,\beta>0$, and $\alpha>\beta$ is added as the SBM's standing assumption $p>q$ (p. 13) and that of (21). The threshold of [2] is printed as an "if and only if"; only the two strict implications are posed, and the boundary $\sqrt\alpha-\sqrt\beta=\sqrt2$ is left out.

The statements cannot be satisfied vacuously: the laws are genuine probability distributions for every $n$, the events compare extended-valued distances without truncation, and recovery requires uniqueness over all real feasible points of (LP-P). An encoding with an empty or degenerate feasible set, or with distances truncated to finite reals, would change the theorems and is excluded.

A complete development needs: Erdős–Rényi and SBM laws, breadth-first exploration bounds for sparse random graphs, the coupling of the SBM between two Erdős–Rényi graphs (mission 6), the LP non-recovery criterion (mission 4), and the information-theoretic threshold of [2]. Contributions on the random-graph distance asymptotics are reusable on their own and especially welcome.

Selected references

• A. Del Pia, A. Khajavirad, D. Kunisky, Linear Programming and Community Detection, Mathematics of Operations Research, 2023. https://arxiv.org/abs/2006.03213 (v2 is the cited version)
• E. Abbe, A. S. Bandeira, G. Hall, Exact recovery in the stochastic block model, IEEE Transactions on Information Theory 62:471–487, 2016. https://arxiv.org/abs/1405.3267
• E. Abbe, Community detection and stochastic block models: recent developments, Journal of Machine Learning Research 18:1–86, 2018. https://arxiv.org/abs/1703.10146
• F. Chung, L. Lu, The diameter of sparse random graphs, Advances in Applied Mathematics 26(4):257–279, 2001. https://doi.org/10.1006/aama.2001.0720
• F. Chung, L. Lu, The average distances in random graphs with given expected degrees, PNAS 99(25):15879–15882, 2002. https://doi.org/10.1073/pnas.252631999
• B. Hajek, Y. Wu, J. Xu, Achieving exact cluster recovery threshold via semidefinite programming, IEEE Transactions on Information Theory 62(5):2788–2797, 2016. https://arxiv.org/abs/1412.6156
• A. S. Bandeira, Random Laplacian matrices and convex relaxations, Foundations of Computational Mathematics 18(2):345–379, 2018. https://arxiv.org/abs/1504.03987

Motivation

The stochastic block model (SBM), introduced by Holland, Laskey and Leinhardt (1983), is the standard random model for networks with community structure, and the basic benchmark for community-detection algorithms (Abbe 2018). In its two-community form the nodes are split into two equal halves, edges inside a half appear with probability $p$, and edges across with probability $q<p$. The task of exact recovery is to identify the hidden halves from the graph alone.

The maximum a posteriori estimator for this model is the minimum bisection problem (find a balanced cut with the fewest crossing edges), which is NP-hard in general. Abbe, Bandeira and Hall (2016) determined when it recovers the planted bisection, and showed that a semidefinite relaxation is as good as the integer program. Del Pia, Khajavirad and Kunisky (arXiv:2006.03213, Mathematics of Operations Research 2023) ask the same question for the cheapest standard relaxation: the metric linear programming relaxation, defined by triangle inequalities. This mission is their positive result in the very dense regime.

Setting

Let $V=\{1,\dots,n\}$ with $n$ even. A bisection is a partition $V=V_1\cup V_2$ with $|V_1|=|V_2|=n/2$. For a graph $G=(V,E)$ let $a_{ij}=1$ if $(i,j)\in E$ and $0$ otherwise. The metric relaxation (LP-P) is

$$\min_{x\in\mathbb R^{\binom n2}}\ \sum_{i<j}a_{ij}x_{ij}\quad\text{s.t.}\quad x_{ij}\le x_{ik}+x_{jk},\quad x_{ij}+x_{ik}+x_{jk}\le 2,\quad \sum_{i<j}x_{ij}=\frac{n^2}{4},$$

the first constraint for all distinct $i,j,k$ with $i<j$, the second for all $i<j<k$, and $x_{ji}:=x_{ij}$. The cut vector $\bar x$ of a bisection has $\bar x_{ij}=0$ for $i,j$ on the same side and $\bar x_{ij}=1$ otherwise. (LP-P) recovers the planted bisection when $\bar x$ is its unique optimal solution.

In the Erdős–Rényi model $\mathcal G_{n,p}$ every pair of nodes is an edge independently with probability $p$. In the SBM $\mathcal G_{n,p,q}$ a bisection $V_1,V_2$ is first chosen uniformly at random; then pairs inside $V_1$ or inside $V_2$ are edges with probability $p$, pairs between them with probability $q$, all independently. $\mathcal G_{n,0,q}$ is the random bipartite graph across a random bisection. An event occurs with high probability (w.h.p.) if its probability tends to $1$ as $n\to\infty$. The graph is very dense when $p$ and $q$ are constants.

For a finite graph $G=(V,E)$ and $b\in\mathbb Z_{\ge0}^V$, a $b$-factor (or $f$-factor) is a set $F\subseteq E$ with exactly $b_v$ edges of $F$ at each node $v$; $N(U,U')$ counts edges with one endpoint in $U$ and one in $U'$; $d_{\min}$, $d_{\max}$ are the minimum and maximum degrees; and the node connectivity $\kappa(G)$ is the minimum number of nodes whose deletion disconnects $G$ (the number of nodes, for a complete graph).

Formalization targets

Goal: Theorem 6 (p. 15)

For constants $0<q<p<1$,

$$p-q>\tfrac12\ \Longrightarrow\ \mathbb P_{G\sim\mathcal G_{n,p,q}}\big[\text{(LP-P) recovers the planted bisection}\big]\xrightarrow[n\to\infty]{}1 .$$

Milestones

1. Proposition 6 (p. 20): for $G\sim\mathcal G_{2m,0,q}$ there is $C>0$ with $d_{\max}\le qm+C\sqrt{m\log m}$ w.h.p.
2. Proposition 5 (p. 20; Schrijver, Cor. 21.4a): a bipartite graph has a $b$-factor iff $N(U,U)\ge b(U)-\frac12 b(V)$ for every $U\subseteq V$.
3. Proposition 3 (p. 14): there is $C_{\mathrm{reg},2}>0$ such that for every $q\in(0,1)$, w.h.p. $G\sim\mathcal G_{n,0,q}$ is a subgraph of a regular bipartite graph with the same bipartition, of degree $d_{\mathrm{reg}}=\frac{qn}2+C_{\mathrm{reg},2}\sqrt{\frac n2\log\frac n2}$ (rounded down).
4. Proposition 8 (p. 24): for $G\sim\mathcal G_{n,p}$ there is $C>0$ with $d_{\min}\ge pn-C\sqrt{n\log n}$ w.h.p.
5. Proposition 9 (p. 24; Bollobás–Thomason): for $G\sim\mathcal G_{n,p}$, $\kappa(G)=d_{\min}$ w.h.p.
6. Proposition 7 (p. 24; Tutte's $f$-factor theorem).
7. Proposition 4 (p. 14): there is $C_{\mathrm{reg},1}>0$ such that for every $p\in(0,1)$, w.h.p. $G\sim\mathcal G_{n,p}$ contains a spanning regular subgraph of degree $d_{\mathrm{reg}}=pn-C_{\mathrm{reg},1}\sqrt{n\log n}$ (rounded up to an even integer).

The deterministic recovery criterion that the goal also depends on, Theorem 4 of the paper (regular sandwiching with $d_{\mathrm{in}}-d_{\mathrm{out}}\ge n/4$), is the goal of mission 3 of this series and is not restated here.

Significance

The result. Theorem 6 is the only positive recovery guarantee for the metric LP in the random setting of the paper. Together with the failure results of Theorems 7 and 8 (missions 6 and 7), it locates the LP strictly between trivial and information-theoretically optimal: it recovers in a region of constant $p,q$, but not up to the threshold $p>q$ that the minimum bisection problem and its SDP relaxation reach. Propositions 3 and 4, that dense random graphs sit inside, and contain, regular graphs of nearly their average degree, are of independent interest in random graph theory, as the authors note.

Formalizing it. The result is proved in the paper; none of it is machine-checked. The mission also requires three classical theorems that are not in Mathlib: the $b$-factor criterion for bipartite graphs, Tutte's $f$-factor theorem (Mathlib has only the perfect-matching case $f\equiv 1$), and the Bollobás–Thomason theorem $\kappa=d_{\min}$ for random graphs, together with degree concentration for $\mathcal G_{n,p}$ and the bipartite SBM. Each is reusable well beyond this paper.

Difficulty

The obvious argument for recovery is to exhibit a dual certificate for (LP-P), which needs regularity of the communities and of the cross edges; a random graph is not regular. The paper bridges the gap by sandwiching the random graph between regular graphs of nearly equal degree, and that step is where the difficulty lies: the existence of a regular sub- or supergraph is a global combinatorial property, characterized by factor theorems with exponentially many conditions, each of which must hold simultaneously with high probability. Degree concentration alone, the first idea, controls only the singleton conditions. Tutte's $f$-factor theorem and the bipartite $b$-factor criterion are themselves substantial combinatorial theorems, and the connectivity statement of Bollobás and Thomason is a deep result on random graphs.

Formalization scope

Nodes are Fin n (0-based). A bisection is a Finset $V_1$ with $2|V_1|=n$. Points of $\mathbb R^{\binom n2}$ are symmetric arrays with zero diagonal; (LP-P) has no box constraints $0\le x\le1$ (they are implied by the constraints and adding them would change the LP). Recovery means: $\bar x$ is optimal and every optimal solution equals $\bar x$.

The random-graph laws are finite: a probability is a weighted sum over all graphs on Fin n, with independent edge weights, and for the SBM an average over all bisections; the event may depend on the drawn bisection. Edge probabilities are clamped into $[0,1]$, which is the identity on the parameters used here. "With high probability" is Tendsto … atTop (𝓝 1), along $n=2m$ for the SBM. The standing assumption $p>q$ is not built into the law, so that $\mathcal G_{n,0,q}$ is the case $p=0$.

Disclosed readings: the printed $d_{\mathrm{reg}}$ of Propositions 3 and 4 is not an integer; Proposition 3 is posed with degree $\lfloor d_{\mathrm{reg}}\rfloor$ and Proposition 4 with $2\lceil d_{\mathrm{reg}}/2\rceil$, the least even integer $\ge d_{\mathrm{reg}}$ (the proof assumes $d_{\mathrm{reg}}$ even). $\kappa(K_n)=n$ as on p. 24. Quantifier order follows each page: in Propositions 3 and 4 the constant precedes the probability parameter, in Propositions 6 and 8 it follows it; no constant depends on $n$.

A statement in which "with high probability" is replaced by a positive probability or an eventual bound, in which the bisection is fixed rather than random, or in which the regular degree is compared with an irrational real (an empty event) is not this mission's target.

Infrastructure needed: the finite random-graph laws, Hoeffding-type concentration over them, the two factor theorems, and node connectivity. Proofs of any milestone, and of the classical results as general graph theory, are welcome.

Selected references

• A. Del Pia, A. Khajavirad, D. Kunisky, Linear Programming and Community Detection, Mathematics of Operations Research, 2023; arXiv:2006.03213v2. https://arxiv.org/abs/2006.03213
• E. Abbe, A. S. Bandeira, G. Hall, Exact Recovery in the Stochastic Block Model, IEEE Transactions on Information Theory 62(1), 2016. https://arxiv.org/abs/1405.3267
• E. Abbe, Community Detection and Stochastic Block Models: Recent Developments, Journal of Machine Learning Research 18, 2018. https://arxiv.org/abs/1703.10146
• P. W. Holland, K. B. Laskey, S. Leinhardt, Stochastic Blockmodels: First Steps, Social Networks 5(2), 1983. https://doi.org/10.1016/0378-8733(83)90021-7
• W. T. Tutte, The Factors of Graphs, Canadian Journal of Mathematics 4, 1952. https://doi.org/10.4153/CJM-1952-028-2
• A. Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer, 2003 (Corollary 21.4a).
• B. Bollobás, A. Thomason, Random Graphs of Small Order, in Random Graphs '83, North-Holland Mathematics Studies 118, 1985 (Theorem 1).
• A. Frieze, M. Karoński, Introduction to Random Graphs, Cambridge University Press, 2016 (Chapter 3). https://doi.org/10.1017/CBO9781316339831

Motivation

The minimum bisection problem asks, for a graph on an even number $n$ of vertices, for a split of the vertices into two halves that cuts as few edges as possible. It is NP-hard, and it is the maximum a posteriori estimator for the two-community stochastic block model (SBM), the standard benchmark for community detection (Abbe, 2018). Convex relaxations are the usual way to make such estimators tractable while keeping guarantees. For the semidefinite relaxation, exact-recovery thresholds are known (Abbe, Bandeira, Hall, 2016; Hajek, Wu, Xu, 2016). Linear programming relaxations are cheaper and much used in combinatorial optimization, but their recovery properties were not understood.

Del Pia, Khajavirad and Kunisky (arXiv:2006.03213v2, Mathematics of Operations Research, 2023) study the best-known LP relaxation of minimum bisection, the metric relaxation. They give a sufficient condition for it to recover a planted bisection (Theorem 4) and a necessary one (Theorem 5). This mission formalizes the necessary condition. Its consequence, developed in §4 of the paper, is that the metric relaxation fails with high probability in most SBM regimes, including those where the minimum bisection itself succeeds.

Setting

Let $G=(V,E)$ be a simple graph on $V=\{1,\dots,n\}$, and write $(i,j)$ for an edge with $i<j$; set $a_{ij}=1$ if $(i,j)\in E$ and $a_{ij}=0$ otherwise. A bisection is a partition of $V$ into two sets $V_1,V_2$ with $|V_1|=|V_2|=n/2$. One fixed bisection, unknown to the solver, is the planted bisection; $E_0$ is the set of edges with one end in $V_1$ and the other in $V_2$.

The cut vector $\bar x\in\{0,1\}^{\binom n2}$ of the planted bisection has $\bar x_{ij}=1$ exactly when $i$ and $j$ lie on different sides. The metric relaxation is the linear program, with $x_{ji}:=x_{ij}$,

$$\min_x\ \sum_{1\le i<j\le n}a_{ij}x_{ij}\quad\text{s.t.}\quad x_{ij}\le x_{ik}+x_{jk}\ (1),\qquad x_{ij}+x_{ik}+x_{jk}\le 2\ (2),\qquad \sum_{1\le i<j\le n}x_{ij}=\frac{n^2}{4}\ (3),$$

where (1) ranges over distinct $i,j,k$ with $i<j$ and (2) over $i<j<k$. The LP recovers the planted bisection if $\bar x$ is its unique optimal solution. The objective at $\bar x$ is $|E_0|$.

The graph distance $\rho_G(i,j)$ is the length of a shortest $i$–$j$ path ($+\infty$ across components). The diameter and the average distance are

$$\rho_{\max}(G)=\max_{i,j\in V}\rho_G(i,j),\qquad \rho_{\mathrm{avg}}(G)=\frac{2}{n^2}\sum_{1\le i<j\le n}\rho_G(i,j).$$

The average is over all $n^2$ ordered pairs, the diagonal included. For $n\ge5$ define

$$c(G)=\max\Big\{0,\ \frac{3\rho_{\max}(G)-4\rho_{\mathrm{avg}}(G)}{1-4/n}\Big\}.\qquad(17)$$

Formalization targets

Goal: Theorem 5

For a connected graph $G$ on $n\ge5$ nodes with a planted bisection,

$$\frac{1+c(G)}{2\rho_{\mathrm{avg}}(G)+2c(G)(1-\frac1n)}\,|E|<|E_0|\quad(18)\qquad\Longrightarrow\qquad\text{(LP-P) does not recover the planted bisection.}$$

Milestones

The proof of Theorem 5 works with the point $\tilde x\in\mathbb R^{\binom n2}$,

$$\tilde x_{ij}=\frac{\rho_G(i,j)+c(G)}{2\rho_{\mathrm{avg}}(G)+2c(G)(1-\frac1n)}.$$

The mission poses three statements about it, for a connected $G$ on $n\ge5$ nodes:

1. display (19), p. 12: for $i<j<k$, $\displaystyle\tilde x_{ij}+\tilde x_{ik}+\tilde x_{jk}\le\frac32\cdot\frac{\rho_{\max}(G)+c(G)}{\rho_{\mathrm{avg}}(G)+c(G)(1-\frac1n)}$;
2. p. 13: $\tilde x$ is feasible for (LP-P);
3. p. 13: the objective of (LP-P) at $\tilde x$ equals $\displaystyle\frac{1+c(G)}{\rho_{\mathrm{avg}}(G)+c(G)(1-\frac1n)}\cdot\frac{|E|}{2}$.

Significance

The result. Theorem 5 is a deterministic certificate of failure, stated for any connected graph, not for a random model. It reduces the question "does the LP recover?" to comparing two numbers that depend only on the distance profile of $G$ and on the fraction of edges cut by the planted bisection. When typical distances are close to the diameter, $c(G)$ is small and (18) asks only that $|E_0|/|E|$ exceed roughly $1/(2\rho_{\mathrm{avg}}(G))$. In random graphs typical distances are close to the diameter. The paper's Theorems 7 and 8 combine Theorem 5 with known distance asymptotics of Erdős–Rényi graphs (Bollobás, Random Graphs, 2001; Chung, Lu, 2001). They show that the metric relaxation fails with high probability in the dense and logarithmic-degree SBM, in contrast with the semidefinite relaxation. Those theorems are separate missions of this series and use Theorem 5 as a black box.

Formalizing it. The result is proved in the paper; no machine-checked version is known. The mission produces a formal metric relaxation of minimum bisection, with LP recovery defined as uniqueness of the optimum, and links it to graph distances through Mathlib's SimpleGraph.edist/ediam. The definitions are written to coincide with those of the other missions of this series, so that one model layer serves the sufficient condition (Theorem 4), the necessary condition (this mission), and the random-graph consequences.

Difficulty

Theorem 5 is not deep, but it is exact. The milestones fix the witness $\tilde x$; the work is in checking it. The obvious candidate, the graph metric $\rho_G$ itself rescaled to satisfy the equality (3), satisfies the triangle inequalities (1). It can violate the perimeter constraints (2) whenever some triangle of vertices is spread out compared with the average distance. The shift by $c(G)$, which depends on $\rho_{\max}$ and on the factor $1-4/n$, is tuned so that (2) holds with no slack in the worst case. A proof has to keep track of the normalization $2/n^2$ (ordered pairs, diagonal included), the factor $1-1/n$, and the sign of $3\rho_{\max}-4\rho_{\mathrm{avg}}$, and must use $n\ge5$ wherever it divides by $1-4/n$. In Lean the further work is converting between sums over ordered pairs, unordered pairs and the edge set, and between extended-valued distances and their real values for a connected graph.

Formalization scope

• Vertices and bisections. Vertices are Fin n (0-based). The planted bisection is a finset $V_1$ with $2|V_1|=n$, and $V_2=V_1^{c}$. $|E_0|$ is the number of pairs $i<j$ adjacent in $G$ and on different sides.
• LP variables. A point of $\mathbb R^{\binom n2}$ is an array $x:\texttt{Fin } n\to\texttt{Fin } n\to\mathbb R$. Feasibility includes symmetry and a zero diagonal, so the free diagonal and lower-triangle entries cannot break uniqueness of the optimum. No bounds $0\le x\le1$ are added; they are not constraints of (LP-P).
• Recovery. LPRecovers G V1 says that the cut vector of $V_1$ is optimal and every optimal point equals it.
• Distances. $\rho_G$ is SimpleGraph.edist (in $\mathbb N\cup\{\infty\}$), $\rho_{\max}$ is SimpleGraph.ediam, and $\rho_{\mathrm{avg}}$ is the printed formula computed in $[0,\infty]$. $c(G)$ and $\tilde x$ use their real values. All statements assume $G$ connected, where these values are finite and $\rho_{\mathrm{avg}}(G)>0$.
• Standing hypotheses. Every statement carries exactly the page's hypotheses: $G$ connected and $n\ge5$, plus, for Theorem 5, the planted bisection. The bisection forces $n$ even, so in effect $n\ge6$; $n\ge5$ is kept as printed. $\tilde x$ is indexed by $i<j$ on the page and is extended symmetrically with zero diagonal.
• Ruled out. A formalization that adds box constraints, drops the symmetric zero-diagonal normalization, averages over $n(n-1)/2$ pairs instead of the printed $2/n^2$, or omits connectivity (where the real value of an infinite distance would be $0$) states a different theorem. None of these is used here.

Contributions welcome: proofs of the three milestones and the goal. Reusable lemmas include the identity $\sum_{i<j}a_{ij}x_{ij}=\sum_{(i,j)\in E}x_{ij}$ for SimpleGraph.edgeFinset, the finiteness of ediam for connected graphs on Fin n, and the bound $\rho_{\mathrm{avg}}(G)\le(1-\frac1n)\rho_{\max}(G)$.

Selected references

• A. Del Pia, A. Khajavirad, D. Kunisky, Linear Programming and Community Detection, Mathematics of Operations Research, 2023; arXiv:2006.03213v2 (2022). https://arxiv.org/abs/2006.03213
• E. Abbe, Community Detection and Stochastic Block Models: Recent Developments, Journal of Machine Learning Research 18 (2018). https://arxiv.org/abs/1703.10146
• E. Abbe, A. S. Bandeira, G. Hall, Exact Recovery in the Stochastic Block Model, IEEE Transactions on Information Theory 62 (2016). https://arxiv.org/abs/1405.3267
• B. Hajek, Y. Wu, J. Xu, Achieving Exact Cluster Recovery Threshold via Semidefinite Programming, IEEE Transactions on Information Theory 62 (2016). https://arxiv.org/abs/1412.6156
• B. Bollobás, Random Graphs, 2nd ed., Cambridge University Press, 2001. https://doi.org/10.1017/CBO9780511814068
• F. Chung, L. Lu, The Diameter of Sparse Random Graphs, Advances in Applied Mathematics 26 (2001). https://doi.org/10.1006/aama.2001.0720

Linear programs as zero-sum games

Linear programming and two-player zero-sum matrix games are two faces of one theory. Von Neumann's minimax theorem is a statement of LP duality, and conversely, since Dantzig's 1951 note, every linear program can be rewritten as a zero-sum game. The equivalence matters in practice whenever an algorithm is much better at one of the two problems. Game solvers based on multiplicative weights and sampling, such as the randomized algorithm of Grigoriadis and Khachiyan (GK95), approximate the value of an $n\times m$ game in time sublinear in the size of the matrix. Carmon, Duchi, Sidford and Tian (arXiv:1903.02675) and van Apeldoorn and Gilyén (arXiv:1904.03180) use such game solvers, classical or quantum, as linear-programming solvers. For that to work, the reduction from a linear program to a game must be explicit, with the exact error budget that the game solver has to meet.

This mission formalizes that reduction as it is stated in §4 of van Apeldoorn and Gilyén (2019), Lemma 12 (p. 14). The paper uses it to turn its quantum zero-sum game solvers into quantum LP solvers with cubic dependence on $R(r+1)/\varepsilon$ (Theorem 13, p. 15).

Setting

The linear program. Let $A \in \mathbb R^{n\times m}$, $b \in \mathbb R^m$ and $c \in \mathbb R^n$. The primal LP (4) and its dual (5) are

$$\max_{y \in \mathbb R^m}\ \{\, b^{\mathsf T}y : Ay \le c,\ y \ge 0 \,\}, \qquad \min_{x \in \mathbb R^n}\ \{\, c^{\mathsf T}x : A^{\mathsf T}x \ge b,\ x \ge 0 \,\}.$$

The paper's standing assumptions (p. 12) are:

• every entry of $A$, $b$ and $c$ lies in $[-1,1]$;
• a constant $R > 0$ is known such that adding $\sum_j y_j \le R$ to the primal does not change its optimal value, and $|c_i| \le R$ for every $i$;
• a constant $r$ is known such that adding $\sum_i x_i \le r$ to the dual does not change its optimal value. The two optimal values coincide, and $\mathrm{OPT}$ denotes the common value.

The game. In a zero-sum game with payoff matrix $M$, the column player picks a mixed strategy $y$ in the standard simplex $\Delta = \{y \ge 0 : \sum_k y_k = 1\}$, and the row player picks the row with the largest payoff. The value of the game (LP (1), p. 2) is

$$\lambda^*(M) = \min_{y \in \Delta}\ \max_i\ (My)_i .$$

The reduction. Fix a threshold $\alpha$. With $e$ the all-ones vector of length $m$, the game matrix (6) acts on the variables $(y, z, h)$ (the original variables, one slack variable and one homogenizing variable):

$$A''' = \begin{pmatrix} e^{\mathsf T} & 1 & -1 \\ -e^{\mathsf T} & -1 & 1 \\ -b^{\mathsf T} & 0 & \alpha/R \\ A & 0 & -c/R \end{pmatrix}.$$

Write $\lambda^* = \lambda^*(A''')$ for its value, and set the error level $\varepsilon''' = \varepsilon/(6R(r+1))$.

Formalization targets

Goal: Lemma 12

For every $\varepsilon > 0$, every threshold $\alpha$ with $|\alpha| \le R$, and every estimate $\tilde\lambda$ with $|\tilde\lambda - \lambda^*| \le \varepsilon'''$,

$$\tilde\lambda > \varepsilon''' \implies \mathrm{OPT} < \alpha, \qquad \tilde\lambda \le \varepsilon''' \implies \mathrm{OPT} \ge \alpha - \varepsilon .$$

This is the paper's "finding the optimal value $\lambda^*$ of the game (6) up to additive error $\varepsilon'''$ suffices to correctly conclude either $\mathrm{OPT} < \alpha$ or $\mathrm{OPT} \ge \alpha - \varepsilon$", with the decision rule its proof uses.

The two cases (milestones)

The goal splits into the two exact implications of the proof:

$$\lambda^* > 0 \implies \mathrm{OPT} < \alpha, \qquad\qquad \lambda^* \le 2\varepsilon''' \implies \mathrm{OPT} \ge \alpha - \varepsilon .$$

The milestones follow the printed proof, all on p. 14:

• the explicit strategy $\hat y$ built from a primal point with objective at least $\alpha$;
• the first case;
• the existence of a strategy that attains the value;
• the bound $|h - 1/2| \le \varepsilon'''$;
• the approximate feasibility and optimality bounds (7)–(8);
• weak duality with relaxed constraints;
• the second case.

Significance

The result. Lemma 12 is the bridge that makes any approximate zero-sum game solver an approximate LP solver. It turns the question "is $\mathrm{OPT} \ge \alpha$?" into a single approximate value computation, and binary search over $\alpha \in [-R, R]$ (p. 12) then locates $\mathrm{OPT}$ to additive error $\varepsilon$. The constant $6R(r+1)$ is the price of the reduction. It fixes how accurately the game must be solved, and therefore the $(R(r+1)/\varepsilon)^3$ and $(R(r+1)/\varepsilon)^{3.5}$ factors of Theorem 13. The same reduction appears, in other forms, in classical sublinear LP solvers.

Formalizing it. The lemma is proved in the paper; this mission produces a machine-checked version with every constant explicit. That is not a formality here. As printed, the second row of (6) is $(-e^{\mathsf T}, 1, 1)$, and with that row the lemma is false: for $n = m = 1$, $A = 1$, $c = 1$, $b = -1$, $R = 1$, $r = 0$ and $\alpha = 0$, one has $\mathrm{OPT} = 0 \ge \alpha$ but $\lambda^* > 0$. The derivation on p. 13 gives $(-e^{\mathsf T}, -1, 1)$, which the mission uses. Step (7) of the proof is written for $\alpha \ge 0$ and needs $|\alpha| \le R$ in general. The mission states the lemma with both repairs, so that later LP-solver formalizations can cite an exact statement. To our knowledge no machine-checked version of this reduction exists.

Difficulty

Each step is elementary, and the difficulty is bookkeeping. The game value is an infimum over the simplex, and the second case needs a strategy that actually attains it, or an approximation argument with slack. The homogenizing variable $h$ is pinned only approximately: an approximately optimal strategy satisfies $h \approx 1/2$ only up to $\varepsilon'''$. That error is multiplied by $\alpha/R$ and $c_i/R$, whose signs are arbitrary, so the inequalities that look natural for nonnegative data fail for negative $\alpha$ or $c_i$. The relaxed constraints then pass through weak duality, where the dual bound $r$ enters, and the errors have to add up to exactly $\varepsilon$. A reading with $\alpha \ge 0$ would cover only half of the binary search.

Formalization scope

• Data. $A$ is Matrix (Fin n) (Fin m) ℝ, $b$ is Fin m → ℝ and $c$ is Fin n → ℝ: constraints are indexed by Fin n and variables by Fin m, as in (4). The paper's index letters in §4 vary.

• Standing assumptions. A structure LPStanding A b c R r OPT collects them:

  • entries of $A$, $b$, $c$ in $[-1,1]$;
  • $R > 0$ and $|c_i| \le R$;
  • $\mathrm{OPT}$ bounds every primal feasible objective and is attained by a primal feasible $y$ with $\sum_j y_j \le R$;
  • $\mathrm{OPT}$ is attained by a dual feasible $x$ with $\sum_i x_i \le r$.

  The last item is the paper's assumption of strong duality, in the form its proof uses. It is a hypothesis, not a theorem to derive.

• The game. The matrix (6) has rows Fin 2 ⊕ (Unit ⊕ Fin n) and columns Fin m ⊕ Fin 2 (with $z$ = inr 0 and $h$ = inr 1), and its second row is the corrected $(-e^{\mathsf T}, -1, 1)$.

• The value. The value is sInf of the image of stdSimplex under $y \mapsto \max_i (My)_i$. It is not an infimum over a membership proposition, which in Lean would return $\min(0, \lambda^*)$ and make the first case vacuous. LP (1)'s side constraint $\lambda \in [-1, 1]$ is omitted because it is inactive for entries in $[-1, 1]$.

• Constants. $\varepsilon''' = \varepsilon/(6R(r+1))$ exactly, with $\varepsilon > 0$.

• Added hypothesis. $|\alpha| \le R$ is the one hypothesis not written in the lemma. §4 supplies it through the binary search range, and through the requirement that (6) be a game with entries in $[-1,1]$.

Trivializing formalizations are ruled out. LPStanding is satisfiable, the second row forces $\sum_j y_j + z = h$, the value is not junk on a positive game, and the goal is stated for every estimate within $\varepsilon'''$ rather than only at $\lambda^* = 0$. A sanity file checks the first three on small instances.

Infrastructure. Everything is built from Mathlib's stdSimplex, Matrix.mulVec and dotProduct. The attainment of the value of a finite matrix game (milestone exists_strategy_le) and weak duality with relaxed constraints are reusable beyond this mission. Proofs of any milestone are welcome, and so are alternative proofs of the second case that avoid attainment by a slack argument.

Selected references

• J. van Apeldoorn and A. Gilyén, Quantum algorithms for zero-sum games, arXiv:1904.03180v1, 2019. https://arxiv.org/abs/1904.03180
• M. D. Grigoriadis and L. G. Khachiyan, A sublinear-time randomized approximation algorithm for matrix games, Operations Research Letters 18(2):53–58, 1995. https://doi.org/10.1016/0167-6377(95)00032-0
• Y. Carmon, J. C. Duchi, A. Sidford and K. Tian, A rank-1 sketch for matrix multiplicative weights, arXiv:1903.02675, 2019. https://arxiv.org/abs/1903.02675
• G. B. Dantzig, A proof of the equivalence of the programming problem and the game problem, in T. C. Koopmans (ed.), Activity Analysis of Production and Allocation, Wiley, 1951, pp. 330–335.
• I. Adler, The equivalence of linear programs and zero-sum games, International Journal of Game Theory 42(1):165–177, 2013. https://doi.org/10.1007/s00182-012-0328-8