Graph theory and algorithms

A Counterexample to Prescribed-Cycle Recovery in Barnette Graphs

ORCID

Preprintv1.0.0

Abstract

Bekos, Kaufmann, and Pfister asked whether every prescribed Hamiltonian cycle of a Barnette graph can be recovered by choosing the dual spanning tree in the book-embedding algorithm of Alam et al. We answer this question negatively. An explicit 16-vertex Barnette graph has a Hamiltonian cycle whose complementary perfect matching meets all three edge-color classes in the simultaneous edge/face coloring used by the algorithm. Every output of the algorithm contains every edge designated green, independently of the spanning tree. The prescribed cycle omits a green edge under every global color labeling and therefore cannot be an output. We give a plane embedding, a two-expansion construction from the cube, a dependency-free verifier, and a pinned Lean companion that checks the principal finite proof interfaces.

Read manuscript PDF ↗Cite this paperDownload BibTeX

Contribution

Gives a concrete 16-vertex obstruction to recovering every prescribed Hamiltonian cycle through the published book-embedding algorithm.

Formalization scope

partial

What Lean checks

The concrete 16-vertex graph, deletion-connectivity, Hamiltonian cycle, complementary matching, oriented face/dual incidence, Euler relation, face-coloring uniqueness, induced edge colors, and the conditional Property-1 obstruction.

What it does not check

The incidence-to-sphere theorem and the published algorithm’s Property 1 are not formalized. The final theorem assumes that the algorithm’s output contains the admissible green edge class, then proves the obstruction for this prescribed cycle.

This scope is reconciled with the hosted manuscript and pinned project README. The mathematical statements and assumptions in the source determine what the formalization establishes; manuscript revisions may clarify the interpretation of the same proof artifact.

Toolchain
leanprover/lean4:v4.30.0
Reproduce the formalization
git clone https://github.com/lennrt/palomar-formalizations.git
cd palomar-formalizations
git checkout 9437c5e5ba09d6ba95285eaac4532414a84923e1
cd zenodo-21890733/palomar
lake exe cache get
lake build

See the project README for the complete setup, dependencies, and selected declarations.

Citation & version

Lennart Rudolph. (2026). A Counterexample to Prescribed-Cycle Recovery in Barnette Graphs. v1.0.0. Zenodo. https://doi.org/10.5281/zenodo.21890733.

View and copy BibTeX
Download .bib

Hosted manuscript
v1.0.0 ·
All versions DOI
10.5281/zenodo.21890732
Manuscript file integrity

SHA-256 of this exact hosted PDF:

a6f49cd7cb838e0940586bcb0b632b62da4ebaed77eeeac7a0f5362aa3271a5f