Graph Theory

Motivation

The circumference $c(G)$ of a graph $G$ is the length of a longest cycle. Extremal graph theory asks how many edges force a long cycle. The Erdős–Gallai theorem (1959) states that every $n$-vertex graph has at most $c(G)(n-1)/2$ edges. Bondy (1971) strengthened it by counting only the edges near a longest cycle: if $C$ is a longest cycle of length $c$, the number of edges with at most one endpoint in $C$ is at most $\tfrac c2(n-c)$, and at most $\lfloor c/2\rfloor (n-c)$ when $G$ is 2-connected. Since $V(C)$ spans at most $\binom c2$ edges, this implies the Erdős–Gallai bound.

A stability result complements an extremal one: a graph close to the extremal bound must be close in structure to the extremal graphs. Jie Ma and Bo Ning (Combinatorica, 2020; arXiv:1708.00704) proved stability versions of Kopylov's edge theorem for 2-connected graphs of given circumference and of Bondy's theorem above. This mission formalizes their stability version of Bondy's theorem, Theorem 1.12. In the paper it is also one of the two halves of the proof of the main stability theorem; the other half is a separate mission in this series.

Timeline (as recorded in §1 of the paper). Dirac (1952): every 2-connected graph has $c(G)\ge\min\{2\delta(G),|V(G)|\}$. Erdős and Gallai (1959): $e(G)\le c(G)(n-1)/2$. Bondy (1971): the bound on edges with at most one endpoint on a longest cycle, and the degree theorem stated here as Theorem 2.1. Woodall (1976): $e(G)\le f(n,\lfloor c/2\rfloor,c)$ for 2-connected $G$ with circumference $c\le(2n+2)/3$. Kopylov (1977): $e(G)\le\max\{f(n,2,c),f(n,\lfloor c/2\rfloor,c)\}$ for 2-connected $G$ with circumference $c\le n-1$; another proof by Fan, Lv and Wang (2004). Fan (1990): an improved version of Bondy's bound for 2-connected graphs, and average-degree bounds on long paths. Füredi, Kostochka and Verstraëte (2016): stability for Kopylov's theorem when $n\ge 3\lfloor c/2\rfloor$; Füredi, Kostochka, Luo and Verstraëte (2018): the complete stability version, with the families $\mathcal X_{n,c}$, $\mathcal Y_{n,c}$. Ma and Ning (2017 preprint, 2020): the results of this mission.

Setting

All graphs are finite and simple, on the vertex set $\{0,\dots,n-1\}$. A path or cycle of length $k$ has $k$ edges. A graph is 2-connected if it has at least three vertices, is connected, and remains connected after deleting any one vertex. A cycle $C$ is a longest cycle if no cycle of $G$ has more edges; $V(C)$ is its vertex set and $c$ its length.

For a longest cycle $C$, write $e(G-C)+e(G-C,C)$ for the number of edges with at most one endpoint in $C$. A vertex $u$ is an isolated vertex of $G-C$ if $u\notin V(C)$ and every neighbour of $u$ lies on $C$; $d_C(u)$ is its number of neighbours on $C$.

The extremal graphs are:

• $W_{n,k,c}$: a clique $K_{c-k+1}$ together with $n-(c-k+1)$ further vertices, each adjacent to the same $k$ vertices of the clique and to nothing else.
• $\mathcal X_{n,c}$: graphs on $A\cup B\cup X$ with $A$ a clique of size $\lfloor c/2\rfloor$, $B$ and $X$ stable, $A$ completely joined to $B$, and two vertices $a\in A$, $b\in B$ such that $N(x)=\{a,b\}$ for all $x\in X$.
• $\mathcal Y_{n,c}$: graphs on $A\cup B\cup Y$ with $A$ a clique of size $\lfloor c/2\rfloor$, $B$ stable, $A$ completely joined to $B$, $G[Y]$ a star forest with at least two stars each having an edge, and two distinct $a,b\in A$ such that each star $S$ has exactly $\{a,b\}$ as outside neighbourhood and, if $|V(S)|\ge 3$, its leaves have degree $2$ and a common neighbour in $\{a,b\}$.

$G\subseteq W$ means that $G$ is isomorphic to a subgraph of $W$.

Formalization targets

Goal: Theorem 1.12

Let $G$ be 2-connected on $n$ vertices and $C$ a longest cycle of length $c$ with $10\le c\le n-1$. If

$$e(G-C)+e(G-C,C) > \left(\left\lfloor \tfrac c2\right\rfloor-1\right)(n-c),$$

then $G\subseteq W_{n,\lfloor c/2\rfloor,c}$, or $c$ is odd and $G$ is a subgraph of a member of $\mathcal X_{n,c}\cup\mathcal Y_{n,c}$.

Milestones

1. Theorem 2.1 (Bondy): all but one vertex of degree $\ge k$ in a 2-connected graph give $c(G)\ge\min\{n,2k\}$.
2. Theorem 2.2 (Fan), first assertion: a longest $(x,y)$-path is at least as long as the average degree of the other vertices.
3. Lemma 2.3: a 2-connected component $H$ of $G-C$ with average degree $r$ satisfies $c\ge 2r$, with equality only for a clique attached to two common vertices of $C$.
4. Theorem 3.2: without connectivity and for $4\le c\le n-1$, the same edge condition gives $c\in\{6,7,9\}$, or a vertex off $C$ with $\lfloor c/2\rfloor$ neighbours on $C$, or a cycle $C'$ meeting $C$ in at most one vertex with $|C'|\ge 2\lfloor c/2\rfloor-3$ (disjoint) or $\ge 2\lfloor c/2\rfloor-1$ (one common vertex).
5. Theorem 3.1: for 2-connected $G$ and $10\le c\le n-1$, an isolated vertex $u$ of $G-C$ with $d_C(u)=\lfloor c/2\rfloor$.
6. Lemma 3.3: such a vertex forces $G\subseteq W_{n,\lfloor c/2\rfloor,c}$ when $c$ is even, and $G\subseteq W_{n,\lfloor c/2\rfloor,c}$ or $G$ in a member of $\mathcal X_{n,c}\cup\mathcal Y_{n,c}$ when $c\ge 9$ is odd.

Significance

In $W_{n,\lfloor c/2\rfloor,c}$ every one of the $n-c$ vertices off a longest cycle sends $\lfloor c/2\rfloor$ edges to the cycle, so Bondy's bound $\lfloor c/2\rfloor(n-c)$ is attained. Theorem 1.12 says that exceeding $(\lfloor c/2\rfloor-1)(n-c)$ already leaves only three structures: a subgraph of $W_{n,\lfloor c/2\rfloor,c}$, or for odd $c$ a subgraph of a member of $\mathcal X_{n,c}$ or $\mathcal Y_{n,c}$. In the paper it is one of the two cases of the proof of the main stability theorem (Theorem 1.9): a graph with many edges and a longest cycle $C$ has either many edges with at most one endpoint on $C$, handled here, or many edges inside $V(C)$, handled by the closure argument of the companion mission.

The result is proved in the paper; none of it, nor Bondy's or Fan's theorems, is formalized on the platform or in Mathlib. The mission produces machine-checked statements of the goal, of the cited tools (Bondy's Theorem 2.1, Fan's Theorem 2.2, Lemma 2.3), and of the steps Theorems 3.1, 3.2 and Lemma 3.3, together with reusable definitions of 2-connectivity, longest cycles and the extremal families.

Difficulty

The obvious approach counts edges at the vertices off $C$: each such vertex has at most $\lfloor c/2\rfloor$ neighbours on $C$, since otherwise two consecutive cycle vertices would let the cycle be extended. This bound is far from enough. The edge count also includes edges between vertices off $C$, and components of $G-C$ can be large, 2-connected, and attached to $C$ in complicated ways. The bound $(\lfloor c/2\rfloor-1)(n-c)$ has to be beaten by every such configuration at once, and Theorem 3.2 states exceptional small cycle lengths $c\in\{6,7,9\}$ for which the analysis does not close. A second difficulty is the passage from one vertex of degree $\lfloor c/2\rfloor$ to a global description of $G$: in the odd case, the structure of every component of $G-C$ has to be determined, which is where the families $\mathcal X_{n,c}$ and $\mathcal Y_{n,c}$ appear.

Formalization scope

Graphs are SimpleGraph (Fin n) with decidable adjacency. A cycle is a closed walk C : G.Walk u u with C.IsCycle; its length is C.length and its vertex set C.support.toFinset. "Longest cycle" is the predicate that every cycle of $G$ is at most as long as $C$; no supremum of cycle lengths is used. 2-connectivity is: at least three vertices, connected, and connected after deleting any one vertex. It is stated for an arbitrary finite vertex type so that it applies to the induced subgraph $G[H]$ in Lemma 2.3. The edge count off $C$ is the number of edges with an endpoint outside $V(C)$, and $\lfloor c/2\rfloor$ is natural-number division; under the stated bounds every natural-number subtraction is exact.

$W_{n,k,c}$ is defined on fixed labels (clique $\{0,\dots,c-k\}$, hubs $\{0,\dots,k-1\}$), and "$G\subseteq W$" is a graph embedding G ⊑ W. Membership in $\mathcal X_{n,c}$ and $\mathcal Y_{n,c}$ are predicates on labelled graphs, closed under relabelling, and "$G$ is a subgraph of a member" is G ≤ H for some member $H$. No hypothesis is added to any statement. Fan's Theorem 2.2 is stated without its equality characterization.

Trivializing formalizations are ruled out explicitly: the alternative "$c$ is odd and …" is a conjunction, never an implication; the circumference is never a junk supremum; containment in $W$ is up to isomorphism, never ≤ on fixed labels; and 2-connectivity excludes $K_2$ and disconnected graphs.

The definitions are reusable for any work on circumference, longest cycles and Bondy–Erdős–Gallai-type problems. Contributions of proofs of the cited tools (Bondy's and Fan's theorems) are especially welcome, as is a proof of Erdős–Gallai's edge theorem, which the proof of Theorem 3.2 uses and which is posed elsewhere on the platform.

Selected references

• J. Ma and B. Ning, Stability results on the circumference of a graph, Combinatorica 40 (2020); arXiv:1708.00704v2. https://arxiv.org/abs/1708.00704 , https://doi.org/10.1007/s00493-019-3843-4
• J. A. Bondy, Large cycles in graphs, Discrete Mathematics 1 (1971/72), no. 2, 121–132.
• G. Fan, Long cycles and the codiameter of a graph, I, Journal of Combinatorial Theory, Series B 49 (1990) 151–180.
• P. Erdős and T. Gallai, On maximal paths and circuits of graphs, Acta Mathematica Academiae Scientiarum Hungaricae 10 (1959) 337–356.
• G. Fan, X. Lv, P. Wang, Cycles in 2-connected graphs, Journal of Combinatorial Theory, Series B 92 (2004) 379–394.
• Z. Füredi, A. Kostochka, J. Verstraëte, Stability in the Erdős–Gallai theorems on cycles and paths, Journal of Combinatorial Theory, Series B 121 (2016) 197–228.
• Z. Füredi, A. Kostochka, R. Luo, J. Verstraëte, Stability in the Erdős–Gallai theorem on cycles and paths, II, Discrete Mathematics 341 (2018) 1253–1263.
• G. N. Kopylov, Maximal paths and cycles in a graph, Soviet Mathematics Doklady 18 (1977) 593–596.
• D. R. Woodall, Maximal circuits of graphs I, Acta Mathematica Academiae Scientiarum Hungaricae 28 (1976) 77–80.

Motivation

Mean field games describe Nash equilibria of large populations in which every player interacts with every other player symmetrically, through the empirical distribution of all states. Many systems of interest are not of this kind: agents in a network interact only with their neighbours, and the interaction structure is a graph rather than a complete graph. Understanding when equilibria on large graphs behave like mean field equilibria, and when they do not, requires models in which the equilibrium on a finite graph can be computed exactly.

Lacker and Soret (arXiv:2005.14102v2, Math. Oper. Res. 2022) introduced such a model: a linear–quadratic flocking game on an arbitrary finite graph, in which each player steers a Brownian particle and pays a terminal penalty for being far from the average of her neighbours. For vertex-transitive graphs they solved the game in closed form, up to a scalar ODE, with an equilibrium that depends on the graph only through the spectrum of its Laplacian. This mission formalizes that finite-graph result, Theorem 2.5 of the paper. Its large-graph consequences are the subject of missions II and III of this series.

Setting

Let $G$ be a finite simple graph on vertices $V=\{1,\dots,n\}$, with adjacency matrix $A_G$ and degree matrix $D_G$. When $G$ has no isolated vertices its random-walk Laplacian is

$$L_G := D_G^{-1}A_G - I .$$

$G$ is transitive if for every two vertices $u,v$ there is a graph automorphism mapping $u$ to $v$. A transitive graph is regular, so its Laplacian $L_G = A_G/\delta(G) - I$ is symmetric, with eigenvalues in $[-2,0]$.

Fix a horizon $T>0$, a noise level $\sigma>0$ and a cost constant $c>0$. Each vertex $v$ is a player with state

$$dX_v(t) = \alpha_v(t,X(t))\,dt + \sigma\,dW_v(t),\qquad t\in[0,T],$$

driven by independent Brownian motions $W_v$, from a non-random initial state $X(0)=x_0\in\mathbb R^V$. A Markovian control $\alpha_v$ is a Borel function of time and the full state vector with at most linear growth. Player $v$ minimises

$$J_v = \tfrac12\,\mathbb E\Big[\int_0^T|\alpha_v(t,X(t))|^2\,dt + c\,\Big|X_v(T)-\frac{1}{\deg(v)}\sum_{u\sim v}X_u(T)\Big|^2\Big].$$

A profile $(\alpha_v)_v$ is a Markovian Nash equilibrium if no player can lower her cost by switching unilaterally to another Markovian control.

The equilibrium is built from

$$Q_G(x) := \det(I-xL_G)^{1/n},\qquad f_G'(t) = c\,Q_G'(f_G(t)),\ f_G(0)=0,$$ $$P_G(t) := -f_G'(T-t)\,L_G\big(I-f_G(T-t)L_G\big)^{-1},\qquad \alpha^G_i(t,x) := -e_i^\top P_G(t)x .$$

Formalization targets

Goal: Theorem 2.5

For a finite transitive graph $G$ without isolated vertices:

1. $Q_G$ is well defined and continuously differentiable on $\mathbb R_+$, and the ODE has a unique solution $f_G:[0,T]\to\mathbb R_+$.
2. $(\alpha^G_i)_i$ is a Markovian Nash equilibrium for every initial state.
3. For every $t\in(0,T]$, the equilibrium state $X(t)$ is Gaussian with

$$\mathbb E X(t) = (I-f_G(T-t)L_G)(I-f_G(T)L_G)^{-1}x_0,\qquad \mathrm{Cov}\,X(t) = \sigma^2(I-f_G(T-t)L_G)^2\int_0^t(I-f_G(T-s)L_G)^{-2}\,ds .$$

4. The average equilibrium cost satisfies

$$\frac1n\sum_{v}J_v = \frac{|P_G(0)x_0|^2}{2\,\mathrm{Tr}\,P_G(0)} - \frac{\sigma^2}{2}\log\frac{\mathrm{Tr}\,P_G(0)}{n\,f_G'(T)} .$$

All four parts are in the goal statement.

Milestones

The milestones follow the paper's proof in §2.2, §3 and §4.

• Graph-spectral facts. Transitive graphs are regular with symmetric $L_G$ (§2.2). The spectrum of $L_G$ lies in $[-2,0]$ (Remark 2.4). The eigenvalue distribution $\mu_G$ has mean $-1$ ((3.2)), and $Q_G = Q_{\mu_G}$ (§2.3).
• The ODE. Bounds on $Q_\mu$ and its first two derivatives (Proposition 3.1), and well-posedness of $f_\mu' = cQ_\mu'(f_\mu)$ with explicit bounds (Proposition 3.2).
• Symmetry. Commutation of $L_G$ with automorphism matrices, and constancy of the diagonal of equivariant matrices (Lemma 4.1).
• The Riccati system. The properties of $P_G(t)$ (§4.4 (i)–(iii)), the reduction of the Nash PDE system to matrix Riccati equations (Lemma 4.2), and the verification that the explicit $F^i = (\mathrm{Tr}\,P/n)^{-1}Pe_ie_i^\top P$ solve them (§4.4).
• Law and value. The fundamental matrix $\exp(-\int_s^tP) = (I-f(T-t)L)(I-f(T-s)L)^{-1}$ (§4.5) and the averaged value identity (§4.6).

Significance

The result. Theorem 2.5 is one of the few explicit Nash equilibria of a stochastic differential game on a non-complete graph. Two features of it are not visible in mean field theory. The equilibrium controls are nonlocal: each player reacts to the whole state vector, not only to her neighbours. The whole equilibrium (law, value, controls) depends on the graph only through the spectrum of $L_G$. The second feature drives the paper's later results. Weak convergence of the eigenvalue distributions $\mu_{G_n}$ yields limits of the equilibrium, and these separate the dense regime, where the mean field approximation is valid, from the sparse regime, where it is not.

Formalizing it. The result is proved in the paper; nothing here is open. No machine-checked version of it or of its ingredients exists: the random-walk Laplacian of a graph, linear–quadratic stochastic differential games, verification theorems for Nash systems, and Gaussian laws of linear SDEs with time-dependent coefficients. The mission produces a checked statement of the equilibrium together with reusable layers: spectral facts about $D^{-1}A - I$, an ODE analysis for $Q_\mu$, and a Riccati reduction for quadratic Nash systems.

Difficulty

Three steps resist a direct approach.

• The verification theorem. The paper passes from a classical solution of the Nash system (4.1) to a Nash equilibrium by appeal to a standard verification argument. Over the full class of Borel controls with linear growth, this requires Itô's formula for the quadratic value functions, together with integrability of the deviated state processes.
• The Riccati system. The $n$ coupled matrix equations (4.6) have no general closed-form solution. The explicit solution exists only because transitivity forces $e_i^\top P(t)e_i = \mathrm{Tr}(P(t))/n$ for every $i$. That identity has to be derived from the action of the automorphism group (Lemma 4.1), not from regularity alone.
• The law of the state. It requires solving a linear SDE with a time-dependent matrix and identifying its Gaussian law, a step for which the library has little support.

Formalization scope

Lean conventions:

• Vertices. The vertex set is Fin n, so the paper's $1,\dots,n$ become $0,\dots,n-1$. The state space is the platform's EthierKurtz.SDEState n (Euclidean $\mathbb R^n$).
• The Laplacian. $L_G$ is the random-walk Laplacian $D^{-1}A-I$, not Mathlib's $D-A$.
• Time and controls. Time is real. Controls are Borel on $\mathbb R\times\mathbb R^n$ with linear growth on $[0,T]$; their values off $[0,T]$ are never used.
• Solutions of (2.1). A solution is a pathwise strong solution on a probability space that the solution itself carries, adapted to the completed Brownian filtration. Costs are compared across solutions; this is faithful because (2.1) has a unique strong solution.
• Costs are $[0,\infty]$-valued lower Lebesgue integrals. They are converted to reals only after their finiteness is asserted.
• Existence of the equilibrium state. The goal also asserts that the equilibrium state equation has a solution, so that the Nash property cannot hold vacuously.
• Derivatives. $f_G'(T-t)$ is written as its ODE value $cQ_G'(f_G(T-t))$. The ODE is solved on $[0,T]$ with one-sided derivatives at the endpoints, and uniqueness is agreement on $[0,T]$.
• Matrix conventions. Covariance integrals are entrywise. Gaussian laws are Mathlib's multivariateGaussian.
• Added hypotheses. $0<n$ is added to three milestones that are false on the empty graph.

A formalization that fixes $x_0=0$, restricts deviations to linear controls, drops the existence of the equilibrium state process, or replaces $L_G$ by $D-A$ is not this theorem.

Infrastructure that a complete development needs:

• symmetric-matrix spectral calculus for $L_G$ and for the matrix functions $(I-xL)^{-1}$ and $\log(I-xL)$;
• differentiation under the integral for $Q_\mu$;
• Picard–Lindelöf and Grönwall on $\mathbb R_+$;
• Itô's formula for quadratic functions of a diffusion with additive noise;
• the Gaussian law of $\int_0^t M(t,s)\,dW_s$ for deterministic $M$.

The spectral, ODE and Riccati layers are reusable beyond this mission. Proofs of individual milestones are welcome; so are general verification theorems for linear–quadratic games.

Selected references

• D. Lacker, A. Soret, A case study on stochastic games on large graphs in mean field and sparse regimes, arXiv:2005.14102v2, 2021; Math. Oper. Res. 47(2), 2022. https://arxiv.org/abs/2005.14102
• F. Chung, Spectral Graph Theory, CBMS Regional Conference Series in Mathematics 92, AMS, 1997. https://doi.org/10.1090/cbms/092
• R. Carmona, F. Delarue, Probabilistic Theory of Mean Field Games with Applications I, Springer, 2018. https://doi.org/10.1007/978-3-319-58920-6
• A. Veretennikov, On strong solutions and explicit formulas for solutions of stochastic integral equations, Math. USSR-Sb. 39(3), 1981. https://doi.org/10.1070/SM1981v039n03ABEH001522

Distributed optimization over directed, changing networks

In distributed optimization, $n$ agents cooperatively minimize the average $f(x)=\frac1n\sum_{i=1}^n f_i(x)$ of private cost functions $f_i:\mathbb R^p\to\mathbb R$, exchanging information only with their current neighbours in a communication network. The model covers sensor networks, multi-robot coordination and machine learning with data split across machines, where no node can see the whole objective. In many of these systems communication is one-directional (broadcast radios with unequal ranges, asymmetric links) and the network changes over time.

Directed links raise a specific obstacle: a node cannot in general choose weights that are both row and column stochastic, because it knows its out-degree but not how its messages are combined by others. The push-sum (ratio consensus) protocol of Kempe, Dobra and Gehrke (2003) circumvents this with column stochastic weights and a scalar correction. Nedić and Olshevsky (2015) combined it with diminishing-step subgradient methods over time-varying directed graphs, obtaining sublinear rates. Gradient tracking methods (Xu, Zhu, Soh and Xie, 2015; Qu and Li, 2016) and EXTRA (Shi, Ling, Wu and Yin, 2015) reached linear rates with constant steps on undirected or static graphs. Nedić, Olshevsky and Shi (arXiv 2016, SIAM J. Optim. 2017) proved geometric convergence of gradient tracking over graphs that are both time-varying and directed; this mission formalizes that result.

Setting

The agents are $\{1,\dots,n\}$. At each time $k$ there is a set $\mathcal A(k)$ of arcs; an arc $j\to i$ means agent $j$ can send to agent $i$. The out-degree $d^{\rm out}_j(k)$ counts the agents $i\ne j$ with $j\to i$ in $\mathcal A(k)$.

Assumption 6. There is $\tilde B_\ominus>0$ such that for every $t\ge0$ the union of the arc sets over the window $t\tilde B_\ominus,\dots,(t+1)\tilde B_\ominus-1$ is strongly connected. Put $B_\ominus=2\tilde B_\ominus-1$.

Assumption 7. The mixing matrix $C(k)$ has $C_{ij}(k)=1/(d^{\rm out}_j(k)+1)$ if $i=j$ or $j\to i\in\mathcal A(k)$, and $0$ otherwise; each $C(k)$ is column stochastic.

Each $f_i$ is differentiable with $L_i$-Lipschitz gradient (Assumption 4) and $\mu_i$-strongly convex with $\mu_i\ge0$, some $\mu_i>0$ (Assumption 5). Write $L=\max_iL_i$, $\bar\mu=\frac1n\sum_i\mu_i$, $\bar\kappa=L/\bar\mu$, and $x^*$ for the minimizer of $f$.

Iterates are $n\times p$ matrices whose row $i$ belongs to agent $i$; $\nabla\mathbf f(\mathbf x)$ has rows $\nabla f_i(x_i)$, and $\|\cdot\|_F$ is the Frobenius norm. Push-DIGing starts from $\mathbf x(0)=\mathbf u(0)$, $\mathbf y(0)=\nabla\mathbf f(\mathbf x(0))$, $\mathbf v(0)=\mathbf 1$ and iterates, with step size $\alpha>0$ and $V(k)=\operatorname{diag}\{\mathbf v(k)\}$,

$$\mathbf u(k+1)=C(k)(\mathbf u(k)-\alpha\mathbf y(k)),\quad \mathbf v(k+1)=C(k)\mathbf v(k),\quad \mathbf x(k+1)=V(k+1)^{-1}\mathbf u(k+1),$$ $$\mathbf y(k+1)=C(k)\mathbf y(k)+\nabla\mathbf f(\mathbf x(k+1))-\nabla\mathbf f(\mathbf x(k)).$$

The constants of the rate are $\tilde\tau=n^{-(2+nB_\ominus)}$, $Q_1=2n(1+\tilde\tau^{-nB_\ominus})/(1-\tilde\tau^{nB_\ominus})$, $\|V^{-1}\|^1_{\max}=\sup_{k,i}1/v_i(k)$ and, for an integer $B$,

$$\delta=Q_1\big(1-\tilde\tau^{nB_\ominus}\big)^{\frac{B-1}{nB_\ominus}},\qquad J_2=3Q_1\|V^{-1}\|^1_{\max}\bar\kappa B\big(\delta+Q_1(B-1)\big)(1+\sqrt n)\big(1+4\sqrt n\sqrt{\bar\kappa}\big).$$

Formalization targets

Goal: Theorem 18

For $n\ge2$, $B\ge B_\ominus$ with $\delta<1$, and every step size

$$0<\alpha<\frac{1.5(1-\delta)^2}{\bar\mu J_2},$$

there is $C>0$ with $\|\mathbf x(k)-\mathbf 1(x^*)^\top\|_F\le C\lambda^k$ for all $k$, where $0<\lambda<1$ is

$$\lambda=\sqrt[2B]{1-\alpha\bar\mu/1.5}\ \text{ if }\ \alpha\le\frac{1.5\big(\sqrt{J_2^2+(1-\delta^2)J_2}-\delta J_2\big)^2}{\bar\mu J_2(J_2+1)^2},\qquad \lambda=\sqrt[B]{\sqrt{\alpha\bar\mu J_2/1.5}+\delta}\ \text{ otherwise}.$$

Milestones

The paper's proof runs a small gain argument around the cycle $\mathbf q\to\mathbf z\to\check{\mathbf h}\to\check{\mathbf x}\to\mathbf q$, where $\mathbf q(k)=\mathbf x(k)-\mathbf 1(x^*)^\top$, $\mathbf z$ are gradient increments, $\mathbf h(k)=V(k)^{-1}\mathbf y(k)$ and $\check{\ }$ is the deviation from the row average. The milestones are the paper's own statements: the equivalent recursion (48) in terms of the row stochastic $\tilde R(k)=V(k+1)^{-1}C(k)V(k)$; the bound (49) $\|V^{-1}\|^1_{\max}\le n^{nB_\ominus}$ and row stochasticity of $\tilde R(k)$; Lemma 13 ($B$-step contraction by $\delta$); Lemmas 14–17 (the four arrows); Lemma 8 (an error bound for inexact gradient descent); Theorem 3 (the small gain theorem) and Lemma 4.

Significance

The theorem gives a geometric rate, with explicit constants, for a first-order method that uses only out-degree information, constant step sizes, one gradient per agent per round, and networks that are directed and need only be strongly connected jointly over windows. Before it, linear rates for distributed gradient methods required undirected or static graphs. The explicit $\lambda$ quantifies how the rate degrades with $n$, $B_\ominus$ and the condition number $\bar\kappa$. The result is proved in the paper; to the extent known, no machine-checked proof exists. A formalization yields a checked statement of the rate together with reusable components: the ergodic-norm small gain theorem, the push-sum weight bound, and the inexact gradient lemma, which also serve the companion DIGing mission on undirected graphs.

Difficulty

The natural Lyapunov approach fails: with asymmetric, time-varying weights there is in general no quadratic function that decreases at every step, and the consensus error contracts only over windows of $B$ iterations. The analysis therefore works with ergodic norms $\max_{k\le K}\lambda^{-k}\|\mathbf s(k)\|_F$ and chains four inequalities. Two further inputs come from outside the paper: the lower bound $v_i(k)\ge n^{-nB_\ominus}$ (Corollary 2(b) of Nedić–Olshevsky 2015) and the contraction of products of row stochastic matrices with entries bounded below on arcs (Lemma 5 of Nedić–Ozdaglar 2010), both of which a complete development has to prove.

Formalization scope

Stacked iterates are functions Fin n → EuclideanSpace ℝ (Fin p); agents are indexed from 0 and time from 0. An arc $j\to i$ is a pair (j, i) in a finite set A k. The weights $\mathbf v(k)$ are defined from $C$ alone, so $\|V^{-1}\|^1_{\max}$ is a constant of the graph sequence; it enters statements as a number with the hypothesis that it is the least upper bound of $\{1/v_i(k)\}$, never as a real supremum. Real powers are Real.rpow. The ergodic norm is the truncated maximum; the untruncated supremum is replaced by its pointwise meaning.

Four hypotheses are added to the page, each disclosed in the statements:

1. Assumption 7 includes the self-weight $C_{jj}(k)=1/(d^{\rm out}_j(k)+1)$. The printed rule assigns weights on arcs only, which makes column sums $d/(d+1)$; the paper's agent updates (p. 21) and analysis use the push-sum convention.
2. The step-size interval is open on the right: at $\alpha=1.5(1-\delta)^2/(\bar\mu J_2)$ the printed formula gives $\lambda=1$.
3. $B\ge B_\ominus$, required by Lemma 13, makes "large enough" precise.
4. $n\ge2$: at $n=1$ the constant $Q_1$ has a zero denominator.

The goal states only the hypotheses of Theorem 18 and the rate; it does not assume any of the arrows, gains, auxiliary parameters $\beta,\eta$ or ergodic-norm bounds, so it cannot be discharged by assembling hypotheses.

A complete development needs matrix-product contraction bounds for push-sum, Frobenius-norm calculus on stacked matrices, and strong convexity estimates for inexact gradient steps. The small gain theorem, Lemma 8 and the push-sum lemmas are reusable beyond this mission. Proofs of individual milestones are welcome independently.

Selected references

• A. Nedić, A. Olshevsky, W. Shi, Achieving geometric convergence for distributed optimization over time-varying graphs, SIAM J. Optim. 27 (2017) 2597–2633; arXiv:1607.03218v3. https://arxiv.org/abs/1607.03218 — https://doi.org/10.1137/16M1084316
• A. Nedić, A. Olshevsky, Distributed optimization over time-varying directed graphs, IEEE Trans. Automat. Control 60 (2015) 601–615. https://arxiv.org/abs/1303.2289
• A. Nedić, A. Olshevsky, Stochastic gradient-push for strongly convex functions on time-varying directed graphs, arXiv:1406.2075, 2014. https://arxiv.org/abs/1406.2075
• D. Kempe, A. Dobra, J. Gehrke, Gossip-based computation of aggregate information, Proc. 44th IEEE FOCS, 2003, 482–491. https://doi.org/10.1109/SFCS.2003.1238221
• W. Shi, Q. Ling, G. Wu, W. Yin, EXTRA: an exact first-order algorithm for decentralized consensus optimization, SIAM J. Optim. 25 (2015) 944–966. https://arxiv.org/abs/1404.6264
• G. Qu, N. Li, Harnessing smoothness to accelerate distributed optimization, arXiv:1605.07112, 2016. https://arxiv.org/abs/1605.07112
• J. Xu, S. Zhu, Y. C. Soh, L. Xie, Augmented distributed gradient methods for multi-agent optimization under uncoordinated constant stepsizes, Proc. 54th IEEE CDC, 2015, 2055–2060.

Motivation

In distributed optimization, $n$ agents each hold a private function $f_i:\mathbb R^p\to\mathbb R$ and must jointly solve

$$\min_{x\in\mathbb R^p}\ f(x)=\frac1n\sum_{i=1}^n f_i(x)$$

by exchanging vectors only with their current neighbours in a communication network. The setting covers distributed estimation and learning in sensor networks, formation control and power-system control, where no agent can see all the data and no central coordinator is available. Often the network changes over time: links appear and fail, and agents move.

The classical method, distributed gradient descent (DGD), mixes neighbours' iterates and takes a local gradient step. With a fixed step size it does not converge to the optimum, because at a consensual optimum the local gradients $\nabla f_i(x^*)$ need not vanish; exact convergence requires diminishing steps and is then sublinear. Nedić, Olshevsky and Shi (arXiv:1607.03218, SIAM J. Optim. 2017) introduced DIGing, which adds a second variable that tracks the network-wide average gradient, and proved that it converges R-linearly (geometrically) to the exact optimum with a fixed step size, over time-varying undirected graphs, with an explicit rate.

Setting

An $n\times p$ matrix $\mathbf x$ is stored by its rows; row $i$ is agent $i$'s copy $x_i\in\mathbb R^p$, and $\|\mathbf x\|_F$ is the Frobenius norm. Write $\bar x=\frac1n\sum_ix_i$ and $\check{\mathbf x}=\mathbf x-\mathbf 1\bar x^\top$ (the consensus violation). The stacked gradient $\nabla\mathbf f(\mathbf x)$ has rows $\nabla f_i(x_i)$.

Objectives. Each $f_i$ is differentiable with $L_i$-Lipschitz gradient, $L_i>0$ (Assumption 4), and satisfies $f_i(x)\ge f_i(y)+\langle\nabla f_i(y),x-y\rangle+\frac{\mu_i}2\|x-y\|^2$ with $\mu_i\ge0$, at least one $\mu_i>0$ (Assumption 5). Put $L=\max_iL_i$, $\bar\mu=\frac1n\sum_i\mu_i$ and $\bar\kappa=L/\bar\mu$. Then $f$ has a unique minimizer $x^*$.

Network. At time $k$ the agents communicate over an undirected graph $E(k)$ and mix with a matrix $W(k)$. Let $W_B(k)=W(k)W(k-1)\cdots W(k-B+1)$ and $\delta(k)=\sigma_{\max}\{W_B(k)-\frac1n\mathbf 1\mathbf 1^\top\}$. Assumption 1 requires: $W_{ij}(k)=0$ when $i\ne j$ and $(j,i)\notin E(k)$; every $W(k)$ is doubly stochastic; and for some positive integer $B$, $\delta=\sup_{k\ge B-1}\delta(k)<1$.

DIGing (Algorithm 1) with step size $\alpha>0$: $\mathbf y(0)=\nabla\mathbf f(\mathbf x(0))$ and

$$\mathbf x(k+1)=W(k)\mathbf x(k)-\alpha\mathbf y(k),\qquad \mathbf y(k+1)=W(k)\mathbf y(k)+\nabla\mathbf f(\mathbf x(k+1))-\nabla\mathbf f(\mathbf x(k)).$$

Formalization targets

Goal: Theorem 10

Let $J_1=3\bar\kappa B^2(1+4\sqrt n\sqrt{\bar\kappa})$. For every step size $0<\alpha<1.5(1-\delta)^2/(\bar\mu J_1)$ there is $C>0$ with

$$\|\mathbf x(k)-\mathbf 1(x^*)^\top\|_F\le C\lambda^k\quad\text{for all }k,$$

where $0<\lambda<1$ is the explicit rate

$$\lambda=\sqrt[2B]{1-\frac{\alpha\bar\mu}{1.5}}\ \text{ if }\ \alpha\le\frac{1.5(\sqrt{J_1^2+(1-\delta^2)J_1}-\delta J_1)^2}{\bar\mu J_1(J_1+1)^2},\qquad \lambda=\sqrt[B]{\sqrt{\frac{\alpha\bar\mu J_1}{1.5}}+\delta}\ \text{ otherwise.}$$

Milestones

The proof runs a small gain argument in the ergodic norm $\|\mathbf s\|_F^{\lambda,K}=\max_{k\le K}\lambda^{-k}\|\mathbf s(k)\|_F$ around the cycle $\mathbf q\to\mathbf z\to\check{\mathbf y}\to\check{\mathbf x}\to\mathbf q$, where $\mathbf q(k)=\mathbf x(k)-\mathbf 1(x^*)^\top$ and $\mathbf z(k)$ are the gradient differences. The milestones are the paper's own lemmas: Lemma 2 (the $B$-step consensus contraction); Lemmas 5, 6, 7 and 9 (the four arrows); Lemma 8 (an error bound for inexact gradient descent, used by Lemma 9); Theorem 3 (the small gain theorem); Lemma 4 (a bounded ergodic norm gives an R-linear rate).

Companions

The existence and uniqueness of $x^*$ (p. 9); Corollary 11, the polynomial-in-$n$ rate $\lambda(\tau)=\sqrt[B]{1-\tau^2/(128B^2n^{4.5}\bar\kappa^{1.5})}$ under the concrete graph and weight Assumptions 2–3; and Proposition 1, the optimality conditions behind the algorithm.

Significance

Theorem 10 gives geometric convergence of a fixed-step method to the exact optimum over networks that may be disconnected at every instant, provided they are jointly well mixed over windows of $B$ steps. Its rate is explicit in $B$, $n$, $\delta$, $\bar\mu$ and $\bar\kappa$, and Corollary 11 turns it into an iteration count polynomial in $n$. Gradient tracking of this kind has since become a standard building block of decentralized optimization and learning algorithms, and the small-gain analysis in the ergodic norm is reused for other methods with time-varying or directed communication; the companion mission in this series treats Push-DIGing over directed graphs with the same machinery.

The result is proved in the paper. As far as is known it has not been machine-checked. A formalization provides checked versions of the paper's reusable components: the small gain theorem in the ergodic norm, the error bound for inexact gradient descent on a sum of strongly convex functions, and the consensus contraction for products of doubly stochastic matrices. It also pins down the conventions the paper leaves implicit, such as the sign of the mixing weights and the endpoint of the step-size interval.

Difficulty

DIGing does not decrease any obvious quantity monotonically: the distance to the optimum can grow while the gradient tracker is still far from consensus, and over a time-varying graph a single mixing step need not contract at all; only products of $B$ matrices do. A one-step Lyapunov argument therefore fails. The paper's way around this is to bound each quantity of the cycle by the previous one in the ergodic norm, with gains that depend on $\lambda$, and to choose $\lambda$ and $\alpha$ so that the product of the four gains is below one. The algebra of that choice, which produces the two-regime formula for $\lambda$, is delicate: the constraints $\delta<\lambda^B<1$, $\sqrt{1-\alpha\bar\mu\beta/(\beta+1)}\le\lambda$ and the gain condition (37) pull in opposite directions. Lemma 8 needs a careful one-step analysis of gradient descent with perturbed gradient evaluations.

Formalization scope

A stacked matrix is Fin n → EuclideanSpace ℝ (Fin p); $\|\cdot\|_F$, $\bar x$, $\check{\mathbf x}$, $\mathbf 1c^\top$ and the ergodic norm (6) are defined in DIGing.Undir.Common; $W_B(k)$, $\sigma_{\max}$ (the operator norm on Euclidean $\mathbb R^n$), $\delta(k)$, Assumptions 1–3, DIGing, $J_1$ and the rate are in DIGing.Undir.Setting. The constants $L_i,\mu_i$ are parameters. $\delta$ is given as the least upper bound of $\{\delta(k):k\ge B-1\}$, and the optimum $x^*$ by its optimality. Agents and iterations are indexed from $0$. Roots are Real.rpow.

Two hypotheses differ from the printed text, both disclosed in the item notes. Doubly stochastic includes nonnegative entries (Mathlib's doublyStochastic); the paper uses the term in this sense, and Lemma 6 is false for signed matrices with unit row and column sums. The right endpoint $\alpha=1.5(1-\delta)^2/(\bar\mu J_1)$, printed as included, is excluded: there the rate formula gives $\lambda=1$. Corollary 11 assumes $p\ge1$, the paper's standing range (p. 4).

The goal assumes nothing about the arrows, the gains, the auxiliary parameters $\beta,\eta$ or the ergodic norm of the iterates; its only rate hypothesis is $0<\alpha<1.5(1-\delta)^2/(\bar\mu J_1)$, and its conclusion includes $\lambda<1$, so a bounded-sequence reading is ruled out.

A complete development needs: products and the spectral norm of doubly stochastic matrices; the ergodic norm and its monotonicity in $K$; basic smooth strongly convex analysis (existence of the minimizer, $\mu_i\le L_i$, co-coercivity); and real-power algebra for the choice of $\lambda$. The small gain theorem, Lemma 8 and Lemma 2 are reusable beyond this mission, and are shared with the Push-DIGing mission of this series. Corollary 11's proof additionally uses a bound $\delta\le1-\tau/(2n^2)$ from the consensus literature; formalizing it is a welcome separate contribution. Proofs of any milestone, and alternative arguments for the arrows, are welcome.

Selected references

• A. Nedić, A. Olshevsky, W. Shi, Achieving geometric convergence for distributed optimization over time-varying graphs, SIAM J. Optim. 27(4), 2017. https://arxiv.org/abs/1607.03218 (v3 is the version formalized)
• A. Nedić, A. Olshevsky, A. Ozdaglar, J. N. Tsitsiklis, On distributed averaging algorithms and quantization effects, IEEE Trans. Automat. Control 54(11), 2009. https://doi.org/10.1109/TAC.2009.2031203
• W. Shi, Q. Ling, G. Wu, W. Yin, EXTRA: An exact first-order algorithm for decentralized consensus optimization, SIAM J. Optim. 25(2), 2015. https://arxiv.org/abs/1404.6264
• A. Nedić, A. Ozdaglar, Distributed subgradient methods for multi-agent optimization, IEEE Trans. Automat. Control 54(1), 2009. https://doi.org/10.1109/TAC.2008.2009515

Motivation

How far is a graph from being regular? Several numerical irregularity measures answer this question, and spectral graph theory supplies a natural one. For a graph $G$ with $n$ vertices and $e(G)$ edges, the largest eigenvalue $\lambda_1(G)$ of the adjacency matrix is always at least the average degree $d(G) = 2e(G)/n$, with equality exactly when $G$ is regular. The difference $\lambda_1 - d$ is therefore a measure of irregularity; it was studied by Bell (1992) alongside the variance of the degrees, and it is one of several such measures, with Albertson's $\sum_{uv \in E} |d_u - d_v|$ and Nikiforov's degree deviation among the others. The measures are incomparable in general, and one way to understand what each gauges is to determine its extremal graphs.

A basic extremal question asks which graphs are the most irregular. Among all graphs the question is uninteresting, because isolated vertices lower $d$ without lowering $\lambda_1$. Among connected graphs it is a genuine optimization problem. Using the variable neighbourhood search system AutoGraphiX, Aouchiche, Bell, Cvetković, Hansen, Rowlinson, Simić and Stevanović (2008) found that the maximizers of $\lambda_1 - d$ over connected graphs on $n$ vertices are always pineapple graphs, a clique with pendant vertices hanging from one clique vertex, and they conjectured that this holds for every $n$ (Aouchiche et al., European J. Oper. Res. 2008).

Timeline:

• 1992: Bell compares $\lambda_1 - d$ with the degree variance as irregularity measures.
• 1988: Hong proves $\lambda_1^2 \le 2e(G) - (n-1)$ for graphs without isolated vertices.
• 2008: Aouchiche et al. state the pineapple conjecture from computer experiments, and determine which pineapple is best (clique size $\lceil n/2\rceil + 1$).
• 2017: Tait and Tobin prove the conjecture for all sufficiently large $n$ (arXiv:1606.01916, J. Combin. Theory Ser. B), in the same paper that settles the spectral extremal problems for outerplanar and planar graphs.

This mission formalizes Section 4 of Tait and Tobin.

Setting

All graphs are finite and simple; an $n$-vertex graph has vertex set $\{0, \dots, n-1\}$. The spectral radius $\lambda_1(G)$ is the largest eigenvalue of the adjacency matrix $A$ of $G$, the published platform definition specRad. The average degree is $d(G) = 2e(G)/n$, a real number.

A connected graph $G$ on $n$ vertices is a maximizer of $\lambda_1 - d$ (Lean: IsIrregMax G) if

$$\lambda_1(G') - d(G') \le \lambda_1(G) - d(G) \quad \text{for every connected graph } G' \text{ on the same } n \text{ vertices.}$$

The pineapple $PA(p,q)$ (Lean: pineapple p q) has $p+q$ vertices: the first $p$ form a complete graph $K_p$, and each of the other $q$ vertices is a pendant vertex, adjacent only to the clique vertex $0$. Stars ($p \le 2$) and complete graphs ($q = 0$) are degenerate pineapples.

The lemmas of the mission speak about the leading eigenvector $\mathbf v$ of a maximizer $G$: a vector with $A\mathbf v = \lambda_1 \mathbf v$, all entries positive, normalized so that its largest entry is $1$. Such a vector exists by the Perron–Frobenius theorem because $G$ is connected. $x$ denotes a vertex with $\mathbf v_x = 1$, $d_u$ the degree of $u$, and $N(x)$ the neighbourhood of $x$. Some statements carry a small parameter $\varepsilon > 0$, fixed before $n$.

Formalization targets

Goal: Theorem 21

$$\exists N\ \forall n \ge N\ \forall G \text{ on } n \text{ vertices}:\quad G \text{ maximizes } \lambda_1 - d \;\Longrightarrow\; \exists\, p, q,\ p + q = n,\ G \cong PA(p,q).$$

The clique size $p$ is left free. The optimal value $p = \lceil n/2\rceil + 1$ is determined by Aouchiche et al. by optimizing a cubic polynomial over pineapples; Tait and Tobin cite it and do not prove it, so it is not part of the goal.

Milestones, in the order of the proof

1. Hong's inequality $\lambda_1^2 \le 2e(G) - (n-1)$ for connected $G$ (cited, p. 14).
2. The pineapple $H = PA(\lceil n/2\rceil+1, \lfloor n/2\rfloor-1)$ has $\lambda_1(H) - 2e(H)/n \ge n/4 - 3/2$ (p. 14).
3. Lemma 16: $\lambda_1 = n/2 + c_1\sqrt n$ and $d = n/4 + c_2\sqrt n$ with $|c_1|, |c_2| < 1$.
4. Lemma 17: $0 \le \frac{1}{|N(x)|}\sum_{y\sim x}(d_y - \lambda_1\mathbf v_y) \le c_3\sqrt n$.
5. Lemma 18: a vertex $u \ne x$ with $\mathbf v_u > 1 - 2\varepsilon$, $d_u - \lambda_1\mathbf v_u = O(\sqrt n)$ and $d_u \ge (1/2 - 2\varepsilon)n$.
6. Inequality (11): $n/2 + \sqrt n + 5 \ge \mathbf v^t\mathbf v > n/2 - 2\varepsilon n - O(\sqrt n)$.
7. Lemma 19 (corrected): $\mathbf v_a\mathbf v_b > 1/2 + n^{-1/2} + 5n^{-1}$ forces $a \sim b$; $\mathbf v_a\mathbf v_b < 1/2 - 3\varepsilon$ forbids $a \sim b$ when $G - ab$ is connected.
8. Every vertex other than a lone vertex of entry $1$ is adjacent to a vertex of entry $1$ (p. 18, corrected).
9. Proposition 20: a partition $U, V, W$ with $U$ a clique of size about $n/2$ and entries near $1$, $V$ pendant vertices of entry below $(2+\varepsilon)/n$, and $W$ vertices of entry near $1/2$ adjacent only to $U$.
10. $W = \emptyset$: $G$ is a clique together with pendant vertices (pp. 20–21).

Significance

The result. Theorem 21 identifies the most spectrally irregular connected graphs for large $n$, confirming a conjecture that came from computer search and that had resisted the usual graph-transformation arguments. Combined with the cited optimization over pineapples, it gives the exact maximum of $\lambda_1 - d$ over connected $n$-vertex graphs for large $n$, which in turn bounds $\lambda_1$ by $d$ plus an explicit term for every connected graph. The intermediate statements, notably Lemma 19 which converts products of Perron entries into adjacency, are reusable in other spectral extremal problems over connected graphs.

Formalizing it. The theorem is proved on paper for large $n$; no machine-checked proof of it, or of Hong's inequality, is known. The formalization must make every "for $n$ sufficiently large" and every $O(\sqrt n)$ explicit, and it repairs two statements that are false as printed (see Formalization scope). A small-$n$ verification, or a proof for all $n$, would be further contributions.

Difficulty

The obvious approach is local improvement: given a non-pineapple, move an edge and show that $\lambda_1 - d$ increases. Each move changes both terms, by amounts of order $\mathbf v_a\mathbf v_b/\mathbf v^t\mathbf v$ and $2/n$ respectively, and these are comparable; neither the sign of the change nor connectivity of the modified graph is under control without first knowing the global structure. The proof therefore needs the whole chain of asymptotic estimates: the size of $\lambda_1$ and $d$, a second vertex of nearly maximal entry, the norm of the Perron vector, and only then the adjacency rules of Lemma 19. Every edge deletion must also keep the graph connected, since the maximum ranges over connected graphs.

Formalization scope

• Vertices are Fin n; graphs are SimpleGraph (Fin n) with classical decidability. $\lambda_1$ is the published WangKangXue.SpectralTuran.specRad, the largest eigenvalue of G.adjMatrix ℝ. $d$ is avgDeg G = 2 · #edges / n in $\mathbb R$.
• The maximum is over connected graphs on the same vertex set (IsIrregMax); dropping connectivity changes the problem.
• The Perron vector enters as universally quantified hypotheses: any v with (G.adjMatrix ℝ).mulVec v = specRad G • v, all entries positive, all entries at most $1$, and a vertex x with v x = 1. It is never quantified existentially.
• "For $n$ sufficiently large" is ∃ N, ∀ n ≥ N. Constants from $O(\sqrt n)$ and "a constant $c_3$ not depending on $n$" are existentially quantified before $N$, $n$ and $G$. In Lemma 18, inequality (11) and Lemma 19 the proof works for every $\varepsilon > 0$, which is universally quantified; Proposition 20 needs $\varepsilon$ small and is stated for $0 < \varepsilon < \varepsilon_0$.
• $\lceil n/2\rceil$ and $\lfloor n/2\rfloor$ are the natural-number quotients $(n+1)/2$ and $n/2$; the pineapple lower bound assumes $n \ge 2$.
• "$G$ is a pineapple" is a graph isomorphism G ≃g pineapple p q with $p + q = n$. The pineapple is defined by its edges, clique plus pendants at one vertex; it is not defined by any property that the proof establishes, and the clique size is not pinned.
• Two printed statements are corrected and the corrections are disclosed. Lemma 19's second half requires $G - ab$ to be connected (without it, a pendant edge of the extremal pineapple is a counterexample), and both halves are for distinct vertices. The claim on p. 18 that every vertex has a neighbour of entry $1$ excludes only a vertex that is the unique vertex of entry $1$ (the hub of a pineapple is the exception). Lemma 17's summand is $(d_y - \lambda_1\mathbf v_y)$, as in its proof.
• A trivializing formalization is ruled out: the class is connected graphs, extremality is the hypothesis rather than a consequence, the eigenvector is universally quantified, constants do not depend on $n$, and the clique size is free. A maximizer exists for every $n \ge 1$, so the goal is not vacuous.
• Needed infrastructure: Perron–Frobenius for connected graphs, the Rayleigh-quotient characterization of $\lambda_1$, Cauchy interlacing (or monotonicity of $\lambda_1$ under subgraphs), and Hong's inequality. These are reusable well beyond this mission, and contributions of any of them are welcome.

Selected references

• M. Tait and J. Tobin, Three conjectures in extremal spectral graph theory, J. Combin. Theory Ser. B (2017); arXiv:1606.01916v2. https://arxiv.org/abs/1606.01916
• M. Aouchiche, F. K. Bell, D. Cvetković, P. Hansen, P. Rowlinson, S. K. Simić and D. Stevanović, Variable neighborhood search for extremal graphs. 16. Some conjectures related to the largest eigenvalue of a graph, European J. Oper. Res. 191(3) (2008) 661–676. (Reference [3] of Tait–Tobin.)
• Y. Hong, A bound on the spectral radius of graphs, Linear Algebra Appl. 108 (1988) 135–139. (Reference [37].)
• F. K. Bell, A note on the irregularity of graphs, Linear Algebra Appl. 161 (1992) 45–54. (Reference [5].)
• M. O. Albertson, The irregularity of a graph, Ars Combin. 46 (1997) 219–225. (Reference [1].)
• V. Nikiforov, Eigenvalues and degree deviation in graphs, Linear Algebra Appl. 414(1) (2006) 347–360. (Reference [26].)

Motivation

The stochastic block model is the basic random-graph model of a network with communities. It serves as a test bed for clustering algorithms in statistics, machine learning and theoretical computer science. In its sparse two-community form, each vertex has a constant expected degree, and the question is how much of the hidden partition a graph reveals. Using the cavity method of statistical physics, Decelle, Krzakala, Moore and Zdeborová (arXiv:1109.3041, 2011) conjectured a sharp threshold: one can label the vertices better than chance when the signal-to-noise ratio $s^2/d$ exceeds one, and not otherwise.

Timeline:

• 2011. Decelle, Krzakala, Moore and Zdeborová state the threshold conjecture, from belief propagation and the stability of its fixed point.
• 2012. Mossel, Neeman and Sly prove the impossibility half: for $s^2\le d$ no estimator is correlated with the planted partition. They also show that $s^2=d$ is the threshold for distinguishing the model from an Erdős–Rényi graph (arXiv:1202.1499).
• 2013. Krzakala, Moore, Mossel, Neeman, Sly, Zdeborová and Zhang propose spectral algorithms based on the non-backtracking matrix (arXiv:1306.5550).
• 2013–2015. Mossel, Neeman and Sly prove the achievability half (arXiv:1311.4115, the source of this mission), with an algorithm built from counts of non-backtracking paths. Massoulié independently gives a different proof via self-avoiding path counts (arXiv:1311.3085).

Setting

Fix $a,b>0$ and let $n$ be the number of vertices. In $\mathcal G(n,a/n,b/n)$ every vertex $u$ receives, independently and uniformly, a label $\sigma_u\in\{+1,-1\}$. Then each unordered pair $\{u,v\}$ is an edge independently, with probability $a/n$ if $\sigma_u=\sigma_v$ and $b/n$ otherwise. Write

$$d=\frac{a+b}{2},\qquad s=\frac{a-b}{2},$$

for the average degree and the signal strength; $s$ may be negative.

An estimator $\hat\tau$ receives only the graph $G$ and outputs a labelling, possibly at random. Its overlap with the planted labelling is $\bigl|\frac1n\sum_v\sigma_v\hat\tau_v\bigr|$, with an absolute value because the two communities carry no names. A uniformly random guess has overlap of order $n^{-1/2}$.

The proof works with paths $\gamma=(u_0,\dots,u_k)$ in the complete graph: consecutive vertices distinct. A path is non-backtracking if $u_i\ne u_{i+2}$ and self-avoiding if all its vertices are distinct. With $W_e=\mathbf 1_{e\in E(G)}-d/n$ and $X_\gamma=\prod_iW_{\{u_{i-1},u_i\}}$, the path sums $N^{(k)}_{u,v}$ and $Y_{u,v}$ add $X_\gamma$ over the non-backtracking, respectively self-avoiding, paths of length $k$ from $u$ to $v$. An $\ell$-tangle is a connected subgraph of diameter at most $2\ell$ that contains two cycles.

Formalization targets

Goal: Theorem 2.1

For fixed $a,b>0$ with $s^2>d$ there are an estimator $\hat\tau$ and an $\varepsilon>0$ with

$$\lim_{n\to\infty}\mathbb P\Bigl[\Bigl|\frac1n\sum_v\sigma_v\hat\tau_v\Bigr|\ge\varepsilon\Bigr]=1 .$$

The goal fixes neither $\varepsilon$ nor the algorithm, so it is the weakest form of the conjecture.

Companions

• Theorem 2.2: the same conclusion for slowly growing $a_n,b_n=n^{o(1/\log\log n)}$ with $s_n^2/d_n\ge\lambda>1$.
• Theorem 2.3: recovery of all but $o(n)$ vertices when $s_n^2/d_n\to\infty$.

Milestones

• Claim 4.3 and Lemma 4.7: counting paths by their new, old and returning steps and by their tangles.
• Lemma 5.1 for $m=1$: the expected weight of a self-avoiding path or simple cycle is exactly $\sigma_u\sigma_vs^z/n^z$.
• Lemma 6.2: the graph is $\ell$-tangle-free with probability $1-n^{-1+o(1)}$.
• Theorem 2.8 (1)–(4): the first and second moments of $Y_{u,v}$, the decorrelation of path sums for disjoint pairs, and the closeness of $N^{(k)}_{u,v}$ to $Y_{u,v}$.
• Lemma 3.5: the aggregate path sum between two small vertex sets.
• Lemma 3.7: on the Poisson($d$) Galton–Watson tree whose labels are copied along each edge with probability $a/(a+b)$ and flipped otherwise, the depth-$R$ label sum $\Psi^+_R$ of a tree with root label $+1$ satisfies $\mathbb P[\Psi^+_R\ge\xi\kappa s^R]\ge\tfrac12+2\varepsilon$ for an independent uniform $\xi$ on $[-1,1]$ and all large $R$.

Significance

Together with the impossibility result for $s^2\le d$, Theorem 2.1 establishes $s^2=d$ as the detection threshold of the sparse two-community block model, a threshold first predicted by statistical physics. It equals the Kesten–Stigum bound for reconstruction on the Poisson Galton–Watson tree with the Ising channel, which locally describes the model. The non-backtracking and self-avoiding path statistics behind it led to the later spectral analyses of the non-backtracking matrix and to the multi-community theory.

The theorem is proved on paper. As far as is known, none of its ingredients is machine-checked: no formal statement of the block model, of path-count moments in sparse random graphs, or of tangle-freeness exists in Mathlib. The mission produces a faithful statement of the threshold theorem together with the first-moment, second-moment and combinatorial estimates the proof rests on. These can be attacked independently.

Difficulty

The obvious approach estimates $\sigma_u\sigma_v$ by the sign of the number of length-$k$ paths between $u$ and $v$, with $k\approx\alpha\log n$. Its mean is right: it is of order $s^k/n$. Its variance is not under control. With probability about $n^{-m^2}$ a clique of size $m$ appears near $u$ and $v$, and on that event the number of paths is so large that the expectation is dominated by a rare configuration. A plain second-moment argument therefore fails. The rare dense structures (tangles) must be excluded by conditioning, and the non-backtracking count must be compared with the self-avoiding one, whose moments can be computed. Even then, the second moment determines $\sigma_u\sigma_v$ only with probability bounded away from $1/2$. Turning many weakly correlated pairwise estimates into a globally correlated labelling is a separate step close to the threshold, where $s^2/d$ is barely above one.

Formalization scope

Everything is a finite sum. Vertices are Fin n, graphs SimpleGraph (Fin n), labellings Fin n → Bool. The joint law of $(\sigma,G)$ is written as an explicit weight. Conditioning on the labels of a vertex set $U$ is a weighted average with positive denominator $2^{-|U|}$. An estimator is a map from graphs to PMFs on labellings, so it never sees $\sigma$ and may be randomized. Its success probability is the probability that the overlap, with absolute value, is at least $\varepsilon$, for an $\varepsilon$ fixed before $n$.

Asymptotic notation follows §1.3 of the paper. $n^{-1+o(1)}$ is $n^{-1+c_n}$ for an explicit $c_n\to0$ chosen before the vertices, sets and labellings it is uniform over. "Sets of size $n^{o(1)}$" in a hypothesis means: for every $e_n\to0$, all sets of size at most $n^{e_n}$. Assumption 2.7 ($s,d=n^{o(1/\log\log n)}$ and $\log\log n\ll\ell\ll\sqrt{\log n}$) and the preamble of Theorem 2.8 ($s^2/d\ge\lambda>1$, the choice of $\alpha$, $k=\lceil\alpha\log n\rceil$) are shared definitions, so the four displays of Theorem 2.8 cannot drift apart. Non-asymptotic statements assume $0<a,b<n$, which is Definition 1.1's $q,q'\in(0,1)$.

Three printed slips are corrected and disclosed. Theorem 2.8 (2) carries the square $(s^2/(s^2-d))^2$ that the proof's display (17) gives. Theorem 2.8 (4) uses $|s|^k$, since $s$ may be negative. Lemma 4.7 assumes distinct endpoints, as all its uses do.

The labelled branching tree of Lemma 3.7 is encoded by its generation counts: the numbers of $+1$ and $-1$ labelled vertices at depth $r$ form a two-type Poisson chain on $\mathbb N^2$, which has the same law by Poisson thinning and superposition. Lemma 3.7 assumes $s>0$, the standing assumption of its section, and is stated for all sufficiently large $R$, the range its proof covers.

The statements rule out the trivial readings: the estimator cannot see $\sigma$, the overlap carries its absolute value, $\varepsilon$ does not depend on $n$, antecedent $o(1)$ bounds are universally quantified, and the model's weights are genuine probabilities for all large $n$.

Reusable infrastructure includes the finite-sum stochastic block model, path edge-type counts, and tangle-freeness. The weights of independent-edge random graphs and the Poisson Galton–Watson tree with the Ising broadcast are also of independent use. Contributions are welcome on any milestone, on infrastructure lemmas such as normalisation of the model's weights and independence of distinct edges given the labels, and on the steps of §3 that connect Theorem 2.8 to the goal.

Selected references

• E. Mossel, J. Neeman, A. Sly, A Proof of the Block Model Threshold Conjecture, arXiv:1311.4115v4, 2015. https://arxiv.org/abs/1311.4115
• E. Mossel, J. Neeman, A. Sly, Reconstruction and Estimation in the Planted Partition Model, Probab. Theory Related Fields 162 (2015). https://arxiv.org/abs/1202.1499
• A. Decelle, F. Krzakala, C. Moore, L. Zdeborová, Asymptotic analysis of the stochastic block model for modular networks and its algorithmic applications, Phys. Rev. E 84 (2011). https://arxiv.org/abs/1109.3041
• F. Krzakala, C. Moore, E. Mossel, J. Neeman, A. Sly, L. Zdeborová, P. Zhang, Spectral redemption in clustering sparse networks, PNAS 110 (2013). https://arxiv.org/abs/1306.5550
• L. Massoulié, Community detection thresholds and the weak Ramanujan property, STOC 2014. https://arxiv.org/abs/1311.3085