Hamiltonicity of Barnette graphs with at most 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. We prove that a finite simple 3-connected cubic bipartite plane graph is Hamiltonian if pairwise vertex-disjoint facial 4-cycles leave exactly six vertices uncovered. We also prove the at-most-six corollary, including impossibility of two uncovered vertices and existence of a matching in the original graph for four uncovered vertices. The chosen cycles need not include every quadrilateral face; other faces may have arbitrary even lengths. This record contains the revised paper PDF, manuscript source, and matching Lean 4 source snapshot. The formalization machine-checks the six-vertex theorem and at-most-six corollary. Verification notes give the pinned toolchain and full build procedure. These conditional results do not resolve Barnette's conjecture in general.