# Deterministic construction of strong thin spanning trees

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

- [The strong thin tree conjecture](../../preprints/The-strong-thin-tree-conjecture-September-23-2026/paper.pdf)
- [A polynomial-time construction of strong thin trees](../../preprints/A-polynomial-time-construction-of-strong-thin-trees-September-23-2026/paper.pdf)

## Scope

The strong thin-tree conjecture asks for spanning trees that cross every cut sparsely relative to the original graph. The formalized result gives one absolute constant $C>0$ such that every finite loopless $k$-edge-connected multigraph with at least two vertices has a spanning tree crossing each nontrivial cut at most $(C/k)$ times the original cut size. Parallel edges remain distinct. No numerical value of $C$ or construction algorithm is asserted.

The strong thin-tree problem asks for a spanning tree that crosses every cut sparsely relative to the original graph. The formalization gives one deterministic polynomial-time algorithm and an absolute constant $C>0$ such that a finite $k$-edge-connected loopless multigraph yields a spanning tree using at most a $C/k$ fraction of the edges of every cut. The input may encode parallel-edge multiplicities in binary, and the running time is polynomial in that binary input length.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Strong thin-tree bound | [StrongThinTree.lean](../ComparatorChallenges/StrongThinTree.lean) |
| Polynomial-time construction of strong thin trees | [AlgorithmicThinTrees.lean](../ComparatorChallenges/AlgorithmicThinTrees.lean) |