Hamiltonicity of Barnette graphs with six vertices uncovered by disjoint facial 4-cycles

Barnette's conjecture asks whether every finite 3-connected cubic bipartite planar graph has a Hamiltonian cycle. This preprint studies a sufficient condition for a fixed plane embedding. Let G be a finite simple 3-connected cubic bipartite plane graph, and let Q be a family of pairwise vertex-disjoint facial 4-cycles in that embedding. We prove that if exactly six original vertices of G lie outside the union of the cycles in Q, then G has a Hamiltonian cycle. The family need not contain every quadrilateral face, no restriction is imposed on the lengths of the other faces, and the order of G is unrestricted. This record contains the paper PDF and the corresponding Lean 4 source snapshot for machine checking the main theorem. The source snapshot records its Lean toolchain and pinned dependencies, and the accompanying verification notes explain how to rebuild and check the formal declaration. This is a result under the stated six-uncovered-vertex condition; it does not resolve Barnette's conjecture in general.