Graph Theory

Motivation

An expander is a sparse graph in which every set of vertices has many neighbours outside itself. Expanders are the building blocks of superconcentrators (sparse directed graphs that route any $r$ inputs to any $r$ outputs along vertex-disjoint paths), of sorting and switching networks, and of many constructions in complexity theory and coding; the survey of Hoory, Linial and Wigderson (Bull. AMS 2006) describes these uses. Random regular graphs are expanders with high probability, but applications need explicit families with fixed degree and a uniform expansion constant.

Alon and Milman (J. Combin. Theory Ser. B 38 (1985)) replace combinatorial expansion by a spectral quantity, the second-smallest eigenvalue $\lambda_1$ of the matrix $Q = D - A$ of a graph, which Fiedler called the algebraic connectivity (Czech. Math. J. 1973). Their Theorem 4.3 shows that a regular graph with $\lambda_1$ bounded away from $0$ yields an expander. This mission formalizes their Section 4 source of such graphs: Cayley graphs of the finite quotients of a group with Kazhdan's property (T).

Timeline:

• 1967: Kazhdan introduces property (T) and proves that $SL(n,\mathbb{Z})$, $n \ge 3$, has it (Funct. Anal. Appl. 1 (1967)).
• 1973: Margulis uses property (T) to give the first explicit expander family (Probl. Inf. Transm. 9 (1973)).
• 1981: Gabber and Galil give a variant of Margulis' construction with an explicit expansion constant, proved by Fourier analysis (J. Comput. Syst. Sci. 22 (1981)).
• 1985: Alon and Milman state the construction in terms of $\lambda_1$ (Lemma 4.8, Theorem 4.9) and link it to the concentration property of Section 2 of their paper.

Setting

Let $T$ be a finite group. A finite multigraph on $T$ is a symmetric matrix $M = (M_{w,u})$ of nonnegative integers, $M_{w,u}$ being the number of edges joining $w$ and $u$ (diagonal entries count loops). It is $k$-regular if every row sums to $k$. Its matrix is $Q = \operatorname{diag}(d(v)) - M$ with $d(v) = \sum_u M_{v,u}$, a real symmetric positive semidefinite matrix. Its eigenvalues, repeated according to multiplicity, are $0 = \lambda_0 \le \lambda_1 \le \dots \le \lambda_{|T|-1}$, and $\lambda_1(G)$ denotes the second of them.

Let $H$ be a group, $S \subseteq H$ a finite set with $S = S^{-1}$, and $\phi : H \to T$ a homomorphism onto $T$. The Cayley multigraph $G(T, \phi(S))$ joins $w$ and $u$ by as many edges as there are $s \in S$ with $w u^{-1} = \phi(s)$. It is $|S|$-regular, and its matrix is $Q = |S| \cdot I - \sum_{s\in S} \pi(\phi(s))$, where $\pi(t)$ is the permutation matrix of the left regular representation, $(\pi(t))_{w,u} = 1$ iff $w u^{-1} = t$.

An $(n,k,\varepsilon)$-enlarger (Definition 4.1) is a $k$-regular graph on $n$ vertices with $\lambda_1 \ge \varepsilon$.

A unitary representation $\pi$ of $H$ in a complex Hilbert space $V$ is essentially nontrivial (Definition 4.5) if no nonzero vector is fixed by every $\pi(h)$. A discrete group $H$ has property (T) (Definition 4.6) if there are $\varepsilon > 0$ and a finite $K \subseteq H$ such that for every essentially nontrivial unitary representation $\pi$ and every unit vector $y$ some $h \in K$ satisfies $|(\pi(h)y, y)| < 1 - \varepsilon$.

Formalization targets

Goal: Theorem 4.9

Let $H$ have property (T), let $S$ be a finite generating set of $H$ with $S = S^{-1}$, and let $\phi_i : H \to T_i$ be surjective homomorphisms onto finite groups with $|T_i| \to \infty$. Then there is one $\varepsilon > 0$ with

$$G(T_i, \phi_i(S)) \text{ is a } (|T_i|,\ |S|,\ \varepsilon)\text{-enlarger for every } i \text{ with } |T_i| \ge 2 .$$

The constant is unspecified: the theorem asserts uniformity in $i$, not a value.

Milestones, in the order the paper's argument uses them

1. Lemma 4.7. For any generating set $S$ of a property (T) group there is $\varepsilon > 0$ such that every essentially nontrivial unitary representation and every unit vector $y$ admit $s \in S$ with $|(\pi(s)y,y)| < 1-\varepsilon$.
2. Proof of Lemma 4.8, essential nontriviality. For $\phi$ onto $T$, every nonzero vector of $W = \{v : \sum_t v_t = 0\}$ is moved by some $\pi(\phi(h))$.
3. Proof of Lemma 4.8, Rayleigh's principle. For the Cayley multigraph, $\min\{(Qy,y) : y \in W,\ \|y\| = 1\} = \lambda_1(G)$.
4. Lemma 4.8. With $H$, $S$ and $\varepsilon$ as in Lemma 4.7, $S$ finite and $S = S^{-1}$, and $\phi$ onto a finite group $T$, the Cayley graph $G(T,\phi(S))$ is a $(|T|, |S|, \varepsilon)$-enlarger.

Significance

Theorem 4.9 turns an analytic property of one infinite group into a uniform spectral bound for infinitely many finite graphs of fixed degree. With Theorem 4.3 of the paper it produces explicit families of linear expanders, hence of linear superconcentrators; for $H = SL(n,\mathbb{Z})$, $n \ge 3$, and its reductions modulo $i$ the paper obtains infinitely many explicit families of $(n, 4, \varepsilon)$-enlargers. The same mechanism underlies later work on expanders from groups, surveyed in Lubotzky's monograph (Birkhäuser 1994).

The result is proved in the paper, modulo Lemma 4.7, which the paper refers to Margulis for. The formalization adds a checked account of every step, including Lemma 4.7 itself. At the pinned Mathlib revision there is no notion of property (T), of Kazhdan constants, or of the algebraic connectivity of a multigraph, and no machine-checked version of Theorem 4.9 is known on this platform.

Difficulty

The combinatorial and linear-algebra steps are routine; the substance is in two places. First, Lemma 4.7: Definition 4.6 supplies a constant for one finite set $K$, nothing in the definition relates $K$ to a given generating set $S$, the paper gives no proof, and the standard references state the textbook form $\|\pi(h)y - y\| \ge \varepsilon$ rather than the paper's absolute-value form $|(\pi(h)y,y)| < 1-\varepsilon$. Second, the uniformity: a spectral gap for each fixed quotient is easy, since a connected graph has $\lambda_1 > 0$, but a bound that does not decay as $|T_i| \to \infty$ is exactly what cannot come from any finite computation and must come from property (T) through Lemma 4.8. The Rayleigh quotient of milestone 3 is taken over real vectors, while Lemma 4.7 is stated for complex Hilbert spaces.

Formalization scope

Groups are Lean types with a Group instance; the finite groups $T$ carry Fintype and DecidableEq. Graphs are multigraphs given by symmetric matrices Matrix T T ℕ, with loops allowed. This matters: when $\phi$ identifies two generators or sends one to the identity, the degree is still $|S|$, and a loop contributes $0$ to $Q$. Mathlib's SimpleGraph Cayley graph forgets these multiplicities and is not used. $\lambda_1$ is the second-smallest eigenvalue with multiplicity of the real symmetric matrix $Q$ (via Matrix.IsHermitian.eigenvalues₀). It is defined spectrally, as in the paper, and not as a Rayleigh minimum. It is only meaningful for $|T| \ge 2$, and the goal excludes trivial quotients explicitly. Unitary representations are homomorphisms into the unitary group of bounded operators on a complex Hilbert space in universe Type. Compact subsets of a discrete group are finite sets.

A trivializing formalization is ruled out. Property (T) is not replaced by the hypothesis that the regular representations of the quotients have no almost-invariant vectors, which would make Theorem 4.9 a restatement of its hypothesis. And $\lambda_1$ is not defined as the minimum of $(Qy,y)$ over zero-sum unit vectors, which would make milestone 3 true by definition.

A complete development needs basic Kazhdan-constant manipulations, Courant–Fischer for real symmetric matrices, and the regular representation of a finite group as a unitary representation. The regularity of Cayley multigraphs and the identity $Q = |S| I - \sum_s \pi(\phi(s))$ are short. The spectral and representation-theoretic lemmas are reusable beyond this mission. Contributions of intermediate lemmas, such as the variational characterization of eigenvalues₀ or the invariance of the zero-sum subspace, are welcome.

Selected references

• N. Alon, V. D. Milman, λ1, Isoperimetric inequalities for graphs, and superconcentrators, J. Combin. Theory Ser. B 38 (1985) 73–88. https://doi.org/10.1016/0095-8956(85)90092-9
• D. A. Kazhdan, Connection of the dual space of a group with the structure of its closed subgroups, Funct. Anal. Appl. 1 (1967) 63–65. https://doi.org/10.1007/BF01075866
• G. A. Margulis, Explicit constructions of concentrators, Probl. Inf. Transm. 9 (1973) 325–332. http://mi.mathnet.ru/ppi1162
• O. Gabber, Z. Galil, Explicit constructions of linear-sized superconcentrators, J. Comput. Syst. Sci. 22 (1981) 407–420. https://doi.org/10.1016/0022-0000(81)90040-4
• M. Fiedler, Algebraic connectivity of graphs, Czech. Math. J. 23 (1973) 298–305. https://doi.org/10.21136/CMJ.1973.101168
• A. Lubotzky, Discrete Groups, Expanding Graphs and Invariant Measures, Birkhäuser, 1994. https://doi.org/10.1007/978-3-0346-0332-4
• B. Bekka, P. de la Harpe, A. Valette, Kazhdan's Property (T), Cambridge University Press, 2008. https://doi.org/10.1017/CBO9780511542749
• S. Hoory, N. Linial, A. Wigderson, Expander graphs and their applications, Bull. AMS 43 (2006) 439–561. https://doi.org/10.1090/S0273-0979-06-01126-8

Motivation

The eigenvalues of the Laplacian of a graph carry metric information about the graph. The second-smallest one, $\lambda_1(G)$, was named the algebraic connectivity by Fiedler (Fiedler 1973), who showed it is positive exactly for connected graphs. N. Alon and V. D. Milman (J. Combin. Theory Ser. B 38 (1985) 73–88) showed that a large $\lambda_1$ also forces two further properties: small diameter and a concentration of measure phenomenon, in which almost every vertex is close to any set containing half the vertices. They used these facts to build explicit expanders and superconcentrators, which are sparse networks with strong connectivity guarantees used in the theory of computation and in communication network design.

This mission covers Section 2 of that paper, "The Main Tools": the edge-count inequality (Lemma 2.1), the isoperimetric inequalities (Theorems 2.5 and 2.6), and the resulting diameter bound (Theorem 2.7).

Timeline:

• 1973: Fiedler introduces $\lambda_1(G)$ as algebraic connectivity and proves $\lambda_1 \le \frac{n}{n-1}\min_v d(v)$.
• 1985: Alon and Milman prove the isoperimetric and diameter bounds of Section 2.
• 1986: Alon proves the converse direction, that edge expansion implies a spectral gap (Alon 1986).
• Later work sharpened the constant in the diameter bound, e.g. Chung 1989.

Setting

Let $G = (V, E)$ be a finite, connected, simple graph on $n = |V| \ge 2$ vertices. Write $d(v)$ for the degree of a vertex $v$, $d = \max_v d(v)$ for the maximum degree, and $A_G$ for the adjacency matrix. The Laplacian is the $V \times V$ matrix

$$Q = Q_G = \operatorname{diag}(d(v))_{v \in V} - A_G .$$

For real functions $f$ on $V$ with scalar product $(f, g) = \sum_v f(v)g(v)$, the quadratic form of $Q$ is $(Qf, f) = \sum_{\{u,v\} \in E} (f(u) - f(v))^2 \ge 0$. The eigenvalues of $Q$, counted with multiplicity, are real and are written $0 = \lambda_0 \le \lambda_1 \le \dots \le \lambda_{n-1}$. The algebraic connectivity $\lambda_1 = \lambda_1(G)$ is the second-smallest of them.

For vertices $u, v$, $\operatorname{dist}(u, v)$ is the number of edges of a shortest path from $u$ to $v$. For disjoint vertex sets $A, B$ the paper writes $\rho$ for the distance between them, $a = |A|/n$ and $b = |B|/n$ for their relative sizes, and $E_A$ ($E_B$) for the set of edges with both endpoints in $A$ (in $B$). $[x]$ denotes the integer part of $x \ge 0$.

Formalization targets

Goal: Theorem 2.7 (p. 79)

$$\operatorname{dist}(u, v) \;\le\; 2\left[\sqrt{2d/\lambda_1}\,\log_2 n\right] \qquad\text{for all } u, v \in V.$$

Milestones, in the order the proof uses them

1. Section 2, p. 76: $0 = \lambda_0 < \lambda_1$ for connected $G$.
2. Eq. (2.1), Rayleigh's principle: if $\sum_v f(v) = 0$ then $(Qf, f) \ge \lambda_1 \|f\|^2$.
3. Lemma 2.1: for nonempty $A, B$ at distance $\rho \ge 1$,

$$\lambda_1 n \le \frac{1}{\rho^2}\Big(\frac1a + \frac1b\Big)\big(|E| - |E_A| - |E_B|\big).$$

4. Remark 2.3: $\lambda_1 \le \frac{n}{n-1}\min_v d(v)$.
5. Theorem 2.5: if $\rho > 1$ then

$$b \le \frac{1-a}{1 + (\lambda_1/d)\,a\rho^2}.$$

6. Theorem 2.6: if every $A$–$B$ distance exceeds a real $\rho \ge 1$, then

$$b \le (1-a)\exp\!\Big(-\ln(1+2a)\Big[\sqrt{\lambda_1/(2d)}\,\rho\Big]\Big).$$

Each statement keeps the paper's explicit constants. The goal is the endpoint of this chain and the paper's headline graph-theoretic bound.

Significance

Theorem 2.7 gives, for any family of graphs of bounded maximum degree whose algebraic connectivity stays bounded away from zero, a diameter of order $\log n$. By the paper's Remark 2.8, the 4-regular graphs constructed in its Section 4 show that this order cannot be improved. Theorem 2.6 is a discrete concentration of measure inequality: the proportion of vertices at distance more than $\rho$ from a set of relative size $a$ decays exponentially in $\rho\sqrt{\lambda_1/(2d)}$. It is the graph analogue of the Gromov–Milman concentration for manifolds, and Section 3 of the paper applies it to cubes and other product graphs. Theorem 2.5 is the input for the construction of expanders from graphs with a spectral gap (Theorem 4.3 of the paper).

All results are proved in the paper, and the formal work here is a machine-checked version of known proofs. As far as could be determined, none of the four inequalities (Lemma 2.1, Theorems 2.5–2.7) has been formalized in Lean or elsewhere. Mathlib has the Laplacian matrix, its positive semidefiniteness, and the relation between its kernel and connected components, but no statement about its second eigenvalue. The spectral facts (milestones 1–2), stated for Mathlib's Matrix.IsHermitian.eigenvalues₀, are reusable for any future work on algebraic connectivity.

Difficulty

The combinatorial steps are short. The work is at the interface between the spectral definition and the quadratic form. Mathlib defines eigenvalues through the spectral theorem for a Hermitian matrix, sorted into a list. Obtaining Rayleigh's principle for the second eigenvalue from that list, with the constant functions as the eigenvector of $\lambda_0 = 0$, takes a Courant–Fischer-type argument over an orthonormal eigenbasis. It does not follow from positive semidefiniteness alone. Strict positivity of $\lambda_1$ additionally needs that the kernel of $Q$ is one-dimensional for a connected graph.

Theorem 2.6 iterates Theorem 2.5 over a sequence of neighbourhoods $\{v : \operatorname{dist}(v, A) \le j\mu\}$ with a real step length $\mu$, so it needs bookkeeping of integer parts and of real-valued distance thresholds. Theorem 2.7 then combines Theorem 2.6 with Remark 2.3 and needs the estimate $\tfrac12\, 2^{-[\log_2 n]} < 1/n$ with the integer part kept. Replacing $[\cdot]$ by the real number inside it changes the statement.

Formalization scope

• Graphs are Mathlib SimpleGraph V on a Fintype vertex type with decidable adjacency. Every item assumes G.Connected and $2 \le |V|$ (the goal writes $1 < |V|$, as the paper does).
• $Q$ is G.lapMatrix ℝ. $\lambda_1$ is the mission definition AlonMilman.Diameter.lambda1: the eigenvalue at index $n-2$ of eigenvalues₀, which lists the eigenvalues in decreasing order. It is $0$ by convention when $n < 2$, a case no theorem uses.
• $\lambda_1$ is defined spectrally. Defining it as the best constant in Eq. (2.1) would make Rayleigh's principle definitional and remove the spectral content of the mission, so that formalization is excluded. Likewise the goal quantifies over all pairs of vertices of a connected graph and does not use SimpleGraph.diam without connectivity, since that is $0$ for a disconnected graph.
• Distances are SimpleGraph.dist (a natural number). "The distance between $A$ and $B$ is $\rho$" is encoded as $\rho \le \operatorname{dist}(u, v)$ for all $u \in A$, $v \in B$. Because the bounds weaken as $\rho$ decreases, this is equivalent to the paper's exact distance. In Theorem 2.6 $\rho$ is real and the hypothesis is strict.
• $E_A$ is AlonMilman.Diameter.edgesWithin G A. All counts are cast to $\mathbb R$ before subtraction, $a = |A|/n$ is a real quotient, $[x]$ is Nat.floor, $\log_2$ is Real.logb 2, and $\ln$ is Real.log.
• Lemma 2.1 requires $A, B$ nonempty (so $a, b > 0$). Theorems 2.5 and 2.6 hold as stated for empty sets and carry no such hypothesis.

Contributions welcome: proofs of any milestone, and in particular general Mathlib-style lemmas for Rayleigh quotients and eigenvalues₀, which have uses beyond this mission.

Selected references

• N. Alon, V. D. Milman, λ1, isoperimetric inequalities for graphs, and superconcentrators, J. Combin. Theory Ser. B 38 (1985) 73–88. https://doi.org/10.1016/0095-8956(85)90092-9
• M. Fiedler, Algebraic connectivity of graphs, Czechoslovak Math. J. 23 (1973) 298–305. https://doi.org/10.21136/CMJ.1973.101168
• N. Alon, Eigenvalues and expanders, Combinatorica 6 (1986) 83–96. https://doi.org/10.1007/BF02579166
• F. R. K. Chung, Diameters and eigenvalues, J. Amer. Math. Soc. 2 (1989) 187–196. https://doi.org/10.1090/S0894-0347-1989-0965008-X

Motivation

Given a $k$-connected graph, many connectivity algorithms run in time that grows with the number of edges $|E|$. A sparse certificate is a spanning subgraph with only $O(k|V|)$ edges that is still $k$-connected; computing one first and running the expensive algorithm on it replaces $|E|$ by $k|V|$ in the bound. Finding a $k$-connected spanning subgraph with the minimum number of edges is NP-complete for every fixed $k \ge 2$ (Garey and Johnson, problem GT31), so the question is how cheaply a sparse, not necessarily minimum, certificate can be found.

Nagamochi and Ibaraki (Algorithmica 7 (1992) 583–596) answered this with a single linear-time scanning procedure, FOREST, which partitions the edges into classes $E_1, E_2, \dots, E_{|E|}$. They showed that the prefix unions $E_1 \cup \dots \cup E_k$ are certificates for edge-connectivity and, for simple graphs, for node-connectivity. The node-connectivity result is the subject of this mission; the edge-connectivity result is the preceding mission of this series.

Timeline:

• 1980: Galil gives an algorithm testing $\kappa(G) \ge k$ whose running time depends on $|E|$ (SIAM J. Comput. 9).
• Before 1992 (as cited on p. 583): Suzuki et al. give $O(|E|)$-time algorithms for sparse 2- and 3-node-connected spanning subgraphs; Nishizeki and Poljak find, for general $k$, a $k$-node-connected spanning subgraph with at most $k(|V|-1)$ edges in $O(|V|^{1/2}|E|^2)$ time.
• 1992: Nagamochi and Ibaraki prove that FOREST, which runs in $O(|V| + |E|)$ time, yields a $k$-node-connected spanning subgraph $G_k$ of every simple $k$-node-connected graph, with $|E(G_k)| \le k|V| - k(k+1)/2$. Their Theorem 3.1 states a stronger, local form.
• 1993: Cheriyan, Kao and Thurimella isolate "scan-first search" as the general principle behind such certificates (SIAM J. Comput. 22 (1993)).

Setting

A graph $G = (V, E)$ has a finite node set $V$ with $|V| \ge 2$ and a finite edge set $E$; each edge has an unordered pair of two distinct end nodes. In this mission the graph is simple: no two edges have the same end nodes. For $F \subseteq E$, $(V, F)$ is the spanning subgraph with edge set $F$.

The local node-connectivity $\kappa(x, y; H)$ of nodes $x, y$ in a graph $H$ on $V$ is $|V| - 1$ if $x$ and $y$ are adjacent in $H$, and otherwise the minimum size of a node set $W \subseteq V - \{x, y\}$ whose deletion leaves no $x$–$y$ path. The node connectivity is $\kappa(G) = \min_{x, y} \kappa(x, y; G)$.

Procedure FOREST keeps a label $r(v) \ge 0$ on each node, initially $0$. While some node is unscanned, it chooses an unscanned node $x$ of largest label; for each unscanned edge $e = (x, y)$ it puts $e$ into the class $E_{r(y)+1}$, increases $r(x)$ by one if $r(x) = r(y)$, and increases $r(y)$ by one; then it marks $x$ scanned. Ties are broken arbitrarily. The time instants are the states between these elementary operations; $E^*_i$ denotes the class $i$ at an instant, and $E_i$ its final value. Put

$$G_i = (V,\ E_1 \cup E_2 \cup \dots \cup E_i).$$

Formalization targets

Goal: Theorem 3.1

For a simple graph $G$ and the classes of any completed run of FOREST, for $1 \le i \le |E|$,

$$\kappa(x, y; G_i) \ \ge\ \min\{\kappa(x, y; G),\ i\} \qquad \text{for any } x, y \in V. \tag{3.1}$$

The statement is local: it holds pair by pair, not only for the global minimum, and for every tie-breaking of the procedure.

Milestones, in the order the proof uses them

1. Lemma 2.2: at every instant, a node $v$ meets $E_i$ exactly for $i = 1, \dots, r(v)$.
2. Lemma 2.4(b): at every instant, a $u$–$v$ path in $E^*_j$ yields $u$–$v$ paths in every $E^*_i$, $i < j$.
3. In-degree at most one (§2, p. 588): orienting each edge from the earlier-scanned to the later-scanned end, every node has at most one entering arc in each class.
4. Lemma 3.1: if an $x$–$y$ path of $E^*_j$ has the form $x, u_1, \dots, u_k = w, y$ with $k = 1$ or $u_1$ scanned before $w$, then any $w$–$x$ and $w$–$y$ paths in $E^*_i$ ($i < j$) share a node other than $w$.
5. Lemma 3.2: for a node cut set $W = \{w_1, \dots, w_i\}$ of $G_{i+1}$ (in scan order) separating a component $X$ from the rest $Y$, immediately after $w_t$ is scanned every $X$–$Y$ path of $E^*_t$ passes through $w_t$, and $E^*_j$ has no $X$–$Y$ path for $t + 1 \le j \le i + 1$.

A companion item states the paper's announcement in §3: $G_k$ is $k$-node-connected for every $1 \le k \le \kappa(G)$.

Significance

Theorem 3.1 at $i = k$ shows that the first $k$ classes of FOREST form a $k$-node-connected spanning subgraph whenever $G$ is, and the edge-count analysis of the companion mission bounds its size by $k|V| - k(k+1)/2$. Since FOREST runs in linear time, any algorithm testing $\kappa(G) \ge k$ can be run on $G_k$ instead of $G$; the paper uses this to improve the bound for testing $\kappa(G) \ge k$ from $O(\max\{k^2|V|^{1/2}, k|V|\}|E|)$ to $O(\max\{k^3|V|^{3/2}, k^2|V|^2\})$, and similar gains for computing the number of node-disjoint paths between two nodes. The local form (3.1) is what makes the $s$–$t$ applications possible.

The result is proved on paper. As far as a search of the platform shows, neither FOREST nor local node-connectivity has a machine-checked treatment there; Mathlib has no notion of vertex connectivity of a pair of nodes. This mission produces a formal model of FOREST as a nondeterministic transition system and the statements needed to verify the paper's proof step by step.

Difficulty

For edge-connectivity the analogous statement follows from a general principle: any sequence of maximal spanning forests, each taken in what remains of the graph, preserves local edge-connectivity up to its length. The obvious attempt is to prove (3.1) the same way, from the fact that each $E_i$ is a maximal spanning forest of what the earlier classes leave. The paper gives no such argument for node-connectivity: its proof uses the specific scan order of FOREST in an essential way, through the orientation of edges from earlier- to later-scanned nodes and the in-degree bound of that orientation (Lemmas 3.1 and 3.2). The argument tracks, for a hypothetical node cut $W$ of size $i$ in $G_{i+1}$, the classes at the moments the nodes of $W$ are scanned, which requires reasoning about intermediate states of the algorithm and about paths in several classes at once. None of this reduces to a static property of the output partition.

Formalization scope

• Graphs. A node type V and an edge type E, both finite, with ends : E → Sym2 V; loop-freeness is ∀ e, ¬ (ends e).IsDiag and simplicity is Function.Injective ends. The standing assumptions of p. 583 and p. 589 ($|V| \ge 2$, no self-loop, a simple graph when node-connectivity is discussed) appear as hypotheses; §2 items are stated for loopless graphs, as on the page.
• Connectivity. $\kappa(x, y; (V, F))$ is valued in $\mathbb N_\infty$: $|V| - 1$ on adjacent pairs, the minimum node cut otherwise, and $\top$ when $x = y$, where (3.1) holds trivially.
• FOREST. A nondeterministic step relation with three steps (select, scan, finish), a run of length $K$ from the initial state, and completion when every node is scanned. Every tie-breaking is allowed, so the theorems quantify over all completed runs. A time instant is a state of a run; "scanned before" compares positions in the run's selection order; "immediately after $w_t$ has been scanned" is the state right after the finish step of $w_t$.
• Excluded. The running time "$O(|V| + |E|)$" and everything in §4 (the connectivity-testing algorithms and their bounds) are not stated: the paper fixes no machine model. The edge bounds on $|E_i|$ belong to the edge-connectivity mission.
• Ruled out. Stating (3.1) for an arbitrary partition into maximal spanning forests, or reading the classes $E^*_j$ of Lemmas 3.1–3.2 off the final state, would state a different theorem from the one the paper proves; the classes are those of a run of FOREST at the instant the page specifies.
• Infrastructure. Reachability avoiding a node set, walks and paths in SimpleGraph, and invariants of the FOREST transition system. The definitions duplicate those of the edge-connectivity mission by design and are candidates for a shared layer. Contributions of general lemmas about the run (label invariants, monotonicity of classes along a run) are welcome.

Selected references

• H. Nagamochi, T. Ibaraki, A linear-time algorithm for finding a sparse $k$-connected spanning subgraph of a $k$-connected graph, Algorithmica 7 (1992), 583–596. https://doi.org/10.1007/BF01758778
• Z. Galil, Finding the vertex connectivity of graphs, SIAM J. Comput. 9 (1980), 197–199. https://doi.org/10.1137/0209016
• J. Cheriyan, M.-Y. Kao, R. Thurimella, Scan-first search and sparse certificates: an improved parallel algorithm for $k$-vertex connectivity, SIAM J. Comput. 22 (1993), 157–174. https://doi.org/10.1137/0222013
• M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, Freeman, 1979.

Motivation

Many graph algorithms for connectivity questions run in time proportional to the number of edges. When the question is only whether a graph is $k$-edge-connected, or what its local edge-connectivities are up to a threshold $k$, most edges are irrelevant: a spanning subgraph with $O(k|V|)$ edges already carries the answer. Such a subgraph is called a sparse certificate. Computing one first and running the expensive algorithm on it replaces $|E|$ by $k|V|$ in the running time of connectivity testing, of Matula-type edge-connectivity algorithms, and of $s$–$t$ flow computations used as connectivity oracles.

Nagamochi and Ibaraki (Algorithmica 7, 1992) gave a procedure, FOREST, that computes such a certificate for edge-connectivity and, on simple graphs, for node-connectivity, with a single graph search. The same partition of the edges into forests is the engine of their deterministic minimum-cut algorithm for multigraphs (SIAM J. Discrete Math. 5, 1992), which later became the maximum-adjacency ordering of the Stoer–Wagner minimum-cut algorithm (J. ACM 44, 1997).

Timeline:

• 1927: Menger identifies the minimum number of edges separating two nodes with the maximum number of edge-disjoint paths between them.
• 1992: Nagamochi and Ibaraki publish Procedure FOREST and prove that its $i$-th prefix preserves local edge-connectivity up to $i$ in multigraphs, and local node-connectivity up to $i$ in simple graphs.
• 1993: Cheriyan, Kao and Thurimella (SIAM J. Comput. 22) obtain sparse certificates by scan-first search; Frank, Ibaraki and Nagamochi (J. Graph Theory 17) give a shorter proof for the node-connectivity case.
• 1994: Nishizeki and Poljak (Discrete Appl. Math. 55) publish the forest-decomposition lemma (Lemma 2.1 below), found independently.

Setting

A graph $G = (V, E)$ is finite and undirected, has $|V| \ge 2$ nodes, may have multiple edges (several edges with the same pair of end nodes), and has no self-loop. It is simple if no two edges have the same end nodes. For $F \subseteq E$, $(V, F)$ is the spanning subgraph with edge set $F$. It is a forest if it has no cycle; two parallel edges form a cycle. It is a maximal spanning forest in $(V, H)$, for $F \subseteq H$, if adding any edge of $H \setminus F$ to $F$ creates a cycle.

The local edge-connectivity $\lambda(x, y; H)$ is the minimum number of edges of $H$ whose removal leaves no path from $x$ to $y$; parallel edges count separately. It is $\infty$ when $x = y$.

Procedure FOREST keeps a label $r(v) \in \mathbb{N}$ on every node, initially $0$, and classes $E_1, E_2, \dots, E_{|E|}$, initially empty. While an unscanned node exists, it picks an unscanned node $x$ of largest label; for every unscanned edge $e$ from $x$ to a node $y$, it puts $e$ into $E_{r(y)+1}$, increases $r(x)$ by one if $r(x) = r(y)$, increases $r(y)$ by one, and marks $e$ scanned; then it marks $x$ scanned. Ties among nodes and the order of edges are free. On termination, $G_i = (V, E_1 \cup \cdots \cup E_i)$.

Formalization targets

Goal: Theorem 2.1 (pp. 588–589), without the running time

For every graph $G$ and every completed execution of FOREST on $G$:

1. every edge lies in exactly one class $E_i$, $1 \le i \le |E|$;
2. for $i = 1, \dots, |E|$,

$$\lambda(x, y; G_i) \ge \min\{\lambda(x, y; G),\ i\} \qquad \text{for all } x, y \in V; \tag{2.1}$$

3. $|E_i| \le |V| - 1$ for all $i$;
4. if $G$ is simple, $|E_i| \le |V| - i$ for $i \le |V| - 1$ and $E_i = \emptyset$ for $i \ge |V|$.

Milestones

• Lemma 2.2 (p. 587): during the execution, a node $v$ has incident edges in exactly the classes $E_1, \dots, E_{r(v)}$.
• Lemma 2.3 (p. 587): each $(V, E_i)$ is a forest at every instant.
• Lemma 2.4 (p. 588): (a) an edge $(u, v)$ added to $E_i$ has its end nodes joined by a path in $E_{i-1}$; (b) a path in $E_j$ between $u$ and $v$ yields a path in every $E_i$, $i < j$.
• Lemma 2.5 (p. 588): each output $(V, E_i)$ is a maximal spanning forest in $G - E_1 \cup \cdots \cup E_{i-1}$.
• Lemma 2.1 (p. 584): any sequence of successive maximal spanning forests satisfies (2.1).

Companions

• the sparse certificate (p. 589): if $\lambda(x, y; G) \ge k$ for all $x, y$, then $G_k$ is $k$-edge-connected with $|E(G_k)| \le k(|V| - 1)$, and $|E(G_k)| \le k|V| - k(k+1)/2$ for simple $G$;
• Lemma 2.6 (p. 589): for $k \le \delta(G)$, $G_k$ has a node of degree exactly $k$.

Significance

(2.1) says that one search produces, for every threshold $k$ at once, a subgraph with at most $k(|V|-1)$ edges that keeps every local edge-connectivity up to $k$. Any algorithm whose running time grows with $|E|$ can then be run on $G_k$ in place of $G$; §4 of the paper uses this to speed up $k$-connectivity tests and the computation of local connectivities. The same forest partition is the structural fact behind the Nagamochi–Ibaraki and Stoer–Wagner minimum-cut algorithms. Lemma 2.6 shows that the certificate is tight: its edge-connectivity is exactly $k$ when $\lambda(G) \ge k$.

The results are proved in the paper. No machine-checked proof of them is known. Formalizing them means formalizing a graph search with free tie-breaking as a transition system, reasoning about invariants of all its executions, and proving a cut-counting statement for multigraphs. Mathlib's connectivity notions, such as SimpleGraph.IsEdgeReachable, do not see parallel edges, so the multigraph cut theory here is new.

Difficulty

Lemma 2.1 is a short cut argument once maximality is available. The difficulty is showing that FOREST, which assigns each edge to a class by looking only at the label of one end node, produces maximal forests in the successive residual graphs (Lemma 2.5). The obvious invariant, that the class of an edge is the first forest it does not close a cycle in, is not what line 7 computes. The label $r(y)$ records only which classes touch $y$, not which component of each class contains $y$. The paper's argument needs Lemma 2.4(a): at the moment an edge is added to $E_i$ its ends already lie in one tree of $E_{i-1}$. That relies on the choice of the unscanned node of largest label, on the order of lines 8 and 9, and on an argument about the scan order of tree roots.

Formalization scope

• Graphs. A graph is a finite node type V with $|V| \ge 2$, a finite edge type E, and ends : E → Sym2 V with no diagonal value (no self-loops). Parallel edges are distinct elements of E. Simplicity is injectivity of ends, and edge subsets are Finset E. A forest is an edge set in which every edge is a bridge, a condition that sees parallel edges.
• Connectivity. $\lambda$ is an infimum in ℕ∞ over separating edge sets, $\infty$ at $x = y$. (2.1) is kept "for all $x, y$", as printed.
• FOREST. FOREST is a nondeterministic step relation (select, scan, finish) on explicit states: labels, class index per edge ($0$ = unscanned), scanned nodes, current node and selection order. The theorems quantify over every run from the initial state, so no tie-breaking rule is fixed. "At some time instant" is a state of the run; "upon completion" is a run whose last state has every node scanned. Lemma 2.2 is stated at every state, not only after a scan block (the other steps change neither labels nor classes). Lemma 2.4(a) assumes $i \ge 2$, since $E_0$ does not exist.
• Exclusions. Theorem 2.1's clause "is found in $O(|V| + |E|)$ time", the bucket implementation, and the time bound of the certificate are not formalized: the paper fixes no machine model. The goal consists of the structural conclusions only. The bound printed "if $G$ is multiple" is stated for every loopless graph.
• Non-triviality. The goal is about the classes of a run of FOREST. An arbitrary partition of $E$ into maximal spanning forests is Lemma 2.1's hypothesis, not a formalization of Theorem 2.1. A statement in which the classes are unconstrained variables, or in which the run hypotheses cannot be met, would be trivial. A separate sanity file checks that a complete run on the triangle $K_3$ exists and attains $|E_1| = |V| - 1$, $|E_2| = |V| - 2$.
• Welcome contributions. Useful reusable infrastructure includes:
  • a cut and Menger layer for finite multigraphs;
  • forest and bridge lemmas for edge-indexed graphs;
  • invariant-style reasoning over runs.

Selected references

• H. Nagamochi, T. Ibaraki, A linear-time algorithm for finding a sparse $k$-connected spanning subgraph of a $k$-connected graph, Algorithmica 7 (1992) 583–596. https://doi.org/10.1007/BF01758778
• H. Nagamochi, T. Ibaraki, Computing edge-connectivity in multigraphs and capacitated graphs, SIAM J. Discrete Math. 5 (1992) 54–66. https://doi.org/10.1137/0405004
• T. Nishizeki, S. Poljak, $k$-connectivity and decomposition of graphs into forests, Discrete Appl. Math. 55 (1994) 295–301. https://doi.org/10.1016/0166-218X(94)90014-0
• J. Cheriyan, M.-Y. Kao, R. Thurimella, Scan-first search and sparse certificates: an improved parallel algorithm for $k$-vertex connectivity, SIAM J. Comput. 22 (1993) 157–174. https://doi.org/10.1137/0222013
• A. Frank, T. Ibaraki, H. Nagamochi, On sparse subgraphs preserving connectivity properties, J. Graph Theory 17 (1993) 275–281. https://doi.org/10.1002/jgt.3190170302
• M. Stoer, F. Wagner, A simple min-cut algorithm, J. ACM 44 (1997) 585–591. https://doi.org/10.1145/263867.263872

Motivation

Boolean networks model gene regulatory networks by giving each gene an on/off value and updating all values synchronously by logical rules (Kauffman, 1969). Adding external Boolean inputs gives Boolean control networks (BCNs), in which a designer (a drug, an intervention) chooses the inputs over time. The basic control-theoretic question is controllability: can the inputs drive the network from any configuration to any other? Cheng and Qi (Automatica 2009) answered it for BCNs using the semi-tensor product of matrices, which rewrites a BCN as a linear recursion on canonical basis vectors.

Biological regulation is not instantaneous: transcription and translation introduce delays, so the next value of a gene can depend on several past values. Lu, Zhong, Ho, Tang and Cao (SIAM J. Control Optim. 2016) study delayed BCNs, in which the update reads the last $\mu$ states, and give criteria for two kinds of controllability, including the case where some configurations are dangerous and must be avoided (in biology, states corresponding to disease). The mission formalizes their criteria.

Setting

Write $\mathcal D=\{0,1\}$. A state is $x=(x_1,\dots,x_n)\in\mathcal D^n$ and an input value is $u\in\mathcal D^m$. Fix $\mu\ge1$. The delayed BCN (2.2) is

$$x_i(t+1)=f_i\big(u(t),x(t-\mu+1),\dots,x(t)\big),\qquad i=1,\dots,n,$$

with arbitrary Boolean functions $f_i:\mathcal D^{m+\mu n}\to\mathcal D$, collected into one map $F$ with $x(t+1)=F(u(t),X(t))$. A trajectory is the window $X(t)=(x(t-\mu+1),\dots,x(t))$ of the last $\mu$ states; its last entry is the current state. One step maps $X(t)$ under the input $u(t)$ to $X(t+1)=(x(t-\mu+2),\dots,x(t+1))$. A control sequence of length $k$ is $U=(u(0),\dots,u(k-1))$, with inputs chosen freely; $y(i)=X(i)$ denotes the trajectory after $i$ steps from an initial trajectory $y(0)$.

The transition-count matrix $Q$ has rows and columns indexed by trajectories: $Q_{b,a}$ is the number of input values $u$ taking trajectory $a$ to trajectory $b$ in one step. For a set $C_t$ of forbidden trajectories, $Q_{C_t}$ is $Q$ with the rows and columns of $C_t$ replaced by zeros, and $\mathbb Q_{C_t}$ is $Q$ with those rows and columns deleted.

The notions of controllability are:

• Trajectory controllable (Definition 3.1): from every initial trajectory, every trajectory $X_d$ equals $X(k)$ for some $k\ge1$ and some control sequence.
• Trajectory controllable under $C_t$ (Definition 3.11): for all trajectories $a,b\notin C_t$ there are $k\ge0$ and a control sequence steering $y(0)=a$ to $y(k)=b$ with $y(i)\notin C_t$ for $i=0,\dots,k$.
• State controllable (Definition 4.1): from every initial trajectory, every state equals $x(k)$ for some $k>0$ and some control sequence.

A real square matrix $A$ of size $N\ge2$ is reducible (Definition 3.7) if a simultaneous permutation of rows and columns brings it to block upper-triangular form $\begin{pmatrix}A_{11}&A_{12}\\0&A_{22}\end{pmatrix}$ with square diagonal blocks; it is irreducible otherwise, so every $1\times1$ matrix is irreducible.

$\mathbb N_1(k;y_a,y_b,C_t)$ counts the control sequences of length $k$ steering $y_a$ to $y_b$ while avoiding $C_t$; $\mathbb N_2(k;a,b_s)$ counts those steering the initial trajectory $a$ to $x(k)=b_s$; $\Xi^{p}_\mu$ is the set of trajectories with current state $p$.

Formalization targets

Goal: Theorem 3.12

$$\text{the delayed BCN is trajectory controllable under } C_t\iff \mathbb Q_{C_t}\ \text{is irreducible},$$

for every $\mu\ge1$, $n$, $m$, every update map and every forbidden set $C_t$. It is the most general criterion of the paper.

Milestones

• Proposition 3.5: for $k>0$, $\mathbb N_1(k;y_a,y_b,C_t)=y_b^{\mathsf T}(Q_{C_t})^ky_a$.
• Remark 3: $\mathbb N_1(k;y_a,y_b)=y_b^{\mathsf T}Q^ky_a$.
• Theorem 3.10: trajectory controllable $\iff$ $Q$ irreducible.
• Theorem 4.3: $\mathbb N_2(k;a,b_s)=\sum_{b\in\Xi^{b_s}_\mu}b^{\mathsf T}Q^ka$.
• Theorem 5.1: the same count while avoiding forbidden states $C_s$, with $Q$ zeroed on the trajectories containing a state of $C_s$.
• Corollary 5.3: trajectory controllability implies state controllability.

A supporting item, Lemma 3.9 (corrected form), relates Definition 3.7 to positivity of entries of powers for nonnegative matrices of size at least 2.

Significance

The criteria replace a question about control sequences of unbounded length by a finite test on one nonnegative integer matrix of size $2^{\mu n}$. The counting identities give more than a yes/no answer: they enumerate the control sequences achieving a transfer, which is what a designer choosing among interventions needs, and they handle forbidden states by passing to forbidden trajectories.

The results are proved in the paper; none of them has a machine-checked proof. Formalizing them yields a reusable Lean model of delayed (and, for $\mu=1$, ordinary) Boolean control networks defined directly through their dynamics, together with a checked bridge from dynamic reachability to the combinatorics of nonnegative matrices. A formal version also pins down points the printed text leaves loose: Lemma 3.9 as printed is false (it characterizes primitive, not irreducible, matrices), and the two different matrices $Q_{C_t}$ (zeroed) and $\mathbb Q_{C_t}$ (deleted) must not be confused.

Difficulty

The central step is the passage between three objects: reachability under the dynamics, positivity of entries of powers of $Q$, and the block-triangular definition of irreducibility. The counting identity for powers of $Q$ is a statement about sequences of inputs, not about paths in a graph, so the bijection between control sequences and weighted walks has to be established with the avoidance constraint carried at every intermediate time, including the endpoints. The equivalence between Definition 3.7 and strong connectivity is the classical graph-theoretic characterization, but it has edge cases the obvious argument misses: a $1\times1$ zero matrix is irreducible by Definition 3.7 yet has no positive power, which is exactly why Definition 3.11 allows $k=0$ while Definition 3.1 does not. A proof that routes through "some power of $\mathbb Q_{C_t}$ is entrywise positive", following the printed Lemma 3.9, proves a false intermediate statement.

Formalization scope

Conventions committed to in Lean:

• A state is Fin n → Bool (true is the paper's 1); a trajectory is Fin μ → State n with index 0 the oldest state and index $\mu-1$ the current state; $\mu\ge1$ is a standing assumption (NeZero μ); $n,m\ge0$ are arbitrary and no assumption is placed on the update functions.
• Matrices are indexed by trajectories rather than by the paper's index $j$ of $\delta^j_{2^{\mu n}}$. The paper's $Q=L\ltimes\mathbf 1_{2^m}$ is obtained by the simultaneous relabelling of Lemma 2.6, and every statement (entries of powers, sums over sets of trajectories, Definition 3.7) is invariant under it. $\mathbb Q_{C_t}$ is indexed by the subtype of allowed trajectories.
• Irreducibility is Definition 3.7 applied to the matrix with entries cast to $\mathbb R$; it is not Mathlib's Matrix.IsIrreducible, which differs on $1\times1$ matrices.
• Pinned readings: Definition 3.1 and Definition 4.1 use $k\ge1$; Definition 3.11 uses $k\ge0$; Proposition 3.5, Theorem 4.3 and Theorem 5.1 are stated for $k>0$ (Proposition 3.5 is false at $k=0$ when $y_a=y_b\in C_t$); Remark 3 holds for all $k\ge0$. "Avoiding $C_s$" in Theorem 5.1 means that no state $x(i)$, $i=1-\mu,\dots,k$, lies in $C_s$, which is the theorem's own middle term $\mathbb N_1(k;a,b,\Xi^{C_s})$. $\Xi^p_\mu$ is defined semantically by eq. (4.3), since the printed index range in (4.4) is a misprint. Lemma 3.9 is included in corrected form with $N\ge2$.

Controllability is defined through the dynamics and control sequences, never as positivity of entries of powers of $Q$; a formalization that defines reachability by $(Q^k)_{b,a}>0$ would reduce Theorems 3.10 and 3.12 to library facts and is ruled out.

Needed infrastructure: the correspondence between control sequences and products of entries of $Q$ (the core of Proposition 3.5), and the equivalence of Definition 3.7 with strong connectivity of the support graph for nonnegative matrices (Mathlib's Matrix.IsIrreducible, Matrix.isIrreducible_iff_exists_pow_pos and Matrix.pow_apply_pos_iff_nonempty_path cover much of the second part for sizes at least 2). Both are reusable beyond this mission, for ordinary BCNs, probabilistic BCNs and finite automata. Contributions of either piece, or of the semi-tensor-product bridge identifying $Q$ with $L\ltimes\mathbf 1_{2^m}$, are welcome.

Selected references

• J. Lu, J. Zhong, D. W. C. Ho, Y. Tang, J. Cao, On Controllability of Delayed Boolean Control Networks, SIAM J. Control Optim. 54(2):475–494, 2016. https://doi.org/10.1137/140991820
• D. Cheng, H. Qi, Controllability and observability of Boolean control networks, Automatica 45(7):1659–1667, 2009. https://doi.org/10.1016/j.automatica.2009.03.006
• S. A. Kauffman, Metabolic stability and epigenesis in randomly constructed genetic nets, J. Theoret. Biol. 22(3):437–467, 1969. https://doi.org/10.1016/0022-5193(69)90015-0
• A. Berman, R. J. Plemmons, Nonnegative Matrices in the Mathematical Sciences, SIAM Classics in Applied Mathematics 9, 1994. https://doi.org/10.1137/1.9781611971262

Motivation

Clique-width is a graph parameter introduced by Courcelle and Olariu (Discrete Appl. Math. 101 (2000)) that measures how far a graph is from being built by a few labelled operations. Every problem expressible in monadic second-order logic with quantification over vertices and vertex sets (MSO$_1$) can be solved in linear time on graphs given together with a decomposition of bounded clique-width (Courcelle, Makowsky and Rotics, Theory Comput. Syst. 33 (2000)). Bounded clique-width is more general than bounded tree-width: complete graphs have unbounded tree-width but clique-width $2$.

For fixed $k$ there was, before this paper, no polynomial-time algorithm that either decides that a graph has clique-width at least $k+1$ or outputs a decomposition of clique-width bounded by a function of $k$; the best known algorithm, by Johansson (2001), gave width $2k\log n$. Oum and Seymour (J. Combin. Theory Ser. B 96 (2006)) closed this gap with approximation $2^{3k+2}-1$, through rank-width and a factor-3 approximation for the branch-width of symmetric submodular functions.

Timeline:

• 1991: Robertson and Seymour introduce branch-width of graphs and hypergraphs (J. Combin. Theory Ser. B 52).
• 2000: Courcelle and Olariu define clique-width; Courcelle, Makowsky and Rotics solve MSO$_1$ problems on graphs given with a $k$-expression.
• 2001: Johansson gives a $2k\log n$ approximation.
• 2006: Oum and Seymour define rank-width, prove $\mathrm{rwd}(G) \le \mathrm{cwd}(G) \le 2^{\mathrm{rwd}(G)+1}-1$, and give an $O(n^9 \log n)$ algorithm that outputs a $(2^{3k+2}-1)$-expression or certifies clique-width above $k$.

Setting

All graphs are finite and simple. For a finite set $V$, a function $f : 2^V \to \mathbb{Z}$ is submodular if $f(X)+f(Y) \ge f(X\cap Y)+f(X\cup Y)$ and symmetric if $f(X) = f(V\setminus X)$.

A branch-decomposition of $f$ is a pair $(T, L)$ where $T$ is a tree with at least two vertices and all degrees at most $3$, and $L$ is a bijection from $V$ onto the leaves of $T$. Removing an edge $e$ of $T$ splits the leaves in two; the width of $e$ is $f$ of the set of elements of $V$ on one side. The width of $(T, L)$ is the largest edge width, and the branch-width $\mathrm{bw}(f)$ is the least width of a branch-decomposition, with $\mathrm{bw}(f) = f(\emptyset)$ when $|V| \le 1$.

A set $W \subseteq V$ is well-linked with respect to $f$ if for every partition $(X, Y)$ of $W$ and every $Z$ with $X \subseteq Z \subseteq V\setminus Y$, $f(Z) \ge \min(|X|, |Y|)$.

Let $A(G)$ be the adjacency matrix of $G$ over $\mathrm{GF}(2)$. For disjoint $X, Y \subseteq V(G)$, $\mathrm{cutrk}^*_G(X, Y)$ is the rank of the submatrix of $A(G)$ with rows $X$ and columns $Y$, and the cut-rank function is $\mathrm{cutrk}_G(X) = \mathrm{cutrk}^*_G(X, V(G)\setminus X)$. The rank-width $\mathrm{rwd}(G)$ is $\mathrm{bw}(\mathrm{cutrk}_G)$.

A $k$-expression is a term built from constants $\cdot_i$ (a vertex with label $i \in \{1,\dots,k\}$), the operators $\eta_{i,j}$ ($i \ne j$; add all edges between labels $i$ and $j$), $\rho_{i\to j}$ (relabel $i$ into $j$) and disjoint union $\oplus$. Its value is the labelled graph it produces; $G$ has clique-width $\mathrm{cwd}(G) \le k$ if some $k$-expression has value isomorphic to $G$.

An interpolation of $f$ is a function $f^*$ on disjoint pairs $(X, Y)$ that agrees with $f$ on $(X, V\setminus X)$, is monotone, submodular in the sense $f^*(A,B)+f^*(C,D) \ge f^*(A\cap C, B\cup D) + f^*(A\cup C, B\cap D)$, and has $f^*(\emptyset,\emptyset)=f(\emptyset)$.

Formalization targets

Goal: Theorem 1.1, certificate form

For a graph $G$ with at least one vertex and an integer $k \ge 1$:

$$\exists\, W,\ |W| = 3k+1,\ W \text{ well-linked for } \mathrm{cutrk}_G \;\Longrightarrow\; \mathrm{cwd}(G) \ge k+1,$$ $$\nexists\, W,\ |W| = 3k+1,\ W \text{ well-linked for } \mathrm{cutrk}_G \;\Longrightarrow\; \mathrm{cwd}(G) \le 2^{3k+2}-1.$$

The same explicit condition decides which side of the approximation holds; this is what the paper's algorithm certifies.

Milestones

1. Proposition 4.1: properties of an interpolation, including that $X \mapsto f^*(X, B) - f(\emptyset)$ is a matroid rank function on $V\setminus B$ when $f(\{v\}) - f(\emptyset) \le 1$.
2. Proposition 4.2: $f_{\min}(X,Y) = \min_{X\subseteq Z\subseteq V\setminus Y} f(Z)$ is an interpolation.
3. Theorem 5.1: a well-linked set of size $k$ forces $\mathrm{bw}(f) \ge k/3$ (for $k \ne 1$).
4. Theorem 5.2: no well-linked set of size $k$ implies $\mathrm{bw}(f) \le k$, when $f(\{v\}) \le 1$.
5. Proposition 6.1: $\mathrm{rk}\,M[X_1,Y_1] + \mathrm{rk}\,M[X_2,Y_2] \ge \mathrm{rk}\,M[X_1\cup X_2, Y_1\cap Y_2] + \mathrm{rk}\,M[X_1\cap X_2, Y_1\cup Y_2]$.
6. Corollary 6.2: submodularity of $\mathrm{cutrk}^*_G$ and $\mathrm{cutrk}_G$.
7. Section 6 claim: $\mathrm{cutrk}_G$ is symmetric submodular and $\mathrm{cutrk}^*_G$ interpolates it.
8. Proposition 6.3: $\mathrm{rwd}(G) \le \mathrm{cwd}(G) \le 2^{\mathrm{rwd}(G)+1}-1$.

Significance

The dichotomy turns clique-width, for which no exact polynomial algorithm is known even for fixed $k$, into a parameter that can be approximated with an explicit witness in each direction. Downstream, every algorithm for graphs of bounded clique-width that needs a $k$-expression as input becomes applicable to graphs given without one, at the cost of an exponential blow-up of the width.

The result is proved in the literature; this mission formalizes it. To our knowledge none of the objects involved — branch-width of set functions, rank-width, cut-rank, $k$-expressions, clique-width — has been formalized in Mathlib, and the submodularity of submatrix rank (Proposition 6.1) is absent from Mathlib's Matrix.rank API. The formal development would give reusable definitions of branch-decompositions of arbitrary integer set functions, of cut-rank, and of clique-width, and a machine-checked link between the combinatorial and the linear-algebraic width parameters.

Difficulty

The upper bound in Theorem 5.2 is the core. The natural approach, growing a branch-decomposition one leaf split at a time while keeping the width at most $k$, gets stuck at a leaf carrying a set $B$ with $f(B) = k$: a split of $B$ into two parts of $f$-value below $k$ has to be found, and it must be found from the failure of well-linkedness of a set that is not obviously related to $B$. The paper's device is the interpolation $f^*$, which attaches a matroid to $B$ whose base has exactly $f(B)$ elements. Formalizing this requires handling partial branch-decompositions, their extensions, and a maximality argument over trees, none of which exists in Mathlib.

Proposition 6.3's upper bound is a second, independent difficulty: a rank-decomposition must be converted into a $k$-expression by an induction over a rooted binary tree, with a relabelling argument bounding the number of labels by the number of distinct nonzero rows of a $\mathrm{GF}(2)$ matrix of rank $k$. Its lower bound needs the tree structure of a $k$-expression to be read as a branch-decomposition.

Formalization scope

The ground set is a Fintype V with DecidableEq V; subsets are Finset V; set functions are Finset V → ℤ, as in the paper. A branch-decomposition is a tree T : SimpleGraph (Fin n) with $n \ge 2$, all neighbour sets of size at most $3$, and an injective map $L$ from $V$ onto the vertices of degree $1$; the side of an edge $uw$ is found by reachability from $u$ after deleting $uw$. Branch-width, rank-width and clique-width are never computed as minima: "$\mathrm{bw}(f) \le k$" is the predicate "$|V| \le 1$ and $f(\emptyset) \le k$, or a branch-decomposition of width at most $k$ exists", lower bounds say that every branch-decomposition has a wide edge, and "$\mathrm{cwd}(G) \le k$" is "$G$ has a $k$-expression". Labels $\{1,\dots,k\}$ are Fin k. The value of a $k$-expression has as vertex type the occurrences of constants (a nested sum type), and $\eta_{i,j}$ requires $i \ne j$. Cut-rank uses Matrix.rank over ZMod 2 of submatrices of SimpleGraph.adjMatrix. An interpolation is a function on all pairs of subsets whose axioms are imposed on disjoint pairs only.

Running time is not formalized. The paper's Theorem 1.1 asserts an $O(n^9\log n)$ algorithm; there is no cost model on the page, and the goal states the certificate the algorithm returns instead. Without the running time, "$\mathrm{cwd}(G) \ge k+1$ or $\mathrm{cwd}(G) \le 2^{3k+2}-1$" holds for every graph, so that reading is ruled out as a formalization of the goal; so are well-linkedness with respect to anything other than $\mathrm{cutrk}_G$, widths defined by an unguarded infimum (which is $0$ on an empty family), $k$-expressions whose value is not the graph up to isomorphism or whose $\eta$ may join equal labels, and Theorem 5.1 stated for $k = 1$.

Correction of Theorem 5.1. As printed, Theorem 5.1 fails for $k = 1$: a singleton is always well-linked, but the edgeless graph on two vertices has cut-rank identically $0$ and branch-width $0 < 1/3$. The milestone carries the hypothesis $k \ne 1$; the goal uses the theorem only at size $3k+1 \ge 4$.

The graph with no vertex is excluded from the goal and from the upper bound of Proposition 6.3, since it has no $k$-expression for any $k$. Contributions welcome: proofs of the milestones, lemmas on branch-decompositions (suppressing degree-2 vertices, extending partial decompositions), and submatrix-rank submodularity, which is reusable beyond this mission.

Selected references

• S. Oum and P. 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
• B. Courcelle and S. Olariu, Upper bounds to the clique width of graphs, Discrete Appl. Math. 101 (2000) 77–114. https://doi.org/10.1016/S0166-218X(99)00184-5
• B. Courcelle, J. A. Makowsky and U. Rotics, Linear time solvable optimization problems on graphs of bounded clique-width, Theory Comput. Syst. 33 (2000) 125–150. https://doi.org/10.1007/s002249910009
• N. Robertson and 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