A cubic graph with no (n−1)-cycle

Gordon Royle asked on MathOverflow (question 263706, 2017) whether a cubic graph on n vertices can be Hamiltonian, not bipartite, and have no cycle of length n − 1, and reported that his computer found none on up to 24 vertices.

Yes, on 20 vertices: take K₄ and replace each vertex by a copy of K_{2,3}, attaching the three edges at that vertex to the three vertices of the larger class (Theorem 1). The graph is cubic; it is Hamiltonian, since any two attachments of a block are joined by a path through all five of its vertices; and a triangle of K₄ becomes a 9-cycle. It has no 19-cycle by a count of cycle edges in the block of the missing vertex: twice the edges inside plus the edges leaving is eight, and the edges inside are twice the inner vertices on the cycle. So either four edges leave through three attachments, or none leave and the cycle is trapped in five vertices. The argument works with any Hamiltonian non-bipartite cubic graph in place of K₄ (the prism gives 30 vertices). Why the reported search missed the example is not known; it has girth 4 and 3-edge cuts.

Preprint v1, 9 October 2026, not peer reviewed. For the 20-vertex graph every statement of Theorem 1 is formally verified in Lean 4 (lean/, standard axioms only): the theorem about cycles is proved for every cycle by the counting argument, and only the finite facts about the fixed graph are checked by evaluation. An independent exhaustive search confirms the result. The author used an AI tool (Claude, Anthropic) in this work, as described in the note, and is responsible for its content.