{"id":"palomar/PALOMAR-2026-08-29-000014","url":"https://github.com/ukiyois/hs-virial-nbc-identity/tree/6ff2cea17ea9320d8974b76f26bd502b4a4076a9","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-29-000014-v2.json","repo":"https://github.com/ukiyois/hs-virial-nbc-identity","tags":["math.CO","math-ph","msc:05C15","msc:82B05","statistical-mechanics","cluster-expansion","lean-formalization","hard-spheres"],"score":0,"title":"ukiyois/hs-virial-nbc-identity","trust":"high","domain":"math.CO","source":"palomar","authors":["ukiyois"],"reviews":0,"subject":"math.CO","summary":"A kernel-checked Lean formalization of the exact no-broken-circuit volume identity for hard-sphere Mayer cluster integrals and the stronger dimension-three fork-packing upper bound for each tree-owned NBC region. The development proves finite broken-circuit cancellation, the measurable finite-region decomposition, the anchored Euclidean product-measure theorem, and its explicit flat-coordinate transport. Its geometric result is the attachment-aware estimate Vol(NBC_T) <= (17/32)^hardSphereNu T * hardSphereKappa^(k-1), where hardSphereNu T is the maximum cardinality of a packing of pairwise…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-03","reactions":{},"formalized":true,"formalizes":[{"title":"Danus hs-virial verified fact chain: hard-sphere NBC identities","identifier":"","relationship":"adapts"}]}