The stacking number of a tree
John Fairfax-Ball
math.CO
Sep 25, 2026 · v2
TL;DR
The main stacking-number theorem for trees and the stackability criterion are fully formalized in Lean 4 with Mathlib, audited for axioms, and registered with Palomar.
Abstract
Csernák and Soukup introduced the stacking number of a graph: the least integer $t\ge2$ such that every configuration of $t$ pebbles can be transformed by pebbling moves into a configuration supported on one vertex. They conjectured an explicit formula for the stacking number of a tree in terms of the degrees of its vertices and their distances from a chosen root. We prove this conjecture for every finite tree with at least two vertices. We also show that whether a configuration on a tree can be stacked at a given vertex is decided exactly by the sign of an integer score built from recursive branch messages; consequently, stackability can be tested with a linear number of arithmetic operations. The proof combines this criterion with an explicit zero-score obstruction and a weighted cancellation argument for arbitrary nonstackable configurations. The main theorem and the stackability criterion are formalized in Lean 4, and the main theorem has passed Palomar mechanical verification; it is publicly registered as PALOMAR-2026-09-25-000010.
Problem
Csernák and Soukup conjectured an explicit formula for the stacking number of a finite tree, the least t ≥ 2 such that every configuration of t pebbles can be moved by pebbling moves onto a single vertex. The formula is given in terms of vertex degrees and distances from a root.
Approach
Integer branch messages are defined recursively across edges, giving a rooted score S_r(C). A configuration is stackable at r exactly when S_r(C) > 0, and necessity is proved for arbitrary move orders via a boundary-flux lemma. An explicit zero-score configuration of mass estim(T)−1 shows the lower bound, and a weighted cancellation argument over defect equations gives the upper bound. The whole proof is formalized in Lean 4 (pinned 4.35.0-rc2 plus a pinned Mathlib revision) as TreeStack.stack_eq_estim_of_two_le_card.
Results
The conjecture stack(T) = estim(T) is proved for every finite tree with at least two vertices, and stackability can be tested with a linear number of arithmetic operations. The Lean proof uses only the standard axioms and passed Palomar mechanical verification, including NanoDa kernel replay (PALOMAR-2026-09-25-000010).
