Linear algebra

Motivation

Many polytopes of combinatorial optimization have exponentially many facets, yet linear optimization over them is tractable because they are projections of simpler convex sets: affine slices of a nonnegative orthant (linear programming) or of the cone of positive semidefinite matrices (semidefinite programming). The size of such a representation, the number of variables of the extended formulation, is the natural measure of how compactly a polytope can be optimized over. Yannakakis (Expressing combinatorial optimization problems by linear programs, JCSS 1991) characterized polyhedral representations through nonnegative factorizations of the slack matrix. Gouveia, Parrilo and Thomas (arXiv:1111.3164, Mathematics of Operations Research 2013) extended the characterization to lifts into arbitrary closed convex cones, in particular to cones of positive semidefinite matrices.

The stable set polytope of a graph is the standard test case. For a perfect graph on $n$ vertices it is a linear image of an affine slice of the cone of $(n+1)\times(n+1)$ positive semidefinite matrices (Lovász's theta body construction, stated in the paper as Theorem 5.1 with a citation to Lovász & Schrijver, SIAM J. Optim. 1991); this is the reason the maximum weight stable set problem is solvable in polynomial time on perfect graphs. The question addressed by this mission is whether a smaller matrix size could suffice. Theorem 5.2 of Gouveia–Parrilo–Thomas answers it: for every graph on $n$ vertices, matrices of size $n$ do not suffice.

Setting

Let $G$ be a graph with vertex set $V = \{1,\dots,n\}$. A set $S \subseteq V$ is stable if no edge joins two of its elements, and its incidence vector $\chi_S \in \{0,1\}^n$ has $(\chi_S)_i = 1$ exactly when $i \in S$. The stable set polytope is

$$\mathrm{STAB}(G) = \mathrm{conv}\{\chi_S : S \text{ stable}\} \subseteq \mathbb R^n .$$

Let $\mathcal S^k_+$ be the cone of $k \times k$ real symmetric positive semidefinite matrices, with the trace inner product $\langle A, B\rangle = \mathrm{tr}(AB)$, under which it is self-dual. For a closed convex cone $K$, a set $C$ has a $K$-lift if $C = \pi(K \cap L)$ for an affine subspace $L$ and a linear map $\pi$; the lift is proper if $L$ meets the interior of $K$.

For a polytope $P$ with vertices $p_1,\dots,p_v$ and facet inequalities $h_1(x) \ge 0, \dots, h_f(x) \ge 0$, the slack matrix is the nonnegative $v\times f$ matrix $(h_j(p_i))$. A $K$-factorization of a nonnegative matrix $M$ assigns $a^i \in K$ to each row and $b^j \in K^*$ to each column with $\langle a^i, b^j\rangle = M_{ij}$. In Lean the objects are stab, HasPSDLift, HasConeLift, HasProperConeLift, IsSlackMatrix, HasConeFactorization and HasPSDFactorization in the namespace ConeLifts.StableSet.

Formalization targets

Goal: Theorem 5.2

For every $n \ge 1$ and every graph $G$ on $n$ vertices,

$$\neg\ \exists\, L,\ \pi:\quad \mathrm{STAB}(G) = \pi(\mathcal S^n_+ \cap L).$$

The statement excludes all lifts, proper or not, and holds for every graph, perfect or not.

Milestones

1. Theorem 3.3 (first sentence). If a full-dimensional polytope $P$ with the origin in its interior has a proper $K$-lift, then every slack matrix of $P$ admits a $K$-factorization.
2. Rows of the submatrix. The origin and $e_1,\dots,e_n$ are vertices of $\mathrm{STAB}(G)$.
3. Columns of the submatrix. For $n \ge 1$, each $\{x \in \mathrm{STAB}(G) : x_i = 0\}$ is a facet, and some facet does not contain the origin.
4. The core lemma. For every $s \in \mathbb R^n$ the block matrix

$$S' = \begin{pmatrix} 1 & 0_n \\ s & I_n\end{pmatrix}$$

has no $\mathcal S^n_+$-factorization.

Significance

Theorem 5.2 shows that the semidefinite representation of $\mathrm{STAB}(G)$ for perfect graphs has the smallest possible matrix size: $n+1$ cannot be lowered to $n$. As Remark 5.3 of the paper notes, the same argument shows that no polytope in $\mathbb R^n$ with a vertex at which it locally looks like the nonnegative orthant has an $\mathcal S^n_+$-lift. It is also an instance of the factorization method: a statement about all possible semidefinite representations is reduced to a finite obstruction on a small submatrix of the slack matrix.

The theorem is proved in the paper. To the best of our knowledge no machine-checked proof of it, of the factorization theorem for cone lifts, or of any positive semidefinite lower bound for a polytope exists in Mathlib or on this platform. A formalization produces reusable statements about positive semidefinite factorizations, slack matrices and lifts, and a verified instance of the general lower-bound technique.

Difficulty

The step from lifts to factorizations is where the direct argument fails. Theorem 3.3 applies only to proper lifts and only to polytopes with the origin in their interior, while the goal concerns all lifts of a polytope that has the origin as a vertex. Applying Theorem 3.3 to $\mathrm{STAB}(G)$ and an arbitrary lift therefore does not match its hypotheses, and the printed proof does not spell out how the two gaps are closed (see Formalization scope). Theorem 3.3 itself is a consequence of the general factorization theorem of the paper (Theorem 2.4), whose proof rests on conic duality. The core lemma about $S'$ is a statement about every family of $2(n+1)$ positive semidefinite matrices, so it cannot be settled by any finite search.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n); vertex $i+1$ of the paper is i : Fin n; graphs are SimpleGraph (Fin n) and stability is SimpleGraph.IsIndepSet. Vertices of a polytope are Set.extremePoints ℝ. $\mathcal S^k_+$ is the set of real $k\times k$ matrices satisfying Matrix.PosSemidef (which includes symmetry), and the ambient space of a positive semidefinite lift is all $k \times k$ matrices; this does not change which sets have lifts, because a lift in the symmetric matrices extends linearly and a lift in all matrices restricts to them. Positive semidefinite factorizations require both factor families to be positive semidefinite and use $\mathrm{tr}(A_iB_j)$.

Reading decisions: the goal assumes $n \ge 1$, the paper's meaning of "a graph with $n$ vertices", since for $n = 0$ the polytope $\{0\}$ is the image of $\mathcal S^0_+$ and the printed statement fails. Milestone 3 also assumes $n \ge 1$, and so does Milestone 1 (Theorem 3.3): in $\mathbb R^0$ the point $\{0\}$ has a proper lift to the whole space $\mathbb R^m$, whose dual cone $\{0\}$ cannot factor the slack matrix $(1)$. In Milestone 4 the column $*_n$ is an arbitrary real vector. The slack matrices of Theorem 3.3 are encoded through the identification on p. 9 of the paper: rows are vertices of $P$, columns are extreme points $y$ of the polar $P^\circ = \{y : \langle x, y \rangle \le 1\ \forall x \in P\}$, the canonical entry is $1 - \langle p, y\rangle$, and every slack matrix is the canonical one with positively scaled columns. Facets in Milestone 3 are nonempty proper exposed faces of dimension one less than the polytope.

The goal must not be weakened to proper lifts, and lifts must use equality $\mathrm{STAB}(G) = \pi(\mathcal S^n_+ \cap L)$ with $\pi$ linear and $L$ affine; with inclusion, or with arbitrary maps, the statement becomes trivial or false. The core lemma is meaningful only with both factor families positive semidefinite; without that requirement $S'$ factors trivially.

Beyond the milestones, a complete proof of the goal needs two facts the paper uses without stating them as claims of this proof: (a) an $\mathcal S^n_+$-lift that is not proper is a proper lift to a face of $\mathcal S^n_+$ (p. 5), every face of $\mathcal S^n_+$ is isomorphic to some $\mathcal S^r_+$ with $r \le n$ (Example 4.2, p. 12), and an $\mathcal S^r_+$-factorization yields an $\mathcal S^n_+$-factorization; (b) lifts are preserved by affine maps (Proposition 2.9, pp. 6–7), and translating a polytope changes its slack matrices only by positive column scalings, which is how Theorem 3.3 applies to $\mathrm{STAB}(G)$, whose origin is a vertex rather than an interior point. Stating (a) and (b) as separate lemmas is welcome.

Needed infrastructure: positive semidefinite matrices and the trace pairing, the face structure of $\mathcal S^n_+$, invariance of lifts under affine maps, and conic duality for Theorem 3.3. All of these are reusable beyond this mission. Contributions welcome: proofs of the milestones, the bridging facts (a) and (b), and alternative routes to the goal.

Selected references

• J. Gouveia, P. A. Parrilo, R. R. Thomas, Lifts of Convex Sets and Cone Factorizations, Mathematics of Operations Research 38(2):248–264, 2013. arXiv:1111.3164v2. https://arxiv.org/abs/1111.3164
• M. Yannakakis, Expressing combinatorial optimization problems by linear programs, Journal of Computer and System Sciences 43(3):441–466, 1991. https://doi.org/10.1016/0022-0000(91)90024-Y
• L. Lovász, A. Schrijver, Cones of matrices and set-functions and 0-1 optimization, SIAM Journal on Optimization 1(2):166–190, 1991. https://doi.org/10.1137/0801013

Motivation

Optimization problems with orthonormality constraints arise throughout numerical linear algebra and its applications: computing a few eigenvectors or singular vectors, Procrustes problems in statistics and shape analysis, orthogonal factor rotation, independent component analysis, and the orthogonality constraints of electronic-structure calculations. The feasible set of such a problem is the Stiefel manifold of orthonormal $m$-frames in $\mathbb R^n$. Riemannian optimization algorithms on this manifold (Riemannian gradient, Newton and trust-region methods; see Absil, Mahony and Sepulchre, Optimization Algorithms on Matrix Manifolds, 2008) take a step in a tangent direction and then need a retraction: a map that brings the updated point back onto the manifold while agreeing with the geometry to first order.

The most natural way to come back to a constraint set is to take the nearest point. P.-A. Absil and J. Malick, Projection-like retractions on matrix manifolds (SIAM J. Optim. 22(1), 2012; the mission follows the authors' version, HAL hal-00651608v2), show in their Proposition 3.2 that the metric projection onto a smooth submanifold yields a retraction, and then work out the projection explicitly for several matrix manifolds. For the Stiefel manifold, their Proposition 3.4 identifies the projection with a factor of the singular value decomposition, equivalently with the orthonormal factor of the polar decomposition. The paper notes that this result was mentioned without proof in Higham's survey of matrix nearness problems, and gives a proof along the lines of Horn and Johnson, Matrix Analysis, §7.4.

Section 4.5 of the same paper treats a second, "orthographic" retraction on the Stiefel manifold, which corrects a tangent step by a normal vector instead of projecting; for the orthogonal group $\mathbf O_n$ (the case $m=n$) it admits a closed form through a matrix square root (Proposition 4.12).

Setting

Fix natural numbers $1\le m\le n$. Matrices are real, and $\mathbb R^{n\times m}$ carries the Frobenius norm

$$\|X\|^2=\sum_{i,j}X_{ij}^2=\operatorname{trace}(X^\top X).$$

The Stiefel manifold is

$$V_{n,m}=\{X\in\mathbb R^{n\times m}:\ X^\top X=I_m\},$$

the set of matrices with orthonormal columns; $V_{n,n}$ is the orthogonal group $\mathbf O_n$.

The singular values of $X$ are $\sigma_1(X)\ge\sigma_2(X)\ge\dots\ge\sigma_{\min\{n,m\}}(X)\ge0$, the square roots of the eigenvalues of $X^\top X$. A singular value decomposition of $X$ is a factorization $X=U\Sigma V^\top$ with $U=[u_1,\dots,u_n]\in\mathbf O_n$, $V=[v_1,\dots,v_m]\in\mathbf O_m$, and $\Sigma\in\mathbb R^{n\times m}$ zero off its diagonal, with nonnegative nonincreasing diagonal entries. For $\bar X\in V_{n,m}$ every singular value equals $1$; in particular $\sigma_m(\bar X)=1$.

A projection of $X$ onto $V_{n,m}$ is a point $Y\in V_{n,m}$ with $\|X-Y\|\le\|X-Z\|$ for all $Z\in V_{n,m}$. A polar decomposition of $X$ is a factorization $X=WS$ with $W\in V_{n,m}$ and $S\in\mathbb R^{m\times m}$ symmetric positive definite.

Formalization targets

Goal: Proposition 3.4 (p. 10)

Let $\bar X\in V_{n,m}$ and let $X$ satisfy $\|X-\bar X\|<\sigma_m(\bar X)$. For every singular value decomposition $X=U\Sigma V^\top$,

$$\{\,Y:\ Y\text{ is a projection of }X\text{ onto }V_{n,m}\,\}=\Big\{\sum_{i=1}^m u_iv_i^\top\Big\},$$

and $\sum_{i=1}^m u_iv_i^\top$ is the $W$ of the polar decomposition $X=WS$: it is the orthonormal factor of every polar decomposition of $X$, and a polar decomposition with this factor exists.

The statement asserts existence, uniqueness and the closed form of the projection on the whole open ball of radius $\sigma_m(\bar X)$, for whichever singular value decomposition is supplied.

Steps of the proof (milestones)

1. For $Y\in V_{n,m}$: $\|X-Y\|^2=\|X\|^2+m-2\operatorname{trace}(Y^\top X)$.
2. For every $Y\in V_{n,m}$, $\operatorname{trace}(Y^\top X)\le\sum_{i=1}^m\sigma_i$, with equality at $Y=\sum_{i=1}^m u_iv_i^\top$.
3. If $\|X-\bar X\|<\sigma_m(\bar X)$ with $\bar X\in V_{n,m}$, then $X$ has full rank $m$.
4. The polar factor of a full-rank matrix is unique (Horn and Johnson, Theorem 7.3.2).

Further items (§4.5)

$$(S+I)^2=I-\Omega^\top\Omega \tag{4.14}$$

for $X\in\mathbf O_n$, $\Omega$ skew-symmetric and $S$ symmetric with $X+X\Omega+XS\in\mathbf O_n$; and Proposition 4.12,

$$R(X,X\Omega)=X\big(\Omega+\sqrt{I-\Omega^\top\Omega}\big),$$

stated as: $S_+=-I+\sqrt{I-\Omega^\top\Omega}$ is the unique symmetric correction of smallest Frobenius norm.

Significance

Proposition 3.4 makes the projective retraction on the Stiefel manifold computable from one singular value decomposition of an $n\times m$ matrix, and identifies it with the polar factor, which is also what many numerical codes already compute for re-orthonormalization. Combined with Proposition 3.2 of the paper, it yields a second-order-accurate retraction usable in any Riemannian algorithm on $V_{n,m}$. The same statement is the orthogonal Procrustes problem in the special case of a full-rank target: the nearest orthonormal frame to $X$.

The result is classical and proved; the paper's argument is short but cites two external facts (Weyl's perturbation bound for singular values and the uniqueness of the polar decomposition). To our knowledge no machine-checked proof of the nearest-orthonormal-frame property, of the uniqueness of the polar factor, or of the closed form of Proposition 4.12 exists in Mathlib or on this platform. A formalization produces reusable pieces: the trace inequality over the Stiefel manifold, the uniqueness of the polar decomposition, and the full-rank property near $V_{n,m}$, all of which recur in matrix analysis and in the analysis of Riemannian algorithms.

Difficulty

Existence of a nearest point is easy (the Stiefel manifold is compact), and attainment of the trace bound is a direct computation. The content is in two places. First, the bound $\operatorname{trace}(Y^\top X)\le\sum_i\sigma_i$ for every $Y\in V_{n,m}$ requires transporting $Y$ by the orthogonal factors of the singular value decomposition and bounding diagonal entries of a matrix with orthonormal columns. Second, uniqueness does not follow from the trace argument: when $X$ is rank deficient there are many maximizers. Uniqueness needs both a perturbation bound (singular values are 1-Lipschitz in the Frobenius norm, so $\sigma_m(X)>0$ near $\bar X$) and the uniqueness of the polar factor, which in turn rests on the uniqueness of the positive-semidefinite square root of $X^\top X$. Mathlib has singular values of linear maps and the spectral theorem but, at the pinned revision, neither Weyl's inequality for singular values nor the polar decomposition.

For Proposition 4.12, the printed proof compares only two solutions $S_\pm$ of (4.14), while (4.14) has other symmetric solutions (mixed signs of the square roots, or non-diagonal ones on repeated eigenvalues); minimality must be proved against all of them.

Formalization scope

Matrices are Matrix (Fin n) (Fin m) ℝ with the Frobenius norm brought in by open scoped Matrix.Norms.Frobenius. The Stiefel manifold is the set stiefel n m of matrices with Xᵀ * X = 1. Singular values are Mathlib's LinearMap.singularValues of Matrix.toEuclideanLin X, re-indexed to be 1-based as on the page (sv X m is $\sigma_m(X)$). A singular value decomposition is the predicate IsSVD X U S V of display (3.5), and $\sum_{i=1}^m u_iv_i^\top$ is U * E * Vᵀ with E the $n\times m$ rectangular identity (frameOfSVD U V). The projection is the set of nearest points, using the published predicate RandomGradFree.Nonsmooth.IsMetricProjection; "exists and is unique" is equality of that set with a singleton. Positive definiteness is Mathlib's Matrix.PosDef, which over $\mathbb R$ includes symmetry.

Standing assumptions and added hypotheses: $m\le n$ is the page's assumption of §3.3; $0<m$ is added so that $\sigma_m$ is meaningful. The radius is $\sigma_m(\bar X)$ with strict inequality, kept in that form although its value is $1$. Two misprints of the page are corrected in the Lean and kept in the verbatim milestone texts: the display of Proposition 3.4 reads $P_{\mathcal R_r}(X)$ for $P_{V_{n,m}}(X)$, and the distance identity reads $m^2$ for $m$. The uniqueness of the polar factor is stated for positive semidefinite factors under the rank hypothesis, which contains the positive definite case of Proposition 3.4. The matrix square root of §4.5 is defined through Mathlib's spectral theorem; Proposition 4.12 is stated for every admissible symmetric correction, and is vacuous only when no symmetric correction exists.

A trivializing formalization is ruled out: the projection is not taken as a hypothesis or chosen by definition; the goal asserts that the nearest-point set equals the singleton of the explicit matrix, for every singular value decomposition supplied, so neither existence nor uniqueness can be assumed away.

Contributions welcome beyond the stated items: Weyl's inequality $|\sigma_i(X)-\sigma_i(Y)|\le\|X-Y\|$ in Mathlib's singular-value API, existence of a singular value decomposition in the matrix form (3.5), and the polar decomposition with its uniqueness, all reusable well beyond this mission.

Selected references

• P.-A. Absil and J. Malick, Projection-like retractions on matrix manifolds, SIAM J. Optim. 22(1):135–158, 2012. https://doi.org/10.1137/100802529 ; authors' version https://hal.science/hal-00651608v2
• P.-A. Absil, R. Mahony and R. Sepulchre, Optimization Algorithms on Matrix Manifolds, Princeton University Press, 2008. https://doi.org/10.1515/9781400830244
• R. A. Horn and C. R. Johnson, Matrix Analysis, Cambridge University Press, 1985 (cited by the paper in its 1989 printing) (Theorem 7.3.2, §7.4). https://doi.org/10.1017/CBO9780511810817
• N. J. Higham, Matrix nearness problems and applications, in Applications of Matrix Theory (M. J. C. Gover and S. Barnett, eds.), Oxford University Press, 1989, pp. 1–27 (cited by the paper as [15, §4]; no DOI).
• A. Edelman, T. A. Arias and S. T. Smith, The geometry of algorithms with orthogonality constraints, SIAM J. Matrix Anal. Appl. 20(2):303–353, 1998. https://doi.org/10.1137/S0895479895290954

Motivation

Semidefinite programs (SDPs) arise as convex relaxations of combinatorial problems such as maximum cut and the Lovász theta function, and in control and eigenvalue optimization. Interior-point methods solve them reliably but manipulate dense $n\times n$ matrices, which limits the size of the instances they can handle. Burer and Monteiro (Math. Program. 95 (2003)) proposed replacing the matrix variable $X\succeq 0$ by a factorization $X=RR^{T}$ with $R$ having only $r$ columns, and solving the resulting nonconvex program by a first-order augmented Lagrangian method. The approach rests on a theorem of Barvinok (1995) and Pataki (1998): an SDP with $m$ linear constraints has an optimal solution of rank $r$ with $r(r+1)/2\le m$, so a small number of columns suffices.

Because the factorized problem is nonconvex, a local minimum it returns is not automatically a solution of the SDP. Section 2 of the paper gives conditions under which it is. This mission formalizes those conditions, culminating in Proposition 2.5, which justifies the paper's strategy of increasing the rank one column at a time.

Setting

For real $p\times q$ matrices, the trace inner product is $A\bullet B=\operatorname{trace}(A^{T}B)$. The data are symmetric matrices $C, A_1,\dots,A_m\in\mathcal S^n$ and a vector $b\in\mathbb R^m$. The primal SDP and dual SDP are

$$\text{(1)}\quad \min\{C\bullet X : A_i\bullet X=b_i,\ i=1,\dots,m,\ X\succeq0\},\qquad \text{(3)}\quad \max\Big\{b^{T}y : S=C-\sum_{i=1}^m y_iA_i,\ S\succeq0\Big\}.$$

The standing assumptions of the paper are that $A_1,\dots,A_m$ are linearly independent and that there are feasible $X^*$ and $(S^*,y^*)$ with $C\bullet X^*=b^{T}y^*$.

For a positive integer $r\le n$, the low-rank program is

$$(N_r)\qquad \min\{C\bullet(RR^{T}) : A_i\bullet(RR^{T})=b_i,\ i=1,\dots,m,\ R\in\mathbb R^{n\times r}\}.$$

Its Lagrangian is $L(R,y)=C\bullet(RR^{T})-\sum_i y_i(A_i\bullet(RR^{T})-b_i)$, and $S(y)=C-\sum_i y_iA_i$. A feasible $R$ is a local minimum if it minimizes the objective among nearby feasible points; it is a regular point if $A_1R,\dots,A_mR$ are linearly independent; it is a stationary point with multiplier $y$ if $\nabla_RL(R,y)=0$. The injection of $R\in\mathbb R^{n\times r}$ is $\hat R=[\,R\ \ 0\,]\in\mathbb R^{n\times(r+1)}$, obtained by appending a zero column.

Formalization targets

Goal: Proposition 2.5

Let $r<n$ and let $R^*$ be a regular local minimum of $(N_r)$ with multiplier $y^*$, $S^*=S(y^*)$, $S^*R^*=0$. If $\hat R$ is a local minimum of $(N_{r+1})$, then

$$X^*=R^*(R^*)^{T}\ \text{solves (1)}\quad\text{and}\quad (S^*,y^*)\ \text{solves (3)}.$$

Milestones

1. The derivative formulas (9): $\nabla_R(A_i\bullet(RR^T)-b_i)=2A_iR$, $\nabla_RL(R,y)=2SR$, and $L''_{RR}(R,y)[D,D]=2S\bullet(DD^T)$.
2. Proposition 2.3: at a regular local minimum of $(N_r)$ there is a unique $y^*$ with $S^*R^*=0$, and $S^*\bullet(DD^T)\ge0$ for every $D$ with $A_iR^*\bullet D=0$ for all $i$.
3. Proposition 2.1: feasible $X$ and $(S,y)$ are simultaneously optimal if and only if $X\bullet S=0$.
4. Proposition 2.4: a stationary point of $(N_r)$ whose $S^*$ is positive semidefinite gives optimal $X^*=R^*R^{*T}$ and $(S^*,y^*)$.

Significance

Proposition 2.5 is a certificate of global optimality for a nonconvex problem obtained from local information alone. It is the basis of the rank-increase scheme described on p. 8 of the paper: compute a local minimum of $(N_r)$ for a small $r$; if the zero-column extension is still a local minimum of $(N_{r+1})$, the current point solves the SDP; otherwise a better point of $(N_{r+1})$ exists and $r$ is increased. Proposition 2.4 gives the companion test, valid for every $r$: positive semidefiniteness of the multiplier matrix at a stationary point. These statements underlie the later convergence analysis of the method (Burer & Monteiro 2005) and the literature on benign landscapes of low-rank SDP formulations (Boumal, Voroninski & Bandeira 2016).

The results are proved in the paper. What this mission adds is a machine-checked version of the full chain from the standard-form SDP to the rank-increase certificate, including the matrix calculus (9), the first- and second-order necessary conditions for an equality-constrained program over rectangular matrices, and SDP complementary slackness in standard form. No machine-checked proof of these results is recorded in Mathlib or on the platform.

Difficulty

The SDP side (Propositions 2.1 and 2.4) is linear algebra: weak duality and the fact that the trace inner product of two positive semidefinite matrices is nonnegative. The substance lies in Proposition 2.3. The feasible set of $(N_r)$ is a variety cut out by $m$ quadratic equations, and the multiplier rule and, especially, the second-order necessary condition require a constraint qualification and a curve in the feasible set realizing every tangent direction. Mathlib provides a first-order Lagrange multiplier rule, but not the second-order condition on the tangent space. A naive attempt to read Proposition 2.5 off Proposition 2.4 fails: local minimality of $R^*$ alone does not make $S^*$ positive semidefinite (when $r$ is below the minimal optimal rank, it is not); the hypothesis on $(N_{r+1})$ is indispensable.

Formalization scope

Matrices are Matrix (Fin n) (Fin r) ℝ with 0-based indices. The trace inner product is frob A B = trace(Aᵀ * B), defined for rectangular matrices. The data carry explicit symmetry hypotheses C.IsSymm and (A i).IsSymm; without them the formulas (9) are false. Primal feasibility uses Mathlib's PosSemidef, which over $\mathbb R$ includes symmetry. Optimality for (1) and (3) is defined relative to their entire feasible sets. The standing assumptions are a separate predicate carried as a hypothesis by Propositions 2.1, 2.3, 2.4 and 2.5, and every statement about $(N_r)$ carries $0<r$ and $r\le n$ (or $r<n$). Gradients are Fréchet derivatives under the Frobenius norm, identified with matrices through the trace inner product; local minima use IsLocalMinOn on the feasible set of $(N_r)$ together with feasibility. The injection appends the zero column as the last column.

The statement admits several trivializing encodings, all excluded here: optimality defined relative to the factorized feasible set instead of the whole SDP, an empty or unconstrained $(N_r)$ (an unconstrained local minimum or a local minimum without feasibility), a stationarity notion that already includes $S\succeq0$, and an injection other than the zero-column extension.

A complete development needs the matrix calculus of $R\mapsto RR^{T}$, a second-order necessary optimality condition under linear independence of the constraint gradients, and standard-form SDP weak duality and complementary slackness; all of these are reusable well beyond this mission. Proofs of individual milestones, in particular the derivative formulas and Proposition 2.4, are welcome independently of the goal.

Selected references

• S. Burer and R. D. C. Monteiro, A nonlinear programming algorithm for solving semidefinite programs via low-rank factorization, Mathematical Programming 95 (2003), 329–357. https://doi.org/10.1007/s10107-002-0352-8 (statements cited from the authors' manuscript of March 9, 2001)
• A. Barvinok, Problems of distance geometry and convex properties of quadratic maps, Discrete & Computational Geometry 13 (1995), 189–202. https://doi.org/10.1007/BF02574037
• G. Pataki, On the rank of extreme matrices in semidefinite programs and the multiplicity of optimal eigenvalues, Mathematics of Operations Research 23 (1998), 339–358. https://doi.org/10.1287/moor.23.2.339
• R. D. C. Monteiro and M. Todd, Path-following methods for semidefinite programming, in Handbook of Semidefinite Programming, Kluwer, 2000 (source of Proposition 2.1).
• S. Burer and R. D. C. Monteiro, Local minima and convergence in low-rank semidefinite programming, Mathematical Programming 103 (2005), 427–444. https://doi.org/10.1007/s10107-004-0564-1
• N. Boumal, V. Voroninski and A. S. Bandeira, The non-convex Burer–Monteiro approach works on smooth semidefinite programs, NeurIPS 2016. https://arxiv.org/abs/1606.04970

Motivation

Extremal graph theory asks how many edges a graph on $n$ vertices can have without containing a fixed graph $F$. The answer, the Turán number $\mathrm{ex}(n,F)$, and the graphs attaining it, the set $\mathrm{Ex}(n,F)$ of extremal graphs, are known precisely only for special $F$; the Erdős–Stone–Simonovits theorem gives $\mathrm{ex}(n,F) = (1 - \frac{1}{\chi(F)-1} + o(1))\frac{n^2}{2}$, where $\chi(F)$ is the chromatic number.

Spectral extremal graph theory asks the same question with the number of edges replaced by the spectral radius $\lambda(G)$, the largest eigenvalue of the adjacency matrix. Since $\lambda(G) \ge 2e(G)/n$, a spectral bound implies an edge bound, and spectral extremal results are usually stronger than their edge versions. Nikiforov (Linear Algebra Appl. 427, 2007) showed that the Turán graph $T_{n,r}$ maximises $\lambda$ among $K_{r+1}$-free graphs, so for $F = K_{r+1}$ the spectral and the edge extremal graphs coincide. Whether this happens for other $F$ is the subject of the paper.

Timeline:

• 1941 Turán: $T_{n,r}$ is the unique extremal graph for $K_{r+1}$.
• 2003 Chen, Gould, Pfender, Wei (J. Combin. Theory Ser. B 89): $\mathrm{ex}(n, F_{k,r+1}) = e(T_{n,r}) + O(1)$ for $k$ copies of $K_{r+1}$ sharing one vertex.
• 2007 Nikiforov (Linear Algebra Appl. 427): spectral Turán theorem for $K_{r+1}$. 2009 Nikiforov (J. Graph Theory 62): spectral stability for large forbidden subgraphs, the source of Lemma 2.5.
• 2020 Cioabă, Feng, Tait, Zhang (Electron. J. Combin. 27): the spectral extremal graph for the friendship graph $F_k$ lies in $\mathrm{Ex}(n, F_k)$.
• 2022 Cioabă, Desai, Tait (European J. Combin. 99) conjecture: if the graphs in $\mathrm{Ex}(n,F)$ are Turán graphs plus $O(1)$ edges, then the spectral extremal graphs lie in $\mathrm{Ex}(n,F)$ for large $n$. Before the general proof it was known for $K_{r+1}$, the friendship graphs $F_k$, the graphs $H_{s,k}$ (Li, Peng) and the intersecting cliques $F_{k,r}$ (Desai, Kang, Li, Ni, Tait, Wang, arXiv:2108.03587).
• 2022/2023 Wang, Kang, Xue (arXiv:2203.10831; J. Combin. Theory Ser. B, 2023): the conjecture holds in general. This mission formalizes their Theorem 1.2.

Setting

All graphs are finite and simple. For a graph $G$ on $n$ vertices, $A(G)$ is its $0/1$ adjacency matrix and $\lambda(G)$ is the largest eigenvalue of $A(G)$. A graph $G$ is $F$-free if no subgraph of $G$ is isomorphic to $F$. The Turán number $\mathrm{ex}(n,F)$ is the maximum number of edges $e(G)$ over $F$-free graphs $G$ on $n$ vertices, and $\mathrm{Ex}(n,F)$ is the set of $F$-free $n$-vertex graphs with $\mathrm{ex}(n,F)$ edges. The Turán graph $T_{n,r}$ is the complete $r$-partite graph on $n$ vertices with parts of sizes $\lfloor n/r\rfloor$ or $\lceil n/r\rceil$.

The hypothesis on $F$ is: for fixed integers $r \ge 2$ and $a \ge 0$ and all large $n$, $\mathrm{ex}(n,F) = e(T_{n,r}) + a$ and every graph in $\mathrm{Ex}(n,F)$ contains a spanning copy of $T_{n,r}$, i.e. is $T_{n,r}$ plus $a$ edges. The paper states "adding $O(1)$ edges" and fixes the constant at the start of Section 3 (p. 4): "We may assume that the graphs in $\mathrm{Ex}(n,F)$ are obtained from $T_{n,r}$ by adding $a$ edges." The mission follows that reading. Examples: $K_{r+1}$ with $a = 0$, the friendship graphs, and the intersecting cliques $F_{k,r+1}$.

A graph $G$ is spectral extremal for $F$ if it is $F$-free and $\lambda(G) \ge \lambda(G')$ for every $F$-free $G'$ on the same $n$ vertices.

Formalization targets

Goal: Theorem 1.2

For $r \ge 2$, $a \ge 0$ and $F$ satisfying the hypothesis, there is $N$ such that for all $n \ge N$ every spectral extremal graph $G$ for $F$ on $n$ vertices satisfies

$$e(G) = \mathrm{ex}(n,F), \qquad\text{i.e.}\qquad G \in \mathrm{Ex}(n,F).$$

The statement contains no numerical constant, and $N$ depends only on $F$, $r$, $a$.

Milestones

The milestones follow the proof, in order: strict monotonicity of $\lambda$ under proper subgraphs of a connected graph (Lemma 2.3); connectivity of $G$ (Lemma 3.1); the bound $\lambda(G) \ge (1-\frac1r)n - \frac{r}{4n} + \frac{2a}{n}$ (Lemma 3.2); spectral stability for $\chi(F) = r+1$ (Corollary 2.6); for every maximum $r$-cut $V_1 \cup \dots \cup V_r$, $\sum_i e(V_i) \le \varepsilon n^2$ and $|V_i| = (\frac1r \pm 3\sqrt\varepsilon)n$ (Lemma 3.3); a counting inequality for intersections (Lemma 2.8); $e(G[V_i]) \le a$ and minimum degree above $(1 - \frac1r - 3r\varepsilon^{1/3})n$ (Lemma 3.6); at most $2a$ vertices of each part have a neighbour in that part, and all others see every other part completely (Lemma 3.7); Perron entries $x_u \ge 1 - 20a^2r^2/n$ for $a \ge 1$ (Lemma 3.8); $e(G_{in}) - e(G_{out}) \le a$ (Lemma 3.9); balancing two parts of a complete multipartite graph increases $\lambda$ (Lemma 2.7); and the maximum partition is balanced, $|n_i - n_j| \le 1$ (Lemma 3.10).

Significance

The theorem settles the Cioabă–Desai–Tait conjecture: for every $F$ whose extremal graphs are Turán graphs plus a bounded number of edges, the spectral extremal problem reduces to the edge extremal problem for large $n$. This recovers the earlier cases (friendship graphs, the graphs $H_{s,k}$, intersecting cliques) at once, and it turns any future determination of $\mathrm{Ex}(n,F)$ of this type into a spectral result with no further work.

The result is proved on paper; it has no machine-checked proof. Mathlib has Turán's theorem (extremalNumber_top, uniqueness of turanGraph) and the definition of extremalNumber, but no spectral extremal graph theory: no Perron–Frobenius theorem for graphs, no spectral Turán theorem, no stability theorem. The formalization would supply these, and the milestone statements are independently reusable: strict monotonicity of $\lambda$ (Lemma 2.3), the spectral comparison of complete multipartite graphs (Lemma 2.7) and spectral stability (Corollary 2.6) are standard tools of the area.

Difficulty

The natural first idea, comparing $G$ with an extremal graph $H$ by Rayleigh quotients, fails at the start: $\lambda(G) \ge \lambda(H)$ gives only $e(G) \ge e(T_{n,r}) - o(n^2)$, far from $\mathrm{ex}(n,F)$. Closing an additive gap of $O(1)$ edges requires control of the Perron vector to within $O(1/n)$ at every vertex and exact control of the part sizes. The second is the delicate step: an imbalance of one vertex between two parts costs $\Theta(1/n)$ in $\lambda$, while the $a$ extra edges contribute only $O(1/n^2)$ beyond the Turán graph, so the two effects must be compared at different scales. Further, the proof needs the deep spectral stability theorem of Nikiforov (Lemma 2.5), whose own proof is long.

Formalization scope

Graphs on $n$ vertices are SimpleGraph (Fin n), matching Mathlib's extremalNumber n F; $F$ is a graph on any finite type. $\lambda(G)$ is the largest eigenvalue of G.adjMatrix ℝ (index $0$ of Mathlib's decreasingly sorted eigenvalues₀), not an absolute value and not a norm. "$F$-free" is F.Free G (no copy of $F$, not necessarily induced). "Sufficiently large $n$" is ∃ N, ∀ n ≥ N with $N$ chosen after $F, r, a$ and before $G$; "sufficiently small $\varepsilon$" is ∃ ε₀ > 0, ∀ ε ∈ (0, ε₀). Partitions $V_1 \cup \dots \cup V_r$ are labellings Fin n → Fin r whose parts may be empty; the Section 3 lemmas hold for every partition maximising the number of crossing edges. Lemma 3.8 carries the extra hypothesis $a \ge 1$, because as printed it is false for $a = 0$ (for $F = K_{r+1}$ and $r \nmid n$ the Perron vector of $T_{n,r}$ has entries below $1$); the goal does not assume it.

Trivializing formalizations are ruled out: $\lambda$ is not defined from the edge count (which would make spectral and edge extremality the same), the hypothesis on $F$ does not contain the conclusion and is satisfiable (a sorry-free check for $F = K_{r+1}$, $a = 0$ was compiled), the conclusion is $e(G) = \mathrm{ex}(n,F)$ and not a weaker bound, and the threshold is not chosen after $G$.

A complete development needs the Perron–Frobenius theorem for irreducible nonnegative symmetric matrices, the Rayleigh quotient characterisation of $\lambda$, the spectrum of complete multipartite graphs, Nikiforov's spectral stability lemma, and max-cut partition arguments. All of these are reusable beyond this mission, and proofs of any milestone, of the cited Lemmas 2.1, 2.2 and 2.5, or of Nikiforov's spectral Turán theorem are welcome.

Selected references

• J. Wang, L. Kang, Y. Xue, On a conjecture of spectral extremal problems, J. Combin. Theory Ser. B, 2023; arXiv:2203.10831v1 (2022). https://arxiv.org/abs/2203.10831
• S. Cioabă, D. N. Desai, M. Tait, The spectral radius of graphs with no odd wheels, European J. Combin. 99 (2022) 103420.
• S. Cioabă, L. H. Feng, M. Tait, X. D. Zhang, The maximum spectral radius of graphs without friendship subgraphs, Electron. J. Combin. 27(4) (2020) P4.22.
• G. Chen, R. J. Gould, F. Pfender, B. Wei, Extremal graphs for intersecting cliques, J. Combin. Theory Ser. B 89 (2003) 159–171.
• V. Nikiforov, Bounds on graph eigenvalues II, Linear Algebra Appl. 427 (2007) 183–189.
• V. Nikiforov, Stability for large forbidden subgraphs, J. Graph Theory 62(4) (2009) 362–368.
• D. N. Desai, L. Kang, Y. Li, Z. Ni, M. Tait, J. Wang, Spectral extremal graphs for intersecting cliques, arXiv:2108.03587v2 (2021). https://arxiv.org/abs/2108.03587

Motivation

Many control tasks have to settle at a given deadline, not merely eventually. Examples are missile guidance, where the interception time is fixed in advance, and rendezvous or consensus manoeuvres that must finish by a scheduled instant. Prescribed-time stabilization asks for a feedback that brings the state of a system to the origin at a time $T>0$ chosen by the designer, independently of the initial condition, and keeps this property under disturbances. It is stronger than finite-time stabilization, where the settling time depends on the initial state, and stronger than fixed-time stabilization, where it is only bounded uniformly.

Song, Wang, Holloway and Krstić (Automatica 2017) obtained prescribed-time regulation of normal-form systems with feedback gains that grow without bound as $t\to T$. The computations required explicit time derivatives of the gain function. Chitour, Ushirobira and Bouhemou (SIAM J. Control Optim. 2020) recast this construction as time-varying homogeneity: a time-dependent dilation of the state combined with a change of time turns the prescribed-time problem into a standard exponential-stabilization problem on an infinite horizon. The analysis then reduces to linear matrix inequalities. This mission formalizes the linear-feedback part of that paper (§3.1, pp. 1026–1030).

Timeline:

• 2010: Chitour and Sigalotti (SIAM J. Control Optim. 48) prove a Lyapunov LMI for $J_n - b e_n K^T$, uniform over a bounded range $\underline b\le b\le\bar b$.
• 2017: Song, Wang, Holloway and Krstić give prescribed-time regulation with a time-varying feedback.
• 2020: Chitour, Ushirobira and Bouhemou remove the upper bound $\bar b$ (Proposition 10) and derive the prescribed-time estimate by time-varying homogeneity (Corollary 14).

Setting

Fix a positive integer $n$ and a prescribed time $T>0$. Let $(e_i)_{1\le i\le n}$ be the canonical basis of $\mathbb R^n$, and let $J_n$ be the $n$-th Jordan block, $J_n e_i = e_{i-1}$ with $e_0=0$. The perturbed chain of integrators is

$$\dot x(t) = J_n x(t) + \big(d(t) + b(t)u(t)\big) e_n, \qquad t\in[0,T),$$

with state $x(t)\in\mathbb R^n$ and control $u(t)\in\mathbb R$. Here $d$ is a measurable matched disturbance, and $b$ is an uncertain control gain with $b(t)\ge\underline b>0$ and no upper bound.

With weights $r_i = n-i+1$, the dilation is $D^{\mathbf r}_\mu = \operatorname{diag}(\mu^{r_1},\dots,\mu^{r_n})$ and $D_{\mathbf r} = \operatorname{diag}(r_1,\dots,r_n)$. An admissible weight is a continuous function $a\ge0$ on $[0,T]$ with $\int_t^T a>0$ for $t<T$. It defines

$$\lambda(t) = \frac{1}{\int_t^T a(\xi)\,d\xi},\qquad s(t) = \int_0^t\lambda(\xi)\,d\xi,\qquad 0\le t<T.$$

The parameter $\lambda$ blows up at $T$, and $s$ maps $[0,T)$ onto $[0,\infty)$. In the coordinates $y = D^{\mathbf r}_{\lambda(t)}x$ and the time $s$, the system becomes

$$y' = \big(a D_{\mathbf r} + J_n\big)y + (b u + d)e_n .$$

The feedback studied is $u = -K^T D^{\mathbf r}_\eta y$, that is $u(t) = -K^T D^{\mathbf r}_{\eta\lambda(t)}x(t)$ in the original variables, where $K\in\mathbb R^n$ and $\eta\ge1$.

Formalization targets

Goal: Corollary 14 (corrected)

There is a rate $\mu>0$ depending only on $n$ and $\underline b$ such that, for every $T$ and admissible $a$, there are $K$ and $C>0$ with

$$|x_i(t)| \le \frac{1}{(\eta\lambda(t))^{n-i+1}}\Big(C\eta\max(1,\eta^{n-1})e^{-\mu\eta s(t)}\|x(0)\| + C\max_{r\in[0,t]}|d(r)|\Big)$$

for every $\eta\ge1$, every $b\ge\underline b$, every disturbance $d$, every closed-loop solution, every $t\in[0,T)$ and every $1\le i\le n$. Since $\lambda(t)\to\infty$, every coordinate reaches $0$ at the prescribed time $T$.

Milestones

1. §3 (10): $\dot\lambda = a\lambda^2$, $\lambda$ is nondecreasing and tends to $\infty$ at $T$, and $s$ is an increasing $C^1$ bijection $[0,T)\to[0,\infty)$.
2. §3 (7)–(11): the transformed dynamics.
3. Proposition 10: $\exists\rho,S,K$ such that $(J_n - be_nK^T)^TS + S(J_n-be_nK^T)\preceq-\rho\,\mathrm{Id}$ for all $b\ge\underline b$.
4. Proposition 11: the same LMI with $aD_{\mathbf r}$ added, uniformly in $|a|\le C_0$.
5. Proposition 12 (corrected): the ISS estimate (17) in the time $s$.
6. Proposition 13: the $\eta$-scaled LMI (20).

Significance

Corollary 14 says that a linear feedback with a time-varying gain drives the chain of integrators to the origin at the designer's deadline $T$. The guarantee holds for every control gain $b\ge\underline b$, however large, and gives an explicit input-to-state bound for the matched disturbance. The weight $a$ is free, so the blow-up profile of the gain can be chosen, for example to converge faster than polynomially. Proposition 10 removes the upper bound on $b$ from the classical LMI, and is of independent use for high-gain and persistently excited systems.

On formalization: the results are proved on paper; no formalization of them is known. The mission produces checked statements of the LMIs, the time change, and the prescribed-time estimate. Two printed estimates are false as stated, (17) and (23), and the mission states corrected versions (see Formalization scope). Formal proofs would certify the corrected constants.

Difficulty

The obvious approach is to take a Lyapunov function for the constant-coefficient closed loop and differentiate it along trajectories. This fails for two reasons. First, $b$ ranges over an unbounded interval, so no compactness argument yields a common Lyapunov matrix, and a single $S$ and $K$ must work for all $b\ge\underline b$ at once. Second, the transformed system carries the time-varying term $a(s)D_{\mathbf r}$, and in the original time the feedback gain $\lambda(t)$ is unbounded. Estimates must survive both the rescaling by $D^{\mathbf r}_{\eta\lambda(t)}$ and the change of time. Constants that look harmless in the new time, such as the condition number of $S$ and the value $\lambda(0)$, reappear in the original variables, and dropping them makes the printed estimates false.

Formalization scope

Lean representation: vectors of $\mathbb R^n$ are Fin n → ℝ, and coordinate i : Fin n is the paper's index i.val + 1, so $r_i$ = n - i.val. Matrices are Matrix (Fin n) (Fin n) ℝ, and $e_nK^T$ is vecMulVec (eN n) K. Matrix inequalities use the Loewner order (open scoped MatrixOrder), and "real symmetric positive definite" is PosDef. The norm $\|\cdot\|$ is Euclidean, written out as eucNorm. Solutions are Carathéodory solutions in integral form: for every $t$ in the interval, the right-hand side is integrable on $[0,t]$ and the integral identity holds. This matches the paper's measurable $b$ and $d$. The standing assumptions are $n\ge1$ (§3), $T>0$, $a$ continuous and nonnegative on $[0,T]$ with $\int_t^Ta>0$ on $[0,T)$, and $b\ge\underline b>0$. No upper bound on $b$ is assumed anywhere. $\max|d|$ is replaced by an arbitrary bound $D$ of $|d|$ on the interval.

Corrected statements, with milestone texts kept verbatim:

• (17) as printed has no constant on the transient term and fails for $n\ge2$: with $a\equiv1$ and $y(0)=e_1$, $|y_1|$ first increases. Proposition 12 is stated with $C_S$ on that term.
• (23) as printed fails at $t=0$ whenever $\int_0^Ta<1$. The goal is stated with a constant $C$ on the transient term, and $K$ and $C$ may depend on $T$ and $a$. The rate $\mu$ and the disturbance gain $C_S$ depend only on $n$ and $\underline b$, as on the page.
• Proposition 13's undefined $\mu_*$ is the $\rho$ of its statement.
• "$\lambda$ increasing" is read as nondecreasing.
• Corollary 14's "$t\ge0$" is read as $t\in[0,T)$.

Trivializing encodings are ruled out as follows. The integrability clause of IsIntegralSolution prevents a non-integrable right-hand side from integrating to $0$. Every constant is quantified before the objects it must not depend on: the rate $\mu$ before $T$ and $a$, $K$ before $\eta$, and $\rho,S,K$ before $b$. No statement weakens the estimates to mere convergence.

Needed infrastructure: Lyapunov estimates for absolutely continuous solutions, Loewner-order congruence, and interval-integral calculus for the time change. The LMI lemmas and the integral-form solution predicate are reusable in other control missions. Proofs of any milestone are welcome, and so are sharper constants.

Selected references

• Y. Chitour, R. Ushirobira, H. Bouhemou, Stabilization for a Perturbed Chain of Integrators in Prescribed Time, SIAM J. Control Optim. 58(2):1022–1048, 2020. https://doi.org/10.1137/19M1285937
• Y. Song, Y. Wang, J. Holloway, M. Krstić, Time-varying feedback for regulation of normal-form nonlinear systems in prescribed finite time, Automatica 83:243–251, 2017. https://doi.org/10.1016/j.automatica.2017.06.008
• Y. Chitour, M. Sigalotti, On the stabilization of persistently excited linear systems, SIAM J. Control Optim. 48:4032–4055, 2010. https://doi.org/10.1137/080737812

Motivation

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

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

Timeline:

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Theorem 1.1, certificate form

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

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

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

Selected references

• S. Oum and P. Seymour, Approximating clique-width and branch-width, J. Combin. Theory Ser. B 96 (2006) 514–528. https://doi.org/10.1016/j.jctb.2005.10.006
• B. Courcelle and S. Olariu, Upper bounds to the clique width of graphs, Discrete Appl. Math. 101 (2000) 77–114. https://doi.org/10.1016/S0166-218X(99)00184-5
• B. Courcelle, J. A. Makowsky and U. Rotics, Linear time solvable optimization problems on graphs of bounded clique-width, Theory Comput. Syst. 33 (2000) 125–150. https://doi.org/10.1007/s002249910009
• N. Robertson and P. D. Seymour, Graph minors. X. Obstructions to tree-decomposition, J. Combin. Theory Ser. B 52 (1991) 153–190. https://doi.org/10.1016/0095-8956(91)90061-N