{"id":"palomar/PALOMAR-2026-11-04-000009","url":"https://github.com/jtraverso/overfull-critical-graphs/tree/8a59940e734ed5c7a5f749d9e2416f032c1c6372","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-11-04-000009-v1.json","repo":"https://github.com/jtraverso/overfull-critical-graphs","tags":["math.CO","msc:05C15"],"score":0,"title":"Overfullness of critical graphs with small minimum degree (Cao–Chen–Jing–Shan, variant)","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 / Mathlib formalization of Theorem 1.2 of Cao, Chen, Jing and Shan with a weaker constant. overfull_of_critical: if a finite simple graph G is Δ-critical (connected, its line graph is not Δ(G)-colourable, and G − e is Δ(G)-edge-colourable for every edge e) and 3|V(G)| + 7δ(G) ≤ 4Δ(G) + 10, then G is overfull: |E(G)| > Δ(G)·⌊|V(G)|/2⌋. The article assumes 4Δ − 7δ ≥ 3n − 17; the hypothesis here is 4Δ − 7δ ≥ 3n − 10, stronger by 7, because two common-neighbour counts in the article's proof (Case 2 of Section 3 and the fork branch of Case 1) use one more unit of degree than is available…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-11-04","reactions":{},"formalized":true,"formalizes":[{"title":"The overfullness of graphs with small minimum degree and large maximum degree","identifier":"arXiv:2105.05333","relationship":"adapts"},{"title":"On the average degree of edge chromatic critical graphs II","identifier":"","relationship":"formalizes"},{"title":"An improvement to the vertex-splitting conjecture","identifier":"arXiv:2103.05171","relationship":"formalizes"},{"title":"On the chromatic index of multigraphs without large triangles","identifier":"","relationship":"formalizes"},{"title":"Critical graphs with given chromatic class","identifier":"","relationship":"formalizes"}]}