{"id":"palomar/PALOMAR-2026-10-27-000024","url":"https://github.com/alialiev78/Polytope_Trees_Lean_Formalization/tree/523f4f928843b4e867a91702d2aea5599a1d126b","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-27-000024-v1.json","repo":"https://github.com/alialiev78/Polytope_Trees_Lean_Formalization","tags":["math.CO","math.GT","msc:05A15","msc:05A19","msc:05C30","msc:57Q15","msc:20B25","msc:05E45"],"score":0,"title":"The Number of Polytope Trees and Beyond — Lean 4 formalization","trust":"high","domain":"math.CO","source":"palomar","authors":["Ali Aliev"],"reviews":0,"subject":"math.CO","summary":"Symmetry-weighted enumeration of finite facet-pairing diagrams and polytope trees: cut-join recurrences, factorial formulas, formal exponential generating functions, local analytic counting series with specified radical branches, binomial identities and asymptotic equivalents. The development also proves unique extension of intrinsic facet isometries for finite spanning flag-regular Euclidean cells, derives their geometric presentation masses, and proves an exponential lower bound for ordinary simplicial triangulation classes from any fixed finite pure triangulation of dimension at least two.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-27","reactions":{},"formalized":true,"formalizes":[{"title":"The Number of Polytope Trees and Beyond","identifier":"https://arxiv.org/abs/2610.33344v1","relationship":"adapts"}]}