Graph Theory

Motivation

For a real symmetric matrix, the largest eigenvalue is the maximum of the quadratic form $\mathbf x^\top A\mathbf x$ on the unit sphere, and it is computable to any accuracy in polynomial time. Tensor eigenvalues, introduced independently by Lim (2005) and Qi (2005), extend this picture to higher order: they are the stationary values of the cubic form $\mathcal A(\mathbf x,\mathbf x,\mathbf x)$ on the unit sphere. They appear in multilinear statistics, signal processing, hypergraph theory and polynomial optimization, and for these applications the symmetric case is the natural one.

Hillar and Lim, in Most Tensor Problems Are NP-Hard (J. ACM 2013), show that the eigenvalue problem stays NP-hard when the tensor is required to be symmetric (their Theorem 9.3). The proof is short once one ingredient is available: a theorem of Nesterov (2003), in a form corrected by Hillar and Lim, that expresses the stability number of a graph as the maximum of an explicit cubic polynomial over a sphere. This mission formalizes that chain.

Setting

Let $G=(V,E)$ be a simple graph on $V=\{1,\dots,v\}$, $v\ge1$. A set of vertices is stable if no two of its members are adjacent; the stability number $\alpha(G)$ is the size of a largest stable set, so $1\le\alpha(G)\le v$.

Put $n=v+v(v-1)/2$ and write a vector of $\mathbb R^n$ as $\mathbf z=(\mathbf x,\mathbf y)$, with $\mathbf x=(x_1,\dots,x_v)$ indexed by vertices and $\mathbf y=(y_{ij})_{i<j}$ indexed by pairs of vertices. The tensor $\mathcal S_G=[\![s_{abc}]\!]\in\mathbb R^{n\times n\times n}$ has entry $1$ at the six orderings of the triple of coordinates $(x_i,x_j,y_{ij})$ for every non-adjacent pair $i<j$, and $0$ elsewhere. It is symmetric: its entries do not change under any permutation of the three indices.

For a real 3-tensor $\mathcal A=[\![a_{abc}]\!]$ the cubic form is $\mathcal A(\mathbf z,\mathbf z,\mathbf z)=\sum_{a,b,c}a_{abc}z_az_bz_c$, and a real $\lambda$ is a unit $\ell^2$-eigenvalue of $\mathcal A$ if

$$\sum_{a,b}a_{abc}z_az_b=\lambda z_c\quad\text{for all }c,\qquad\text{for some }\mathbf z\text{ with }\|\mathbf z\|_2=1 .$$

Finally, $\lambda_l=2\sqrt{\tfrac23\left(1-\tfrac1l\right)}$ for $l\ge1$. In Lean these are TensorNP.SymEigen.stabTensor, cubicForm, IsUnitL2Eigenvalue and lambdaL, and $\alpha(G)$ is Mathlib's SimpleGraph.indepNum.

Formalization targets

Goal: Theorem 9.3, core

$$\alpha(G)=\max\{\,l\in\{1,\dots,v\}:\ \lambda_l\text{ is a unit }\ell^2\text{-eigenvalue of }\mathcal S_G\,\}.$$

That is, $\lambda_{\alpha(G)}$ is an eigenvalue of $\mathcal S_G$, and no $\lambda_l$ with $\alpha(G)<l\le v$ is. This is the statement on which the paper's $v$-query reduction rests; nothing is claimed about $l<\alpha(G)$.

Milestones, in the paper's order

1. Theorem 9.2 (Nesterov). With $\mathbb S^{n-1}=\{(\mathbf x,\mathbf y):\|\mathbf x\|_2^2+\|\mathbf y\|_2^2=1\}$,

$$\sqrt{1-\frac1{\alpha(G)}}=3\sqrt{\frac32}\cdot\max_{(\mathbf x,\mathbf y)\in\mathbb S^{n-1}}\ \sum_{i<j,\ \{i,j\}\notin E}x_ix_jy_{ij}.$$

2. The tensor. $\mathcal S_G$ is symmetric and $\mathcal S_G(\mathbf z,\mathbf z,\mathbf z)=6\sum_{i<j,\{i,j\}\notin E}x_ix_jy_{ij}$.
3. The maximum is an eigenvalue. $\max_{\|\mathbf z\|_2=1}\mathcal S_G(\mathbf z,\mathbf z,\mathbf z)$ is attained and is a unit $\ell^2$-eigenvalue of $\mathcal S_G$.
4. Its value. $\max_{\|\mathbf z\|_2=1}\mathcal S_G(\mathbf z,\mathbf z,\mathbf z)=\lambda_{\alpha(G)}$.
5. Further result: Theorem 6.9 (Banach), (23). For every symmetric $\mathcal S\in\mathbb R^{n\times n\times n}$,

$$\sup_{\mathbf x,\mathbf y,\mathbf z\ne\mathbf 0}\frac{|\mathcal S(\mathbf x,\mathbf y,\mathbf z)|}{\|\mathbf x\|_2\|\mathbf y\|_2\|\mathbf z\|_2}=\sup_{\mathbf x\ne\mathbf 0}\frac{|\mathcal S(\mathbf x,\mathbf x,\mathbf x)|}{\|\mathbf x\|_2^3},$$

both sides finite. The paper uses it in §10 to transfer Theorem 9.3 to the spectral norm and the best rank-one approximation of symmetric tensors.

Significance

The result. Theorem 9.3 places symmetric tensor eigenvalue among the NP-hard problems of Hillar and Lim's Table I, and through Banach's theorem (Theorem 10.2 of the paper) the same holds for the largest singular value, the spectral norm and the best rank-one approximation of a symmetric 3-tensor. These are the quantities computed by higher-order power methods and by moment-based estimators, so the result marks where the matrix theory stops transferring.

Formalizing it. All results here are proved in the literature; none is machine-checked. Nesterov's theorem, which rests on the Motzkin–Straus theorem for the complement graph, is not on the platform or in Mathlib, and its formal statement settles the constant that the original paper got wrong by a factor $1/\sqrt2$ (Hillar–Lim, footnote 12). Banach's theorem on symmetric multilinear forms is likewise absent from Mathlib and is useful well beyond this mission.

Difficulty

The tensor identity (milestone 2) is bookkeeping. The analytic content sits in two places. First, Nesterov's theorem: the obvious route, fixing $\mathbf x$ and maximizing over $\mathbf y$ by Cauchy–Schwarz, reduces the cubic problem to a quartic one in $\mathbf x$, whose value still has to be identified with $\alpha(G)$; that identification is the Motzkin–Straus theorem, which is not available in Lean and is itself a nontrivial optimization over the simplex. Second, the passage from a maximum to an eigenvalue needs a Lagrange multiplier argument on the sphere, and the symmetry of $\mathcal S_G$ is what makes the gradient of the cubic form match the eigen-equation. Part (b) of the goal needs a further, unprinted observation relating every unit eigenpair to the cubic form. Banach's theorem has no short proof; the classical arguments go through polarization estimates or a variational argument specific to symmetric forms.

Formalization scope

• Tensors and indices. A 3-tensor is a function ι → ι → ι → ℝ on a finite index type. For $\mathcal S_G$ the index type is the disjoint union of the vertices Fin v and the pairs $\{(i,j): i<j\}$; this is $\mathbb R^n$ with coordinates labelled by name instead of by the paper's enumeration $\varphi(i,j)=(i-1)v-i(i-1)/2+j-i$. Vertices are $0,\dots,v-1$.
• Normalization. Eigenvalues are taken with a unit eigenvector. The paper's Problem 9.1 and Definition 5.1 say only $\mathbf x\ne\mathbf 0$; since $(\lambda,\mathbf x)\mapsto(t\lambda,t\mathbf x)$ preserves the eigen-equation, that reading would make every nonzero real an eigenvalue of $\mathcal S_G$ and the goal false. The unit sphere (13) is where the paper derives the notion.
• Explicit readings. The paper's index range "$1\le i<j<k\le v$" in the definition of $s_{ijk}$ is read as $k\le n$ (taken literally it gives $\mathcal S_G=0$). Every "max" is stated as a greatest element, so attainment is claimed. In (23) the suprema are real suprema over nonzero vectors with boundedness part of the conclusion. $v\ge1$ is assumed wherever the paper uses $\alpha(G)\in\{1,\dots,v\}$.
• Not formalized. The oracle procedure of the proof of Theorem 9.3, the polynomial size of $\mathcal S_G$, the input model of Problem 9.1 with quadratic irrationalities (Remark 9.4), and the NP-completeness of the stability number (Karp 1972, via $\alpha(G)=\omega(\overline G)$). The goal is the mathematical core of the Turing reduction, not a complexity statement.
• Trivializations ruled out. Without the unit normalization the eigenvalue statements are trivial or false; a goal stating only (a), or only an inequality between the maximum and $\lambda_{\alpha(G)}$, would not determine $\alpha(G)$; both are excluded by the statements above.
• Infrastructure. Everything rests on Mathlib (SimpleGraph.indepNum, real analysis on finite-dimensional spaces, Lagrange multipliers). A Motzkin–Straus theorem for SimpleGraph and Banach's theorem for symmetric trilinear forms are both reusable beyond this mission; contributions of either, or of a general "maximum of a symmetric cubic form on the sphere is an eigenvalue" lemma, are welcome.

Selected references

• C. J. Hillar, L.-H. Lim, Most Tensor Problems Are NP-Hard, Journal of the ACM 60(6), Article 45, 2013. https://doi.org/10.1145/2512329 (arXiv:0911.1393v5: https://arxiv.org/abs/0911.1393)
• Yu. Nesterov, Random walk in a simplex and quadratic optimization over convex polytopes, CORE Discussion Paper 2003/71, 2003. http://edoc.bib.ucl.ac.be:83/archive/00000238/01/dp2003-71.pdf
• E. de Klerk, The complexity of optimizing over a simplex, hypercube or sphere: a short survey, Central European Journal of Operations Research 16, 111–125, 2008. https://doi.org/10.1007/s10100-007-0052-9
• T. S. Motzkin, E. G. Straus, Maxima for graphs and a new proof of a theorem of Turán, Canadian Journal of Mathematics 17, 533–540, 1965. https://doi.org/10.4153/CJM-1965-053-6
• S. Banach, Über homogene Polynome in ($L^2$), Studia Mathematica 7(1), 36–44, 1938 (reference [Banach 1938] of Hillar–Lim).
• L.-H. Lim, Singular values and eigenvalues of tensors: a variational approach, Proc. IEEE CAMSAP 1, 129–132, 2005. https://arxiv.org/abs/math/0607648
• L. Qi, Eigenvalues of a real supersymmetric tensor, Journal of Symbolic Computation 40, 1302–1324, 2005. https://doi.org/10.1016/j.jsc.2005.05.007
• R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, 85–103, 1972. https://doi.org/10.1007/978-1-4684-2001-2_9

Motivation

The spectral norm of a matrix, its largest singular value, is computable in polynomial time to any accuracy. Its analogue for 3-tensors appears in the analysis of multilinear systems, in the best rank-1 approximation of a data array, in quantum information (the geometric measure of entanglement), and in the injective norm of tensor products. Hillar and Lim, Most Tensor Problems Are NP-Hard (J. ACM 60(6), 2013, Article 45; final version arXiv:0911.1393v5), show that, in contrast with matrices, deciding whether a fixed nonzero rational number is a singular value or the spectral norm of a rational 3-tensor is NP-hard (their Theorems 6.5 and 1.10).

The proof is a reduction from the clique number $\omega(G)$ of a graph. It combines three classical ingredients: the theorem of Motzkin and Straus (1965), which expresses $\omega(G)$ as the value of a quadratic program over the simplex; a theorem of Banach (1938) on the spectral norm of symmetric tensors; and an observation from He, Li and Zhang (2010) on maxima of sums of squared bilinear forms. Deciding $\omega(G)\ge l$ is one of Karp's (1972) NP-complete problems.

Setting

A real 3-tensor is an array $\mathcal A=[\![a_{ijk}]\!]\in\mathbb R^{l\times m\times n}$ with trilinear form $\mathcal A(\mathbf x,\mathbf y,\mathbf z)=\sum_{i,j,k}a_{ijk}x_iy_jz_k$. With the Euclidean norm $\|\cdot\|_2$, its spectral norm is

$$\|\mathcal A\|_{2,2,2}=\sup_{\mathbf x,\mathbf y,\mathbf z\ne\mathbf 0}\frac{|\mathcal A(\mathbf x,\mathbf y,\mathbf z)|}{\|\mathbf x\|_2\|\mathbf y\|_2\|\mathbf z\|_2}.$$

A real $\sigma$ is a unit $\ell^2$-singular value of $\mathcal A$ if there are unit vectors $\mathbf u,\mathbf v,\mathbf w$ with

$$\textstyle\sum_{j,k}a_{ijk}v_jw_k=\sigma u_i,\quad \sum_{i,k}a_{ijk}u_iw_k=\sigma v_j,\quad \sum_{i,j}a_{ijk}u_iv_j=\sigma w_k$$

for all $i,j,k$: the stationarity conditions of $\mathcal A(\mathbf u,\mathbf v,\mathbf w)$ on a product of unit spheres.

Let $G=(V,E)$ be a simple graph on $V=\{1,\dots,v\}$, $v\ge1$, with $e$ edges $\{i_k,j_k\}$, $k=1,\dots,e$, and clique number $\omega$. Let $\Delta_v$ be the standard simplex, $A_G$ the adjacency matrix and $J$ the all-ones matrix. For a positive integer $l$ set $Q_l=A_G+\frac1lJ$ and $M_l=\max_{\mathbf x\in\Delta_v}\mathbf x^\top Q_l\mathbf x$. Let $E_k=\frac12E_{i_kj_k}+\frac12E_{j_ki_k}$, and let $T_l$ be the maximum over unit $\mathbf u,\mathbf v\in\mathbb R^v$, $\mathbf w\in\mathbb R^{l+2e}$ of the multilinear form

$$\sum_{i=1}^l\Big(\mathbf u^\top\tfrac1lI\mathbf v\Big)w_i+\sum_{k=1}^e(\mathbf u^\top E_k\mathbf v)w_{l+k}+\sum_{k=1}^e(\mathbf u^\top E_k\mathbf v)w_{e+l+k}. \tag{26}$$

The graph tensor $\mathcal A_l\in\mathbb Q^{v\times v\times(l+2e)}$ has as entry $a_{ijk}$ the coefficient of $u_iv_jw_k$ in (26).

Formalization targets

Goal: Theorems 6.5 and 1.10, encoding-free core

For every graph $G$ on $v\ge1$ vertices and every enumeration of its edges:

$$\forall l\ge1:\ \|\mathcal A_l\|_{2,2,2}=1\iff l=\omega;\qquad 1\text{ is a unit singular value of }\mathcal A_\omega;\qquad \forall l>\omega:\ 1\text{ is not one of }\mathcal A_l,$$

so $\omega$ is the largest $l\in\{1,\dots,v\}$ for which $1$ is a unit singular value of $\mathcal A_l$. The paper's $v$-query Turing reductions rest on exactly this.

Milestones (in attack order)

1. Theorem 6.7 (Motzkin–Straus): $1-1/\omega=2\max_{\mathbf x\in\Delta_v}\sum_{\{i,j\}\in E}x_ix_j$.
2. (22): $M_l=1+\frac{\omega-l}{l\omega}$; so $M_\omega=1$, $M_l>1$ for $l<\omega$, $M_l<1$ for $l>\omega$.
3. Lemma 6.8: $M_l=N_l$, where $N_l=\max_{\|\mathbf u\|_2=1}\{\sum_{i=1}^l(\mathbf u^\top\frac1lI\mathbf u)^2+2\sum_k(\mathbf u^\top E_k\mathbf u)^2\}$.
4. Theorem 6.9 (Banach), (24): for a symmetric 4-tensor, $\|\mathcal S\|_{2,2,2,2}=\sup_{\mathbf x\neq\mathbf 0}|\mathcal S(\mathbf x,\mathbf x,\mathbf x,\mathbf x)|/\|\mathbf x\|_2^4$.
5. Proposition 6.10 (He–Li–Zhang): for symmetric $A_k$, $\max_{\|\mathbf u\|=\|\mathbf v\|=1}\sum_k(\mathbf u^\top A_k\mathbf v)^2=\max_{\|\mathbf v\|=1}\sum_k(\mathbf v^\top A_k\mathbf v)^2$.
6. Lemma 6.11: $T_l=M_l^{1/2}$, hence $T_l=1$ iff $l=\omega$, $T_l>1$ iff $l<\omega$, $T_l<1$ iff $l>\omega$.
7. Proof of Theorem 6.5: $\|\mathcal A_l\|_{2,2,2}=T_l$, $T_l$ is a unit singular value of $\mathcal A_l$, and every unit singular value has absolute value at most $T_l$.
8. §7 (content of Theorem 1.13): $\min_{\sigma\ge0,\ \text{unit }\mathbf u,\mathbf v,\mathbf w}\|\mathcal A-\sigma\,\mathbf u\otimes\mathbf v\otimes\mathbf w\|_F^2=\|\mathcal A\|_F^2-\|\mathcal A\|_{2,2,2}^2$, attained only with $\sigma=\|\mathcal A\|_{2,2,2}$.

Significance

The result. The goal shows that a single comparison with $1$ of the spectral norm, or of the singular-value spectrum, of an explicit rational tensor of size $v\times v\times(l+2e)$ encodes whether $l=\omega(G)$. It is the step that makes the spectral norm, the largest singular value, and (through §7) the best rank-1 approximation of a 3-tensor NP-hard, whereas all three are polynomial-time for matrices. It explains why the higher-order power method and its relatives carry no global guarantees, and it is the starting point for inapproximability results such as the paper's Theorem 1.11.

Formalizing it. The results are proved on paper; none of them is formalized. Motzkin–Straus, Banach's polarization theorem for symmetric 4-tensors, and the He–Li–Zhang identity are classical results that are not in Mathlib and not on the platform; each is reusable well beyond this mission (Turán-type bounds, polynomial optimization over spheres, injective norms). The mission also checks the paper's construction at the level of indices and constants.

Difficulty

The construction of $\mathcal A_l$ is explicit, and the comparison with $1$ is arithmetic once $T_l=M_l^{1/2}$ is known. Everything rests on the three cited theorems. Motzkin–Straus is an optimization statement over the simplex whose maximizers may lie on the boundary and need not be unique, so a first-order computation at an interior critical point does not settle it. Banach's theorem asserts equality, not equality up to a constant: the standard polarization identity bounds the 4-linear form by its diagonal values only up to a factor. Proposition 6.10 is where the paper's own argument is loose: the 4-linear form it introduces is not symmetric, so (24) does not apply as printed. Finally, the singular-value clauses require that the maximum of a trilinear form on a product of spheres is a stationary value. This must be proved, not assumed.

Formalization scope

Tensors are arrays Fin l → Fin m → Fin n → ℝ with 0-based indices: the paper's $a_{ijk}$ is A (i-1) (j-1) (k-1). The Euclidean norm is Real.sqrt (∑ i, x i ^ 2). Suprema and maxima are sSup of sets that are nonempty and bounded under the stated hypotheses; where the paper's "max" carries content (Motzkin–Straus, (22), §7), attainment is stated with IsGreatest/IsLeast. The graph is a SimpleGraph (Fin v) with $v\ge1$, clique number Mathlib's SimpleGraph.cliqueNum, and its edges are enumerated by an arbitrary Fin e ≃ G.edgeSet. Every statement holds for each enumeration, so the tensor depends on the choice and the conclusions do not. $\mathcal A_l$ is a rational tensor, read over $\mathbb R$ by casting.

Explicit readings of the paper:

• Definition 6.1 has no norm constraint. Since $(\sigma,\mathbf u,\mathbf v,\mathbf w)\mapsto(t\sigma,t\mathbf u,t\mathbf v,t\mathbf w)$ preserves (20), unnormalized singular values make every nonzero real a singular value of $\mathcal A_l$, so the clause "not for $l>\omega$" would be false. Singular vectors are therefore unit vectors, as in the paper's derivation on p. 0:21.
• The statement of Lemma 6.11 prints $w_{m+l+k}$. There is no $m$ in §6, and the proof uses $w_{e+l+k}$, which is formalized.
• $E_k$ is written entrywise as $\frac12[\{i,j\}=\{i_k,j_k\}]$, which equals $\frac12E_{i_kj_k}+\frac12E_{j_ki_k}$ for a loopless edge.
• "$T_l$ is just the maximum $\ell^2$-singular value of $\mathcal A_l$" is made explicit as milestone 7.
• The goal does not claim that $1$ fails to be a singular value of $\mathcal A_l$ for $l<\omega$; the paper neither claims nor uses this.

This is the mathematical core of a polynomial-time Turing reduction, not an NP-hardness theorem. The polynomial size of $\mathcal A_l$, the $v$-query procedure, the scaling to a general fixed $0\ne\sigma\in\mathbb Q$, and the NP-completeness of CLIQUE (Karp 1972, cited) are not formalized. Theorem 1.11 and Corollary 1.12 are out of scope.

Two formalizations would make the goal trivial, and both are excluded. One is dropping the unit-norm constraint, which makes every nonzero number a singular value. The other is a spectral norm taken as a supremum over all vectors without normalization, which makes it unbounded and junk-valued; here the quotients are normalized.

Contributions are welcome on each milestone. Motzkin–Straus, Banach (24) and He–Li–Zhang are self-contained and reusable. Lemma 6.11 and milestone 7 need Cauchy–Schwarz and a Lagrange-type stationarity argument on spheres, which Mathlib supports through IsLocalExtrOn and the Lagrange multiplier files.

Selected references

• C. J. Hillar, L.-H. Lim, Most Tensor Problems Are NP-Hard, J. ACM 60(6), Article 45, 2013. https://doi.org/10.1145/2512329 (final version arXiv:0911.1393v5, https://arxiv.org/abs/0911.1393v5)
• T. S. Motzkin, E. G. Straus, Maxima for graphs and a new proof of a theorem of Turán, Canadian J. Math. 17, 533–540, 1965. https://doi.org/10.4153/CJM-1965-053-6
• S. Banach, Über homogene Polynome in (L²), Studia Math. 7, 36–44, 1938. https://doi.org/10.4064/sm-7-1-36-44
• S. He, Z. Li, S. Zhang, Approximation algorithms for homogeneous polynomial optimization with quadratic constraints, Math. Program. Ser. B 125(2), 353–383, 2010. https://doi.org/10.1007/s10107-010-0409-z
• R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 85–103, 1972. https://doi.org/10.1007/978-1-4684-2001-2_9

Motivation

A snark is an uncolourable, cyclically 4-edge-connected cubic graph of girth at least 5: a cubic graph whose edges cannot be properly coloured with three colours, and which is not reducible to a smaller such graph by an elementary operation. Snarks are the critical cases for several of the central conjectures of graph theory, among them the cycle double cover conjecture, Tutte's 5-flow conjecture and the Berge–Fulkerson conjecture: a minimal counterexample to any of them, if one exists, is a snark. Lists of all small snarks are therefore used to test such conjectures by computer.

Brinkmann, Goedgebeur, Hägglund and Markström (arXiv:1206.6690v3, 2013) generated all snarks on up to 36 vertices. Testing 3-edge-colourability is NP-complete, and only a vanishing fraction of cubic graphs are snarks (0.00044% of the cubic graphs of girth at least 5 on 28 vertices, p. 4), so the generation algorithm needs cheap criteria that recognise, before a graph is built, that it will be colourable and can be skipped. Section 3.1 of the paper supplies such a criterion for the last construction step, and this mission formalizes it.

Setting

All graphs are finite and simple. A graph is cubic if every vertex has degree 3. A 3-colouring of a graph $G=(V,E)$ is a map $C:E\to\{0,1,2\}$ that gives different colours to any two distinct edges sharing an end-vertex; $G$ is colourable if it has one, i.e. its chromatic index satisfies $\chi'(G)\le 3$ (p. 2, Isaacs' terminology).

A 2-factor of $G$ is a spanning 2-regular subgraph $F$ (p. 4); each connected component of $F$ is a cycle. $F$ is an even 2-factor if all its cycles have even length (p. 5). For a 3-colouring $C$ and colours $i\ne j$, write $G_{ij}$ for the spanning subgraph whose edges are those coloured $i$ or $j$.

The edge insertion operation (Figure 1(d), p. 5) takes two distinct edges $e=ab$ and $e'=cd$ of $G$, which may share an end-vertex, subdivides $e$ by a new vertex $x$ and $e'$ by a new vertex $y$, and adds the edge $xy$. The resulting graph $G'$ has vertex set $V\cup\{x,y\}$ and edge set

$$E(G')=\bigl(E\setminus\{e,e'\}\bigr)\cup\{ax,xb,cy,yd,xy\}.$$

If $G$ is cubic, so is $G'$. In the generation algorithm every graph of girth at least 4 is produced from a graph with two fewer vertices by this operation.

Formalization targets

Goal: Theorem 3.3 (p. 5)

Let $G$ be a cubic graph with a 3-colouring $C$, let $i\ne j$ be colours, and let $e=ab$, $e'=cd$ be distinct edges of $G_{ij}$ lying on the same cycle of $G_{ij}$. Then

$$\chi'(G')\le 3,\qquad G' = G \text{ with an edge inserted between } e \text{ and } e'.$$

Milestones

1. Lemma 3.1 (p. 5). For a cubic graph $G$,

$$\chi'(G)\le 3 \iff G \text{ has an even 2-factor.}$$

2. The two-colour observation (§3.1, p. 5). If $G$ is cubic, $C$ is a 3-colouring and $i\ne j$, then $G_{ij}$ is an even 2-factor of $G$.
3. Lemma 3.2 (p. 5). If $F$ is an even 2-factor of a cubic graph $G$ and $e\ne e'$ are edges of $F$ on the same cycle of $F$, then the graph obtained by inserting an edge between $e$ and $e'$ is colourable.

Supporting statement (not on the goal's path)

Theorem 3.4 (p. 6, stated as folklore without proof). If $G$ is a colourable cubic graph and the inserted edge $xy$ lies on a 4-cycle of $G'$, then $G'$ is colourable.

Significance

The result. Theorem 3.3 is the look-ahead of the snark generator: one 3-colouring of a graph on $n-2$ vertices excludes, at once, every pair of edges lying on a common cycle of one of its three bicoloured 2-factors. For 28 vertices the first colouring alone discards on average 85% of the candidate edge pairs (p. 6), and the overall ratio of weak snarks among generated graphs on the last level improves by a factor of 85 (p. 4). The enumeration of all snarks up to 36 vertices, on which the paper's counterexamples and statistics rest, depends on this pruning being sound: a wrong pruning rule would silently delete snarks from the lists. Theorem 3.4 is a second pruning rule of the same kind.

Formalizing it. The results are proved (Lemma 3.1 is classical; the paper gives the argument for Lemma 3.2 in one sentence and for Theorem 3.3 by combination). None of them, and no statement about 3-edge-colourings of cubic graphs and their 2-factors, is formalized on the platform. The mission produces a machine-checked soundness proof of the pruning criterion and, along the way, a reusable development of the equivalence between 3-edge-colourings and even 2-factors in Lean's SimpleGraph library. Theorem 3.4 has no proof in the paper.

Difficulty

The combinatorial content is short; the difficulty lies in graph-theoretic infrastructure that Mathlib does not have. Lemma 3.1 relates a global object (a proper colouring of all edges) to the cycle structure of a spanning 2-regular subgraph, and either direction needs the description of a finite 2-regular graph as a disjoint union of cycles together with parity information along each cycle. Mathlib has walks, cycles and connected components, but no decomposition of a 2-regular graph into cycles and no notion of the length of a component as a cycle.

Lemma 3.2 and Theorem 3.3 change the vertex type: $G'$ lives on $V\sqcup\{x,y\}$, so 2-factors, connected components and cycle lengths must be transported from $G$ to $G'$, and the case where $e$ and $e'$ share an end-vertex (allowed by Figure 1(d)) has to be handled alongside the generic one. A first idea, to extend a given 3-colouring of $G$ directly to $G'$, does not work in general: the colours forced on the edges at $x$ and $y$ by the old colours of $e$ and $e'$ can conflict, and the hypothesis "same cycle" is what has to be used to avoid the conflict.

Formalization scope

Vertices form a type V with [Fintype V] [DecidableEq V]; graphs are SimpleGraph V with decidable adjacency, and "cubic" is Mathlib's G.IsRegularOfDegree 3. Colourability is G.lineGraph.Colorable 3 (an edge colouring, not a vertex colouring), and a 3-colouring is G.lineGraph.Coloring (Fin 3). A 2-factor is a graph F on the same vertex type with F ≤ G and F.IsRegularOfDegree 2; it is even if every connected component has an even number of vertices (Nat.card). The edge insertion operation produces a graph on V ⊕ Fin 2, with Sum.inr 0 subdividing $e$ and Sum.inr 1 subdividing $e'$; edges are unordered pairs Sym2 V. "On the same cycle" is encoded as membership of both edges in the 2-factor plus reachability of their end-vertices inside the 2-factor. Oddness is not defined as a number; Lemma 3.1 is stated in its second form.

Dropping "on the same cycle" would make Theorem 3.3 and Lemma 3.2 false (inserting edges between different cycles of a bicoloured 2-factor is exactly how snarks are produced), and both statements require the two edges to be distinct; a formalization without either hypothesis is ruled out. Every statement assumes cubicity, without which Lemma 3.1 fails.

Out of scope: the algorithmic content of §3 (isomorphism rejection, the look-ahead implementation, recolouring along non-hamiltonian cycles, the 85% / 11% / 3.4% statistics), the generation counts, and every exhaustive-search claim of the paper. The remaining results of the paper are covered by three sibling missions of this series.

Reusable beyond this mission: the 2-factor and even-2-factor definitions, the two-colour 2-factor of an edge colouring, and Lemma 3.1 itself. Contributions welcome: the cycle decomposition of finite 2-regular graphs, alternating colourings of even cycles, and a proof of Theorem 3.4.

Selected references

• G. Brinkmann, J. Goedgebeur, J. Hägglund, K. Markström, Generation and properties of snarks, J. Combin. Theory Ser. B 103 (2013); arXiv:1206.6690v3. https://arxiv.org/abs/1206.6690
• R. Isaacs, Infinite families of nontrivial trivalent graphs which are not Tait colorable, Amer. Math. Monthly 82 (1975) 221–239. https://doi.org/10.2307/2319844

Motivation

In distributed computing, many graph problems (minimum spanning tree, shortest paths, connectivity checks) are solved by processors that sit at the vertices of the input network and communicate only along its edges. When every edge can carry only a few bits per round, the number of rounds an algorithm needs can be far larger than the network's diameter. Understanding by how much is the central question of the CONGEST (here: B) model of Peleg's monograph Distributed Computing: A Locality-Sensitive Approach (SIAM, 2000).

Das Sarma, Holzer, Kor, Korman, Nanongkai, Pandurangan, Peleg and Wattenhofer (SIAM J. Comput. 41 (2012) 1235–1265) proved round lower bounds for a long list of verification problems (is a given subgraph a spanning tree, a cut, a Hamiltonian cycle, …) and for approximating optimization problems such as the minimum spanning tree and shortest paths. Every one of those bounds goes through a single reduction, the Simulation Theorem (Theorem 3.1), which transfers lower bounds from two-party communication complexity to distributed algorithms.

Timeline:

• 2000: Peleg and Rubinovich (SIAM J. Comput. 30) prove an $\tilde\Omega(\sqrt n)$ lower bound for distributed MST construction on a family of graphs built from paths and a tree.
• 2006: Elkin (SIAM J. Comput. 36) extends it to MST approximation, using the networks $G(\Gamma,d,p)$ (reference [10] of the paper).
• 2011–2012: Das Sarma et al. isolate the Simulation Theorem as a general reduction for arbitrary Boolean functions $f$ and derive lower bounds for many verification and approximation problems.

Setting

A B-model network is an undirected graph whose vertices are processors with unbounded local computation. Computation proceeds in synchronous rounds; in each round, every vertex sends a message of $B$ bits along each incident edge in each direction, then updates its local state from its old state and the messages it received. Two vertices $s$ and $r$ hold inputs $x,y\in\{0,1\}^b$; all other vertices start without input. A public-coin randomized algorithm additionally lets all vertices read a shared random string. It computes $f:\{0,1\}^b\times\{0,1\}^b\to\{0,1\}$ with $\epsilon$-error in $T$ rounds if, for every $(x,y)$, both $s$ and $r$ output $f(x,y)$ after round $T$ with probability at least $1-\epsilon$. $R^{G}_\epsilon(f)$ is the least such $T$.

In the communication complexity model, Alice holds $x$, Bob holds $y$, one bit is sent per round, and both must output $f(x,y)$. $R^{cc-pub}_\epsilon(f)$ is the least number of bits of an $\epsilon$-error public-coin protocol.

The network $G(\Gamma,d,p)$ consists of $\Gamma$ paths $\mathcal P^1,\dots,\mathcal P^\Gamma$ with $d^p$ vertices $v^\ell_0,\dots,v^\ell_{d^p-1}$ each, a complete $d$-ary tree $\mathcal T$ of depth $p$ with vertices $u^\ell_0,\dots,u^\ell_{d^\ell-1}$ at level $\ell$, and spoke edges joining each leaf $u^p_j$ to $v^\ell_j$ on every path. The inputs sit at the two extreme leaves, $s=u^p_0$ and $r=u^p_{d^p-1}$. The $i$-right set $R_i$ consists of all path vertices at positions $j\ge i$, the leaves $u^p_j$ with $j\ge i$, and their ancestors; the $i$-left set $L_i$ is the mirror image, and $L_0=V\setminus\{r\}$, $R_0=V\setminus\{s\}$. $C_{R_t}$ denotes the vector of states of the vertices of $R_t$ at the end of round $t$.

Formalization targets

Goal: Theorem 3.1 (Simulation Theorem)

If a public-coin algorithm on $G(\Gamma,d,p)$ computes $f$ with $\epsilon$-error in $T$ rounds and

$$T<\frac{d^p-1}{2},$$

then some public-coin two-party protocol computes $f$ with $\epsilon$-error using at most

$$2\,d\,p\,B\,T\ \text{bits},\qquad\text{i.e.}\qquad R^{cc-pub}_\epsilon(f)\le 2dpB\,R^{G(\Gamma,d,p)}_\epsilon(f).$$

Milestones

1. Observation 3.3: the configuration of $U$ at round $t$ is determined by the configuration of $U'\supseteq U$ at round $t-1$ and the messages into $U$ from outside $U'$.
2. §3.3 edge count: for $0<t<(d^p-1)/2$, at most $dp$ edges join $V\setminus R_{t-1}$ to $R_t$ (and $V\setminus L_{t-1}$ to $L_t$).
3. Inclusion from the proof of Lemma 3.4: $V\setminus R_{t-1}\subseteq L_{t-1}$ (and its mirror image).
4. Lemma 3.4: $C_{R_t}=g_R(C_{R_{t-1}},M_1,\dots,M_{dp})$ for $dp$ messages of $B$ bits sent from $L_{t-1}$, with $g_R$ and the message edges fixed before the inputs; and symmetrically for $C_{L_t}$.

Significance

The theorem turns any lower bound $R^{cc-pub}_\epsilon(f)=\Omega(b)$, such as those for set disjointness and equality, into a round lower bound on $G(\Gamma,d,p)$: an algorithm with $T<(d^p-1)/2$ rounds forces $T\ge R^{cc-pub}_\epsilon(f)/(2dpB)$. Choosing the parameters gives the paper's bounds of order $\sqrt{n/(B\log n)}$ rounds for verification and approximation problems (§§4–7), and the same reduction underlies a large body of later CONGEST lower bounds.

The result has been proved since 2011. A machine-checked version would provide the first formal model of synchronous bandwidth-limited message passing and of public-coin two-party protocols on the platform, together with a verified reduction between them. No formalization of the theorem, of the B model, or of two-party communication protocols is known to exist in Mathlib or on the platform.

Difficulty

The informal proof is short; the work lies in making the information flow precise. The naive simulation, in which Alice simulates the vertices near $s$ and Bob those near $r$, fails because the cut between the two halves contains $\Gamma$ path edges plus the spokes, and $\Gamma$ can be large: sending every message across it costs $\Gamma B$ bits per round. The argument must instead let both parties' simulated regions shrink by one path position per round, so that the only messages crossing into Bob's region come from $p$ tree vertices with $d$ children each. Making this rigorous requires a careful accounting of which vertices belong to $R_t$, which edges leave $V\setminus R_{t-1}$, and why the functions that update the configurations do not depend on the other party's input.

Formalization scope

• Network. Vertices are (Fin Γ × Fin (d^p)) ⊕ Σ ℓ : Fin (p+1), Fin (d^ℓ); paths are numbered from $0$. The children of $u^\ell_i$ are $u^{\ell+1}_{di+k}$, $0\le k<d$. $L_i,R_i$ are Finsets defined for every $i$, with the paper's special case at $i=0$. The nodes $s,r$ require $d^p\ge1$.
• Messages are exactly $B$ bits (Fin B → Bool) on every directed edge in every round. Optional or variable-length messages would let silence carry information and make the theorem false (e.g. at $B=0$).
• Algorithms. Inputs enter only through the initial states of $s$ and $r$; a vertex receives a fixed dummy from non-neighbours. Running time is a fixed number $T$ of rounds, outputs read after round $T$; this is equivalent to the paper's worst-case time.
• Randomness is a PMF on an arbitrary type, shared by all vertices (resp. both parties); $\epsilon$-error requires both outputs to be correct on the same random string, and $\epsilon\ge0$.
• Protocols send one bit per round, so cost equals bits exchanged. Alice's moves read only $x$ and the transcript, Bob's only $y$. Modelling the two-party side as a two-vertex B-model network would carry two bits per round and weaken the constant $2dpB$ by a factor of $2$; the formalization does not do this.
• Lemma 3.4 is stated with the functions $g_L,g_R$ and the message edges chosen before the inputs. A version where they may depend on $(x,y)$ is trivially true and is ruled out.
• The "in other words" inequality between the minimal complexities is not posed through sInf, which would be $0$ on an empty set; the goal is stated for every algorithm.

Contributions welcome: proofs of the milestones, and reusable infrastructure for executions of message-passing algorithms (locality lemmas such as Observation 3.3 hold on any graph).

Selected references

• A. Das Sarma, S. Holzer, L. Kor, A. Korman, D. Nanongkai, G. Pandurangan, D. Peleg, R. Wattenhofer, Distributed Verification and Hardness of Distributed Approximation, SIAM J. Comput. 41(5), 2012, 1235–1265. https://doi.org/10.1137/11085178X
• M. Elkin, An Unconditional Lower Bound on the Time-Approximation Trade-off for the Distributed Minimum Spanning Tree Problem, SIAM J. Comput. 36(2), 2006, 433–456. https://doi.org/10.1137/S0097539704441848
• D. Peleg, V. Rubinovich, A Near-Tight Lower Bound on the Time Complexity of Distributed Minimum-Weight Spanning Tree Construction, SIAM J. Comput. 30(5), 2000, 1427–1442. https://doi.org/10.1137/S0097539700369740
• D. Peleg, Distributed Computing: A Locality-Sensitive Approach, SIAM, 2000. https://doi.org/10.1137/1.9780898719772
• E. Kushilevitz, N. Nisan, Communication Complexity, Cambridge University Press, 1997. https://doi.org/10.1017/CBO9780511574948

Motivation

Networks of coupled oscillators model generators in an electric power grid, pacemaker cells, Josephson junction arrays and many other systems in which units with their own rhythm interact through their phase differences. Dörfler and Bullo (arXiv:0910.5673v4; SIAM J. Control Optim. 50(3), 2012, doi:10.1137/110851584) show that, after a singular-perturbation reduction, the transient-stability question for a lossy power network with non-uniform generators becomes a synchronization question for a non-uniform Kuramoto model: oscillators with different damping coefficients, different natural frequencies, an arbitrary coupling graph and phase shifts induced by line losses.

This mission concerns the cleanest regime of that model: lossless coupling and natural frequencies proportional to the damping. There the oscillators do more than agree on a frequency; they agree on a phase. For the classic Kuramoto model (Kuramoto, 1975) with identical frequencies, phase synchronization from inside an open half-circle was obtained by consensus methods for nonlinear coupled systems (Lin, Francis and Maggiore, 2007) and by Jadbabaie, Motee and Barahona (2004). Theorem V.10 of Dörfler–Bullo extends this to non-uniform damping, directed coupling with a globally reachable node, and gives an explicit worst-case rate for symmetric coupling. The proof rests on the contraction theory of time-varying consensus protocols (Moreau, 2004).

Setting

There are $n \ge 2$ oscillators. Oscillator $i$ has a phase $\theta_i$ on the circle, a damping coefficient $D_i > 0$ and a natural frequency $\omega_i \in \mathbb R$. Oscillators interact through coupling weights $P_{ij} \ge 0$ ($i \ne j$, with $P_{ii} = 0$) and phase shifts $\varphi_{ij} \in [0, \pi/2[$. The non-uniform Kuramoto model (8) is

$$D_i\,\dot\theta_i = \omega_i - \sum_{j=1}^n P_{ij}\sin(\theta_i - \theta_j + \varphi_{ij}), \qquad i = 1,\dots,n .$$

The weights define a directed graph with an edge from $i$ to $j$ whenever $P_{ij} > 0$; a globally reachable node is a node $k$ to which every node has a directed path. For $\gamma \in [0,\pi]$ the closed arc set $\bar\Delta(\gamma)$ is the set of configurations whose angles all lie in a closed arc of length $\gamma$.

This mission assumes zero phase shifts, $\varphi_{\max} = \max_{i,j}\varphi_{ij} = 0$, and proportional frequencies, $\omega_i / D_i = \bar\omega$ for all $i$. The phases synchronize exponentially to a trajectory $\theta_\infty(t)$ when there are $C$ and $\lambda > 0$ with $|\theta_i(t) - \theta_\infty(t)| \le C e^{-\lambda t}$ for all $i$ and $t \ge 0$.

For the rate, $L(a_{ij}) = \mathrm{diag}(\sum_j a_{ij}) - A$ is the Laplacian of a weight array, $\lambda_2(L(P_{ij}))$ is its second-smallest eigenvalue (the algebraic connectivity) when $P = P^T$, $\cos\angle(D\mathbf 1,\mathbf 1) = \sum_i D_i / (\sqrt n \sqrt{\sum_i D_i^2})$, $D_{\max} = \max_i D_i$, $D_{\min} = \min_i D_i$, and $\mathrm{sinc}(x) = \sin(x)/x$.

Formalization targets

Goal: Theorem V.10 (Phase synchronization)

For every solution with $\theta(0) \in \bar\Delta(\gamma)$, $\gamma \in [0,\pi[$:

1. there is $c \in [\theta_{\min}(0), \theta_{\max}(0)]$ such that the phases synchronize exponentially to $\theta_\infty(t) = c + \bar\omega t$;
2. if $P = P^T$, they synchronize exponentially to the weighted mean angle $\theta_\infty(t) = \sum_i D_i\theta_i(0)/\sum_i D_i + \bar\omega t$, and $\delta(t) = \theta(t) - \theta_\infty(t)\mathbf 1$ obeys

$$\|\delta(t)\|_2 \le \sqrt{D_{\max}/D_{\min}}\;\|\delta(0)\|_2\; e^{-\lambda_{\mathrm{ps}} t}, \qquad \lambda_{\mathrm{ps}} = \frac{\lambda_2(L(P_{ij}))\,\mathrm{sinc}(\gamma)\,\cos(\angle(D\mathbf 1,\mathbf 1))^2}{D_{\max}} .$$

Milestones, in the order the proof uses them

• Proof of V.10, p. 27: at a configuration in $\bar\Delta(\gamma)$ with extreme indices $m,\ell$, the arc-length derivative $\dot\theta_m - \dot\theta_\ell = -\sum_k\big(\tfrac{P_{mk}}{D_m}\sin(\theta_m-\theta_k) + \tfrac{P_{\ell k}}{D_\ell}\sin(\theta_k-\theta_\ell)\big)$ is $\le 0$.
• Proof of V.10, p. 27: $\bar\Delta(\gamma)$ is positively invariant for every $\gamma \in [0,\pi[$.
• (43): in the rotating frame $\theta \mapsto \theta - \bar\omega t$ the model is the consensus protocol $\dot\theta_i = -\sum_j a_{ij}(t)(\theta_i - \theta_j)$ with $a_{ij}(t) = (P_{ij}/D_i)\,\mathrm{sinc}(\theta_i(t)-\theta_j(t)) > 0$ on every edge.
• (44): for $P = P^T$, $\tfrac{d}{dt}D\theta = -L(w_{ij}(t))\theta$ in the rotating frame, so $\sum_i D_i\theta_i(t) = \sum_i D_i\theta_i(0) + \bar\omega t\sum_i D_i$.
• Theorem V.10 1) on its own.

Significance

Theorem V.10 gives phase synchronization of non-uniform oscillators from every initial configuration inside an open half-circle, for directed coupling graphs that need only a globally reachable node, and identifies the limit phase: anywhere in the initial range in general, the damping-weighted mean under symmetric coupling. The rate $\lambda_{\mathrm{ps}}$ separates three effects: graph connectivity ($\lambda_2$), initial phase cohesiveness ($\mathrm{sinc}(\gamma)$) and non-uniformity of the damping ($\cos\angle(D\mathbf 1,\mathbf 1)$, $D_{\max}$). For the classic Kuramoto model the statements reduce to known results ([19] and [33] of the paper).

The result is proved in the paper; no machine-checked proof is known. A formal proof needs a Dini-derivative argument for the maximum of finitely many smooth functions along an ODE, a contraction theorem for linear time-varying consensus with positive, bounded weights on a graph with a globally reachable node, and a Courant–Fischer bound on the weighted disagreement. Each is a reusable piece of infrastructure for networked control and synchronization.

Difficulty

The obvious argument linearizes: $\sin(\theta_i - \theta_j) \approx \theta_i - \theta_j$, so the model looks like linear consensus. That only holds near the diagonal; from an arc of length close to $\pi$ the effective weights $\mathrm{sinc}(\theta_i - \theta_j)$ come close to zero and depend on the state, so neither a fixed Laplacian nor a local linearization covers the claimed region. One needs first that the arc never grows, which is a statement about a non-smooth function (the arc length) along trajectories, and then exponential convergence of a consensus protocol whose weights are time-varying and, for directed graphs, non-symmetric, so there is no quadratic Lyapunov function in general. For the explicit rate the disagreement vector is orthogonal to $D\mathbf 1$, not to $\mathbf 1$, and the angle between the two hyperplanes has to be controlled.

Formalization scope

Angles are represented by real lifts $\theta \in \mathbb R^n$; the vector field is $2\pi$-periodic in each coordinate, so solutions on the torus are projections of solutions on $\mathbb R^n$. $\theta \in \bar\Delta(\gamma)$ is encoded as $\theta_i - \theta_j \le \gamma$ for all $i,j$ on the initial lift, and every conclusion (invariance, $\theta_{\min}(0)$, $\theta_{\max}(0)$, the weighted mean, the convergence bounds) refers to that lift and the same continuous lifted trajectory, which is at least as strong as the statement on the torus. A solution is a curve on $[0,\infty)$ whose derivative within $[0,\infty)$ equals the vector field at every $t \ge 0$; statements quantify over every such curve. The model is stated with the paper's general field $D_i^{-1}(\omega_i - \sum_j P_{ij}\sin(\theta_i - \theta_j + \varphi_{ij}))$ and hypotheses $\varphi_{ij} = 0$, $\omega_i/D_i = \bar\omega$ ($\bar\omega$ arbitrary, not set to zero).

Conventions and corrections, each disclosed in the item's Formalization Note:

• $n \ge 2$, $P_{ii} = 0$ and $P_{ij} \ge 0$ for $i \ne j$ are the paper's conventions (§V allows zero and non-symmetric weights).
• (42) is printed with a leading minus sign; the rate is a decay exponent and is stated as the positive number above.
• The page says only "a rate no worse than $\lambda_{\mathrm{ps}}$"; the stated bound uses the constant $\sqrt{D_{\max}/D_{\min}}$ that the referenced proof of Theorem V.1 2) produces (p. 19).
• "$a_{ij}(t)$ is strictly positive" in (43) is stated on the edges, $P_{ij} > 0$; elsewhere $a_{ij} = 0$.
• $\|\cdot\|_2$ is the Euclidean norm, written out (Mathlib's default norm on functions $\mathrm{Fin}\,n \to \mathbb R$ is the sup norm); $\lambda_2$ is the platform definition AlonMilman.PropertyT.lambda1 applied to the symmetric Laplacian.

Exponential convergence requires a rate $\lambda > 0$; a statement with $\lambda = 0$ or with a solution predicate that no curve satisfies would be trivial. The synchronous trajectory $\theta_i(t) = c + \bar\omega t$ satisfies the solution predicate, so the hypotheses are satisfiable.

Infrastructure welcome beyond this mission: upper Dini derivatives and comparison lemmas for maxima of differentiable functions, exponential stability of linear time-varying consensus (Moreau's theorem), and Laplacian ordering $\mathrm{sinc}(\gamma)L(P) \preceq L(w)$ for entrywise-dominated weights.

Selected references

• F. Dörfler and F. Bullo, Synchronization and Transient Stability in Power Networks and Nonuniform Kuramoto Oscillators, SIAM J. Control Optim. 50(3), 2012; this mission cites the arXiv preprint v4. https://arxiv.org/abs/0910.5673v4, https://doi.org/10.1137/110851584
• Y. Kuramoto, Self-entrainment of a population of coupled non-linear oscillators, Lecture Notes in Physics 39, Springer, 1975. https://doi.org/10.1007/BFb0013365
• L. Moreau, Stability of continuous-time distributed consensus algorithms, IEEE Conference on Decision and Control, 2004. https://arxiv.org/abs/math/0409010
• Z. Lin, B. Francis and M. Maggiore, State agreement for continuous-time coupled nonlinear systems, SIAM J. Control Optim. 46(1), 2007. https://doi.org/10.1137/050626405
• N. Chopra and M. W. Spong, On exponential synchronization of Kuramoto oscillators, IEEE Trans. Automatic Control 54(2), 2009. https://doi.org/10.1109/TAC.2008.2007884

Motivation

Transient stability of a power grid asks whether the generators of the network return to synchronous operation after a large disturbance such as a fault or a line trip. In the classical network-reduced model the rotor angles obey second-order swing equations, and stability certificates usually come from energy functions evaluated numerically. Dörfler and Bullo (arXiv:0910.5673v4; SIAM J. Control Optim. 50(3), 2012) relate this problem to a first-order system of coupled phase oscillators, the non-uniform Kuramoto model, and derive purely algebraic conditions on the network parameters under which the oscillators synchronize. Such conditions read as "the network connectivity dominates non-uniformity, losses and lack of phase cohesiveness" and are checked from the data alone, without simulation.

The paper gives two such sufficient conditions. This mission formalizes the second, Theorem V.5, which measures connectivity by the algebraic connectivity of the lossless coupling and therefore applies to sparse (connected, not necessarily complete) networks. A companion mission treats Theorem V.3, the condition for complete graphs.

Timeline. For the classical Kuramoto model, Jadbabaie, Motee and Barahona (ACC, 2004) and Chopra and Spong (IEEE TAC, 2009) analysed synchronization with the Lyapunov function $\|H\theta\|_2^2$, and Chopra and Spong proved frequency synchronization under cohesive phases. Dörfler and Bullo (2009–2012) extended the analysis to non-uniform time constants $D_i$, phase shifts $\varphi_{ij}$ and non-complete graphs, using a weighted Lyapunov function.

Setting

There are $n\ge2$ oscillators with phases $\theta_i$, time constants $D_i>0$, natural frequencies $\omega_i\in\mathbb R$, coupling weights $P_{ij}\ge0$ and phase shifts $\varphi_{ij}\in[0,\pi/2[$ ($i\ne j$), with $P_{ii}=\varphi_{ii}=0$. The non-uniform Kuramoto model is

$$D_i\dot\theta_i=\omega_i-\sum_{j=1}^nP_{ij}\sin(\theta_i-\theta_j+\varphi_{ij}),\qquad i=1,\dots,n. \tag{8}$$

In this mission $P=P^T$, and its non-zero entries induce a connected graph.

• $H\in\mathbb R^{n(n-1)/2\times n}$ is the incidence matrix of the complete graph: $H\theta=(\theta_2-\theta_1,\dots)$ lists all pairwise differences, and $\|H\theta\|_2^2=\sum_{i<j}(\theta_i-\theta_j)^2$.
• $\Delta(\gamma)$ is the set of configurations contained in an open arc of length $\gamma$, i.e. $\max_{i,j}|\theta_i-\theta_j|<\gamma$.
• The Laplacian of a symmetric matrix $A$ is $L(a_{ij})=\operatorname{diag}(\sum_ja_{ij})-A$ and $\lambda_2(L(a_{ij}))$ is its second-smallest eigenvalue, the algebraic connectivity. The lossless coupling is the matrix $(P_{ij}\cos\varphi_{ij})$.
• $\kappa=\sum_kD_k$, $\alpha=\sqrt{\min_{i\ne j}\{D_iD_j\}/\max_{i\ne j}\{D_iD_j\}}$, $\varphi_{\max}=\max_{i,j}\varphi_{ij}$, $\Omega=\sum_i\omega_i/\sum_iD_i$.
• The critical value is

$$\lambda_{\mathrm{critical}}=\frac{\|HD^{-1}\omega\|_2+\sqrt n\,\big\|\big[\sum_j\tfrac{P_{1j}}{D_1}\sin\varphi_{1j},\dots,\sum_j\tfrac{P_{nj}}{D_n}\sin\varphi_{nj}\big]\big\|_2}{\cos(\varphi_{\max})(\kappa/n)\alpha/\max_{i\ne j}\{D_iD_j\}}. \tag{33}$$

• The radii $\gamma_{\max}\in\,]\pi/2-\varphi_{\max},\pi]$ and $\gamma_{\min}\in[0,\pi/2-\varphi_{\max}[$ solve $\operatorname{sinc}(\gamma_{\max})/\operatorname{sinc}(\pi/2-\varphi_{\max})=\sin(\gamma_{\min})/\cos(\varphi_{\max})=\lambda_{\mathrm{critical}}/\lambda_2(L(P_{ij}\cos\varphi_{ij}))$.

Formalization targets

Goal: Theorem V.5 (Synchronization condition II)

If $\lambda_2(L(P_{ij}\cos\varphi_{ij}))>\lambda_{\mathrm{critical}}$, then

1. for every $\gamma\in[\gamma_{\min},\alpha\gamma_{\max}]$ the set $\{\theta\in\Delta(\pi):\|H\theta\|_2\le\gamma\}$ is positively invariant, and every solution with $\theta(0)\in\Delta(\pi)$, $\|H\theta(0)\|_2<\alpha\gamma_{\max}$ eventually satisfies $\|H\theta(t)\|_2\le\gamma$ for every $\gamma>\gamma_{\min}$;
2. for every such solution the frequencies converge exponentially to a common $\dot\theta_\infty\in[\dot\theta_{\min}(0),\dot\theta_{\max}(0)]$; if $\varphi\equiv0$, then $\dot\theta_\infty=\Omega$ and the rate is no worse than

$$\lambda_{\mathrm{fe}}(\gamma)=\lambda_2(L(P_{ij}))\cos(\gamma)\cos(\angle(D\mathbf 1,\mathbf 1))^2/D_{\max}\qquad(\gamma\in\,]\gamma_{\min},\pi/2[).$$

Milestones

Lemma V.8 (the identity (36) that replaces $HD^{-1}H^T$ by $\kappa$), Lemma V.9 (a quadratic-form bound by $\lambda_2$), the sinc estimate and the bound $\tilde X$ on the lossy coupling (p. 25), the Lyapunov-derivative bound (37), the sandwich bounds (39) on $W$, the existence and uniqueness of $\gamma_{\min},\gamma_{\max}$ from the analysis of (41), and the eventual entry of every trajectory into $\{\|H\theta\|_2<\pi/2-\varphi_{\max}\}$.

Significance

The condition is checkable from network data: $\lambda_2$ of a weighted Laplacian, two vector norms and the extreme time constants. It applies to sparse networks, where the complete-graph condition of Theorem V.3 does not, and specializes for classical Kuramoto oscillators to $K>\|H\omega\|_2$ (Remark V.7). Through the singular-perturbation argument of Section IV, conditions of this kind certify transient stability of the network-reduced power system.

The result is proved in the paper; no machine-checked version is known. A formalization fixes several points the printed text leaves loose: the norm $\|H\theta\|_2$ is written on p. 23 with a double sum that counts each pair twice; the chain defining $\tilde X$ on p. 25 is printed with its inequalities reversed; and "reaches $\{\|H\theta\|_2\le\gamma_{\min}\}$" holds only asymptotically. The formal statements make each of these precise.

Difficulty

The obvious Lyapunov function, $\|H\theta\|_2^2$, has a sign-indefinite derivative as soon as the $D_i$ differ, because the coupling $P_{ij}/D_i$ is not symmetric. The weighted function $W(H\theta)=\frac14\sum_{i,j}D_iD_j|\theta_i-\theta_j|^2$ restores a symmetric structure, but only through the non-obvious identity (36). After that, the sinusoidal coupling has to be bounded below by a quadratic form on a set where the phase differences stay below $\pi$, the lossy coupling has to be bounded above uniformly in the state, and the resulting ultimate-boundedness argument has to be run with sublevel sets of $W$, which are ellipsoids rather than balls of $\|H\theta\|_2$ unless all $D_i$ coincide. The constants $\alpha$, $\gamma_{\min}$, $\gamma_{\max}$ come from this mismatch, and the passage from sublevel sets back to balls is the most delicate step.

Formalization scope

• Configurations are real lifts $\theta\in\mathbb R^n$; $\Delta(\pi)$ means $\theta_i-\theta_j<\pi$ for all $i,j$, and $\|H\theta\|_2$ is the pair-sum norm. A solution is a function $\theta:\mathbb R\to\mathbb R^n$ with right derivative at $0$ and derivative at every $t>0$ equal to the vector field of (8), and statements quantify over every solution. $\dot\theta$ is the vector field evaluated along the solution.
• Added hypotheses: $n\ge2$ (needed for $\lambda_2$ and the extrema over $i\ne j$), and $\varphi_{ij}=\varphi_{ji}$, which the page uses silently (the lossless coupling must be a symmetric Laplacian) and which holds for power networks. $P_{ij}\ge0$ off the diagonal, since §V.B allows zero weights.
• Corrections: $\|H\theta\|_2$ sums over pairs $i<j$; the $\tilde X$ chain is stated as $\|HX\|_2\le\tilde X$; the attraction clause of 1) is stated as "eventually below every $\gamma>\gamma_{\min}$"; the rate of (19) is taken positive (it is printed with a minus sign), and the "Moreover" rate is stated for every $\gamma\in\,]\gamma_{\min},\pi/2[$ because (19) depends on an arc length the theorem does not name. The page's "Moreover, if $\gamma_{\max}=0$" is read as $\varphi_{\max}=0$, a misprint: $\gamma_{\max}>\pi/2-\varphi_{\max}$ is never zero.
• $\gamma_{\min},\gamma_{\max}$ are quantified subject to their defining equations, and a milestone proves they exist and are unique, so they are not free parameters. Condition (33) is satisfiable (equal ratios $\omega_i/D_i$ and $\varphi\equiv0$ give $\lambda_{\mathrm{critical}}=0$), so the goal is not vacuous.
• Source: the arXiv preprint v4 of the SICON article; every page and number refers to that preprint.
• Infrastructure: weighted graph Laplacians, their second eigenvalue and Courant–Fischer-type bounds, incidence matrices, and ultimate-boundedness arguments for ODEs. The Laplacian and incidence-matrix layer is reusable for consensus and network-dynamics missions; contributions on any milestone are welcome.

Selected references

• F. Dörfler, F. Bullo, Synchronization and Transient Stability in Power Networks and Nonuniform Kuramoto Oscillators, SIAM J. Control Optim. 50(3), 2012; preprint arXiv:0910.5673v4. https://arxiv.org/abs/0910.5673v4
• N. Chopra, M. W. Spong, On exponential synchronization of Kuramoto oscillators, IEEE Trans. Automatic Control 54(2), pp. 353–357, 2009 (reference [32] of the source).
• A. Jadbabaie, N. Motee, M. Barahona, On the stability of the Kuramoto model of coupled nonlinear oscillators, American Control Conference, Boston, 2004, pp. 4296–4301 (reference [33] of the source).
• H. K. Khalil, Nonlinear Systems, 3rd ed., Prentice Hall, 2002 (ultimate boundedness, Theorem 4.18; reference [51] of the source).