Graph Theory

Motivation

Mean field games describe large populations of agents who interact symmetrically: every agent sees the same average of all the others. Many populations interact instead along a network, where each agent responds only to its neighbours. Lacker and Soret (arXiv:2005.14102v2, 2021; Math. Oper. Res. 2022) study a linear-quadratic stochastic differential game on a finite graph that is simple enough to solve explicitly on every vertex-transitive graph, and then ask what happens to the equilibrium as the graph grows. The question is the network analogue of the classical convergence problem for mean field games: does the $n$-player equilibrium have a limit, and does that limit depend on the graph only through a small amount of information?

The answer of the paper is that the limit is governed by the empirical eigenvalue distribution of the graph Laplacian. Dense graph sequences (degrees tending to infinity) all have the same limit, the mean field game; sparse ones (bounded degrees) have limits that depend on the graph, through its spectrum. This mission formalizes that large-graph limit theorem, Theorem 2.6 of the paper. Mission I of the series formalizes the explicit equilibrium on a fixed transitive graph (Theorem 2.5), on which this mission builds.

Setting

Let $G$ be a finite simple graph on vertex set $\{1,\dots,n\}$ with adjacency matrix $A_G$ and degree matrix $D_G$. Its Laplacian is $L_G = D_G^{-1}A_G - I$. $G$ is transitive if every vertex can be mapped to every other one by a graph automorphism; such a graph is regular, of degree $\delta(G)$, and $L_G$ is then symmetric with eigenvalues $\lambda^G_1,\dots,\lambda^G_n\in[-2,0]$. The empirical eigenvalue distribution is $\mu_G = \frac1n\sum_i\delta_{\lambda^G_i}$.

Fix a horizon $T>0$, a volatility $\sigma>0$ and a weight $c>0$. Player $v$ controls the state

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

driven by independent Brownian motions, with Markovian feedback controls $\alpha_v$, and pays

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

On a transitive graph without isolated vertices, Theorem 2.5 gives an explicit Nash equilibrium: with $Q_G(x) = \det(I - xL_G)^{1/n}$ and $f_G$ the solution of $f_G' = c\,Q_G'(f_G)$, $f_G(0) = 0$ on $[0,T]$, the feedback is $\alpha^G_i(t,\boldsymbol x) = -e_i^\top P_G(t)\boldsymbol x$ with $P_G(t) = -f_G'(T-t)L_G(I - f_G(T-t)L_G)^{-1}$. The resulting equilibrium state process $\boldsymbol X^G$ is Gaussian, and the value is $\mathrm{Val}(G) = \frac1n\sum_v J_v$.

For a probability measure $\mu$ define $Q_\mu(x) = \exp\int_{[-2,0]}\log(1-x\lambda)\,\mu(d\lambda)$, so that $Q_{\mu_G} = Q_G$.

Formalization targets

Goal: Theorem 2.6

Let $(G_n)$ be finite transitive graphs without isolated vertices, $|G_n|\to\infty$, with $\boldsymbol X^{G_n}(0) = 0$, and suppose $\mu_{G_n}\to\mu$ weakly for a probability measure $\mu$. Then (1) the ODE $f_\mu' = c\,Q_\mu'(f_\mu)$, $f_\mu(0) = 0$ has a unique solution on $[0,T]$; (2) for every vertex sequence $k_n$ and $t\in[0,T]$,

$$\mathrm{Law}\big(X^{G_n}_{k_n}(t)\big)\to\mathcal N\big(0,V_\mu(t)\big),\qquad V_\mu(t) = \sigma^2\int_0^t\int_{[-2,0]}\Big(\frac{1-\lambda f_\mu(T-t)}{1-\lambda f_\mu(T-s)}\Big)^2\mu(d\lambda)\,ds;$$

(3) the empirical measure $\frac1{|G_n|}\sum_i\delta_{X^{G_n}_i(t)}$ converges weakly in probability to $\mathcal N(0,V_\mu(t))$; (4)

$$\lim_{n\to\infty}\mathrm{Val}(G_n) = -\frac{\sigma^2}2\log\int_{[-2,0]}\frac{-\lambda}{1-\lambda f_\mu(T)}\,\mu(d\lambda).$$

Milestones

The milestones are the statements the paper's proof (§3, §6, §7.1) relies on: the stability of $f_\mu$ in $\mu$ (Proposition 3.2, last sentence); the finite-graph variance formula (2.7); monotonicity and concavity of $f_\mu$ (Proposition 3.3, first sentence); correlation decay (Proposition 2.12) for distinct vertices; the relation between degrees and the spectral limit (Lemma 7.1); the Gaussian Poincaré bound (7.3) and the concentration (7.1) of the empirical measure; and the spectral form (2.9) of the value.

Significance

Theorem 2.6 reduces the large-population behaviour of a network game to one spectral object. For complete graphs $\mu = \delta_{-1}$ and the limit is the mean field game; for sparse sequences such as cycles, tori, or random regular graphs, $\mu$ is a non-degenerate measure and the limiting variance and value differ from the mean field ones. The theorem thereby gives a quantitative criterion for when a mean field approximation of a network game is accurate, and it shows propagation of chaos in both regimes: in the dense case because interactions are weak, in the sparse case because typical players are far apart in the graph.

The result is proved in the paper; none of it has been machine-checked. A complete formalization requires a Lean account of Gaussian laws of linear SDEs with additive noise, of weak convergence of spectral measures of graph Laplacians, and of a Gaussian Poincaré inequality, none of which is currently in Mathlib in the needed form. Each of these is reusable well beyond this mission.

Difficulty

Parts (2) and (4) follow from the finite-graph formulas once $f_{G_n}\to f_\mu$ uniformly, but that convergence requires stability of a nonlinear ODE whose vector field is defined through the spectral measure, uniformly over a class of measures. The harder step is (3). Convergence of one player's law does not imply convergence of the empirical measure: the players are correlated, and on sparse graphs every player has a bounded number of strong neighbours, so the correlations do not vanish uniformly. Bounding them requires an estimate that decays in the graph distance and in the degree, and combining it with the growth of graph balls, which is controlled differently in the dense and in the sparse regime. The usual mean field route is closed: unless the graph is complete, the state vector is not exchangeable, so propagation-of-chaos arguments based on exchangeability do not apply.

Formalization scope

The Lean development lives in namespace GraphLQGame.Asymptotics.

• Vertices $\{1,\dots,n\}$ are Fin n; a graph sequence is G : ∀ k, SimpleGraph (Fin (N k)) with $N_k\to\infty$.
• $L_G$ is the random-walk Laplacian above, not Mathlib's lapMatrix. $\mu_G$ is built from the real roots of the characteristic polynomial of $L_G$, with multiplicity.
• Weak convergence of measures on $\mathbb R$ is convergence of $\int h\,d\mu_k$ for every bounded continuous $h$. Weak convergence in probability of the empirical measure is convergence in probability of $\int h\,dm^{G_n}(t)$ for every bounded continuous $h$.
• A state process is a pathwise strong solution of (2.1) on its own probability space, driven by a standard Brownian motion and adapted to its completed filtration. Statements about several graphs are statements about laws.
• Costs are $[0,\infty]$-valued lower integrals; the value is computed after asserting finiteness.
• In $P_G$, $f_G'(T-t)$ is written as its ODE value $c\,Q_G'(f_G(T-t))$. ODE solutions are constrained on $[0,T]$ (or on $\mathbb R_+$ for Propositions 3.2 and 3.3), with uniqueness stated on that domain.
• The Gaussian law $\mathcal N(0,V)$ is gaussianReal 0 V.toNNReal; $V_\mu(t)\ge0$.

The goal quantifies over every solution $f_{G_n}$, $f_\mu$ and every equilibrium state process, and also asserts that the graph ODE solutions and the state processes exist, so it cannot be discharged vacuously. Proposition 2.12 is stated for distinct vertices: as printed, (2.17) is also claimed for $u = v$, where it fails on complete graphs of large degree; the off-diagonal case is the one the proof of Theorem 2.6 uses. Theorem 2.5 (mission I) is not restated here; a solver proves what is needed of it.

Contributions are welcome at every level: Gaussian laws of linear SDEs, spectral measures of graph matrices, ODE stability, a Gaussian Poincaré inequality, and the milestones themselves.

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; published in Math. Oper. Res., 2022, https://doi.org/10.1287/moor.2021.1179. 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
• S. Boucheron, G. Lugosi, P. Massart, Concentration Inequalities: A Nonasymptotic Theory of Independence, Oxford University Press, 2013 (Theorem 3.20, Gaussian Poincaré inequality). https://doi.org/10.1093/acprof:oso/9780199535255.001.0001
• 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

Why mean field approximations on graphs need a threshold

Mean field games (MFGs) describe the limit of symmetric stochastic differential games as the number of players tends to infinity, when every player interacts with the empirical distribution of all the others. Their main practical use is the converse direction: an equilibrium of the limiting game supplies a simple, decentralized control that is an approximate Nash equilibrium of the game with finitely many players. For the complete graph, where everybody interacts with everybody, this is classical, with the standard rate $O(1/\sqrt n)$ (Carmona and Delarue, Probabilistic Theory of Mean Field Games, Vol. II, §6.1; Huang, Malhamé and Caines 2006, Theorem 12), as recalled on p. 10 of the paper.

Many interacting systems are not complete graphs: players see only their neighbours in a network. The question is then how dense the network must be for the mean field approximation to remain valid. Lacker and Soret (arXiv:2005.14102v2) answer it exactly for a linear-quadratic "flocking" game, where explicit computations are possible. This mission formalizes their Theorem 2.11, which applies to every finite graph, with no transitivity or regularity assumed.

Setting

Let $G$ be a finite simple graph on the vertex set $V=\{1,\dots,n\}$; $u\sim v$ means $u$ and $v$ are adjacent and $\deg_G(v)$ is the number of neighbours of $v$. Fix a horizon $T>0$, a volatility $\sigma>0$ and a cost weight $c>0$. Each player $v\in V$ controls a real state $X_v$ through

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

where $W_1,\dots,W_n$ are independent standard Brownian motions and $\boldsymbol X=(X_u)_{u\in V}$. A Markovian control $\alpha_v\in\mathcal A_G$ is a Borel function of time and the full state $\boldsymbol X(t)\in\mathbb R^V$, of linear growth. The cost of player $v$ under a profile $\boldsymbol\alpha=(\alpha_u)_{u\in V}$ is

$$J_v(\boldsymbol\alpha)=\frac12\,\mathbb E\Big[\int_0^T|\alpha_v(t,\boldsymbol X(t))|^2\,dt+c\,\Big|X_v(T)-\frac1{\deg_G(v)}\sum_{u\sim v}X_u(T)\Big|^2\Big],$$

and $\frac12\mathbb E[\int_0^T|\alpha_v|^2dt+c|X_v(T)|^2]$ for an isolated vertex: each player wants to end near the average of its neighbours at minimal quadratic effort. For a vector $\boldsymbol\varepsilon\in\mathbb R^V_+$, a profile is a Markovian $\boldsymbol\varepsilon$-Nash equilibrium if no player $v$ can lower its cost by more than $\varepsilon_v$ by switching unilaterally to another control $\beta\in\mathcal A_G$, written $(\beta,\boldsymbol\alpha^{-v})$.

The mean-field control is

$$\alpha^{\mathrm{MF}}(t,y)=\frac{-cy}{1+c(T-t)},\qquad \alpha^{\mathrm{MF}}_v(t,\boldsymbol x)=\alpha^{\mathrm{MF}}(t,x_v):$$

each player looks only at its own state, as if its neighbours' average were frozen at its mean.

Formalization targets

Goal: Theorem 2.11

Define $\epsilon^G_v=\sigma^2\frac{cT}{1+cT}\sqrt{\frac{cT(2+cT)}{\deg_G(v)}}$ if $\deg_G(v)\ge1$ and $\epsilon^G_v=0$ if $\deg_G(v)=0$, and with the minimal degree $\delta(G)=\min_v\deg_G(v)$,

$$\epsilon_G=\sigma^2\frac{cT}{1+cT}\sqrt{\frac{cT(2+cT)}{1\vee\delta(G)}}.$$

Then, with zero initial states, the state equation for $(\alpha^{\mathrm{MF}}_v)_{v\in V}$ has a solution, and

$$(\alpha^{\mathrm{MF}}_v)_{v\in V}\ \text{is an } \epsilon^G\text{-Nash equilibrium and an } \epsilon_G\text{-Nash equilibrium on } G.$$

Milestones

1. Lemma 7.2: $\alpha^{\mathrm{MF}}$ is optimal for the one-player problem $\min\frac12\mathbb E[\int_0^T\beta^2dt+c|Y(T)|^2]$, $dY=\beta\,dt+\sigma dW$, over all progressively measurable $\beta$.
2. Isolated vertices (p. 40): $J_v(\boldsymbol\alpha)=\inf_\beta J_v(\beta,\boldsymbol\alpha^{-v})$ when $\deg_G(v)=0$.
3. (7.7): under $\alpha^{\mathrm{MF}}$, $(X_u(T))_u$ are i.i.d. $N(0,\sigma^2T/(1+cT))$, so the neighbour average has second moment $\sigma^2T/(\deg_G(v)(1+cT))$.
4. Steps (1), (2), (3) (p. 41): a lower bound on $J_v(\beta,\boldsymbol\alpha^{-v})$, an energy bound for deviations no worse than the zero control, and the comparison with $J_v(\boldsymbol\alpha^{\mathrm{MF}})$.
5. (7.5): for $\deg_G(v)\ge1$ and every admissible $\beta$, $J_v(\beta,\boldsymbol\alpha^{-v})\ge J_v(\boldsymbol\alpha)-\epsilon^G_v$.

Significance

The result. Theorem 2.11 gives an explicit threshold for the mean field approximation on networks: along any sequence of graphs whose minimal degree diverges, the decentralized control $\alpha^{\mathrm{MF}}$ is an $\epsilon_{G_n}$-Nash equilibrium with $\epsilon_{G_n}\to0$, and the vector form says more: if the average of $(1\vee\deg_{G_n}(v))^{-1/2}$ over vertices tends to zero, the per-player errors vanish on average (the paper's (2.16)). The rate $\deg_G(v)^{-1/2}$ quantifies how the accuracy of the approximation depends on denseness. In the same paper, transitive graphs whose degrees stay bounded lead to equilibria that do not agree with the mean field one, so a denseness condition cannot be dropped.

Formalizing it. The theorem is proved in the paper; to our knowledge no part of it is machine-checked. A formal development needs, beyond the statement, a verification argument for a one-dimensional linear-quadratic control problem with additive noise, Gaussian computations for linear SDEs driven by Brownian motion, and the comparison of costs between the equilibrium system and a system with one deviating player. The one-player result (Lemma 7.2) and the Gaussian facts of (7.7) are reusable well beyond this mission.

Difficulty

The obvious argument compares a deviating player with an isolated player and treats the neighbour average as noise independent of the deviation. Two things stand in the way. The cost of player $v$ couples its terminal state with the neighbours' average through a cross term $\mathbb E[\frac1{\deg_G(v)}\sum_{u\sim v}X_u(T)\,Y_v(T)]$, and the deviation $\beta(t,\boldsymbol Y(t))$ may look at the neighbours' states, so the cross term does not vanish; it has to be bounded through the size of the deviation's energy. And an arbitrary deviation has no a priori energy bound: one is available only for deviations that do at least as well as the zero control, which is why the argument passes through a (near-)optimal deviation. Lemma 7.2 itself requires a verification theorem over all progressively measurable controls, not only feedback ones.

Formalization scope

The Lean development lives in the namespace GraphLQGame.DenseApprox and uses the shared encoding of this series:

• vertices are Fin n (the paper's $\{1,\dots,n\}$ become $\{0,\dots,n-1\}$), the state space is EthierKurtz.SDEState n, and $G$ is any SimpleGraph (Fin n); isolated vertices are allowed;
• controls are Borel with linear growth on $[0,T]$ only; their values at other times are never used, and the formula for $\alpha^{\mathrm{MF}}$ outside $[0,T]$ is evaluated with Lean's total division;
• a solution of the state equation is a pathwise strong solution carrying its own probability space and an $n$-dimensional standard Brownian motion; costs are $[0,\infty]$-valued lower Lebesgue integrals, and the Nash inequality is required for every solution of the profile and of each deviation (faithful by strong uniqueness);
• $T,\sigma,c>0$ are the standing assumptions of §2.1;
• initial states are zero. The printed theorem does not mention $X(0)$; the paper fixes non-random initial states that are "in many cases" zero, and the whole proof is for $X(0)=0$. With non-zero initial states the claim fails in general, so this is a disclosed hypothesis;
• the goal also asserts that the state equation for $\alpha^{\mathrm{MF}}$ has a solution, so the Nash property cannot hold vacuously; Lemma 7.2 is stated over every continuous adapted solution of its SDE, and Step (2) carries, as an explicit hypothesis, the comparison with the zero control that its proof uses.

A formalization in which $\alpha^{\mathrm{MF}}$ is compared only with deviations depending on the player's own state, or in which the costs are Bochner integrals that vanish when not integrable, would be trivially or wrongly satisfied; both are ruled out by the encoding above.

Welcome contributions: the verification argument for Lemma 7.2, the Gaussian law of linear SDEs with additive noise, and proofs of the three steps. Related missions in this series: I (an explicit Nash equilibrium on transitive graphs) and II (large-graph limits).

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 (2022). https://arxiv.org/abs/2005.14102
• R. Carmona, F. Delarue, Probabilistic Theory of Mean Field Games with Applications II, Springer, 2018. https://doi.org/10.1007/978-3-319-56436-4
• M. Huang, R. P. Malhamé, P. E. Caines, Large population stochastic dynamic games: closed-loop McKean–Vlasov systems and the Nash certainty equivalence principle, Commun. Inf. Syst. 6 (2006), 221–252. https://doi.org/10.4310/CIS.2006.v6.n3.a5
• H. Pham, Continuous-time Stochastic Control and Optimization with Financial Applications, Springer, 2009 (verification theorem, Theorem 3.5.2). https://doi.org/10.1007/978-3-540-89500-8

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.

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].)