Graph Theory

Motivation

Barabási and Albert (Science 1999) proposed preferential attachment as a mechanism behind the heavy-tailed degree distributions observed in the web graph and other networks: vertices arrive one at a time and attach to existing vertices with probability proportional to their degree. Empirical work on such networks reported that typical distances are very small compared with their size. The original description left the model underdetermined (the joint law of the $m$ edges of a new vertex was not specified), so its distances could not be analysed as stated.

Bollobás and Riordan (Combinatorica 2004) fixed a precise version of the model, the LCD model, and determined its diameter: for $m\ge2$ edges per vertex it is asymptotically $\log n/\log\log n$. For $m=1$ the graph is a forest (with loops), and a result of Pittel states essentially that its diameter is of order $\log n$. Together with the degree-sequence analysis of Bollobás, Riordan, Spencer and Tusnády (Random Struct. Alg. 2001), the paper is one of the first rigorous results on a scale-free random graph model.

Setting

The process $G_1^N$. Vertices are $1,\dots,N$. Vertex $t$ sends a single edge to a vertex $g_t\in\{1,\dots,t\}$, chosen given the past with

$$\mathbb P(g_t=i)=\frac{d_{G_1^{t-1}}(i)}{2t-1}\ (i<t),\qquad \mathbb P(g_t=t)=\frac1{2t-1},$$

where $d_{G_1^{t-1}}(i)$ is the degree of $i$ in the graph built so far (a loop counts twice). Loops ($g_t=t$) are allowed.

The graph $G_m^n$. Run $G_1^{mn}$ and identify the vertices $(k-1)m+1,\dots,km$ into a single vertex $k$, for $k=1,\dots,n$. The resulting random graph on $[n]$ is $G_m^n\in\mathcal G_m^n$. The paper's graph has loops and multiple edges; its diameter is the largest graph distance between two vertices of the underlying simple graph.

Almost every. For fixed $m$, a.e. $G_m^n$ has a property if its probability tends to $1$ as $n\to\infty$. All logarithms are natural.

The endpoint model (for the upper bound). Let $r_1,\dots,r_{mn}$ be independent with density $2x$ on $(0,1)$ ($M_2(0,1)$), $R_1\le\dots\le R_{mn}$ their sorted values, $W_i=R_{mi}$, $W_0=0$, $w_i=W_i-W_{i-1}$. Given $0<W_1<\dots<W_n<1$, the random graph $G(W_1,\dots,W_n)$ joins each vertex $i$ to $l_{i,1}$ and $l_{i,2}$, independent with $\mathbb P_L(l_{i,j}=k)=w_k/W_i$ for $k\le i$. The events $E_1,\dots,E_5$ (Lemma 7) say that the $W_i$ follow the profile $\sqrt{i/n}$ and that the spacings $w_i$ are neither too small nor too large in specified ranges.

Formalization targets

Goal: Theorem 1

For fixed $m\ge2$ and $\varepsilon>0$, a.e. $G_m^n$ is connected and

$$(1-\varepsilon)\frac{\log n}{\log\log n}\le\operatorname{diam}(G_m^n)\le(1+\varepsilon)\frac{\log n}{\log\log n}.$$

Lower bound (§4)

• Lemma 2: $\mathbb P(g_j=i)=O((ij)^{-1/2})$ and $\mathbb P(g_j=i,g_k=i)=O(i^{-1}(jk)^{-1/2})$ with absolute constants.
• Lemma 3: events $\bigcap\{g_{j_s}=i_s\}$ with disjoint sets of targets are negatively correlated.
• Lemma 4: $\mathbb P(S\subset G_1^N)\le C^{e(S)}\prod_{ij\in E(S)}1/\sqrt{ij}$ for graphs $S$ with at most one earlier and two later neighbours per vertex.
• Theorem 5: for every $m\ge1$, a.e. $G_m^n$ has $\operatorname{diam}(G_m^n)>\log n/\log(3Cm^2\log n)$, $C$ the constant of Lemma 4.

Upper bound (§§5–8)

• Lemma 6: Chernoff–Janson tails for sums of independent Bernoulli variables.
• Lemma 7: $\mathbb P(E_r)\to1$ for $r=1,\dots,5$.
• The coupling of §6: $G(W)$ with $W_i=R_{mi}$ is stochastically dominated by $G_m^n$ in the subgraph order, i.e. $\mathbb P(G(W)\in\mathcal P)\le\mathbb P(G_m^n\in\mathcal P)$ for every property $\mathcal P$ preserved under adding edges.
• Lemma 10 and Lemma 8: under $E_1,\dots,E_5$, every vertex reaches a useful vertex ($i\le n/(\log n)^5$, $w_i\ge(\log n)^2/n$) by a descending path of length at most $8\log\log n$, with probability $1-o(1)$.
• Lemma 12 (a deterministic growth estimate) and Lemma 11: a useful vertex is joined to vertex $1$ by a path of length at most $(1/2+\varepsilon)\log n/\log\log n$ with probability $1-o(n^{-1})$.
• The display of p. 29: under $E_1,\dots,E_5$, $\mathbb P_L\big(\operatorname{diam}G(W)>(1+\varepsilon/2)\log n/\log\log n+16\log\log n\big)=o(1)$.

Significance

The theorem shows that the diameter of this scale-free graph is smaller by a factor $\log\log n$ than that of a classical random graph with the same constant average degree, and identifies $m=1$ versus $m\ge2$ as the dividing line. It made the "small world" claims about the Barabási–Albert model precise for one exact version of it, and the LCD representation and the endpoint model introduced here were used in later work on preferential attachment.

The result is proved in the paper; nothing here is open. The work of the mission is formalizing the known proof. As far as is known, no machine-checked development of preferential-attachment graphs exists in Mathlib or elsewhere. A complete development would supply a reusable probability space for the attachment process, a Chernoff–Janson inequality for heterogeneous Bernoulli sums, a negative-correlation lemma for the process, and order-statistic estimates for i.i.d. samples, each of independent use.

Difficulty

The lower bound is a first-moment count of short paths, but the edges of $G_1^N$ are not independent: an earlier edge into a vertex raises the chance of later ones. Lemmas 2–4 show that small subgraphs still appear with probability comparable to an independent model with edge probabilities $C/\sqrt{ij}$; Lemma 3 requires a description of the process in which the needed independence is visible.

The upper bound is the hard half. A naive breadth-first expansion from a vertex fails: the weight of the next neighbourhood has the right mean but a very skewed distribution, and vertices near the end of the ordering have few early neighbours. The paper replaces the process by a conditionally independent model given the sorted endpoints $W_i$, controls the $W_i$ globally (Lemma 7), handles late vertices separately (Lemmas 8–10), and runs a weighted expansion with a growing blow-up factor (Lemmas 11–12). Each step needs uniformity in $W$: every $o(\cdot)$ must depend on $n$ only.

Formalization scope

Vertices are stored as Fin N (0-based) and statements read 1-based labels through the accessors tgt and lab. A sequence $(g_t)$ is a dependent function (t : Fin N) → Fin (t+1), its probability is the product of the exact conditional factors $(1+\#\{s<t: g_s=g_t\})/(2t-1)$, and probabilities are finite weighted sums. $G_1^N$, $G_m^n$ and $G(W)$ are Mathlib simple graphs: loops and multiple edges are dropped, which does not change connectivity or distances. The model is the paper's: not uniform attachment, not $m$ independent choices per vertex, and with the self-loop term.

$\operatorname{diam}$ in the goal is SimpleGraph.diam, which is $0$ on a disconnected graph; the goal therefore keeps connectivity explicit, as the page does. Every other diameter bound uses "every two vertices are joined by a walk of length $\le x$", and lower bounds use its negation, so a disconnected graph never satisfies an upper bound by default. Hidden constants follow the paper's quantifier order: the constants of Lemmas 2 and 4 come before every index; each $o(\cdot)$ of §§7–8 is a function $\delta(n)\to0$ chosen before $W$ (a bound chosen after $W$ would make these statements nearly empty); "for $n$ sufficiently large" is $\exists N_0$ before $W$ or $f$. Theorem 5 assumes the bound of Lemma 4 for its constant $C$. Every statement about $G(W)$ assumes $0=W_0<W_1<\dots<W_n<1$. Lemma 7 is stated as "the probability of the complement tends to $0$" under the product law of $M_2(0,1)$; the coupling is stated as the equivalent stochastic-domination inequality for every property preserved under adding edges.

Not formalized: Lemma 9 (a conditional bound given the history of a breadth-first exploration), the LCD representation of $G_1^n$ (§2), and Theorem 13 ($m=1$), which the paper states without proof.

Contributions welcome: proofs of any milestone, the identity $\mathbb P(g_j=i)=\mu_{j-1,i}/(2j-1)$ with $\mu_{t,i}=\prod_{s=i}^t(1+1/(2s-1))$, the LCD representation, and general lemmas about the attachment process and Bernoulli tails.

Selected references

• B. Bollobás and O. Riordan, The diameter of a scale-free random graph, Combinatorica 24(1):5–34, 2004. https://doi.org/10.1007/s00493-004-0002-2
• A.-L. Barabási and R. Albert, Emergence of scaling in random networks, Science 286:509–512, 1999. https://doi.org/10.1126/science.286.5439.509
• B. Bollobás, O. Riordan, J. Spencer and G. Tusnády, The degree sequence of a scale-free random graph process, Random Structures & Algorithms 18(3):279–290, 2001. https://doi.org/10.1002/rsa.1009
• S. Janson, T. Łuczak and A. Ruciński, Random Graphs, Wiley, 2000. https://doi.org/10.1002/9781118032718

Motivation

Belief propagation (BP) is the message-passing algorithm used throughout artificial intelligence, coding theory and statistical physics to approximate marginals of graphical models. On graphs with cycles it is a heuristic: it may fail to converge, and when it converges its output need not be the true marginal. Rigorous guarantees had mostly been confined to the high-temperature regime, as a consequence of a uniform decay of correlations (spatial mixing) under which any boundary condition is forgotten; see the works cited as [3, 23, 26] in §1 of the paper.

Dembo and Montanari (arXiv:0804.4726v3, Ann. Appl. Probab. 20 (2010)) proved that for the ferromagnetic Ising model with a positive external field, BP converges exponentially fast on every graph of bounded degree, at every temperature, and that on locally tree-like graphs its fixed point computes local marginals accurately. The low-temperature regime, where the Gibbs measure on the limiting infinite tree is not unique, is the point: the field breaks the $\pm$ symmetry, and monotonicity replaces spatial mixing.

Setting

Let $G=(V,E)$ be a finite graph in which every vertex has at most $\Delta$ neighbours, $\beta\ge0$ an inverse temperature and $B$ a magnetic field. The Ising model on $G$ is the distribution on spin configurations $\underline x\in\{+1,-1\}^V$

$$\mu(\underline x)=\frac1{Z(\beta,B)}\exp\Big\{\beta\sum_{(i,j)\in E}x_ix_j+B\sum_{i\in V}x_i\Big\}.$$

More generally one allows a field $B_i$ at each vertex, and $B_i=+\infty$ (a vertex pinned to $+1$).

A message $\nu_{i\to j}$ is a distribution on $x_i\in\{+1,-1\}$ attached to the directed edge $i\to j$. The BP iteration is

$$\nu^{(t+1)}_{i\to j}(x_i)=\frac1{z^{(t)}_{i\to j}}\,e^{Bx_i}\prod_{l\in\partial i\setminus j}\ \sum_{x_l}e^{\beta x_ix_l}\,\nu^{(t)}_{l\to i}(x_l),$$

with $\partial i$ the neighbours of $i$ and $z^{(t)}_{i\to j}$ a normalization. An initial condition is positive if $\nu^{(0)}_{i\to j}(+1)\ge\nu^{(0)}_{i\to j}(-1)$ on every directed edge. Distances between distributions are in total variation, $\|p-q\|_{\mathrm{TV}}=\tfrac12\sum_x|p(x)-q(x)|$.

For $i_*\in V$, $U=\mathsf B_{i_*}(r)$ is the ball of radius $r$, $\partial U$ its vertices at distance exactly $r$, and $j(i)$ a neighbour in $U$ of each $i\in\partial U$. Given a BP fixed point $\nu^*$, the BP estimate of the marginal on $U$ is

$$\nu_U(\underline x_U)=\frac1{z_U}\exp\Big\{\beta\sum_{(i,j)\in E_U}x_ix_j+B\sum_{i\in U\setminus\partial U}x_i\Big\}\prod_{i\in\partial U}\nu^*_{i\to j(i)}(x_i).$$

The proofs run through Ising models on rooted trees $\mathsf T$: $\mathsf T(\ell)$ is the tree of the first $\ell$ generations, $\partial\mathsf T(\ell)$ the $\ell$-th generation, and $\mu^{\ell,0}$, $\mu^{\ell,+}$ the Ising models on $\mathsf T(\ell)$ with free and plus boundary conditions (the latter pins $\partial\mathsf T(\ell)$ to $+1$). A random tree is conditionally independent with average offspring bounded by $\Delta$ if, given the first $k$ generations, the offspring numbers of generation $k$ are independent with conditional means at most $\Delta$ (Definition 2.5).

Formalization targets

Goal: Theorem 2.6

For $\beta\ge0$, $B>0$ and $\Delta$, there are $A<\infty$ and $\lambda>0$ depending only on $(\beta,B,\Delta)$ such that every finite graph of maximal degree $\Delta$ has a BP fixed point $\nu^*$ with

$$\sup_{(i,j)\in E}\big\|\nu^{(t)}_{i\to j}-\nu^*_{i\to j}\big\|_{\mathrm{TV}}\le A\exp(-\lambda t)$$

for every positive initial condition and every $t\ge0$. The constants are uniform over graphs; this uniformity is the content of the theorem.

Companion: Theorem 2.7

With $c=c(\beta,B,\Delta)$ and $\lambda>0$: if $\mathsf B_{i_*}(t)$ is a tree, then $\|\mu_U-\nu_U\|_{\mathrm{TV}}\le\exp\{c^{r+1}-\lambda(t-r)\}$.

Milestones

The tree estimates of §3–§4, in the order the proofs use them: Griffiths' inequality (Theorem 3.1); the GHS inequality (Theorem 3.2); the reweighting bound in total variation (Lemma 3.3); marginals on subtrees (Lemma 4.1); the $M/\ell$ bound $\mathbb E\{m^{\ell,+}-m^{\ell,0}\}\le M/\ell$ on root magnetizations (Lemma 4.3); its extension to marginals near the root (Theorem 4.2); a Simon-type factorization of tree correlations (Lemma 4.4); and Corollary 4.5: exponential decay of correlations (4.13), Theorem 4.2 with rate $Ae^{-\lambda t}$, and the root-magnetization bound $\mathbb E\{m^{\ell,+}-m^{\ell,0}\}\le Ae^{-\lambda\ell}$.

Significance

The theorem gives an unconditional convergence guarantee for BP on a nontrivial class of models with cycles, valid deep in the low-temperature phase, with a rate independent of the number of vertices. Theorem 2.7 adds that the fixed point is accurate on locally tree-like graphs such as random regular graphs and sparse Erdős–Rényi graphs, so BP is a polynomial-time algorithm for local marginals there. The tree estimates of §4, in particular the insensitivity of the root to plus versus free boundary conditions on conditionally independent trees, are also the engine of the free-entropy theorem of the same paper (mission 1 of this series).

The results are proved in the paper; none of them, nor Griffiths' or the GHS inequality, has a machine-checked proof known to this mission. Formalizing them produces a reusable library for ferromagnetic Ising models on finite graphs and trees (correlation inequalities, pinned boundary conditions, marginals on subtrees) and a formal account of BP as an operator on message families.

Difficulty

The obvious argument is a contraction: show that one BP step shrinks the distance between message families, uniformly over the graph. At low temperature this fails: the BP map is not a contraction, the infinite-tree Ising model has several Gibbs measures, and without a field BP has several fixed points. Uniform decay of correlations, the tool behind high-temperature results, is false in this regime. What has to be controlled instead is a single, weaker quantity: how much the root of a tree of depth $t$ feels a plus boundary condition compared with a free one, with a bound that is uniform over all trees of bounded average offspring and over all depths. The difficulty is concentrated in that estimate (Lemma 4.3), and in upgrading its $1/\ell$ rate to an exponential one (Corollary 4.5), which is where the positive field enters quantitatively.

Formalization scope

Spins are Booleans (true $=+1$); the edge sum counts each unordered edge once; a field $+\infty$ is a pinned vertex, never a large real number. Graphs are finite (Fintype V) with all degrees at most $\Delta$. Messages are functions on ordered vertex pairs whose values on directed edges are distributions on $\{+1,-1\}$; the BP iterates are computed from the update, not posited. Total variation is $\tfrac12\ell^1$. Trees are encoded by offspring functions on finite words (Ulam–Harris), random trees by probability measures on offspring functions with the product $\sigma$-algebra; conditional independence uses Mathlib's iCondIndepFun, with integrable offspring numbers. Fields on trees are nonrandom functions of the vertex. Expectations that may be infinite, such as $\mathbb E\{C^{|\mathsf T(r)|}\}$, are lower Lebesgue integrals in $[0,\infty]$, and every expectation of a tree functional comes with a measurability conclusion, so that no integral can take a junk value. Constants are quantified before the graph, the tree law and the field, and, where the paper names their dependence (Theorem 4.2's $M(\beta_{\max},B_{\min},\Delta)$ and $C(\beta_{\max},B_{\max})$), as functions of exactly those parameters.

Two readings are fixed explicitly. Theorem 2.7 is stated for every positive BP fixed point, which by Theorem 2.6 is the paper's fixed point. Corollary 4.5's clause (4.13) carries the hypotheses of Theorem 4.2 ($B_i\le B_{\max}$ on $\mathsf T(r-1)$). A fixed point that is not a family of distributions, a "zero message" family, or a bound that holds only because an integral defaults to $0$ does not satisfy these statements.

The computation tree of §5, through which the paper derives Theorems 2.6–2.7 from Corollary 4.5, is a proof device and is not part of any statement; building it is welcome as supporting work. Proofs of the classical inequalities (Griffiths, GHS) are independently reusable.

Selected references

• A. Dembo, A. Montanari, Ising models on locally tree-like graphs, Ann. Appl. Probab. 20(2) (2010) 565–592. arXiv:0804.4726v3, doi:10.1214/09-AAP627
• R. B. Griffiths, C. A. Hurst, S. Sherman, Concavity of magnetization of an Ising ferromagnet in a positive external field, J. Math. Phys. 11 (1970) 790–795. MR0266507
• T. M. Liggett, Interacting Particle Systems, Grundlehren 276, Springer, 1985 (Theorem IV.1.21, Griffiths' inequality). MR776231
• B. Simon, Correlation inequalities and the decay of correlations in ferromagnets, Comm. Math. Phys. 77 (1980) 111–126. MR589426

Motivation

Time-indexed formulations are a standard way to model scheduling problems as integer programs: a binary variable $x_{jt}$ records whether job $j$ starts at time $t$. They were introduced by Pritsker, Watters and Wolfe (1969) and give strong linear relaxations, at the price of many variables. In project scheduling, jobs are linked by time lags: a lag $(i,j)$ of length $d_{ij}$ requires $S_j \ge S_i + d_{ij}$, and since $d_{ij}$ may be negative, lags express both minimal and maximal distances between start times, i.e. time windows. Many project scheduling objectives (weighted completion times, net present value, earliness–tardiness, and the Lagrangian subproblems of resource-constrained scheduling) reduce to minimizing a sum of start-time dependent costs $w_{jt}$ subject to such lags.

Möhring, Schulz, Stork and Uetz showed that this problem, despite being an integer program, is solved by one minimum cut computation in a directed graph built from the time-indexed variables. This makes the Lagrangian relaxation of resource-constrained project scheduling computationally practical, which is the use the paper puts it to.

Timeline.

• 1969: Pritsker, Watters and Wolfe give a time-indexed 0/1 formulation of multiproject scheduling with the weak form of the precedence constraints.
• 1970: Rhys and Balinski show that selection / minimum-weight closure problems reduce to minimum cut.
• 1985: Chang and Edmonds reduce the case of ordinary precedence constraints and unit processing times to minimum-weight closure, hence to minimum cut.
• 1987: Christofides, Alvarez-Valdés and Tamarit propose the strong (disaggregated) form (3) of the temporal constraints.
• 2003: Möhring, Schulz, Stork and Uetz give a direct transformation for arbitrary time lags and arbitrary processing times (Management Science 49(3)).

Setting

Jobs form the set $J = \{0, \dots, n\}$; job $j$ has an integral processing time $p_j \ge 0$. A set $L \subseteq J \times J$ of time lags is given, with integral lengths $d_{ij}$. A schedule is an integral vector $S = (S_0, \dots, S_n)$ of start times; it is feasible if $S_j \ge S_i + d_{ij}$ for all $(i,j) \in L$ and it lies within the horizon $T$: $0 \le S_j$ and $S_j + p_j \le T$. Starting job $j$ at time $t$ costs $w_{jt} \ge 0$. The earliest and latest feasible start times $e(j)$ and $\ell(j)$ are the minimum and the maximum of $S_j$ over feasible schedules. Throughout, a feasible schedule is assumed to exist.

The integer program (1)–(5) has variables $x_{jt} \in \mathbb{Z}$:

$$\min\ w(x) = \sum_{j} \sum_{t=0}^{T} w_{jt} x_{jt} \quad\text{s.t.}\quad \sum_{t=0}^{T} x_{jt} = 1,\qquad \sum_{s=t}^{T} x_{is} + \sum_{s=0}^{t+d_{ij}-1} x_{js} \le 1,\qquad x_{jt} \ge 0,$$

for all $j \in J$, $(i,j) \in L$, $t = 0, \dots, T$, and all variables with $t$ outside $[e(j), \ell(j)]$ are zero.

The minimum cut digraph $D = (V, A)$ has a source $a$, a sink $b$, and nodes $v_{jt}$ for $t = e(j), \dots, \ell(j)+1$. Its arcs are the assignment arcs $(v_{jt}, v_{j,t+1})$ for $t = e(j), \dots, \ell(j)$, of capacity $w_{jt}$; the temporal arcs $(v_{it}, v_{j,t+d_{ij}})$ for $(i,j) \in L$ and $e(i)+1 \le t \le \ell(i)$, $e(j)+1 \le t+d_{ij} \le \ell(j)$; and the auxiliary arcs $(a, v_{j,e(j)})$ and $(v_{j,\ell(j)+1}, b)$. Temporal and auxiliary arcs have infinite capacity. An $a$-$b$-cut $(X, \bar X)$ splits $V$ with $a \in X$, $b \in \bar X$; its capacity $c(X, \bar X)$ is the total capacity of the arcs from $X$ to $\bar X$. An $n$-cut is an $a$-$b$-cut containing exactly one assignment arc of every job. The mapping (7) sends a cut to $x$ with $x_{jt} = 1$ iff $(v_{jt}, v_{j,t+1})$ is in the cut.

Formalization targets

Goal: Theorem 1 (p. 7)

$$\text{(7) is a bijection } \{n\text{-cuts with } c(X,\bar X) < \infty\} \to \{\text{feasible } x \text{ of (1)–(5)}\},\qquad c(X, \bar X) = w(x),$$ $$\text{and}\quad c(X, \bar X) = w(x^*) \text{ for every minimum } a\text{-}b\text{-cut } (X, \bar X) \text{ and some optimal } x^*.$$

Milestones (in the paper's order of proof)

1. Proof of Lemma 1 (p. 7): for every lag $(i,j) \in L$, $e(i) + d_{ij} \le e(j)$.
2. Lemma 1 (p. 6): every minimum $a$-$b$-cut has an $n$-cut of the same capacity.
3. Lemma 2 (p. 8): every feasible $x$ is the image of an $n$-cut $(X, \bar X)$ with $w(x) = c(X, \bar X)$.
4. p. 8: the mapping (7) is injective on finite-capacity $n$-cuts.
5. Lemma 3 (p. 8): the image of a finite-capacity $n$-cut is feasible, with $w(x) = c(X, \bar X)$.
6. Lemma 4 (p. 8): the minimum cut capacity equals the optimal value.

A companion statement (p. 8) covers strictly positive weights: then every minimum $a$-$b$-cut is an $n$-cut, and (7) is a bijection between minimum $a$-$b$-cuts and optimal solutions.

Significance

The result. Theorem 1 shows that the time-indexed integer program with arbitrary (also negative) time lags has an integral linear relaxation in disguise: it is a minimum cut problem, solvable in strongly polynomial time, $O(nmT^2 \log(n^2T/m))$ with push-relabel (Corollary 1). This is what allows the paper to compute Lagrangian lower bounds for resource-constrained project scheduling with time windows by repeated minimum cut computations, and to use the resulting dual information for list scheduling heuristics (§§3–4). The construction is a direct reduction, sparser than the closure-based route of Chang and Edmonds.

Formalizing it. The result is proved on paper; no machine-checked proof is known. The mission produces a formal model of the time-indexed project scheduling IP with time lags and of its cut digraph, together with checked versions of the correspondence and of each lemma of its proof. The model of cuts with infinite capacities and tagged parallel arcs is reusable for other cut-based reductions (selection, closure, and image segmentation problems).

Difficulty

The bijection itself is bookkeeping. The substance is in two places. First, Lemma 1: a minimum cut need not be an $n$-cut (a zero-weight assignment arc can be cut twice), and repairing it to the canonical prefix cut must not introduce a temporal arc into the cut. The repair argument shifts a hypothetical violating temporal arc back along the lag, and needs that the lags are consistent with the earliest and latest start times, $e(i) + d_{ij} \le e(j)$ and $\ell(i) + d_{ij} \le \ell(j)$, facts about the feasible schedules rather than about the graph. Second, Lemma 3: temporal arcs exist only for $t$ in a restricted window, so a finite-capacity $n$-cut satisfies the temporal constraint (3) only after a boundary case analysis at $t = e(i)$ and $t + d_{ij} > \ell(j)$. The naive reading "every temporal constraint is an infinite arc" is false at the boundary.

Formalization scope

An instance is a Lean structure with fields $p, L, d, T, w$; jobs are Fin (n + 1), start times are integers, and $x$ is a function $J \to \mathbb{N} \to \mathbb{Z}$ (integrality by type). The standing assumptions of §2 are hypotheses of every theorem: $w_{jt} \ge 0$ (p. 5) and the existence of a feasible schedule (p. 4). The horizon condition $0 \le S_j$, $S_j + p_j \le T$ is read from "$t = 0, \dots, T$", "$e(j) \ge 0$" and "$\ell(j) \le T - p_j$" (p. 5), which the paper never writes as a formula. The paper's artificial jobs $0$ and $n$ with zero processing time are not assumed: §2.2 never uses them, so the statements are stronger. $e(j)$ and $\ell(j)$ are defined as the minimum and maximum feasible start times, never taken as parameters. Capacities live in $[0, \infty]$ with $\infty$ on temporal and auxiliary arcs; arcs are a tagged type, so parallel arcs and self-lags remain distinct. A cut is its source side $X \subseteq V$. Running-time claims (the $O(nT)$ clause of Lemma 1, Corollary 1, the Goldberg–Rao bound) are not formalized.

Trivializing formalizations are ruled out: the integer program is not replaced by schedules, infinite capacities are not big-M constants, the minimum is taken over all $a$-$b$-cuts and not only over $n$-cuts, and $e, \ell$ are computed from the instance rather than quantified over.

Needed infrastructure: finite sums in $[0, \infty]$, minimum and maximum of finite sets of integers, and elementary reasoning on integer intervals. Proofs of any milestone, and of the auxiliary fact $\ell(i) + d_{ij} \le \ell(j)$ used in Lemma 3, are welcome.

Selected references

• R. H. Möhring, A. S. Schulz, F. Stork, M. Uetz, Solving project scheduling problems by minimum cut computations, Management Science 49(3):330–350, 2003. https://doi.org/10.1287/mnsc.49.3.330.12737 (formalized from the authors' manuscript, July 2000, revised April and November 2002).
• A. A. B. Pritsker, L. J. Watters, P. M. Wolfe, Multiproject scheduling with limited resources: a zero-one programming approach, Management Science 16(1):93–108, 1969. https://doi.org/10.1287/mnsc.16.1.93
• G. J. Chang, J. Edmonds, The poset scheduling problem, Order 2(2):113–118, 1985. https://doi.org/10.1007/BF00334849
• N. Christofides, R. Alvarez-Valdés, J. M. Tamarit, Project scheduling with resource constraints: a branch and bound approach, European Journal of Operational Research 29(3):262–273, 1987. https://doi.org/10.1016/0377-2217(87)90240-2
• J. M. W. Rhys, A selection problem of shared fixed costs and network flows, Management Science 17(3):200–207, 1970. https://doi.org/10.1287/mnsc.17.3.200
• A. V. Goldberg, R. E. Tarjan, A new approach to the maximum-flow problem, Journal of the ACM 35(4):921–940, 1988. https://doi.org/10.1145/48014.61051

Motivation

The ferromagnetic Ising model is the basic model of statistical mechanics for interacting binary variables. On a finite graph it is a probability distribution over spin configurations, and its normalizing constant, the partition function, encodes the thermodynamics: the free entropy per vertex determines the magnetization, the correlations, and the location of phase transitions. On lattices this quantity is understood only in special cases. On sparse random graphs, such as random regular graphs and Erdős–Rényi graphs with bounded average degree, physicists predicted it with the cavity method (Mézard and Parisi, The Bethe lattice spin glass revisited, 2001): locally these graphs look like trees, and on trees the model can be solved by a recursion. The same recursion underlies belief propagation, the message-passing algorithm used in coding theory and machine learning.

Timeline:

• Dembo and Montanari (2008/2010), Ising models on locally tree-like graphs, Ann. Appl. Probab. 20 (2010) 565–592: for every uniformly sparse graph sequence converging locally to a Galton–Watson tree whose offspring law has finite mean, the free entropy density converges at every temperature $\beta \ge 0$ and every field $B$, and for $B > 0$ the limit is the Bethe prediction. Earlier rigorous results covered special cases, among them Erdős–Rényi graphs in a restricted range of parameters (reference [7] of the paper) and random regular graphs (reference [11]).
• Dembo, Montanari and Sun (2013), Factor models on locally tree-like graphs, extended the approach to a class of factor models on locally tree-like graphs.

Setting

Let $G_n = (V_n = [n], E_n)$ be a sequence of finite graphs. The Ising measure at inverse temperature $\beta \ge 0$ and magnetic field $B \in \mathbb R$ is

$$\mu(\underline x) = \frac{1}{Z_n(\beta,B)} \exp\Big\{\beta \sum_{(i,j)\in E_n} x_i x_j + B \sum_{i \in V_n} x_i\Big\}, \qquad x_i \in \{+1,-1\},$$

each edge counted once, and the free entropy density is $\phi_n(\beta,B) = \frac1n \log Z_n(\beta,B)$.

A degree distribution is a law $P = \{P_k\}$ on $\{0,1,2,\dots\}$ with $0 < \bar P = \sum_k k P_k < \infty$; its size-biased version is $\rho_k = k P_k/\bar P$, and $\bar\rho = \sum_k (k-1)\rho_k$. The Galton–Watson tree $T(P,\rho,\infty)$ has a root with $k$ children with probability $P_k$, and every other vertex independently has $k-1$ children with probability $\rho_k$; $T(P,\rho,t)$ is its first $t$ generations.

The ball $B_i(t)$ is the subgraph induced by the vertices within distance $t$ of $i$, rooted at $i$. The sequence converges locally to $T(P,\rho,\infty)$ if, for every $t$ and every rooted tree $T$, the fraction of vertices $i$ with $B_i(t) \simeq T$ (root-preserving isomorphism) tends to $\mathbb P\{T(P,\rho,t) \simeq T\}$. It is uniformly sparse if $\lim_{l\to\infty}\limsup_n \frac1n\sum_i |\partial i|\,\mathbb I(|\partial i| \ge l) = 0$.

The cavity recursion acts on laws of a real random variable $h$:

$$h \overset{d}{=} B + \sum_{i=1}^{K-1} \xi(\beta, h_i), \qquad \xi(\beta,h) = \operatorname{atanh}[\tanh\beta \tanh h],$$

with $K \sim \rho$ and $h_i$ i.i.d. copies of $h$ independent of $K$. For $B > 0$ it has a unique fixed point $h^*$ supported on $[0,\infty)$. The Bethe functional of a law of $h$ is

$$\varphi_h(\beta,B) = \frac{\bar P}{2}\log\cosh\beta - \frac{\bar P}{2}\mathbb E\log[1+\tanh\beta\tanh h_1\tanh h_2] + \mathbb E\log\Big\{e^B\prod_{i=1}^L[1+\tanh\beta\tanh h_i] + e^{-B}\prod_{i=1}^L[1-\tanh\beta\tanh h_i]\Big\},$$

with $L \sim P$ independent of the $h_i$.

Formalization targets

Goal: Theorem 2.4

Assume $\{G_n\}$ is uniformly sparse, converges locally to $T(P,\rho,\infty)$, and $\sum_k k\rho_k < \infty$. Then for every $\beta \ge 0$:

$$\lim_{n\to\infty}\phi_n(\beta,B) = \varphi_{h^*}(\beta,|B|) \quad (B \ne 0),$$

and $\varphi_{h^*}(\beta,B)$ has a limit $L_0$ as $B \downarrow 0$, with $\phi_n(\beta,0) \to L_0$. This is the paper's statement that the limit exists for every $B$, equals (2.9) for $B > 0$, is even in $B$, and is continuous at $B = 0$.

Milestones

1. Tools on Ising models: Griffiths' inequality (Theorem 3.1), the GHS inequality (Theorem 3.2), the subtree-marginal identity (Lemma 4.1).
2. Trees: the boundary effect on the root magnetization, $\mathbb E\{m^{\ell,+}-m^{\ell,0}\} \le M/\ell$ (Lemma 4.3); the correlation factorization (Lemma 4.4); exponential decay of root-to-generation correlations (Corollary 4.5, (4.13)).
3. The recursion: monotone convergence to the unique nonnegative fixed point (Lemma 2.3) and its Lipschitz dependence on $\beta$ in Monge–Kantorovich distance (Lemma 4.6).
4. The Bethe functional: the second-order perturbation bound (Lemma 6.1, Remark 6.2) and its consequence, stationarity of $\varphi_h$ at fixed points (Corollary 6.3, with corrected constant).
5. From trees to graphs: edge averages converge to averages over the edge-rooted tree $\bar T(\rho,t)$ (Lemma 6.4), and $\partial_\beta\phi_n = \frac1n\sum_{(i,j)\in E_n}\langle x_ix_j\rangle_n$ (6.10).

Significance

The result. Theorem 2.4 establishes the replica-symmetric (Bethe) formula for the ferromagnetic Ising model on the standard sparse random graph ensembles at all temperatures, including below the critical temperature $\tanh\beta_c = 1/\bar\rho$ where the Gibbs measure on the limiting tree is not unique. It identifies the free energy of random regular graphs, Erdős–Rényi graphs and configuration models with arbitrary degree distributions of finite variance, and the derivative identities that follow give the limiting magnetization and energy per edge. The tree estimates of Section 4 also yield the convergence of belief propagation (the companion mission of this series).

Formalizing it. The theorem is proved; nothing in this mission has been machine-checked before. A formal proof requires infrastructure that Lean's Mathlib does not have: Ising measures with boundary conditions, correlation inequalities, Galton–Watson trees as laws of offspring functions, local weak convergence of graph sequences, distributional fixed-point equations, and the Monge–Kantorovich distance on the real line. While stating the milestones, Corollary 6.3 turned out to be false as printed (the constant $\bar P\bar\rho$ should be $\mathbb E[L^2]$; a counterexample is $P = \delta_1$); the mission states the corrected version, which is what the paper's proof gives.

Difficulty

The obvious route through uniqueness of the Gibbs measure on the tree fails below the critical temperature: different boundary conditions give different limits, so local quantities are not determined by the local graph structure alone. The paper replaces uniqueness by insensitivity to positive boundary conditions when $B > 0$ (Lemma 4.3), which rests on Griffiths and GHS monotonicity and on averaging over the random tree; the deterministic statement is false. Passing from derivatives to the free entropy itself requires that the Bethe functional be stationary in the cavity law (Corollary 6.3), so that the $\beta$-dependence of $h^*$ can be ignored. Finally, the case $B = 0$ at low temperature is reached only as a limit: there is no fixed-point characterization at $B = 0$.

Formalization scope

• Spins are Booleans ($+1$ = true); edges are unordered and counted once. Graphs $G_n$ live on Fin n.
• A field $B_i = +\infty$ (plus boundary) is encoded by pinning vertex $i$ to $+1$, never by a large real field.
• Rooted trees are offspring functions List ℕ → ℕ in Ulam–Harris form; random trees are laws of offspring functions under the product σ-algebra. Galton–Watson trees are infinite product measures. Fields on trees are nonrandom functions of the vertex.
• Laws of cavity fields are probability measures on $\mathbb R$; the recursion is a map on ProbabilityMeasure ℝ, and convergence in distribution is weak convergence. Expectations over $L \sim P$ are series $\sum_l P_l\,\mathbb E[\cdot]$ with product laws.
• The Monge–Kantorovich distance takes values in $[0,\infty]$. Uniform sparsity is computed in $[0,\infty]$ so that an unbounded sequence does not get a junk $\limsup$ of $0$.
• The fixed point $h^*$ in the goal is the one supported on $[0,\infty)$, selected by choice; Lemma 2.3 shows it exists and is unique, so an arbitrary fixed point cannot be substituted. Theorem 2.4 is stated with $\beta \ge 0$ and asserts convergence for $B > 0$, $B < 0$ and $B = 0$ separately; the $B = 0$ clause asserts the existence of the one-sided limit rather than assuming it.

A complete development needs: Griffiths and GHS inequalities for finite Ising models (reusable for any ferromagnetic model); Ulam–Harris random trees with conditional independence; local weak convergence of graph sequences (reusable for random graph theory); distributional recursions with stochastic ordering; and the coupling characterization of the Wasserstein-1 distance on $\mathbb R$. Contributions of any milestone are welcome, as are proofs of the classical inequalities of Section 3 independent of this paper.

Selected references

• A. Dembo, A. Montanari, Ising models on locally tree-like graphs, Ann. Appl. Probab. 20(2) (2010) 565–592. https://arxiv.org/abs/0804.4726v3 , https://doi.org/10.1214/09-AAP627
• M. Mézard, G. Parisi, The Bethe lattice spin glass revisited, Eur. Phys. J. B 20 (2001) 217–233. https://doi.org/10.1007/PL00011099
• R. B. Griffiths, C. A. Hurst, S. Sherman, Concavity of magnetization of an Ising ferromagnet in a positive external field, J. Math. Phys. 11 (1970) 790–795. https://doi.org/10.1063/1.1665211
• T. M. Liggett, Interacting Particle Systems, Springer, 1985 (Theorem IV.1.21, Griffiths' inequality). https://doi.org/10.1007/978-1-4613-8542-4
• A. Dembo, A. Montanari, N. Sun, Factor models on locally tree-like graphs, Ann. Probab. 41(6) (2013) 4162–4213. https://doi.org/10.1214/12-AOP828

Motivation

A well-quasi-order is a reflexive, transitive relation in which every infinite sequence $x_1,x_2,\dots$ contains a pair $i<j$ with $x_i\le x_j$. Showing that a class of finite combinatorial objects is well-quasi-ordered by a containment relation is a standard way to prove that every property closed under that containment is characterised by finitely many forbidden objects. The best-known instance is the Graph Minor Theorem (Wagner's conjecture), completed by Robertson and Seymour in Graph Minors XX (JCTB 92, 2004).

Nash-Williams proposed the analogous conjecture for a different containment, immersion, in which edges of the smaller graph are mapped to edge-disjoint paths of the larger graph. Graph Minors XXIII (JCTB 100, 2010) proves it by deriving a general well-quasi-ordering theorem for labelled hypergraphs from the machinery of Graph Minors XX.

Timeline.

• 1963 (published 1964): Nash-Williams conjectures that finite graphs are well-quasi-ordered by immersion ([Theory of Graphs and Its Applications, Smolenice 1963, pp. 83–84]).
• 1965: Nash-Williams proposes a second, "strong" immersion conjecture, in which the image paths may not pass through images of non-incident vertices (Proc. Cambridge Philos. Soc. 61).
• 2004: Graph Minors XX proves Wagner's conjecture: finite graphs are well-quasi-ordered by minors.
• 2010: Graph Minors XXIII proves the (weak) immersion conjecture together with a labelled hypergraph generalisation. The paper states that it does not prove the strong conjecture.

Setting

All graphs and hypergraphs are finite. A graph $G$ has a vertex set $V(G)$, an edge set $E(G)$, and for each edge an unordered pair of ends; an edge with equal ends is a loop, and several edges may have the same ends (parallel edges). A graph is loopless if no edge is a loop. A path has at least one vertex and no repeated vertices; a circuit has at least one edge and no repeated vertices, so a loop and a pair of parallel edges are circuits.

An immersion of $H$ in $G$ is a map $\alpha$ on $V(H)\cup E(H)$ such that $\alpha$ is injective on vertices; every non-loop edge $e$ with ends $u,v$ goes to a path $\alpha(e)$ of $G$ with ends $\alpha(u),\alpha(v)$; every loop at $v$ goes to a circuit $\alpha(e)$ of $G$ through $\alpha(v)$; and $\alpha(e)$, $\alpha(f)$ share no edge when $e\ne f$.

A hypergraph $G$ has finite sets $V(G)$, $E(G)$ and an incidence relation; $V(e)$ is the set of ends of the edge $e$, of any size. Write $K_V$ for the complete graph on $V$. A collapse of $G$ to $H$ maps each vertex $v$ of $H$ to a non-null connected subgraph $\eta(v)$ of $K_{V(G)}$, pairwise vertex-disjoint, and each edge $e$ of $H$ injectively to an edge $\eta(e)$ of $G$, so that $\eta(e)$ meets $\eta(v)$ whenever $e$ is incident with $v$, and every edge $xy$ of every $\eta(v)$ is covered by some edge of $G$ incident with both $x$ and $y$. The transpose of a graph $G$ is the hypergraph with vertex set $E(G)$, edge set $V(G)$ and the same incidence.

A quasi-order $\Omega$ is an ideal of $\Omega'$ if it is a sub-quasi-order closed downwards in $\Omega'$; a shadow is a tuple $(\Omega_\infty,m,\Omega_m,\dots,\Omega_1,R_2,R_1)$ of well-quasi-orders and finite sets, ordered lexicographically (Section 3 of the paper).

Formalization targets

Goal: Nash-Williams' immersion conjecture (1.1)

$$\forall\,(G_i)_{i\ge1}\text{ finite graphs}:\quad \exists\, j>i\ge1,\ \ G_i \text{ is immersed in } G_j .$$

Milestones, in the order the proof uses them

• 3.1 No sequence $\Omega_1,\Omega_2,\dots$ with $\Omega_1$ a well-quasi-order and $\Omega_{i+1}$ a proper ideal of $\Omega_i$ for all $i$.
• 3.2 No sequence of shadows with $\Sigma_{i+1}<\Sigma_i$ for all $i$.
• 1.6 For a well-quasi-order $\Omega$ and hypergraphs $G_i$ with edge labels $\phi_i$, distinguished edges $M_i$ of at most $k$ ends and orderings $\mu_i(e)$ of their ends, some $j>i$ admit a collapse $\eta$ of $G_j$ to $G_i$ with $\phi_i(e)\le\phi_j(\eta(e))$, $\eta(e)\in M_j\iff e\in M_i$, and preserving the orderings.
• 1.4 The same with $M_i=\emptyset$: $\phi_i(e)\le\phi_j(\eta(e))$ for all edges.
• 1.2 For every sequence of hypergraphs there is a collapse of some $G_j$ to some earlier $G_i$.
• 1.3 For loopless graphs $G,H$, a collapse of the transpose of $G$ to the transpose of $H$ yields an immersion of $H$ in $G$.
• 1.5 Vertex-labelled loopless graphs: an immersion $\alpha$ of $G_i$ in $G_j$ with $\phi_i(v)\le\phi_j(\alpha(v))$.
• 1.7 (off the goal's path) A labelled form of Wagner's conjecture for directed graphs with loops.

Significance

The immersion theorem implies that every class of finite graphs closed under taking immersions is characterised by finitely many excluded immersions. Theorem 1.6 is stronger than both 1.1 and Wagner's conjecture: it handles hypergraphs, labels from an arbitrary well-quasi-order and ordered edges, which is the form in which the Graph Minors machinery is reused by later work.

All results here are proved in the paper. None of them has a machine-checked proof: Mathlib has well-quasi-orders and Higman's lemma, but not the Graph Minor Theorem or any notion of graph immersion. The value of this mission is a faithful formal statement of the immersion theorem and of the reductions the paper performs in Section 1 (1.3 and the passage from 1.6 to 1.4, 1.5 and 1.1), each of which can be formalized independently of Graph Minors XX, plus the order-theoretic lemmas 3.1 and 3.2.

Difficulty

The reductions in Section 1 (1.3, and the passages from 1.6 to 1.4, 1.5 and 1.1) are short on paper but require a working library of multigraph walks, paths and circuits, which Mathlib does not have for graphs with loops and parallel edges. The real difficulty is 1.6, which the paper derives from a theorem on patchworks of Graph Minors XX (its 2.2) together with tangle results of Graph Minors X, and therefore rests on the structure theory of the whole Graph Minors series. No route around that theory is known: when the hypergraphs are loopless graphs, a collapse of $G_j$ to $G_i$ makes $G_i$ a minor of $G_j$, so already 1.2 contains Wagner's conjecture. Nor does 1.2 alone give 1.1: loops cannot be routed through the transpose construction of 1.3, and the paper handles them by counting loops at each vertex as a label from the well-quasi-order $\mathbb N$, which is why the labelled forms 1.4–1.6 are needed.

Formalization scope

A graph is Graph V E with ends : E → Sym2 V; a hypergraph is Hypergraph V E with inc : E → V → Prop; each lives on its own finite types, and a sequence is a family indexed by ℕ (from $0$; the paper's $j>i\ge1$ becomes $i<j$). Paths and circuits are walks with vertex and edge lists; the ends of a path are unordered. An immersion is the structure GraphImmersion H G; a collapse of $G$ to $H$ is Collapse G H, whose branch sets are Subgraphs of ⊤ : SimpleGraph V(G) (Mathlib's Subgraph.Connected includes non-emptiness). Well-quasi-orders are Mathlib's WellQuasiOrdered on a type with a preorder for 1.4–1.7, and QO.IsWQO on subsets of an ambient type for 3.1–3.2, where quasi-orders are compared by inclusion. Directed graphs for 1.7 are DirGraph V E with heads and tails.

Three trivializing formalizations are excluded: the collapse keeps condition (iv), so branch sets cannot use arbitrary pairs of vertices; immersion paths are edge-disjoint, not vertex-disjoint (which would give topological minors, not a well-quasi-order); and each graph lives on its own type, never all on one fixed finite type, which would make the goal a pigeonhole statement. Strong immersion is not stated.

Contributions welcome: proofs of 3.1, 3.2 and 1.3, the reductions 1.6 ⇒ 1.4 ⇒ 1.2 and 1.4 + 1.3 ⇒ 1.5 ⇒ 1.1, and library material on multigraph walks, paths and circuits, which is reusable beyond this mission. A proof of 1.6 would require formalizing the Graph Minors series.

Selected references

• N. Robertson, P. Seymour, Graph Minors XXIII. Nash-Williams' immersion conjecture, J. Combin. Theory Ser. B 100 (2010) 181–205 (authors' manuscript rev. April 18, 2011, used here). https://doi.org/10.1016/j.jctb.2009.07.003
• N. Robertson, P. Seymour, Graph Minors XX. Wagner's conjecture, J. Combin. Theory Ser. B 92 (2004) 325–357. https://doi.org/10.1016/j.jctb.2004.08.001
• C. St. J. A. Nash-Williams, On well-quasi-ordering infinite trees, Proc. Cambridge Philos. Soc. 61 (1965) 697–720. https://doi.org/10.1017/S0305004100039062

Motivation

Network design problems often ask for a cheap spanning tree in which no vertex is overloaded: in multicast and overlay networks the degree of a node bounds the number of copies it must forward, and in physical networks it bounds the number of ports. The minimum bounded degree spanning tree problem asks for a minimum-cost spanning tree whose degrees respect given bounds. Deciding whether a graph has a spanning tree of maximum degree 2 is already the Hamiltonian path problem, so exact solutions are out of reach, and the question becomes how little the bounds and the cost must be relaxed.

Some problems also impose lower bounds: a vertex that must serve as a hub, or a leaf-avoidance requirement, asks for degree at least $A_v$. Singh and Lau (STOC 2007) showed that the iterative rounding method they used for upper bounds extends to both kinds at once: a spanning tree of cost at most the LP optimum whose degree at every vertex lies in $[A_v-1,\,B_v+1]$.

Timeline. Fürer and Raghavachari (1994) found a spanning tree of maximum degree at most $\Delta^*+1$ in the unweighted case. For costs, Goemans (FOCS 2006) obtained cost at most OPT with degrees at most $B_v+2$. Singh and Lau (STOC 2007) improved this to $B_v+1$, which is the best possible additive violation unless P = NP, and gave the extension to lower and upper bounds formalized here. The journal version appeared in J. ACM 62(1), 2015.

Setting

Let $G=(V,E)$ be a finite simple graph with edge costs $c_e\in\mathbb R$; no sign or triangle inequality is assumed. Let $F$ be a forest on $V$ with no edge in common with $E$. A set $H\subseteq E$ is an $F$-tree if $H\cup F$ is a spanning tree of $V$, and $d_H(v)$ is the number of edges of $H$ at $v$. Integer lower bounds $A_v$ are given on $U\subseteq V$ and integer upper bounds $B_v$ on $W\subseteq V$. The minimum bounded degree connecting tree problem asks for a cheapest $F$-tree with $A_v\le d_H(v)$ on $U$ and $d_H(v)\le B_v$ on $W$; with $F=\varnothing$ it is the spanning-tree problem.

The supernodes are the vertex sets of the components of $(V,F)$, isolated vertices included, and $\mathcal I(F)$ is the family of unions of supernodes. For $S\subseteq V$, $E(S)$ and $F(S)$ are the edges with both endpoints in $S$, $\delta(S)$ the edges with exactly one endpoint in $S$, and $x(D)=\sum_{e\in D}x_e$. The linear relaxation LP-MBDCT$(G,\mathcal A,\mathcal B,U,W,F)$ minimizes $\sum_e c_ex_e$ subject to

$$x(E(V))=|V|-|F(V)|-1,\quad x(E(S))\le|S|-|F(S)|-1\ (S\in\mathcal I(F)),\quad A_v\le x(\delta(v))\ (v\in U),\quad x(\delta(v))\le B_v\ (v\in W),\quad x\ge0.$$

MBDCT Algorithm2 (Figure 5 of the paper) repeats: if $F$ is a spanning tree, stop; otherwise take a basic optimal solution $x^*$, delete the edges with $x^*_e=0$, move one edge with $x^*_e=1$ (if any) into $F$ and lower $A$ and $B$ by one at its endpoints, and otherwise remove from $U$ and $W$ one vertex whose support degree is at most two.

Formalization targets

Goal: Theorem 5.2

For every well-formed instance whose LP is feasible, MBDCT Algorithm2

1. has a terminating run;
2. makes at most $|V|-|F|-1+|U\cup W|$ iterations on every run;
3. returns only $F$-trees $H\subseteq E$ with

$$c(H)\le\sum_{e\in E}c_ex_e\ \text{for every feasible }x,\qquad A_v-1\le d_H(v)\ (v\in U),\qquad d_H(v)\le B_v+1\ (v\in W).$$

The statement fixes no constants beyond the paper's $\pm1$, and it is uniform over every choice of basic optimal solution, 1-edge and removed vertex.

Milestones

In the order the proof uses them: Lemma 5.3 (a basic solution is determined by a laminar family of tight sets and tight lower and upper degree rows, with $|E^*|=|\mathcal L|+|T_U|+|T_W|$); Claims 5.4, 5.7, 5.8 and 5.9 (special supernodes, cut sizes, the value $x^*(D(S))=r-1$ on the edges between the $r$ members of $S$, and when a set is special); Lemma 5.6 (every set of $\mathcal L$ keeps at least three tokens, exactly three only if it is special or $V$); and Lemma 5.1 (a basic solution has an edge with $x^*_e=1$ or a vertex of $U\cup W$ with support degree two).

Significance

The theorem gives, in one algorithm, a tree that is no more expensive than the LP lower bound and whose degrees miss both bounds by at most one. For the pure upper-bound problem it implies the $(1,B_v+1)$ guarantee, which cannot be improved to $B_v$ unless P = NP, since a Hamiltonian path is the case $B_v\equiv 2$. With lower bounds it also covers prescribed minimum degrees.

The result is proved in the paper; no machine-checked proof of it, or of any iterative rounding analysis, is known to exist. No platform item treats bounded-degree spanning trees or iterative rounding; the nearest related item is the open Williamson–Shmoys minimum-degree spanning tree local-search goal, which concerns a different, unweighted problem. Formalizing this mission requires the extreme-point structure of the spanning tree polytope with degree constraints (uncrossing to a laminar family), the token counting argument, and the induction over the algorithm's recursion, all of which are reusable for other iterative rounding results.

Difficulty

The obvious argument rounds an optimal LP solution once. It fails: an optimal vertex may be entirely fractional, and no single rounding keeps both the cost and the degrees. The algorithm instead re-solves the LP after each change, and its correctness rests on Lemma 5.1, that every extreme point of the current LP has an integral edge or a vertex with support degree two. That lemma is a counting statement about extreme points: the rank bound $|E^*|=|\mathcal L|+|T_U|+|T_W|$ from a laminar basis must be contradicted by a token distribution. With upper bounds only, every set of the laminar family can collect four tokens. With lower bounds a set may collect only three, and the proof must characterize those sets (special sets, Definition 5.5) and show by linear independence that the remaining cases cannot occur. A second difficulty is that the guarantee concerns the final tree after many iterations, so the degree accounting must survive the changes of $A$, $B$, $U$, $W$ and $F$ along the run.

Formalization scope

Vertices form a Fintype; edges are elements of Sym2 V with no loops, and $E$, $F$ are finite sets of edges with $F$ acyclic and disjoint from $E$. LP vectors are functions on Sym2 V that vanish off $E$. Right-hand sides are computed in $\mathbb R$, degree bounds are integers, and the subtour rows range over nonempty $S\in\mathcal I(F)$ (at $S=\varnothing$ the literal row $0\le-1$ would make the LP empty). A basic solution is a feasible $x$ that is the only vector on $E$ satisfying with equality every constraint tight at $x$, including the tight rows $x_e=0$. Supernodes are never contracted: the paper's contraction of a supernode with one active vertex is a proof device, and all of §5.1's notions are stated on the original instance.

The paper's loose phrases are made explicit as follows.

• "Polynomial time" becomes the iteration bound; the LP is solved by an oracle that returns any basic optimal solution. The ellipsoid method and the separation oracle are out of scope.
• "The algorithm returns" becomes three claims: a run exists, every run is bounded, and every returned set satisfies the guarantee. The guarantee alone would hold vacuously for a relation that can get stuck.
• "Cost at most the cost of the optimal LP solution" becomes $c(H)\le c\cdot x$ for every feasible $x$.
• "Distribute the tokens" (Lemma 5.6) becomes a counting inequality on the surplus of tokens.
• Claim 5.9's "contains exactly three special members" means that $S$ has exactly three members, all of them special.
• Figure 5's Step 4 is guarded by "no edge was picked in Step 3", as the paper's text under Lemma 5.1 states.
• "$F$ is not a spanning tree" and LP feasibility are explicit hypotheses where the paper leaves them implicit.

Two trivializations are ruled out. Existence of a cheap tree with degrees in $[A_v-1,B_v+1]$ is not the target: the statement is about the algorithm's outputs and quantifies over all of them. And a run that never terminates does not satisfy the goal, which requires a run to exist and every run to be bounded.

Contributions are welcome at every level: the laminar uncrossing argument (Lemma 5.3), which is reusable for any spanning-tree LP with degree rows; the counting claims; and the invariants of the recursion.

Selected references

• M. Singh, L. C. Lau, Approximating minimum bounded degree spanning trees to within one of optimal, STOC 2007, pp. 661–670. https://doi.org/10.1145/1250790.1250887
• M. Singh, L. C. Lau, Approximating minimum bounded degree spanning trees to within one of optimal, J. ACM 62(1), 2015. https://doi.org/10.1145/2629366
• M. X. Goemans, Minimum bounded degree spanning trees, FOCS 2006, pp. 273–282. https://doi.org/10.1109/FOCS.2006.48
• M. Fürer, B. Raghavachari, Approximating the minimum-degree Steiner tree to within one of optimal, J. Algorithms 17(3), 1994, pp. 409–423. https://doi.org/10.1006/jagm.1994.1042