Motivation

Szemerédi's regularity lemma partitions the vertex set of any graph into a bounded number of parts between which edges are distributed almost randomly. It is a central tool of extremal graph theory, but the number of parts it needs is a tower of exponentials in $1/\epsilon$, which makes it unusable in algorithms. In 1996 and 1999 Frieze and Kannan introduced a weaker notion, now called weak regularity: a partition is good if, for every pair of disjoint vertex sets $S,T$, the number of edges between them is predicted, up to an additive error $\epsilon n^2$, by the densities between the parts. This weaker requirement is enough to approximate dense instances of Max-Cut and other problems, and it can be met with only $2^{O(1/\epsilon^2)}$ parts.

The paper Frieze and Kannan, Quick approximation to matrices and applications, Combinatorica 19 (1999) derives such partitions from a matrix decomposition. Section 5.1 shows that if the adjacency matrix of a graph is approximated by a sum of a few cut matrices with small error in the cut norm, then the atoms of the sets defining those cut matrices form a pseudo-regular partition. The weak regularity of this paper later became the basis of the cut-distance theory of graph limits (Lovász, Large networks and graph limits, AMS, 2012).

Setting

Let $G=(V,E)$ be a simple graph with $n=|V|$ vertices and adjacency matrix $\mathbf A$. For a real $V\times V$ matrix $\mathbf M$ and $S,T\subseteq V$ write $\mathbf M(S,T)=\sum_{i\in S}\sum_{j\in T}\mathbf M(i,j)$. A cut matrix $\mathrm{CUT}(R,C,d)$ has entry $d$ on $R\times C$ and $0$ elsewhere. A cut decomposition of width $s$ is a sum $\mathbf D=\mathbf D^{(1)}+\dots+\mathbf D^{(s)}$ of cut matrices $\mathbf D^{(t)}=\mathrm{CUT}(R_t,C_t,d_t)$; its error is $\mathbf W=\mathbf A-\mathbf D$.

Let $\mathcal P=V_1,\dots,V_k$ be a partition of $V$ with index set $K$, write $X_i=X\cap V_i$, let $e(S,T)$ be the number of edges between disjoint sets $S$ and $T$, and let $d_{i,j}=e(V_i,V_j)/(|V_i||V_j|)$ be the density between parts. The deviation from regularity is

$$\Delta_{\mathcal P}(S,T)=e(S,T)-\sum_{i\in K}\sum_{j\in K}d_{i,j}|S_i||T_j|,$$

and $\mathcal P$ is $\epsilon$-pseudo-regular if $|\Delta_{\mathcal P}(S,T)|\le\epsilon n^2$ for all disjoint $S,T\subseteq V$.

For a partition $\mathcal Q=W_1,\dots,W_q$, the block average $\mathbf M_{\mathcal Q}$ of $\mathbf M$ takes the value $\mathbf M(W_i,W_j)/(|W_i||W_j|)$ on $W_i\times W_j$, and $\mathbf M$ is compatible with $\mathcal Q$ if it is constant on every block $W_i\times W_j$. The atom partition of $R_1,\dots,R_s,C_1,\dots,C_s$ is the coarsest partition of $V$ in which every $R_t$ and $C_t$ is a union of parts; it has at most $4^s$ parts.

Formalization targets

Goal: claim (50), p. 204

If the cut decomposition has error at most $\epsilon n^2$, that is

$$|\mathbf A(S,T)-\mathbf D(S,T)|\le\epsilon n^2\quad\text{for all }S,T\subseteq V,$$

then the atom partition $V_1,\dots,V_k$ of the sets $R_t,C_t$ satisfies

$$|\Delta_{\mathcal P}(S,T)|\le 2\epsilon n^2\quad\text{for all disjoint }S,T\subseteq V,$$

i.e. it is $2\epsilon$-pseudo-regular. The width $s$ is unconstrained: the statement holds for decompositions of any width, and the width only enters through the bound $k\le 4^s$ on the number of parts.

Milestones

1. (47), p. 203. For disjoint $S,T$: $\mathbf A(S,T)=e(S,T)$, $\mathbf A_{\mathcal Q}(S,T)=\sum_{i,j}d_{i,j}|S_i||T_j|$, hence

$$\mathbf A(S,T)-\mathbf A_{\mathcal Q}(S,T)=\Delta_{\mathcal Q}(S,T).$$

2. D is compatible with $\mathcal P$, p. 204. The sum of the cut matrices is constant on every block of the atom partition.
3. Lemma 7(a), p. 203. If $\mathcal Q$ refines $\mathcal P$ and $\mathbf M$ is compatible with $\mathcal P$, then

$$\sup_{S,T\subseteq V}|\mathbf A(S,T)-\mathbf A_{\mathcal Q}(S,T)|\le 2\sup_{S,T\subseteq V}|\mathbf A(S,T)-\mathbf M(S,T)|.$$

Companions

• Lemma 7(b), p. 204. If $\mathbf M$ is compatible with $\mathcal P$, then $\|\mathbf A-\mathbf A_{\mathcal P}\|_F\le\|\mathbf A-\mathbf M\|_F$.
• $k\le 4^s$, p. 204. The atom partition of $2s$ sets has at most $4^s$ parts.

Significance

Claim (50) is the bridge from matrix approximation to graph partitions. Combined with Theorem 7 of the same paper (every matrix has a cut decomposition of width at most $1/\epsilon^2$ with cut-norm error $\epsilon\sqrt{mn}\|\mathbf A\|_F\le\epsilon n^2$ for a graph), it gives the weak regularity lemma: every graph has a $2\epsilon$-pseudo-regular partition into at most $4^{1/\epsilon^2}$ parts. Pseudo-regularity in turn means that $e(S,T)$ is determined up to $2\epsilon n^2$ by the numbers $|S_i|,|T_j|$, which reduces Max-Cut and related problems on dense graphs to a search over a bounded-dimensional space. Lemma 7(a) is of independent use: Section 5.1.1 of the paper applies it again to pass to an equitable refinement.

The results are proved in the paper. Mathlib contains Szemerédi's regularity lemma in its equipartition form, and the platform has a published statement of it; neither the Frieze–Kannan weak regularity statement, the deviation $\Delta_{\mathcal P}$, nor Lemma 7 has a machine-checked proof known to this mission. The mission produces a formal statement and proof of the partition half of the weak regularity lemma, reusable with any cut decomposition, including the existence result of the companion mission on cut decompositions.

Difficulty

The identity (47) and the compatibility of $\mathbf D$ are bookkeeping, but bookkeeping over Mathlib's Finpartition, atomise and the rational-valued edgeDensity, with sums over parts that must be regrouped into sums over vertices. The substance lies in Lemma 7(a). The obvious argument bounds $|\mathbf A-\mathbf A_{\mathcal Q}|$ by $|\mathbf A-\mathbf M|+|\mathbf M-\mathbf A_{\mathcal Q}|$, and the difficulty is the second term: $\mathbf M-\mathbf A_{\mathcal Q}$ is constant on the blocks of $\mathcal Q$, but its block sums on arbitrary $S,T$ have to be controlled by block sums of $\mathbf A-\mathbf M$, on which $\mathbf A$ and $\mathbf A_{\mathcal Q}$ need not agree. The printed argument handles only disjoint $S,T$, while the lemma is stated, and needed, for all pairs; a complete proof must cover pairs that overlap.

Formalization scope

All objects are defined in one definitions item in the namespace FriezeKannan.PseudoReg. The vertex set is a Fintype $V$ with decidable equality, the graph a SimpleGraph V with decidable adjacency, and its adjacency matrix Mathlib's adjMatrix over $\mathbb R$. A partition of $V$ is a Finpartition of Finset.univ, whose parts are the index set $K$; refinement is Mathlib's order $\mathcal Q\le\mathcal P$. Densities are SimpleGraph.edgeDensity, cast to $\mathbb R$, for all pairs of parts. For distinct parts this is the paper's $d(V_i,V_j)$. For a part with itself it is the block average $\mathbf A(V_i,V_i)/|V_i|^2$, not the value $e(A,A)/\binom{|A|}{2}$ printed in the §5 preamble: with the printed value the identity (47) fails on diagonal blocks, and the proof of (50) uses (47). The atom partition is Mathlib's Finpartition.atomise of the family $\{R_t\}\cup\{C_t\}$. The Frobenius norm is the square root of the sum of squared entries.

The paper takes the cut matrices from its Theorem 2, a randomized algorithm. The goal replaces this by the one property its proof uses: the hypothesis $|\mathbf A(S,T)-\mathbf D(S,T)|\le\epsilon n^2$ for all $S,T\subseteq V$ (Theorem 2 bounds the cut norm, a maximum over all pairs, by $\epsilon n\|\mathbf A\|_F\le\epsilon n^2$). The paper's symmetrised error $\bar{\mathbf W}$ is not needed. Lemma 7 is stated for an arbitrary real matrix $\mathbf A$, and the suprema of Lemma 7(a) are written as "every bound $c$ on the right-hand family gives the bound $2c$ on the left-hand family", over all pairs $S,T$. No hypothesis is added to any statement.

The partition in the goal is fixed as the atom partition. A formalization that let the partition vary would be trivial: the partition into singletons has $\Delta\equiv0$.

Needed infrastructure: regrouping sums over a Finpartition, and block sums of matrices constant on the blocks of a partition, on arbitrary and on block-compatible sets. These are reusable for any statement about cut norms of block-constant matrices. Proofs of the milestones, of the companions, and of the goal are all welcome.

Selected references

• A. Frieze and R. Kannan, Quick approximation to matrices and applications, Combinatorica 19(2):175–220, 1999. https://doi.org/10.1007/s004930050052
• A. Frieze and R. Kannan, The regularity lemma and approximation schemes for dense problems, Proc. 37th FOCS, 12–20, 1996. https://doi.org/10.1109/SFCS.1996.548459
• E. Szemerédi, Regular partitions of graphs, Problèmes combinatoires et théorie des graphes, Colloq. Internat. CNRS 260, 399–401, 1978.
• L. Lovász, Large networks and graph limits, AMS Colloquium Publications 60, 2012. https://doi.org/10.1090/coll/060

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

Routing several commodities through one capacitated network at the same time is a basic problem of network optimization, with applications to communication networks, VLSI layout and divide-and-conquer graph algorithms. Its optimum is the value of a linear program, but the natural certificates of an upper bound are combinatorial: every cut of the network limits how much can be routed across it. For a single commodity the max-flow min-cut theorem says that the best cut certificate is exact. With many commodities it is not, and the size of the gap between the best flow and the best cut is the question of this mission.

• 1988–1999, Leighton and Rao proved that for uniform demands (one unit between every pair of vertices) the gap is $O(\log n)$ on an $n$-vertex network, and that the bound is attained on expanders (Leighton–Rao, JACM 1999; FOCS 1988).
• 1990–1995, Klein, Rao, Agrawal and Ravi extended a polylogarithmic bound to arbitrary demands, $O(\log C \log D)$ in the total capacity $C$ and total demand $D$ (Combinatorica 15, 1995); Plotkin and Tardos improved it to $O(\log^2 k)$ in the number of commodities $k$ (Combinatorica 15, 1995).
• 1995, Linial, London and Rabinovich (Combinatorica 15, 1995), and independently Aumann and Rabani (SIAM J. Comput. 1998), showed that the gap is bounded by the least distortion of embedding a metric derived from the network into $\ell_1$, and obtained the bound $O(\log k)$ from Bourgain's embedding theorem. This mission formalizes that theorem, Theorem 4.1 of the Linial–London–Rabinovich paper.

Setting

A multicommodity flow network has a finite vertex set $V$, capacities $C_{i,j} = C_{j,i} \ge 0$ (zero for non-edges and on the diagonal), and $k$ commodities: commodity $\mu$ has a source $s_\mu$, a sink $t_\mu$ and a demand $D_\mu \ge 0$.

A feasible concurrent flow of value $\lambda$ sends, for every $\mu$, $\lambda D_\mu$ units of commodity $\mu$ from $s_\mu$ to $t_\mu$: arc flows $f_\mu(i,j) \ge 0$ satisfy conservation of matter, with net outflow $\lambda D_\mu$ at $s_\mu$, $-\lambda D_\mu$ at $t_\mu$ and $0$ elsewhere, and the total flow of all commodities through each undirected edge $\{i,j\}$, in both directions, is at most $C_{i,j}$. The maxflow of the network is the largest such $\lambda$.

For $S \subseteq V$, $\mathrm{Cap}(S) = \sum_{i \in S}\sum_{j \notin S} C_{i,j}$ is the capacity of the edges leaving $S$, and $\mathrm{Dem}(S)$ is the total demand of the pairs that $S$ separates, i.e. with $|S \cap \{s_\mu,t_\mu\}| = 1$. Every flow of value $\lambda$ has to push $\lambda\,\mathrm{Dem}(S)$ units across the cut, so

$$\mathrm{maxflow} \le \frac{\mathrm{Cap}(S)}{\mathrm{Dem}(S)} \quad\text{for every } S \text{ with } \mathrm{Dem}(S) > 0.$$

A semi-metric on $V$ is a function $d \ge 0$ with $d(i,i) = 0$, symmetry and the triangle inequality; distinct points may be at distance $0$, as in the paper.

Formalization targets

Goal: Theorem 4.1

There is an absolute constant $C_0 > 0$ such that every network in which some commodity has $D_\mu > 0$ and $s_\mu \ne t_\mu$ has a set $S \subseteq V$ with $\mathrm{Dem}(S) > 0$ and

$$\frac{\mathrm{Cap}(S)}{\mathrm{Dem}(S)} \le C_0 \log(\max(k,2)) \cdot \mathrm{maxflow}.$$

The constant is not fixed; only the shape $O(\log k)$ in the number of commodities is asserted.

Milestones, in the order the proof uses them

1. Weak duality (§4, p. 226): $\lambda\,\mathrm{Dem}(S) \le \mathrm{Cap}(S)$ for every feasible $\lambda \ge 0$ and every $S$.
2. LP duality display (p. 227): $\mathrm{maxflow} = \min_d \dfrac{\sum_{\{i,j\}} C_{i,j} d_{i,j}}{\sum_\mu D_\mu d_{s_\mu,t_\mu}}$ over semi-metrics $d$.
3. Corollary 3.4, Claim 2 (p. 223): every finite semi-metric space with $k$ marked pairs has a non-expanding map into some $\ell_1^m$ that shrinks each marked pair by at most $C_1 \log(\max(k,2))$.
4. Coordinate minimum (p. 227): for points of $\ell_1^m$, the cost-to-demand ratio is at least its value on the best single coordinate.
5. 0/1 rounding (pp. 227–228): for symmetric real weights $a$ and nonnegative symmetric weights $b$, the minimum of $\sum a_{ij}|z_i - z_j| / \sum b_{ij}|z_i - z_j|$ over real vectors $z$ is attained at a 0/1 vector.

Significance

The theorem bounds the flow–cut gap: the integrality gap of the linear relaxation of the sparsest cut problem is $O(\log k)$, so solving one linear program and rounding gives an $O(\log k)$-approximation to the sparsest cut. Sparsest-cut approximations are the engine of approximation algorithms for minimum bisection, graph partitioning, crossing number and VLSI layout. The dependence on $k$ rather than on the number of vertices matters when few pairs carry demand. The bound is tight up to the constant: on constant-degree expanders with all-pairs unit demands the gap is $\Omega(\log n)$ (Leighton–Rao).

The result has been proved since 1995 and is textbook material (Williamson–Shmoys, Ch. 15). It has no machine-checked proof. A formalization adds a verified bridge between concurrent flows, LP duality on networks and $\ell_1$ embeddings of finite metrics; each piece is reusable on its own. Corollary 3.4, Claim 2 in particular is a terminal version of Bourgain's theorem, of which no formal proof exists either.

Difficulty

Two steps carry the weight. The first is the duality between concurrent flows and metrics: Mathlib has no linear programming duality theorem in a form that applies directly, and the dual of the arc-flow program has to be identified with a minimum over semi-metrics, which needs a shortest-path argument on top of LP duality. The second is the embedding: Claim 2 of Corollary 3.4 must achieve distortion $O(\log k)$ on the $k$ marked pairs, independent of $|X|$. A direct application of Bourgain's theorem to the whole space gives $O(\log |X|)$, which is not enough when $k$ is much smaller than the number of vertices, and the paper's proof is a one-line reference to an earlier argument.

Formalization scope

• Vertex sets are finite types V with [Fintype V] [DecidableEq V]; capacities are a function C : V → V → ℝ with symmetry, nonnegativity and zero diagonal as fields of a Network structure. Commodities are indexed by Fin k; coincident or repeated pairs are allowed.
• Flows are arc flows; the capacity bounds the total over all commodities and both directions. maxflow is the supremum of feasible values; Lean's sSup returns $0$ on an unbounded set, which only happens without a commodity of positive demand and distinct endpoints, and the goal assumes one.
• Sums over edges are over unordered pairs: the page's $\sum_{i \ne j}$ in the LP-duality and coordinate displays counts each edge twice, while $\mathrm{Cap}$ counts it once; the statements use $\tfrac12\sum_i\sum_j$ in both places, which removes the factor-2 slip without changing the proof.
• Explicit constants. The paper's $O(\log k)$ in Theorem 4.1 is $C_0 \log(\max(k,2))$ with $C_0$ quantified before the network; the $\Omega(1/\log k)$ of Corollary 3.4 is $1/(C_1\log(\max(k,2)))$ with $C_1$ quantified before the metric space. The $\max(k,2)$ keeps $k = 1$ in scope, where $\log k = 0$.
• Out of scope. The deterministic polynomial-time algorithms of Theorem 4.1 and Corollary 3.4, and the target dimension $\ell_1^{O(n^2)}$ of the latter, are not stated; the statements assert the existence of the cut and of the embedding.
• The 0/1 rounding step adds $b \ge 0$, which the page omits but its argument needs.
• A trivializing formalization is ruled out: the constant $C_0$ is quantified before the network, so it cannot depend on the instance, and maxflow is defined from flows, not as the metric minimum.
• Contributions welcome: an LP duality theorem for finite-dimensional linear programs in the form needed here, a formal Bourgain-type embedding with terminal distortion, and the max-flow min-cut theorem for undirected capacities.

Selected references

• N. Linial, E. London, Y. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica 15 (1995) 215–245. https://doi.org/10.1007/BF01200757
• Y. Aumann, Y. Rabani, An O(log k) approximate min-cut max-flow theorem and approximation algorithm, SIAM J. Comput. 27 (1998) 291–301. https://doi.org/10.1137/S0097539794285983
• T. Leighton, S. Rao, Multicommodity max-flow min-cut theorems and their use in designing approximation algorithms, J. ACM 46 (1999) 787–832. https://doi.org/10.1145/331524.331526
• J. Bourgain, On Lipschitz embedding of finite metric spaces in Hilbert space, Israel J. Math. 52 (1985) 46–52. https://doi.org/10.1007/BF02776078
• D. P. Williamson, D. B. Shmoys, The Design of Approximation Algorithms, Cambridge University Press, 2011, Chapter 15. https://doi.org/10.1017/CBO9780511921735