{"id":"palomar/PALOMAR-2026-08-21-000002","url":"https://github.com/lennrt/palomar-formalizations/tree/090b3b300ba8ec76fdba09a17f086953d13f2653/zenodo-21890733/palomar","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-21-000002-v2.json","repo":"https://github.com/lennrt/palomar-formalizations","tags":["math.CO","cs.CG","msc:05C10","msc:05C45","msc:68R10","graph-theory","cubic-graphs","lean-formalization","combinatorics"],"score":0,"title":"lennrt/palomar-formalizations","trust":"high","domain":"math.CO","source":"palomar","authors":["Lennart Rudolph"],"reviews":0,"subject":"math.CO","summary":"A kernel-checked certificate for the finite mathematical core of the paper's explicit 16-vertex counterexample. The compared declarations prove cubicity, bipartiteness, connectivity after every deletion of at most two vertices, Hamiltonicity of the displayed cycle, its exact complementary perfect matching, the displayed oriented facial incidence and dual data, Euler's equality, properness and uniqueness up to global permutation of the face coloring, the induced edge-color classes, their unavoidable intersections with the complementary matching, and the instantiated final obstruction. The…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-03","reactions":{},"formalized":true,"formalizes":[{"title":"A Counterexample to Prescribed-Cycle Recovery in Barnette Graphs","identifier":"doi:10.5281/zenodo.21890733","relationship":"formalizes"}]}