Small Biplanar Graphs Are 9-Colorable: The Earth–Moon Problem up to 16 Vertices

The Earth–Moon problem asks for the maximum chromatic number of a graph of thickness at most two. The best known general bounds are 9 ≤ χ ≤ 12. Assuming the completeness of Olivier Lalonde's published enumeration of edge-7-critical graphs on 13 vertices, this work proves that every biplanar graph on at most 16 vertices is 9-colorable. Consequently, any biplanar graph with chromatic number at least 10 must have at least 17 vertices. The proof combines the structural theory of critical graphs, Gallai decomposition, the Kostochka–Yancey lower bound, planar edge bounds, and a narrowly isolated computer-assisted step. The 41-edge extremal case is handled theoretically via the characterization of extremal critical graphs as Ore graphs. The remaining 42-edge case is reduced to a unique graph in Lalonde's published enumeration; an explicit K₆ certificate then implies the presence of K₉, which is not biplanar. An accompanying public verification repository provides exact-arithmetic checks, the pinned SHA-256 hash and cardinality of the published census, the graph6 record used by the proof, the explicit clique certificate, and automated continuous verification.