Nonnegative rank of the spanning-tree slack matrix

@misc{lemmata:2610.00003,
  title        = {Nonnegative rank of the spanning-tree slack matrix},
  author       = {Sebastian Pokutta},
  howpublished = {Lemmata Repository, lemmata:2610.00003, \url{https://lemmata.iol.berlin/abs/2610.00003}},
  year         = {2026},
  url          = {https://lemmata.iol.berlin/abs/2610.00003},
  note         = {Version a9429cb9cbf5; formal statements checked in Lean 4}
}

A minimum-root decomposition of tree slacks can also accommodate every edge nonnegativity row without adding factors. This gives an explicit cubic upper bound on nonnegative rank, saving $\binom n2$ factors over appending a separate factor for every edge. No symmetry of the factorization is required.

The matrix and the result¶

Nonnegative rank is the smallest inner dimension of a factorization $M=AB$ with $A,B$ entrywise nonnegative. The Lean definition uses extended natural numbers, assigning infinity if no such factorization exists; the explicit witness below makes the rank finite here.

Construction and proof¶

For a tree rooted at $r$, let $p_{T,r}(v)$ be the neighbor of $v$ toward $r$, with $p_{T,r}(r)=r$. For every $r\in S$,

Indeed, the parent-edge map bijects the nonroot vertices with the tree edges. The internal edges of $S$ correspond precisely to the children in $S\setminus\{r\}$ whose parents are also in $S$. Subtracting their number from $|S|-1$ gives the identity, including when the induced forest on $S$ is disconnected.

Index the factors by

The diagonal slots $(0,v,v)$ are special: put $B_{(0,v,v),T}=\mathbf1_{\{0,v\}\in E(T)}$ and $A_{S,(0,v,v)}=0$ for every subtour row. For every other slot $c=(r,v,w)$, put

For an edge row $\{a,b\}$ with $a<b$, its row factor is one at $(0,b,b)$ if $a=0$; if $a>0$, it is one at the two slots $(0,a,b)$ and $(0,b,a)$. All its other coefficients are zero.

This remains cubic, with leading term $n^3/3$. The saving relative to the older append-every-edge count is

Scope and source¶

The formalization constructs parents from unique paths in actual SimpleGraph trees, proves the parent-edge bijection and slack identity, and checks both row families. It does not assume an abstract tree-model correctness interface. The connection between nonnegative rank and extension complexity, an affine extended formulation, and completeness of a polyhedral description are outside this entry. No optimality or literature-priority claim is made.

The construction comes from Sebastian Pokutta’s spanning-tree extension-complexity project: the unpublished note Candidate upper improvement by reusing full-slack factors and the earlier min-split factorization. The source snapshot is commit 75f45e8dd38eae648222e11a99559ed8ec991e2e of symmetric-spanning-tree-lb. The graph lemmas adapt that project’s unique-path and parent-edge proofs. These source notes are not distributed with this entry; the construction and proofs needed here are given in full. The entry is self-contained over the archive’s pinned Mathlib and does not import the source project.

/-- The full standard spanning-tree slack matrix has an explicit nonnegative
factorization with n(n-1)(2n-1)/6 factors, including all nonnegativity rows. -/
theorem fullSlack_factorization (n : ℕ) (hn : 3 ≤ n) :
    Nonempty (NonnegativeFactorization (fullSlack n) (n * (n - 1) * (2 * n - 1) / 6)) := by
  let : NeZero n := ⟨by omega⟩
  simpa only [card_cert] using
    (⟨fullFactorization (n := n)⟩ : Nonempty
      (NonnegativeFactorization (fullSlack n) (Fintype.card (Cert n))))

/-- The nonnegative-rank bound for the actual full graph slack matrix. -/
theorem fullSlack_rank_bound (n : ℕ) (hn : 3 ≤ n) :
    nonnegativeRank (fullSlack n) ≤ ((n * (n - 1) * (2 * n - 1) / 6 : ℕ) : ℕ∞) := by
  obtain ⟨F⟩ := fullSlack_factorization n hn
  exact nonnegativeRank_le F