{"id":"palomar/PALOMAR-2026-11-01-000022","url":"https://github.com/jtraverso/erdos81-series-notes/tree/01be11e33fc4f416d5ef5df4d71aec936bc48023","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-11-01-000022-v1.json","repo":"https://github.com/jtraverso/erdos81-series-notes","tags":["math.CO","msc:05C70","msc:05C35","msc:05C75"],"score":0,"title":"Two application notes of the Erdős #81 series: realizability transfer and exact chordal stability","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 two research notes of the author's Erdős #81 series, in one package. Note I, \"From realizability certificates to the Erdős 81 bound\": a realizability certificate of Paper V for an auxiliary conflict system whose target is the physical system of copies of K₃ and K₄ in G (conflict when they share an edge, gain C(|K|,2) − 1), with q ≥ 1 classes and budget q·e(G) + cost ≤ q·T + w(X), gives a clique partition of G into pieces of order at most four with at most T pieces (note_I_partition_of_certificate; no chordality); a physical packing with e(G) − g(P) ≤ T…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-11-01","reactions":{},"formalized":true,"formalizes":[{"title":"From realizability certificates to the Erdős 81 bound","identifier":"doi:10.5281/zenodo.23458871","relationship":"formalizes"},{"title":"Exact stability for nearly extremal chordal clique partitions","identifier":"doi:10.5281/zenodo.23458871","relationship":"formalizes"}]}