Papers With

← All papers
First page of Simple Cuts, Simple Landscape: Dimension-Free Rank Bounds for Burer-Monteiro Factorizations via Rank-Width

Simple Cuts, Simple Landscape: Dimension-Free Rank Bounds for Burer-Monteiro Factorizations via Rank-Width

Hongjin Wu

math.OC Oct 29, 2026 · v1
formalization analysis
Read PDF arXiv abstract
TL;DR
The main theorem and the key energy lower bounds were formally verified in Lean 4, with Lean source files provided as ancillary material.
Abstract
In this work, we study Burer-Monteiro factorizations of semidefinite programs with unit diagonal constraints. For a real symmetric cost matrix whose rank-width over $\mathbb{R}$ is at most $k$, we prove that every non-flat second-order stationary point of the factorized problem is globally optimal whenever the factorization rank is at least $2k$, independently of the matrix size.
Problem

The question is how large the Burer-Monteiro factorization rank must be so that every second-order stationary point of a unit-diagonal semidefinite program is globally optimal. Existing general bounds depend on the matrix size rather than on the structure of the cost matrix.

Approach

The cost matrix structure is measured by its rank-width over the reals. The energy change from a stationary point is split along a rooted rank-decomposition into contributions from two vertex sets plus a cross term. Each part's contribution is lower-bounded using low-rank cut factorizations and the second-order conditions. The main theorem and these lower bounds were machine-checked in Lean 4.

Results

For a cost matrix of rank-width at most k, every non-flat second-order stationary point is globally optimal whenever the factorization rank is at least 2k, independent of the matrix size. The Lean 4 verification covers all stated parameter regimes.