{"id":"palomar/PALOMAR-2026-11-01-000006","url":"https://github.com/jtraverso/erdos81-optimal-clique-partitions/tree/719e39baf9d0e356a13f6bfe36b60b4ad5e910d6","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-11-01-000006-v1.json","repo":"https://github.com/jtraverso/erdos81-optimal-clique-partitions","tags":["math.CO","msc:05C70","msc:05C35"],"score":0,"title":"Optimal clique partitions under local perturbations","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 \"Optimal Clique Partitions under Local Perturbations\" (Erdős #81 series, Paper VI). For a graph G on n vertices with a core P of size p = ⌊(n+1)/3⌋, h = Δ(G △ (K_P ∨ I_O)) and u, s, m the numbers of core, crossing and exterior edges: if p ≥ 18h + 1 then cp(G) = cp_{≤4}(G) = s − u − 2m = M(n) + C − A − 2m with M(n) = ⌊n(n+1)/6⌋ (Theorem A), and cp_{≤3}(G) − cp(G) = m (Theorem B); if p ≥ 63h, every assignment of the orders 4 or 5 to the exterior edges is realized by an optimal partition (Theorem C); for p ≥ 16 each…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-11-01","reactions":{},"formalized":true,"formalizes":[{"title":"Optimal Clique Partitions under Local Perturbations","identifier":"doi:10.5281/zenodo.23479507","relationship":"formalizes"}]}