Papers With

← All papers
First page of Power-of-two cycles in projective cubic graphs of large edge-width

Power-of-two cycles in projective cubic graphs of large edge-width

Jean-Fran{\c c}ois Culus

math.CO Oct 19, 2026 · v1
formalization combinatorics
Read PDF arXiv abstract
TL;DR
An extension lemma and a sumset inclusion for twelve profiles listed in an appendix were formalized in Lean 4; the main theorem was not formally verified.
Abstract
Heckman and Krakovski proved that every 3-connected cubic planar graph contains a cycle of length 2^m for some 2 $\le$ m $\le$ 7. We extend this to 3-connected cubic graphs embedded in the real projective plane with face-width at least three and edge-width at least 48; the cycle may moreover be taken contractible. The argument passes to the spherical double cover, where the planar theorem provides the cycle inside a subgraph of diameter at most 47, and the condition on the edge-width guarantees that this subgraph projects injectively.
Problem

Heckman and Krakovski showed that every 3-connected cubic planar graph contains a cycle of length 2^m for some 2 ≤ m ≤ 7. The question is whether this extends to cubic graphs embedded in the real projective plane.

Approach

The argument passes to the spherical double cover. There the planar theorem supplies a power-of-two cycle inside a subgraph of diameter at most 47. An edge-width of at least 48 guarantees that this subgraph projects injectively back to the projective plane. Supporting lemmas, namely an extension lemma and a sumset inclusion for twelve profiles, were formalized in Lean 4.

Results

Every 3-connected cubic graph embedded in the projective plane with face-width at least three and edge-width at least 48 contains a contractible cycle of length 2^m for some 2 ≤ m ≤ 7. Only the auxiliary lemmas are machine-checked; the main theorem is not.