{"id":"palomar/PALOMAR-2026-09-30-000023","url":"https://github.com/jfairfaxball-348/ProbStack-Random-Stacking-on-Trees/tree/1897a76956168fba047f5943fa7998601f4fe459","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-30-000023-v1.json","repo":"https://github.com/jfairfaxball-348/ProbStack-Random-Stacking-on-Trees","tags":["math.CO","msc:05C99","graph-pebbling","combinatorics","lean-formalization"],"score":0,"title":"ProbStack — Random Stacking on Trees","trust":"high","domain":"math.CO","source":"palomar","authors":["John Fairfax-Ball"],"reviews":0,"subject":"math.CO","summary":"Lean 4 formalization of a deterministic finite-path necessity theorem for graph-pebbling stackability: a positive-mass nonstackable path configuration above an explicit mass threshold must contain an actual directed integer branch message at most -h. The package also verifies the exact fixed-total corollary at total n*mu, forcing a message at most -(2*mu-1). The project's two-sided random path threshold theorem is not part of this Palomar result.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-30","reactions":{},"formalized":true,"formalizes":[{"title":"ProbStack Session 5/23 global deep-message necessity theorem","identifier":"https://github.com/jfairfaxball-348/ProbStack-Random-Stacking-on-Trees/tree/6b58462042a41125bd8d113168bb51276b2940ef","relationship":"formalizes"},{"title":"TreeStack — Structural Certificates for Stacking on Trees","identifier":"https://github.com/jfairfaxball-348/TreeStack-Structural-Certificates-for-Stacking-on-Trees/tree/f4112f08d42a37c0941bf469ac124621b1f54f22","relationship":"adapts"}]}