{"id":"palomar/PALOMAR-2026-10-18-000006","url":"https://github.com/jtraverso/chordal-split-threshold-graphs/tree/ed65dcdc7339767d3e8e412420abbf54eae65ddb","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-18-000006-v1.json","repo":"https://github.com/jtraverso/chordal-split-threshold-graphs","tags":["math.CO","msc:05C75","msc:05C05","chordal-graphs","graph-structure","lean","cographs"],"score":0,"title":"Chordal, split, threshold and cograph structure","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 / Mathlib formalization of classical structure theorems for finite simple graphs. Chordal graphs: every minimal a–b separator is a clique, a nonempty finite chordal graph has a simplicial vertex, and a connected non-complete one has two non-adjacent simplicial vertices (Dirac 1961); a finite graph is chordal iff it has a perfect elimination order (Fulkerson–Gross 1965), iff it is the intersection graph of subtrees of a finite tree (Gavril 1974); a nonempty finite chordal graph has treewidth ω − 1, and every finite graph has ω ≤ tw + 1. Split graphs: split iff the graph and its…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-18","reactions":{},"formalized":true,"formalizes":[{"title":"On rigid circuit graphs","identifier":"doi:10.1007/BF02992776","relationship":"formalizes"},{"title":"Incidence matrices and interval graphs","identifier":"doi:10.2140/pjm.1965.15.835","relationship":"formalizes"},{"title":"The intersection graphs of subtrees in trees are exactly the chordal graphs","identifier":"doi:10.1016/0095-8956(74)90094-X","relationship":"formalizes"},{"title":"Split graphs","identifier":"","relationship":"formalizes"},{"title":"Aggregation of Inequalities in Integer Programming","identifier":"doi:10.1016/S0167-5060(08)70731-3","relationship":"formalizes"}]}