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

For finite simple 3-connected cubic bipartite plane graphs, pairwise vertex-disjoint facial 4-cycles leaving at most six original vertices uncovered force a partition of the faces of length at least six into two induced forests satisfying Florek's colour constraints. Every internal edge meets one set of at most three big faces of a single colour. This supplies a structural certificate within Florek's existing Hamiltonicity criterion. A separate direct construction avoids any chosen residual perfect matching and uses every other external edge in the matching branch. An unbounded family realizes the no-matching branch, and a verified 66-vertex example attains the three-face bound. The accompanying Lean 4 source formalizes the exactly-six and at-most-six Hamiltonicity results and the forest certificate, including its three-face bound. The edge-control refinement and infinite-family arguments are proved in the manuscript. These conditional results do not resolve Barnette's conjecture. Manuscript version 1.2.1, editorial revision dated 30 September 2026. Mathematical statements are unchanged. The accompanying Lean software remains version 1.2.0, with an unchanged source archive. The manuscript, figures and example data are CC BY 4.0; original Lean and Python code is Apache-2.0. Third-party dependencies retain their own licenses. OpenAI's ChatGPT assisted with the Lean 4 formalization and with the English translation of author-written text and manuscript editing and review. The author reviewed and edited the resulting material and takes responsibility for the final manuscript and formalization.