Papers With

← All papers
First page of Symmetric Extension Complexity of the Spanning Tree Polytope

Symmetric Extension Complexity of the Spanning Tree Polytope

Sebastian Pokutta

math.CO Jun 15, 2026 · v1 math.OC
formalization combinatorics
Read PDF arXiv abstract
TL;DR
The acknowledgments mention a companion Lean 4 formalization of the results, developed with LLM assistance and to be released on GitHub.
Abstract
In this note, we prove a tight lower bound on symmetric extended formulations for the spanning tree polytope of the complete graph. More precisely, let $P_{ST}(K_n)$ be the spanning tree polytope of $K_n$. We show that, for all $n\ge13$, every symmetric extended formulation for $P_{ST}(K_n)$ has at least $\binom n3$ inequalities. Since the classical Martin formulation has a symmetric formulation of size $O(n^3)$, this gives \[ \operatorname{xcs}(P_{ST}(K_n))=Θ(n^3). \]
Problem

The extension complexity of the spanning tree polytope of K_n is known only to lie between Ω(n^2) and O(n^3). The paper asks whether symmetry under vertex relabeling alone forces extended formulations to have Ω(n^3) inequalities.

Approach

A signed weight certificate is built on spanning trees of K_6, using orbits of four path trees under the group permuting two triples. It is lifted to K_n by attaching the remaining vertices as leaves. A small-index theorem for symmetric extensions shows that the resulting affine combination would lie in the polytope while violating a triangle subtour inequality, which gives a contradiction. A companion Lean 4 formalization was produced with LLM assistance.

Results

For all n ≥ 13, every symmetric extended formulation of P_ST(K_n) has at least C(n,3) inequalities. Together with Martin's O(n^3) symmetric formulation, this gives xcs(P_ST(K_n)) = Θ(n^3).