Papers With

← All papers
First page of The stacking number of a tree

The stacking number of a tree

John Fairfax-Ball

math.CO Sep 25, 2026 · v1
formalization combinatorics
Read PDF arXiv abstract Code
TL;DR
Proves the tree stacking-number formula conjectured by Csernák and Soukup, with the complete theorem formalized in Lean 4 using Mathlib.
Abstract
The stacking number of a graph is the least integer t >= 2 such that every configuration of t pebbles can be transformed by pebbling moves into a configuration supported on one vertex. We prove that, for every finite tree T with at least two vertices, this number equals the rooted distance-and-degree estimator conjectured by Csernák and Soukup. The proof uses an exact recursive characterization of stackability at a prescribed vertex, an explicit zero-score obstruction, and a weighted cancellation argument for arbitrary nonstackable configurations. The complete theorem is formalized in Lean 4; the formal result has also passed Palomar mechanical verification and is publicly registered as PALOMAR-2026-09-25-000010.
Problem

The stacking number of a graph is the least t>=2 such that every configuration of t pebbles can be transformed via pebbling moves onto a single vertex. Csernák and Soukup conjectured an explicit rooted distance-and-degree estimator formula for trees, verified only computationally up to order seven.

Approach

An exact recursive characterization of stackability at a prescribed vertex is developed via integer branch messages sent across boundary edges recording gain or cost of clearing. An explicit zero-score obstruction configuration of mass estim(T)-1 establishes the lower bound. A weighted cancellation argument on local defect equations gives the upper bound for arbitrary nonstackable configurations, combined with an exact-size threshold lemma. The full theorem is formalized in Lean 4 with a pinned Mathlib revision.

Results

For every finite tree with at least two vertices, stack(T)=estim(T), proving the conjecture for all trees without an order bound. The Lean declaration TreeStack.stack_eq_estim_of_two_le_card uses only the standard axioms propext, Quot.sound and Classical.choice, and passed independent mechanical verification.