Graph Theory

Motivation

Many models in economics, biology and computer science are finite Markov chains that have several absorbing states or recurrent classes, so their long-run behaviour depends on where they start. Adding a small amount of noise (mistakes, mutations, experimentation) makes the chain irreducible, and the noisy chain then has a unique stationary distribution. As the noise vanishes, that distribution concentrates on some of the original recurrent classes. The stochastically stable states are the ones that keep positive weight in the limit; they are the states the system spends nearly all its time in when the noise is small but nonzero.

H. Peyton Young's The Evolution of Conventions (Econometrica, 1993) proved a general finite-state characterization of these states, which he used to select among the equilibria of coordination games under adaptive play. The characterization rests on the theory of small random perturbations of Freidlin and Wentzell (1984), developed for diffusions, and on a combinatorial lemma of theirs expressing stationary distributions through spanning trees. Kandori, Mailath and Rob (1993) characterized the limit distribution by spanning trees on the whole state space for their model of learning with mutations; Young's Lemma 1 generalizes their Theorem 1 (p. 78), and his Lemma 2 reduces the computation to the much smaller graph of recurrent classes. Foster and Young (1990) introduced stochastic stability for evolutionary dynamics, and the equilibria it selects in $2\times 2$ games coincide with the risk-dominant equilibria of Harsanyi and Selten (1988).

Setting

Let $X$ be a finite set and $P^0$ the transition matrix of a Markov chain on $X$. A state $y$ is reachable from $x$ if $(P^0)^n_{xy} > 0$ for some $n \ge 0$; $x$ is recurrent if every state reachable from $x$ can reach $x$ back; the recurrent communication classes $X_1, \dots, X_J$ are the communication classes of recurrent states.

A family $(P^\varepsilon)_{\varepsilon \in (0,a]}$ of Markov chains on $X$ is a regular perturbation of $P^0$ if for all $x, y$:

• (6) $P^\varepsilon$ is aperiodic and irreducible for every $\varepsilon \in (0,a]$;
• (7) $P^\varepsilon_{xy} \to P^0_{xy}$ as $\varepsilon \to 0$;
• (8) if $P^\varepsilon_{xy} > 0$ for some $\varepsilon$, there is $r \ge 0$ with $0 < \lim_{\varepsilon \to 0} \varepsilon^{-r} P^\varepsilon_{xy} < \infty$.

The exponent $r = r(x,y)$ is the resistance of the transition $x \to y$. The graph $G$ has vertex set $X$ and an edge $(x,y)$ when $P^\varepsilon_{xy} > 0$ for all small $\varepsilon$, weighted by $r(x,y)$.

For $z \in X$, a $z$-tree is a spanning tree of edges of $G$ in which every $x \ne z$ has a unique directed path to $z$. The potential of $z$ is

$$\gamma(z) = \min_{T \in \mathcal T_z} \sum_{(x,y) \in T} r(x,y). \tag{9}$$

For classes $i \ne j$, $r_{ij}$ is the least resistance of a path in $G$ from $X_i$ to $X_j$. On the complete directed graph $\mathcal G$ with vertices $1, \dots, J$ and edge weights $r_{ij}$, the stochastic potential $\gamma_j$ of $X_j$ is the least total weight of a $j$-tree in $\mathcal G$.

Formalization targets

Goal: Theorem 4 (p. 78)

If $\mu^\varepsilon$ is the stationary distribution of $P^\varepsilon$ for $\varepsilon \in (0,a]$, then $\mu^\varepsilon \to \mu^0$ as $\varepsilon \to 0$, where $\mu^0$ is a stationary distribution of $P^0$, and

$$\mu^0_x > 0 \iff x \in X_j \text{ for some } j \text{ with } \gamma_j = \min_i \gamma_i .$$

Milestones, in the order of the paper's proof

1. Resistance (p. 77). The exponent in (8) is unique; a transition positive for some $\varepsilon$ is an edge of $G$; and the edges of zero resistance are exactly the transitions with $P^0_{xy} > 0$.
2. Markov chain tree formula (p. 79). For an aperiodic irreducible chain $P'$, $\mu'_z = p'_z / \sum_x p'_x$ with $p'_z = \sum_{T \in \mathcal T_z} \prod_{(x,y)\in T} P'_{xy}$ is the unique stationary distribution.
3. Lemma 1 (p. 78). $\mu^\varepsilon \to \mu^0$, $\mu^0$ is stationary for $P^0$, and $\mu^0_x > 0$ iff $\gamma(x) \le \gamma(y)$ for all $y$.
4. (p. 80) A stationary distribution of a finite chain vanishes on non-recurrent states.
5. (p. 80) All states of a recurrent class of $P^0$ have the same potential.
6. Lemma 2 (p. 80). $\gamma(x) = \gamma_j$ for every $x \in X_j$.

Significance

Theorem 4 turns a limit of stationary distributions into a finite optimization: compute least-resistance paths between the recurrent classes, then a minimum-weight arborescence on the reduced graph. The answer depends only on the orders of magnitude of the perturbations, not on their exact values, which is what makes the result usable when the noise model is known only qualitatively. It underlies the equilibrium-selection results of the same paper (risk dominance in $2\times 2$ coordination games, Theorem 3) and much of the later stochastic evolutionary game theory literature.

The result is proved in the paper, with the tree formula imported from Freidlin and Wentzell. As far as is known, none of it is formalized: Mathlib has irreducible and primitive nonnegative matrices but neither the Markov chain tree formula, aperiodicity, recurrent classes of a finite chain, nor minimum arborescences. A complete development would produce these as reusable components.

Difficulty

The first idea is to take the limit in $\mu^\varepsilon P^\varepsilon = \mu^\varepsilon$: compactness and (7) give that every limit point of $\mu^\varepsilon$ is stationary for $P^0$, but $P^0$ has many stationary distributions, so this neither proves convergence nor identifies the support. Both come from the tree formula, which makes $\mu^\varepsilon_z$ a ratio of sums of products whose orders of magnitude are read off from the resistances; the absence of cancellation (all terms are nonnegative) is essential. The second difficulty is Lemma 2: an optimal $x$-tree on the whole state space must be transformed, by the paper's tree surgery on junctions (pp. 80–83), into something comparable with a $j$-tree on the class graph without increasing its resistance. The easy inequality $\gamma(x_j) \le \gamma_j$ glues optimal paths and zero-resistance trees together; the reverse inequality is where the work lies.

Formalization scope

States form a Fintype X with decidable equality; chains are real matrices Matrix X X ℝ, row stochasticity is Matrix.rowStochastic, irreducibility is Mathlib's Matrix.IsIrreducible, and aperiodicity (every state has period 1) is defined in the mission. The family $P^\varepsilon$ is a function ℝ → Matrix X X ℝ constrained only on $(0, a]$; all limits are one-sided ($\varepsilon \to 0^+$), $\varepsilon^{-r}$ is the real power, and "$0 < \lim < \infty$" is a real limit $c > 0$. Distributions are row vectors and stationarity is $\mu A = \mu$. Trees are parent maps with edges pointing toward the root. Potentials, class resistances and stochastic potentials are infima in EReal, where an empty infimum is $+\infty$; under the hypotheses all of them are finite.

The goal quantifies over every regular perturbation, not a parametric family such as $(1-\varepsilon)P^0 + \varepsilon Q$, and over every family of stationary distributions of the $P^\varepsilon$ (unique by (6)). The recurrent classes are computed from $P^0$, not supplied as data, and $\gamma_j$ is computed on the class graph with weights $r_{ij}$; defining $\gamma_j$ as $\gamma(x)$ for some $x \in X_j$ would make Lemma 2 definitional and is ruled out.

Contributions welcome: the Markov chain tree formula and the uniqueness of stationary distributions for irreducible finite chains (both reusable well beyond this mission), recurrence and the support of stationary distributions, and the arborescence surgery of Lemma 2.

Selected references

• H. P. Young, The Evolution of Conventions, Econometrica 61(1), 1993, 57–84. https://doi.org/10.2307/2951778
• M. I. Freidlin and A. D. Wentzell, Random Perturbations of Dynamical Systems, Springer, 1984 (Ch. 6, Lemma 3.1). https://doi.org/10.1007/978-1-4684-0176-9
• M. Kandori, G. J. Mailath and R. Rob, Learning, Mutation, and Long Run Equilibria in Games, Econometrica 61(1), 1993, 29–56. https://doi.org/10.2307/2951777
• D. P. Foster and H. P. Young, Stochastic Evolutionary Game Dynamics, Theoretical Population Biology 38, 1990, 219–232. https://doi.org/10.1016/0040-5809(90)90011-J
• J. C. Harsanyi and R. Selten, A General Theory of Equilibrium Selection in Games, MIT Press, 1988. https://mitpress.mit.edu/9780262582384/
• Related missions on learning dynamics: StochFictPlay.* (Hofbauer and Sandholm 2002, stochastic fictitious play) and CalibratedCE.* (calibrated learning and correlated equilibrium).

Why edge-disjoint spanning trees

A connected network survives the failure of any single link exactly when it has no bridge, but a stronger and more useful property is to carry several edge-disjoint spanning trees: each tree can broadcast to every node on its own, so $k$ such trees give $k$ independent routing or broadcast structures, and the network stays connected after any $k-1$ link failures. The question of when a graph contains $k$ edge-disjoint spanning trees was answered in 1961, simultaneously and independently, by W. T. Tutte (On the problem of decomposing a graph into n connected factors) and C. St.J. A. Nash-Williams (Edge-disjoint spanning trees of finite graphs). The answer is a min-max condition over vertex partitions, now called the Tutte–Nash-Williams tree-packing theorem. It is a standard result in combinatorial optimization and the graphic case of Edmonds's matroid base-packing theorem (1965).

Timeline:

• 1961. Tutte proves the theorem in an equivalent form; Nash-Williams, unaware of Tutte's work, gives a different proof a few months later, the one formalized here.
• 1964. Nash-Williams proves the companion covering theorem: the edges can be covered by $k$ forests iff every vertex set $U$ spans at most $k(|U|-1)$ edges.
• 1965. Edmonds derives both results from matroid partition (Minimum partition of a matroid into independent subsets).

Setting

A graph $G$ here is a finite unoriented multigraph in which every edge joins two distinct vertices; two vertices may be joined by several edges. Write $V$ for its vertex set and $E$ for its edge set. A tree on a non-empty vertex set $W$ is an edge set $T$, all of whose edges have both ends in $W$, containing no cycle (two parallel edges count as a cycle), such that any two vertices of $W$ are joined by a path of $T$-edges. A spanning tree of $G$ is a tree on all of $V$ using edges of $G$. Spanning trees are edge-disjoint if no two share an edge.

A partition $P$ of $V$ is a set of non-empty, pairwise disjoint subsets of $V$ whose union is $V$; $|P|$ is the number of its members. The crossing edges $E_P(G)$ are the edges whose two ends lie in different members of $P$, counted with multiplicity. Throughout, $k$ is a fixed positive integer. For $X \subseteq V$, $E_X$ is the set of edges with both ends in $X$, $e_X = |E_X|$, and

$$\Delta_G(X) = k(|X|-1) - e_X .$$

Formalization targets

Goal: Theorem 1

$$G \text{ has } k \text{ edge-disjoint spanning trees} \iff |E_P(G)| \ge k(|P|-1) \text{ for every partition } P \text{ of } V. \tag{1}$$

Milestones, in the order of the proof

1. Lemma 1: a tree on $W$ has $|W|-1$ edges. Lemma 2: every connected graph has a spanning tree.
2. Necessity: $k$ edge-disjoint spanning trees imply (1) for every $P$.
3. (*) On couples $[G,g]$ ($g \ge 0$ on vertices, $\Delta_G \ge 0$ on non-empty sets): critical sets ($\Delta_G = 0$) whose intersection is non-empty are closed under $\cap$ and $\cup$. The same holds for crucial sets ($\Gamma = 0$, where $\Gamma(X) = \Delta_G(X) - s + g\,.\,\bar X$) when the couple is $s$-good.
4. Lemma 3: for $s \ge 1$, an $s$-good couple has an $(s-1)$-good supercouple with one added edge. Corollary 3A: an $s$-good couple has an $s$-supercouple, obtained by adding $s$ edges.
5. (†) and Lemma 4: a spanning tree of a graph produced by fusions at $\xi$ (replacing edges $\xi\eta$, $\xi\zeta$ by a new edge $\eta\zeta$) pulls back to a spanning tree of the original graph.
6. Lemma 5: a graph with $|E| = k(|V|-1)$ satisfies (1) iff $\Delta_G(X) \ge 0$ for every non-empty $X$.
7. Lemma 6: under the inductive hypothesis of the proof, a critical partition other than $\{V\}$ and the partition into singletons yields $k$ edge-disjoint spanning trees.

Significance

The theorem gives an exact, checkable certificate in both directions: a family of $k$ trees certifies the packing, and a single partition violating (1) certifies that no packing exists. Corollaries include that every $2k$-edge-connected graph has $k$ edge-disjoint spanning trees, and that the maximum number of edge-disjoint spanning trees (the strength-type parameter used in network reliability and in Nagamochi–Ibaraki style connectivity algorithms) is the minimum of $\lfloor |E_P(G)|/(|P|-1) \rfloor$ over partitions with $|P| \ge 2$. The partition condition is also the prototype of the rank condition in matroid base packing.

The result itself is classical and fully proved. What this mission adds is a machine-checked version in a multigraph setting. Mathlib has trees and spanning trees for simple graphs (SimpleGraph.IsTree, SimpleGraph.Connected.exists_isTree_le), but not edge-disjoint tree packing, and its simple graphs cannot express the parallel edges that the theorem and its proof need. Related items on the platform include the multigraph layer NagamochiIbaraki.EdgeConn.Multigraph (reused here), the Keller–Trotter spanning-forest count for simple graphs, and Edmonds's matroid partition theorem with Nash-Williams's covering corollary. Covering and packing are different statements, so none of these yields Theorem 1 directly. Formalizing Tutte's alternative proof, or deriving Theorem 1 from a formalized matroid union theorem, would also be welcome.

Difficulty

Necessity is a counting argument. The difficulty lies in sufficiency. The obvious induction deletes an edge or contracts a set of vertices, but deleting an edge can destroy (1), and contracting changes the vertex set, so neither reduction preserves the hypothesis on its own. The hardest case is a graph in which only the partition into singletons is critical. There a vertex of degree less than $2k$ has to be removed while (1) is preserved on the remaining graph, and the trees found there have to be converted back into trees of the original graph. Both steps need careful bookkeeping of edges incident with that vertex. A simple-graph development cannot carry the argument, because the edges that the reduction adds among the neighbours of the removed vertex may be parallel to existing ones.

Formalization scope

• Graphs. A vertex type V, an edge type E (both finite, in Type), and ends : E → Sym2 V, the published encoding of NagamochiIbaraki.EdgeConn. Loops are excluded by the hypothesis ∀ e, ¬ (ends e).IsDiag. Parallel edges are allowed, and simplicity is never assumed. A subgraph is a pair (W : Finset V, F : Finset E).
• Trees. "Tree" means non-empty vertex set, edges inside it, no cycle (IsForest: every edge is a bridge) and connected. $|T| = |W|-1$ is Lemma 1, not part of the definition. "$k$ edge-disjoint spanning trees" is a family Fin k → Finset E of pairwise disjoint spanning trees.
• Partitions are Mathlib Finpartition (Finset.univ : Finset V). (1) is required for every partition, including the one-part partition and the singletons. All counts involving subtraction ($\Delta_G$, (1), criticality, $\Gamma$) are in $\mathbb Z$.
• Explicit readings. $V$ is non-empty in Theorem 1, since the paper's graphs have a vertex and on $V = \emptyset$ condition (1) holds while no tree exists. $k \ge 1$ in every statement. The paper's "$X \subset V(G)$" includes $X = V(G)$ and is read as $\subseteq$. "Exactly $g(\xi)-h(\xi)$ new edges" is written $\deg_{\text{new}}(\xi) + h(\xi) = g(\xi)$, without natural-number subtraction. A supergraph with $s$ added edges has edge type E ⊕ Fin s, so the added edges always exist; none of them may be a loop. A fusion uses a given fresh edge ρ : E in an ambient edge type, and a sequence of fusions is a list, each valid on the graph produced by the later ones ($L = \Phi_1\cdots\Phi_n G$ applies $\Phi_n$ first). In (†) and Lemma 4, "is a tree" means "is a spanning tree of $G$", since the vertex set is all of $V$. Lemma 6 carries the paper's inductive hypothesis as an explicit hypothesis: Theorem 1 (admissible implies $k$ trees) for all loopless multigraphs with smaller $|V|+|E|$.
• Ruled out. Defining a spanning tree by an edge count alone, or by acyclicity alone, would make Lemma 1 or the goal trivial; the definitions require both acyclicity and connectivity on the stated vertex set. Taking added edges from a fixed ambient type would make Lemma 3 false. Dropping or globalizing Lemma 6's inductive hypothesis would turn it into the goal or a tautology.
• Infrastructure. Multigraph trees, the tree edge count and spanning-tree existence, contraction $G_P$ of a partition, and splitting-off at a vertex. All of these are reusable beyond this mission. Contributions of general multigraph lemmas are welcome.

Selected references

• C. St.J. A. Nash-Williams, Edge-disjoint spanning trees of finite graphs, J. London Math. Soc. 36 (1961), 445–450. https://doi.org/10.1112/jlms/s1-36.1.445
• W. T. Tutte, On the problem of decomposing a graph into n connected factors, J. London Math. Soc. 36 (1961), 221–230. https://doi.org/10.1112/jlms/s1-36.1.221
• C. St.J. A. Nash-Williams, Decomposition of finite graphs into forests, J. London Math. Soc. 39 (1964), 12. https://doi.org/10.1112/jlms/s1-39.1.12
• J. Edmonds, Minimum partition of a matroid into independent subsets, J. Res. Nat. Bur. Standards 69B (1965), 67–72. https://doi.org/10.6028/jres.069B.004
• C. Berge, Théorie des graphes et ses applications, Dunod, Paris, 1958.

Why a grid has a tangle

Robertson and Seymour introduced tangles as a way to describe a region of a graph that cannot be isolated by a separation of low order. A separation divides the edges into two sides, and its order counts the vertices shared by those sides. A tangle makes a consistent choice of the side regarded as small at every order below a threshold. This turns an informal idea of a highly connected region into an object with explicit axioms. In Graph Minors. X, the authors connect tangles with branch-width, tree-width and grid minors; the grid construction is the direct example behind that connection. The paper states the existence of a tangle of order $\theta$ in every $\theta$-grid as (7.3) on p. 173. Robertson and Seymour, 1991.

The result is already proved in the paper. The present target is its Lean statement and proof, together with the two numbered results from §7 on which the construction rests. This mission concerns the grid itself. The paper's further assertion that a grid minor induces a tangle in a larger graph uses the separate minor-transfer result (6.1), whose edge identities require additional definitions. Robertson and Seymour, 1991, pp. 170–173.

The grid, its edge boundary and its small sets

Fix an integer $\theta\ge2$. The $\theta$-grid $G$ has vertices $(i,j)$ for $1\le i,j\le\theta$. Two vertices are adjacent exactly when their coordinate differences have absolute values summing to one. For each $i$, $P_i$ is the horizontal row with vertices $(i,1),\ldots,(i,\theta)$; for each $j$, $Q_j$ is the vertical column. Write $E(P_i)$ and $E(Q_j)$ for their edge sets. The Lean development uses the already published definition of this same simple graph, with coordinates shifted to start at zero. The shift changes no adjacency or row and column relation. Robertson and Seymour, 1991, p. 171.

For an edge set $X\subseteq E(G)$, the edge boundary $\partial(X)$ consists of vertices incident both with an edge in $X$ and with an edge outside $X$. The source prints “vertices $v\in X$” when introducing this set. Since $X$ is a set of edges, this is a type slip; the two incidence conditions give the intended reading. An edge set is small if $|\partial(X)|<\theta$ and it contains no complete row edge set $E(P_i)$. These are two separate requirements. An edge set can have a small boundary while still containing a whole row. Robertson and Seymour, 1991, pp. 171–172.

A subhypergraph $A$ specifies subsets $V(A)$ and $E(A)$ of the grid's vertices and edges, retaining the incidences of the ambient grid. A separation $(A,B)$ satisfies $A\cup B=G$ and $E(A\cap B)=\varnothing$; its order is $|V(A\cap B)|$. Although the grid is a simple graph, these are the paper's hypergraph definitions. A tangle $\mathcal T$ of order $\theta$ contains only separations of order below $\theta$ and satisfies three axioms: it chooses an orientation of every such separation; the union of the first sides of any three chosen separations is not $G$; and no chosen first side contains every vertex of $G$. The chosen three may coincide. Robertson and Seymour, 1991, pp. 153–154.

Formalization targets

The first milestone, (7.1), identifies a symmetry between rows and columns under a low boundary:

$$|\partial(X)|<\theta\quad\Longrightarrow\quad \bigl(\exists i,\ E(P_i)\subseteq X\bigr) \Longleftrightarrow \bigl(\exists j,\ E(Q_j)\subseteq X\bigr).$$

The second milestone, (7.2), says that three small edge sets cannot cover all the grid's edges:

$$X_1\cup X_2\cup X_3=E(G) \quad\Longrightarrow\quad \neg\bigl(X_1,X_2,X_3\text{ are all small}\bigr).$$

The goal, (7.3), defines $\mathcal T_\theta$ rather than taking it as an arbitrary set. It selects precisely the separations $(A,B)$ of order less than $\theta$ for which $E(A)$ is small, and asserts

$$\mathcal T_\theta\text{ is a tangle in }G\text{ of order }\theta.$$

These are the numbered §7 results on pp. 171–173, in the order used by the paper. Robertson and Seymour, 1991, pp. 171–173.

What the result supplies

The theorem gives an explicit tangle in a familiar graph for every order $\theta\ge2$. A tangle is more than a numerical connectivity bound: it records coherent choices across all separations below its order. In the paper, the grid tangle feeds the link between large grids and tangles of high order. The extension from a grid minor in another graph to a tangle of that graph invokes (6.1), beyond this mission's goal. The converse direction, that large tree-width forces a large grid minor, is (7.4), proved in Graph Minors V (Robertson and Seymour, 1986); the published definitions and statements of that paper on this platform are about grid minors and tree-width, not tangles. Robertson and Seymour, 1991, pp. 170, 173.

Formalizing (7.3) will make the grid tangle available as a checked object alongside the already published grid graph. It will also produce reusable definitions for an edge boundary, small edge sets and the paper's hypergraph separations. The Lean files here are draft statements with open proofs; the published 1986 grid definition is the existing checked ingredient. No machine-checked proof of (7.1), (7.2) or (7.3) is claimed by this proposal.

Where the difficulty lies

The obvious attempt at (7.2) counts boundary vertices column by column. If every column $Q_j$ has all its edges in $X_1\cup X_2$ and meets both sets, each column contributes at least two vertices to $|\partial(X_1)|+|\partial(X_2)|$, so the two boundaries together have at least $2\theta$ vertices. This only works when the third set misses the first and last rows; in general the third set can absorb edges of every column, and no single count over the whole grid bounds all three boundaries at once. The statement is a covering property of three sets, not a bound on any one of them, and the paper's argument for it is credited to D. Kleitman and M. Saks. The goal must then meet all three tangle axioms. The page's proof of (7.3) argues the first axiom and says only that the rest follows from (7.2); the third axiom, $V(A)\ne V(G)$, is part of the definition and must be established, not dropped. Robertson and Seymour, 1991, pp. 172–173.

Formalization scope

The source assumes finite hypergraphs throughout, and §7 fixes $\theta\ge2$. Lean uses a finite simple graph on Fin θ × Fin θ, reusing RobertsonSeymour1986.GM5.grid, and views its edge set as the edge type of a local hypergraph. Subhypergraphs hold vertex and edge subsets with inherited incidence. Set.ncard counts boundary vertices and separation order. Rows and columns use all grid edges whose two endpoints have the specified coordinate. This representation keeps every grid edge's identity, even though it is written as a SimpleGraph edge subtype.

IsSmall retains both $|\partial(X)|<\theta$ and the exclusion of full row edge sets. boundary requires an incident edge on each side of $X$. Both details are necessary for the claimed tangle: an IsSmall without the row clause would call every set with a small boundary small, including sets that contain whole rows, and the resulting set of separations is not a tangle; a boundary defined with "every edge outside $X$" instead of "some edge outside $X$" would be empty and make the size condition vacuous. The formalization keeps the third tangle axiom and does not replace it with an easier condition. The definitions of hypergraph, separation and tangle duplicate the shared encoding used by the other missions for this paper and can later be consolidated. The definitions also include the paper's tangle number and maximum edge size for that shared layer, though the grid goal does not invoke them; on finite inputs their maxima are bounded, and their empty-set value is zero.

The companion missions are Graph Minors. X. Obstructions to Tree-Decomposition I: Tangle Number Equals max(Branch-Width, Largest Edge Size), max(β(G), γ(G)) = θ(G); Graph Minors. X. Obstructions to Tree-Decomposition II: Branch-Width and Tree-Width Satisfy max(β, γ) ≤ ω + 1 ≤ max(⌊3β/2⌋, γ, 1); Graph Minors. X. Obstructions to Tree-Decomposition IV: Mutually Distinguishable Tangles Have a Tree-Decomposition Separating Them by Their Distinctions; and Graph Minors. X. Obstructions to Tree-Decomposition V: A θ-Pervasive Class of Designs Gives a Tree-Decomposition over 𝒮^{3θ−2} ∪ ℛ_{4θ−3}. Those missions address the paper's other main results; this one isolates the grid construction.

Selected references

• N. Robertson and P. D. Seymour, Graph Minors. X. Obstructions to Tree-Decomposition, Journal of Combinatorial Theory, Series B 52 (1991), 153–190. DOI: 10.1016/0095-8956(91)90061-n.
• N. Robertson and P. D. Seymour, Graph Minors. V. Excluding a Planar Graph, Journal of Combinatorial Theory, Series B 41 (1986), 92–114. DOI: 10.1016/0095-8956(86)90030-4.

Motivation

Tangles were introduced by Robertson and Seymour in Graph Minors. X (JCTB 1991) to make precise the idea of a "highly connected region" of a graph. A tangle orients every low-order separation of the graph towards one side, consistently. They are the organising notion of the later papers of the Graph Minors series, which culminate in the graph structure theorem and the proof of Wagner's conjecture.

Section 11 of Graph Minors X, Structure relative to a tangle, asks how local and global structure are related. In the paper's words: suppose that $G$ has large tangle number, but relative to each high-order tangle the graph has a structure of a certain kind $X$. What can be inferred about the global structure of $G$? One might guess that $G$ has a tree-decomposition into pieces each with structure $X$, but that is false. The theorem of §11 shows that $G$ does have a tree-decomposition into pieces which almost have structure $X$. The authors state that they need this for an application in a later paper of the series, cited as [6], Graph minors. XVII. Excluding a non-planar graph (submitted); it appeared as Graph Minors XVI (2003), where the local structure relative to a tangle is a near-embedding in a surface.

Setting

A hypergraph $G$ has a finite vertex set $V(G)$, a finite edge set $E(G)$ and an incidence relation. A subhypergraph $G' \subseteq G$ has $V(G') \subseteq V(G)$ and $E(G') \subseteq E(G)$, with every end of an edge of $G'$ in $V(G')$. A separation of $G$ is a pair $(A, B)$ of subhypergraphs with $A \cup B = G$ and $E(A \cap B) = \emptyset$, and its order is $|V(A \cap B)|$.

For $\theta \ge 1$, a tangle of order $\theta$ in $G$ is a set $\mathcal T$ of separations of order $< \theta$ such that (i) for each separation $(A, B)$ of order $< \theta$ one of $(A,B)$, $(B,A)$ is in $\mathcal T$; (ii) no three members $(A_i, B_i)$ of $\mathcal T$ have $A_1 \cup A_2 \cup A_3 = G$; (iii) $V(A) \ne V(G)$ for $(A, B) \in \mathcal T$.

A tree-decomposition $(T, \tau)$ of $G$ is a tree $T$ and subhypergraphs $\tau(t)$, $t \in V(T)$, whose union is $G$, which are pairwise edge-disjoint, and with $\tau(t) \cap \tau(t'') \subseteq \tau(t')$ whenever $t'$ lies on the path of $T$ between $t$ and $t''$.

A design is a pair $(H, M)$ of a hypergraph $H$ and a set $M$ of subsets of $V(H)$.

• The design of a node $t_0$ of $(T, \tau)$ with neighbours $t_1, \dots, t_k$ is $(\tau(t_0), \{V(\tau(t_0) \cap \tau(t_i))\})$. A tree-decomposition is over a class $\mathcal S$ of designs if the design of every node belongs to $\mathcal S$.
• $(H', M')$ is an $n$-enlargement of $(H, M)$ if, for some $Z \subseteq V(H')$ with $|Z| \le n$, $H \subseteq H'$, $V(H') - V(H) \subseteq Z$, $E(H') \subseteq E(H)$, and $X \cap V(H) \in M$ for every $X \in M'$ other than $Z$. $\mathcal S^n$ is the class of $n$-enlargements of members of $\mathcal S$, and $\mathcal R_n$ is the class of designs with at most $n$ vertices.
• A location in $G'$ is a set of separations $(A_i, B_i)$ of $G'$ with $A_i \subseteq B_j$ for $i \ne j$. Its design is $(G' \cap B_1 \cap \dots \cap B_k, \{V(A_i \cap B_i)\})$.
• A class $\mathcal S$ is $\theta$-pervasive in $G$ if for every subhypergraph $G' \subseteq G$ and every tangle $\mathcal T$ in $G'$ of order $\ge \theta$, some location $\mathcal L \subseteq \mathcal T$ in $G'$ has its design in $\mathcal S$.
• The $Z$-extension of $(H, M)$ is $(H, M \cup \{Z\})$.

Formalization targets

Goal: (11.1), p. 185

For $\theta \ge 1$ and a class $\mathcal S$ that is $\theta$-pervasive in $G$,

$$G \text{ has a tree-decomposition over } \mathcal S^{3\theta-2} \cup \mathcal R_{4\theta-3}.$$

Milestone: (11.2), pp. 185–186

If $\mathcal S$ is $\theta$-pervasive in $G$ and $|Z| = 3\theta - 2$, then either some separation $(A, B)$ of order $< \theta$ has

$$|(Z \cup V(A)) \cap V(B)|,\ |(Z \cup V(B)) \cap V(A)| \le 3\theta - 3,$$

or some location $\{(A_i, B_i)\}$ in $G$ with design in $\mathcal S$ has $|Z \cap V(A_i)| \le |V(A_i \cap B_i)| < \theta$ for all $i$.

Milestone: (11.3), p. 186

If $|Z| \le 3\theta - 2$, there is a tree-decomposition of $G$ over $\mathcal S' = \mathcal S^{3\theta-2} \cup \mathcal R_{4\theta-3}$ with a node $t_0$ such that $Z \subseteq V(\tau(t_0))$ and the $Z$-extension of the design of $t_0$ is in $\mathcal S'$. The goal is the case $Z = \emptyset$.

Companion: the remark on p. 188

For every $\theta \ge 1$, if $G$ has no tangle of order $\theta$, then

$$\omega(G) \le 4\theta - 4.$$

Consequently $\omega(G) \le 4\theta(G)$, where $\theta(G)$ is the tangle number. This is the p. 188 remark following (11.3).

Significance

(11.1) converts local information, stated tangle by tangle, into a global decomposition. Every piece of the decomposition is either small (at most $4\theta - 3$ vertices) or differs from a structure in $\mathcal S$ by at most $3\theta - 2$ added vertices. This is the kind of local-to-global step the later Graph Minors papers need: there the local structure near each high-order tangle is a near-embedding in a surface, and a result of this shape glues such local structures along a tree. With $\mathcal S = \emptyset$ it gives a tree-width bound $\omega(G) \le 4\theta(G)$, a weaker form of the tangle/tree-width duality.

The result has been proved since 1991. To our knowledge no proof assistant formalizes it, and none formalizes the hypergraph tangles or tree-decompositions of this paper. This mission produces machine-checked statements of the paper's notions of design, enlargement, location and pervasiveness, the structure theorem, and its inductive strengthening.

Difficulty

The first idea is to take the pieces in $\mathcal S$ themselves as the pieces of the tree-decomposition. That fails, and the paper says so: the pieces can only almost have the structure. Locations for different tangles interact, and the decomposition must absorb up to $3\theta - 2$ extra vertices into each piece. The induction also has to control a set $Z$ of attachment vertices of bounded size: a piece built at one node must still accept the vertices through which it is glued to the rest of the tree. Keeping $|Z| \le 3\theta - 2$ throughout the recursion is the delicate point, and it is why the strengthened statement (11.3), not (11.1), is the one that admits induction.

Formalization scope

• Hypergraphs. A hypergraph is a structure Hypergraph V E with an incidence relation. Finiteness is [Finite V] [Finite E] on every theorem. Subhypergraphs, separations, tangles and tree-decompositions are the series' shared encodings (namespace RobertsonSeymour1991.GM10.Structure). The tree of a tree-decomposition is a SimpleGraph on Fin n satisfying IsTree.
• Designs. Every design the statements involve has as hypergraph a subhypergraph of the fixed $G$. So a design is a $G$-design G.Sub × Set (Set V), and a class of designs is a set of $G$-designs. Classes need not be closed under isomorphism; the paper never uses that.
• Relative tangles. Separations, tangles and locations in a subhypergraph $G'$ are pairs of subhypergraphs of $G$ whose union is $G'$. For $G' = G$ they agree definitionally with the absolute notions.
• Pervasiveness. It quantifies over every subhypergraph $G'$ and every order $\theta' \ge \theta$. Restricting to $G' = G$ would be a different, stronger theorem. The paper's opening remark in the proof of (11.3), that pervasiveness passes to subhypergraphs, is immediate in this encoding and is not a separate item.
• Edge cases. The empty set is a location; its design is $(G', \emptyset)$.
• Integer arithmetic. Since $\theta \ge 1$, the bounds $3\theta-2$, $3\theta-3$ and $4\theta-3$ are exact natural numbers. Tree-width is an integer, and it is $-1$ for an empty vertex set.
• No trivial instances. IsPervasive is satisfiable: the class of all designs is $\theta$-pervasive, through the empty location. The conclusion is satisfiable too: the one-node decomposition lies over $\mathcal R_{|V(G)|}$. So neither the hypothesis nor the conclusion of (11.1) is vacuous.

The other main results of the paper are separate missions of this series:

• Graph Minors. X. Obstructions to Tree-Decomposition I (tangle number versus branch-width);
• II (branch-width versus tree-width);
• III (the grid tangle);
• IV (the tree-decomposition separating mutually distinguishable tangles).

Contributions are welcome on any item: proofs of (11.2) and (11.3), and of the p. 188 companion. The companion needs two auxiliary facts: a tangle of order $\ge \theta$ in a subhypergraph yields one of order $\theta$ in $G$, and tree-width is bounded by bag size.

Selected references

• N. Robertson, P. D. Seymour, Graph Minors. X. Obstructions to Tree-Decomposition, J. Combin. Theory Ser. B 52 (1991) 153–190. https://doi.org/10.1016/0095-8956(91)90061-n
• N. Robertson, P. D. Seymour, Graph Minors. XVI. Excluding a non-planar graph, J. Combin. Theory Ser. B 89 (2003) 43–76. https://doi.org/10.1016/S0095-8956(03)00042-X
• N. Robertson, P. D. Seymour, Graph Minors. V. Excluding a planar graph, J. Combin. Theory Ser. B 41 (1986) 92–114. https://doi.org/10.1016/0095-8956(86)90030-4

Motivation

The Graph Minors series of Robertson and Seymour proves that finite graphs are well-quasi-ordered under the minor relation. A central tool of the series is the duality between two ways of measuring how "tree-like" a graph is: decompositions along a tree, which certify that a graph is thin, and tangles, which certify that it contains a highly connected region that no small separation can split. Graph Minors X (Robertson and Seymour, 1991) introduces tangles and proves the exact minimax relation between the tangle number and branch-width, an invariant within a constant factor of tree-width. Tangles became a standard object of structural graph theory and were later abstracted to connectivity systems, matroids and data clustering; branch-width is the parameter behind dynamic-programming algorithms on graphs and matroids of bounded width.

Setting

A hypergraph $G$ consists of a finite vertex set $V(G)$, a finite edge set $E(G)$ and an incidence relation; an edge may be incident with any number of vertices, its ends, and the size of an edge is its number of ends. Write $\gamma(G)$ for the maximum size of an edge ($\gamma(G)=0$ if $E(G)=\emptyset$).

A subhypergraph is given by a set of vertices and a set of edges containing all ends of its edges. A separation of $G$ is a pair $(A,B)$ of subhypergraphs with $A\cup B=G$ and no common edge; its order is $|V(A\cap B)|$.

For an integer $\theta\ge1$, a tangle of order $\theta$ is a set $\mathcal T$ of separations of order $<\theta$ such that (i) for every separation $(A,B)$ of order $<\theta$, one of $(A,B),(B,A)$ lies in $\mathcal T$; (ii) $A_1\cup A_2\cup A_3\ne G$ for any three members $(A_i,B_i)$ of $\mathcal T$; (iii) $V(A)\ne V(G)$ for every $(A,B)\in\mathcal T$. The tangle number $\theta(G)$ is the largest order of a tangle in $G$, or $0$ if there is none.

A ternary tree is a tree whose vertices have valency $1$ or $3$. A branch-decomposition $(T,\tau)$ of $G$ is a ternary tree $T$ with a bijection $\tau$ from its leaves onto $E(G)$. Deleting an edge $f$ of $T$ splits the leaves, hence $E(G)$, into two parts; the order of $f$ is the number of vertices of $G$ incident with edges on both sides. The width is the largest order of an edge of $T$, and the branch-width $\beta(G)$ is the minimum width over all branch-decompositions, with $\beta(G)=0$ when $|E(G)|\le1$.

The proof goes through an abstract setting. On a finite set $E$, a connectivity function is a symmetric submodular map $\kappa:2^E\to\mathbb Z$. A set $X$ is efficient if $\kappa(X)\le0$. A bias is a set of efficient sets containing one of $X,E-X$ for each efficient $X$ and no three members covering $E$. Its dual object is a tree-labelling: a ternary tree whose incidences carry efficient sets, complementary across each edge, covering $E$ at each internal vertex, and absorbed by a given family $\mathcal A$ at each leaf.

Formalization targets

Goal: (4.3), p. 165

$$\max\bigl(\beta(G),\gamma(G)\bigr)=\theta(G)\qquad\text{unless }\gamma(G)=0\text{ and }V(G)\ne\emptyset.$$

The exception is genuine: a hypergraph with a vertex and only edges without ends has $\beta=\gamma=0$ and $\theta=1$.

Milestones

1. Tangle lemmas of §2: (2.2) closure under $(A\cup A',B\cap B')$; (2.3) $E(A_1\cup A_2\cup A_3)\ne E(G)$ for order $\ge2$; (2.4) an edge of size $\ge\theta$ defines a tangle of order $\theta$; (2.5) $G$ has a tangle iff $V(G)\ne\emptyset$; (2.7) the third axiom reduces to separations $(K_e,G\setminus e)$; (2.8) extreme separations have order $\theta-1$, and their large side is well connected.
2. The abstract minimax of §3: (3.1) a bias extending $\mathcal A$ excludes tree-labellings over $\mathcal A$; (3.2) tree-labellings can be made exact on the same tree; (3.3) leaf sets of an exact tree-labelling partition $E$; (3.4) no bias gives an exact tree-labelling; (3.5) the three-way equivalence; (3.6) leaf labels can be taken different from $E$.
3. The three claims of the proof of (4.3), for $\gamma(G)>0$, $k\ge\gamma(G)$, $\kappa=\kappa_0-k$ and $\mathcal A=\{\{e\}\}$: biases correspond to tangles of order $k+1$, exact tree-labellings to $\beta(G)\le k$, and hence $G$ has a tangle of order $k+1$ iff $k<\beta(G)$.

A companion statement, (4.4), computes $\theta(K_n)=\lceil 2n/3\rceil$ and, for $n\ge3$, $\beta(K_n)=\lceil 2n/3\rceil$.

Significance

The minimax theorem makes tangles the exact obstruction to small branch-width: either a branch-decomposition of width at most $k$ exists, or a tangle of order $k+1$ witnesses that none does. Every later use of tangles as certificates of high connectivity in the Graph Minors series, including the tree-decomposition of a graph into regions indexed by its maximal tangles and the grid theorem, rests on this duality. The abstract lemma (3.5) applies to any connectivity function, so it also gives the duality for matroid branch-width and for other symmetric submodular functions.

The results are proved in the published paper; none has a machine-checked proof that this mission is aware of. The platform has branch-width objects for set functions on subcubic trees, from the Oum–Seymour approximation of clique-width (ApproxCliqueWidth.Certificate.bw_ge_of_wellLinked, bw_le_of_no_wellLinked), which bound branch-width by well-linked sets, a different obstruction. This mission adds a hypergraph tangle library and the exact minimax.

Difficulty

The inequality $\theta(G)\ge\gamma(G)$ and the direction "a tangle of order $k+1$ excludes width $\le k$" are short. The converse, building a branch-decomposition of width $\le k$ when no tangle of order $k+1$ exists, is the hard direction. A natural first attempt is to merge small separations greedily into a tree, but the submodular uncrossing step can destroy the leaf conditions already established, and an induction on the edge set does not preserve the tangle hypothesis. A second difficulty is bookkeeping: the trees are ternary, so every construction that cuts, joins or contracts trees must restore valencies $1$ and $3$, and the passage between leaf labels and edges of $G$ needs the labels at the leaves to partition $E(G)$.

Formalization scope

The objects live in the namespace RobertsonSeymour1991.GM10.Minimax.

• Hypergraphs are a structure with an incidence predicate on arbitrary types V, E; every theorem assumes [Finite V] [Finite E], as the paper assumes all hypergraphs finite.
• Subhypergraphs are determined by their vertex and edge sets.
• A tangle is a predicate IsTangle G θ 𝒯 with $\theta\ge1$ built in, and the three members in the second axiom need not be distinct. The tangle number is a supremum in $\mathbb N$ of a set bounded by $|V(G)|$, so it is a maximum.
• Ternary trees and the trees of branch-decompositions and tree-labellings live on Fin n. A branch-decomposition stores $\tau$ as an injection of the edges onto the leaves.
• Branch-width is $0$ for $|E(G)|\le1$ and otherwise an infimum over a nonempty set.
• In §3 subsets are Set E, and $E-X$ is the complement. The incidence $(u,e)$ with $e=uw$ is the adjacent pair $(u,w)$, and every condition on labels is required on adjacent pairs only.
• The claims of the proof of (4.3) carry the paper's own context, $\gamma(G)>0$ and $k\ge\gamma(G)$, as hypotheses.

Junk values would make the goal trivial: a tangle number of $0$ from an unbounded set of orders, or a branch-width of $0$ from an empty set of decompositions. Neither occurs: every tangle has order at most $|V(G)|$, and a branch-decomposition exists whenever $|E(G)|\ge2$. The goal also keeps the exact exception $\neg(\gamma(G)=0\wedge V(G)\neq\emptyset)$, neither dropped nor strengthened.

A complete development needs finite trees with leaf counting, path and component reasoning in SimpleGraph, and submodular uncrossing arguments. The tangle library of §2 and the abstract minimax of §3 can be reused beyond this mission. Contributions of tree lemmas (ternary trees on Fin n, grafting two trees at a leaf, contracting a valency-2 vertex) are welcome.

The other main results of the paper are separate missions of this series: Graph Minors. X. … II: Branch-Width and Tree-Width Satisfy max(β, γ) ≤ ω + 1 ≤ max(⌊3β/2⌋, γ, 1), III: In the θ-Grid, the Separations of Order < θ With Small E(A) Form a Tangle of Order θ, IV: Mutually Distinguishable Tangles Have a Tree-Decomposition Separating Them by Their Distinctions, and V: A θ-Pervasive Class of Designs Gives a Tree-Decomposition over 𝒮^{3θ−2} ∪ ℛ_{4θ−3}.

Selected references

• N. Robertson, P. D. Seymour, Graph Minors. X. Obstructions to Tree-Decomposition, J. Combin. Theory Ser. B 52 (1991) 153–190. https://doi.org/10.1016/0095-8956(91)90061-n
• N. Robertson, P. D. Seymour, Graph Minors. V. Excluding a Planar Graph, J. Combin. Theory Ser. B 41 (1986) 92–114. https://doi.org/10.1016/0095-8956(86)90030-4
• S. Oum, P. D. Seymour, Approximating clique-width and branch-width, J. Combin. Theory Ser. B 96 (2006) 514–528. https://doi.org/10.1016/j.jctb.2005.10.006

Motivation

Tree-width measures how closely a graph resembles a tree. It is the central width parameter of the Graph Minors series of N. Robertson and P. D. Seymour, which proves that finite graphs are well-quasi-ordered by the minor relation, and it governs the complexity of many algorithms: problems that are NP-hard in general become solvable in linear time on graphs of bounded tree-width (Courcelle's theorem). Branch-width, introduced in Graph Minors X (Robertson, Seymour 1991), is a second width parameter, defined from ternary trees whose leaves carry the edges of the graph. It is the natural parameter for the paper's main minimax theorem, which equates branch-width with the maximum order of a tangle, the obstruction to small decompositions.

Section 5 of Graph Minors X shows that the two parameters are equivalent, within a factor 3/2. This is what transfers the tangle duality from branch-width to tree-width, and it is why later work (for instance on matroid branch-width and on rank-width) treats branch-width as an interchangeable substitute for tree-width.

Setting

All objects are finite. A hypergraph $G$ has a vertex set $V(G)$, an edge set $E(G)$, and an incidence relation; the ends of an edge are the vertices incident with it, and an edge may have any number of ends. $\gamma(G)$ is the maximum number of ends of an edge, or $0$ if $E(G)=\emptyset$. A subhypergraph consists of subsets of $V(G)$ and $E(G)$ such that every end of a chosen edge is a chosen vertex; unions, intersections and inclusion of subhypergraphs are taken setwise.

A tree is a connected non-null graph without circuits; its leaves are its vertices of valency at most $1$, and it is ternary if every valency is $1$ or $3$.

A branch-decomposition of $G$ is a pair $(T,\tau)$ with $T$ a ternary tree and $\tau$ a bijection from the leaves of $T$ onto $E(G)$. The order of an edge $f$ of $T$ is the number of vertices $v$ of $G$ such that $v$ is an end both of an edge labelling a leaf in one component of $T\setminus f$ and of an edge labelling a leaf in the other. The width of $(T,\tau)$ is the maximum order of an edge of $T$, and the branch-width $\beta(G)$ is the minimum width, or $0$ if $|E(G)|\le 1$.

A tree-decomposition of $G$ is a pair $(T,\tau)$ with $T$ a tree and $\tau(t)$ a subhypergraph of $G$ for every $t\in V(T)$, such that

1. the union of all $\tau(t)$ is $G$;
2. for distinct $t,t'$, the parts $\tau(t)$ and $\tau(t')$ share no edge;
3. if $t'$ lies on the path of $T$ between $t$ and $t''$, then $\tau(t)\cap\tau(t'')\subseteq\tau(t')$.

Its width is $\max_t\,(|V(\tau(t))|-1)$, and the tree-width $\omega(G)$ is the minimum width; $\omega(G)=-1$ exactly when $V(G)=\emptyset$. Each part is a subhypergraph and each edge lies in exactly one part, which differs from the familiar vertex-bag tree-decompositions of graphs, but gives the same tree-width on graphs.

The tangle number $\theta(G)$ is the maximum order of a tangle in $G$ (p. 154), or $0$ if there are none.

Formalization targets

Goal: (5.1)

$$\max\bigl(\beta(G),\gamma(G)\bigr)\;\le\;\omega(G)+1\;\le\;\max\bigl(\lfloor\tfrac32\beta(G)\rfloor,\ \gamma(G),\ 1\bigr)\qquad\text{for every finite hypergraph } G.$$

Milestones

• Second inequality of (5.1): $\omega(G)+1\le\max(\lfloor\tfrac32\beta(G)\rfloor,\gamma(G),1)$.
• Claims (1), (2), (3) of the proof of (5.1), under the proof's standing assumptions $\gamma(G)>0$, $|E(G)|\ge 2$ and no isolated vertices: there is a tree-decomposition of width $\omega(G)$ in which (1) every edge $e$ is the only edge of a leaf part whose vertices are exactly the ends of $e$, and parts at vertices of valency $\ge2$ have no edges; (2) moreover every leaf part has exactly one edge; (3) moreover every vertex of $T$ has valency at most $3$. The claims are cumulative.
• First inequality of (5.1): $\max(\beta(G),\gamma(G))\le\omega(G)+1$.

Companion: (5.2)

$$\theta(G)\;\le\;\omega(G)+1\;\le\;\tfrac32\,\theta(G).$$

Significance

The result. (5.1) shows that branch-width and tree-width bound each other up to the factor $3/2$ and the edge-size correction, and the page records that both bounds are attained ($K_n$ with $3\mid n$ for the right-hand side, $K_{n,n}$ minus a perfect matching for the left-hand side). Together with the minimax theorem (4.3) of the same paper, $\max(\beta(G),\gamma(G))=\theta(G)$ unless $\gamma(G)=0$ and $V(G)\ne\emptyset$, it yields (5.2): tangles are, up to the factor $3/2$, the exact obstruction to tree-decompositions of small width. That duality is the form in which tree-width enters the later papers of the Graph Minors series.

Formalizing it. The result is proved (1991); no machine-checked proof of it is known to exist. The platform holds tree-width statements for simple graphs with vertex bags (Graph Minors V, RobertsonSeymour1986.GM5.treewidth_le_theta9 and excluding_planar_graph), which are a different theorem about a different object. This mission formalizes the hypergraph tree-decomposition and branch-decomposition of Graph Minors X and the comparison between them. The companion missions of this series are Graph Minors. X. Obstructions to Tree-Decomposition I (the minimax theorem (4.3)), III (the grid tangle (7.3)), IV (the tree-decomposition separating distinguishable tangles (10.3)) and V (the structure theorem (11.1)).

Difficulty

The second inequality converts a branch-decomposition into a tree-decomposition; the difficulty is to obtain the bound with the floor $\lfloor\tfrac32\beta\rfloor$ and the separate $\gamma(G)$ term exactly, not up to an additive error.

The first inequality is where the obvious approach stalls: a tree-decomposition of minimum width is not a branch-decomposition. Its tree may have vertices of any valency, its leaves may carry no edge or several, and an edge may sit at an internal vertex. The three claims of the proof normalize an optimal tree-decomposition step by step without increasing its width. Each step modifies a tree on a finite vertex type while preserving three structural conditions (covering, edge-disjointness, the path condition), and the final step, suppressing vertices of valency $2$, must be shown to produce a ternary tree with the edge orders bounded by part sizes. Most of the formal work is this tree surgery.

Formalization scope

• Every theorem quantifies over types V, E with [Finite V] [Finite E] (the paper's "all hypergraphs in this paper are finite", p. 154) and a hypergraph G : Hypergraph V E given by its incidence relation.
• Trees are SimpleGraph (Fin n) with IsTree (connected, hence non-null, and acyclic). A leaf is a vertex of valency at most $1$; valency is (T.neighborSet t).ncard.
• A branch-decomposition stores $\tau$ as its inverse, an injective map from edges onto the leaves. $\beta(G)$ is set to $0$ when $|E(G)|\le1$ and is otherwise the sInf of the widths, which is a genuine minimum because a branch-decomposition exists when $|E(G)|\ge2$.
• Widths of tree-decompositions are integers, so that $\omega(G)=-1$ when $V(G)=\emptyset$. $\omega(G)$ is the sInf in $\mathbb Z$ of all $w$ bounding every $|V(\tau(t))|-1$; the set is nonempty (one-vertex tree with $\tau=G$) and bounded below by $-1$, so the sInf is the minimum width and not a junk value.
• $\lfloor\tfrac32\beta(G)\rfloor$ is the natural-number division 3 * β / 2; the ceiling would be a weaker statement. In (5.2), $\omega(G)+1\le\tfrac32\theta(G)$ is stated as $2(\omega(G)+1)\le3\theta(G)$, which is equivalent.
• The claims read "we may assume X" as "some tree-decomposition of width $\omega(G)$ satisfies X", under the proof's standing assumptions $\gamma(G)>0$, $|E(G)|\ge2$ and no isolated vertices (p. 168).
• Condition (ii) of a tree-decomposition, edge-disjointness of the parts, is kept as on the page. Replacing it by "every edge lies in some part", or allowing an empty tree, would change the tree-width and trivialize the comparison; both are ruled out.

Infrastructure needed and reusable beyond this mission: tree surgery on SimpleGraph (Fin n) (attaching a leaf, deleting a leaf, splitting a vertex, suppressing valency-2 vertices), the existence of branch-decompositions for $|E|\ge2$, and the computation of sInf-defined widths. Contributions of such lemmas, of proofs of the individual claims, and of small examples ($K_n$, grids) are welcome.

Selected references

• N. Robertson, P. D. Seymour, Graph Minors. X. Obstructions to Tree-Decomposition, J. Combin. Theory Ser. B 52 (1991) 153–190. https://doi.org/10.1016/0095-8956(91)90061-n
• N. Robertson, P. D. Seymour, Graph Minors. V. Excluding a Planar Graph, J. Combin. Theory Ser. B 41 (1986) 92–114. https://doi.org/10.1016/0095-8956(86)90030-4
• B. Courcelle, The monadic second-order logic of graphs. I. Recognizable sets of finite graphs, Information and Computation 85 (1990) 12–75. https://doi.org/10.1016/0890-5401(90)90043-H

Motivation

Telephone and data networks are often fully connected at the core: every pair of switching centres has a direct trunk group, and a call that finds its direct trunk full may be alternatively routed over a two-link path through a third, tandem centre. Whether such a network can absorb fluctuations of demand without losing traffic depends on how the spare capacity of lightly loaded links can be borrowed by heavily loaded ones. F. P. Kelly's survey Loss networks (Ann. Appl. Probab., 1991, doi:10.1214/aoap/1177005872) studies this question in §4.6, "Results respecting graph structure", by looking at a static snapshot of the network: random loads on the edges of a complete graph, and the question whether they can all be carried at once.

Timeline:

• Hajek (1986, personal communication cited as [21] in the survey) considered edges coloured independently red (a pair that needs twice an edge's capacity) or white (an idle edge), and proved that for red probability $p<1/3$ all red pairs can be served over white two-edge paths with probability tending to one (Theorem 4.40, p. 357).
• Hajek (1987, [22]) showed the same threshold for routing each red pair on a single two-edge path (Theorem 4.43, quoted, p. 358).
• Kelly (1991, Theorem 4.45, p. 358) extended Theorem 4.40 from two-valued loads to general i.i.d. loads with an exponential moment, under the condition $2\,\mathbb E(X-C)^+<\mathbb E(C-X)^+$. The survey gives the proof in full on p. 359.

Setting

Let $K\ge 1$ and consider the complete graph on the nodes $\{0,\dots,K-1\}$: every unordered pair $e=\{a,b\}$ of distinct nodes is an edge, and there are $\tfrac12K(K-1)$ edges. Every edge has capacity $C$.

An offered load $x_e\ge 0$ is attached to every edge $e$. The load of $e=\{a,b\}$ may be carried on its direct edge, or on a two-edge route $a-k-b$ through a tandem node $k\notin e$; such a route uses the two edges $\{a,k\}$ and $\{b,k\}$. Loads are divisible. The loads are routable with capacity $C$ if there are flows $f_{e,k}\ge 0$ (zero when $k\in e$) with $\sum_k f_{e,k}\le x_e$ such that on every edge $g$

$$\Big(x_g-\sum_k f_{g,k}\Big)+\sum_{(e,k):\ g \text{ on the route of } e \text{ via } k} f_{e,k}\le C,$$

i.e. the directly carried part of $g$'s own load plus all two-edge traffic passing through $g$ is at most $C$.

The loads are random: $X$ is a nonnegative real random variable with law $\mu$, and the loads $(x_e)$ are independent, each distributed as $X$. Let

$$P(K)=\mathbb P\{\text{the loads on the complete graph on } K \text{ nodes are routable}\}.$$

Write $\mathbb E(X-C)^+$ for the mean excess of a load over the capacity and $\mathbb E(C-X)^+$ for the mean spare capacity.

Formalization targets

Goal: Theorem 4.45

If $\mathbb E\,e^{\lambda X}<\infty$ for some $\lambda>0$ and

$$2\,\mathbb E(X-C)^+<\mathbb E(C-X)^+ \tag{4.46}$$

then

$$P(K)\to 1 \qquad (K\to\infty).$$

Milestones (in the order of the proof on pp. 358–359)

With $m=\mathbb E(C-X)^+$ and $0<\varepsilon<m^2$:

1. In each triangle the cyclic reservations $(x_e-C)^+(C-x_{ak})^+(C-x_{bk})^+/((K-2)(m^2-\varepsilon))$ are positive at most once, and only for an overloaded edge routed through two underloaded ones.
2. If every overloaded edge's reservations cover its excess and no underloaded edge has more reserved through it than it has spare, the loads are routable.
3. $\mathbb E\,Y=m^2/(m^2-\varepsilon)>1$ for $Y=(C-X_2)^+(C-X_3)^+/(m^2-\varepsilon)$.
4. $\mathbb E\,Z=2\,\mathbb E(X-C)^+\,m/(m^2-\varepsilon)<1$ for small $\varepsilon$, for $Z=\big((X_1-C)^+(C-X_2)^++(X_2-C)^+(C-X_1)^+\big)/(m^2-\varepsilon)$.
5. (4.48): $\mathbb P\{\sum_{i\le n} n^{-1}Y_i<1\}\le e^{-nI_1}$ for some $I_1>0$ and all $n\ge 1$.
6. (4.49): $\mathbb P\{\sum_{i\le n} n^{-1}Z_i>1\}\le e^{-nI_2}$ for some $I_2>0$ and all $n\ge 1$, when $X$ has an exponential moment.
7. $1-P(K)\le\tfrac12K(K-1)\,(P_1(K-2)+P_2(K-2))$.

Significance

The result. Theorem 4.45 says that in a large fully connected network, a load distribution whose mean overload is less than half its mean spare capacity can be served, with probability tending to one, using only direct and two-link routes. The factor $2$ reflects that each unit of overflow occupies two edges. The condition is explicit and depends on the load law only through two expectations, which makes it a design rule: capacity $C$ suffices for large networks as soon as (4.46) holds. Comment 4.47 (p. 358) observes that the two-valued law $\mathbb P\{X=2\}=p$, $\mathbb P\{X=0\}=1-p$ with $C=1$ turns (4.46) into Hajek's threshold $p<1/3$.

Formalizing it. The theorem is proved, in full, on one page; nothing here is open. The mission produces a machine-checked version of that proof: a precise routing event on the complete graph, the deterministic reservation argument, two Cramér–Chernoff tail bounds with rates uniform in the network size, and the union bound over edges. To our knowledge none of these steps is formalized anywhere, and no routing-feasibility event on a complete graph exists in Mathlib or on the platform.

Difficulty

The obvious approach is to fix an overloaded edge and argue that, among its $K-2$ two-edge routes, enough pass through two underloaded edges. That count is binomial and concentrates, but it does not prove the theorem: the same underloaded edge sits on two-edge routes of many overloaded pairs, so the reservations of different pairs compete for its spare capacity, and the routing decisions of different pairs are dependent. Any argument has to control, simultaneously at every edge, both the flow an overloaded edge can shed and the flow an underloaded edge is asked to absorb, with exponential rates uniform in $K$ so that a union bound over $\tfrac12K(K-1)$ edges survives; this is the central difficulty. On the upper side the variables are unbounded, so the exponential moment of $X$ has to be carried over to the reserved flows.

Formalization scope

The Lean development lives in the namespace KellyLossNetworks.Routing.

• Edges are {e : Sym2 (Fin K) // ¬ e.IsDiag}; loads are functions Edge K → ℝ.
• The routing event Feasible C x lets each pair split its load arbitrarily over its direct edge and all its two-edge routes, charges a two-edge flow to both edges of its route, requires the flow sent away from a pair not to exceed its load, and imposes the capacity constraint on every edge, including overloaded ones. Flows are real (divisible loads); integer routing is a different problem.
• "Independent and identically distributed" is the product measure Measure.pi (fun _ : Edge K => μ), with μ a probability measure on ℝ and X ≥ 0 almost surely. $P(K)$ is the measure of the routing event; no measurability of that event is presupposed.
• Expectations are Bochner integrals. The exponential moment is integrability of $t\mapsto e^{\theta t}$ for some $\theta>0$; it implies that $(X-C)^+$ is integrable, so (4.46) compares genuine expectations.
• The limit is along $K\in\mathbb N$ with no lower bound on $K$; for $K\le 2$ there are no two-edge routes, which does not affect the limit.
• The rates $I_1,I_2$ in (4.48) and (4.49) are quantified before $n$ and may not depend on it.

A trivializing formalization is ruled out: an event that allows only direct routing, ignores the capacity of the edges a detour passes through, or lets a pair send away more than its load would make the statement false or empty, and the routing event here does none of these.

A complete development needs Fubini on product measures, the Cramér–Chernoff method for averages of i.i.d. variables (both tails, with the lower tail for a bounded nonnegative variable and the upper tail under an exponential moment), measure-preserving projections of Measure.pi, and combinatorics of the triangles through an edge of the complete graph. The Cramér–Chernoff bounds with rates uniform in $n$ are reusable well beyond this mission. Contributions to any milestone are welcome; the deterministic milestones 1–2 and the expectation computations 3–4 are independent of the tail bounds and of each other.

Selected references

• F. P. Kelly, Loss networks, Annals of Applied Probability 1(3):319–378, 1991. doi:10.1214/aoap/1177005872
• B. Hajek, Average case analysis of greedy algorithms for Kelly's triangle problem and the independent set problem, 26th IEEE Conference on Decision and Control, 1987 (reference [22] of the survey; the source of Theorem 4.43).
• H. Chernoff, A measure of asymptotic efficiency for tests of a hypothesis based on the sum of observations, Annals of Mathematical Statistics 23(4):493–507, 1952. doi:10.1214/aoms/1177729330