# Uniform sparsest cut: hardness and semidefinite gaps

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Near-square-root logarithmic integrality gaps for uniform sparsest cut](../../preprints/Near-square-root-logarithmic-integrality-gaps-for-uniform-sparsest-cut-September-24-2026/Near-square-root-logarithmic-integrality-gaps-for-uniform-sparsest-cut-September-24-2026.pdf)

## Scope

The formalized result gives integrality gaps for the Goemans–Linial relaxation of uniform sparsest cut. Along a sequence of instance sizes $n\to\infty$, the ratio of the integral optimum to the positive relaxation optimum is at least $c\sqrt{\log n}/(\log\log n)^3$ for one absolute $c>0$. Every unordered pair has unit demand, and the relaxation uses squared Euclidean distances satisfying the triangle inequalities. The result is an existential sequence, not a bound for every size or a computational hardness theorem.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Uniform sparsest-cut integrality gaps | [UniformSparsestCut.lean](../ComparatorChallenges/UniformSparsestCut.lean) |