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 a sufficient condition for a finite simple 3-connected cubic bipartite plane graph: if a family of pairwise vertex-disjoint facial 4-cycles leaves at most six vertices uncovered, then the graph is Hamiltonian. The six-vertex case is the main theorem. The remaining cases include a proof that two uncovered vertices are impossible and that four uncovered vertices admit the required matching in the original graph. The paper also gives an infinite family satisfying the condition and examines its relation to earlier sufficient conditions. This record contains the corrected paper PDF, complete LaTeX manuscript source, and the Lean 4 formalization snapshot already released with version 1.1.0. The formalization checks both the six-vertex theorem and the at-most-six consequence with pinned dependencies. Verification and reproduction instructions are included. These conditional results do not resolve Barnette's conjecture in general.