{"id":"palomar/PALOMAR-2026-11-01-000021","url":"https://github.com/jtraverso/erdos81-chordal-quantitative-stability/tree/0e1cd910f2e77955cd8165e80fffb6d8dae91378","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-11-01-000021-v1.json","repo":"https://github.com/jtraverso/erdos81-chordal-quantitative-stability","tags":["math.CO","msc:05C70","msc:05C35","msc:05C75"],"score":0,"title":"Clique partitions of chordal graphs: quantitative stability and sharp eventual bounds","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 chordal results of the author's preprint \"Clique partitions with rooted simplicial defect: quantitative stability and sharp eventual bounds\" (Erdős #81 series, Paper IV). With M(n) = ⌊n(n+1)/6⌋: there is b such that every chordal graph on n vertices has a clique partition into pieces of order at most four with at most M(n) + b pieces (Theorem A); for n large every chordal graph on n vertices has one with at most M(n) pieces, and some chordal graph on n vertices has one with exactly M(n) pieces that is optimal among all clique partitions (Theorem B, the…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-11-01","reactions":{},"formalized":true,"formalizes":[{"title":"Clique partitions with rooted simplicial defect: quantitative stability and sharp eventual bounds","identifier":"doi:10.5281/zenodo.23479507","relationship":"formalizes"}]}