{"id":"palomar/PALOMAR-2026-11-01-000020","url":"https://github.com/jtraverso/erdos81-colorability-realizability-defects/tree/0c2f7dff52e5c578f39191c4905dd12248e7bb9a","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-11-01-000020-v1.json","repo":"https://github.com/jtraverso/erdos81-colorability-realizability-defects","tags":["math.CO","msc:05C70","msc:05C15","msc:90C27"],"score":0,"title":"Colorability and realizability defects in resource-dominated packing relaxations","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 / Mathlib formalization of the main results of the author's preprint \"Colorability and Realizability Defects in Resource-Dominated Packing Relaxations\" (Erdős #81 series, Paper V). For a conflict system (finite objects with a symmetric irreflexive conflict relation) and a multiset X of objects, the loss between fractional and integral packings is bounded by the colourability defect D_q of the conflict graph H[X] of the copies (Lemma 3.1, Corollary 3.2, Theorems 3.3, 3.4, 3.4w), and, more generally, by the cost of a realizability certificate whose classes are realized in a fixed…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-11-01","reactions":{},"formalized":true,"formalizes":[{"title":"Colorability and Realizability Defects in Resource-Dominated Packing Relaxations","identifier":"doi:10.5281/zenodo.23479507","relationship":"formalizes"}]}