{"id":"palomar/PALOMAR-2026-09-25-000010","url":"https://github.com/jfairfaxball-348/TreeStack-Structural-Certificates-for-Stacking-on-Trees/tree/457b88b785e50a749710108a935a661a9d992348","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-25-000010-v1.json","repo":"https://github.com/jfairfaxball-348/TreeStack-Structural-Certificates-for-Stacking-on-Trees","tags":["math.CO","msc:05C05","graph-theory","tree-stacking","lean-formalization"],"score":0,"title":"Tree stacking equals the Csernák--Soukup estimator on nontrivial finite trees","trust":"high","domain":"math.CO","source":"palomar","authors":["John Fairfax-Ball"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 proof of the corrected nontrivial-tree form of the Csernák--Soukup tree-stacking conjecture. For every finite tree with at least two vertices, the exact-size stacking number equals the explicit rooted-distance-and-degree estimator. The one-vertex case is excluded because the source stacking-number convention restricts admissible thresholds to t >= 2 while the displayed estimator is 1 on the one-vertex tree.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-25","reactions":{},"formalized":true,"formalizes":[{"title":"Stacking and clearing in graph pebbling","identifier":"arXiv:2604.22341v1","relationship":"adapts"}]}