Forest certificates and Hamilton cycles in Barnette graphs with at most six uncovered vertices

Barnette's conjecture asks whether every finite 3-connected cubic bipartite planar graph has a Hamiltonian cycle. We show that, for a finite simple 3-connected cubic bipartite plane graph, pairwise vertex-disjoint facial 4-cycles leaving at most six vertices uncovered force a colour-constrained partition of the big faces into two induced forests. Every edge internal to these forests has an endpoint in a set of at most three big faces of one colour. This certificate yields a Hamiltonian cycle through Florek's criterion. We also give an independent direct proof using residual matchings, connectivity after edge deletion, and expansion of the facial cycles. A verified 66-vertex example attains the three-face bound and fails a simpler two-colour forest condition; an unbounded family realizes the no-matching branch. This record contains the revised paper PDF, complete LaTeX source, reproducibility files, and a pinned Lean 4 snapshot formalizing the exactly-six and at-most-six Hamiltonicity results and the forest certificate. The edge-control refinement and broader two-active-face proposition are proved in the paper. The paper and data are CC BY 4.0; original Lean and Python code is Apache-2.0. These conditional results do not resolve Barnette's conjecture.